Search code examples
haskelltype-inferencegadttype-variables

Haskell GADT 'Show'- instance type-variable deduction

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.

Solution

  • 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