[Haskell-cafe] ghc-9 needs type declaration where ghc-8 didn't (with RankNTypes)

Fri Oct 2 18:35:55 UTC 2020

Hi all,

This problem definitely is caused by the change to subsumption in GHC 9.0 (which is a precursor to, but separate from, the new -XImpredicativeTypes).

Jon's explanation below gets close to the mark, but I have a different way of explaining a few details.

As Jon points out, a key aspect of this is the contravariance of the first argument of the (->) constructor. That is, for A -> B to be more general than C -> D (written (A -> B) <: (C -> D)), then we must have C <: A and B <: D. Note that the order in the first relation is reversed. Why? If E <: F, that means that we can use an E wherever we need an F -- this is really the definition of <: (and suggests, correctly, that G <: G for all G -- in other words, <: is reflexive). When can one function type be used in place of another? In other words, when can a function f of type A -> B be used instead of C -> D? Well, f must be able to accept things of type C, because the context expecting something of type C -> D will pass f something of type C. So, we must be able to supply a C instead of an A -- in other words, we must have C <: A. And then, the context expecting something of type C -> D will want a D, so B must suffice instead of D -- in other words, we must have B <: D. And thus we get the sub-typing rule for (->).

This rule is relaxed in GHC 9.0 not because it is unsound -- it's perfectly sound and continues to be -- but because its particular implementation in GHC causes perhaps-unexpected runtime changes around divergent expressions (bottoms) and interferes with type inference in places. See https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0287-simplify-subsumption.rst <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0287-simplify-subsumption.rst> for more details.

Previous to GHC 9.0, we had this:

> f :: (forall a. a -> ()) -> ()
> f = g
> 
> g x = undefined

We'll first get a type for g, completely unaffected by f. g's type is, unsurprisingly, forall b c. b -> c, as there's nothing to constrain either its input nor its result.

Now, how can we accept f = g? At the appearance of g, we first choose two unification variables (that is, stand-ins for as-yet-unknown types) for the type variables b and c. (This is where my explanation diverges from Jon's.) This is the same as we do for all polymorphic functions, and it's how GHC accepts e.g. show True, by instantiating the variable `a` in show's type. Let's call these unification variables beta and gamma; we thus say g :: beta -> gamma, for some types beta and gamma. Now we must determine whether (beta -> gamma) <: ((forall a. a -> ()) -> ()) holds. Using the rule for <: and (->) we developed above, we must show (forall a. a -> ()) <: beta and gamma <: (). GHC is clever, and will choose beta to be (Any <https://hackage.haskell.org/package/base-4.14.0.0/docs/GHC-Exts.html#t:Any> -> ()) and gamma to be (). So we must show (forall a. a -> ()) <: Any -> () and () <: (). The second is known by the reflexivity of <:. For the first, we realize that we are free to choose the `a` in forall a. a -> (). (This bit is subtle. See Section 4.4 of https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/putting.pdf <https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/putting.pdf> for more details.) So we create a new unification variable alpha; we now must check (alpha -> ()) <: (Any -> ()). But this is easy: just choose alpha to be Any, and we're all set.

In GHC 9.0, we can't do this, because we don't have any rule that allows us to "look under" (->) when checking (beta -> gamma) <: ((forall a. a -> ()) -> ()). The only way for this to work out in GHC 9.0 is for beta to become (forall a. a -> ()) and for gamma to become (). Yet this requires setting beta to be a polytype (a type with a forall), and GHC won't do that -- unless -XImpredicativeTypes is on. In the new implementation of -XImpredicativeTypes, available in GHC HEAD, this indeed works, simply by enabling the extension.

I hope this is helpful!
Richard

> On Oct 1, 2020, at 2:43 PM, Jon Purdy <evincarofautumn at gmail.com> wrote:
> 
> I think this is a consequence of the fact that function types are now invariant in their domain, rather than contravariant.
> 
> If anyone’s more familiar with GHC’s typechecker, please correct me if I’m mistaken here, but I’ll try to explain what I think is happening.
> 
> The rule for checking a definition against a signature is a subtyping relation, “is at least as polymorphic as”, which matches the intuition that a signature can constrain the inferred type, but can’t promise more than the inferred type can offer.
> 
> Previously, the inferred type of ‘g’, ∀p a. p → a, would be checked as a subtype of the declared type of ‘f’, (∀a′. a′ → ())  → (). According to the old rules, I₁ → O₁ ≤: I₂ → O₂ if O₁ ≤: O₂ (covariant) and I₂ ≤: I₁ (contravariant), and when polytypes are involved, you eta-expand to juggle the foralls around. So this would judge a ≤: () covariantly, i.e., a type variable is more polymorphic than a type, and (∀a′. a′ → ()) ≤: p contravariantly, because a polytype is more polymorphic than a type variable. Note the reversed order! This was handled in GHC.Tc.Utils.Unify.tc_sub_type_ds.
> 
> Whereas now this is rejected by the simplified subsumption check, which only unifies using type equality. Can we unify a = ()? Yes, with the substitution a = (). Can we unify p = ∀a′. a′ → ()? No, this would require implicit polymorphic instantiation, which isn’t allowed.
> 
> I believe the eta-expanded version typechecks in this case because we end up checking a lambda λx. g x against (∀a′. a′ → ())  → (), which causes the typechecker to first assume that x has the polymorphic type ∀a′. a′ → () and then check the application g x in that context. It accepts this because p can be explicitly filled with a polytype just fine in an application (and RankNTypes allows this impredicative instantiation, for the (→) constructor only).
> 
> I hope this helps (and that I haven’t completely botched the explanation haha)
> 
> On Thu, Oct 1, 2020 at 9:38 AM Johannes Waldmann <johannes.waldmann at htwk-leipzig.de <mailto:johannes.waldmann at htwk-leipzig.de>> wrote:
> 
> > The 9.0 upgrade may help: 
> > https://gitlab.haskell.org/ghc/ghc/-/wikis/migration/9.0 <https://gitlab.haskell.org/ghc/ghc/-/wikis/migration/9.0>
> 
> Thanks for that pointer!
> 
> So, what I observed is an effect of
> https://gitlab.haskell.org/ghc/ghc/-/wikis/migration/9.0#simplified-subsumption <https://gitlab.haskell.org/ghc/ghc/-/wikis/migration/9.0#simplified-subsumption>
> ?
> I was browsing that, but could not make the connection.
> "nested foralls" are mentioned only together with
> GADT/instance/deriving, none of which is in my example.
> 
> - J.
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe <http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe>
> Only members subscribed via the mailman list are allowed to post.
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20201002/b48d01a2/attachment.html>