Check for bogus quantified tyvars in partial type sigs

This fixes Trac #14479.  Not difficult.

See Note [Quantification and partial signatures] Wrinkle 4,
in TcSimplify.

5 files changed, 96 insertions, 47 deletions

diff --git a/compiler/typecheck/TcBinds.hs b/compiler/typecheck/TcBinds.hs
index 6189ba51d2..0c5179c473 100644
--- a/compiler/typecheck/TcBinds.hs
+++ b/compiler/typecheck/TcBinds.hs
@@ -939,32 +939,35 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs
                                       , sig_inst_theta = annotated_theta
                                       , sig_inst_skols = annotated_tvs }))
   = -- Choose quantifiers for a partial type signature
-    do { psig_qtvs            <- mk_psig_qtvs annotated_tvs
-       ; annotated_theta      <- zonkTcTypes annotated_theta
-       ; (free_tvs, my_theta) <- choose_psig_context psig_qtvs annotated_theta wcx
-       ; return (mk_final_qtvs psig_qtvs free_tvs, my_theta) }
-  where
-    mk_final_qtvs psig_qtvs free_tvs
-      = [ mkTyVarBinder vis tv
-        | tv <- qtvs -- Pulling from qtvs maintains original order
-        , tv `elemVarSet` keep_me
-        , let vis | tv `elemVarSet` psig_qtvs = Specified
-                  | otherwise                 = Inferred ]
-      where
-        keep_me = free_tvs `unionVarSet` psig_qtvs
-
-    mk_psig_qtvs :: [(Name,TcTyVar)] -> TcM TcTyVarSet
-    mk_psig_qtvs annotated_tvs
-       = do { annotated_tvs <- zonkSigTyVarPairs annotated_tvs
+    do { psig_qtv_prs <- zonkSigTyVarPairs annotated_tvs
 
-            -- Report an error if the quantified variables of the
+            -- Check whether the quantified variables of the
             -- partial signature have been unified together
             -- See Note [Quantified variables in partial type signatures]
-            ; mapM_ report_sig_tv_err (findDupSigTvs annotated_tvs)
+       ; mapM_ report_dup_sig_tv_err  (findDupSigTvs psig_qtv_prs)
 
-            ; return (mkVarSet (map snd annotated_tvs)) }
+            -- Check whether a quantified variable of the partial type
+            -- signature is not actually quantified.  How can that happen?
+            -- See Note [Quantification and partial signatures] Wrinkle 4
+            --     in TcSimplify
+       ; mapM_ report_mono_sig_tv_err [ n | (n,tv) <- psig_qtv_prs
+                                          , not (tv `elem` qtvs) ]
+
+       ; let psig_qtvs = mkVarSet (map snd psig_qtv_prs)
+
+       ; annotated_theta      <- zonkTcTypes annotated_theta
+       ; (free_tvs, my_theta) <- choose_psig_context psig_qtvs annotated_theta wcx
 
-    report_sig_tv_err (n1,n2)
+       ; let keep_me    = free_tvs `unionVarSet` psig_qtvs
+             final_qtvs = [ mkTyVarBinder vis tv
+                          | tv <- qtvs -- Pulling from qtvs maintains original order
+                          , tv `elemVarSet` keep_me
+                          , let vis | tv `elemVarSet` psig_qtvs = Specified
+                                    | otherwise                 = Inferred ]
+
+       ; return (final_qtvs, my_theta) }
+  where
+    report_dup_sig_tv_err (n1,n2)
       | PartialSig { psig_name = fn_name, psig_hs_ty = hs_ty } <- sig
       = addErrTc (hang (text "Couldn't match" <+> quotes (ppr n1)
                         <+> text "with" <+> quotes (ppr n2))
@@ -974,6 +977,14 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs
       | otherwise -- Can't happen; by now we know it's a partial sig
       = pprPanic "report_sig_tv_err" (ppr sig)
 
+    report_mono_sig_tv_err n
+      | PartialSig { psig_name = fn_name, psig_hs_ty = hs_ty } <- sig
+      = addErrTc (hang (text "Can't quantify over" <+> quotes (ppr n))
+                     2 (hang (text "bound by the partial type signature:")
+                           2 (ppr fn_name <+> dcolon <+> ppr hs_ty)))
+      | otherwise -- Can't happen; by now we know it's a partial sig
+      = pprPanic "report_sig_tv_err" (ppr sig)
+
     choose_psig_context :: VarSet -> TcThetaType -> Maybe TcTyVar
                         -> TcM (VarSet, TcThetaType)
     choose_psig_context _ annotated_theta Nothing
@@ -1129,6 +1140,7 @@ So we make a test, one per parital signature, to check that the
 explicitly-quantified type variables have not been unified together.
 Trac #14449 showed this up.
 
+
 Note [Validity of inferred types]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We need to check inferred type for validity, in case it uses language
diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs
index 16bf345e4e..6ebf27d3e8 100644
--- a/compiler/typecheck/TcSimplify.hs
+++ b/compiler/typecheck/TcSimplify.hs
@@ -855,24 +855,36 @@ decideMonoTyVars :: InferMode
 --   (c) Connected by an equality to (a) or (b)
 -- Also return the reduced set of constraint we can generalise
 decideMonoTyVars infer_mode name_taus psigs candidates
-  = do { (no_quant, yes_quant) <- pick infer_mode candidates
+  = do { (no_quant, maybe_quant) <- pick infer_mode candidates
+
+       -- If possible, we quantify over partial-sig qtvs, so they are
+       -- not mono. Need to zonk them because they are meta-tyvar SigTvs
+       ; psig_qtvs <- mapM zonkTcTyVarToTyVar $
+                      concatMap (map snd . sig_inst_skols) psigs
 
        ; gbl_tvs <- tcGetGlobalTyCoVars
        ; let eq_constraints  = filter isEqPred candidates
              mono_tvs1       = growThetaTyVars eq_constraints gbl_tvs
-             constrained_tvs = growThetaTyVars eq_constraints
+
+             constrained_tvs = (growThetaTyVars eq_constraints
                                                (tyCoVarsOfTypes no_quant)
-                               `minusVarSet` mono_tvs1
-             mono_tvs2       = mono_tvs1 `unionVarSet` constrained_tvs
-             -- A type variable is only "constrained" (so that the MR bites)
-             -- if it is not free in the environment (Trac #13785)
-
-       -- Always quantify over partial-sig qtvs, so they are not mono
-       -- Need to zonk them because they are meta-tyvar SigTvs
-       -- Note [Quantification and partial signatures], wrinkle 3
-       ; psig_qtvs <- mapM zonkTcTyVarToTyVar $
-                      concatMap (map snd . sig_inst_skols) psigs
-       ; let mono_tvs = mono_tvs2 `delVarSetList` psig_qtvs
+                                `minusVarSet` mono_tvs1)
+                               `delVarSetList` psig_qtvs
+             -- constrained_tvs: the tyvars that we are not going to
+             -- quantify solely because of the moonomorphism restriction
+             --
+             -- (`minusVarSet` mono_tvs`): a type variable is only
+             --   "constrained" (so that the MR bites) if it is not
+             --   free in the environment (Trac #13785)
+             --
+             -- (`delVarSetList` psig_qtvs): if the user has explicitly
+             --   asked for quantification, then that request "wins"
+             --   over the MR.  Note: do /not/ delete psig_qtvs from
+             --   mono_tvs1, because mono_tvs1 cannot under any circumstances
+             --   be quantified (Trac #14479); see
+             --   Note [Quantification and partial signatures], Wrinkle 3, 4
+
+             mono_tvs = mono_tvs1 `unionVarSet` constrained_tvs
 
            -- Warn about the monomorphism restriction
        ; warn_mono <- woptM Opt_WarnMonomorphism
@@ -885,11 +897,11 @@ decideMonoTyVars infer_mode name_taus psigs candidates
        ; traceTc "decideMonoTyVars" $ vcat
            [ text "gbl_tvs =" <+> ppr gbl_tvs
            , text "no_quant =" <+> ppr no_quant
-           , text "yes_quant =" <+> ppr yes_quant
+           , text "maybe_quant =" <+> ppr maybe_quant
            , text "eq_constraints =" <+> ppr eq_constraints
            , text "mono_tvs =" <+> ppr mono_tvs ]
 
-       ; return (mono_tvs, yes_quant) }
+       ; return (mono_tvs, maybe_quant) }
   where
     pick :: InferMode -> [PredType] -> TcM ([PredType], [PredType])
     -- Split the candidates into ones we definitely
@@ -980,7 +992,7 @@ decideQuantifiedTyVars
 decideQuantifiedTyVars mono_tvs name_taus psigs candidates
   = do {     -- Why psig_tys? We try to quantify over everything free in here
              -- See Note [Quantification and partial signatures]
-             --     wrinkles 2 and 3
+             --     Wrinkles 2 and 3
        ; psig_tv_tys <- mapM TcM.zonkTcTyVar [ tv | sig <- psigs
                                                   , (_,tv) <- sig_inst_skols sig ]
        ; psig_theta <- mapM TcM.zonkTcType [ pred | sig <- psigs
@@ -1093,17 +1105,22 @@ sure to quantify over them.  This leads to several wrinkles:
 
 * Wrinkle 3 (Trac #13482). Also consider
     f :: forall a. _ => Int -> Int
-    f x = if undefined :: a == undefined then x else 0
+    f x = if (undefined :: a) == undefined then x else 0
   Here we get an (Eq a) constraint, but it's not mentioned in the
-  psig_theta nor the type of 'f'.  Moreover, if we have
-    f :: forall a. a -> _
-    f x = not x
-  and a constraint (a ~ g), where 'g' is free in the environment,
-  we would not usually quanitfy over 'a'.  But here we should anyway
-  (leading to a justified subsequent error) since 'a' is explicitly
-  quantified by the programmer.
-
-  Bottom line: always quantify over the psig_tvs, regardless.
+  psig_theta nor the type of 'f'.  But we still want to quantify
+  over 'a' even if the monomorphism restriction is on.
+
+* Wrinkle 4 (Trac #14479)
+    foo :: Num a => a -> a
+    foo xxx = g xxx
+      where
+        g :: forall b. Num b => _ -> b
+        g y = xxx + y
+
+  In the signature for 'g', we cannot quantify over 'b' because it turns out to
+  get unified with 'a', which is free in g's environment.  So we carefully
+  refrain from bogusly quantifying, in TcSimplify.decideMonoTyVars.  We
+  report the error later, in TcBinds.chooseInferredQuantifiers.
 
 Note [Quantifying over equality constraints]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/testsuite/tests/partial-sigs/should_fail/T14479.hs b/testsuite/tests/partial-sigs/should_fail/T14479.hs
new file mode 100644
index 0000000000..13ee256e83
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_fail/T14479.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE ScopedTypeVariables, PartialTypeSignatures #-}
+
+module T14479 where
+
+foo :: Num a => a -> a
+foo xxx = g xxx
+  where
+    g :: forall b. Num b => _ -> b
+    g y = xxx + y
diff --git a/testsuite/tests/partial-sigs/should_fail/T14479.stderr b/testsuite/tests/partial-sigs/should_fail/T14479.stderr
new file mode 100644
index 0000000000..84ba90a572
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_fail/T14479.stderr
@@ -0,0 +1,10 @@
+
+T14479.hs:9:5: error:
+    • Can't quantify over ‘b’
+        bound by the partial type signature: g :: forall b. Num b => _ -> b
+    • In an equation for ‘foo’:
+          foo xxx
+            = g xxx
+            where
+                g :: forall b. Num b => _ -> b
+                g y = xxx + y
diff --git a/testsuite/tests/partial-sigs/should_fail/all.T b/testsuite/tests/partial-sigs/should_fail/all.T
index bb813f0b08..91509c4f36 100644
--- a/testsuite/tests/partial-sigs/should_fail/all.T
+++ b/testsuite/tests/partial-sigs/should_fail/all.T
@@ -66,3 +66,4 @@ test('T12634', normal, compile_fail, [''])
 test('T12732', normal, compile_fail, ['-fobject-code -fdefer-typed-holes'])
 test('T14040a', normal, compile_fail, [''])
 test('T14449', normal, compile_fail, [''])
+test('T14479', normal, compile_fail, [''])