Conditionally derive Show for existential type parameterized on type constructor

Question

Suppose I have a data type like this:

{-# LANGUAGE RankNTypes #-}
data X a = forall b. Show b => X (a b)

I would like to derive Show (X a), but of course I can only do so if there is an instance of Show (a b). I'm tempted to write

{-# LANGUAGE StandaloneDeriving #-}
deriving instance Show (a b) => Show (X a)

but unfortunately the type variable b is not available in the instance context because it is bound by the forall.

My next attempt was to move the Show (a b) context into the forall in the data type definition, like so:

data X a = forall b. Show (a b) => X (a b)
deriving instance Show (X a)

This compiles, but unfortunately now I've lost the ability to construct an X with an unshowable (a b).

Is there any way to allow X to be constructed with any (a b), and then conditionally derive Show (X a) only if (a b) is showable?

Answer 1

This is a deficiency in the Prelude classes. There's a nice way around it though embodied in the prelude-extras package. I'll outline it below.

We'd like to create a higher-kinded Show class. It looks like this

class Show1 a where
  show1 :: Show b => a b -> String

Then we can at least accurately express our desired constraint like

deriving instance Show1 a => Show (X a)

Unfortunately, the compiler does not yet have enough information to achieve this derivation. We need to show that (Show b, Show1 a) is enough to derive Show (a b). To do so we'll need to enable some (scary, but sanely-used) extensions

{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE OverlappingInstances      #-}

instance (Show b, Show1 a) => Show (a b) where
  show = show1

And now that we have that proof the compiler will be able to derive what we need

data X a = forall b . Show b => X (a b)
deriving instance Show1 a => Show (X a) 

Answer 2

I would take a similar but slightly different approach to J. Abrahamson's answer.

Precisely what you ask for can't be done, because type classes need to be resolved statically, but the existence of Show (a b) might be dynamic depending on the instantation of b. This instantiation is hidden inside the X value and therefore not visible to the type checker when you have nothing but an X b of unknown origin.

It would be nice to write a condition on a like Show (a b) exists whenever Show b does, because then the existence of Show (a b) isn't actually dependent on b as we already know that Show b is always true.

We can't write that condition directly, but we can express something like it using GADTs:

{-# LANGUAGE GADTs #-}
data ShowDict a where
    ShowDict :: Show a => ShowDict a

The ShowDict a type provides a sort of reification of the Show a class - it's something we can pass around and define functions over.

In particular we can now define a Show1 class that expresses the condition Show (a b) whenever we have a Show b:

class Show1 a where
    show1Dict :: ShowDict b -> ShowDict (a b)

And now we can define Show (X a) in terms of Show1, by constructing ShowDict (a b) and then pattern-matching on it to reveal the Show instance:

{-# LANGUAGE ScopedTypeVariables #-}
instance Show1 a => Show (X a) where
    show (X (v :: a b)) =
       case show1Dict ShowDict :: ShowDict (a b) of
           ShowDict -> "X (" ++ show v ++ ")"

A more complete implementation would also include the other members of Show (showsPrec and showList).

The nice thing about this solution is that we can easily define Show1 for [], automatically reusing the underlying Show instance:

instance Show1 [] where
    show1Dict ShowDict = ShowDict

I also prefer to avoid the very generic Show (a b) instance from J. Abrahamson's answer, but the downside of having to put the logic in the Show instance for X is that we end up having to implement it manually rather than getting the auto-derived behaviour for the constructor.