[GHC] #14554: Core Lint error mixing

[GHC]

#14554: Core Lint error mixing
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.2.1
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 While trying to deeply embed ''Singletons''-style defunctionalization
 symbol application using the code from
 [http://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1014&context=compsci_pubs
 System FC with Explicit Kind Equality], I ran into the following `-dcore-
 lint` error:

 {{{#!hs
 {-# Language UndecidableInstances, DataKinds, TypeOperators,
 KindSignatures, PolyKinds, TypeInType, TypeFamilies, GADTs, LambdaCase,
 ScopedTypeVariables #-}

 import Data.Kind
 import Data.Proxy

 type a ~> b = (a, b) -> Type

 type family (@@) (f::k ~> k') (a::k)::k'

 data IdSym0 :: Type ~> Type

 type instance IdSym0 @@ 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') = IK k ~> IK k'

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

 zero :: TyRep X a -> IT a
 zero = \case
   TFnApp TID a -> undefined
 }}}

 {{{
 $ ghci -ignore-dot-ghci -dcore-lint ~/hs/123-bug.hs
 GHCi, version 8.3.20171122: http://www.haskell.org/ghc/  :? for help
 [1 of 1] Compiling Main             ( /home/baldur/hs/123-bug.hs,
 interpreted )
 ghc-stage2: panic! (the 'impossible' happened)
   (GHC version 8.3.20171122 for x86_64-unknown-linux):
         ASSERT failed!
   Bad coercion hole {a2UN}: (IT
                                (a_a1S5 |> Sym (TY (Sym co_a2UC))_N) |>
 D:R:IK[0])
                             (IT (a_a1S5 |> Sym (TY (Sym co_a2UC))_N) |>
 D:R:IK[0])
                             nominal
                             <(IT (a_a1S5 |> Sym (TY (Sym co_a2UC))_N) |>
 D:R:IK[0])>_N
                             IT (a_a1S5 |> Sym (TY (Sym co_a2UC))_N)
                             IT (a_a1S5[ssk:3] |> Sym (TY (Sym co_a2UC))_N)
                             nominal
   Call stack:
       CallStack (from HasCallStack):
         callStackDoc, called at compiler/utils/Outputable.hs:1205:22 in
 ghc:Outputable
         assertPprPanic, called at compiler/typecheck/TcMType.hs:305:105 in
 ghc:TcMType
   Call stack:
       CallStack (from HasCallStack):
         callStackDoc, called at compiler/utils/Outputable.hs:1147:37 in
 ghc:Outputable
         pprPanic, called at compiler/utils/Outputable.hs:1203:5 in
 ghc:Outputable
         assertPprPanic, called at compiler/typecheck/TcMType.hs:305:105 in
 ghc:TcMType

 Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

 >
 }}}

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