Note [Deep subsumption]

The DeepSubsumption extension, documented here

    https://github.com/ghc-proposals/ghc-proposals/pull/511.

makes a best-efforts attempt implement deep subsumption as it was
prior to the Simplify Subsumption proposal:

    https://github.com/ghc-proposals/ghc-proposals/pull/287

The effects are in these main places:

1. In the subsumption check, tcSubType, we must do deep skolemisation:
   see the call to tcSkolemise Deep in tc_sub_type_deep

2. In tcPolyExpr we must do deep skolemisation:
   see the call to tcSkolemise in tcSkolemiseExpType

3. for expression type signatures (e :: ty), and functions with type
   signatures (e.g. f :: ty; f = e), we must deeply skolemise the type;
   see the call to tcDeeplySkolemise in tcSkolemiseScoped.

4. In GHC.Tc.Gen.App.tcApp we call tcSubTypeDS to match the result
   type. Without deep subsumption, tcSubTypeMono would be sufficent.

In all these cases note that the deep skolemisation must be done /first/.
Consider (1)
     (forall a. Int -> a -> a)  <=  Int -> (forall b. b -> b)
We must skolemise the `forall b` before instantiating the `forall a`.
See also Note [Deep skolemisation].

Wrinkles:

(DS1) Note that we /always/ use shallow subsumption in the ambiguity check.
      See Note [Ambiguity check and deep subsumption].

(DS2) When doing deep subsumption, we must be careful not to needlessly
      drop down to unification, e.g. in cases such as:
        (Bool -> ∀ d. d->d)   <=   alpha beta gamma
      See Note [FunTy vs non-FunTy case in tc_sub_type_deep].

(DS3) The interaction between deep subsumption and required foralls
      (forall a -> ty) is a bit subtle.  See #24696 and
      Note [Deep subsumption and required foralls]