No, up to now the only changes are in the type checking of applications and variables. However, I guess that it would be possible to give [| id |] the type Code (forall a. a -> a) with a explicit type signature (the system always allows impredicative instantiation is explicitly marked), but without the annotation it would the usual type forall a. Code (a -> a).
El vie., 28 jun. 2019 a las 14:17, Matthew Pickering (< [email protected]>) escribió: > Have you modified how typed quotations are type checked? For example, > with your patch I would hope that > > [| id |] :: Code (forall a . a -> a) > > would be accepted? > > I'll try it out. This patch will have big ramifications for the typed > template haskell community. > > Matt > > 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
