Skip to content

Can't unify `k -> Type` with visible dependent quantification that ignores its quantifiee `forall (x :: k) -> Type`

I'm making sure this is intended or not, it is possible to wrap k -> Type in a VDQ that ignores its argument forall (x :: k) -> Type (Dep).

But Indep fails to compile:

{-# Language GADTs                    #-}
{-# Language PolyKinds                #-}
{-# Language RankNTypes               #-}
{-# Language StandaloneKindSignatures #-}

import Data.Kind

type    Dep :: (k -> Type) -> (forall (x :: k) -> Type)
newtype Dep f a where
 Dep :: f a -> Dep f a

{-
• Expected kind ‘forall (x :: k0) -> Type’,
  but ‘f’ has kind ‘k0 -> Type’
• In the first argument of ‘Indep’, namely ‘f’
  In the type ‘Indep f a’
  In the definition of data constructor ‘Indep’
-}
-- type    Indep :: (forall (x :: k) -> Type) -> (k -> Type)
-- newtype Indep f a where
--  Indep :: f a -> Indep f a
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information