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@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-subsumpt... ? 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.