Guarded Impredicativity

[Alejandro Serrano Mena]

Just to keep you posted about the current development, we are working on a
new approach to impredicativity which is inspired by guarded
impredicativity but requires much fewer changes to the codebase. In
particular, our goal is to isolate the inference of impredicativity,
instead of contaminating the whole compiler with it.

The repo where we are developing it lives in
https://gitlab.haskell.org/trupill/ghc (branch "quick-look").

Regards,
Alejandro

El vie., 19 jul. 2019 a las 23:40, Ryan Scott (<ryan.gl.scott at gmail.com>)
escribió:

> Good to know. Thanks for checking!
>
> Ryan S.
>
> On Fri, Jul 19, 2019 at 11:22 AM Artem Pelenitsyn
> <a.pelenitsyn at gmail.com> wrote:
> >
> > Hello Ryan,
> >
> > Your example seems to work out of the box with the GI branch.
> >
> > With the oneliner Matthew posted before:
> > nix run -f
> https://github.com/mpickering/ghc-artefact-nix/archive//master.tar.gz \
> > ghc-head-from -c ghc-head-from \
> >
> https://gitlab.haskell.org/mpickering/ghc/-/jobs/114593/artifacts/raw/ghc-x86_64-fedora27-linux.tar.xz
> > It is really easy to check. Also, I didn't see anywhere mentioned that
> one need to provide -XImpredicativeTypes. The whole example, therefore, is:
> >
> > {-#LANGUAGE ImpredicativeTypes, ConstraintKinds #-}
> > module M where
> > type F f = (Functor f, forall a. Eq (f a))
> >
> > --
> > Best, Artem
> >
> > On Fri, 19 Jul 2019 at 09:18, Ryan Scott <ryan.gl.scott at gmail.com>
> wrote:
> >>
> >> I have another interesting application of guarded impredicativity that
> >> I want to bring up. Currently, GHC #16140 [1] makes it rather
> >> inconvenient to use quantified constraints in type synonyms. For
> >> instance, GHC rejects the following example by default:
> >>
> >>     type F f = (Functor f, forall a. Eq (f a))
> >>
> >> This is because F is a synonym for a constraint tuple, so mentioning a
> >> quantified constraint in one of its arguments gets flagged as
> >> impredicative. In the discussion for #16140, we have pondered doing a
> >> major rewrite of the code in TcValidity to permit F. But perhaps we
> >> don't need to! After all, the quantified constraint in the example
> >> above appears directly underneath a type constructor (namely, the type
> >> constructor for the constraint 2-tuple), which should be a textbook
> >> case of guarded impredicativity.
> >>
> >> I don't have the guarded impredicativity branch built locally, so I am
> >> unable to test if this hypothesis is true. In any case, I wanted to
> >> mention it as another motivating use case.
> >>
> >> Ryan S.
> >> -----
> >> [1] https://gitlab.haskell.org/ghc/ghc/issues/16140
> >> _______________________________________________
> >> 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
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20190722/aa0820ea/attachment.html>