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