Fix #11305.

Summary:
In the fallthrough case when doing a subsumption case, we
need to deeply instantiate to remove any buried foralls in
the "actual" type.

Once this validates, please feel free to commit it; I may not
have the chance to do this on Tuesday. Back in full action on
Wed.

Test Plan: ./validate, typecheck/should_compiler/T11305

Reviewers: austin, bgamari, hvr

Subscribers: thomie

Differential Revision: https://phabricator.haskell.org/D1715

GHC Trac Issues: #11305

3 files changed, 90 insertions, 25 deletions

diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs
index b7bc77db73..908b6920a3 100644
--- a/compiler/typecheck/TcUnify.hs
+++ b/compiler/typecheck/TcUnify.hs
@@ -630,7 +630,7 @@ tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected
                  do { traceTc "tcSubTypeDS_NC_O following filled act meta-tyvar:"
                         (ppr tv_a <+> text "-->" <+> ppr ty_a')
                     ; tc_sub_type_ds eq_orig inst_orig ctxt ty_a' ty_e }
-               Unfilled _   -> mkWpCastN <$> unify }
+               Unfilled _   -> unify }
 
 
     go ty_a (TyVarTy tv_e)
@@ -645,33 +645,14 @@ tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected
                Unfilled details
                  |  canUnifyWithPolyType dflags details
                     && isTouchableMetaTyVar tclvl tv_e  -- don't want skolems here
-                 -> mkWpCastN <$> unify
+                 -> unify
 
      -- We've avoided instantiating ty_actual just in case ty_expected is
      -- polymorphic. But we've now assiduously determined that it is *not*
      -- polymorphic. So instantiate away. This is needed for e.g. test
      -- typecheck/should_compile/T4284.
                  |  otherwise
-                 -> do { (wrap, rho_a) <- deeplyInstantiate inst_orig ty_actual
-
-                           -- if we haven't recurred through an arrow, then
-                           -- the eq_orig will list ty_actual. In this case,
-                           -- we want to update the origin to reflect the
-                           -- instantiation. If we *have* recurred through
-                           -- an arrow, it's better not to update.
-                       ; let eq_orig' = case eq_orig of
-                               TypeEqOrigin { uo_actual   = orig_ty_actual
-                                            , uo_expected = orig_ty_expected
-                                            , uo_thing    = thing }
-                                 |  orig_ty_actual `tcEqType` ty_actual
-                                 -> TypeEqOrigin
-                                      { uo_actual = rho_a
-                                      , uo_expected = orig_ty_expected
-                                      , uo_thing    = thing }
-                               _ -> eq_orig
-
-                       ; cow <- uType eq_orig' TypeLevel rho_a ty_expected
-                       ; return (mkWpCastN cow <.> wrap) } }
+                 -> inst_and_unify }
 
     go (ForAllTy (Anon act_arg) act_res) (ForAllTy (Anon exp_arg) exp_res)
       | not (isPredTy act_arg)
@@ -693,11 +674,37 @@ tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected
            ; return (body_wrap <.> in_wrap) }
 
       | otherwise   -- Revert to unification
-      = do { cow <- unify
-           ; return (mkWpCastN cow) }
+      = inst_and_unify
+         -- It's still possible that ty_actual has nested foralls. Instantiate
+         -- these, as there's no way unification will succeed with them in.
+         -- See typecheck/should_compiler/T11350 for an example of when this
+         -- is important.
+
+    inst_and_unify = do { (wrap, rho_a) <- deeplyInstantiate inst_orig ty_actual
+
+                           -- if we haven't recurred through an arrow, then
+                           -- the eq_orig will list ty_actual. In this case,
+                           -- we want to update the origin to reflect the
+                           -- instantiation. If we *have* recurred through
+                           -- an arrow, it's better not to update.
+                        ; let eq_orig' = case eq_orig of
+                                TypeEqOrigin { uo_actual   = orig_ty_actual
+                                             , uo_expected = orig_ty_expected
+                                             , uo_thing    = thing }
+                                  |  orig_ty_actual `tcEqType` ty_actual
+                                  ,  not (isIdHsWrapper wrap)
+                                  -> TypeEqOrigin
+                                       { uo_actual = rho_a
+                                       , uo_expected = orig_ty_expected
+                                       , uo_thing    = thing }
+                                _ -> eq_orig
+
+                        ; cow <- uType eq_orig' TypeLevel rho_a ty_expected
+                        ; return (mkWpCastN cow <.> wrap) }
+
 
      -- use versions without synonyms expanded
-    unify = uType eq_orig TypeLevel ty_actual ty_expected
+    unify = mkWpCastN <$> uType eq_orig TypeLevel ty_actual ty_expected
 
 -----------------
 -- needs both un-type-checked (for origins) and type-checked (for wrapping)
diff --git a/testsuite/tests/typecheck/should_compile/T11305.hs b/testsuite/tests/typecheck/should_compile/T11305.hs
new file mode 100644
index 0000000000..14cb955ed5
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T11305.hs
@@ -0,0 +1,57 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Data.Profunctor.Strong where
+
+import Control.Arrow
+import Control.Category
+import Data.Tuple
+import Prelude hiding (id,(.))
+
+infixr 0 :->
+type p :-> q = forall a b. p a b -> q a b
+
+class Profunctor p where
+  dimap :: (a -> b) -> (c -> d) -> p b c -> p a d
+
+class ProfunctorFunctor t where
+  promap    :: Profunctor p => (p :-> q) -> t p :-> t q
+
+class ProfunctorFunctor t => ProfunctorMonad t where
+  proreturn :: Profunctor p => p       :-> t p
+  projoin   :: Profunctor p => t (t p) :-> t p
+
+class ProfunctorFunctor t => ProfunctorComonad t where
+  proextract   :: Profunctor p => t p :-> p
+  produplicate :: Profunctor p => t p :-> t (t p)
+
+class Profunctor p => Strong p where
+  first' :: p a b  -> p (a, c) (b, c)
+  first' = dimap swap swap . second'
+
+  second' :: p a b -> p (c, a) (c, b)
+  second' = dimap swap swap . first'
+
+----------------------------------------------------------------------------
+
+newtype Tambara p a b = Tambara { runTambara :: forall c. p (a, c) (b, c) }
+
+instance Profunctor p => Profunctor (Tambara p) where
+  dimap f g (Tambara p) = Tambara $ dimap (first f) (first g) p
+
+instance ProfunctorFunctor Tambara where
+  promap f (Tambara p) = Tambara (f p)
+
+instance ProfunctorComonad Tambara where
+  proextract (Tambara p) = dimap (\a -> (a,())) fst p
+
+  produplicate (Tambara p) = Tambara (Tambara $ dimap hither yon p)
+    where
+      hither :: ((a, b), c) -> (a, (b, c))
+      hither ~(~(x,y),z) = (x,(y,z))
+
+      yon    :: (a, (b, c)) -> ((a, b), c)
+      yon    ~(x,~(y,z)) = ((x,y),z)
+
+instance Profunctor p => Strong (Tambara p) where
+  first' = runTambara . produplicate
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 20ef3a7b47..3fa1f8cfaa 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -486,3 +486,4 @@ test('T10971a', normal, compile, [''])
 test('T11237', normal, compile, [''])
 test('T10592', normal, compile, [''])
 test('T11254', expect_broken(11254), compile, [''])
+test('T11305', normal, compile, [''])