I believe the restriction is because of impredicativity.. My idea was to temporarily break the CI config whilst the tests don't pass. I can make a MR for you if this would be acceptable.
Matt On Fri, Jun 28, 2019 at 3:27 PM Alejandro Serrano Mena <[email protected]> wrote: > > After having a quick look, I think it could be done easily in terms of type > checking. Alas, there's some code in TcSplice.hs which insists anyway on > having a quantifier-free type: > > tcTExpTy :: TcType -> TcM TcType > tcTExpTy exp_ty > = do { unless (isTauTy exp_ty) $ addErr (err_msg exp_ty) > ; ... } > where > err_msg ty > = vcat [ text "Illegal polytype:" <+> ppr ty > , text "The type of a Typed Template Haskell expression must" <+> > text "not have any quantification." ] > > Does anybody have any pointers about why this restriction is in place? > > Regards, > Alejandro > > 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? >> >> 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. >> >> Cheers, >> >> Matt >> >> 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
