# The quantified constraint trick

My favorite Haskell trick is how to use quantified constraints with type families.
Kudos to *Iceland_jack* for coming up with it.

## Quantified constraints and type families

`QuantifiedConstraints`

is an extension from GHC 8.6 that lets us
use `forall`

in constraints.

It lets us express constraints for instances of higher-kinded types like `Fix`

:

```
newtype Fix f = Fix (f (Fix f))
deriving instance (forall a. Eq a => Eq (f a)) => Eq (Fix f)
```

Other solutions existed previously, but they’re less elegant:

```
deriving instance Eq (f (Fix f)) => Eq (Fix f)
instance Eq1 f => Eq (Fix f) where ...
```

It also lets us say that a monad transformer indeed transforms monads:

```
class (forall m. Monad m => Monad (t m)) => MonadTrans t where
lift :: m a -> t m a
```

(Examples lifted from the GHC User Guide on `QuantifiedConstraints`

, section Motivation.)

One restriction is that the conclusion of a quantified constraint cannot mention a type family.

```
type family F a
-- (forall a. C (F a)) -- Illegal type family application in a quantified constraint
```

A quantified constraint can be thought of as providing a local instance, and they are subject to a similar restriction on the shape of instance heads so that instance resolution may try to match required constraints with the head of existing instances.

Type families are not matchable: we cannot determine whether an applied
type family `F a`

matches a type constructor `T`

in a manner satisfying the
properties required by instance resolution (“coherence”). So type families
can’t be in the conclusion of a type family.

## The quantified constraint trick

### Step 1

To legalize type families in quantified constraints,
all we need is a *class synonym*:

```
class C (F a) => CF a
instance C (F a) => CF a
```

That `CF a`

is equivalent to `C (F a)`

, and `forall a. CF a`

is legal.

### Step 2?

Since GHC 9.2, Step 1 alone solves the problem. It Just Works™. And I don’t know why.

Before that, for GHC 9.0 and prior, we also needed to hold the compiler’s hand and tell it how to instantiate the quantified constraint.

Indeed, now functions may have constraints of the form `forall a. CF a`

,
which should imply `C (F x)`

for any `x`

.
Although `CF`

and `C (F x)`

are logically related, when `C (F x)`

is required,
that triggers a search for instances of the class `C`

, and not the `CF`

which
is provided by the quantified constraint.
The search would fail unless some hint is provided to the compiler.

When you require a constraint `C (F x)`

, insert a type annotation mentioning
the `CF x`

constraint (using the `CF`

class instead of `C`

).

`_ {- C (F x) available here -} :: CF x => _`

Inside the annotation (to the left of `::`

), we are given `CF x`

, from which `C (F x)`

is inferred as a superclass. Outside the annotation, we are requiring `CF x`

,
which is trivially solved by the quantified constraint `forall a. CF a`

.

### Recap

```
-- Mixing quantified constraints with type families --
class C a
type family F a
-- forall a. C (F a) -- Nope.
class C (F a) => CF a -- Class synonym
instance C (F a) => CF a
-- forall a. CF a -- Yup.
-- Some provided function we want to call.
f :: C (F t) => t
-- A function we want to implement using f.
g :: (forall a. CF a) => t
g = f -- OK on GHC >= 9.2
g = f :: CF t => t -- Annotation needed on GHC <= 9.0
```

The part of that type annotation that really matters is the constraint. The rest of the type to the right of the arrow is redundant. Another way to write only the constraint uses the following identity function with a fancy type:

```
with :: forall c r. (c => r) -> (c => r)
with x = x
```

So you can supply the hint like this instead:

```
g :: forall t. (forall a. CF a) => t
g = with @(CF t) f
```

## Application: *generic-functor*

What do I need that trick for? It comes up in generic metaprogramming.

Imagine deriving `Functor`

for `Generic`

types (no `Generic1`

, which is not as
general as you might hope). One way is to implement the following class on
generic representations:

```
class RepFmap a a' rep rep' where
repFmap :: (a -> a') -> rep -> rep'
```

A type constructor `f :: Type -> Type`

will be a `Functor`

when its
generic representation (`Rep`

) implements `RepFmap a a'`

…
for all `a`

, `a'`

.

```
-- Class synonym for generically derivable functors
class (forall a. Generic (f a), forall a a'. RepFmap a a' (Rep (f a) ()) (Rep (f a') ())) => GFunctor f
instance ... -- idem (class synonym)
-- Wait a second...
```

But that is illegal, because the type family `Rep`

occurs in the conclusion of
a quantified constraint.

Time for the trick! We give a new name to the conclusion:

```
class RepFmap a a' (Rep (f a) ()) (Rep (f a') ()) => RepFmapRep a a' f
instance ... -- idem (class synonym)
```

And we can use it in a quantified constraint:

