Note [Unwrap newtypes first]

See also Note [Decomposing newtype equalities]

Consider
  newtype N m a = MkN (m a)
N will get a conservative, Nominal role for its second parameter 'a',
because it appears as an argument to the unknown 'm'. Now consider
  [W] N Maybe a  ~R#  N Maybe b

If we /decompose/, we'll get
  [W] a ~N# b

But if instead we /unwrap/ we'll get
  [W] Maybe a ~R# Maybe b
which in turn gives us
  [W] a ~R# b
which is easier to satisfy.

Conclusion: we must unwrap newtypes before decomposing them. This happens
in `can_eq_newtype_nc`

We did flirt with making the /rewriter/ expand newtypes, rather than
doing it in `can_eq_newtype_nc`.   But with recursive newtypes we want
to be super-careful about expanding!

   newtype A = MkA [A]   -- Recursive!

   f :: A -> [A]
   f = coerce

We have [W] A ~R# [A].  If we rewrite [A], it'll expand to
   [[[[[...]]]]]
and blow the reduction stack.  See Note [Newtypes can blow the stack]
in GHC.Tc.Solver.Rewrite.  But if we expand only the /top level/ of
both sides, we get
   [W] [A] ~R# [A]
which we can, just, solve by reflexivity.

So we simply unwrap, on-demand, at top level, in `can_eq_newtype_nc`.

This is all very delicate. There is a real risk of a loop in the type checker
with recursive newtypes -- but I think we're doomed to do *something*
delicate, as we're really trying to solve for equirecursive type
equality. Bottom line for users: recursive newtypes do not play well with type
inference for representational equality.  See also Section 5.3.1 and 5.3.4 of
"Safe Zero-cost Coercions for Haskell" (JFP 2016).

See also Note [Decomposing newtype equalities].

Historical side note ---

We flirted with doing /both/ unwrap-at-top-level /and/ rewrite-deeply;
see #22519.  But that didn't work: see discussion in #22924. Specifically
we got a loop with a minor variation:
   f2 :: a -> [A]
   f2 = coerce