Guarded Impredicativity

[Ryan Scott]

I have another interesting application of guarded impredicativity that
I want to bring up. Currently, GHC #16140 [1] makes it rather
inconvenient to use quantified constraints in type synonyms. For
instance, GHC rejects the following example by default:

    type F f = (Functor f, forall a. Eq (f a))

This is because F is a synonym for a constraint tuple, so mentioning a
quantified constraint in one of its arguments gets flagged as
impredicative. In the discussion for #16140, we have pondered doing a
major rewrite of the code in TcValidity to permit F. But perhaps we
don't need to! After all, the quantified constraint in the example
above appears directly underneath a type constructor (namely, the type
constructor for the constraint 2-tuple), which should be a textbook
case of guarded impredicativity.

I don't have the guarded impredicativity branch built locally, so I am
unable to test if this hypothesis is true. In any case, I wanted to
mention it as another motivating use case.

Ryan S.
-----
[1] https://gitlab.haskell.org/ghc/ghc/issues/16140