```
-- Now this works!
class (forall a. Generic (f a), forall a a'. RepFmapRep a a' f) => GFunctor f
instance ... -- idem (class synonym)
```

To obtain the final generic implementation of `fmap`

, we wrap `repFmap`

between `to`

and `from`

.

```
gfmap :: forall f a a'. GFunctor f => (a -> a') -> f a -> f a'
gfmap f =
with @(RepFmapRep a a' f) -- Hand-holding for GHC <= 9.0
to @_ @() . repFmap f . from @_ @()) (
```

Et voilà.

## Appendix: Couldn’t we do this instead?

If you’ve followed all of that, there’s one other way you might try defining
`gfmap`

without `QuantifiedConstraints`

, by just listing the three constraints
actually needed in the body of the function.

```
-- Dangerous gfmap!
gfmap ::
Generic (f a) =>
Generic (f a') =>
RepFmap a a' (Rep (f a) ()) (Rep (f a') ()) =>
a -> a') -> f a -> f a'
(gfmap f = to @_ @() . repFmap f . from @_ @()
```

This is okay as long as it is only ever used to implement `fmap`

as in:

`fmap = gfmap`

Any other use voids a guarantee you didn’t know you expected.

The thing I haven’t told you is that `RepFmap`

is implemented with…
incoherent instances!^{1} In fact, this `gfmap`

may behave differently
depending on how it is instantiated *at compile time*.

For example, for a functor with a field of constant type:

```
data T a b = C Int a b
deriving Generic
```

`gfmap @(T a) @b @b'`

where `a`

, `b`

and `b'`

are distinct type variables
behaves like `fmap`

should. But `gfmap @(T Int) @Int @Int`

will unexpectedly apply its argument function to every field.
They all have type `Int`

, so a function `Int -> Int`

can and will be applied to
all fields.

I could demonstrate this if I had implemented `RepFmap`

…
Luckily, there is a more general version of this “dangerous `gfmap`

” readily
available in my library
*generic-functor*.
It can be very incoherent, but if you follow some rules, it can also be very
fun to use.

### Playing with fire

`gsolomap`

^{2} is a function from *generic-functor* that can implement
`fmap`

, and much more.

```
fmapT :: (b -> b') -> T a b -> T a b'
fmapT = gsolomap
```

Map over the first parameter if you prefer:

```
firstT :: (a -> a') -> T a b -> T a' b
firstT = gsolomap
```

Or map over both type parameters at once:

```
bothT :: (a -> a') -> T a a -> T a' a'
bothT = gsolomap
```

I don’t know what to call this, but `gsolomap`

also does what you might guess
from this type:

```
watT ::
a -> a') ->
(T (a , a ) ((a -> a') -> Maybe a ) ->
T (a', a') ((a' -> a ) -> Maybe a')
watT = gsolomap
```

It’s important to specialize `gsolomap`

with *distinct type variables*
(`a`

and `a'`

).
You cannot refactor code by inlining a function if its body uses `gsolomap`

,
as it risks breaking that requirement.

### Witnessing incoherence

For an example of surprising result caused by incoherence, apply the `fmapT`

defined above to some concrete arguments. See how the result changes then you
replace `fmapT`

with its definition, `gsolomap`

.

```
fmapT ((+1) :: Int -> Int) (C 0 0 0) == C 0 0 1 :: T Int Int
gsolomap ((+1) :: Int -> Int) (C 0 0 0) == C 1 1 1 :: T Int Int -- Noooooo...
```

(Gist of those `gsolomap`

(counter)examples)

This is why `gfmap`

’s signature should use quantified constraints:
this guarantees that when the `RepFmap`

constraint is solved,
the first two parameters are going to be *distinct type variables*,
thanks to the universal quantification (`forall a a'`

).
Thus, incoherence is hidden away.

Following that recipe, *generic-functor* contains *safe* implementations of
`Functor`

, `Foldable`

, `Traversable`

, `Bifunctor`

, and `Bitraversable`

.

In particular, the type of `gfmap`

guarantees that it has a unique
inhabitant satisfying `gfmap id = id`

, and this property is quite
straightforward to check by visual inspection of the implementation.

After all, `gfmap`

will essentially do one of three things:
(1) it will be `id`

on types that don’t mention the type parameters
in its function argument `a -> a'`

, (2) it will apply the provided function
`f`

, or (3) it will `fmap`

(or `bimap`

, or `dimap`

) itself through a type
constructor. In all cases (with some inductive reasoning for (3)),
if `f = id`

, then `gfmap f = id`

.

```
gfmap f = id
gfmap f = f
gfmap f = fmap (gfmap f)
```

The dangerous `gfmap`

(without `QuantifiedConstraints`

) or `gsolomap`

fail this
property, because the extra occurrences of `a`

and `a'`

in its constraint make
their signatures have a different “shape” from `fmap`

.

The trade-off is that those safe functions can’t do the same crazy things
as `gsolomap`

above.