<div dir="ltr"><div>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:</div><div><br></div><div><div style="color:rgb(108,118,128);background-color:rgb(250,250,250);font-family:Ubuntu Mono;font-weight:normal;font-size:16px;line-height:22px;white-space:pre"><div><span style="color:rgb(242,174,73)">tcTExpTy</span><span style="color:rgb(108,118,128)"> </span><span style="color:rgb(250,141,62)">::</span><span style="color:rgb(108,118,128)"> </span><span style="color:rgb(57,158,230)">TcType</span><span style="color:rgb(108,118,128)"> </span><span style="color:rgb(250,141,62)">-></span><span style="color:rgb(108,118,128)"> </span><span style="color:rgb(57,158,230)">TcM</span><span style="color:rgb(108,118,128)"> </span><span style="color:rgb(57,158,230)">TcType</span></div><div><span style="color:rgb(108,118,128)">tcTExpTy exp_ty</span></div><div><span style="color:rgb(108,118,128)"> </span><span style="color:rgb(237,147,102)">=</span><span style="color:rgb(108,118,128)"> </span><span style="color:rgb(250,141,62)">do</span><span style="color:rgb(108,118,128)"> { unless (isTauTy exp_ty) </span><span style="color:rgb(237,147,102)">$</span><span style="color:rgb(108,118,128)"> addErr (err_msg exp_ty)</span></div><div><span style="color:rgb(108,118,128)"> ; ... }</span></div><div><span style="color:rgb(108,118,128)"> </span><span style="color:rgb(250,141,62)">where</span></div><div><span style="color:rgb(108,118,128)"> err_msg ty</span></div><div><span style="color:rgb(108,118,128)"> </span><span style="color:rgb(237,147,102)">=</span><span style="color:rgb(108,118,128)"> vcat [ text </span><span style="color:rgb(134,179,0)">"Illegal polytype:"</span><span style="color:rgb(108,118,128)"> </span><span style="color:rgb(237,147,102)"><+></span><span style="color:rgb(108,118,128)"> ppr ty</span></div><div><span style="color:rgb(108,118,128)"> </span><span style="color:rgb(108,118,128)">,</span><span style="color:rgb(108,118,128)"> text </span><span style="color:rgb(134,179,0)">"The type of a Typed Template Haskell expression must"</span><span style="color:rgb(108,118,128)"> </span><span style="color:rgb(237,147,102)"><+></span></div><div><span style="color:rgb(108,118,128)"> text </span><span style="color:rgb(134,179,0)">"not have any quantification."</span><span style="color:rgb(108,118,128)"> ]</span></div></div></div><div><br></div><div>Does anybody have any pointers about why this restriction is in place?</div><div><br></div><div>Regards,</div><div>Alejandro<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">El vie., 28 jun. 2019 a las 15:19, Matthew Pickering (<<a href="mailto:matthewtpickering@gmail.com">matthewtpickering@gmail.com</a>>) escribió:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">I just tried it and it doesn't currently work.<br>
<br>
[1 of 1] Compiling Id ( Id.hs, interpreted )<br>
<br>
Id.hs:14:7: error:<br>
• Couldn't match type ‘a0 -> a0’ with ‘forall a. a -> a’<br>
Expected type: TExpQ (forall a. a -> a)<br>
Actual type: Q (TExp (a0 -> a0))<br>
• In the Template Haskell quotation [|| id ||]<br>
In the expression: [|| id ||]<br>
In an equation for ‘foo’: foo = [|| id ||]<br>
|<br>
14 | foo = [|| id ||]<br>
|<br>
<br>
Do you think you could perhaps take a look into fixing it?<br>
<br>
PS: If you disable the testsuite on CI (so that the build passes) then<br>
people can download and use the artefacts from your branch rather than<br>
have to build the compiler from source.<br>
<br>
Cheers,<br>
<br>
Matt<br>
<br>
On Fri, Jun 28, 2019 at 1:20 PM Alejandro Serrano Mena<br>
<<a href="mailto:trupill@gmail.com" target="_blank">trupill@gmail.com</a>> wrote:<br>
><br>
> No, up to now the only changes are in the type checking of applications and variables.<br>
> 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).<br>
><br>
> El vie., 28 jun. 2019 a las 14:17, Matthew Pickering (<<a href="mailto:matthewtpickering@gmail.com" target="_blank">matthewtpickering@gmail.com</a>>) escribió:<br>
>><br>
>> Have you modified how typed quotations are type checked? For example,<br>
>> with your patch I would hope that<br>
>><br>
>> [| id |] :: Code (forall a . a -> a)<br>
>><br>
>> would be accepted?<br>
>><br>
>> I'll try it out. This patch will have big ramifications for the typed<br>
>> template haskell community.<br>
>><br>
>> Matt<br>
>><br>
>> On Fri, Jun 28, 2019 at 1:12 PM Alejandro Serrano Mena<br>
>> <<a href="mailto:trupill@gmail.com" target="_blank">trupill@gmail.com</a>> wrote:<br>
>> ><br>
>> > Dear all,<br>
>> ><br>
>> > We are trying to bring back `ImpredicativeTypes` into GHC by using the ideas in the "Guarded Impredicative Polymorphism" paper [<a href="https://www.microsoft.com/en-us/research/publication/guarded-impredicative-polymorphism/" rel="noreferrer" target="_blank">https://www.microsoft.com/en-us/research/publication/guarded-impredicative-polymorphism/</a>].<br>
>> ><br>
>> > For now I have produced a first attempt, which lives in <a href="https://gitlab.haskell.org/trupill/ghc" rel="noreferrer" target="_blank">https://gitlab.haskell.org/trupill/ghc</a>. It would be great if those interested in impredicative polymorphism could give it a try and see whether it works as expected or not.<br>
>> ><br>
>> > 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 (->).<br>
>> > 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.<br>
>> ><br>
>> > Just for reference, the best to get a working clone is to follow these steps:<br>
>> > > git clone --recursive <a href="https://gitlab.haskell.org/ghc/ghc" rel="noreferrer" target="_blank">https://gitlab.haskell.org/ghc/ghc</a> impredicative-ghc<br>
>> > > cd impredicative-ghc<br>
>> > > git remote add trupill git@gitlab.haskell.org:trupill/ghc.git<br>
>> > > git fetch trupill<br>
>> > > git checkout trupill master<br>
>> ><br>
>> > Thanks very much in advance,<br>
>> > Alejandro<br>
>> ><br>
>> > _______________________________________________<br>
>> > ghc-devs mailing list<br>
>> > <a href="mailto:ghc-devs@haskell.org" target="_blank">ghc-devs@haskell.org</a><br>
>> > <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
</blockquote></div>