Infinite loop/panic with an existential type.
The symptoms of this bug are quite similar to #14723 (closed), but I don't know if the cause is exactly the same, ergo a new report.
To reproduce:
- Make
T.hs
{-# LANGUAGE DataKinds, ExistentialQuantification, GADTs, PolyKinds, TypeOperators #-}
module T where
import Data.Kind
data Elem :: k -> [k] -> Type where
Here :: Elem x (x : xs)
There :: Elem x xs -> Elem x (y : xs)
data EntryOfVal (v :: Type) (kvs :: [Type]) = forall (k :: Type). EntryOfVal (Elem (k, v) kvs)
- Compile it with
ghc T.hs -ddump-tc-trace
# etc.
checkExpectedKind
*
TYPE t_aXd[tau:1]
<*>_N
kcLHsQTyVars: not-cusk
EntryOfVal
[]
[(k_aW0 :: Type)]
[]
[k_aW0[sk:1]]
*ghc: panic! (the 'impossible' happened)
(GHC version 8.4.3 for x86_64-apple-darwin):
kcConDecl
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
- Append the following to
T.hs
(not minimized, sorry)
type family EntryOfValKey (eov :: EntryOfVal v kvs) :: Type where
EntryOfValKey ('EntryOfVal (_ :: Elem (k, v) kvs)) = k
type family GetEntryOfVal (eov :: EntryOfVal v kvs) :: Elem (EntryOfValKey eov, v) kvs where
GetEntryOfVal ('EntryOfVal e) = e
type family FirstEntryOfVal (v :: Type) (kvs :: [Type]) :: EntryOfVal v kvs where
FirstEntryOfVal v ((k, v) : _) = 'EntryOfVal Here
FirstEntryOfVal v (_ : kvs) = 'EntryOfVal (There (GetEntryOfVal (FirstEntryOfVal v kvs)))
- Compile with a plain
ghc T.hs
- Wait until bored, then knock the compiler out of its infinite loop by killing it.
- Compile again with
ghc T.hs -ddump-tc-trace
# etc.
checkExpectedKind
*
TYPE t_aYg[tau:1]
<*>_N
kcLHsQTyVars: not-cuskghc: panic! (the 'impossible' happened)
(GHC version 8.4.3 for x86_64-apple-darwin):
kcConDecl
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
Found while trying to answer this SO question.
Trac metadata
Trac field | Value |
---|---|
Version | 8.4.3 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |