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, 11 insertions, 9 deletions

diff --git a/testsuite/tests/indexed-types/should_compile/Simple14.hs b/testsuite/tests/indexed-types/should_compile/Simple14.hs
index bedf5bb3e7..a1b2e5eaca 100644
--- a/testsuite/tests/indexed-types/should_compile/Simple14.hs
+++ b/testsuite/tests/indexed-types/should_compile/Simple14.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE Haskell2010 #-}
 {-# LANGUAGE TypeFamilies, RankNTypes, FlexibleContexts, ScopedTypeVariables #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
 
 module Simple14 where
 
@@ -7,6 +8,7 @@ data EQ_ x y = EQ_
 
 -- Nov 2014: actually eqE has an ambiguous type
 -- Apr 2020: now it doesn't again
+-- Jun 2022: now it does again -- because of DeepSubsumption
 eqE :: EQ_ x y -> (x~y => EQ_ z z) -> p
 eqE x y = error "eqE"
 
diff --git a/testsuite/tests/indexed-types/should_compile/Simple14.stderr b/testsuite/tests/indexed-types/should_compile/Simple14.stderr
index 7489ffce5a..c9c83b6434 100644
--- a/testsuite/tests/indexed-types/should_compile/Simple14.stderr
+++ b/testsuite/tests/indexed-types/should_compile/Simple14.stderr
@@ -1,21 +1,21 @@
 
-Simple14.hs:20:27: error:
+Simple14.hs:22:27: error:
     • Couldn't match type ‘z0’ with ‘n’
       Expected: EQ_ z0 z0
         Actual: EQ_ m n
-        ‘z0’ is untouchable
-          inside the constraints: Maybe m ~ Maybe n
-          bound by a type expected by the context:
-                     (Maybe m ~ Maybe n) => EQ_ z0 z0
-          at Simple14.hs:20:26-41
+    • ‘z0’ is untouchable
+        inside the constraints: Maybe m ~ Maybe n
+        bound by a type expected by the context:
+                   (Maybe m ~ Maybe n) => EQ_ z0 z0
+        at Simple14.hs:22:26-41
       ‘n’ is a rigid type variable bound by
         the type signature for:
           foo :: forall m n. EQ_ (Maybe m) (Maybe n)
-        at Simple14.hs:19:1-42
+        at Simple14.hs:21:1-42
     • In the second argument of ‘eqE’, namely ‘(eqI :: EQ_ m n)’
       In the expression: x `eqE` (eqI :: EQ_ m n)
       In the first argument of ‘ntI’, namely
         ‘(\ x -> x `eqE` (eqI :: EQ_ m n))’
     • Relevant bindings include
-        x :: EQ_ (Maybe m) (Maybe n) (bound at Simple14.hs:20:13)
-        foo :: EQ_ (Maybe m) (Maybe n) (bound at Simple14.hs:20:1)
+        x :: EQ_ (Maybe m) (Maybe n) (bound at Simple14.hs:22:13)
+        foo :: EQ_ (Maybe m) (Maybe n) (bound at Simple14.hs:22:1)