Core Lint error
From Generic Programming of All Kinds,
{-# Language RankNTypes, TypeOperators, DataKinds, PolyKinds, GADTs, TypeInType, TypeFamilies #-}
{-# Options_GHC -dcore-lint #-}
import Data.Kind
import GHC.Exts
import Data.Function
data Ctx :: Type -> Type where
E :: Ctx(Type)
(:&:) :: a -> Ctx(as) -> Ctx(a -> as)
type family
Apply(kind) (f :: kind) (ctx :: Ctx kind) :: Type where
Apply(Type) a E = a
Apply(k -> ks) f (a:&:as) = Apply(ks) (f a) as
data ApplyT kind :: kind -> Ctx(kind) -> Type where
A0 :: a
-> ApplyT(Type) a E
AS :: ApplyT(ks) (f a) as
-> ApplyT(k -> ks) f (a:&:as)
type f ~> g = (forall xx. f xx -> g xx)
unravel :: ApplyT(k) f ~> Apply(k) f
unravel (A0 a) = a
unravel (AS fa) = unravel fa
gives a core lint error
$ ghci -ignore-dot-ghci hs/443.hs > /tmp/bug.log