Get the Untouchables level right in simplifyInfer
authorSimon Peyton Jones <simonpj@microsoft.com>
Wed, 29 Oct 2014 17:18:33 +0000 (17:18 +0000)
committerSimon Peyton Jones <simonpj@microsoft.com>
Tue, 4 Nov 2014 10:37:58 +0000 (10:37 +0000)
Previously we could get constraints in which the untouchables-level did not
strictly increase, which is one of the main invariants!

This patch also simplifies and modularises the tricky case of generalising
an inferred let-binding

compiler/typecheck/FunDeps.lhs
compiler/typecheck/TcBinds.lhs
compiler/typecheck/TcPatSyn.lhs
compiler/typecheck/TcSimplify.lhs
compiler/typecheck/TcTyClsDecls.lhs

index 283886e..36dc641 100644 (file)
@@ -15,7 +15,7 @@ module FunDeps (
         Equation(..), pprEquation,
         improveFromInstEnv, improveFromAnother,
         checkInstCoverage, checkFunDeps,
-        growThetaTyVars, pprFundeps
+        pprFundeps
     ) where
 
 #include "HsVersions.h"
@@ -41,46 +41,6 @@ import Data.Maybe       ( isJust )
 
 %************************************************************************
 %*                                                                      *
-\subsection{Close type variables}
-%*                                                                      *
-%************************************************************************
-
-Note [Growing the tau-tvs using constraints]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-(growThetaTyVars insts tvs) is the result of extending the set
-    of tyvars tvs using all conceivable links from pred
-
-E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e}
-Then growThetaTyVars preds tvs = {a,b,c}
-
-Notice that
-   growThetaTyVars is conservative       if v might be fixed by vs
-                                         => v `elem` grow(vs,C)
-
-\begin{code}
-growThetaTyVars :: ThetaType -> TyVarSet -> TyVarSet
--- See Note [Growing the tau-tvs using constraints]
-growThetaTyVars theta tvs
-  | null theta = tvs
-  | otherwise  = fixVarSet mk_next tvs
-  where
-    mk_next tvs = foldr grow_one tvs theta
-    grow_one pred tvs = growPredTyVars pred tvs `unionVarSet` tvs
-
-growPredTyVars :: PredType
-               -> TyVarSet      -- The set to extend
-               -> TyVarSet      -- TyVars of the predicate if it intersects the set,
-growPredTyVars pred tvs
-   | isIPPred pred                   = pred_tvs   -- Always quantify over implicit parameers
-   | pred_tvs `intersectsVarSet` tvs = pred_tvs
-   | otherwise                       = emptyVarSet
-  where
-    pred_tvs = tyVarsOfType pred
-\end{code}
-
-
-%************************************************************************
-%*                                                                      *
 \subsection{Generate equations from functional dependencies}
 %*                                                                      *
 %************************************************************************
index e96e0be..9f3576d 100644 (file)
@@ -591,14 +591,15 @@ tcPolyInfer
   -> [LHsBind Name]
   -> TcM (LHsBinds TcId, [TcId], TopLevelFlag)
 tcPolyInfer rec_tc prag_fn tc_sig_fn mono closed bind_list
-  = do { ((binds', mono_infos), wanted)
-             <- captureConstraints $
+  = do { (((binds', mono_infos), untch), wanted)
+             <- captureConstraints  $
+                captureUntouchables $
                 tcMonoBinds rec_tc tc_sig_fn LetLclBndr bind_list
 
        ; let name_taus = [(name, idType mono_id) | (name, _, mono_id) <- mono_infos]
        ; traceTc "simplifyInfer call" (ppr name_taus $$ ppr wanted)
        ; (qtvs, givens, mr_bites, ev_binds)
-                 <- simplifyInfer closed mono name_taus wanted
+                 <- simplifyInfer untch mono name_taus wanted
 
        ; theta   <- zonkTcThetaType (map evVarPred givens)
        ; exports <- checkNoErrs $ mapM (mkExport prag_fn qtvs theta) mono_infos
index 9b2b511..d27ab4f 100644 (file)
@@ -48,18 +48,23 @@ tcPatSynDecl PSB{ psb_id = lname@(L _ name), psb_args = details,
                   psb_def = lpat, psb_dir = dir }
   = do { traceTc "tcPatSynDecl {" $ ppr name $$ ppr lpat
        ; tcCheckPatSynPat lpat
-       ; pat_ty <- newFlexiTyVarTy openTypeKind
+       ; 
 
        ; let (arg_names, is_infix) = case details of
                  PrefixPatSyn names      -> (map unLoc names, False)
                  InfixPatSyn name1 name2 -> (map unLoc [name1, name2], True)
-       ; ((lpat', args), wanted) <- captureConstraints       $
-                                    tcPat PatSyn lpat pat_ty $
-                                    mapM tcLookupId arg_names
-       ; let named_taus = (name, pat_ty):map (\arg -> (getName arg, varType arg)) args
+       ; (((lpat', (args, pat_ty)), untch), wanted) 
+            <- captureConstraints       $
+               captureUntouchables      $
+               do { pat_ty <- newFlexiTyVarTy openTypeKind
+                  ; tcPat PatSyn lpat pat_ty $
+               do { args <- mapM tcLookupId arg_names
+                  ; return (args, pat_ty) } }
+
+       ; let named_taus = (name, pat_ty) : map (\arg -> (getName arg, varType arg)) args
 
        ; traceTc "tcPatSynDecl::wanted" (ppr named_taus $$ ppr wanted)
-       ; (qtvs, req_dicts, _mr_bites, ev_binds) <- simplifyInfer True False named_taus wanted
+       ; (qtvs, req_dicts, _mr_bites, ev_binds) <- simplifyInfer untch False named_taus wanted
 
        ; (ex_vars, prov_dicts) <- tcCollectEx lpat'
        ; let univ_tvs   = filter (not . (`elemVarSet` ex_vars)) qtvs
index d834763..e6da566 100644 (file)
@@ -2,7 +2,8 @@
 {-# LANGUAGE CPP #-}
 
 module TcSimplify(
-       simplifyInfer, quantifyPred,
+       simplifyInfer, 
+       quantifyPred, growThetaTyVars,
        simplifyAmbiguityCheck,
        simplifyDefault,
        simplifyRule, simplifyTop, simplifyInteractive,
@@ -20,8 +21,8 @@ import TcSMonad as TcS
 import TcInteract
 import Kind     ( isKind, defaultKind_maybe )
 import Inst
-import FunDeps  ( growThetaTyVars )
-import Type     ( classifyPredType, PredTree(..), getClassPredTys_maybe )
+import Type     ( classifyPredType, isIPClass, PredTree(..), getClassPredTys_maybe )
+import TyCon    ( isSynFamilyTyCon )
 import Class    ( Class )
 import Var
 import Unique
@@ -41,6 +42,7 @@ import BasicTypes       ( RuleName )
 import Outputable
 import FastString
 import TrieMap () -- DV: for now
+import Data.List( partition )
 \end{code}
 
 
@@ -236,8 +238,27 @@ simplifyDefault theta
 *                                                                                 *
 ***********************************************************************************
 
+Note [Inferring the type of a let-bound variable]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+   f x = rhs
+
+To infer f's type we do the following:
+ * Gather the constraints for the RHS with ambient level *one more than*
+   the current one.  This is done by the call
+        captureConstraints (captureUntouchables (tcMonoBinds...))
+   in TcBinds.tcPolyInfer
+
+ * Call simplifyInfer to simplify the constraints and decide what to
+   quantify over. We pass in the level used for the RHS constraints,
+   here called rhs_untch.
+
+This ensures that the implication constraint we generate, if any,
+has a strictly-increased level compared to the ambient level outside
+the let binding.
+
 \begin{code}
-simplifyInfer :: Bool
+simplifyInfer :: Untouchables          -- Used when generating the constraints
               -> Bool                  -- Apply monomorphism restriction
               -> [(Name, TcTauType)]   -- Variables to be generalised,
                                        -- and their tau-types
@@ -248,7 +269,7 @@ simplifyInfer :: Bool
                                     --   so the results type is not as general as
                                     --   it could be
                       TcEvBinds)    -- ... binding these evidence variables
-simplifyInfer _top_lvl apply_mr name_taus wanteds
+simplifyInfer rhs_untch apply_mr name_taus wanteds
   | isEmptyWC wanteds
   = do { gbl_tvs <- tcGetGlobalTyVars
        ; qtkvs <- quantifyTyVars gbl_tvs (tyVarsOfTypes (map snd name_taus))
@@ -258,7 +279,7 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
   | otherwise
   = do { traceTc "simplifyInfer {"  $ vcat
              [ ptext (sLit "binds =") <+> ppr name_taus
-             , ptext (sLit "closed =") <+> ppr _top_lvl
+             , ptext (sLit "rhs_untch =") <+> ppr rhs_untch
              , ptext (sLit "apply_mr =") <+> ppr apply_mr
              , ptext (sLit "(unzonked) wanted =") <+> ppr wanteds
              ]
@@ -278,10 +299,10 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
               -- bindings, so we can't just revert to the input
               -- constraint.
 
-       ; ev_binds_var <- newTcEvBinds
-       ; wanted_transformed_incl_derivs
-               <- solveWantedsTcMWithEvBinds ev_binds_var wanteds solve_wanteds
-                  -- Post: wanted_transformed_incl_derivs are zonked
+       ; ev_binds_var <- TcM.newTcEvBinds
+       ; wanted_transformed_incl_derivs <- setUntouchables rhs_untch $
+                                           runTcSWithEvBinds ev_binds_var (solveWanteds wanteds)
+       ; wanted_transformed_incl_derivs <- zonkWC wanted_transformed_incl_derivs
 
               -- Step 4) Candidates for quantification are an approximation of wanted_transformed
               -- NB: Already the fixpoint of any unifications that may have happened
@@ -289,83 +310,48 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
               -- to less polymorphic types, see Note [Default while Inferring]
 
        ; tc_lcl_env <- TcRnMonad.getLclEnv
-       ; let untch = tcl_untch tc_lcl_env
-             wanted_transformed = dropDerivedWC wanted_transformed_incl_derivs
+       ; null_ev_binds_var <- TcM.newTcEvBinds
+       ; let wanted_transformed = dropDerivedWC wanted_transformed_incl_derivs
        ; quant_pred_candidates   -- Fully zonked
            <- if insolubleWC wanted_transformed_incl_derivs
               then return []   -- See Note [Quantification with errors]
-                               -- NB: must include derived errors in this test, 
+                               -- NB: must include derived errors in this test,
                                --     hence "incl_derivs"
 
               else do { let quant_cand = approximateWC wanted_transformed
                             meta_tvs   = filter isMetaTyVar (varSetElems (tyVarsOfCts quant_cand))
                       ; gbl_tvs <- tcGetGlobalTyVars
-                      ; null_ev_binds_var <- newTcEvBinds
                             -- Miminise quant_cand.  We are not interested in any evidence
                             -- produced, because we are going to simplify wanted_transformed
                             -- again later. All we want here is the predicates over which to
-                            -- quantify.  
+                            -- quantify.
                             --
                             -- If any meta-tyvar unifications take place (unlikely), we'll
                             -- pick that up later.
 
-                      ; (flats, _insols) <- runTcSWithEvBinds null_ev_binds_var $
-                        do { mapM_ (promoteAndDefaultTyVar untch gbl_tvs) meta_tvs
-                                 -- See Note [Promote _and_ default when inferring]
-                           ; _implics <- solveInteract quant_cand
-                           ; getInertUnsolved }
 
-                      ; flats' <- zonkFlats null_ev_binds_var untch $
-                                  filterBag isWantedCt flats
-                           -- The quant_cand were already fully zonked, so this zonkFlats
-                           -- really only unflattens the flattening that solveInteract
-                           -- may have done (Trac #8889).  
-                           -- E.g. quant_cand = F a, where F :: * -> Constraint
-                           --      We'll flatten to   (alpha, F a ~ alpha)
-                           -- fail to make any further progress and must unflatten again 
+                      ; WC { wc_flat = flats }
+                           <- setUntouchables rhs_untch           $
+                              runTcSWithEvBinds null_ev_binds_var $
+                              do { mapM_ (promoteAndDefaultTyVar rhs_untch gbl_tvs) meta_tvs
+                                     -- See Note [Promote _and_ default when inferring]
+                                 ; solveFlatWanteds quant_cand }
 
-                      ; return (map ctPred $ bagToList flats') }
+                      ; return [ ctEvPred ev | ct <- bagToList flats
+                                             , let ev = ctEvidence ct
+                                             , isWanted ev ] }
 
        -- NB: quant_pred_candidates is already the fixpoint of any
        --     unifications that may have happened
-       ; gbl_tvs        <- tcGetGlobalTyVars
-       ; zonked_tau_tvs <- TcM.zonkTyVarsAndFV (tyVarsOfTypes (map snd name_taus))
-       ; let poly_qtvs = growThetaTyVars quant_pred_candidates zonked_tau_tvs
-                         `minusVarSet` gbl_tvs
-             pbound    = filter (quantifyPred poly_qtvs) quant_pred_candidates
 
-             -- Monomorphism restriction
-             constrained_tvs = tyVarsOfTypes pbound `unionVarSet` gbl_tvs
-             mr_bites        = apply_mr && not (null pbound)
+       ; zonked_tau_tvs <- TcM.zonkTyVarsAndFV (tyVarsOfTypes (map snd name_taus))
+       ; (mono_tvs, qtvs, bound, mr_bites) <- decideQuantification apply_mr quant_pred_candidates zonked_tau_tvs
 
-       ; (qtvs, bound) <- if mr_bites
-                          then do { qtvs <- quantifyTyVars constrained_tvs zonked_tau_tvs
-                                  ; return (qtvs, []) }
-                          else do { qtvs <- quantifyTyVars gbl_tvs poly_qtvs
-                                  ; return (qtvs, pbound) }
+       ; outer_untch <- TcRnMonad.getUntouchables
+       ; runTcSWithEvBinds null_ev_binds_var $  -- runTcS just to get the types right :-(
+         mapM_ (promoteTyVar outer_untch) (varSetElems (zonked_tau_tvs `intersectVarSet` mono_tvs))
 
-       ; traceTc "simplifyWithApprox" $
-         vcat [ ptext (sLit "quant_pred_candidates =") <+> ppr quant_pred_candidates
-              , ptext (sLit "gbl_tvs=") <+> ppr gbl_tvs
-              , ptext (sLit "zonked_tau_tvs=") <+> ppr zonked_tau_tvs
-              , ptext (sLit "pbound =") <+> ppr pbound
-              , ptext (sLit "bbound =") <+> ppr bound
-              , ptext (sLit "poly_qtvs =") <+> ppr poly_qtvs
-              , ptext (sLit "constrained_tvs =") <+> ppr constrained_tvs
-              , ptext (sLit "mr_bites =") <+> ppr mr_bites
-              , ptext (sLit "qtvs =") <+> ppr qtvs ]
-
-       ; if null qtvs && null bound
-         then do { traceTc "} simplifyInfer/no implication needed" empty
-                 ; emitConstraints wanted_transformed
-                    -- Includes insolubles (if -fdefer-type-errors)
-                    -- as well as flats and implications
-                 ; return ([], [], mr_bites, TcEvBinds ev_binds_var) }
-         else do
-
-      {     -- Step 7) Emit an implication
-            -- See Trac #9633 for an instructive example 
-         let minimal_flat_preds = mkMinimalBySCs bound
+       ; let minimal_flat_preds = mkMinimalBySCs bound
                   -- See Note [Minimize by Superclasses]
              skol_info = InferSkol [ (name, mkSigmaTy [] minimal_flat_preds ty)
                                    | (name, ty) <- name_taus ]
@@ -374,11 +360,9 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
                         -- tidied uniformly
 
        ; minimal_bound_ev_vars <- mapM TcM.newEvVar minimal_flat_preds
-       ; let implic = Implic { ic_untch    = pushUntouchables untch
+       ; let implic = Implic { ic_untch    = rhs_untch
                              , ic_skols    = qtvs
                              , ic_no_eqs   = False
-                             , ic_fsks     = []  -- wanted_tansformed arose only from solveWanteds
-                                                 -- hence no flatten-skolems (which come from givens)
                              , ic_given    = minimal_bound_ev_vars
                              , ic_wanted   = wanted_transformed
                              , ic_insol    = False
@@ -388,22 +372,125 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
        ; emitImplication implic
 
        ; traceTc "} simplifyInfer/produced residual implication for quantification" $
-             vcat [ ptext (sLit "implic =") <+> ppr implic
-                       -- ic_skols, ic_given give rest of result
-                  , ptext (sLit "qtvs =") <+> ppr qtvs
-                  , ptext (sLit "spb =") <+> ppr quant_pred_candidates
-                  , ptext (sLit "bound =") <+> ppr bound ]
+         vcat [ ptext (sLit "quant_pred_candidates =") <+> ppr quant_pred_candidates
+              , ptext (sLit "zonked_tau_tvs=") <+> ppr zonked_tau_tvs
+              , ptext (sLit "mono_tvs=") <+> ppr mono_tvs
+              , ptext (sLit "bound =") <+> ppr bound
+              , ptext (sLit "minimal_bound =") <+> vcat [ ppr v <+> dcolon <+> ppr (idType v) 
+                                                        | v <- minimal_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) } }
+                , mr_bites,  TcEvBinds ev_binds_var) } 
+
+\end{code}
+
+%************************************************************************
+%*                                                                      *
+                Quantification
+%*                                                                      *
+%************************************************************************
+
+Note [Deciding quantification]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+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
+    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
 
+    The result is poly_qtvs, which we will quantify over.
+
+  * Filter the constraints using quantifyPred and the poly_qtvs
+
+If the MR does apply, mono_tvs includes all the constrained tyvars,
+and the quantified constraints are empty.
+
+
+
+\begin{code}
+decideQuantification :: Bool -> [PredType] -> TcTyVarSet
+                     -> TcM ( TcTyVarSet      -- Do not quantify over these
+                            , [TcTyVar]       -- Do quantify over these
+                            , [PredType]      -- and these
+                            , 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 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
+       ; return (mono_tvs, 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
+       ; qtvs <- quantifyTyVars mono_tvs poly_qtvs
+       ; return (mono_tvs, qtvs, theta, False) }
+
+------------------
 quantifyPred :: TyVarSet           -- Quantifying over these
              -> PredType -> Bool   -- True <=> quantify over this wanted
 quantifyPred qtvs pred
-  | isIPPred pred = True  -- Note [Inheriting implicit parameters]
-  | otherwise     = tyVarsOfType pred `intersectsVarSet` qtvs
+  = case classifyPredType pred of
+      ClassPred cls tys
+         | isIPClass cls -> True  -- See note [Inheriting implicit parameters]
+         | otherwise     -> tyVarsOfTypes tys `intersectsVarSet` qtvs
+      EqPred ty1 ty2     -> quant_fun ty1 || quant_fun ty2
+      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
+    quant_fun ty
+      = case tcSplitTyConApp_maybe ty of
+          Just (tc, tys) | isSynFamilyTyCon tc
+                         -> tyVarsOfTypes tys `intersectsVarSet` qtvs
+          _ -> False
+
+------------------
+growThetaTyVars :: ThetaType -> TyVarSet -> TyVarSet
+-- See Note [Growing the tau-tvs using constraints]
+growThetaTyVars theta tvs
+  | null theta             = tvs
+  | isEmptyVarSet seed_tvs = tvs
+  | otherwise              = fixVarSet mk_next seed_tvs
+  where
+    seed_tvs = tvs `unionVarSet` tyVarsOfTypes ips
+    (ips, non_ips) = partition isIPPred theta
+                         -- See note [Inheriting implicit parameters]
+    mk_next tvs = foldr grow_one tvs non_ips
+    grow_one pred tvs
+       | pred_tvs `intersectsVarSet` tvs = tvs `unionVarSet` pred_tvs
+       | otherwise                       = tvs
+       where
+         pred_tvs = tyVarsOfType pred
 \end{code}
 
+Note [Growing the tau-tvs using constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+(growThetaTyVars insts tvs) is the result of extending the set
+    of tyvars tvs using all conceivable links from pred
+
+E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e}
+Then growThetaTyVars preds tvs = {a,b,c}
+
+Notice that
+   growThetaTyVars is conservative       if v might be fixed by vs
+                                         => v `elem` grow(vs,C)
+
 Note [Inheriting implicit parameters]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider this:
index a58d8e7..fd3c8f8 100644 (file)
@@ -28,8 +28,8 @@ import TcRnMonad
 import TcEnv
 import TcValidity
 import TcHsSyn
+import TcSimplify( growThetaTyVars )
 import TcBinds( tcRecSelBinds )
-import FunDeps( growThetaTyVars )
 import TcTyDecls
 import TcClassDcl
 import TcHsType