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 <trup...@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 (< > matthewtpicker...@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 >> <trup...@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 g...@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 >
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs