# The quantified constraint trick

Posted on September 21, 2022

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à.

(Gist of this example)

## 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.

1. AFAICT there is no way around that with `GHC.Generics`. Incoherent instances can be avoided with kind-generics.↩︎

2. `gsolomap` accepts one function parameter. There is also `gmultimap` which accepts arbitrarily many functions.↩︎