Automatically deriving show instances for GADTs

Question

Assume I have a complex GADT which with many hidden type parameters as constructors:

data T where
  A :: Num n => n -> T
  B :: (Num n, Integral m) => n -> m -> T
  C :: Floating a => [a] -> T
  -- and so on
  Z :: Num n => n -> n -> T

I want to make this datatype showable without having to manually write the instance. Problem is, that since Show isn't a superclass of Num anymore, adding a simple deriving instance Show T isn't enough for the compiler to infer that it has to add Show constraints to all the internal hidden type parameters.

For each hidden type parameter, it outputs something like

Could not deduce (Show n) arising from a use of 'showsPrec'
from the context Num n
  bound by a pattern with constructor
             A :: forall n. Num n => n -> T
...
Possible fix:
  add (Show n) to the context of the data constructor 'A'

Adding a Show constraint to the datatype isn't an option either, since it limits the possible inhabitants of T. It seems like deriving instanec Show T should introduce the constraint Show on the hidden data types, although I am not sure.

How can I go about this?

If adding the constraint will limit the inhabitants, the deriving mechanism certainly won't do it for you, nor would you want it to. — Lazersmoke
@Lazersmoke I mean adding the constraints to the derived instance. This doesn't limit inhabitants, it only constructs the Show instance in a coherent way. — ThreeFx
there is no good Show instance for T, no matter what you do, unless you restrict all tyvars (including existentials) to Show. — Lazersmoke
If the A constructor is allowed to contain a non-showable number, how would you expect to show such T value? — chi

luqui luqui · Accepted Answer · 2017-05-22T19:27:19

I had an interesting thought, not sure how practical it is. But if you want T to be showable when the parameters are showable, but also usable with not showable parameters, you could parameterize T over a constraint, using ConstraintKinds.

{-# LANGUAGE GADTs, ConstraintKinds #-}

import Data.Kind

data T :: (* -> Constraint) -> * where
    A :: (Num n, c n) => n -> T c
    B :: (Num n, c n, Integral m, c m) => n -> m -> T c
    ...

Then T Show will be showable... maybe

deriving instance Show (T Show)

(with StandaloneDeriving extension) will work, but at the very least, T is showable in principle and you could write the instance manually.

Though my practical advice is to reify the existentials. An existential type is equivalent to the collection of its observations. For example, if you had a class like

class Foo a where
   getBool :: a -> Bool
   getInt  :: a -> Int

then the existential

data AFoo where
   AFoo :: Foo a => a

is exactly equivalent to (Bool,Int), because the only thing you can do with a Foo whose type you don't know is call getBool on it or getInt on it. You use Num in your datatype, and Num has no observations, since if you have an unknown a with Num a, the only thing you can do by calling methods of Num is get more as out, and nothing ever concrete. So your A constructor

A :: (Num n) => n -> T

gives you nothing and you might as well just say

A :: T

Integral, on the other hand, has toInteger as an observation. So you could probably replace

B :: (Num n, Integral m) => n -> m -> T

with

B :: Integer -> T

(we lost the n argument and replaced m with Integer). I don't think this is technically equivalent since we could have implemented its operations differently than Integral does, but we're getting pretty technical at this point and I doubt you have need for it (I'd be interested in how if you do).

Automatically deriving show instances for GADTs

1 Answers