<div dir="ltr"><div>I think this is a consequence of the fact that function types are now invariant in their domain, rather than contravariant.<br></div><div><br></div><div> 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.<br></div><div><br></div><div>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.<br></div><div><br></div><div>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.</div><div><br></div><div>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.<br></div><div><br></div><div>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).</div><div><br></div><div>I hope this helps (and that I haven’t completely botched the explanation haha)<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Oct 1, 2020 at 9:38 AM Johannes Waldmann <<a href="mailto:johannes.waldmann@htwk-leipzig.de">johannes.waldmann@htwk-leipzig.de</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"><br>
> The 9.0 upgrade may help: <br>
> <a href="https://gitlab.haskell.org/ghc/ghc/-/wikis/migration/9.0" rel="noreferrer" target="_blank">https://gitlab.haskell.org/ghc/ghc/-/wikis/migration/9.0</a><br>
<br>
Thanks for that pointer!<br>
<br>
So, what I observed is an effect of<br>
<a href="https://gitlab.haskell.org/ghc/ghc/-/wikis/migration/9.0#simplified-subsumption" rel="noreferrer" target="_blank">https://gitlab.haskell.org/ghc/ghc/-/wikis/migration/9.0#simplified-subsumption</a><br>
?<br>
I was browsing that, but could not make the connection.<br>
"nested foralls" are mentioned only together with<br>
GADT/instance/deriving, none of which is in my example.<br>
<br>
- J.<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
Only members subscribed via the mailman list are allowed to post.</blockquote></div>