[GHC] #7090: Panic "mkCoVarLCo" with ConstraintKinds and type-level equality

[GHC]

#7090: Panic "mkCoVarLCo" with ConstraintKinds and type-level equality
--------------------------------+-------------------------------------------
 Reporter:  goldfire            |          Owner:                  
     Type:  bug                 |         Status:  new             
 Priority:  normal              |      Component:  Compiler        
  Version:  7.5                 |       Keywords:  ConstraintKinds 
       Os:  Unknown/Multiple    |   Architecture:  Unknown/Multiple
  Failure:  Compile-time crash  |       Testcase:                  
Blockedby:                      |       Blocking:                  
  Related:                      |  
--------------------------------+-------------------------------------------
 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>>
 }}}

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