Good to know. Thanks for checking! Ryan S.
On Fri, Jul 19, 2019 at 11:22 AM Artem Pelenitsyn <[email protected]> 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 <[email protected]> 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 >> [email protected] >> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs _______________________________________________ ghc-devs mailing list [email protected] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
