Panic "mkCoVarLCo" with ConstraintKinds and type-level equality
The following abuse of the type system causes a panic:
{-# LANGUAGE TypeFamilies, DataKinds, ScopedTypeVariables, TypeOperators #-}
import Data.Constraint
data Nat = Zero | Succ Nat
type family Plus (a :: Nat) (b :: Nat) :: Nat
type instance Plus Zero b = b
type instance Plus (Succ a) b = Succ (Plus a b)
type One = Succ Zero
type family (a :: Nat) :==: (b :: Nat) :: Bool
boolToProp :: (a :==: b) ~ True => Dict (a ~ b)
boolToProp = undefined
foo :: forall n. (Succ n :==: Plus n One) ~ True => ()
foo = case (boolToProp :: Dict (Succ n ~ Plus n One)) of
Dict -> ()
Here is the error message:
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 7.7.20120720 for x86_64-apple-darwin):
mkCoVarLCo
<<details unavailable>>
Trac metadata
Trac field | Value |
---|---|
Version | 7.5 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |