How to apply wildcard in constraint in Haskell?

Question

It sounds trivial but I can't find out what I'm supposed to do.

The following is my type definition:

data CDeq q a = Shallow (q a)
              | Deep{ hq   ⦂ q a
                    , susp ⦂ CDeq q (q a)
                    , tq   ⦂ q a }

and I want it to have an instance of Show.

Since GHC doesn't allow deriving here, I just tried to write one myself:

instance (Show a, Show ????) => Show (CDeq q a) where
    ....

but I got stuck.

I don't know how to represent that for all type v, (q v) can be shown in Haskell.

I can't simply do the following:

instance (Show a, Show (q a)) => Show (CDeq q a) where
    ....

since to show CDeq q (q a), Show (q (q a)) is required, then Show (q (q (q a))) is required, then on and on.

So I am wondering is there a syntax such that I can express the meaning I stated up there?

I once thought forall could be the solution to this, but it doesn't work:

instance (Show a, forall v. Show (q v)) => Show (CDeq q a)

Answer 1

@Cirdec's already accepted answer is a great pragmatic answer for this use case. I wanted to write a bit about more general techniques (especially the Data.Constraint.Forall mentioned in a comment, since that almost works for this use case but doesn't quite, and there's another thing from constraints that does work), but I wanted to also try to explain a bit about why this isn't directly possible first and what Show1, Forall, and Lifting do to work around that (they're each different trade offs). So it got a little long, apologies.

---

By standard Haskell mechanisms you can't have such a "wildcard" constraint. The reason is that Show makes a constraint from a type, with potentially a different instance (with different method definitions) for each type you could apply it to.

When your code requires a Show (CDeq q a) instance and finds instance (Show a, Show ????) => Show (CDeq q a), that means it now also needs to find an instance for Show a and Show ????.

Show a is easy; either a has already been chosen as some concrete type like Int, and it can use the Show instance for that type (or error if there isn't one in scope). Or your code was in a function that was polymorphic in a; in that case there must have been a Show a constraint on the function you wrote, so the compiler will just rely on the caller having chosen some particular a and passed in the Show a instance definition.

But the wildcard constraint Show ???? is different. We're not talking about a concrete type here, so that path to resolution isn't going to work. And we're not even talking about a polymorphic constraint in the sense that there's a type variable the caller would choose (in that case we could punt the problem of choosing a single instance dictionary to the caller).

What you need is to be able to show q a, and q (q a), and q (q (q a), etc. But each of those could have its own instance! The types are gone at runtime, so the compiler can't even attempt to round up all of those instances (or require the caller to pass in an unbounded number of instances) and emit code that switches between which show it calls. It needs to emit code that only calls one version of show; either a specific one from a specific instance it's been able to choose, or one that is passed in by the caller to the function.

One way to workaround this is with an alternative type class like Show1. Here the "unit of overloading" is on the * -> * type constructor. It's impossible to make a Show1 instance for types like Int (they're not the right shape), but a single Show1 q instance is applicable to all types of the form q a, so you don't need an unbounded number of instances to support q a, q (q a), q (q (q a)), etc anymore.

But there also are Show instances that are polymorphic in some type variables. For example the list instance is Show a => Show [a]; knowing that this instance exists (and there aren't any overlapping instances), we know we'll be using the same instance for [a], [[a]], [[[a]]], etc. If we could somehow write a constraint that required a polymorphic instance like that.

There's no direct way to say we want a polymorphic instance - the constraint language only allows us to ask for instances for particular types, or particular types that the caller chooses. But the Data.Forall module in the constraints package (https://hackage.haskell.org/package/constraints), which @Cirdec suggested in a comment, uses clever tricks internally to provide a few ways of doing this.¹ Here's an example of how that would look:

{-# LANGUAGE FlexibleContexts
           , ScopedTypeVariables
           , TypeApplications
           , TypeOperators
  #-}

module Foo where

import Data.Constraint ( (:-), (\\) )
import Data.Constraint.Forall (ForallF, instF)

data Nested q a = Stop | Deeper a (Nested q (q a))

data None a = None

instance Show (None a)
  where show None = "None"

instance (Show a, ForallF Show q) => Show (Nested q a)
  where show Stop = "Stop"
        show (Deeper a r) = show a ++ " " ++ show r
                              \\ (instF @Show @q @a)

The constraint ForallF Show q represents forall a. Show (q a).² But it's not that constraint directly, so we can't just derive Show using this; we need to write an instance manually so we can do some massaging.

A ForallF constraint gives us access to instF which is of type forall p f a. ForallF p f :- p (f a). The :- is a type of the constraints package; values of type c :- d represent a proof that when the constraint c holds the constraint d also holds (or in terms of instance dictionaries: it contains a dictionary for d that's parameterised on a dictionary for c). So ForallF p f :- p (f a) is a proof that when we have ForallF p f we can get p (f a). Type application syntax is a less verbose way of pinning down the types at which we're using instF, we want the left side of :- to tie back to the ForallF Show q that we know we have from the instance constraint. That means the right hand side will give us a Show (q a), as we needed! The \\ operator just takes an expression on the left and an c :- d on the right, and basically connects c and d instances for us; the expression will be evaluated with access to a dictionary for d, but the overall expression only needs c.

Here's an example of use:

λ Deeper 'a' (Deeper None (Deeper None Stop))
'a' None None Stop
it :: Nested None Char

Hurrah! But why did I use None? What happens when we try it with nested lists?

λ :t Deeper [] (Deeper [] Stop)
Deeper [] (Deeper [] Stop) :: Nested [] [t]

λ Deeper [] (Deeper [] Stop)

<interactive>:65:1: error:
    • No instance for (Show
                         (Data.Constraint.Forall.Skolem
                            (Data.Constraint.Forall.ComposeC Show [])))
        arising from a use of ‘print’
    • In a stmt of an interactive GHCi command: print it

Drat. What went wrong? Well, our polymorphic Show instance for lists is actually Show a => Show [a]. The instance head is polymorphic, so it applies to all types of forms [a]. But it also needs the extra constraint that Show a holds, so it's not truly polymorphic. Basically what happens is the internal unexported thing in Data.Constraint doesn't have an instance for Show (it can't have any instances for the technique to work), so we get the error above. And that's actually a good thing; dictionaries for [a] contain a nested dictionary for a, so the trick of getting an instance we know is polymorphic and then unsafeCoercing it to the right type wouldn't be applicable here. ForallF only works to find instances that are completely polymorphic, with no restrictions at all.

But there is one more thing the constraints package has to offer here! Data.Constraint.Lifting gives us a class Lifting p f, that represents the idea "p (f a) holds whenever p a holds". The idea that the constraint p "lifts through" the type constructor f. This is actually exactly the notion you needed, since you can just apply it recursively to nest arbitrarily many depths of q.

{-# LANGUAGE FlexibleContexts
           , ScopedTypeVariables
           , TypeApplications
           , TypeOperators
  #-}

module Foo where

import Data.Constraint ( (:-), (\\) )
import Data.Constraint.Lifting ( Lifting (lifting) )

data Nested q a = Stop | Deeper a (Nested q (q a))

instance (Show a, Lifting Show q) => Show (Nested q a)
  where show Stop = "Stop"
        show (Deeper a r) = show a ++ " " ++ show r
                              \\ (lifting @Show @q @a)

Here the lifting method of the class Lifting is doing basically what instF was doing before. lifting :: Lifting p f => p a :- p (f a), so when we have Lifting Show q and we have Show a, then we can use \\ and lifting (used at the right type) to get the Show (q a) dictionary we need to recursively invoke show.

Now we can show Nested applied to list types:

λ Deeper [] (Deeper [[True]] Stop)
[] [[True]] Stop
it :: Nested [] [Bool]

Data.Constraint.Lifting does have a lot of predefined instances for things in the prelude, but you'll likely to have to write your own instances. Fortunately this pretty much is generally a matter of writing:

instance Lifting SomeClass MyType
  where lifting = Sub Dict

The instance resolver does all the actual work for you, provided your type really does allow that class to be "lifted through" it.

---

¹ My understanding of the code in that module is not 100% complete (and the full details are a bit involved to make it as safe as possible), but basically the technique is to apply a class to a hidden unexported thing and capture the dictionary. Since no third-party instance could have actually referenced our unexported thing, the only way an instance could be resolved is if it was actually polymorphic and would work for anything. So then the captured dictionary can just be unsafeCoerced to apply to any type you like.

² There are a few other variants of Forall* for representing different "shapes" of polymorphism in the constraint. I believe you can't make a one-size-fits-all version because you have to not mention the variable you're being polymorphic over, which means you can't actually use the constraint applied, you have to have something that takes the class as a parameter as well as all of the non-polymorphic parameters and applies them together in a particular fashion.

Answer 2

There's a class Show1 in Prelude.Extras to represent "for all type v, (q v) can be shown".

class Show1 f where
  showsPrec1 :: Show a => Int -> f a -> ShowS
  default showsPrec1 :: (Show (f a), Show a) => Int -> f a -> ShowS
  showsPrec1 = showsPrec
  ...

You can use this to write a show instance for CDeq q a.

instance (Show a, Show1 q) => Show (CDeq q a) where
    ....

Where you would use show or showsPrec on a q x you'll instead use show1 or showsPrec1.

If you use these, you should also provide instances for CDeq q.

instance (Show1 q) => Show1 (CDeq q) where
    showsPrec1 = showsPrec