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

8 files changed, 161 insertions, 5 deletions

diff --git a/testsuite/tests/typecheck/should_compile/DeepSubsumption01.hs b/testsuite/tests/typecheck/should_compile/DeepSubsumption01.hs
new file mode 100644
index 0000000000..d07525b7eb
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/DeepSubsumption01.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE DeepSubsumption #-}
+module Repro where
+
+import GHC.Generics
+import Data.Binary
+
+data FFIType
+  = FFIVoid
+  deriving (Show, Generic, Binary)
diff --git a/testsuite/tests/typecheck/should_compile/DeepSubsumption02.hs b/testsuite/tests/typecheck/should_compile/DeepSubsumption02.hs
new file mode 100644
index 0000000000..fe8be78f38
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/DeepSubsumption02.hs
@@ -0,0 +1,73 @@
+{-# LANGUAGE BangPatterns, Rank2Types, FlexibleContexts, LambdaCase, DeepSubsumption #-}
+module DeepSubsumption02 where
+
+import Data.Semigroup
+
+-- | Finite source
+type Source r s = Tap r (Maybe s)
+
+newtype Sink t m a = Sink
+  { unSink :: forall r. t m -> (a -> t m -> m r) -> m r }
+
+-- | Mono in/out
+type Converter p q r s m = Source r s (Sink (Source p q) m)
+
+type Pipe a b m = forall r. (Monoid r, Semigroup r) => Converter r a r b m
+
+newtype Tap r s m = Tap { unTap :: r -> m (s, Tap r s m) }
+
+type Distiller tap r s m = Tap r s (Sink tap m)
+
+filter :: Monad m => (a -> Bool) -> Pipe a a m
+--filter f = filtering $ maybe True f
+filter = filtering . maybe True
+{-# INLINE filter #-}
+
+mapAccum :: Monad m => (s -> a -> (s, b)) -> s -> Pipe a b m
+--mapAccum f x = go x where
+mapAccum f = go where
+  go s = reservingTap $ \case
+    Just a -> let (s', b) = f s a in return (Just b, go s')
+    Nothing -> return (Nothing, go s)
+{-# INLINE mapAccum #-}
+
+traverse :: (Monad m) => (a -> m b) -> Pipe a b m
+-- traverse f = traversing $ Prelude.traverse f
+traverse = traversing . Prelude.traverse
+{-# INLINE traverse #-}
+
+-- | Get one element preserving a request
+reservingTap :: Monad m => (a -> Sink (Tap r a) m (b, Distiller (Tap r a) r b m)) -> Distiller (Tap r a) r b m
+reservingTap k = Tap $ \r -> Sink $ \t cont -> do
+  (a, t') <- unTap t r
+  unSink (k a) t' cont
+{-# INLINE reservingTap #-}
+
+traversing :: (Monad m) => (a -> m b) -> Distiller (Tap r a) r b m
+traversing f = go where
+  go = reservingTap $ \a -> do
+    b <- undefined $ f a
+    return (b, go)
+{-# INLINE traversing #-}
+
+filtering :: (Monoid r, Monad m) => (a -> Bool) -> Distiller (Tap r a) r a m
+filtering f = go where
+  go = reservingTap $ \a -> if f a
+    then return (a, go)
+    else unTap go mempty
+{-# INLINE filtering #-}
+
+instance Functor (Sink s m) where
+  fmap f m = Sink $ \s k -> unSink m s (k . f)
+
+instance Applicative (Sink s m) where
+  pure a = Sink $ \s k -> k a s
+  Sink mf <*> Sink mx = Sink
+    $ \s k -> mf s $ \f s' -> mx s' $ k . f
+  m *> k = m >>= \_ -> k
+
+instance Monad (Sink s m) where
+  return = pure
+  {-# INLINE return #-}
+  m >>= k = Sink $ \s cont -> unSink m s $ \a s' -> unSink (k a) s' cont
+
diff --git a/testsuite/tests/typecheck/should_compile/DeepSubsumption03.hs b/testsuite/tests/typecheck/should_compile/DeepSubsumption03.hs
new file mode 100644
index 0000000000..8f8c465047
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/DeepSubsumption03.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE DeepSubsumption #-}
+{-# LANGUAGE NoPolyKinds #-}
+module DeepSubsumption03 where
+
+class Profunctor p where
+  dimap :: (s -> a) -> (b -> t) -> p i a b -> p i s t
+
+type Iso s t a b = forall p i . Profunctor p => p i a b -> p i s t
+
+iso :: (s -> a) -> (b -> t) -> Iso s t a b
+-- iso f g = dimap f g
+iso = dimap
diff --git a/testsuite/tests/typecheck/should_compile/DeepSubsumption04.hs b/testsuite/tests/typecheck/should_compile/DeepSubsumption04.hs
new file mode 100644
index 0000000000..abaf8d569b
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/DeepSubsumption04.hs
@@ -0,0 +1,29 @@
+{-# LANGUAGE DeepSubsumption #-}
+{-# LANGUAGE KindSignatures #-}
+module DeepSubsumption04 where
+
+import Data.Kind
+
+data TermOutput = TermOutput
+
+type TermAction = () -> TermOutput
+
+type ActionT = WriterT TermAction
+
+class MonadReader r m  where
+  ask :: m r
+
+data WriterT w (m :: Type -> Type) a = WriterT
+
+type ActionM a = forall m . (MonadReader () m) => ActionT m a
+
+output :: TermAction -> ActionM ()
+output t = undefined
+
+termText :: String -> TermOutput
+termText = undefined
+
+outputText :: String -> ActionM ()
+outputText = output . const . termText
+--outputText x = output . const . termText $ x
+
diff --git a/testsuite/tests/typecheck/should_compile/DeepSubsumption05.hs b/testsuite/tests/typecheck/should_compile/DeepSubsumption05.hs
new file mode 100644
index 0000000000..a6d9db3cb9
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/DeepSubsumption05.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE DeepSubsumption #-}
+module DeepSubsumption06 where
+
+type Traversal' s a = forall f . Applicative f => (a -> a) -> f s -> f s
+type LensLike f m a = (a -> a) -> f m -> f m
+
+class Ixed m where
+  ix :: () -> Traversal' m ()
+
+  default ix :: (Applicative f) => () -> LensLike f m ()
+  ix = undefined
diff --git a/testsuite/tests/typecheck/should_compile/T21548a.hs b/testsuite/tests/typecheck/should_compile/T21548a.hs
new file mode 100644
index 0000000000..399f3e5386
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T21548a.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE RankNTypes, DeepSubsumption #-}
+
+module T21548a where
+
+f1 :: (forall a. a -> forall b. b -> b) -> Int
+f1 = f1
+
+g1 :: forall p q. p -> q -> q
+g1 = g1
+
+foo1 = f1 g1
+
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 62edaf99e6..3410ad68bb 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -843,3 +843,9 @@ test('T18802', normal, compile, [''])
 test('T18802b', normal, compile, [''])
 test('T21289', normal, compile, [''])
 test('HardRecordUpdate', normal, compile, [''])
+test('T21548a', normal, compile, [''])
+test('DeepSubsumption01', normal, compile, [''])
+test('DeepSubsumption02', normal, compile, [''])
+test('DeepSubsumption03', normal, compile, [''])
+test('DeepSubsumption04', normal, compile, [''])
+test('DeepSubsumption05', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/T14618.stderr b/testsuite/tests/typecheck/should_fail/T14618.stderr
index 05a763048e..6cf768bbce 100644
--- a/testsuite/tests/typecheck/should_fail/T14618.stderr
+++ b/testsuite/tests/typecheck/should_fail/T14618.stderr
@@ -1,10 +1,10 @@
 
 T14618.hs:7:14: error:
-    • Couldn't match type ‘b’ with ‘forall c. a’
-      Expected: a -> b
-        Actual: a -> forall c. a
-      Cannot equate type variable ‘b’
-      with a type involving polytypes: forall c. a
+    • Couldn't match expected type ‘b’ with actual type ‘a’
+      ‘a’ is a rigid type variable bound by
+        the type signature for:
+          safeCoerce :: forall a b. a -> b
+        at T14618.hs:6:1-20
       ‘b’ is a rigid type variable bound by
         the type signature for:
           safeCoerce :: forall a b. a -> b