Guarded Impredicativity

Simon Peyton Jones simonpj at
Fri Jun 28 12:15:24 UTC 2019

Just to amplify: we are very interested to

  *   Get some idea of whether anyone  cares about impredicativity.  If we added it to GHC, would you use it?  Have you ever bumped up Haskell’s inability to instantiate a polymorphic function at a polytype.

  *   Get some idea of whether the particular form of impredicativity described in the paper would be expressive enough for your application.


From: ghc-devs <ghc-devs-bounces at> On Behalf Of Alejandro Serrano Mena
Sent: 28 June 2019 13:12
To: ghc-devs at
Subject: Guarded Impredicativity

Dear all,

We are trying to bring back `ImpredicativeTypes` into GHC by using the ideas in the "Guarded Impredicative Polymorphism" paper [<>].

For now I have produced a first attempt, which lives in<>. It would be great if those interested in impredicative polymorphism could give it a try and see whether it works as expected or not.

The main idea behing "guarded impredicativity" is that you can infer an impredicative instantiation for a type variable in a function call if you have at least one given argument where that type variable appears under a type constructor different from (->).
For example, consider the call `(\x -> x) : ids`, where `ids :: [forall a. a -> a]`. Since in the type of `(:)`, namely `forall a. a -> [a] -> [a]`, the variable `a` appears under the `[]` constructor and that second argument is given, we are allowed to instantiate `a := forall a. a -> a`. On the other hand, if we try to do `ids <> ids`, where `(<>)` is monoid concatenation with type `forall m. Monoid m => m -> m -> m`, we are forced to instantiate `m` with a not-polymorphic type because at no point the variable appears under a type constructor.

Just for reference, the best to get a working clone is to follow these steps:
> git clone --recursive<> impredicative-ghc
> cd impredicative-ghc
> git remote add trupill git at<mailto:git at>
> git fetch trupill
> git checkout trupill master

Thanks very much in advance,

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <>

More information about the ghc-devs mailing list