Sorry meant to reply all:

I ran into the error recently here: https://github.com/monadfix/named/issues/24

trying to use a fun named arguments library. I can't immediately tell if these changes to GHC are sufficient to help. This library is using a newtype with phantom arguments.

On Fri, Jun 28, 2019, 8:20 AM Alejandro Serrano Mena <trupill@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@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@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@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
_______________________________________________
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs