GADT pattern matching

Question

I created a GADT for expressions. When I map a template to constrained constructors, typechecker cannot infer constraints on type variables used in constructor constraints. I think the code and error message are more clear.

{-# LANGUAGE GADTs, MultiParamTypeClasses #-} import Data.Word data Expr a where Value :: a -> Expr a Cast :: (Castable ab) => Expr a -> Expr b class Castable ab where cast :: a -> b instance Castable Word64 Word32 where cast = fromIntegral instance (Show a) => Show (Expr a) where show (Cast e) = "Cast " ++ show e -- ERROR 

The error I am getting is:

 gadt.hs:16:30: Could not deduce (Show a1) arising from a use of `show' from the context (Show a) bound by the instance declaration at gadt.hs:15:10-34 or from (Castable a1 a) bound by a pattern with constructor Cast :: forall b a. Castable ab => Expr a -> Expr b, in an equation for `show' at gadt.hs:16:9-14 Possible fix: add (Show a1) to the context of the data constructor `Cast' or the instance declaration In the second argument of `(++)', namely `show e' In the expression: "Cast " ++ show e In an equation for `show': show (Cast e) = "Cast " ++ show e 

---

Edit: if I comment on an instance of Show (Expr a) and add the following code, it works fine:

 eval :: Expr a -> a eval (Value a) = a eval (Cast e) = cast $ eval e main = do let bigvalue = maxBound `div` 2 + 5 :: Word64 e = Cast (Value bigvalue) :: Expr Word32 v = eval e putStrLn "typechecks." print (bigvalue, v) 

I would like the show instance to basically print something like Cast (Value bigvalue) .

Answer 1

 Cast :: (Castable ab) => Expr a -> Expr b 

So here:

 instance (Show a) => Show (Expr a) where show (Cast e) = "Cast " ++ show e -- ERROR 

Cast e is of type Expr a . We have a restriction of Show a , and it is this instance that implies Show (Expr a) , so we can call show for things like Expr a .

But e not of type Expr a . Cast takes an argument of any type Expr a1 and gives you Expr a (renaming type variables to stay consistent with what we say in the instance), so e is of type Expr a1 . We do not have a show restriction for type a1 , and we require Show a1 mean Show (Expr a1) , so there is no way to show e .

And there is no way to add such a restriction to the show instance, because type a1 not displayed in type Cast e . It seems like you should use GADT here; you intentionally threw away all the information about the type of thing Cast was applied to (except that Castable a1 a ), and declared the result simply Expr a .