Obtaining `Show a` from the context `Show (a,b)`

Question

As the title says, I'm interested in using Show a in a context where I have Show (a,b). This problem easily arises with GADTs as follows:

data PairOrNot a where
  Pair :: (b,c) -> PairOrNot (b,c)
  Not :: a -> PairOrNot a

showFirstIfPair :: Show a => PairOrNot a -> String
showFirstIfPair (Not a) = show a
showFirstIfPair (Pair (b,c)) = show b

The error is:

Could not deduce (Show b) arising from a use of ‘show’
from the context (Show a)
  bound by the type signature for
             showFirstIfPair :: Show a => PairOrNot a -> String
  at app/Main.hs:24:20-50
or from (a ~ (b, c))
  bound by a pattern with constructor
             Pair :: forall b c. (b, c) -> PairOrNot (b, c),
           in an equation for ‘showFirstIfPair’
  at app/Main.hs:26:18-27
Possible fix:
  add (Show b) to the context of the data constructor ‘Pair’
In the expression: show b
In an equation for ‘showFirstIfPair’:
    showFirstIfPair (Pair (b, c)) = show b

I'd think the instance declaration instance (Show a, Show b) => Show (a,b) proves Show element, but I can also imagine that the problem also has something to do with how the typeclass machinery is implemented at runtime.

I've discovered that if we can modify the class definition it's possible to solve this via:

class Show' a where
  show' :: a -> String
  unpair :: a -> Dict (a ~ (b,c)) -> Dict (Show' b, Show' c)

-- An example non-pair instance
instance Show' Int where
  show' i = ""
  unpair = undefined -- This is OK, since no one can construct Dict (Int ~ (b,c))

instance (Show' a, Show' b) => Show' (a,b) where
  show' (a,b) = ""
  unpair _ Dict = Dict -- In this context we have access to Show' for elems

Then at the use site, we fetch the dictionary explicitly:

showFirstIfPair :: Show' a => PairOrNot a -> String
showFirstIfPair (Not a) = show' a
showFirstIfPair (Pair a@(b,c)) = 
  case unpair a Dict of -- This is a Dict (a~(b,c))
    Dict -> show' b -- This is Dict (Show' b,Show' c)

I was wondering if there is a non-intrusive (or just different) way of obtaining Show element. If not, could you explain why exactly this problem is arising?

Answer 1

If you don't mind the restriction that b must always be an instance of Show, then this is a simple solution:

data PairOrNot a where
  Pair :: Show b => (b,c) -> PairOrNot (b,c)
  Not :: a -> PairOrNot a

Answer 2

I've kept trying to see if I can come up with something better, and here's the best I could come up with:

In my original attempt, I've coupled the Show' type class with the instance declaration for pairs. Even though I couldn't find a way around modifying the type class, I've at least managed to generalize this for any instance declaration.

As pointed out in the question's comments instance (Show a, Show b) => Show (a,b) is a one-way implication, but I assumed it could be applied in the other direction as well, given the absence of overlapping instances. Unfortunately GHC doesn't rely on that, but we can assert that ourselves. My intuition can be translated into code: (:=> is from Data.Constraint from the constraints package, and a :=> b means that there is an instance a => b somewhere)

class Show' a where
  show' :: a -> String
  noOverlap :: (b :=> Show' a) => Proxy a -> Dict b

Here, the noOverlap function is a promise that if you can find a constraint b which gives rise to an instance Show' a, I can prove b given Show' a. This promise is equivalent to stating that there will be no overlapping instances for Show'

Now, we need a helper function to actually implement noOverlap

basedOn :: forall k a. (k :=> Show' a, k) => 
             (forall b. (b :=> Show' a) => Proxy a -> Dict b)
basedOn _ = unsafeCoerce (Dict :: Dict k)

What this function does is that, if you call it in a context where you have an instance k :=> Show' a, it will return a function that will return Dict b for any instance b :=> Show' a. We have to use unsafeCoerce to convince GHC that Dict k and Dict b are the same, but as far as I can see, this is a safe use of unsafeCoerce, since the functional dependency a :=> b | b -> a makes sure that there can be only one instance of k :=> Show' a for a given Show' a.

Now, given this helper, here's how you define instances

-- An example non-pair instance
instance () :=> Show' Int where ins = Sub Dict 
instance        Show' Int where
  show' i = ""
  noOverlap = basedOn

instance (Show' a, Show' b) :=> Show' (a,b) where ins = Sub Dict
instance (Show' a, Show' b)  => Show' (a,b) where
  show' (a,b) = ""
  noOverlap = basedOn -- GHC does all the plumbing here

We have to define the :=> instances manually, since GHC doesn't do it automatically, but there's no room for error there. If we give a too weak constraint on the left of a manually defined :=>, ins = Sub Dict will fail to compile and if we give a too strong constraint, then noOverlap = basedOn will fail to compile, so that boilerplate is forced by the compiler.

We can then use noOverlap as follows:

showFirstIfPair :: Show' a => PairOrNot a -> String
showFirstIfPair (Not a) = show' a
showFirstIfPair (Pair a@(b,c)) = 
  -- In this context we have (Show' b, Show' c) :=> Show' a
  case noOverlap Proxy of -- This is a Proxy a
    Dict -> show' b -- This is a Dict (Show' b, Show' c)

The nice thing is that, now we can also go from, say, Show' [a] to Show' a, or any other instance declaration.

Note: You'll need {-# LANGUAGE FlexibleContexts, TypeOperators, RankNTypes, ConstraintKinds, AllowAmbiguousTypes #-} to compile these.

Answer 3

Here's a generalisation of user2297560 that's doesn't require hard-coding Show in the GADT:

{-# LANGUAGE ConstraintKinds, KindSignatures #-}
import GHC.Exts (Constraint)

data PairOrNot (cl :: * -> Constraint) (a :: *) where
  Pair :: (cl b, cl c) => (b,c) -> PairOrNot (b,c)
  Not :: cl a => a -> PairOrNot a

Then you can

showFirstIfPair :: PairOrNot Show a -> String
showFirstIfPair (Not a) = show a
showFirstIfPair (Pair (b,c)) = show b