[GHC] #15664: Core Lint error

21 Sep 2018

      #15664: Core Lint error
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.6.1
          Component:  Compiler       |           Version:  8.6.1-beta1
           Keywords:  TypeInType     |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 From
 [https://github.com/VictorCMiraldo/victorcmiraldo.github.io/blob/845e74b59aee...
 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/845e74b59aee...

 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
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler