Fix typechecking of partial type signatures

Partial type sigs had grown hair.  tcHsParialSigType was
doing lots of unnecessary work, and tcInstSig was cloning it
unnecessarily -- and the result didn't even work: #16728.

This patch cleans it all up, described by TcHsType
  Note [Checking parital type signatures]

I basically just deleted code... but very carefully!

Some refactoring along the way

* Distinguish more explicintly between "anonymous" wildcards "_"
  and "named" wildcards "_a".  I changed the names of a number
  of functions to make this distinction much more apparent.

The patch also revealed that the code in `TcExpr`
that implements the special typing rule for `($)` was wrong.
It called `getRuntimeRep` in a situation where where was no
particular reason to suppose that the thing had kind `TYPE r`.

This caused a crash in typecheck/should_run/T10846.

The fix was easy, and actually simplifies the code in `TcExpr`
quite a bit.  Hooray.

18 files changed, 215 insertions, 124 deletions

diff --git a/compiler/rename/RnTypes.hs b/compiler/rename/RnTypes.hs
index 755ed206f0..4b4d519324 100644
--- a/compiler/rename/RnTypes.hs
+++ b/compiler/rename/RnTypes.hs
@@ -693,8 +693,8 @@ checkAnonWildCard env
            | otherwise
            = case rtke_what env of
                RnTypeBody      -> Nothing
-               RnConstraint    -> Just constraint_msg
                RnTopConstraint -> Just constraint_msg
+               RnConstraint    -> Just constraint_msg
 
     constraint_msg = hang
                          (notAllowed pprAnonWildCard <+> text "in a constraint")
@@ -714,7 +714,10 @@ checkNamedWildCard env name
            | otherwise
            = case rtke_what env of
                RnTypeBody      -> Nothing   -- Allowed
-               RnTopConstraint -> Nothing   -- Allowed
+               RnTopConstraint -> Nothing   -- Allowed; e.g.
+                  -- f :: (Eq _a) => _a -> Int
+                  -- g :: (_a, _b) => T _a _b -> Int
+                  -- The named tyvars get filled in from elsewhere
                RnConstraint    -> Just constraint_msg
     constraint_msg = notAllowed (ppr name) <+> text "in a constraint"
 
diff --git a/compiler/typecheck/TcBinds.hs b/compiler/typecheck/TcBinds.hs
index c8c1bc06bd..72748ac76f 100644
--- a/compiler/typecheck/TcBinds.hs
+++ b/compiler/typecheck/TcBinds.hs
@@ -1020,7 +1020,7 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs
 
            ; case tcGetCastedTyVar_maybe wc_var_ty of
                -- We know that wc_co must have type kind(wc_var) ~ Constraint, as it
-               -- comes from the checkExpectedKind in TcHsType.tcWildCardOcc. So, to
+               -- comes from the checkExpectedKind in TcHsType.tcAnonWildCardOcc. So, to
                -- make the kinds work out, we reverse the cast here.
                Just (wc_var, wc_co) -> writeMetaTyVar wc_var (ctuple `mkCastTy` mkTcSymCo wc_co)
                Nothing              -> pprPanic "chooseInferredQuantifiers 1" (ppr wc_var_ty)
diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index c296a9eee3..31c9ad9a89 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -1009,6 +1009,8 @@ can_eq_nc_forall ev eq_rel s1 s2
                                                   (substTy subst (tyVarKind tv2))
                    ; let subst' = extendTvSubstAndInScope subst tv2
                                        (mkCastTy (mkTyVarTy skol_tv) kind_co)
+                         -- skol_tv is already in the in-scope set, but the
+                         -- free vars of kind_co are not; hence "...AndInScope"
                    ; (co, wanteds2) <- go skol_tvs subst' bndrs2
                    ; return ( mkTcForAllCo skol_tv kind_co co
                             , wanteds1 `unionBags` wanteds2 ) }
diff --git a/compiler/typecheck/TcExpr.hs b/compiler/typecheck/TcExpr.hs
index adaea90767..891f3ad8c3 100644
--- a/compiler/typecheck/TcExpr.hs
+++ b/compiler/typecheck/TcExpr.hs
@@ -378,42 +378,35 @@ tcExpr expr@(OpApp fix arg1 op arg2) res_ty
          -- So: arg1_ty = arg2_ty -> op_res_ty
          -- where arg2_sigma maybe polymorphic; that's the point
 
