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