Fix two more bugs in partial signatures

These were shown up by Trac #14643

Bug 1: if we had a single partial signature for
two functions
   f, g :: forall a. _ -> a
then we made two different SigTvs but with the sane Name.
This was jolly confusing and ultimately led to deeply bogus
results with Any's appearing in the resulting program. Yikes.
Fix: clone the quantified variables in TcSigs.tcInstSig (as
indeed its name suggests).

Bug 2: we were not eliminating duplicate/superclass constraints
in the partial signatures of a mutually recursive group.

Easy to fix: we are already doing dup/superclass elim in
TcSimplify.decideQuantification.  So we move the partial-sig
constraints there too.

11 files changed, 113 insertions, 45 deletions

diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index 52183a8a4a..08dc56d18c 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -1668,6 +1668,7 @@ tcExplicitTKBndrsX :: (Name -> Kind -> TcM TyVar)
                         -- ^ Thing inside returns the set of variables bound
                         -- in the scope. See Note [Scope-check inferred kinds]
                    -> TcM (a, TyVarSet)  -- ^ returns augmented bound vars
+-- See also Note [Associated type tyvar names] in Class
 tcExplicitTKBndrsX new_tv orig_hs_tvs thing_inside
   = go orig_hs_tvs $ \ tvs ->
     do { (result, bound_tvs) <- thing_inside tvs
@@ -2095,9 +2096,7 @@ tcHsPartialSigType ctxt sig_ty
     do { (implicit_tvs, (wcs, wcx, explicit_tvs, theta, tau))
             <- tcWildCardBindersX newWildTyVar sig_wcs        $ \ wcs ->
                tcImplicitTKBndrsX new_implicit_tv implicit_hs_tvs $
-               tcExplicitTKBndrsX newSigTyVar explicit_hs_tvs $ \ explicit_tvs ->
-                  -- Why newSigTyVar?  See TcBinds
-                  -- Note [Quantified variables in partial type signatures]
+               tcExplicitTKBndrs explicit_hs_tvs $ \ explicit_tvs ->
              do {   -- Instantiate the type-class context; but if there
                     -- is an extra-constraints wildcard, just discard it here
                     (theta, wcx) <- tcPartialContext hs_ctxt
@@ -2122,6 +2121,7 @@ tcHsPartialSigType ctxt sig_ty
 
         ; theta   <- mapM zonkTcType theta
         ; tau     <- zonkTcType tau
+
         ; checkValidType ctxt (mkSpecForAllTys all_tvs $ mkPhiTy theta tau)
 
         ; traceTc "tcHsPartialSigType" (ppr all_tvs)
@@ -2129,9 +2129,7 @@ tcHsPartialSigType ctxt sig_ty
   where
     new_implicit_tv name
       = do { kind <- newMetaKindVar
-           ; tv <- newSigTyVar name kind
-             -- Why newSigTyVar?  See TcBinds
-             -- Note [Quantified variables in partial type signatures]
+           ; tv <- newSkolemTyVar name kind
            ; return (tv, False) }
 
 tcPartialContext :: HsContext GhcRn -> TcM (TcThetaType, Maybe TcTyVar)
diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs
index 58b220b839..79e337d905 100644
--- a/compiler/typecheck/TcMType.hs
+++ b/compiler/typecheck/TcMType.hs
@@ -509,10 +509,11 @@ tcInstSkolTyVars' overlappable subst tvs
        ; lvl <- getTcLevel
        ; instSkolTyCoVarsX (mkTcSkolTyVar lvl loc overlappable) subst tvs }
 
-mkTcSkolTyVar :: TcLevel -> SrcSpan -> Bool -> TcTyVarMaker
-mkTcSkolTyVar lvl loc overlappable
-  = \ uniq old_name kind -> mkTcTyVar (mkInternalName uniq (getOccName old_name) loc)
-                                      kind details
+mkTcSkolTyVar :: TcLevel -> SrcSpan -> Bool -> TcTyCoVarMaker gbl lcl
+mkTcSkolTyVar lvl loc overlappable old_name kind
+  = do { uniq <- newUnique
+       ; let name = mkInternalName uniq (getOccName old_name) loc
+       ; return (mkTcTyVar name kind details) }
   where
     details = SkolemTv (pushTcLevel lvl) overlappable
               -- NB: skolems bump the level
@@ -524,31 +525,36 @@ freshenTyVarBndrs :: [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyVar])
 -- Used in FamInst.newFamInst, and Inst.newClsInst
 freshenTyVarBndrs = instSkolTyCoVars mk_tv
   where
-    mk_tv uniq old_name kind = mkTyVar (setNameUnique old_name uniq) kind
+    mk_tv old_name kind
+       = do { uniq <- newUnique
+            ; return (mkTyVar (setNameUnique old_name uniq) kind) }
 
 freshenCoVarBndrsX :: TCvSubst -> [CoVar] -> TcRnIf gbl lcl (TCvSubst, [CoVar])
 -- ^ Give fresh uniques to a bunch of CoVars
 -- Used in FamInst.newFamInst
 freshenCoVarBndrsX subst = instSkolTyCoVarsX mk_cv subst
   where
-    mk_cv uniq old_name kind = mkCoVar (setNameUnique old_name uniq) kind
+    mk_cv old_name kind
+      = do { uniq <- newUnique
+           ; return (mkCoVar (setNameUnique old_name uniq) kind) }
 
 ------------------
-type TcTyVarMaker = Unique -> Name -> Kind -> TyCoVar
-instSkolTyCoVars :: TcTyVarMaker -> [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyCoVar])
+type TcTyCoVarMaker gbl lcl = Name -> Kind -> TcRnIf gbl lcl TyCoVar
+     -- The TcTyCoVarMaker should make a fresh Name, based on the old one
+     -- Freshness is critical. See Note [Skolems in zonkSyntaxExpr] in TcHsSyn
+
+instSkolTyCoVars :: TcTyCoVarMaker gbl lcl -> [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyCoVar])
 instSkolTyCoVars mk_tcv = instSkolTyCoVarsX mk_tcv emptyTCvSubst
 
-instSkolTyCoVarsX :: TcTyVarMaker
+instSkolTyCoVarsX :: TcTyCoVarMaker gbl lcl
                   -> TCvSubst -> [TyCoVar] -> TcRnIf gbl lcl (TCvSubst, [TyCoVar])
 instSkolTyCoVarsX mk_tcv = mapAccumLM (instSkolTyCoVarX mk_tcv)
 
-instSkolTyCoVarX :: TcTyVarMaker
+instSkolTyCoVarX :: TcTyCoVarMaker gbl lcl
                  -> TCvSubst -> TyCoVar -> TcRnIf gbl lcl (TCvSubst, TyCoVar)
 instSkolTyCoVarX mk_tcv subst tycovar
-  = do  { uniq <- newUnique  -- using a new unique is critical. See
-                             -- Note [Skolems in zonkSyntaxExpr] in TcHsSyn
-        ; let new_tcv = mk_tcv uniq old_name kind
-              subst1 | isTyVar new_tcv
+  = do  { new_tcv <- mk_tcv old_name kind
+        ; let subst1 | isTyVar new_tcv
                      = extendTvSubstWithClone subst tycovar new_tcv
                      | otherwise
                      = extendCvSubstWithClone subst tycovar new_tcv
diff --git a/compiler/typecheck/TcSigs.hs b/compiler/typecheck/TcSigs.hs
index 5d95503b07..62fa83287c 100644
--- a/compiler/typecheck/TcSigs.hs
+++ b/compiler/typecheck/TcSigs.hs
@@ -405,12 +405,30 @@ tcInstSig sig@(PartialSig { psig_hs_ty = hs_ty
                           , sig_loc = loc })
   = setSrcSpan loc $  -- Set the binding site of the tyvars
     do { (wcs, wcx, 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 Trac #14643
+        ; (subst, tvs') <- instSkolTyCoVars mk_sig_tv tvs
+        ; let tv_prs = map tyVarName tvs `zip` tvs'
+
        ; return (TISI { sig_inst_sig   = sig
-                      , sig_inst_skols = map (\tv -> (tyVarName tv, tv)) tvs
+                      , sig_inst_skols = tv_prs
                       , sig_inst_wcs   = wcs
                       , sig_inst_wcx   = wcx
-                      , sig_inst_theta = theta
-                      , sig_inst_tau   = tau }) }
+                      , sig_inst_theta = substTys subst theta
+                      , sig_inst_tau   = substTy  subst tau
+                }) }
+  where
+    mk_sig_tv old_name kind
+      = do { uniq <- newUnique
+           ; newSigTyVar (setNameUnique old_name uniq) kind }
+      -- Why newSigTyVar?  See TcBinds
+      -- Note [Quantified variables in partial type signatures]
 
 
 {- Note [Pattern bindings and complete signatures]
diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs
index 76765f7396..0048c090a0 100644
--- a/compiler/typecheck/TcSimplify.hs
+++ b/compiler/typecheck/TcSimplify.hs
@@ -662,32 +662,39 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
        -- Decide what type variables and constraints to quantify
        -- NB: quant_pred_candidates is already fully zonked
        -- NB: bound_theta are constraints we want to quantify over,
-       --     /apart from/ the psig_theta, which we always quantify over
+       --     including the psig_theta, which we always quantify over
+       -- NB: bound_theta are fully zonked
        ; (qtvs, bound_theta, co_vars) <- decideQuantification infer_mode rhs_tclvl
                                                      name_taus partial_sigs
                                                      quant_pred_candidates
-
-        -- We must retain the psig_theta_vars, because we've used them in
-        -- evidence bindings constructed by solveWanteds earlier
-       ; psig_theta_vars  <- mapM zonkId       psig_theta_vars
        ; bound_theta_vars <- mapM TcM.newEvVar bound_theta
-       ; let full_theta_vars = psig_theta_vars ++ bound_theta_vars
 
+       -- We must produce bindings for the psig_theta_vars, because we may have
+       -- used them in evidence bindings constructed by solveWanteds earlier
+       -- Easiest way to do this is to emit them as new Wanteds (Trac #14643)
+       ; ct_loc <- getCtLocM AnnOrigin Nothing
+       ; let psig_wanted = [ CtWanted { ctev_pred = idType psig_theta_var
+                                      , ctev_dest = EvVarDest psig_theta_var
+                                      , ctev_nosh = WDeriv
+                                      , ctev_loc  = ct_loc }
+                           | psig_theta_var <- psig_theta_vars ]
+
+       -- Now we can emil the residual constraints
        ; emitResidualConstraints rhs_tclvl tc_lcl_env ev_binds_var
                                  name_taus co_vars qtvs
-                                 full_theta_vars wanted_transformed
+                                 bound_theta_vars
+                                 (wanted_transformed `andWC` mkSimpleWC psig_wanted)
 
          -- All done!
        ; traceTc "} simplifyInfer/produced residual implication for quantification" $
          vcat [ text "quant_pred_candidates =" <+> ppr quant_pred_candidates
               , text "psig_theta =" <+> ppr psig_theta
               , text "bound_theta =" <+> ppr bound_theta
-              , text "full_theta =" <+> ppr (map idType full_theta_vars)
               , text "qtvs ="       <+> ppr qtvs
               , text "definite_error =" <+> ppr definite_error ]
 
-       ; return ( qtvs, full_theta_vars, TcEvBinds ev_binds_var, definite_error ) }
-         -- NB: full_theta_vars must be fully zonked
+       ; return ( qtvs, bound_theta_vars, TcEvBinds ev_binds_var, definite_error ) }
+         -- NB: bound_theta_vars must be fully zonked
 
 
 --------------------
@@ -871,18 +878,20 @@ decideQuantification infer_mode rhs_tclvl name_taus psigs candidates
        --         predicates to actually quantify over
        -- NB: decideQuantifiedTyVars turned some meta tyvars
        -- into quantified skolems, so we have to zonk again
-       ; candidates <- TcM.zonkTcTypes candidates
+       ; let psig_theta = concatMap sig_inst_theta psigs
+       ; all_candidates <- TcM.zonkTcTypes (psig_theta ++ candidates)
        ; let theta = pickQuantifiablePreds (mkVarSet qtvs) $
                      mkMinimalBySCs id $  -- See Note [Minimize by Superclasses]
-                     candidates
+                     all_candidates
 
        ; traceTc "decideQuantification"
-           (vcat [ text "infer_mode:"   <+> ppr infer_mode
-                 , text "candidates:"   <+> ppr candidates
-                 , text "mono_tvs:"     <+> ppr mono_tvs
-                 , text "co_vars:"      <+> ppr co_vars
-                 , text "qtvs:"         <+> ppr qtvs
-                 , text "theta:"        <+> ppr theta ])
+           (vcat [ text "infer_mode:"      <+> ppr infer_mode
+                 , text "candidates:"      <+> ppr candidates
+                 , text "all_candidates:"  <+> ppr all_candidates
+                 , text "mono_tvs:"        <+> ppr mono_tvs
+                 , text "co_vars:"         <+> ppr co_vars
+                 , text "qtvs:"            <+> ppr qtvs
+                 , text "theta:"           <+> ppr theta ])
        ; return (qtvs, theta, co_vars) }
 
 ------------------
diff --git a/testsuite/tests/partial-sigs/should_compile/T14643.hs b/testsuite/tests/partial-sigs/should_compile/T14643.hs
new file mode 100644
index 0000000000..b6de27db65
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_compile/T14643.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE PartialTypeSignatures #-}
+
+module T14653 where
+
+af, ag :: (Num a,_) => a -> a
+-- It's important that one signature covers both
+
+af y = ag y
+ag x = af (x-1)
diff --git a/testsuite/tests/partial-sigs/should_compile/T14643.stderr b/testsuite/tests/partial-sigs/should_compile/T14643.stderr
new file mode 100644
index 0000000000..c5f204e799
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_compile/T14643.stderr
@@ -0,0 +1,8 @@
+
+T14643.hs:5:18: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’ standing for ‘()’
+    • In the type signature: af :: (Num a, _) => a -> a
+
+T14643.hs:5:18: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’ standing for ‘()’
+    • In the type signature: ag :: (Num a, _) => a -> a
diff --git a/testsuite/tests/partial-sigs/should_compile/T14643a.hs b/testsuite/tests/partial-sigs/should_compile/T14643a.hs
new file mode 100644
index 0000000000..47ef519e37
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_compile/T14643a.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE PartialTypeSignatures #-}
+
+module T14653a where
+
+af :: (Num a,_) => a -> a
+af y = ag y
+
+ag :: (Num a,_) => a -> a
+ag x = af (x-1)
diff --git a/testsuite/tests/partial-sigs/should_compile/T14643a.stderr b/testsuite/tests/partial-sigs/should_compile/T14643a.stderr
new file mode 100644
index 0000000000..1514ac92ed
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_compile/T14643a.stderr
@@ -0,0 +1,8 @@
+
+T14643a.hs:5:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’ standing for ‘()’
+    • In the type signature: af :: (Num a, _) => a -> a
+
+T14643a.hs:8:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’ standing for ‘()’
+    • In the type signature: ag :: (Num a, _) => a -> a
diff --git a/testsuite/tests/partial-sigs/should_compile/all.T b/testsuite/tests/partial-sigs/should_compile/all.T
index 0f4e425c8e..d13af5ca17 100644
--- a/testsuite/tests/partial-sigs/should_compile/all.T
+++ b/testsuite/tests/partial-sigs/should_compile/all.T
@@ -38,7 +38,7 @@ test('PatBind', normal, compile, ['-ddump-types -fno-warn-partial-type-signature
 # Bug
 test('PatBind2', normal, compile, ['-ddump-types -fno-warn-partial-type-signatures'])
 test('PatternSig', normal, compile, ['-ddump-types -fno-warn-partial-type-signatures'])
-test('PatternSplice', normal, compile, ['-fno-warn-partial-type-signatures'])
+test('PatternSplice', [req_interp, normal], compile, ['-fno-warn-partial-type-signatures'])
 test('Recursive', normal, compile, ['-ddump-types -fno-warn-partial-type-signatures'])
 test('ScopedNamedWildcards', normal, compile, ['-ddump-types -fno-warn-partial-type-signatures'])
 test('ScopedNamedWildcardsGood', normal, compile, ['-ddump-types -fno-warn-partial-type-signatures'])
@@ -53,7 +53,7 @@ test('WarningWildcardInstantiations', normal, compile, ['-ddump-types'])
 test('SplicesUsed', [extra_files(['Splices.hs']),
                      req_interp, omit_ways(prof_ways)], multimod_compile,
      ['SplicesUsed', config.ghc_th_way_flags])
-test('TypedSplice', [req_interp, normal], compile, [''])
+test('TypedSplice', normal, compile, [''])
 test('T10403', normal, compile, [''])
 test('T10438', normal, compile, [''])
 test('T10519', normal, compile, [''])
@@ -71,3 +71,6 @@ test('T12845', normal, compile, [''])
 test('T12844', normal, compile, [''])
 test('T13482', normal, compile, [''])
 test('T14217', normal, compile_fail, [''])
+test('T14643', normal, compile, [''])
+test('T14643a', normal, compile, [''])
+
diff --git a/testsuite/tests/partial-sigs/should_fail/T14040a.stderr b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr
index b4f0e26822..ac9ad8a1bd 100644
--- a/testsuite/tests/partial-sigs/should_fail/T14040a.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr
@@ -21,7 +21,7 @@ T14040a.hs:34:8: error:
                                            -> Sing xs
                                            -> p (WeirdList z1) w1 xs
                                            -> p z1 w2 ('WeirdCons x xs))
-                                       -> p a w3 wl’
+                                       -> p a1 w3 wl’
       to a visible type argument ‘(WeirdList z)’
     • In the sixth argument of ‘pWeirdCons’, namely
         ‘(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)’
diff --git a/testsuite/tests/partial-sigs/should_fail/all.T b/testsuite/tests/partial-sigs/should_fail/all.T
index b974ce8950..0f7496d1f5 100644
--- a/testsuite/tests/partial-sigs/should_fail/all.T
+++ b/testsuite/tests/partial-sigs/should_fail/all.T
@@ -3,7 +3,7 @@ test('AnnotatedConstraintNotForgotten', normal, compile_fail, [''])
 test('Defaulting1MROff', normal, compile, [''])
 test('ExtraConstraintsWildcardInExpressionSignature', normal, compile, [''])
 test('ExtraConstraintsWildcardInPatternSignature', normal, compile_fail, [''])
-test('ExtraConstraintsWildcardInPatternSplice', normal, compile_fail, [''])
+test('ExtraConstraintsWildcardInPatternSplice', [req_interp, normal], compile_fail, [''])
 test('ExtraConstraintsWildcardInTypeSpliceUsed', [extra_files(['ExtraConstraintsWildcardInTypeSplice.hs']),
                                                   req_interp],
      multimod_compile_fail,