Note [Defaulting representational equalities]

Suppose we end up with [W] alpha ~#R Int, with no other constraints on alpha.
Then it makes sense to simply unify alpha := Int -- the alternative is to
reject the program due to an ambiguous metavariable alpha, so it makes sense
to unify and accept instead.

This is particularly convenient for users of `coerce`, as it lessens the
amount of type annotations required (see #21003). Consider for example:

  'foldMap' defined using 'traverse'
  foldMapUsingTraverse :: forall t m a. (Traversable t, Monoid m) => (a -> m) -> t a -> m
  foldMapUsingTraverse = coerce $ traverse @t @(Const m)

  'traverse_' defined using 'foldMap'
  traverse_UsingFoldMap :: forall f t a. (Foldable t, Applicative f) => (a -> f ()) -> t a -> f ()
  traverse_UsingFoldMap = coerce $ foldMap @t @(Ap f ())

Typechecking these functions results in unsolved Wanted constraints of the form
[W] alpha[tau] ~R# some_ty; accepting such programs by unifying
alpha := some_ty avoids the need for users to specify tiresome additional
type annotations, such as:

    foldMapUsingTraverse = coerce $ traverse @t @(Const m) @a
    traverse_UsingFoldMap = coerce $ foldMap @t @(Ap f ()) @a

Consider also the following example:

  'sequence_', but for two nested 'Foldable' structures
  sequenceNested_ :: forall f1 f2. (Foldable f1, Foldable f2) => f1 (f2 (IO ())) -> IO ()
  sequenceNested_ = coerce $ sequence_ @( Compose f1 f2 )

Here, we end up with [W] mu[tau] beta[tau] ~#R IO (), and it similarly makes
sense to default mu := IO, beta := (). This avoids requiring the
user to provide additional type applications:

    sequenceNested_ = coerce $ sequence_ @( Compose f1 f2 ) @IO @()

The plan for defaulting a representational equality, say [W] ty1 ~R# ty2,
is thus as follows:

  1. attempt to unify ty1 ~# ty2 (at nominal role)
  2. a. if this succeeds without deferring any constraints, accept this solution
     b. otherwise, keep the original constraint.

(2b) ensures that we don't degrade all error messages by always turning unsolved
representational equalities into nominal ones; we only want to default a
representational equality when we can fully solve it.

Note that this does not threaten principle types. Recall that the original worry
(as per Note [Do not unify representational equalities]) was that we might have

    [W] alpha ~R# Int
    [W] alpha ~ Age

in which case unifying alpha := Int would be wrong, as the correct solution is
alpha := Age. This worry doesn't concern us in top-level defaulting, because
defaulting takes place after generalisation; it is fully monomorphic.

*********************************************************************************
*                                                                               *
*                Type-class defaulting
*                                                                               *
*********************************************************************************