Re: Guarded Impredicativity

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 () escribió:

Good to know. Thanks for checking!

Ryan S.

On Fri, Jul 19, 2019 at 11:22 AM Artem Pelenitsyn 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-x8...

...

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 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@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