Note [Decomposing newtype equalities]

This Note also applies to data families, which we treat like
newtype in case of 'newtype instance'.

As Note [Decomposing TyConApp equalities] describes, if N is injective
at role r, we can do this decomposition?
   [G/W] (N ty1) ~r (N ty2)    to     [G/W]  ty1 ~r' ty2

For a Given with r=R, the answer is a solid NO: newtypes are not injective at
representational role, and we must not decompose, or we lose soundness.
Example is wrinkle {1} in Note [Decomposing TyConApp equalities].

For a Wanted with r=R, since newtypes are not injective at representational
role, decomposition is sound, but we may lose completeness.  Nevertheless,
if the newtype is abstract (so can't be unwrapped) we can only solve
the equality by (a) using a Given or (b) decomposition.  If (a) is impossible
(e.g. no Givens) then (b) is safe albeit potentially incomplete.

There are two ways in which decomposing (N ty1) ~r (N ty2) could be incomplete:

* Incompleteness example (EX1): unwrap first
      newtype Nt a = MkNt (Id a)
      type family Id a where Id a = a

      [W] Nt Int ~R Nt Age

  Because of its use of a type family, Nt's parameter will get inferred to
  have a nominal role. Thus, decomposing the wanted will yield [W] Int ~N Age,
  which is unsatisfiable. Unwrapping, though, leads to a solution.

  CONCLUSION: always unwrap newtypes before attempting to decompose
  them.  This is done in can_eq_nc.  Of course, we can't unwrap if the data
  constructor isn't in scope.  See Note [Unwrap newtypes first].

* Incompleteness example (EX2): prioritise Nominal equalities. See #24887
      data family D a
      data instance D Int  = MkD1 (D Char)
      data instance D Bool = MkD2 (D Char)
  Now suppose we have
      [W] g1: D Int ~R# D a
      [W] g2: a ~# Bool
  If we solve g2 first, giving a:=Bool, then we can solve g1 easily:
      D Int ~R# D Char ~R# D Bool
  by newtype unwrapping.

  BUT: if we instead attempt to solve g1 first, we can unwrap the LHS (only)
  leaving     [W] D Char ~#R D Bool
  If we decompose now, we'll get (Char ~R# Bool), which is insoluble.

  CONCLUSION: prioritise nominal equalites in the work list.
  See Note [Prioritise equalities] in GHC.Tc.Solver.InertSet.

* Incompleteness example (EX3): check available Givens
      newtype Nt a = Mk Bool         -- NB: a is not used in the RHS,
      type role Nt representational  -- but the user gives it an R role anyway

      [G] Nt t1 ~R Nt t2
      [W] Nt alpha ~R Nt beta

  We *don't* want to decompose to [W] alpha ~R beta, because it's possible
  that alpha and beta aren't representationally equal.  And if we figure
  out (elsewhere) that alpha:=t1 and beta:=t2, we can solve the Wanted
  from the Given.  This is somewhat similar to the question of overlapping
  Givens for class constraints: see Note [Instance and Given overlap] in
  GHC.Tc.Solver.Dict.

  CONCLUSION: don't decompose [W] N s ~R N t, if there are any Given
  equalities that could later solve it.

  But what precisely does it mean to say "any Given equalities that could
  later solve it"?  It's tricky!

  * In #22924 we had
       [G] f a ~R# a     [W] Const (f a) a ~R# Const a a
    where Const is an abstract newtype.  If we decomposed the newtype, we
    could solve.  Not-decomposing on the grounds that (f a ~R# a) might turn
    into (Const (f a) a ~R# Const a a) seems a bit silly.

  * In #22331 we had
       [G] N a ~R# N b   [W] N b ~R# N a
    (where N is abstract so we can't unwrap). Here we really /don't/ want to
    decompose, because the /only/ way to solve the Wanted is from that Given
    (with a Sym).

  * In #22519 we had
       [G] a <= b     [W] IO Age ~R# IO Int

    (where IO is abstract so we can't unwrap, and newtype Age = Int; and (<=)
    is a type-level comparison on Nats).  Here we /must/ decompose, despite the
    existence of an Irred Given, or we will simply be stuck.  (Side note: We
    flirted with deep-rewriting of newtypes (see discussion on #22519 and
    !9623) but that turned out not to solve #22924, and also makes type
    inference loop more often on recursive newtypes.)

  * In #26020 we had a /quantified/ constraint
        forall x. Coercible (N t1) (N t2)
    and (roughly) [W] N t1 ~R# N t2
    That quantified constraint can solve the Wanted, so don't decompose!

  The currently-implemented compromise is this:
       We decompose [W] N s ~R# N t unless there is
       - an Irred [G] N s' ~ N t'
       - a quantified [G] forall ... => N s' ~ N t'
       that is, a Given equality with both sides headed with N.
  See the call to `noGivenNewtypeReprEqs` in `canTyConApp`.

  This is not perfect.  In principle a Given like [G] (a b) ~ (c d), or
  even just [G] c, could later turn into N s ~ N t.  But since the free
  vars of a Given are skolems, or at least untouchable unification
  variables, this is extremely unlikely to happen.

  Another worry: there could, just, be a CDictCan with some
  un-expanded equality superclasses; but only in some very obscure
  recursive-superclass situations.

   Yet another approach (!) is described in
   Note [Decomposing newtypes a bit more aggressively].

Remember: decomposing Wanteds is always /sound/. This Note is
only about /completeness/.