Fix quantification for inference with sigs

When we are *inferring* the type of a let-bound function,
we might still have a type signature.  And we must be sure
to quantify over its type variables, else you get the crash
in Trac #10615.

See Note [Which type variables to quantify] in TcSimplify

6 files changed, 100 insertions, 11 deletions

diff --git a/compiler/typecheck/TcBinds.hs b/compiler/typecheck/TcBinds.hs
index 9a7ad6184a..8a7ca4d5c1 100644
--- a/compiler/typecheck/TcBinds.hs
+++ b/compiler/typecheck/TcBinds.hs
@@ -650,9 +650,11 @@ tcPolyInfer rec_tc prag_fn tc_sig_fn mono bind_list
                 tcMonoBinds rec_tc tc_sig_fn LetLclBndr bind_list
 
        ; let name_taus = [(name, idType mono_id) | (name, _, mono_id) <- mono_infos]
+             sig_qtvs   = [ tv | (_, Just sig, _) <- mono_infos
+                               , (_, tv) <- sig_tvs sig ]
        ; traceTc "simplifyInfer call" (ppr name_taus $$ ppr wanted)
        ; (qtvs, givens, _mr_bites, ev_binds)
-                 <- simplifyInfer tclvl mono name_taus wanted
+                 <- simplifyInfer tclvl mono sig_qtvs name_taus wanted
 
        ; let inferred_theta = map evVarPred givens
        ; exports <- checkNoErrs $
diff --git a/compiler/typecheck/TcRnDriver.hs b/compiler/typecheck/TcRnDriver.hs
index 4cfa449a88..e361dcbc3f 100644
--- a/compiler/typecheck/TcRnDriver.hs
+++ b/compiler/typecheck/TcRnDriver.hs
@@ -1798,6 +1798,7 @@ tcRnExpr hsc_env rdr_expr
                                       {-# SCC "simplifyInfer" #-}
                                       simplifyInfer tclvl
                                                     False {- No MR for now -}
+                                                    []    {- No sig vars -}
                                                     [(fresh_it, res_ty)]
                                                     lie ;
     -- Wanted constraints from static forms
diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs
index 4129adcd46..825ce215ee 100644
--- a/compiler/typecheck/TcSimplify.hs
+++ b/compiler/typecheck/TcSimplify.hs
@@ -384,8 +384,10 @@ has a strictly-increased level compared to the ambient level outside
 the let binding.
 -}
 
-simplifyInfer :: TcLevel          -- Used when generating the constraints
+simplifyInfer :: TcLevel               -- Used when generating the constraints
               -> Bool                  -- Apply monomorphism restriction
+              -> [TcTyVar]             -- The quantified tyvars of any signatures
+                                       --   see Note [Which type variables to quantify]
               -> [(Name, TcTauType)]   -- Variables to be generalised,
                                        -- and their tau-types
               -> WantedConstraints
@@ -395,7 +397,7 @@ simplifyInfer :: TcLevel          -- Used when generating the constraints
                                     --   so the results type is not as general as
                                     --   it could be
                       TcEvBinds)    -- ... binding these evidence variables
