Here is a nix one liner to test the current state of the branch. nix run -f https://github.com/mpickering/ghc-artefact-nix/archive//master.tar.gz ghc-head-from -c ghc-head-from https://gitlab.haskell.org/mpickering/ghc/-/jobs/114593/artifacts/raw/ghc-x86_64-fedora27-linux.tar.xz
On Fri, Jun 28, 2019 at 1:12 PM Alejandro Serrano Mena <[email protected]> wrote: > > 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 [email protected]:trupill/ghc.git > > git fetch trupill > > git checkout trupill master > > Thanks very much in advance, > Alejandro > > _______________________________________________ > ghc-devs mailing list > [email protected] > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs _______________________________________________ ghc-devs mailing list [email protected] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
