Core Lint error mixing

While trying to deeply embed Singletons-style defunctionalization symbol application using the code from System FC with Explicit Kind Equality, I ran into the following -dcore-lint error:

{-# 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

> 

Trac metadata

Trac field	Value
Version	8.2.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture