Note [Deep subsumption and required foralls]

A required forall, (forall a -> ty) behaves like a "rho-type", one with no
top-level quantification.  In particular, it is neither implicitly instantiated nor
skolemised.  So

  rid1 :: forall a -> a -> a
  rid1 = id

  rid2 :: forall a -> a -> a
  rid2 a = id

Here `rid2` wll typecheck, but `rid1` will not, because we don't implicitly skolemise
the  type.

This "no implicit subsumption nor skolemisation" applies during subsumption.
For example
   (forall a. a->a)  <=  (forall a -> a -> a)  -- NOT!
does /not/ hold, because that would require implicitly skoleming the (forall a->).

Note also that, in Core, `eqType` distinguishes between
   (forall a. blah) and forall a -> blah)
See discussion on #22762 and these Notes in GHC.Core.TyCo.Compare
  * Note [ForAllTy and type equality]
  * Note [Comparing visibility]

So during deep subsumption we simply stop (and drop down to equality) when we encounter
a (forall a->).  This is a little odd:
* Deep subsumption looks inside invisible foralls (forall a. ty)
* Deep subsumption looks inside arrows (t1 -> t2)
* But it does not look inside required foralls (forall a -> ty)

There is discussion on #24696.  How is this implemented?

* In `tc_sub_type_deep`, the calls to `topInstantiate` and `deeplyInstantiate`
  instantiate only /invisible/ binders.
* In `tc_sub_type_ds`, the call to `tcSkolemise` skolemises only /invisible/
  binders.

Here is a slightly more powerful alternative
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 In the story above, if we have
    (forall a -> Eq a => a -> a)  <=  (forall a -> Ord a => a -> a)
we'll reject it, because both are rho-types but they aren't equal.  But in the
"drop to equality" stage we could instead see if both rho-types are headed with
(forall a ->) and if so strip that off and go back into deep subsumption.

This is a bit more powerful, but also a bit more complicated, so GHC
doesn't do it yet, awaiting credible user demand.  See #24696.