eacameron at gmail.com
Fri Jun 28 12:26:02 UTC 2019
Sorry meant to reply all:
I ran into the error recently here:
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 at gmail.com>
> 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.
>> 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 [
>> > 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
>> > > git clone --recursive https://gitlab.haskell.org/ghc/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
> ghc-devs mailing list
> ghc-devs at haskell.org
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the ghc-devs