<div dir="ltr"><div>Dear all,</div><div><br></div><div>We are trying to bring back `ImpredicativeTypes` into GHC by using the ideas in the "Guarded Impredicative Polymorphism" paper [<a href="https://www.microsoft.com/en-us/research/publication/guarded-impredicative-polymorphism/" target="_blank">https://www.microsoft.com/en-us/research/publication/guarded-impredicative-polymorphism/</a>].</div><div><br></div><div>For now I have produced a first attempt, which lives in <a href="https://gitlab.haskell.org/trupill/ghc" target="_blank">https://gitlab.haskell.org/trupill/ghc</a>. It would be great if those interested in impredicative polymorphism could give it a try and see whether it works as expected or not.</div><div><br></div><div>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 (->).</div><div>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.<br></div><div><br></div><div>Just for reference, the best to get a working clone is to follow these steps:<br></div><div>> git clone --recursive <a href="https://gitlab.haskell.org/ghc/ghc" target="_blank">https://gitlab.haskell.org/ghc/ghc</a> impredicative-ghc</div><div>> cd impredicative-ghc</div><div>> git remote add trupill git@gitlab.haskell.org:trupill/ghc.git</div><div>> git fetch trupill<br></div><div>> git checkout trupill master</div><div><br></div><div>Thanks very much in advance,</div><div>Alejandro<br></div><div><br></div></div>