Need a better error message

[sweirich]

wg28.hs:60:12: Couldn't match type ‘k7’ with ‘k1’ ‘k7’ is a rigid type variable bound by the type signature for eqtycon :: Tycon a -> Tycon b -> Maybe (a :~: b) at wg28.hs:60:12ghc-stage2: panic! (the 'impossible' happened) (GHC version 7.11.20150420 for x86_64-apple-darwin): No skolem info: k1_a3QV

I need this error to motivate heterogeneous equality. Here's the code:

import Data.Type.Equality import GHC.Exts import Data.Type.Bool import Data.Proxy

{- Part I: Dynamic Typing in a Statically Typed Language -}

dynIf :: Dynamic -> a -> a -> a dynIf (Dyn (TCon TBool) True) t = t dynIf (Dyn (TCon TBool) False) f = f dynIf (Dyn ) = error "runtime type error"

dynApply :: Dynamic -> Dynamic -> Dynamic dynApply (Dyn (TApp (TApp (TCon TFun) t1) t2) f) (Dyn t3 x) = case eqtype t1 t3 of Just Refl -> Dyn t2 (f x) dynApply (Dyn ) _ = error "runtime type error"

dynFst :: Dynamic -> Dynamic dynFst (Dyn (TApp (TApp (TCon TProd) t1) t2) (x1,)) = Dyn t1 x1 dynFst (Dyn _) = error "runtime type error"

data Dynamic where Dyn :: Typerep a -> a -> Dynamic

data Tycon (a :: k) where TBool :: Tycon Bool TFun :: Tycon (->) TProd :: Tycon (,) TMaybe :: Tycon Maybe

data Typerep (a :: k) where TCon :: Tycon c -> Typerep c TApp :: Typerep a -> Typerep b -> Typerep (a b)

eqtycon :: forall (k1 :: ) (k2:: ) (a :: k1) (b :: k2). Tycon a -> Tycon b -> Maybe (a :~: b) eqtycon TBool TBool = Just Refl eqtycon TFun TFun = Just Refl eqtycon TProd TProd = Just Refl eqtycon TMaybe TMaybe = Just Refl

eqtype :: Typerep a -> Typerep b -> Maybe (a :~: b) eqtype (TCon c1) (TCon c2) = eqtycon c1 c2 eqtype (TApp a1 b1) (TApp a2 b2) = case eqtype a1 a2 of Just Refl -> case eqtype b1 b2 of Just Refl -> Just Refl Nothing -> Nothing Nothing -> Nothing

[goldfirere]

Do you need this fixed by 2.8? And if you say -fprint-explicit-kinds, you should get a more informative (but maybe too informative) error message. Workaround: omit the explicit quantification.

[sweirich]

I'd rather not have a "panic! the impossible happened" in the 2.8 demo. :-) At least, not on purpose.

I'll try to remember to omit the type annotation when it's live. That does make the error message go away.

[goldfirere]

Fixed now.