Strange polytype unification behavior

Summary

While looking into https://github.com/ghc-proposals/ghc-proposals/issues/558, I noticed some strangeness around can_eq_nc_forall, which I thought I should record while it is fresh. Specifically:

Bug

• When there are nested foralls, we only check that the outermost visibilities match:
  • We (correctly) reject unifying forall b -> (a, b) with forall b. (a, b), but
  • we (wrongly) succeed unifying forall a. forall b -> (a, b) with forall a. forall b. (a, b).

Opportuntity

• We only match successfully if the forall nesting depth is the same for both types. For nominal equality, this is expected (I think), but it's a bit odd for representational equality. If we have newtype P a = PC (forall c. (a, c)):
  • We (correctly?) representationally unify P a with forall b. (a, b), but
  • we reject representationally unifying forall a. P a with forall a. forall b. (a, b).

Here is a concrete example:

import Data.Coerce

newtype M   = MkM (forall a b. a -> b -> b)
newtype N a = MkN (forall b. a -> b -> b)
newtype P   = MkP (forall a. N a)

g1 :: M -> P
g1 x = coerce x

g2 :: P -> M
g2 x = coerce x

It is not unreasonable to expect g1 and g2 to typecheck; there are perfectly well-behaved coercions that connect them.

Expected behavior

• We should definitely reject matching forall a. forall b -> (a, b) with forall a. forall b. (a, b), at least when matching for nominal equality.
• It's surprising and neat-o that representational equality solving with newtypes around polytypes even sort-of works. But I don't have an informed opinion about whether this "should" be expected to generally work.