-       ; arg2'  <- tcArg op arg2 arg2_sigma 2
+       ; arg2' <- tcArg op arg2 arg2_sigma 2
 
        -- Make sure that the argument type has kind '*'
        --   ($) :: forall (r:RuntimeRep) (a:*) (b:TYPE r). (a->b) -> a -> b
        -- Eg we do not want to allow  (D#  $  4.0#)   #5570
        --    (which gives a seg fault)
-       --
-       -- The *result* type can have any kind (#8739),
-       -- so we don't need to check anything for that
        ; _ <- unifyKind (Just (XHsType $ NHsCoreTy arg2_sigma))
                         (tcTypeKind arg2_sigma) liftedTypeKind
-           -- ignore the evidence. arg2_sigma must have type * or #,
-           -- because we know arg2_sigma -> or_res_ty is well-kinded
+           -- Ignore the evidence. arg2_sigma must have type * or #,
+           -- because we know (arg2_sigma -> op_res_ty) is well-kinded
            -- (because otherwise matchActualFunTys would fail)
-           -- There's no possibility here of, say, a kind family reducing to *.
+           -- So this 'unifyKind' will either succeed with Refl, or will
+           -- produce an insoluble constraint * ~ #, which we'll report later.
 
-       ; wrap_res <- tcSubTypeHR orig1 (Just expr) op_res_ty res_ty
-                       -- op_res -> res
+       -- NB: unlike the argument type, the *result* type, op_res_ty can
+       -- have any kind (#8739), so we don't need to check anything for that
 
        ; op_id  <- tcLookupId op_name
-       ; res_ty <- readExpType res_ty
-       ; let op' = L loc (mkHsWrap (mkWpTyApps [ getRuntimeRep res_ty
+       ; let op' = L loc (mkHsWrap (mkWpTyApps [ getRuntimeRep op_res_ty
                                                , arg2_sigma
-                                               , res_ty])
+                                               , op_res_ty])
                                    (HsVar noExt (L lv op_id)))
              -- arg1' :: arg1_ty
              -- wrap_arg1 :: arg1_ty "->" (arg2_sigma -> op_res_ty)
-             -- wrap_res :: op_res_ty "->" res_ty
-             -- op' :: (a2_ty -> res_ty) -> a2_ty -> res_ty
+             -- op' :: (a2_ty -> op_res_ty) -> a2_ty -> op_res_ty
 
-             -- wrap1 :: arg1_ty "->" (arg2_sigma -> res_ty)
-             wrap1 = mkWpFun idHsWrapper wrap_res arg2_sigma res_ty doc
-                     <.> wrap_arg1
-             doc = text "When looking at the argument to ($)"
+             expr' = OpApp fix (mkLHsWrap wrap_arg1 arg1') op' arg2'
 
-       ; return (OpApp fix (mkLHsWrap wrap1 arg1') op' arg2') }
+       ; tcWrapResult expr expr' op_res_ty res_ty }
 
   | (L loc (HsRecFld _ (Ambiguous _ lbl))) <- op
   , Just sig_ty <- obviousSig (unLoc arg1)
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index f2a7950450..adc25f5ff8 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -36,7 +36,7 @@ module TcHsType (
         -- Kind-checking types
         -- No kind generalisation, no checkValidType
         kcLHsQTyVars,
-        tcWildCardBinders,
+        tcNamedWildCardBinders,
         tcHsLiftedType,   tcHsOpenType,
         tcHsLiftedTypeNC, tcHsOpenTypeNC,
         tcLHsType, tcLHsTypeUnsaturated, tcCheckLHsType,
@@ -387,7 +387,7 @@ tcHsTypeApp wc_ty kind
                unsetWOptM Opt_WarnPartialTypeSignatures $
                setXOptM LangExt.PartialTypeSignatures $
                -- See Note [Wildcards in visible type application]
-               tcWildCardBinders sig_wcs $ \ _ ->
+               tcNamedWildCardBinders sig_wcs $ \ _ ->
                tcCheckLHsType hs_ty kind
        -- We must promote here. Ex:
        --   f :: forall a. a
@@ -402,18 +402,19 @@ tcHsTypeApp (XHsWildCardBndrs _) _ = panic "tcHsTypeApp"
 
 {- Note [Wildcards in visible type application]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-A HsWildCardBndrs's hswc_ext now only includes named wildcards, so any unnamed
-wildcards stay unchanged in hswc_body and when called in tcHsTypeApp, tcCheckLHsType
-will call emitWildCardHoleConstraints on them. However, this would trigger
-error/warning when an unnamed wildcard is passed in as a visible type argument,
-which we do not want because users should be able to write @_ to skip a instantiating
-a type variable variable without fuss. The solution is to switch the
-PartialTypeSignatures flags here to let the typechecker know that it's checking
-a '@_' and do not emit hole constraints on it.
-See related Note [Wildcards in visible kind application]
-and Note [The wildcard story for types] in HsTypes.hs
-
+A HsWildCardBndrs's hswc_ext now only includes /named/ wildcards, so
+any unnamed wildcards stay unchanged in hswc_body.  When called in
+tcHsTypeApp, tcCheckLHsType will call emitAnonWildCardHoleConstraint
+on these anonymous wildcards. However, this would trigger
+error/warning when an anonymous wildcard is passed in as a visible type
+argument, which we do not want because users should be able to write
+@_ to skip a instantiating a type variable variable without fuss. The
+solution is to switch the PartialTypeSignatures flags here to let the
+typechecker know that it's checking a '@_' and do not emit hole
+constraints on it.  See related Note [Wildcards in visible kind
+application] and Note [The wildcard story for types] in HsTypes.hs
+
+Ugh!
 -}
 
 {-
@@ -829,7 +830,7 @@ tc_hs_type mode ty@(HsAppKindTy{})         ek = tc_infer_hs_type_ek mode ty ek
 tc_hs_type mode ty@(HsOpTy {})             ek = tc_infer_hs_type_ek mode ty ek
 tc_hs_type mode ty@(HsKindSig {})          ek = tc_infer_hs_type_ek mode ty ek
 tc_hs_type mode ty@(XHsType (NHsCoreTy{})) ek = tc_infer_hs_type_ek mode ty ek
-tc_hs_type _    wc@(HsWildCardTy _)        ek = tcWildCardOcc wc ek
+tc_hs_type _    wc@(HsWildCardTy _)        ek = tcAnonWildCardOcc wc ek
 
 ------------------------------------------
 tc_fun_type :: TcTyMode -> LHsType GhcRn -> LHsType GhcRn -> TcKind
@@ -849,18 +850,18 @@ tc_fun_type mode ty1 ty2 exp_kind = case mode_level mode of
                            liftedTypeKind exp_kind }
 
 ---------------------------
-tcWildCardOcc :: HsType GhcRn -> Kind -> TcM TcType
-tcWildCardOcc wc exp_kind
-  = do { wc_tv <- newWildTyVar
-          -- The wildcard's kind should be an un-filled-in meta tyvar
-       ; loc <- getSrcSpanM
-       ; uniq <- newUnique
-       ; let name = mkInternalName uniq (mkTyVarOcc "_") loc
+tcAnonWildCardOcc :: HsType GhcRn -> Kind -> TcM TcType
+tcAnonWildCardOcc wc exp_kind
+  = do { wc_tv <- newWildTyVar  -- The wildcard's kind will be an un-filled-in meta tyvar
+
        ; part_tysig <- xoptM LangExt.PartialTypeSignatures
        ; warning <- woptM Opt_WarnPartialTypeSignatures
-       -- See Note [Wildcards in visible kind application]
-       ; unless (part_tysig && not warning)
-             (emitWildCardHoleConstraints [(name,wc_tv)])
+
+       ; unless (part_tysig && not warning) $
+         emitAnonWildCardHoleConstraint wc_tv
+         -- Why the 'unless' guard?
+         -- See Note [Wildcards in visible kind application]
+
        ; checkExpectedKind wc (mkTyVarTy wc_tv)
                            (tyVarKind wc_tv) exp_kind }
 
@@ -877,11 +878,11 @@ x = MkT
 So we should allow '@_' without emitting any hole constraints, and
 regardless of whether PartialTypeSignatures is enabled or not. But how would
 the typechecker know which '_' is being used in VKA and which is not when it
-calls emitWildCardHoleConstraints in tcHsPartialSigType on all HsWildCardBndrs?
+calls emitNamedWildCardHoleConstraints in tcHsPartialSigType on all HsWildCardBndrs?
 The solution then is to neither rename nor include unnamed wildcards in HsWildCardBndrs,
-but instead give every unnamed wildcard a fresh wild tyvar in tcWildCardOcc.
+but instead give every anonymous wildcard a fresh wild tyvar in tcAnonWildCardOcc.
 And whenever we see a '@', we automatically turn on PartialTypeSignatures and
-turn off hole constraint warnings, and never call emitWildCardHoleConstraints
+turn off hole constraint warnings, and do not call emitAnonWildCardHoleConstraint
 under these conditions.
 See related Note [Wildcards in visible type application] here and
 Note [The wildcard story for types] in HsTypes.hs
@@ -1722,23 +1723,26 @@ To avoid the double-zonk, we do two things:
     gathers free variables. So this way effectively sidesteps step 3.
 -}
 
-tcWildCardBinders :: [Name]
-                  -> ([(Name, TcTyVar)] -> TcM a)
-                  -> TcM a
-tcWildCardBinders wc_names thing_inside
+tcNamedWildCardBinders :: [Name]
+                       -> ([(Name, TcTyVar)] -> TcM a)
+                       -> TcM a
+-- Bring into scope the /named/ wildcard binders.  Remember that
+-- plain wildcards _ are anonymous and dealt with by HsWildCardTy
+-- Soe Note [The wildcard story for types] in HsTypes
+tcNamedWildCardBinders wc_names thing_inside
   = do { wcs <- mapM (const newWildTyVar) wc_names
        ; let wc_prs = wc_names `zip` wcs
        ; tcExtendNameTyVarEnv wc_prs $
          thing_inside wc_prs }
 
 newWildTyVar :: TcM TcTyVar
--- ^ New unification variable for a wildcard
+-- ^ New unification variable '_' for a wildcard
 newWildTyVar
   = do { kind <- newMetaKindVar
        ; uniq <- newUnique
        ; details <- newMetaDetails TauTv
-       ; let name = mkSysTvName uniq (fsLit "_")
-             tyvar = (mkTcTyVar name kind details)
+       ; let name  = mkSysTvName uniq (fsLit "_")
+             tyvar = mkTcTyVar name kind details
        ; traceTc "newWildTyVar" (ppr tyvar)
        ; return tyvar }
 
@@ -2490,11 +2494,11 @@ tcHsPartialSigType
   -> LHsSigWcType GhcRn       -- The type signature
   -> TcM ( [(Name, TcTyVar)]  -- Wildcards
          , Maybe TcType       -- Extra-constraints wildcard
-         , [Name]             -- Original tyvar names, in correspondence with ...
-         , [TcTyVar]          -- ... Implicitly and explicitly bound type variables
+         , [(Name,TcTyVar)]   -- Original tyvar names, in correspondence with
+                              --   the implicitly and explicitly bound type variables
          , TcThetaType        -- Theta part
          , TcType )           -- Tau part
--- See Note [Recipe for checking a signature]
+-- See Note [Checking partial type signatures]
 tcHsPartialSigType ctxt sig_ty
   | HsWC { hswc_ext  = sig_wcs, hswc_body = ib_ty } <- sig_ty
   , HsIB { hsib_ext = implicit_hs_tvs
@@ -2502,8 +2506,11 @@ tcHsPartialSigType ctxt sig_ty
   , (explicit_hs_tvs, L _ hs_ctxt, hs_tau) <- splitLHsSigmaTy hs_ty
   = addSigCtxt ctxt hs_ty $
     do { (implicit_tvs, (explicit_tvs, (wcs, wcx, theta, tau)))
-            <- solveLocalEqualities "tcHsPatSigTypes"      $
-               tcWildCardBinders sig_wcs $ \ wcs ->
+            <- solveLocalEqualities "tcHsPartialSigType"    $
+                 -- This solveLocalEqualiltes fails fast if there are
+                 -- insoluble equalities. See TcSimplify
+                 -- Note [Fail fast if there are insoluble kind equalities]
+               tcNamedWildCardBinders sig_wcs $ \ wcs ->
                bindImplicitTKBndrs_Tv implicit_hs_tvs       $
                bindExplicitTKBndrs_Tv explicit_hs_tvs       $
                do {   -- Instantiate the type-class context; but if there
@@ -2514,38 +2521,23 @@ tcHsPartialSigType ctxt sig_ty
 
                   ; return (wcs, wcx, theta, tau) }
 
-         -- We must return these separately, because all the zonking below
-         -- might change the name of a TyVarTv. This, in turn, causes trouble
-         -- in partial type signatures that bind scoped type variables, as
-         -- we bring the wrong name into scope in the function body.
-         -- Test case: partial-sigs/should_compile/LocalDefinitionBug
-       ; let tv_names = implicit_hs_tvs ++ hsLTyVarNames explicit_hs_tvs
-
        -- Spit out the wildcards (including the extra-constraints one)
        -- as "hole" constraints, so that they'll be reported if necessary
        -- See Note [Extra-constraint holes in partial type signatures]
-       ; emitWildCardHoleConstraints wcs
+       ; emitNamedWildCardHoleConstraints wcs
 
-         -- The TyVarTvs created above will sometimes have too high a TcLevel
-         -- (note that they are generated *after* bumping the level in
-         -- the tc{Im,Ex}plicitTKBndrsSig functions. Bumping the level
-         -- is still important here, because the kinds of these variables
-         -- do indeed need to have the higher level, so they can unify
-         -- with other local type variables. But, now that we've type-checked
-         -- everything (and solved equalities in the tcImplicit call)
-         -- we need to promote the TyVarTvs so we don't violate the TcLevel
-         -- invariant
-       ; implicit_tvs <- zonkAndScopedSort implicit_tvs
-       ; explicit_tvs <- mapM zonkAndSkolemise explicit_tvs
-       ; theta        <- mapM zonkTcType theta
-       ; tau          <- zonkTcType tau
-
-       ; let all_tvs = implicit_tvs ++ explicit_tvs
+         -- 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
+       ; let tv_prs = (implicit_hs_tvs                  `zip` implicit_tvs)
+                      ++ (hsLTyVarNames explicit_hs_tvs `zip` explicit_tvs)
 
-       ; checkValidType ctxt (mkSpecForAllTys all_tvs $ mkPhiTy theta tau)
+      -- 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
 
-       ; traceTc "tcHsPartialSigType" (ppr all_tvs)
-       ; return (wcs, wcx, tv_names, all_tvs, theta, tau) }
+       ; traceTc "tcHsPartialSigType" (ppr tv_prs)
+       ; return (wcs, wcx, tv_prs, theta, tau) }
 
 tcHsPartialSigType _ (HsWC _ (XHsImplicitBndrs _)) = panic "tcHsPartialSigType"
 tcHsPartialSigType _ (XHsWildCardBndrs _) = panic "tcHsPartialSigType"
@@ -2555,14 +2547,43 @@ tcPartialContext hs_theta
   | Just (hs_theta1, hs_ctxt_last) <- snocView hs_theta
   , L wc_loc wc@(HsWildCardTy _) <- ignoreParens hs_ctxt_last
   = do { wc_tv_ty <- setSrcSpan wc_loc $
-                     tcWildCardOcc wc constraintKind
+                     tcAnonWildCardOcc wc constraintKind
        ; theta <- mapM tcLHsPredType hs_theta1
        ; return (theta, Just wc_tv_ty) }
   | otherwise
   = do { theta <- mapM tcLHsPredType hs_theta
        ; return (theta, Nothing) }
 
-{- Note [Extra-constraint holes in partial type signatures]
+{- Note [Checking partial type signatures]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+See also Note [Recipe for checking a signature]
+
+When we have a parital signature like
+   f,g :: forall a. a -> _
+we do the following
+
+* In TcSigs.tcUserSigType we return a PartialSig, which (unlike
+  the companion CompleteSig) contains the original, as-yet-unchecked
+  source-code LHsSigWcType
+
+* Then, for f and g /separately/, we call tcInstSig, which in turn
+  call tchsPartialSig (defined near this Note).  It kind-checks the
+  LHsSigWcType, creating fresh unification variables for each "_"
+  wildcard.  It's important that the wildcards for f and g are distinct
+  becase they migh get instantiated completely differently.  E.g.
+     f,g :: forall a. a -> _
+     f x = a
+     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.
+
+Note [Extra-constraint holes in partial type signatures]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider
   f :: (_) => a -> a
@@ -2631,12 +2652,12 @@ tcHsPatSigType ctxt sig_ty
                  -- Always solve local equalities if possible,
                  -- else casts get in the way of deep skolemisation
                  -- (#16033)
-               tcWildCardBinders sig_wcs        $ \ wcs ->
+               tcNamedWildCardBinders sig_wcs        $ \ wcs ->
                tcExtendNameTyVarEnv sig_tkv_prs $
                do { sig_ty <- tcHsOpenType hs_ty
                   ; return (wcs, sig_ty) }
 
-        ; emitWildCardHoleConstraints wcs
+        ; emitNamedWildCardHoleConstraints wcs
 
           -- sig_ty might have tyvars that are at a higher TcLevel (if hs_ty
           -- contains a forall). Promote these.
diff --git a/compiler/typecheck/TcRnDriver.hs b/compiler/typecheck/TcRnDriver.hs
index d13abf4e03..3ffc5df61e 100644
--- a/compiler/typecheck/TcRnDriver.hs
+++ b/compiler/typecheck/TcRnDriver.hs
@@ -2438,8 +2438,8 @@ tcRnType hsc_env flexi normalise rdr_type
                         -- must push level to satisfy level precondition of
                         -- kindGeneralize, below
                        solveEqualities       $
-                       tcWildCardBinders wcs $ \ wcs' ->
-                       do { emitWildCardHoleConstraints wcs'
+                       tcNamedWildCardBinders wcs $ \ wcs' ->
+                       do { emitNamedWildCardHoleConstraints wcs'
                           ; tcLHsTypeUnsaturated rn_type }
 
        -- Do kind generalisation; see Note [Kind-generalise in tcRnType]
diff --git a/compiler/typecheck/TcRnMonad.hs b/compiler/typecheck/TcRnMonad.hs
index 25cf04f153..9a76e9ced8 100644
--- a/compiler/typecheck/TcRnMonad.hs
+++ b/compiler/typecheck/TcRnMonad.hs
@@ -103,7 +103,8 @@ module TcRnMonad(
   pushTcLevelM_, pushTcLevelM, pushTcLevelsM,
   getTcLevel, setTcLevel, isTouchableTcM,
   getLclTypeEnv, setLclTypeEnv,
-  traceTcConstraints, emitWildCardHoleConstraints,
+  traceTcConstraints,
+  emitNamedWildCardHoleConstraints, emitAnonWildCardHoleConstraint,
 
   -- * Template Haskell context
   recordThUse, recordThSpliceUse, recordTopLevelSpliceLoc,
@@ -1676,8 +1677,16 @@ traceTcConstraints msg
          hang (text (msg ++ ": LIE:")) 2 (ppr lie)
        }
 
-emitWildCardHoleConstraints :: [(Name, TcTyVar)] -> TcM ()
-emitWildCardHoleConstraints wcs
+emitAnonWildCardHoleConstraint :: TcTyVar -> TcM ()
+emitAnonWildCardHoleConstraint tv
+  = do { ct_loc <- getCtLocM HoleOrigin Nothing
+       ; emitInsolubles $ unitBag $
+         CHoleCan { cc_ev = CtDerived { ctev_pred = mkTyVarTy tv
+                                      , ctev_loc  = ct_loc }
+                  , cc_hole = TypeHole (mkTyVarOcc "_") } }
+
+emitNamedWildCardHoleConstraints :: [(Name, TcTyVar)] -> TcM ()
+emitNamedWildCardHoleConstraints wcs
   = do { ct_loc <- getCtLocM HoleOrigin Nothing
        ; emitInsolubles $ listToBag $
          map (do_one ct_loc) wcs }
@@ -1690,7 +1699,7 @@ emitWildCardHoleConstraints wcs
        where
          real_span = case nameSrcSpan name of
                            RealSrcSpan span  -> span
-                           UnhelpfulSpan str -> pprPanic "emitWildCardHoleConstraints"
+                           UnhelpfulSpan str -> pprPanic "emitNamedWildCardHoleConstraints"
                                                       (ppr name <+> quotes (ftext str))
                -- Wildcards are defined locally, and so have RealSrcSpans
          ct_loc' = setCtLocSpan ct_loc real_span
diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index 221d9cea8c..3c6b8ca685 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ -1561,7 +1561,7 @@ data TcIdSigInst
                -- Extra-constraints wildcard to fill in, if any
                -- If this exists, it is surely of the form (meta_tv |> co)
                -- (where the co might be reflexive). This is filled in
-               -- only from the return value of TcHsType.tcWildCardOcc
+               -- only from the return value of TcHsType.tcAnonWildCardOcc
          }
 
 {- Note [sig_inst_tau may be polymorphic]
diff --git a/compiler/typecheck/TcSigs.hs b/compiler/typecheck/TcSigs.hs
index 5bcb0eee9c..da18065b93 100644
--- a/compiler/typecheck/TcSigs.hs
+++ b/compiler/typecheck/TcSigs.hs
@@ -498,25 +498,14 @@ tcInstSig hs_sig@(PartialSig { psig_hs_ty = hs_ty
                              , sig_loc = loc })
   = setSrcSpan loc $  -- Set the binding site of the tyvars
     do { traceTc "Staring partial sig {" (ppr hs_sig)
-       ; (wcs, wcx, tv_names, tvs, theta, tau) <- tcHsPartialSigType ctxt hs_ty
-
-        -- Clone the quantified tyvars
-        -- Reason: we might have    f, g :: forall a. a -> _ -> a
-        --         and we want it to behave exactly as if there were
-        --         two separate signatures.  Cloning here seems like
-        --         the easiest way to do so, and is very similar to
-        --         the tcInstType in the CompleteSig case
-        -- See #14643
-       ; (subst, tvs') <- newMetaTyVarTyVars tvs
-                         -- Why newMetaTyVarTyVars?  See TcBinds
-                         -- Note [Quantified variables in partial type signatures]
-       ; let tv_prs = tv_names `zip` tvs'
-             inst_sig = TISI { sig_inst_sig   = hs_sig
+       ; (wcs, wcx, tv_prs, theta, tau) <- tcHsPartialSigType ctxt hs_ty
+         -- See Note [Checking partial type signatures] in TcHsType
+       ; let inst_sig = TISI { sig_inst_sig   = hs_sig
                              , sig_inst_skols = tv_prs
                              , sig_inst_wcs   = wcs
                              , sig_inst_wcx   = wcx
-                             , sig_inst_theta = substTysUnchecked subst theta
-                             , sig_inst_tau   = substTyUnchecked  subst tau }
+                             , sig_inst_theta = theta
+                             , sig_inst_tau   = tau }
        ; traceTc "End partial sig }" (ppr inst_sig)
        ; return inst_sig }
 
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index 55427d509a..55cb501139 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -1795,11 +1795,14 @@ hasTyVarHead ty                 -- Haskell 98 allows predicates of form
        Nothing      -> False
 
 evVarPred :: EvVar -> PredType
-evVarPred var
-  = ASSERT2( isEvVarType var_ty, ppr var <+> dcolon <+> ppr var_ty )
-    var_ty
- where
-    var_ty = varType var
+evVarPred var = varType var
+  -- Historical note: I used to have an ASSERT here,
+  -- checking (isEvVarType (varType var)).  But with something like
+  --   f :: c => _ -> _
+  -- we end up with (c :: kappa), and (kappa ~ Constraint).  Until
+  -- we solve and zonk (which there is no particular reason to do for
+  -- partial signatures, (isEvVarType kappa) will return False. But
+  -- nothing is wrong.  So I just removed the ASSERT.
 
 ------------------
 -- | When inferring types, should we quantify over a given predicate?
diff --git a/testsuite/tests/partial-sigs/should_compile/T16728.hs b/testsuite/tests/partial-sigs/should_compile/T16728.hs
new file mode 100644
index 0000000000..f54f17ef56
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_compile/T16728.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE PartialTypeSignatures #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+module Bug where
+
+import Data.Proxy
+
+f :: forall k (x :: k). Proxy (x :: _)
+f = Proxy
diff --git a/testsuite/tests/partial-sigs/should_compile/T16728.stderr b/testsuite/tests/partial-sigs/should_compile/T16728.stderr
new file mode 100644
index 0000000000..6efdae343e
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_compile/T16728.stderr
@@ -0,0 +1,9 @@
+
+T16728.hs:8:37: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’ standing for ‘k’
+      Where: ‘k’ is a rigid type variable bound by
+               the inferred type of f :: Proxy x
+               at T16728.hs:9:1-9
+    • In the kind ‘_’
+      In the first argument of ‘Proxy’, namely ‘(x :: _)’
+      In the type ‘Proxy (x :: _)’
diff --git a/testsuite/tests/partial-sigs/should_compile/T16728a.hs b/testsuite/tests/partial-sigs/should_compile/T16728a.hs
new file mode 100644
index 0000000000..96d693a192
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_compile/T16728a.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE ExplicitForAll, PartialTypeSignatures #-}
+module Bug where
+
+g,h:: forall a. a -> _
+g x = h x
+
+h x = g x
+
diff --git a/testsuite/tests/partial-sigs/should_compile/T16728a.stderr b/testsuite/tests/partial-sigs/should_compile/T16728a.stderr
new file mode 100644
index 0000000000..50785ebc1c
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_compile/T16728a.stderr
@@ -0,0 +1,20 @@
+
+T16728a.hs:4:22: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’ standing for ‘_’
+      Where: ‘_’ is a rigid type variable bound by
+               the inferred types of
+                 g :: a -> _
+                 h :: a -> _
+               at T16728a.hs:(5,1)-(7,9)
+    • In the type ‘a -> _’
+      In the type signature: g :: forall a. a -> _
+
+T16728a.hs:4:22: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’ standing for ‘_’
+      Where: ‘_’ is a rigid type variable bound by
+               the inferred types of
+                 g :: a -> _
+                 h :: a -> _
+               at T16728a.hs:(5,1)-(7,9)
+    • In the type ‘a -> _’
+      In the type signature: h :: forall a. a -> _
diff --git a/testsuite/tests/partial-sigs/should_compile/T16728b.hs b/testsuite/tests/partial-sigs/should_compile/T16728b.hs
new file mode 100644
index 0000000000..db1e564a14
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_compile/T16728b.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE ExplicitForAll, PartialTypeSignatures #-}
+module Bug where
+
+g,h:: forall a. a -> _
+
+g x = x       -- Instantiates the wildcard to 'a'
+
+h x = True    -- Instantiates the wildcard to Bool
+
diff --git a/testsuite/tests/partial-sigs/should_compile/T16728b.stderr b/testsuite/tests/partial-sigs/should_compile/T16728b.stderr
new file mode 100644
index 0000000000..712acfe0b9
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_compile/T16728b.stderr
@@ -0,0 +1,13 @@
+
+T16728b.hs:4:22: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’ standing for ‘Bool’
+    • In the type ‘a -> _’
+      In the type signature: h :: forall a. a -> _
+
+T16728b.hs:4:22: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’ standing for ‘a’
+      Where: ‘a’ is a rigid type variable bound by
+               the inferred type of g :: a -> a
+               at T16728b.hs:6:1-7
+    • In the type ‘a -> _’
+      In the type signature: g :: forall a. a -> _
diff --git a/testsuite/tests/partial-sigs/should_compile/all.T b/testsuite/tests/partial-sigs/should_compile/all.T
index 56d821eca0..4cb12ed144 100644
--- a/testsuite/tests/partial-sigs/should_compile/all.T
+++ b/testsuite/tests/partial-sigs/should_compile/all.T
@@ -92,3 +92,6 @@ test('T15039c', normal, compile, ['-fprint-equality-relations'])
 test('T15039d', normal, compile,
                 ['-fprint-explicit-kinds -fprint-equality-relations'])
 test('T16334', normal, compile, [''])
+test('T16728', normal, compile, [''])
+test('T16728a', normal, compile, [''])
+test('T16728b', normal, compile, [''])
diff --git a/testsuite/tests/partial-sigs/should_fail/T14040a.stderr b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr
index 0a07f0590d..24782235ba 100644
--- a/testsuite/tests/partial-sigs/should_fail/T14040a.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr
@@ -1,10 +1,10 @@
 
 T14040a.hs:34:8: error:
-    • Cannot apply expression of type ‘Sing wl0
-                                       -> (forall y. p0 _0 'WeirdNil)
+    • Cannot apply expression of type ‘Sing wl
+                                       -> (forall y. p _2 'WeirdNil)
                                        -> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)).
-                                           Sing x -> Sing xs -> p0 _1 xs -> p0 _2 ('WeirdCons x xs))
-                                       -> p0 _3 wl0’
+                                           Sing x -> Sing xs -> p _0 xs -> p _1 ('WeirdCons x xs))
+                                       -> p _2 wl’
       to a visible type argument ‘(WeirdList z)’
     • In the sixth argument of ‘pWeirdCons’, namely
         ‘(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)’