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.

The easiest solution is to change signature of Eq from Eq a => Expr a -> Expr a -> Expr Bool, which allows a in this context to be whichever numeric type (which may or may not be instance of class show), to (Eq a, Show a) => Expr a -> Expr a -> Expr Bool which will allow to construct eq only expression only when comparing expressions of showable type. — Antisthenes
Thank you, this works; however a solution without this additional requirement in the type constructor would be interesting as well — user2656155
With the original type there is no good solution. There is just too little you can do with an existential type. Another way is to restrict Val to a fixed type (or to have multiple Val-like constructors representing a finite set of types). — Li-yao Xia

leftaroundabout leftaroundabout · Accepted Answer · 2017-09-06T18:38:16

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

Haskell GADT 'Show'- instance type-variable deduction

2 Answers