There are a few times in my Haskelling that I’ve wanted to use universal quantification to specify a constraint. Earlier this year, I went ahead and asked glasgow-haskell-users about it, and thus learned about the `Data.Constraint.Forall`

module in Edward Kmett’s `constraints`

package. He uses an interesting mechanism for extra robustness in there that took me a while to appreciate. Over the next few posts, I explain his mechanism and then demonstrate a path toward even more robustness that I’ve been discussing with him. It was initially inspired by SPJ’s idea for “Fixing `Any`

” and some discussions with my lab mate Neil Sculthorpe. My hopes for it were raised when Kmett noticed its resemblance to Hilbert’s ε operator.

My lab mate Neil also learned me some domain theory, which I’ll use to (hopefully correctly) discuss a subtlety of GHC’s type equality that derails one of our early attempts.

This draft post ended up quite long, so I split it in three. Find a break down and links at the bottom of this one.

### Objective: Universally quantified constraints

Here’s the general form of quantification that I’m discussing in this post.

`example :: (forall a. p a) => ... -- not valid in GHC 7.6.1`

The constraint is a *universally quantified constraint*. In it, we have quantified over the predicate `p`

, by saying for how many of its possible arguments it must be satisfiable: all of them.

The *need* for quantified constraints arises when you attempt to work with an existentially quantified type that is not constrained as much as you would like it to be. For example, somewhere within an expression, I open up a `Box`

and want to act on its contents with some class method, say `mappend`

.

```
data Box t = forall a. Box (t a)
-- ill-typed!
-- example (Box x) = Box (x `mappend` x)
--
-- No instance for (Monoid (t a)) arising from a use of `mappend'
-- Possible fix: add an instance declaration for (Monoid (t a))
```

This error is pointing out that we don’t know enough about the existential type variable (*ie* `a`

) that is encapsulated by `Box`

to gaurantee we get a monoid when you tuck that variable inside some `t`

.

I know two ways to make this well-typed. One is to change the binding of the existential type variable. We would update the definition of `Box`

.

```
data Box t = forall a. Monoid (t a) => Box (t a)
-- inferred: example :: Box t -> Box t
example (Box x) = Box (x `mappend` x)
```

But that’s a bit dissatisfying. Perhaps we use `Box`

in other parts of our program in ways that are now ill-typed. Or maybe during development we learn that we need other properties of `t a`

; we’ll have to glom them into the constraint inside `Box`

too. Do note, though, that this is a simple fix, and might work well for you in the future. In particular, if your constraint actually depends directly on the existential type variable, it’s your only option. But future-you also might prefer to use a universally quantified constraint, if future-you can.

Here’s a little bit of prep work, pulling in Kmett’s `constraints`

package and putting a thin wrapper on one of its combinators.

```
-- Kmett's constraints on Hackage
import Data.Constraint (Constraint, (:-), (\\))
import Data.Constraint.Forall (ForallF, instF)
-- thin wrapper around Data.Constraint.Forall (instF)
instF_ :: Predicate p -> Proxy (t a) -> ForallF p t :- p (t a)
instF_ _ _ = instF
data Predicate (a :: * -> Constraint) = Predicate
data Proxy (a :: *) = Proxy
proxy :: a -> Proxy a
proxy _ = Proxy
```

The `instF`

function provides evidence (*eg* a type class dictionary) for the constraint `p (t a)`

, given evidence for the constraint `ForallF p t`

. Notice how it is polymorphic in `a`

; that’s the key. My wrapper just let’s me tidily specify some of the type arguments `instF`

is expecting.

Here’s how to put `instF`

to work in our example. Note that `Box`

is back to its original definition.

```
data Box t = forall a. Box (t a) -- as originally
-- inferred, but tidied by hand:
-- example :: ForallF Monoid t => Box t -> Box t
example (Box x) = Box (x `mappend` x)
\\ instF_ (Predicate :: Predicate Monoid) (proxy x)
```

Read the constraint `ForallF Monoid t`

as `forall a. Monoid (t a)`

. The idea is that we don’t want the invocation of `mappend`

to have anything to do with the existential type variable `a`

. We want to instead require that the relevant `Monoid`

instance for `t`

is parametric in `t`

’s argument: it works for all `a`

.

Stepping back a bit, there might be some greater significance/usefulness to this quantifier. The general benefit is that we can now build constraints over higher-kinded parameters out of constraints over lower-kinded parameters. One place where this would be handy is in Oleg Kiselyov’s `Haskell1`

sublanguage. I had only the foggiest recollection of that article when writing this post, but Cale Gibbard, Jason Dagit, and Daniel Peebles helped me track it down in the #haskell IRC channel — thanks, guys! In that article Oleg makes a `Monad`

ish “class” that explicitly has the carrier as a class argument. Using a universal quantifier, we could recover the normal `Monad`

constraint as a quantification of his.

```
-- a constraint synonym (via `XConstraintKinds`)
type Monad m = (forall a. C (RET m a), forall a b. C (BIND m a b))
```

OK. That’s the hook.

### End of Part 1

Aww! Just before we get to the juicy parts: `instF`

involves `Unsafe.Coerce.unsafeCoerce`

! Kmett put some cleverness in `Data.Constraint.Forall`

that guards rather well against the unsafeness; it is very practically safe.

In Part 2, I first explain the naïve direct approach to defining the `Forall`

constraint synonym, and we see why it’s not as safe as Kmett’s mechanism. I also show how to subvert his mechanism, which motivates the most robust definition for `Forall`

that I know of, given in Part 3. I then discuss some details of the GHC type system, focusing mostly on an elusive “a bottom type”. We end up discussing Hilbert’s ε operator a bit, thanks to Kmett’s eye for recognizing those important sort of things.