Hi, El vie., 28 jun. 2019 a las 15:19, Matthew Pickering (< [email protected]>) escribió:
> I just tried it and it doesn't currently work. > > [1 of 1] Compiling Id ( Id.hs, interpreted ) > > Id.hs:14:7: error: > • Couldn't match type ‘a0 -> a0’ with ‘forall a. a -> a’ > Expected type: TExpQ (forall a. a -> a) > Actual type: Q (TExp (a0 -> a0)) > • In the Template Haskell quotation [|| id ||] > In the expression: [|| id ||] > In an equation for ‘foo’: foo = [|| id ||] > | > 14 | foo = [|| id ||] > | > > Do you think you could perhaps take a look into fixing it? > I will give it a try. > > PS: If you disable the testsuite on CI (so that the build passes) then > people can download and use the artefacts from your branch rather than > have to build the compiler from source. > Is there an easy way to do this (or a tutorial), better in a way which doesn't break the actual CI pipeline if this is finally merged? Regards, Alejandro > > > On Fri, Jun 28, 2019 at 1:20 PM Alejandro Serrano Mena > <[email protected]> wrote: > > > > 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
