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