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).

It can't deduce that b is an instance of Show I guess, this compiles: ideone.com/BWtyIR and so does this ideone.com/6KiB3W — Wes
What behavior are you expecting? The type in the Cast value is existential, so you don't know anything about, e.g. how to show it. Your current GADT is essentially equivalent to something like data Expr a = Value a | Cast (Expr a). You could add a Show constraint but I suspect that's a case of treating the symptom, and that what you should really do is take a step back and think about what you're trying to do in the first place. — shachaf
I agree with shachaf, I'm not sure what you actually want here. — Wes
@Wes: Your code compiles but you changed the type of the Cast constructor. — nitromaster101
To avoid confusion is GADTs it's best to keep the result types of the constructors as consistent as possible. In this case Cast :: (Castable b a) => Expr b -> Expr a would probably have been enough for you to understand what the problem was. — augustss

Ben Ben · Accepted Answer · 2013-07-31T23:53:28

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.

Pattern Matching on GADTs

1 Answers