-simplifyInfer rhs_tclvl apply_mr name_taus wanteds
+simplifyInfer rhs_tclvl apply_mr sig_qtvs name_taus wanteds
   | isEmptyWC wanteds
   = do { gbl_tvs <- tcGetGlobalTyVars
        ; qtkvs <- quantifyTyVars gbl_tvs (tyVarsOfTypes (map snd name_taus))
@@ -472,7 +474,7 @@ simplifyInfer rhs_tclvl apply_mr name_taus wanteds
        ; zonked_taus <- mapM (TcM.zonkTcType . snd) name_taus
        ; let zonked_tau_tvs = tyVarsOfTypes zonked_taus
        ; (qtvs, bound_theta, mr_bites)
-             <- decideQuantification apply_mr quant_pred_candidates zonked_tau_tvs
+             <- decideQuantification apply_mr sig_qtvs quant_pred_candidates zonked_tau_tvs
 
          -- Emit an implication constraint for the
          -- remaining constraints from the RHS
@@ -564,18 +566,19 @@ and the quantified constraints are empty.
 
 decideQuantification
     :: Bool                       -- Apply monomorphism restriction
+    -> [TcTyVar]
     -> [PredType] -> TcTyVarSet   -- Constraints and type variables from RHS
     -> TcM ( [TcTyVar]       -- Quantify over these tyvars (skolems)
            , [PredType]      -- and this context (fully zonked)
            , Bool )          -- Did the MR bite?
 -- See Note [Deciding quantification]
-decideQuantification apply_mr constraints zonked_tau_tvs
+decideQuantification apply_mr sig_qtvs constraints zonked_tau_tvs
   | apply_mr     -- Apply the Monomorphism restriction
   = do { gbl_tvs <- tcGetGlobalTyVars
        ; let constrained_tvs = tyVarsOfTypes constraints
              mono_tvs = gbl_tvs `unionVarSet` constrained_tvs
              mr_bites = constrained_tvs `intersectsVarSet` zonked_tau_tvs
-       ; qtvs <- quantifyTyVars mono_tvs zonked_tau_tvs
+       ; qtvs <- quantify_tvs mono_tvs zonked_tau_tvs
        ; traceTc "decideQuantification 1" (vcat [ppr constraints, ppr gbl_tvs, ppr mono_tvs, ppr qtvs])
        ; return (qtvs, [], mr_bites) }
 
@@ -583,7 +586,7 @@ decideQuantification apply_mr constraints zonked_tau_tvs
   = do { gbl_tvs <- tcGetGlobalTyVars
        ; let mono_tvs     = growThetaTyVars (filter isEqPred constraints) gbl_tvs
              tau_tvs_plus = growThetaTyVars constraints zonked_tau_tvs
-       ; qtvs        <- quantifyTyVars mono_tvs tau_tvs_plus
+       ; qtvs        <- quantify_tvs mono_tvs tau_tvs_plus
        ; constraints <- zonkTcThetaType constraints
               -- quantifyTyVars turned some meta tyvars into
               -- quantified skolems, so we have to zonk again
@@ -595,6 +598,12 @@ decideQuantification apply_mr constraints zonked_tau_tvs
                                                 , ppr tau_tvs_plus, ppr qtvs, ppr min_theta])
        ; return (qtvs, min_theta, False) }
 
+  where
+    quantify_tvs mono_tvs tau_tvs   -- See Note [Which type variable to quantify]
+      | null sig_qtvs = quantifyTyVars mono_tvs tau_tvs
+      | otherwise     = quantifyTyVars (mono_tvs `delVarSetList`    sig_qtvs)
+                                       (tau_tvs  `extendVarSetList` sig_qtvs)
+
 ------------------
 pickQuantifiablePreds :: TyVarSet         -- Quantifying over these
                       -> TcThetaType      -- Proposed constraints to quantify
@@ -651,7 +660,34 @@ growThetaTyVars theta tvs
        where
          pred_tvs = tyVarsOfType pred
 
-{-
+{- Note [Which type variables to quantify]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When choosing type variables to quantify, the basic plan is to
+quantify over all type variables that are
+ * free in the tau_tvs, and
+ * not forced to be monomorphic (mono_tvs),
+   for example by being free in the environment
+
+However, for a pattern binding, or with wildards, we might
+be doing inference *in the presence of a type signature*.
+Mostly, if there is a signature we use CheckGen, not InferGen,
+but with pattern bindings or wildcards we might do inference
+and still have a type signature.  For example:
+   f :: _ -> a
+   f x = ...
+or
+   p :: a -> a
+   (p,q) = e
+In both cases we use plan InferGen, and hence call simplifyInfer.
+But those 'a' variables are skolems, and we should be sure to quantify
+over them, regardless of the monomorphism restriction etc.  If we
+don't, when reporting a type error we panic when we find that a
+skolem isn't bound by any enclosing implication.
+
+That's why we pass sig_qtvs to simplifyInfer, and make sure (in
+quantify_tvs) that we do quantify over them.  Trac #10615 is
+a case in point.
+
 Note [Quantifying over equality constraints]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Should we quantify over an equality constraint (s ~ t)?  In general, we don't.
@@ -1082,6 +1118,7 @@ warnRedundantGivens (SigSkol ctxt _)
        FunSigCtxt _ warn_redundant -> warn_redundant
        ExprSigCtxt                 -> True
        _                           -> False
+
 warnRedundantGivens (InstSkol {}) = True
 warnRedundantGivens _             = False
 
@@ -1201,9 +1238,12 @@ works:
      we do an ambiguity check on the type (which would find that one
      of the Ord a constraints was redundant), and then we check that
      the definition has that type (which might find that both are
-     redundant).  We don't want to report the same error twice, so
-     we disable it for the ambiguity check.  Hence the flag in
-     TcType.FunSigCtxt.
+     redundant).  We don't want to report the same error twice, so we
+     disable it for the ambiguity check.  Hence using two different
+     FunSigCtxts, one with the warn-redundant field set True, and the
+     other set False in
+        - TcBinds.tcSpecPrag
+        - TcBinds.tcTySig
 
   This decision is taken in setImplicationStatus, rather than TcErrors
   so that we can discard implication constraints that we don't need.
