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.

(cherry picked from commit 7b9be6c8b94b3c2eb3441febb4a8005a03fa34a5)

2 files changed, 19 insertions, 0 deletions

diff --git a/libraries/ghc-boot-th/GHC/LanguageExtensions/Type.hs b/libraries/ghc-boot-th/GHC/LanguageExtensions/Type.hs
index ce07116a1e..76b20bed35 100644
--- a/libraries/ghc-boot-th/GHC/LanguageExtensions/Type.hs
+++ b/libraries/ghc-boot-th/GHC/LanguageExtensions/Type.hs
@@ -30,6 +30,7 @@ data Extension
    | UndecidableSuperClasses
    | MonomorphismRestriction
    | MonoLocalBinds
+   | DeepSubsumption
    | RelaxedPolyRec           -- Deprecated
    | ExtendedDefaultRules     -- Use GHC's extended rules for defaulting
    | ForeignFunctionInterface
diff --git a/libraries/ghc-prim/GHC/Magic/Dict.hs b/libraries/ghc-prim/GHC/Magic/Dict.hs
index 560ab3956f..34886fee3b 100644
--- a/libraries/ghc-prim/GHC/Magic/Dict.hs
+++ b/libraries/ghc-prim/GHC/Magic/Dict.hs
@@ -5,6 +5,7 @@
 {-# LANGUAGE NoImplicitPrelude #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}  -- See Note [withDict has an ambiguous type]
 {-# LANGUAGE Unsafe #-}
 
 -----------------------------------------------------------------------------
@@ -40,3 +41,20 @@ import GHC.Types (RuntimeRep, TYPE)
 -- @Note [withDict]@ in "GHC.Tc.Instance.Class" in GHC.
 class WithDict cls meth where
   withDict :: forall {rr :: RuntimeRep} (r :: TYPE rr). meth -> (cls => r) -> r
+
+{- Note [withDict has an ambiguous type]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The type of `withDict` is ambiguous.  Consider
+   foo :: forall cls meth. WithDict cls meth
+       => forall rr (r::rr). meth -> (cls => r) -> r
+   foo m k = withDict m k
+
+If we instantiate `withDict` with fresh unification variables, including cls0 for cls,
+there is nothing that forces the `cls` Wanted from the call to `k` to unify with the
+`cls0` Given from the call to `withDict`.  You have to give it a class argument:
+
+   foo m k = withDict @cls m k
+
+That's fine.  But it means we need -XAllowAmbiguousTypes for the withDict definition,
+at least with deep subsumption.
+-}
\ No newline at end of file