Note [Defaulting equalities]

In top-level defaulting (as per Note [Top-level Defaulting Plan]), it makes
sense to try to default equality constraints, in addition to e.g. typeclass
defaulting: this doesn't threaten principal types (see DE1 below), but
allows GHC to accept strictly more programs.

This Note explains defaulting nominal equalities; see also
Note [Defaulting representational equalities] which describes
the defaulting of representational equalities.

Consider

  f :: forall a. (forall t. (F t ~ Int) => a -> Int) -> Int

  g :: Int
  g = f id

We'll typecheck

  id :: forall t. (F t ~ Int) => alpha[1] -> Int

where the `alpha[1]` comes from instantiating `f`. So we'll end up
with the implication constraint

   forall[2] t. (F t ~ Int) => alpha[1] ~ Int

and that can't be solved because `alpha` is untouchable under the
equality (F t ~ Int).

This is tiresome, and gave rise to user complaints: #25125 and #25029.
Moreover, in this case there is no good reason not to unify alpha:=Int.
Doing so solves the constraint, and since `alpha` is not otherwise
constrained, it does no harm.

In conclusion, for a Wanted equality constraint [W] lhs ~ rhs, if the only
reason for not unifying is that either lhs or rhs is an untouchable metavariable
then, in top-level defaulting, go ahead and unify.

In top-level defaulting, we already do several other somewhat-ad-hoc,
but terribly convenient, unifications. This is just one more.

Wrinkles:

(DE1) Note carefully that this does not threaten principal types.
  The original worry about unifying untouchable type variables was this:

     data T a where
       T1 :: T Bool
     f x = case x of T1 -> True

  Should we infer f :: T a -> Bool, or f :: T a -> a.  Both are valid, but
  neither is more general than the other.

(DE2) We still can't unify if there is a skolem-escape check, or an occurs check,
  or it it'd mean unifying a TyVarTv with a non-tyvar.  It's only the
  "untouchability test" that we lift.

(DE3) The contraint we are looking at may not be fully zonked; for example,
  an earlier defaulting might have affected it. So we zonk-on-the fly in
  `defaultEquality`.

(DE4) Promotion. Suppose we see  alpha[2] := Maybe beta[4].  We want to promote
  beta[4] to level 2 and unify alpha[2] := Maybe beta'[2].  This is done by
  checkTyEqRhs called in defaultEquality.

(DE5) Promotion. Suppose we see  alpha[2] := F beta[4], where F is a type
  family. Then we still want to promote beta to beta'[2], and unify. This is
  unusual: more commonly, we don't promote unification variables under a
  type family.  But here we want to.  (This mattered in #25251.)

  Hence the Bool flag on LC_Promote, and its use in `tef_unifying` in
  `defaultEquality`.

(DE6) /Don't/ unify if the RHS has a free coercion hole in it.  That means
  that there is an as-yet-unsolved equality constraint (whose evidence
  will fill that hole); unifying can lead to very confusing type errors.
  e.g.    [W] co1 :: IntRep ~ LiftedRep
          [W] co2 {rewritten by co1} :: alpha ~ t2 |> (TYPE co1)
  Unifying alpha := (t1 |> TYPE co1) is a Bad Idea.

  Note that we /do/ unify even if the constraint has a non-empty rewriter
  set, which has prevented unification up to now; see
  Note [Unify only if the rewriter set is empty] in GHC.Tc.Solver.Equality.
  In obscure situations a constraint can end up in its own rewriter set, but
  without a coercion hole being in the RHS.

  See #10009, and Note [Limited defaulting in the ambiguity check].