Guarded Impredicativity

Ryan Scott at
Fri Jul 19 21:39:33 UTC 2019

Good to know. Thanks for checking!

Ryan S.

On Fri, Jul 19, 2019 at 11:22 AM Artem Pelenitsyn
<a.pelenitsyn at> wrote:
> 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

More information about the ghc-devs mailing list