X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcSimplify.lhs;h=b312d09f846b1d70b50fd038db1620a75d781e1f;hb=ef6d82a4e1d4ba4884c322be85cff291e017f0e6;hp=a4bf30f6916bd4c1263b4439c330870d4473790c;hpb=c80364f8e4681b34e974f5df36ecdacec7cd9cd8;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs index a4bf30f..b312d09 100644 --- a/compiler/typecheck/TcSimplify.lhs +++ b/compiler/typecheck/TcSimplify.lhs @@ -10,7 +10,6 @@ module TcSimplify( import HsSyn import TcRnMonad import TcErrors -import TcCanonical import TcMType import TcType import TcSMonad @@ -33,6 +32,7 @@ import BasicTypes ( RuleName ) import Data.List ( partition ) import Outputable import FastString +import Control.Monad ( unless ) \end{code} @@ -440,8 +440,7 @@ over implicit parameters. See the predicate isFreeWhenInferring. *********************************************************************************** When constructing evidence for superclasses in an instance declaration, - * we MUST have the "self" dictionary available, but - * we must NOT have its superclasses derived from "self" + * we MUST have the "self" dictionary available Moreover, we must *completely* solve the constraints right now, not wrap them in an implication constraint to solve later. Why? @@ -461,25 +460,85 @@ Now, if there is some *other* top-level constraint solved looking like foo :: Ord [Int] foo = scsel dCInt -we must not solve the (Ord [Int]) wanted from foo!! +we must not solve the (Ord [Int]) wanted from foo! + +Note [Dependencies in self dictionaries] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Moreover, notice that when solving for a superclass, we record the dependency of +self on the superclass. This is because this dependency is not evident in the +EvBind of the self dictionary, which only involves a call to a DFun. Example: + +class A a => C a +instance B a => C a + +When we check the instance declaration, we pass in a self dictionary that is merely + self = dfun b +But we will be asked to solve that from: + [Given] d : B a + [Derived] self : C a +We can show: + [Wanted] sc : A a +The problem is that self *depends* on the sc variable, but that is not apparent in +the binding self = dfun b. So we record the extra dependency, using the evidence bind: + EvBind self (EvDFunApp dfun [b] [b,sc]) +It is these dependencies that are the ''true'' dependencies in an EvDFunApp, and those +that we must chase in function isGoodRecEv (in TcSMonad) \begin{code} -simplifySuperClass :: EvVar -- The "self" dictionary - -> WantedConstraints - -> TcM () -simplifySuperClass self wanteds - = do { wanteds <- mapBagM zonkWanted wanteds - ; loc <- getCtLoc NoScSkol - ; ((unsolved_flats,unsolved_impls), frozen_errors, ev_binds) +simplifySuperClass :: [TyVar] + -> [EvVar] -- givens + -> EvVar -- the superclass we must solve for + -> EvBind -- the 'self' evidence bind + -> TcM TcEvBinds +-- Post: +-- ev_binds <- simplifySuperClasses tvs inst_givens sc_dict self_ev_bind +-- Then: +-- 1) ev_binds already contains self_ev_bind +-- 2) if successful then ev_binds contains binding for +-- the wanted superclass, sc_dict +simplifySuperClass tvs inst_givens sc_dict (EvBind self_dict self_ev) + = do { giv_loc <- getCtLoc InstSkol -- For the inst_givens + ; want_loc <- getCtLoc ScOrigin -- As wanted/derived (for the superclass and self) + ; lcl_env <- getLclTypeEnv + + -- Record the dependency of self_dict to sc_dict, see Note [Dependencies in self dictionaries] + ; let wanted = unitBag $ WcEvVar $ WantedEvVar sc_dict want_loc + self_ev_with_dep + = case self_ev of + EvDFunApp df tys insts deps -> EvDFunApp df tys insts (sc_dict:deps) + _ -> panic "Self-dictionary not EvDFunApp!" + + -- And solve for it + ; ((unsolved_flats, unsolved_implics), frozen_errors, ev_binds) <- runTcS SimplCheck NoUntouchables $ - do { can_self <- canGivens loc [self] - ; let inert = foldlBag updInertSet emptyInert can_self - -- No need for solveInteract; we know it's inert - - ; solveWanteds inert wanteds } - - ; ASSERT2( isEmptyBag ev_binds, ppr ev_binds ) - reportUnsolved (unsolved_flats,unsolved_impls) frozen_errors } + do { -- Record a binding for self_dict that *depends on sc_dict* + -- And canonicalise self_dict (which adds its superclasses) + -- with a Derived origin, which in turn triggers the + -- goodRecEv recursive-evidence check + ; setEvBind self_dict self_ev_with_dep + -- The rest is just like solveImplication + ; 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, + -- so that we get decent error messages + ; let implic = Implic { ic_untch = NoUntouchables + , ic_env = lcl_env + , ic_skols = mkVarSet tvs + , ic_given = inst_givens + , ic_wanted = mapBag WcEvVar unsolved_flats + , ic_scoped = panic "super1" + , ic_binds = panic "super2" + , ic_loc = giv_loc } + ; ASSERT (isEmptyBag unsolved_implics) -- Impossible to have any implications! + unless (isEmptyBag unsolved_flats) $ + reportUnsolved (emptyBag, unitBag implic) frozen_errors + + ; return (EvBinds ev_binds) } \end{code} @@ -644,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 }" $ @@ -665,73 +723,97 @@ 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 ] - - -- See Note [Preparing inert set for implications] - ; inert_for_implics <- solveInteract inert2 (makeGivens unsolved_flats) - ; traceTcS "solveWanteds: doing nested implications {" $ - vcat [ text "inerts_for_implics =" <+> ppr inert_for_implics - , text "implics =" <+> ppr implics ] - ; (implic_eqs, unsolved_implics) - <- flatMapBagPairM (solveImplication inert_for_implics) implics - - ; traceTcS "solveWanteds: done nested implications }" $ - vcat [ text "implic_eqs =" <+> ppr implic_eqs - , text "unsolved_implics =" <+> ppr unsolved_implics ] + , text "unsolved =" <+> ppr unsolved_cans ] + + -- Go inside each implication + ; (implic_eqs, unsolved_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 - } } - -solveImplication :: InertSet -- Given - -> Implication -- Wanted - -> TcS (Bag WantedEvVar, -- Unsolved unification var = type - Bag Implication) -- Unsolved rest (always empty or singleton) + -- some wanteds in the incoming can_ws + } + +solveNestedImplications :: InertSet -> Bag WantedEvVar -> Bag Implication + -> TcS (Bag WantedEvVar, Bag Implication) +solveNestedImplications inerts unsolved implics + | isEmptyBag implics + = return (emptyBag, emptyBag) + | otherwise + = do { -- See Note [Preparing inert set for implications] + traceTcS "solveWanteds: preparing inerts for implications {" empty + ; inert_for_implics <- solveInteract inerts (makeGivens unsolved) + ; traceTcS "}" empty + + ; traceTcS "solveWanteds: doing nested implications {" $ + vcat [ text "inerts_for_implics =" <+> ppr inert_for_implics + , text "implics =" <+> ppr implics ] + + ; let tcs_untouchables = filterVarSet isFlexiTcsTv $ + tyVarsOfInert inert_for_implics + -- See Note [Extra TcsTv untouchables] + ; (implic_eqs, unsolved_implics) + <- flatMapBagPairM (solveImplication tcs_untouchables inert_for_implics) implics + + ; traceTcS "solveWanteds: done nested implications }" $ + vcat [ text "implic_eqs =" <+> ppr implic_eqs + , text "unsolved_implics =" <+> ppr unsolved_implics ] + + ; return (implic_eqs, unsolved_implics) } + +solveImplication :: TcTyVarSet -- Untouchable TcS unification variables + -> InertSet -- Given + -> Implication -- Wanted + -> TcS (Bag WantedEvVar, -- Unsolved unification var = type + Bag Implication) -- Unsolved rest (always empty or singleton) -- Returns: -- 1. A bag of floatable wanted constraints, not mentioning any skolems, -- that are of the form unification var = type @@ -739,14 +821,14 @@ solveImplication :: InertSet -- Given -- 2. Maybe a unsolved implication, empty if entirely solved! -- -- Precondition: everything is zonked by now -solveImplication inert +solveImplication tcs_untouchables inert imp@(Implic { ic_untch = untch , ic_binds = ev_binds , ic_skols = skols , ic_given = givens , ic_wanted = wanteds , ic_loc = loc }) - = nestImplicTcS ev_binds untch $ + = nestImplicTcS ev_binds (untch, tcs_untouchables) $ recoverTcS (return (emptyBag, emptyBag)) $ -- Recover from nested failures. Even the top level is -- just a bunch of implications, so failing at the first @@ -754,8 +836,10 @@ solveImplication 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 @@ -825,9 +909,11 @@ Note [Preparing inert set for implications] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Before solving the nested implications, we convert any unsolved flat wanteds to givens, and add them to the inert set. Reasons: - a) In checking mode, suppresses unnecessary errors. We already have + + a) In checking mode, suppresses unnecessary errors. We already have on unsolved-wanted error; adding it to the givens prevents any consequential errors from showing uop + b) More importantly, in inference mode, we are going to quantify over this constraint, and we *don't* want to quantify over any constraints that are deducible from it. @@ -840,7 +926,34 @@ Hence the call to solveInteract. Example: We were not able to solve (a ~w [beta]) but we can't just assume it as given because the resulting set is not inert. Hence we have to do a -'solveInteract' step first +'solveInteract' step first. + +Note [Extra TcsTv untouchables] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Furthemore, we record the inert set simplifier-generated unification variables of the TcsTv +kind (such as variables from instance that have been applied, or unification flattens). These +variables must be passed to the implications as extra untouchable variables. Otherwise +we have the danger of double unifications. Example (from trac ticket #4494): + + (F Int ~ uf) /\ (forall a. C a => F Int ~ beta) + +In this example, beta is touchable inside the implication. The first solveInteract step +leaves 'uf' ununified. Then we move inside the implication where a new constraint + uf ~ beta +emerges. We may spontaneously solve it to get uf := beta, so the whole implication disappears +but when we pop out again we are left with (F Int ~ uf) which will be unified by our final +solveCTyFunEqs stage and uf will get unified *once more* to (F Int). + +The solution is to record the TcsTvs (i.e. the simplifier-generated unification variables) +that are generated when solving the flats, and make them untouchables for the nested +implication. In the example above uf would become untouchable, so beta would be forced to +be unified as beta := uf. + +NB: A consequence is that every simplifier-generated TcsTv variable that gets floated out + of an implication becomes now untouchable next time we go inside that implication to + solve any residual constraints. In effect, by floating an equality out of the implication + we are committing to have it solved in the outside. + \begin{code} @@ -893,7 +1006,7 @@ type FunEqBinds = [(TcTyVar,(TcType,CoVar,CtFlavor))] -- [... a -> (ta,...) ... b -> (tb,...) ... ] -- then 'ta' cannot mention 'b' -getSolvableCTyFunEqs :: Untouchables +getSolvableCTyFunEqs :: TcsUntouchables -> CanonicalCts -- Precondition: all wanteds -> (CanonicalCts, FunEqBinds) -- Postcondition: returns the unsolvables getSolvableCTyFunEqs untch cts @@ -985,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 @@ -1008,7 +1121,7 @@ applyDefaultingRules inert wanteds ; return (unionManyBags deflt_cts `unionBags` unionManyBags tv_cts) } ------------------ -defaultTyVar :: Untouchables -> TcTyVar -> TcS (Bag WantedEvVar) +defaultTyVar :: TcsUntouchables -> TcTyVar -> TcS (Bag WantedEvVar) -- defaultTyVar is used on any un-instantiated meta type variables to -- default the kind of ? and ?? etc to *. This is important to ensure -- that instance declarations match. For example consider @@ -1041,7 +1154,7 @@ findDefaultableGroups :: ( SimplContext , [Type] , (Bool,Bool) ) -- (Overloaded strings, extended default rules) - -> Untouchables -- Untouchable + -> TcsUntouchables -- Untouchable -> CanonicalCts -- Unsolved -> [[(CanonicalCt,TcTyVar)]] findDefaultableGroups (ctxt, default_tys, (ovl_strings, extended_defaults)) @@ -1101,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 @@ -1121,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!"