Moved canonicalisation inside solveInteract
authordimitris@microsoft.com <unknown>
Thu, 9 Dec 2010 14:12:15 +0000 (14:12 +0000)
committerdimitris@microsoft.com <unknown>
Thu, 9 Dec 2010 14:12:15 +0000 (14:12 +0000)
Moreover canonicalisation now is "clever", i.e. it never canonicalizes a class
constraint if it can already discharge it from some other inert or previously
encountered constraints. See Note [Avoiding the superclass explosion]

compiler/typecheck/TcInteract.lhs
compiler/typecheck/TcSMonad.lhs
compiler/typecheck/TcSimplify.lhs

index e1ea65f..aeb78d8 100644 (file)
@@ -187,6 +187,8 @@ foldISEqCts k z IS { inert_eqs = eqs }
   = Bag.foldlBag k z eqs
 
 extractUnsolved :: InertSet -> (InertSet, CanonicalCts)
+-- Postcondition: the canonical cts returnd are the very same as the 
+-- WantedEvVars in their canonical form. 
 extractUnsolved is@(IS {inert_eqs = eqs}) 
   = let is_solved  = is { inert_eqs    = solved_eqs
                         , inert_dicts  = solved_dicts
@@ -397,11 +399,62 @@ React with (F Int ~ b) ==> IR Stop True []    -- after substituting we re-canoni
 -- returning an extended inert set.
 --
 -- See Note [Touchables and givens].
-solveInteract :: InertSet -> CanonicalCts -> TcS InertSet
+solveInteract :: InertSet -> Bag (CtFlavor,EvVar) -> TcS InertSet
 solveInteract inert ws 
   = do { dyn_flags <- getDynFlags
-       ; solveInteractWithDepth (ctxtStkDepth dyn_flags,0,[]) inert ws
-       }
+       ; can_ws    <- foldlBagM (tryPreSolveAndCanon inert) emptyCCan ws
+       ; solveInteractWithDepth (ctxtStkDepth dyn_flags,0,[]) inert can_ws }
+
+tryPreSolveAndCanon :: InertSet -> CanonicalCts -> (CtFlavor, EvVar) -> TcS CanonicalCts
+-- Checks if this constraint can be immediately solved from a constraint in the 
+-- inert set or in the previously encountered CanonicalCts and only then  
+-- canonicalise it. See Note [Avoiding the superclass explosion]
+tryPreSolveAndCanon is cts_acc (fl,ev_var)
+  | ClassP clas tys <- evVarPred ev_var 
+  = do { let (relevant_inert_dicts,_) = getRelevantCts clas (inert_dicts is) 
+       ; b <- dischargeFromCans (cts_acc `unionBags` relevant_inert_dicts)
+                                (fl,ev_var,clas,tys)
+       ; extra_cts <- if b then return emptyCCan else mkCanonical fl ev_var 
+       ; return (cts_acc `unionBags` extra_cts) }
+  | otherwise 
+  = do { extra_cts <- mkCanonical fl ev_var
+       ; return (cts_acc `unionBags` extra_cts) }
+
+dischargeFromCans :: CanonicalCts -> (CtFlavor,EvVar,Class,[Type]) -> TcS Bool
+dischargeFromCans cans (fl,ev,clas,tys) 
+  = Bag.foldlBagM discharge_ct False cans 
+  where discharge_ct :: Bool -> CanonicalCt -> TcS Bool 
+        discharge_ct True _ct = return True
+        discharge_ct False (CDictCan { cc_id = ev1, cc_flavor = fl1
+                                     , cc_class = clas1, cc_tyargs = tys1 })
+          | clas1 == clas
+          , (and $ zipWith tcEqType tys tys1)
+          , fl1 `canSolve` fl 
+          = setEvBind ev (EvId ev1) >> return True
+        discharge_ct False _ct = return False
+\end{code}
+
+Note [Avoiding the superclass explosion] 
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
+
+Consider the example: 
+  f = [(0,1,0,1,0)] 
+We have 5 wanted (Num alpha) constraints. If we simply try to canonicalize and add them
+in our worklist, we will also get all of their superclasses as Derived, hence we will 
+have an inert set that contains 5*n constraints, where n is the number of superclasses 
+of of Num. That is bad for the additional reason that we keep *all* the Derived, even 
+for identical class constraints (for reasons related to recursive dictionaries). 
+
+Instead, what we do with tryPreSolveAndCanon, is when we encounter a new constraint, 
+such as the second (Num alpha) above we very quickly see if it can be immediately 
+discharged by a class constraint in our inert set or the previous canonicals. If so, 
+we add nothing to the returned canonical constraints.
+
+For our particular example this will reduce the size of the inert set that we use from 
+5*n to just n. And hence the number of all possible interactions that we have to look 
+through is significantly smaller!
+
+\begin{code}
 solveOne :: InertSet -> WorkItem -> TcS InertSet 
 solveOne inerts workItem 
   = do { dyn_flags <- getDynFlags
index 7b7a9f4..0920a8b 100644 (file)
@@ -181,8 +181,9 @@ data CanonicalCt
 compatKind :: Kind -> Kind -> Bool 
 compatKind k1 k2 = k1 `isSubKind` k2 || k2 `isSubKind` k1 
 
-makeGivens :: CanonicalCts -> CanonicalCts
-makeGivens = mapBag (\ct -> ct { cc_flavor = mkGivenFlavor (cc_flavor ct) UnkSkol })
+makeGivens :: Bag WantedEvVar -> Bag (CtFlavor,EvVar) 
+makeGivens = mapBag (\(WantedEvVar ev wloc) -> (mkGivenFlavor (Wanted wloc) UnkSkol, ev))
+-- ct { cc_flavor = mkGivenFlavor (cc_flavor ct) UnkSkol })
           -- The UnkSkol doesn't matter because these givens are
           -- not contradictory (else we'd have rejected them already)
 
index 0da5eec..b312d09 100644 (file)
@@ -10,7 +10,6 @@ module TcSimplify(
 import HsSyn          
 import TcRnMonad
 import TcErrors
-import TcCanonical
 import TcMType
 import TcType 
 import TcSMonad 
@@ -518,12 +517,11 @@ simplifySuperClass tvs inst_givens sc_dict (EvBind self_dict self_ev)
                        -- with a Derived origin, which in turn triggers the
                        -- goodRecEv recursive-evidence check
                    ; setEvBind self_dict self_ev_with_dep
-                   ; can_selfs <- mkCanonical  (Derived want_loc DerSelf) self_dict
-
                        -- The rest is just like solveImplication
-                   ; can_inst_givens <- mkCanonicals (Given giv_loc) inst_givens
-                   ; inert           <- solveInteract emptyInert $
-                                        can_inst_givens `andCCan` can_selfs
+                   ; let cts = mapBag (\d -> (Given giv_loc, d)) (listToBag inst_givens)
+                                          `snocBag` (Derived want_loc DerSelf, self_dict)
+                   ; inert           <- solveInteract emptyInert cts
+                                        
                    ; solveWanteds inert wanted }
 
        -- For error reporting, conjure up a fake implication,
@@ -705,12 +703,11 @@ solveWanteds :: InertSet        -- Given
 -- out of one or more of the implications 
 solveWanteds inert wanteds
   = do { let (flat_wanteds, implic_wanteds) = splitWanteds wanteds
-       ; can_flats <- canWanteds $ bagToList flat_wanteds
        ; traceTcS "solveWanteds {" $
                  vcat [ text "wanteds =" <+> ppr wanteds
                       , text "inert =" <+> ppr inert ]
        ; (unsolved_flats, unsolved_implics) 
-               <- simpl_loop 1 inert can_flats implic_wanteds
+               <- simpl_loop 1 inert flat_wanteds implic_wanteds
        ; bb <- getTcEvBindsBag
        ; tb <- getTcSTyBindsMap
        ; traceTcS "solveWanteds }" $
@@ -726,63 +723,66 @@ solveWanteds inert wanteds
   where
     simpl_loop :: Int 
                -> InertSet 
-               -> CanonicalCts -- May inlude givens (in the recursive call)
+               -> Bag WantedEvVar
                -> Bag Implication
                -> TcS (CanonicalCts, Bag Implication)
-    simpl_loop n inert can_ws implics
+    simpl_loop n inert work_items implics
       | n>10
-      = trace "solveWanteds: loop" $   -- Always bleat
+      = trace "solveWanteds: loop" $                   -- Always bleat
         do { traceTcS "solveWanteds: loop" (ppr inert)  -- Bleat more informatively
-           ; return (can_ws, implics) }
+
+             -- We don't want to call the canonicalizer on those wanted ev vars
+             -- so try one last time to solveInteract them 
+           ; inert1 <- solveInteract inert $ 
+                       mapBag (\(WantedEvVar ev wloc) -> (Wanted wloc, ev)) work_items
+           ; let (_, unsolved_cans) = extractUnsolved inert1
+           ; return (unsolved_cans, implics) }
 
       | otherwise
       = do { traceTcS "solveWanteds: simpl_loop start {" $
                  vcat [ text "n =" <+> ppr n
-                      , text "can_ws =" <+> ppr can_ws
+                      , text "work_items =" <+> ppr work_items
                       , text "implics =" <+> ppr implics
                       , text "inert =" <+> ppr inert ]
-           ; inert1 <- solveInteract inert can_ws
-           ; let (inert2, unsolved_flats) = extractUnsolved inert1
+           ; inert1 <- solveInteract inert $ 
+                       mapBag (\(WantedEvVar ev wloc) -> (Wanted wloc,ev)) work_items
+           ; let (inert2, unsolved_cans) = extractUnsolved inert1
+                 unsolved_wevvars 
+                     = mapBag (\ct -> WantedEvVar (cc_id ct) (getWantedLoc ct)) unsolved_cans
 
            -- NB: Importantly, inerts2 may contain *more* givens than inert 
            -- because of having solved equalities from can_ws 
            ; traceTcS "solveWanteds: done flats"  $
                  vcat [ text "inerts =" <+> ppr inert2
-                      , text "unsolved =" <+> ppr unsolved_flats ]
+                      , text "unsolved =" <+> ppr unsolved_cans ]
 
                 -- Go inside each implication
            ; (implic_eqs, unsolved_implics) 
-               <- solveNestedImplications inert2 unsolved_flats implics
+               <- solveNestedImplications inert2 unsolved_wevvars implics
 
                 -- Apply defaulting rules if and only if there
                -- no floated equalities.  If there are, they may
                -- solve the remaining wanteds, so don't do defaulting.
            ; final_eqs <- if not (isEmptyBag implic_eqs)
                          then return implic_eqs
-                          else applyDefaultingRules inert2 unsolved_flats
-                                     
-               -- default_eqs are *givens*, so simpl_loop may 
-               -- recurse with givens in the argument
+                          else applyDefaultingRules inert2 unsolved_cans
 
            ; traceTcS "solveWanteds: simpl_loop end }" $
                  vcat [ text "final_eqs =" <+> ppr final_eqs
-                      , text "unsolved_flats =" <+> ppr unsolved_flats
+                      , text "unsolved_flats =" <+> ppr unsolved_cans
                       , text "unsolved_implics =" <+> ppr unsolved_implics ]
 
            ; if isEmptyBag final_eqs then
-                 return (unsolved_flats, unsolved_implics)
+                 return (unsolved_cans, unsolved_implics)
              else 
-                 do { can_final_eqs <- canWanteds (Bag.bagToList final_eqs)
-                       -- final eqs is *just* a bunch of WantedEvVars
-                    ; simpl_loop (n+1) inert2 
-                          (can_final_eqs `andCCan` unsolved_flats) unsolved_implics 
+                 simpl_loop (n+1) inert2 -- final_eqs are just some WantedEvVars
+                            (final_eqs `unionBags` unsolved_wevvars) unsolved_implics
                        -- Important: reiterate with inert2, not plainly inert
                        -- because inert2 may contain more givens, as the result of solving
-                       -- some wanteds in the incoming can_ws 
-                     }       
+                       -- some wanteds in the incoming can_ws
            }
 
