Refactor decideQuantification

Richard was interrogating me about decideQuantification yesterday.
I got a bit stuck on the promote_tvs part. This refactoring

 * simplifes the API of decideQuantification

 * move mkMinimalBySCs into decideQuantification (a better place for it)

 * moves promotion out of decideQuantification (where it didn't really
   fit), and comments much more fully what is going on with the promtion stuff

 * comments decideQuantification more fully

 * coments the EqPred case of quantifyPred more fully

It turned out that the theta returned by decideQuantification,
and hence by simplifyInfer, is now fully zonked, so I could remove
a zonking in TcBinds.

4 files changed, 144 insertions, 105 deletions

diff --git a/compiler/typecheck/TcBinds.hs b/compiler/typecheck/TcBinds.hs
index fc84c595e6..9d0bb551bf 100644
--- a/compiler/typecheck/TcBinds.hs
+++ b/compiler/typecheck/TcBinds.hs
@@ -598,7 +598,7 @@ tcPolyInfer rec_tc prag_fn tc_sig_fn mono closed bind_list
        ; (qtvs, givens, mr_bites, ev_binds)
                  <- simplifyInfer tclvl mono name_taus wanted
 
-       ; inferred_theta  <- zonkTcThetaType (map evVarPred givens)
+       ; let inferred_theta = map evVarPred givens
        ; exports <- checkNoErrs $ mapM (mkExport prag_fn qtvs inferred_theta)
                                        mono_infos
 
diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs
index 773a5e6a12..f528da33fe 100644
--- a/compiler/typecheck/TcSimplify.hs
+++ b/compiler/typecheck/TcSimplify.hs
@@ -266,7 +266,7 @@ simplifyInfer :: TcLevel          -- Used when generating the constraints
                                        -- and their tau-types
               -> WantedConstraints
               -> TcM ([TcTyVar],    -- Quantify over these type variables
-                      [EvVar],      -- ... and these constraints
+                      [EvVar],      -- ... and these constraints (fully zonked)
                       Bool,         -- The monomorphism restriction did something
                                     --   so the results type is not as general as
                                     --   it could be
@@ -331,7 +331,6 @@ simplifyInfer rhs_tclvl apply_mr name_taus wanteds
                             -- If any meta-tyvar unifications take place (unlikely), we'll
                             -- pick that up later.
 
-
                       ; WC { wc_simple = simples }
                            <- setTcLevel rhs_tclvl                $
                               runTcSWithEvBinds null_ev_binds_var $
@@ -343,30 +342,27 @@ simplifyInfer rhs_tclvl apply_mr name_taus wanteds
                                              , let ev = ctEvidence ct
                                              , isWanted ev ] }
 
-       -- NB: quant_pred_candidates is already the fixpoint of any
-       --     unifications that may have happened
+       -- NB: quant_pred_candidates is already fully zonked
 
+         -- Decide what type variables and constraints to quantify
        ; zonked_taus <- mapM (TcM.zonkTcType . snd) name_taus
        ; let zonked_tau_tvs = tyVarsOfTypes zonked_taus
