Re: Guarded Impredicativity

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 (< matthewtpickering@gmail.com>) 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 wrote:

...

No, up to now the only changes are in the type checking of applications

...

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 (< matthewtpickering@gmail.com>) 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 wrote:

...

Dear all,

We are trying to bring back `ImpredicativeTypes` into GHC by using

...

...

...

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

...

...

...

Just for reference, the best to get a working clone is to follow

and variables. the ideas in the "Guarded Impredicative Polymorphism" paper [ https://www.microsoft.com/en-us/research/publication/guarded-impredicative-p... ]. the variable appears under a type constructor. these steps:

...

...

...

...

git clone --recursive https://gitlab.haskell.org/ghc/ghc impredicative-ghc cd impredicative-ghc git remote add trupill git@gitlab.haskell.org:trupill/ghc.git git fetch trupill git checkout trupill master

Thanks very much in advance, Alejandro

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs