Guarded Impredicativity

Artem Pelenitsyn a.pelenitsyn at
Fri Jul 19 15:22:19 UTC 2019

Hello Ryan,

Your example seems to work out of the box with the GI branch.

With the oneliner Matthew posted before:
nix run -f \
ghc-head-from -c ghc-head-from \
It is really easy to check. Also, I didn't see anywhere mentioned that one
need to provide -XImpredicativeTypes. The whole example, therefore, is:

{-#LANGUAGE ImpredicativeTypes, ConstraintKinds #-}

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

Best, Artem

On Fri, 19 Jul 2019 at 09:18, Ryan Scott < at> wrote:

> 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]
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <>

More information about the ghc-devs mailing list