Check quantification for partial type signatues

Trac #14449 showed that we were failing to check that the
quantified type variables of a partial type signature remained
distinct.

See Note [Quantified variables in partial type signatures]
in TcBinds.

A little refactoring along the way.

5 files changed, 103 insertions, 49 deletions

diff --git a/compiler/typecheck/TcBinds.hs b/compiler/typecheck/TcBinds.hs
index 6a9b22a9bb..6b351830dc 100644
--- a/compiler/typecheck/TcBinds.hs
+++ b/compiler/typecheck/TcBinds.hs
@@ -938,46 +938,11 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs
                                       , sig_inst_wcx   = wcx
                                       , sig_inst_theta = annotated_theta
                                       , sig_inst_skols = annotated_tvs }))
-  | Nothing <- wcx
-  = do { annotated_theta <- zonkTcTypes annotated_theta
-       ; let free_tvs = closeOverKinds (tyCoVarsOfTypes annotated_theta
-                                        `unionVarSet` tau_tvs)
-       ; traceTc "ciq" (vcat [ ppr sig, ppr annotated_theta, ppr free_tvs])
-       ; psig_qtvs <- mk_psig_qtvs annotated_tvs
-       ; return (mk_final_qtvs psig_qtvs free_tvs, annotated_theta) }
-
-  | Just wc_var <- wcx
-  = do { annotated_theta <- zonkTcTypes annotated_theta
-       ; let free_tvs = closeOverKinds (growThetaTyVars inferred_theta seed_tvs)
-                          -- growThetaVars just like the no-type-sig case
-                          -- Omitting this caused #12844
-             seed_tvs = tyCoVarsOfTypes annotated_theta  -- These are put there
-                        `unionVarSet` tau_tvs            --       by the user
-
-       ; psig_qtvs <- mk_psig_qtvs annotated_tvs
-       ; let my_qtvs  = mk_final_qtvs psig_qtvs free_tvs
-             keep_me  = psig_qtvs `unionVarSet` free_tvs
-             my_theta = pickCapturedPreds keep_me inferred_theta
-
-       -- Fill in the extra-constraints wildcard hole with inferred_theta,
-       -- so that the Hole constraint we have already emitted (in tcHsPartialSigType)
-       -- can report what filled it in.
-       -- NB: my_theta already includes all the annotated constraints
-             inferred_diff = [ pred
-                             | pred <- my_theta
-                             , all (not . (`eqType` pred)) annotated_theta ]
-       ; ctuple <- mk_ctuple inferred_diff
-       ; writeMetaTyVar wc_var ctuple
-
-       ; traceTc "completeTheta" $
-            vcat [ ppr sig
-                 , ppr annotated_theta, ppr inferred_theta
-                 , ppr inferred_diff ]
-       ; return (my_qtvs, my_theta) }
-
-  | otherwise  -- A complete type signature is dealt with in mkInferredPolyId
-  = pprPanic "chooseInferredQuantifiers" (ppr sig)
-
+  = -- 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
@@ -988,14 +953,66 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs
       where
         keep_me = free_tvs `unionVarSet` psig_qtvs
 
+    mk_psig_qtvs :: [(Name,TcTyVar)] -> TcM TcTyVarSet
+    mk_psig_qtvs annotated_tvs
+       = do { let (sig_tv_names, sig_tvs) = unzip annotated_tvs
+            ; psig_qtvs <- mapM zonkTcTyVarToTyVar sig_tvs
+
+            -- Report an error if the quantified variables of the
+            -- partial signature have been unified together
+            -- See Note [Quantified variables in partial type signatures]
+            ; let bad_sig_tvs = findDupsEq eq (sig_tv_names `zip` psig_qtvs)
+                  eq (_,tv1) (_,tv2) = tv1 == tv2
+            ; mapM_ (report_sig_tv_err sig) bad_sig_tvs
+
+            ; return (mkVarSet psig_qtvs) }
+
+    report_sig_tv_err (PartialSig { psig_name = fn_name, psig_hs_ty = hs_ty })
+                      ((n1,_) :| (n2,_) : _)
+      = addErrTc (hang (text "Couldn't match" <+> quotes (ppr n1)
+                        <+> text "with" <+> quotes (ppr n2))
+                     2 (hang (text "both bound by the partial type signature:")
+                           2 (ppr fn_name <+> dcolon <+> ppr hs_ty)))
+    report_sig_tv_err sig _ = pprPanic "report_sig_tv_err" (ppr sig)
+                              -- Can't happen; by now we know it's a partial sig
+
+    choose_psig_context :: VarSet -> TcThetaType -> Maybe TcTyVar
+                        -> TcM (VarSet, TcThetaType)
+    choose_psig_context _ annotated_theta Nothing
+      = do { let free_tvs = closeOverKinds (tyCoVarsOfTypes annotated_theta
+                                            `unionVarSet` tau_tvs)
+           ; return (free_tvs, annotated_theta) }
+
+    choose_psig_context psig_qtvs annotated_theta (Just wc_var)
+      = do { let free_tvs = closeOverKinds (growThetaTyVars inferred_theta seed_tvs)
+                            -- growThetaVars just like the no-type-sig case
+                            -- Omitting this caused #12844
+                 seed_tvs = tyCoVarsOfTypes annotated_theta  -- These are put there
+                            `unionVarSet` tau_tvs            --       by the user
+
+           ; let keep_me  = psig_qtvs `unionVarSet` free_tvs
+                 my_theta = pickCapturedPreds keep_me inferred_theta
+
+           -- Fill in the extra-constraints wildcard hole with inferred_theta,
+           -- so that the Hole constraint we have already emitted
+           -- (in tcHsPartialSigType) can report what filled it in.
+           -- NB: my_theta already includes all the annotated constraints
+           ; let inferred_diff = [ pred
+                                 | pred <- my_theta
+                                 , all (not . (`eqType` pred)) annotated_theta ]
+           ; ctuple <- mk_ctuple inferred_diff
+           ; writeMetaTyVar wc_var ctuple
+
+           ; traceTc "completeTheta" $
+                vcat [ ppr sig
+                     , ppr annotated_theta, ppr inferred_theta
+                     , ppr inferred_diff ]
+           ; return (free_tvs, my_theta) }
+
     mk_ctuple preds = return (mkBoxedTupleTy preds)
        -- Hack alert!  See TcHsType:
        -- Note [Extra-constraint holes in partial type signatures]
 
-    mk_psig_qtvs :: [(Name,TcTyVar)] -> TcM TcTyVarSet
-    mk_psig_qtvs annotated_tvs
-       = do { psig_qtvs <- mapM (zonkTcTyVarToTyVar . snd) annotated_tvs
-            ; return (mkVarSet psig_qtvs) }
 
 mk_impedance_match_msg :: MonoBindInfo
                        -> TcType -> TcType
@@ -1093,6 +1110,27 @@ It's stupid to apply the MR here.  This test includes an extra-constraints
 wildcard; that is, we don't apply the MR if you write
    f3 :: _ => blah
 
+Note [Quantified variables in partial type signatures]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+  f :: forall a. a -> a -> _
+  f x y = g x y
+  g :: forall b. b -> b -> _
+  g x y = [x, y]
+
+Here, 'f' and 'g' are mutually recursive, and we end up unifyin 'a' and 'b'
+together, which is fine.  So we bind 'a' and 'b' to SigTvs, which can then
+unify with each other.
+
+But now consider:
+  f :: forall a b. a -> b -> _
+  f x y = [x, y]
+
+We want to get an error from this, because 'a' and 'b' get unified.
+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/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index 6908d16dfc..10794e2d2b 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -2004,8 +2004,10 @@ tcHsPartialSigType ctxt sig_ty
             <- tcWildCardBindersX newWildTyVar sig_wcs        $ \ wcs ->
                tcImplicitTKBndrsX new_implicit_tv implicit_hs_tvs $
                tcExplicitTKBndrsX newSigTyVar explicit_hs_tvs $ \ explicit_tvs ->
-               do {   -- Instantiate the type-class context; but if there
-                      -- is an extra-constraints wildcard, just discard it here
+                  -- Why newSigTyVar?  See TcBinds
+                  -- Note [Quantified variables in partial type signatures]
+             do {   -- Instantiate the type-class context; but if there
+                    -- is an extra-constraints wildcard, just discard it here
                     (theta, wcx) <- tcPartialContext hs_ctxt
 
                   ; tau <- tcHsOpenType hs_tau
@@ -2033,9 +2035,12 @@ tcHsPartialSigType ctxt sig_ty
         ; traceTc "tcHsPartialSigType" (ppr all_tvs)
         ; return (wcs, wcx, all_tvs, theta, tau) }
   where
-    new_implicit_tv name = do { kind <- newMetaKindVar
-                              ; tv <- newSigTyVar name kind
-                              ; return (tv, False) }
+    new_implicit_tv name
+      = do { kind <- newMetaKindVar
+           ; tv <- newSigTyVar name kind
+             -- Why newSigTyVar?  See TcBinds
+             -- Note [Quantified variables in partial type signatures]
+           ; return (tv, False) }
 
 tcPartialContext :: HsContext GhcRn -> TcM (TcThetaType, Maybe TcTyVar)
 tcPartialContext hs_theta
diff --git a/testsuite/tests/partial-sigs/should_fail/T14449.hs b/testsuite/tests/partial-sigs/should_fail/T14449.hs
new file mode 100644
index 0000000000..d49a390af2
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_fail/T14449.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE PartialTypeSignatures #-}
+
+module T14449 where
+
+f :: a -> b -> _
+f x y = [x, y]
diff --git a/testsuite/tests/partial-sigs/should_fail/T14449.stderr b/testsuite/tests/partial-sigs/should_fail/T14449.stderr
new file mode 100644
index 0000000000..01e73b5edb
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_fail/T14449.stderr
@@ -0,0 +1,4 @@
+
+T14449.hs:6:1: error:
+    Couldn't match ‘a’ with ‘b’
+      both bound by the partial type signature: f :: a -> b -> _
diff --git a/testsuite/tests/partial-sigs/should_fail/all.T b/testsuite/tests/partial-sigs/should_fail/all.T
index 183791868f..d452dad101 100644
--- a/testsuite/tests/partial-sigs/should_fail/all.T
+++ b/testsuite/tests/partial-sigs/should_fail/all.T
@@ -64,3 +64,4 @@ test('PatBind3', normal, compile_fail, [''])
 test('T12039', normal, compile_fail, [''])
 test('T12634', normal, compile_fail, [''])
 test('T12732', normal, compile_fail, ['-fobject-code -fdefer-typed-holes'])
+test('T14449', normal, compile_fail, [''])