-solveNestedImplications :: InertSet -> CanonicalCts -> Bag Implication
+solveNestedImplications :: InertSet -> Bag WantedEvVar -> Bag Implication
                         -> TcS (Bag WantedEvVar, Bag Implication)
 solveNestedImplications inerts unsolved implics
   | isEmptyBag implics
@@ -836,8 +836,10 @@ solveImplication tcs_untouchables inert
     do { traceTcS "solveImplication {" (ppr imp) 
 
          -- Solve flat givens
-       ; can_givens  <- canGivens loc givens
-       ; given_inert <- solveInteract inert can_givens
+--       ; can_givens  <- canGivens loc givens
+--       ; let given_fl = Given loc
+       ; given_inert <- solveInteract inert $ 
+                        mapBag (\c -> (Given loc,c)) (listToBag givens)
 
          -- Simplify the wanteds
        ; (unsolved_flats, unsolved_implics) <- solveWanteds given_inert wanteds
@@ -1096,7 +1098,7 @@ Basic plan behind applyDefaulting rules:
 
 \begin{code}
 applyDefaultingRules :: InertSet
-                     -> CanonicalCts          -- All wanteds
+                     -> CanonicalCts        -- All wanteds
                      -> TcS (Bag WantedEvVar)  -- All wanteds again!  
 -- Return some *extra* givens, which express the 
 -- type-class-default choice
@@ -1212,16 +1214,12 @@ disambigGroup (default_ty:default_tys) inert group
   = do { traceTcS "disambigGroup" (ppr group $$ ppr default_ty)
        ; let ct_loc = get_ct_loc (cc_flavor the_ct) 
        ; ev <- TcSMonad.newWantedCoVar (mkTyVarTy the_tv) default_ty
-       ; let wanted_eq = CTyEqCan { cc_id = ev
-                                  , cc_flavor = Wanted ct_loc
-                                  , cc_tyvar  = the_tv 
-                                  , cc_rhs    = default_ty }
        ; success <- tryTcS $ 
-                   do { final_inert <- solveInteract inert(listToBag $ wanted_eq:wanteds)
-                      ; let (_, unsolved) = extractUnsolved final_inert                                    
-                       ; errs <- getTcSErrorsBag 
+                   do { final_inert <- solveInteract inert $
+                                        consBag (Wanted ct_loc, ev) wanted_to_solve
+                      ; let (_, unsolved) = extractUnsolved final_inert                         
+                       ; errs <- getTcSErrorsBag
                       ; return (isEmptyBag unsolved && isEmptyBag errs) }
-
        ; case success of
            True  ->  -- Success: record the type variable binding, and return
                     do { wrapWarnTcS $ warnDefaulting wanted_ev_vars default_ty
@@ -1232,8 +1230,10 @@ disambigGroup (default_ty:default_tys) inert group
                        ; disambigGroup default_tys inert group } }
   where
     ((the_ct,the_tv):_) = group
-    wanteds = map fst group
-    wanted_ev_vars = map deCanonicaliseWanted wanteds
+    wanteds             = map fst group
+    wanted_ev_vars      = map deCanonicaliseWanted wanteds
+    wanted_to_solve     = listToBag $ 
+                          map (\(WantedEvVar ev wloc) -> (Wanted wloc,ev)) wanted_ev_vars
 
     get_ct_loc (Wanted l) = l
     get_ct_loc _ = panic "Asked  to disambiguate given or derived!"