[GHC] #14556: Core Lint error: Ill-kinded result in coercion

5 Dec 2017

      #14556: Core Lint error: Ill-kinded result in coercion
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.3
           Keywords:  TypeInType     |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:  #14554
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 {{{#!hs
 {-# Language UndecidableInstances, DataKinds, TypeOperators,
 KindSignatures, PolyKinds, TypeInType, TypeFamilies, GADTs, LambdaCase,
 ScopedTypeVariables #-}

 import Data.Kind
 import Data.Proxy

 data Fn a b where
   IdSym :: Fn Type Type

 type family
   (@@) (f::Fn k k') (a::k)::k' where
   IdSym @@ a = a

 data KIND = X | FNARR KIND KIND

 data TY :: KIND -> Type where
   ID    :: TY (FNARR X X)
   FNAPP :: TY (FNARR k k') -> TY k -> TY k'

 data TyRep (kind::KIND) :: TY kind -> Type where
   TID    :: TyRep (FNARR X X)  ID
   TFnApp :: TyRep (FNARR k k') f
          -> TyRep k            a
          -> TyRep k'           (FNAPP f a)

 type family
   IK (kind::KIND) :: Type where
   IK X            = Type
   IK (FNARR k k') = Fn (IK k) (IK k')

 type family
   IT (ty::TY kind) :: IK kind where
   IT ID          = IdSym
   IT (FNAPP f x) = IT f @@ IT x

 zero :: TyRep X a -> IT a
 zero = undefined
 }}}

 which gives Core lint error when run with `ghci -ignore-dot-ghci -dcore-
 lint` (8.3.20171122) attached.

 It compiles fine with

 {{{#!hs
 zero :: TyRep X a -> IT a
 zero = zero
 }}}

 but fails with `zero = let x = x in x`. See #14554.

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14556
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler