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, 18 insertions, 3 deletions

diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs
index 22b627a36f..cd628b5622 100644
--- a/compiler/GHC/Tc/Validity.hs
+++ b/compiler/GHC/Tc/Validity.hs
@@ -26,7 +26,7 @@ import GHC.Prelude
 import GHC.Data.Maybe
 
 -- friends:
-import GHC.Tc.Utils.Unify    ( tcSubTypeSigma )
+import GHC.Tc.Utils.Unify    ( tcSubTypeAmbiguity )
 import GHC.Tc.Solver         ( simplifyAmbiguityCheck )
 import GHC.Tc.Instance.Class ( matchGlobalInst, ClsInstResult(..), InstanceWhat(..), AssocInstInfo(..) )
 import GHC.Core.TyCo.FVs
@@ -141,7 +141,9 @@ This neatly takes account of the functional dependency stuff above,
 and implicit parameter (see Note [Implicit parameters and ambiguity]).
 And this is what checkAmbiguity does.
 
-What about this, though?
+Note [The squishiness of the ambiguity check]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+What about this?
    g :: C [a] => Int
 Is every call to 'g' ambiguous?  After all, we might have
    instance C [a] where ...
@@ -152,6 +154,17 @@ with -XFlexibleInstances we could have
 and now a call could be legal after all!  Well, we'll reject this
 unless the instance is available *here*.
 
+But even that's not quite right. Even a function with an utterly-ambiguous
+type like f :: Eq a => Int -> Int
+is still callable if you are prepared to use visible type application,
+thus (f @Bool x).
+
+In short, the ambiguity check is a good-faith attempt to say "you are likely
+to have trouble if your function has this type"; it is NOT the case that
+"you can't call this function without giving a type error".
+
+See also Note [Ambiguity check and deep subsumption] in GHC.Tc.Utils.Unify.
+
 Note [When to call checkAmbiguity]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We call checkAmbiguity
@@ -220,7 +233,9 @@ checkAmbiguity ctxt ty
        ; allow_ambiguous <- xoptM LangExt.AllowAmbiguousTypes
        ; (_wrap, wanted) <- addErrCtxt (mk_msg allow_ambiguous) $
                             captureConstraints $
-                            tcSubTypeSigma (AmbiguityCheckOrigin ctxt) ctxt ty ty
+                            tcSubTypeAmbiguity ctxt ty ty
+                            -- See Note [Ambiguity check and deep subsumption]
+                            -- in GHC.Tc.Utils.Unify
        ; simplifyAmbiguityCheck ty wanted
 
        ; traceTc "Done ambiguity check for" (ppr ty) }