Haskell GADT 'Show'- instance type-variable deduction

Question

This code

{-# LANGUAGE GADTs #-}

data Expr a where
    Val :: Num a => a -> Expr a
    Eq :: Eq a => Expr a -> Expr a -> Expr Bool

eval :: Expr a -> a
eval (Val x) = x
eval (Eq x y) = (eval x) == (eval y)

instance Show a => Show (Expr a) where
    show (Val x) = "Val " ++ (show x)
    show (Eq x y) = "Eq (" ++ (show y) ++ ") (" ++ (show x) ++ ")"

fails to compile with the following error message:

Test.hs:13:32: error:
    * Could not deduce (Show a1) arising from a use of `show'
      from the context: Show a
        bound by the instance declaration at test.hs:11:10-32
      or from: (a ~ Bool, Eq a1)
        bound by a pattern with constructor:
                   Eq :: forall a. Eq a => Expr a -> Expr a -> Expr Bool,
                 in an equation for `show'
        at test.hs:13:11-16
      Possible fix:
        add (Show a1) to the context of the data constructor `Eq'
    * In the first argument of `(++)', namely `(show y)'
      In the second argument of `(++)', namely
        `(show y) ++ ") (" ++ (show x) ++ ")"'
      In the expression: "Eq (" ++ (show y) ++ ") (" ++ (show x) ++ ")" Failed, modules loaded: none.

Commenting out the last line fixes the issue and inspecting the type of Expr in GHCi reveals, that, instead of inferring Eq to be of type Eq a => (Expr a) -> (Expr a) -> Expr Bool, GHC actually infers it to be Eq a1 => (Expr a1) -> (Expr a1) -> Expr Bool for data Expr a where .... This explains the error message, since instance Show a => Show (Expr a) where ... won't enforce a1 to be an instance of Show.

However I do not understand, why GHC chooses to do so. If I had to make a guess, I'd say it has something to do with Eq returning a value, that doesn't depend on a at all and thus GHC "forgetting" about a, once Eq returns a Expr Bool. Is this - at least sort of - what is happening here?

Also, is there a clean solution to this? I tried several things, including trying to "force" the desired type via InstanceSigs and ScopedTypeVariables doing something like this:

instance Show a => Show (Expr a) where
    show :: forall a. Eq a => Expr a -> String
    show (Eq x y) = "Eq (" ++ (show (x :: Expr a)) ++ ") (" ++ (show (y :: Expr a)) ++ ")"
    ...

, but with no success. And since I'm still a Haskell novice, I'm not even sure, if this could somehow work anyways, due to my initial guess why GHC doesn't infer the "correct"/desired type in the first place.

EDIT:

Ok, so I decided to add a function

extract (Eq x _) = x

to the file (without a type signature), just to see, what return type it would have. GHC again refused to compile, but this time, the error message contained some information about skolem type variables. A quick search yielded this question, which (I think?) formalizes, what I believe the issue to be: Once Eq :: Expr a -> Expr a -> Expr Bool returns a Expr Bool, a goes "out of scope". Now we don't have any information left about a, so extract would have to have the signature exists a. Expr Bool -> a, since forall a. Expr Bool -> a won't be true for every a. But because GHC doesn't support exists, type-checking fails.

Answer 1

One option is not requiring a Show a superconstraint.

instance Show (Expr a) where
  showsPrec p (Eq x y) = showParen (p>9)
       $ ("Eq "++) . showsPrec 10 x . (' ':) . showsPrec 10 y

Of course this somewhat kicks the stone down the road, because now you can not write

  showsPrec p (Val x) = showParen (p>9) $ ("Val "++) . showsPrec 10 x

anymore – now the leaf-value is not Show constrained. But here you can hack your way around this by making the Num constraint a bit stronger:

data Expr a where
    Val :: RealFrac a => a -> Expr a
    Eq :: Eq a => Expr a -> Expr a -> Expr Bool
instance Show (Expr a) where
  showsPrec p (Val x) = showParen (p>9) $ ("Val "++)
          . showsPrec 10 (realToFrac x :: Double)

Well, that is a big hack, and at that point you might as well use simply

data Expr a where
    Val :: Double -> Expr Double
    Eq :: Eq a => Expr a -> Expr a -> Expr Bool

(or whatever other single type best fits your number requirements). That's not a good solution.

To retain the ability to store numbers of any type in Expr leaves, yet be able to constrain them to Show if desired, you need to be polymorphic on the constraint.

{-# LANGUAGE ConstraintKinds, KindSignatures #-}

import GHC.Exts (Constraint)

data Expr (c :: * -> Constraint) a where
    Val :: (Num a, c a) => a -> Expr a
    Eq :: Eq a => Expr a -> Expr a -> Expr Bool

Then you can do

instance Show (Expr Show a) where
  showsPrec p (Val x) = showParen (p>9) $ ("Val "++) . showsPrec 10 x
  showsPrec p (Eq x y) = showParen (p>9)
       $ ("Eq "++) . showsPrec 10 x . (' ':) . showsPrec 10 y

Answer 2

I will only explain this point.

However I do not understand, why GHC chooses to do so.

The issue is, one can write a custom type with a Num and Eq instance, but no Show one.

newtype T = T Int deriving (Num, Eq) -- no Show, on purpose!

Then, this type checks:

e1 :: Expr T
e1 = Val (T 42)

as does this:

e2 :: Expr Bool
e2 = Eq e1 e1

However, it should be clear that e1 and e2 can not be showed. To print these, we would need Show T, which is missing.

Further, the constraint

instance Show a => Show (Expr a) where
      -- ^^^^^^

is useless here, since we do have Show Bool, but this is not enough to print e2 :: Expr Bool.

This is the problem of existential types: you get what you pay for. When we construct e2 = Eq e1 e2 we only have to "pay" the constraint Eq T. Hence, when we pattern match Eq a b we only get Eq t back (where t is a suitable type variable). We do not get to know whether Show t holds. Indeed, even if we did remember t ~ T, we would still lack the required Show T instance.