Add a missing zonk in tcHsPartialTypewip/T18008

I omitted a vital zonk when refactoring tcHsPartialType in
   commit 48fb3482f8cbc8a4b37161021e846105f980eed4
   Author: Simon Peyton Jones <simonpj@microsoft.com>
   Date:   Wed Jun 5 08:55:17 2019 +0100

   Fix typechecking of partial type signatures

This patch fixes it and adds commentary to explain why.

Fixes #18008

4 files changed, 94 insertions, 14 deletions

diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index be5b4f7694..094ed623ac 100644
--- a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ -732,6 +732,7 @@ tc_hs_type mode forall@(HsForAllTy { hst_fvf = fvf, hst_bndrs = hs_tvs
              m_telescope = Just (sep (map ppr hs_tvs))
 
        ; emitResidualTvConstraint skol_info m_telescope tvs' tclvl wanted
+         -- See Note [Skolem escape and forall-types]
 
        ; return (mkForAllTys bndrs ty') }
 
@@ -920,6 +921,26 @@ under these conditions.
 See related Note [Wildcards in visible type application] here and
 Note [The wildcard story for types] in GHC.Hs.Types
 
+Note [Skolem escape and forall-types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+  f :: forall a. (forall kb (b :: kb). Proxy '[a, b]) -> ()
+
+The Proxy '[a,b] forces a and b to have the same kind.  But a's
+kind must be bound outside the 'forall a', and hence escapes.
+We discover this by building an implication constraint for
+each forall.  So the inner implication constraint will look like
+    forall kb (b::kb).  kb ~ ka
+where ka is a's kind.  We can't unify these two, /even/ if ka is
+unification variable, because it would be untouchable inside
+this inner implication.
+
+That's what the pushLevelAndCaptureConstraints, plus subsequent
+emitResidualTvConstraint is all about, when kind-checking
+HsForAllTy.
+
+Note that we don't need to /simplify/ the constraints here
+because we aren't generalising. We just capture them.
 -}
 
 {- *********************************************************************
@@ -2819,10 +2840,13 @@ kindGeneralizeAll ty = do { traceTc "kindGeneralizeAll" empty
                           ; kindGeneralizeSome (const True) ty }
 
 -- | Specialized version of 'kindGeneralizeSome', but where no variables
--- can be generalized. Use this variant when it is unknowable whether metavariables
--- might later be constrained.
--- See Note [Recipe for checking a signature] for why and where this
--- function is needed.
+-- can be generalized, but perhaps some may neeed to be promoted.
+-- Use this variant when it is unknowable whether metavariables might
+-- later be constrained.
+--
+-- To see why this promotion is needed, see
+-- Note [Recipe for checking a signature], and especially
+-- Note [Promotion in signatures].
 kindGeneralizeNone :: TcType  -- needn't be zonked
                    -> TcM ()
 kindGeneralizeNone ty
@@ -3160,7 +3184,7 @@ tcHsPartialSigType ctxt sig_ty
 
                   ; return (wcs, wcx, theta, tau) }
 
-         -- No kind-generalization here:
+       -- No kind-generalization here, but perhaps some promotion
        ; kindGeneralizeNone (mkSpecForAllTys implicit_tvs $
                              mkSpecForAllTys explicit_tvs $
                              mkPhiTy theta $
@@ -3171,6 +3195,14 @@ tcHsPartialSigType ctxt sig_ty
        -- See Note [Extra-constraint holes in partial type signatures]
        ; emitNamedWildCardHoleConstraints wcs
 
+       -- Zonk, so that any nested foralls can "see" their occurrences
+       -- See Note [Checking partial type signatures], in
+       -- the bullet on Nested foralls.
+       ; implicit_tvs <- mapM zonkTcTyVarToTyVar implicit_tvs
+       ; explicit_tvs <- mapM zonkTcTyVarToTyVar explicit_tvs
+       ; theta        <- mapM zonkTcType theta
+       ; tau          <- zonkTcType tau
+
          -- We return a proper (Name,TyVar) environment, to be sure that
          -- we bring the right name into scope in the function body.
          -- Test case: partial-sigs/should_compile/LocalDefinitionBug
@@ -3179,7 +3211,7 @@ tcHsPartialSigType ctxt sig_ty
 
       -- NB: checkValidType on the final inferred type will be
       --     done later by checkInferredPolyId.  We can't do it
-      --     here because we don't have a complete tuype to check
+      --     here because we don't have a complete type to check
 
        ; traceTc "tcHsPartialSigType" (ppr tv_prs)
        ; return (wcs, wcx, tv_prs, theta, tau) }
@@ -3198,12 +3230,31 @@ tcPartialContext hs_theta
 
 {- Note [Checking partial type signatures]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-See also Note [Recipe for checking a signature]
+This Note is about tcHsPartialSigType.  See also
+Note [Recipe for checking a signature]
 
 When we have a partial signature like
-   f,g :: forall a. a -> _
+   f :: forall a. a -> _
 we do the following
 
+* tcHsPartialSigType does not make quantified type (forall a. blah)
+  and then instantiate it -- it makes no sense to instantiate a type
+  with wildcards in it.  Rather, tcHsPartialSigType just returns the
+  'a' and the 'blah' separately.
+
+  Nor, for the same reason, do we push a level in tcHsPartialSigType.
+
+* We instantiate 'a' to a unification variable, a TyVarTv, and /not/
+  a skolem; hence the "_Tv" in bindExplicitTKBndrs_Tv.  Consider
+    f :: forall a. a -> _
+    g :: forall b. _ -> b
+    f = g
+    g = f
+  They are typechecked as a recursive group, with monomorphic types,
+  so 'a' and 'b' will get unified together.  Very like kind inference
+  for mutually recursive data types (sans CUSKs or SAKS); see
+  Note [Cloning for tyvar binders] in GHC.Tc.Gen.HsType
+
 * In GHC.Tc.Gen.Sig.tcUserSigType we return a PartialSig, which (unlike
   the companion CompleteSig) contains the original, as-yet-unchecked
   source-code LHsSigWcType
@@ -3218,12 +3269,28 @@ we do the following
      g x = True
   It's really as if we'd written two distinct signatures.
 
-* Note that we don't make quantified type (forall a. blah) and then
-  instantiate it -- it makes no sense to instantiate a type with
-  wildcards in it.  Rather, tcHsPartialSigType just returns the
-  'a' and the 'blah' separately.
-
-  Nor, for the same reason, do we push a level in tcHsPartialSigType.
+* Nested foralls. Consider
+     f :: forall b. (forall a. a -> _) -> b
+  We do /not/ allow the "_" to be instantiated to 'a'; but we do
+  (as before) allow it to be instantiated to the (top level) 'b'.
+  Why not?  Because suppose
+     f x = (x True, x 'c')
+  We must instantiate that (forall a. a -> _) when typechecking
+  f's body, so we must know precisely where all the a's are; they
+  must not be hidden under (filled-in) unification variables!
+
+  We achieve this in the usual way: we push a level at a forall,
+  so now the unification variable for the "_" can't unify with
+  'a'.
+
+* Just as for ordinary signatures, we must zonk the type after
+  kind-checking it, to ensure that all the nested forall binders can
+  see their occurrenceds
+
+  Just as for ordinary signatures, this zonk also gets any Refl casts
+  out of the way of instantiation.  Example: #18008 had
+       foo :: (forall a. (Show a => blah) |> Refl) -> _
+  and that Refl cast messed things up.  See #18062.
 
 Note [Extra-constraint holes in partial type signatures]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/testsuite/tests/partial-sigs/should_compile/T18008.hs b/testsuite/tests/partial-sigs/should_compile/T18008.hs
new file mode 100644
index 0000000000..5e76173a04
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_compile/T18008.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE PartialTypeSignatures #-}
+module Bug where
+
+f :: (forall a. Show a => a -> String) -> _
+f s = s ()
+
diff --git a/testsuite/tests/partial-sigs/should_compile/T18008.stderr b/testsuite/tests/partial-sigs/should_compile/T18008.stderr
new file mode 100644
index 0000000000..4b59da8b03
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_compile/T18008.stderr
@@ -0,0 +1,5 @@
+
+T18008.hs:5:43: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’ standing for ‘String’
+    • In the type ‘(forall a. Show a => a -> String) -> _’
+      In the type signature: f :: (forall a. Show a => a -> String) -> _
diff --git a/testsuite/tests/partial-sigs/should_compile/all.T b/testsuite/tests/partial-sigs/should_compile/all.T
index 4cb12ed144..e8d84fe3bb 100644
--- a/testsuite/tests/partial-sigs/should_compile/all.T
+++ b/testsuite/tests/partial-sigs/should_compile/all.T
@@ -95,3 +95,4 @@ test('T16334', normal, compile, [''])
 test('T16728', normal, compile, [''])
 test('T16728a', normal, compile, [''])
 test('T16728b', normal, compile, [''])
+test('T18008', normal, compile, [''])