Fix tcSplitNestedSigmaTys

When I did the shallow-subusmptuion 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].

(cherry picked from commit 936fe7435d9da63f78c032b027179e1f1f22a482)
(cherry picked from commit 58ad696d42316b1a89a3ce8324218a0ad7257b8e)
(cherry picked from commit dc27e15a76486b1ebd27a77f8515044c2671e22d)

4 files changed, 60 insertions, 26 deletions

diff --git a/compiler/GHC/Tc/Gen/Head.hs b/compiler/GHC/Tc/Gen/Head.hs
index 7e569a8b24..ab52a152a7 100644
--- a/compiler/GHC/Tc/Gen/Head.hs
+++ b/compiler/GHC/Tc/Gen/Head.hs
@@ -1191,9 +1191,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
@@ -1240,7 +1240,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:
 
@@ -1251,7 +1251,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
@@ -1259,11 +1259,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.
 -}
 
 
diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs
index 00b3aa69a2..2cc14e8b00 100644
--- a/compiler/GHC/Tc/Utils/TcType.hs
+++ b/compiler/GHC/Tc/Utils/TcType.hs
@@ -1316,35 +1316,51 @@ tcSplitSigmaTy ty = case tcSplitForAllInvisTyVars ty of
                         (tvs, rho) -> case tcSplitPhiTy rho of
                                         (theta, tau) -> (tvs, theta, tau)
 
--- | Split a sigma type into its parts, going underneath as many @ForAllTy@s
--- as possible. For example, given this type synonym:
---
--- @
--- type Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f t
--- @
---
--- if you called @tcSplitSigmaTy@ on this type:
---
--- @
--- forall s t a b. Each s t a b => Traversal s t a b
--- @
---
--- then it would return @([s,t,a,b], [Each s t a b], Traversal s t a b)@. But
--- if you instead called @tcSplitNestedSigmaTys@ on the type, it would return
--- @([s,t,a,b,f], [Each s t a b, Applicative f], (a -> f b) -> s -> f t)@.
+-- | Split a sigma type into its parts, going underneath as many arrows
+-- and foralls as possible. See Note [tcSplitNestedSigmaTys]
 tcSplitNestedSigmaTys :: Type -> ([TyVar], ThetaType, Type)
--- NB: This is basically a pure version of topInstantiate (from Inst) that
--- doesn't compute an HsWrapper.
+-- See Note [tcSplitNestedSigmaTys]
+-- NB: This is basically a pure version of deeplyInstantiate (from Unify) that
+--     doesn't compute an HsWrapper.
 tcSplitNestedSigmaTys ty
     -- If there's a forall, split it apart and try splitting the rho type
     -- underneath it.
-  | (tvs1, theta1, rho1) <- tcSplitSigmaTy ty
+  | (arg_tys, body_ty)   <- tcSplitFunTys ty
+  , (tvs1, theta1, rho1) <- tcSplitSigmaTy body_ty
   , not (null tvs1 && null theta1)
   = let (tvs2, theta2, rho2) = tcSplitNestedSigmaTys rho1
-    in (tvs1 ++ tvs2, theta1 ++ theta2, rho2)
+    in (tvs1 ++ tvs2, theta1 ++ theta2, mkVisFunTys arg_tys rho2)
+
     -- If there's no forall, we're done.
   | otherwise = ([], [], ty)
 
+{- Note [tcSplitNestedSigmaTys]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+tcSplitNestedSigmaTys splits out all the /nested/ foralls and constraints,
+including under function arrows.  E.g. given this type synonym:
+  type Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f t
+
+then
+  tcSplitNestedSigmaTys (forall s t a b. C s t a b => Int -> Traversal s t a b)
+
+will return
+  ( [s,t,a,b,f]
+  , [C s t a b, Applicative f]
+  , Int -> (a -> f b) -> s -> f t)@.
+
+This function is used in these places:
+* 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
+
+In other words, just in validity checking and error messages; hence
+no wrappers or evidence generation.
+
+Notice that tcSplitNestedSigmaTys even looks under function arrows;
+doing so is the Right Thing even with simple subsumption, not just
+with deep subsumption.
+-}
+
 -----------------------
 tcTyConAppTyCon :: Type -> TyCon
 tcTyConAppTyCon ty
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/all.T b/testsuite/tests/typecheck/should_compile/all.T
index fd18df7707..47ad8285c8 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -799,3 +799,4 @@ test('DeepSubsumption01', normal, compile, [''])
 test('DeepSubsumption02', normal, compile, [''])
 test('DeepSubsumption03', normal, compile, [''])
 test('DeepSubsumption04', normal, compile, [''])
+test('DeepSubsumption05', normal, compile, [''])