Guarded Impredicativity

[Matthew Pickering]

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
<trupill at gmail.com> 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 (<matthewtpickering at 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
>> <trupill at gmail.com> 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 (<matthewtpickering at 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
>> >> <trupill at gmail.com> 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 git at 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 at haskell.org
>> >> > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs