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].

1 files changed, 10 insertions, 6 deletions

diff --git a/compiler/GHC/Tc/Gen/Head.hs b/compiler/GHC/Tc/Gen/Head.hs
index a56b9c833e..1c72c877ab 100644
--- a/compiler/GHC/Tc/Gen/Head.hs
+++ b/compiler/GHC/Tc/Gen/Head.hs
@@ -1402,9 +1402,9 @@ addFunResCtxt fun args fun_res_ty env_ty thing_inside
            ; let -- See Note [Splitting nested sigma types in mismatched
                  --           function types]
                  (_, _, fun_tau) = tcSplitNestedSigmaTys fun_res'
-                 -- No need to call tcSplitNestedSigmaTys here, since env_ty is
-                 -- an ExpRhoTy, i.e., it's already instantiated.
-                 (_, _, env_tau) = tcSplitSigmaTy env'
+                 (_, _, env_tau) = tcSplitNestedSigmaTys env'
+                     -- env_ty is an ExpRhoTy, but with simple subsumption it
+                     -- is not deeply skolemised, so still use tcSplitNestedSigmaTys
                  (args_fun, res_fun) = tcSplitFunTys fun_tau
                  (args_env, res_env) = tcSplitFunTys env_tau
                  n_fun = length args_fun
@@ -1451,7 +1451,7 @@ Previously, GHC computed the number of argument types through tcSplitSigmaTy.
 This is incorrect in the face of nested foralls, however!
 This caused Ticket #13311, for instance:
 
-  f :: forall a. (Monoid a) => forall b. (Monoid b) => Maybe a -> Maybe b
+  f :: forall a. (Monoid a) => Int -> forall b. (Monoid b) => Maybe a -> Maybe b
 
 If one uses `f` like so:
 
@@ -1462,7 +1462,7 @@ Then tcSplitSigmaTy will decompose the type of `f` into:
   Tyvars: [a]
   Context: (Monoid a)
   Argument types: []
-  Return type: forall b. Monoid b => Maybe a -> Maybe b
+  Return type: Int -> forall b. Monoid b => Maybe a -> Maybe b
 
 That is, it will conclude that there are *no* argument types, and since `f`
 was given no arguments, it won't print a helpful error message. On the other
@@ -1470,11 +1470,15 @@ hand, tcSplitNestedSigmaTys correctly decomposes `f`'s type down to:
 
   Tyvars: [a, b]
   Context: (Monoid a, Monoid b)
-  Argument types: [Maybe a]
+  Argument types: [Int, Maybe a]
   Return type: Maybe b
 
 So now GHC recognizes that `f` has one more argument type than it was actually
 provided.
+
+Notice that tcSplitNestedSigmaTys looks through function arrows too, regardless
+of simple/deep subsumption.  Here we are concerned only whether there is a
+mis-match in the number of value arguments.
 -}