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

[Jon Purdy]

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

>
> > The 9.0 upgrade may help:
> > 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
> ?
> 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
> 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/20201001/1c2d54a9/attachment.html>