-       ; (promote_tvs, qtvs, bound, mr_bites) <- decideQuantification apply_mr quant_pred_candidates zonked_tau_tvs
-
-       ; outer_tclvl <- TcRnMonad.getTcLevel
-       ; runTcSWithEvBinds null_ev_binds_var $  -- runTcS just to get the types right :-(
-         mapM_ (promoteTyVar outer_tclvl) (varSetElems promote_tvs)
+       ; (qtvs, bound_theta, mr_bites) 
+             <- decideQuantification apply_mr quant_pred_candidates zonked_tau_tvs
 
-       ; let minimal_simple_preds = mkMinimalBySCs bound
-                  -- See Note [Minimize by Superclasses]
-             skol_info = InferSkol [ (name, mkSigmaTy [] minimal_simple_preds ty)
+         -- Emit an implication constraint for the 
+         -- remaining constaints from the RHS
+       ; bound_ev_vars <- mapM TcM.newEvVar bound_theta
+       ; let skol_info = InferSkol [ (name, mkSigmaTy [] bound_theta ty)
                                    | (name, ty) <- name_taus ]
                         -- Don't add the quantified variables here, because
-                        -- they are also bound in ic_skols and we want them to be
-                        -- tidied uniformly
+                        -- they are also bound in ic_skols and we want them
+                        -- to be tidied uniformly
 
-       ; minimal_bound_ev_vars <- mapM TcM.newEvVar minimal_simple_preds
-       ; let implic = Implic { ic_tclvl    = rhs_tclvl
+             implic = Implic { ic_tclvl    = rhs_tclvl
                              , ic_skols    = qtvs
                              , ic_no_eqs   = False
-                             , ic_given    = minimal_bound_ev_vars
+                             , ic_given    = bound_ev_vars
                              , ic_wanted   = wanted_transformed
                              , ic_status   = IC_Unsolved
                              , ic_binds    = ev_binds_var
@@ -374,20 +370,40 @@ simplifyInfer rhs_tclvl apply_mr name_taus wanteds
                              , ic_env      = tc_lcl_env }
        ; emitImplication implic
 
+         -- Promote any type variables that are free in the inferred type
+         -- of the function:
+         --    f :: forall qtvs. bound_theta => zonked_tau
+         -- These variables now become free in the envt, and hence will show 
+         -- up whenever 'f' is called.  They may currently at rhs_tclvl, but
+         -- they had better be unifiable at the outer_tclvl!
+         -- Example:   envt mentions alpha[1]
+         --            tau_ty = beta[2] -> beta[2]
+         --            consraints = alpha ~ [beta]
+         -- we don't quantify over beta (since it is fixed by envt)
+         -- so we must promote it!  The inferred type is just
+         --   f :: beta -> beta
+       ; outer_tclvl    <- TcRnMonad.getTcLevel
+       ; zonked_tau_tvs <- TcM.zonkTyVarsAndFV zonked_tau_tvs
+              -- decideQuantification turned some meta tyvars into
+              -- quantified skolems, so we have to zonk again
+       ; let phi_tvs     = tyVarsOfTypes bound_theta `unionVarSet` zonked_tau_tvs
+             promote_tvs = varSetElems (closeOverKinds phi_tvs `delVarSetList` qtvs)
+       ; runTcSWithEvBinds null_ev_binds_var $  -- runTcS just to get the types right :-(
+         mapM_ (promoteTyVar outer_tclvl) promote_tvs
+
+         -- All done!
        ; traceTc "} simplifyInfer/produced residual implication for quantification" $
          vcat [ ptext (sLit "quant_pred_candidates =") <+> ppr quant_pred_candidates
               , ptext (sLit "zonked_taus") <+> ppr zonked_taus
               , ptext (sLit "zonked_tau_tvs=") <+> ppr zonked_tau_tvs
               , ptext (sLit "promote_tvs=") <+> ppr promote_tvs
-              , ptext (sLit "bound =") <+> ppr bound
-              , ptext (sLit "minimal_bound =") <+> vcat [ ppr v <+> dcolon <+> ppr (idType v)
-                                                        | v <- minimal_bound_ev_vars]
+              , ptext (sLit "bound_theta =") <+> vcat [ ppr v <+> dcolon <+> ppr (idType v)
+                                                        | v <- bound_ev_vars]
               , ptext (sLit "mr_bites =") <+> ppr mr_bites
               , ptext (sLit "qtvs =") <+> ppr qtvs
               , ptext (sLit "implic =") <+> ppr implic ]
 
-       ; return ( qtvs, minimal_bound_ev_vars
-                , mr_bites,  TcEvBinds ev_binds_var) }
+       ; return ( qtvs, bound_ev_vars, mr_bites, TcEvBinds ev_binds_var) }
 
 {-
 ************************************************************************
@@ -402,66 +418,76 @@ If the monomorphism restriction does not apply, then we quantify as follows:
   * Take the global tyvars, and "grow" them using the equality constraints
     E.g.  if x:alpha is in the environment, and alpha ~ [beta] (which can
           happen because alpha is untouchable here) then do not quantify over
-          beta
+          beta, because alpha fixes beta, and beta is effectively free in
+          the environment too
     These are the mono_tvs
 
   * Take the free vars of the tau-type (zonked_tau_tvs) and "grow" them
-    using all the constraints, but knocking out the mono_tvs
+    using all the constraints.  These are tau_tvs_plus
 
-    The result is poly_qtvs, which we will quantify over.
+  * Use quantifyTyVars to quantify over (tau_tvs_plus - mono_tvs), being
+    careful to close over kinds, and to skolemise the quantified tyvars.
+    (This actually unifies each quantifies meta-tyvar with a fresh skolem.)
+    Result is qtvs.
 
-  * Filter the constraints using quantifyPred and the poly_qtvs
+  * Filter the constraints using quantifyPred and the qtvs.  We have to
+    zonk the constraints first, so they "see" the freshly created skolems.
 
 If the MR does apply, mono_tvs includes all the constrained tyvars,
 and the quantified constraints are empty.
 -}
 
-decideQuantification :: Bool -> [PredType] -> TcTyVarSet
-                     -> TcM ( TcTyVarSet      -- Promote these
-                            , [TcTyVar]       -- Do quantify over these
-                            , [PredType]      -- and these
-                            , Bool )          -- Did the MR bite?
+decideQuantification 
+    :: Bool                       -- Apply monomorphism restriction
+    -> [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
   | apply_mr     -- Apply the Monomorphism restriction
   = do { gbl_tvs <- tcGetGlobalTyVars
-       ; let mono_tvs = gbl_tvs `unionVarSet` constrained_tvs
+       ; let constrained_tvs = tyVarsOfTypes constraints
+             mono_tvs = gbl_tvs `unionVarSet` constrained_tvs
              mr_bites = constrained_tvs `intersectsVarSet` zonked_tau_tvs
-             promote_tvs = constrained_tvs `unionVarSet` (zonked_tau_tvs `intersectVarSet` gbl_tvs)
        ; qtvs <- quantifyTyVars mono_tvs zonked_tau_tvs
        ; traceTc "decideQuantification 1" (vcat [ppr constraints, ppr gbl_tvs, ppr mono_tvs, ppr qtvs])
-       ; return (promote_tvs, qtvs, [], mr_bites) }
+       ; return (qtvs, [], mr_bites) }
 
   | otherwise
   = do { gbl_tvs <- tcGetGlobalTyVars
-       ; let mono_tvs    = growThetaTyVars (filter isEqPred constraints) gbl_tvs
-             poly_qtvs   = growThetaTyVars constraints zonked_tau_tvs
-                           `minusVarSet` mono_tvs
-             theta       = filter (quantifyPred poly_qtvs) constraints
-             promote_tvs = mono_tvs `intersectVarSet` (constrained_tvs `unionVarSet` zonked_tau_tvs)
-       ; qtvs <- quantifyTyVars mono_tvs poly_qtvs
-       ; traceTc "decideQuantification 2" (vcat [ppr constraints, ppr gbl_tvs, ppr mono_tvs, ppr poly_qtvs, ppr qtvs, ppr theta])
-       ; return (promote_tvs, qtvs, theta, False) }
-  where
-    constrained_tvs = tyVarsOfTypes constraints
+       ; let mono_tvs     = growThetaTyVars (filter isEqPred constraints) gbl_tvs
+             tau_tvs_plus = growThetaTyVars constraints zonked_tau_tvs
+       ; qtvs        <- quantifyTyVars mono_tvs tau_tvs_plus
+       ; constraints <- zonkTcThetaType constraints
+              -- quantifyTyVars turned some meta tyvars into
+              -- quantified skolems, so we have to zonk again
+
+       ; let theta     = filter (quantifyPred (mkVarSet qtvs)) constraints
+             min_theta = mkMinimalBySCs theta  -- See Note [Minimize by Superclasses]
+       ; traceTc "decideQuantification 2" (vcat [ppr constraints, ppr gbl_tvs, ppr mono_tvs
+                                                , ppr tau_tvs_plus, ppr qtvs, ppr min_theta])
+       ; return (qtvs, min_theta, False) }
 
 ------------------
 quantifyPred :: TyVarSet           -- Quantifying over these
              -> PredType -> Bool   -- True <=> quantify over this wanted
+-- This function decides whether a particular constraint shoudl be
+-- quantified over, given the type variables that are being quantified
 quantifyPred qtvs pred
   = case classifyPredType pred of
       ClassPred cls tys
          | isIPClass cls    -> True -- See note [Inheriting implicit parameters]
          | otherwise        -> tyVarsOfTypes tys `intersectsVarSet` qtvs
+
       EqPred NomEq ty1 ty2  -> quant_fun ty1 || quant_fun ty2
         -- representational equality is like a class constraint
       EqPred ReprEq ty1 ty2 -> tyVarsOfTypes [ty1, ty2] `intersectsVarSet` qtvs
+
       IrredPred ty          -> tyVarsOfType ty `intersectsVarSet` qtvs
       TuplePred {}          -> False
   where
-    -- Only quantify over (F tys ~ ty) if tys mentions a quantifed variable
-    -- In particular, quanitifying over (F Int ~ ty) is a bit like quantifying
-    -- over (Eq Int); the instance should kick in right here
+    -- See Note [Quantifying over equality constraints]
     quant_fun ty
       = case tcSplitTyConApp_maybe ty of
           Just (tc, tys) | isTypeFamilyTyCon tc
@@ -488,6 +514,19 @@ growThetaTyVars theta tvs
          pred_tvs = tyVarsOfType pred
 
 {-
+Note [Quantifying over equality constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Should we quantify over an equality constraint (s ~ t)?  In general, we don't.
+Doing so may simply postpone a type error from the function definition site to
+its call site.  (At worst, imagine (Int ~ Bool)).
+
+However, consider this
+         forall a. (F [a] ~ Int) => blah
+Should we quantify over the (F [a] ~ Int).  Perhaps yes, because at the call
+site we will know 'a', and perhaps we have instance  F [Bool] = Int.
+So we *do* quantify over a type-family equality where the arguments mention
+the quantified variables.
+
 Note [Growing the tau-tvs using constraints]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 (growThetaTyVars insts tvs) is the result of extending the set
diff --git a/testsuite/tests/indexed-types/should_fail/T2693.stderr b/testsuite/tests/indexed-types/should_fail/T2693.stderr
index 8fdb9985b6..0c6ea152a7 100644
--- a/testsuite/tests/indexed-types/should_fail/T2693.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T2693.stderr
@@ -1,38 +1,38 @@
-
-T2693.hs:11:7:
-    Couldn't match expected type ‘TFn a’ with actual type ‘TFn a0’
-    NB: ‘TFn’ is a type function, and may not be injective
-    The type variable ‘a0’ is ambiguous
-    When checking that ‘x’ has the inferred type
-      x :: forall a. TFn a
-    Probable cause: the inferred type is ambiguous
-    In the expression:
-      do { let Just x = ...;
-           let n = fst x + fst x;
-           return () }
-    In an equation for ‘f’:
-        f = do { let Just x = ...;
-                 let n = ...;
-                 return () }
-
-T2693.hs:19:15:
-    Couldn't match expected type ‘(a2, b0)’ with actual type ‘TFn a3’
-    The type variables ‘a2’, ‘b0’, ‘a3’ are ambiguous
-    Relevant bindings include n :: a2 (bound at T2693.hs:19:7)
-    In the first argument of ‘fst’, namely ‘x’
-    In the first argument of ‘(+)’, namely ‘fst x’
-
-T2693.hs:19:23:
-    Couldn't match expected type ‘(a4, a2)’ with actual type ‘TFn a5’
-    The type variables ‘a2’, ‘a4’, ‘a5’ are ambiguous
-    Relevant bindings include n :: a2 (bound at T2693.hs:19:7)
-    In the first argument of ‘snd’, namely ‘x’
-    In the second argument of ‘(+)’, namely ‘snd x’
-
-T2693.hs:29:20:
-    Couldn't match type ‘TFn a0’ with ‘PVR a1’
-    The type variables ‘a0’, ‘a1’ are ambiguous
-    Expected type: () -> Maybe (PVR a1)
-      Actual type: () -> Maybe (TFn a0)
-    In the first argument of ‘mapM’, namely ‘g’
-    In a stmt of a 'do' block: pvs <- mapM g undefined
+

+T2693.hs:11:7:

+    Couldn't match expected type ‘TFn a’ with actual type ‘TFn a0’

+    NB: ‘TFn’ is a type function, and may not be injective

+    The type variable ‘a0’ is ambiguous

+    When checking that ‘x’ has the inferred type

+      x :: forall a. TFn a

+    Probable cause: the inferred type is ambiguous

+    In the expression:

+      do { let Just x = ...;

+           let n = fst x + fst x;

+           return () }

+    In an equation for ‘f’:

+        f = do { let Just x = ...;

+                 let n = ...;

+                 return () }

+

+T2693.hs:19:15:

+    Couldn't match expected type ‘(a5, b0)’ with actual type ‘TFn a2’

+    The type variables ‘b0’, ‘a2’, ‘a5’ are ambiguous

+    Relevant bindings include n :: a5 (bound at T2693.hs:19:7)

+    In the first argument of ‘fst’, namely ‘x’

+    In the first argument of ‘(+)’, namely ‘fst x’

+

+T2693.hs:19:23:

+    Couldn't match expected type ‘(a3, a5)’ with actual type ‘TFn a4’

+    The type variables ‘a3’, ‘a4’, ‘a5’ are ambiguous

+    Relevant bindings include n :: a5 (bound at T2693.hs:19:7)

+    In the first argument of ‘snd’, namely ‘x’

+    In the second argument of ‘(+)’, namely ‘snd x’

+

+T2693.hs:29:20:

+    Couldn't match type ‘TFn a0’ with ‘PVR a1’

+    The type variables ‘a0’, ‘a1’ are ambiguous

+    Expected type: () -> Maybe (PVR a1)

+      Actual type: () -> Maybe (TFn a0)

+    In the first argument of ‘mapM’, namely ‘g’

+    In a stmt of a 'do' block: pvs <- mapM g undefined

diff --git a/testsuite/tests/typecheck/should_fail/T4921.stderr b/testsuite/tests/typecheck/should_fail/T4921.stderr
index c304b05c4b..a7267a26d3 100644
--- a/testsuite/tests/typecheck/should_fail/T4921.stderr
+++ b/testsuite/tests/typecheck/should_fail/T4921.stderr
@@ -1,19 +1,19 @@
-
-T4921.hs:10:9:
-    No instance for (C a0 b1) arising from a use of ‘f’
-    The type variables ‘a0’, ‘b1’ are ambiguous
-    Relevant bindings include x :: a0 (bound at T4921.hs:10:1)
-    Note: there is a potential instance available:
-      instance C Int Char -- Defined at T4921.hs:7:10
-    In the first argument of ‘fst’, namely ‘f’
-    In the expression: fst f
-    In an equation for ‘x’: x = fst f
-
-T4921.hs:12:9:
-    No instance for (C Int b0) arising from a use of ‘f’
-    The type variable ‘b0’ is ambiguous
-    Note: there is a potential instance available:
-      instance C Int Char -- Defined at T4921.hs:7:10
-    In the first argument of ‘fst’, namely ‘f’
-    In the expression: fst f :: Int
-    In an equation for ‘y’: y = fst f :: Int
+

+T4921.hs:10:9:

+    No instance for (C a0 b1) arising from a use of ‘f’

+    The type variables ‘b1’, ‘a0’ are ambiguous

+    Relevant bindings include x :: a0 (bound at T4921.hs:10:1)

+    Note: there is a potential instance available:

+      instance C Int Char -- Defined at T4921.hs:7:10

+    In the first argument of ‘fst’, namely ‘f’

+    In the expression: fst f

+    In an equation for ‘x’: x = fst f

+

+T4921.hs:12:9:

+    No instance for (C Int b0) arising from a use of ‘f’

+    The type variable ‘b0’ is ambiguous

+    Note: there is a potential instance available:

+      instance C Int Char -- Defined at T4921.hs:7:10

+    In the first argument of ‘fst’, namely ‘f’

+    In the expression: fst f :: Int

+    In an equation for ‘y’: y = fst f :: Int