Forall constraints

Question

How do I write a forall constraint, for example for some type families F and G:

forall x y. G (F x y) ~ (x, y) 

Is it possible using Edward A. Kmett Constraints package? And if so could a small example be provided? I presume I need to use Forall.

Answer 1

Yes, this is possible using constraints. Be careful, however! The equality you claim is unlikely to hold with enough generality for constraints if the type families are non-trivial. Consider, in particular, whether the type families successfully reduce when x and y are stuck type families

type family X where {}
type family Y where {}

Also, I see that your particular desired constraint has no free variables whatsoever. Hopefully, it's just an example; an actual closed constraint like that is unlikely to be useful.

---

The fundamental type family in Data.Constraint.Forall is Forall. This particular example might be handled a bit more conveniently using ForallT, but it's most important to understand how to use Forall.

Generally, Forall p means forall x . p x. That doesn't sound very general, but it actually is, if you build up your p step by step. You seek

forall x y. G (F x y) ~ (x, y)

Start by defining a class expressing the relationship you seek.

class G (F x y) ~ (x, y) => C x y
instance G (F x y) ~ (x, y) => C x y

Now you can go step by step, defining

class Forall (C x) => D x
instance Forall (C x) => D x

(which you can read as D x = forall y . C x y)

and then using Forall D (i.e., forall x . D x) to express your constraint. You'll need to use inst to get the Dict (D x) and again to get the Dict (C x y).