[GHC] #15664: Core Lint error

[GHC]

#15664: Core Lint error
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:  (none)
            Type:  bug               |               Status:  closed
        Priority:  normal            |            Milestone:  8.6.1
       Component:  Compiler          |              Version:  8.6.1-beta1
      Resolution:  fixed             |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:  indexed-
                                     |  types/should_compile/T15664
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Description changed by Iceland_jack:

Old description:

> From
> [https://github.com/VictorCMiraldo/victorcmiraldo.github.io/blob/845e74b59aee5a322b6cdd1e45355db16a30d8af/data/hask2018_draft.pdf
> Generic Programming of All Kinds],
>
> {{{#!hs
> {-# Language RankNTypes, TypeOperators, DataKinds, PolyKinds, GADTs,
> TypeInType, TypeFamilies #-}
>
> {-# Options_GHC -dcore-lint #-}
>
> --
> https://github.com/VictorCMiraldo/victorcmiraldo.github.io/blob/845e74b59aee5a322b6cdd1e45355db16a30d8af/data/hask2018_draft.pdf
>
> 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
> }}}

New description:

 From [https://dl.acm.org/citation.cfm?id=3242745 Generic Programming of
 All Kinds],

 {{{#!hs
 {-# 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
 }}}

--

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15664#comment:5>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler