Pattern Matching on GADTs

Question

I've created a GADT for expressions. When I pattern match on constructors that have constraints, the typechecker is unable to deduce constraints on the type variables used in the constructor's constraints. I think the code and error message are more elucidating.

{-# LANGUAGE GADTs, MultiParamTypeClasses #-}
import Data.Word

data Expr a where
  Value :: a -> Expr a
  Cast :: (Castable a b) => Expr a -> Expr b

class Castable a b 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 get:

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 a b => 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 out the Show (Expr a) instance 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 want the show instance to basically print something like Cast (Value bigvalue).

Answer 1

Cast :: (Castable a b) => 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 Show a constraint, and by this very instance that implies Show (Expr a), so we can call show on things of type Expr a.

But e is not of type Expr a. Cast takes an argument of any type Expr a1 and gives you an Expr a (renaming the type variables to stay consistent with what we're talking about in the instance), so e is of type Expr a1. We don't have a Show constraint for the type a1, and we require Show a1 to imply Show (Expr a1), so there's no way to show e.

And there's no way to add such a constraint in the Show instance, because the type a1 doesn't appear in the type of Cast e. That seems to be the whole point of using a GADT here; you've deliberately thrown away all information about the type of the thing that Cast was applied to (other than the fact that Castable a1 a holds), and declared the result to simply be Expr a.