diff --git a/testsuite/tests/partial-sigs/should_fail/T10615.hs b/testsuite/tests/partial-sigs/should_fail/T10615.hs
new file mode 100644
index 0000000000..6938736e02
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_fail/T10615.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE RankNTypes #-}
+module T10615 where
+
+f1 :: _ -> f
+f1 = const
+
+f2 :: _ -> _f
+f2 = const
+
+
diff --git a/testsuite/tests/partial-sigs/should_fail/T10615.stderr b/testsuite/tests/partial-sigs/should_fail/T10615.stderr
new file mode 100644
index 0000000000..22ce84af63
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_fail/T10615.stderr
@@ -0,0 +1,34 @@
+

+T10615.hs:4:7: error:

+    Found type wildcard ‘_’ standing for ‘a1’

+    Where: ‘a1’ is an ambiguous type variable

+    To use the inferred type, enable PartialTypeSignatures

+    In the type signature for:

+      f1 :: _ -> f

+

+T10615.hs:5:6: error:

+    Couldn't match type ‘f’ with ‘b1 -> a1’

+    ‘f’ is a rigid type variable bound by

+        the inferred type of f1 :: a1 -> f at T10615.hs:4:7

+    Expected type: a1 -> f

+      Actual type: a1 -> b1 -> a1

+    Relevant bindings include f1 :: a1 -> f (bound at T10615.hs:5:1)

+    In the expression: const

+    In an equation for ‘f1’: f1 = const

+

+T10615.hs:7:7: error:

+    Found type wildcard ‘_’ standing for ‘a0’

+    Where: ‘a0’ is an ambiguous type variable

+    To use the inferred type, enable PartialTypeSignatures

+    In the type signature for:

+      f2 :: _ -> _f

+

+T10615.hs:8:6: error:

+    Couldn't match type ‘_f’ with ‘b0 -> a0’

+    ‘_f’ is a rigid type variable bound by

+         the inferred type of f2 :: a0 -> _f at T10615.hs:7:7

+    Expected type: a0 -> _f

+      Actual type: a0 -> b0 -> a0

+    Relevant bindings include f2 :: a0 -> _f (bound at T10615.hs:8:1)

+    In the expression: const

+    In an equation for ‘f2’: f2 = const

diff --git a/testsuite/tests/partial-sigs/should_fail/all.T b/testsuite/tests/partial-sigs/should_fail/all.T
index 8f0b0a0f77..d172a01c7c 100644
--- a/testsuite/tests/partial-sigs/should_fail/all.T
+++ b/testsuite/tests/partial-sigs/should_fail/all.T
@@ -58,3 +58,5 @@ test('WildcardInstantiations', normal, compile_fail, [''])
 test('WildcardInTypeFamilyInstanceRHS', normal, compile_fail, [''])
 test('WildcardInTypeSynonymLHS', normal, compile_fail, [''])
 test('WildcardInTypeSynonymRHS', normal, compile_fail, [''])
+test('T10615', normal, compile_fail, [''])
+