Guarded Impredicativity

[Matthew Pickering]

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