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 |