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