Implement DeepSubsumption

This MR adds the language extension -XDeepSubsumption, implementing
GHC proposal #511.  This change mitigates the impact of GHC proposal

The changes are highly localised, by design.  See Note [Deep subsumption]
in GHC.Tc.Utils.Unify.

The main changes are:

* Add -XDeepSubsumption, which is on by default in Haskell98 and Haskell2010,
  but off in Haskell2021.

  -XDeepSubsumption largely restores the behaviour before the "simple subsumption" change.
  -XDeepSubsumpition has a similar flavour as -XNoMonoLocalBinds:
  it makes type inference more complicated and less predictable, but it
  may be convenient in practice.

* The main changes are in:
  * GHC.Tc.Utils.Unify.tcSubType, which does deep susumption and eta-expanansion
  * GHC.Tc.Utils.Unify.tcSkolemiseET, which does deep skolemisation
  * In GHC.Tc.Gen.App.tcApp we call tcSubTypeNC to match the result
    type. Without deep subsumption, unifyExpectedType would be sufficent.

  See Note [Deep subsumption] in GHC.Tc.Utils.Unify.

* There are no changes to Quick Look at all.

* The type of `withDict` becomes ambiguous; so add -XAllowAmbiguousTypes to
  GHC.Magic.Dict

* I fixed a small but egregious bug in GHC.Core.FVs.varTypeTyCoFVs, where
  we'd forgotten to take the free vars of the multiplicity of an Id.

* I also had to fix tcSplitNestedSigmaTys

  When I did the shallow-subsumption patch
    commit 2b792facab46f7cdd09d12e79499f4e0dcd4293f
    Date:   Sun Feb 2 18:23:11 2020 +0000
    Simple subsumption

  I changed tcSplitNestedSigmaTys to not look through function arrows
  any more.  But that was actually an un-forced change.  This function
  is used only in

  * Improving error messages in GHC.Tc.Gen.Head.addFunResCtxt
  * Validity checking for default methods: GHC.Tc.TyCl.checkValidClass
  * A couple of calls in the GHCi debugger: GHC.Runtime.Heap.Inspect

  All to do with validity checking and error messages. Acutally its
  fine to look under function arrows here, and quite useful a test
  DeepSubsumption05 (a test motivated by a build failure in the
  `lens` package) shows.

  The fix is easy.  I added Note [tcSplitNestedSigmaTys].

2 files changed, 36 insertions, 10 deletions

diff --git a/docs/users_guide/exts/default_signatures.rst b/docs/users_guide/exts/default_signatures.rst
index 54e995e2ce..210bbea560 100644
--- a/docs/users_guide/exts/default_signatures.rst
+++ b/docs/users_guide/exts/default_signatures.rst
@@ -88,7 +88,7 @@ default type signatures.
 
 - Ignoring outermost contexts, a default type signature must match the original
   type signature according to
-  :ref:`GHC's subsumption rules <simple-subsumption>`. As a result, the order
+  :ref:`GHC's subsumption rules <subsumption>`. As a result, the order
   of type variables in the default signature is important. Recall the ``Foo``
   example from the previous section: ::
 
@@ -122,7 +122,7 @@ default type signatures.
 
       default bar :: forall b. (C', b ~ Int) => a -> b -> b
 
-- Because of :ref:`GHC's subsumption rules <simple-subsumption>` rules, there
+- Because of :ref:`GHC's subsumption rules <subsumption>` rules, there
   are relatively tight restrictions concerning nested or higher-rank
   ``forall``\ s (see :ref:`arbitrary-rank-polymorphism`). Consider this
   class: ::
diff --git a/docs/users_guide/exts/rank_polymorphism.rst b/docs/users_guide/exts/rank_polymorphism.rst
index d91c2fae6d..75066e8c7f 100644
--- a/docs/users_guide/exts/rank_polymorphism.rst
+++ b/docs/users_guide/exts/rank_polymorphism.rst
@@ -167,7 +167,7 @@ In the function ``h`` we use the record selectors ``return`` and
 ``MonadT`` data structure, rather than using pattern matching.
 
 
-.. _simple-subsumption:
+.. _subsumption:
 
 Subsumption
 -------------
@@ -209,13 +209,39 @@ A similar phenomenon occurs for operator sections. For example,
 ``(\`g3a\` "hello")`` is not well typed, but it can be made to typecheck by eta
 expanding it to ``\x -> x \`g3a\` "hello"``.
 
-Historical note.  Earlier versions of GHC allowed these now-rejected applications, by inserting
-automatic eta-expansions, as described in Section 4.6 of `Practical type inference for arbitrary-rank types <https://www.microsoft.com/en-us/research/publication/practical-type-inference-for-arbitrary-rank-types/>`__, where it is
-called "deep skolemisation".
-But these automatic eta-expansions may silently change the semantics of the user's program,
-and deep skolemisation was removed from the language by
-`GHC Proposal #287 <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0287-simplify-subsumption.rst>`__.
-This proposal has many more examples.
+.. extension:: DeepSubsumption
+    :shortdesc: Enable deep subsumption
+
+    :since: 9.2.4
+
+    Relax the simple subsumption rules, implicitly inserting eta-expansions
+    when matching up function types with different quantification structures.
+
+The :extension:`DeepSubsumption` extension relaxes the aforementioned requirement that
+foralls must appear in the same place. GHC will instead automatically rewrite expressions
+like ``f x`` of type ``ty1 -> ty2`` to become ``(\ (y :: ty1) -> f x y)``; this is called eta-expansion.
+See Section 4.6 of
+`Practical type inference for arbitrary-rank types <https://www.microsoft.com/en-us/research/publication/practical-type-inference-for-arbitrary-rank-types/>`__,
+where this process is called "deep skolemisation".
+
+Note that these eta-expansions may silently change the semantics of the user's program: ::
+
+  h1 :: Int -> forall a. a -> a
+  h1 = undefined
+  h2 :: forall b. Int -> b -> b
+  h2 = h1
+
+With :extension:`DeepSubsumption`, GHC will accept these definitions,
+inserting an implicit eta-expansion: ::
+
+  h2 = \ i -> h1 i
+
+This means that ``h2 `seq` ()`` will not crash, even though ``h1 `seq` ()`` does crash.
+
+Historical note: Deep skolemisation was initially removed from the language by
+`GHC Proposal #287 <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0287-simplify-subsumption.rst>`__,
+but was re-introduced as part of the :extension:`DeepSubsumption` extension following
+`GHC Proposal #511 <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0511-deep-subsumption.rst>`__.
 
 .. _higher-rank-type-inference: