<div dir="ltr"><div>Hello Ryan,</div><div><br></div><div>Your example seems to work out of the box with the GI branch.</div><div><br></div><div>With the oneliner Matthew posted before:</div><div>nix run -f <a href="https://github.com/mpickering/ghc-artefact-nix/archive//master.tar.gz">https://github.com/mpickering/ghc-artefact-nix/archive//master.tar.gz</a> \<br>ghc-head-from -c ghc-head-from \<br><a href="https://gitlab.haskell.org/mpickering/ghc/-/jobs/114593/artifacts/raw/ghc-x86_64-fedora27-linux.tar.xz">https://gitlab.haskell.org/mpickering/ghc/-/jobs/114593/artifacts/raw/ghc-x86_64-fedora27-linux.tar.xz</a></div><div></div><div>It is really easy to check. Also, I didn't see anywhere mentioned that one need to provide -XImpredicativeTypes. The whole example, therefore, is:</div><div><br></div><div>{-#LANGUAGE ImpredicativeTypes, ConstraintKinds #-} <br>module M where<br>type F f = (Functor f, forall a. Eq (f a))</div><div><br></div><div>--</div><div>Best, Artem<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, 19 Jul 2019 at 09:18, Ryan Scott <<a href="mailto:ryan.gl.scott@gmail.com">ryan.gl.scott@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">I have another interesting application of guarded impredicativity that<br>
I want to bring up. Currently, GHC #16140 [1] makes it rather<br>
inconvenient to use quantified constraints in type synonyms. For<br>
instance, GHC rejects the following example by default:<br>
<br>
type F f = (Functor f, forall a. Eq (f a))<br>
<br>
This is because F is a synonym for a constraint tuple, so mentioning a<br>
quantified constraint in one of its arguments gets flagged as<br>
impredicative. In the discussion for #16140, we have pondered doing a<br>
major rewrite of the code in TcValidity to permit F. But perhaps we<br>
don't need to! After all, the quantified constraint in the example<br>
above appears directly underneath a type constructor (namely, the type<br>
constructor for the constraint 2-tuple), which should be a textbook<br>
case of guarded impredicativity.<br>
<br>
I don't have the guarded impredicativity branch built locally, so I am<br>
unable to test if this hypothesis is true. In any case, I wanted to<br>
mention it as another motivating use case.<br>
<br>
Ryan S.<br>
-----<br>
[1] <a href="https://gitlab.haskell.org/ghc/ghc/issues/16140" rel="noreferrer" target="_blank">https://gitlab.haskell.org/ghc/ghc/issues/16140</a><br>
_______________________________________________<br>
ghc-devs mailing list<br>
<a href="mailto:ghc-devs@haskell.org" target="_blank">ghc-devs@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
</blockquote></div>