Guarded Impredicativity

[Alejandro Serrano Mena]

Dear all,

We are trying to bring back `ImpredicativeTypes` into GHC by using the
ideas in the "Guarded Impredicative Polymorphism" paper [
https://www.microsoft.com/en-us/research/publication/guarded-impredicative-polymorphism/
].

For now I have produced a first attempt, which lives in
https://gitlab.haskell.org/trupill/ghc. 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 https://gitlab.haskell.org/ghc/ghc impredicative-ghc
> cd impredicative-ghc
> git remote add trupill git at gitlab.haskell.org:trupill/ghc.git
> git fetch trupill
> git checkout trupill master

Thanks very much in advance,
Alejandro
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20190628/64b754be/attachment.html>