X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcSimplify.lhs;h=f6b9ed23ffc37509215c31dd7b5291e3194d534f;hb=cd450d41e84c2bf09bb9c3a646c7408eb2c2d772;hp=0e7acdd6761197638aaa013a88f2d4069865d9fe;hpb=c1e6031c54cda2c6f9fc107eb6cb04ab490f1fef;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs index 0e7acdd..f6b9ed2 100644 --- a/compiler/typecheck/TcSimplify.lhs +++ b/compiler/typecheck/TcSimplify.lhs @@ -18,6 +18,9 @@ import TcInteract import Inst import Var import VarSet +import VarEnv +import TypeRep + import Name import NameEnv ( emptyNameEnv ) import Bag @@ -185,7 +188,7 @@ simplifyInfer :: Bool -- Apply monomorphism restriction TcEvBinds) -- ... binding these evidence variables simplifyInfer apply_mr tau_tvs wanted | isEmptyBag wanted -- Trivial case is quite common - = do { zonked_tau_tvs <- zonkTcTyVarsAndFV (varSetElems tau_tvs) + = do { zonked_tau_tvs <- zonkTcTyVarsAndFV tau_tvs ; gbl_tvs <- tcGetGlobalTyVars -- Already zonked ; qtvs <- zonkQuantifiedTyVars (varSetElems (zonked_tau_tvs `minusVarSet` gbl_tvs)) ; return (qtvs, [], emptyTcEvBinds) } @@ -198,26 +201,50 @@ simplifyInfer apply_mr tau_tvs wanted , ptext (sLit "tau_tvs =") <+> ppr tau_tvs ] - ; (simple_wanted, tc_binds) - <- simplifyAsMuchAsPossible SimplInfer zonked_wanted + -- Make a guess at the quantified type variables + -- Then split the constraints on the baisis of those tyvars + -- to avoid unnecessarily simplifying a class constraint + -- See Note [Avoid unecessary constraint simplification] + ; gbl_tvs <- tcGetGlobalTyVars + ; zonked_tau_tvs <- zonkTcTyVarsAndFV tau_tvs + ; let proto_qtvs = growWanteds gbl_tvs zonked_wanted $ + zonked_tau_tvs `minusVarSet` gbl_tvs + (perhaps_bound, surely_free) + = partitionBag (quantifyMeWC proto_qtvs) zonked_wanted + + ; emitConstraints surely_free + ; traceTc "sinf" $ vcat + [ ptext (sLit "perhaps_bound =") <+> ppr perhaps_bound + , ptext (sLit "surely_free =") <+> ppr surely_free + ] + + -- Now simplify the possibly-bound constraints + ; (simplified_perhaps_bound, tc_binds) + <- simplifyAsMuchAsPossible SimplInfer perhaps_bound + -- Sigh: must re-zonk because because simplifyAsMuchAsPossible + -- may have done some unification ; gbl_tvs <- tcGetGlobalTyVars - ; zonked_tau_tvs <- zonkTcTyVarsAndFV (varSetElems tau_tvs) - ; zonked_simples <- mapBagM zonkWantedEvVar simple_wanted - ; let qtvs = findQuantifiedTyVars apply_mr zonked_simples zonked_tau_tvs gbl_tvs - (bound, free) | apply_mr = (emptyBag, zonked_simples) - | otherwise = partitionBag (quantifyMe qtvs) zonked_simples + ; zonked_tau_tvs <- zonkTcTyVarsAndFV tau_tvs + ; zonked_simples <- mapBagM zonkWantedEvVar simplified_perhaps_bound + ; let init_tvs = zonked_tau_tvs `minusVarSet` gbl_tvs + mr_qtvs = init_tvs `minusVarSet` constrained_tvs + constrained_tvs = tyVarsOfWantedEvVars zonked_simples + qtvs = growWantedEVs gbl_tvs zonked_simples init_tvs + (final_qtvs, (bound, free)) + | apply_mr = (mr_qtvs, (emptyBag, zonked_simples)) + | otherwise = (qtvs, partitionBag (quantifyMe qtvs) zonked_simples) ; traceTc "end simplifyInfer }" $ vcat [ ptext (sLit "apply_mr =") <+> ppr apply_mr , text "wanted = " <+> ppr zonked_wanted - , text "qtvs = " <+> ppr qtvs + , text "qtvs = " <+> ppr final_qtvs , text "free = " <+> ppr free , text "bound = " <+> ppr bound ] -- Turn the quantified meta-type variables into real type variables ; emitConstraints (mapBag WcEvVar free) - ; qtvs_to_return <- zonkQuantifiedTyVars (varSetElems qtvs) + ; qtvs_to_return <- zonkQuantifiedTyVars (varSetElems final_qtvs) ; let bound_evvars = bagToList $ mapBag wantedEvVarToVar bound ; return (qtvs_to_return, bound_evvars, EvBinds tc_binds) } @@ -227,23 +254,22 @@ simplifyAsMuchAsPossible :: SimplContext -> WantedConstraints -- We use this function when inferring the type of a function -- The wanted constraints are already zonked simplifyAsMuchAsPossible ctxt wanteds - = do { let untch = emptyVarSet + = do { let untch = NoUntouchables -- We allow ourselves to unify environment -- variables; hence *no untouchables* - ; ((unsolved_flats, unsolved_implics), ev_binds) + ; ((unsolved_flats, unsolved_implics), frozen_errors, ev_binds) <- runTcS ctxt untch $ simplifyApproxLoop 0 wanteds -- Report any errors - ; reportUnsolved (emptyBag, unsolved_implics) + ; reportUnsolved (emptyBag, unsolved_implics) frozen_errors - ; let final_wanted_evvars = mapBag deCanonicaliseWanted unsolved_flats - ; return (final_wanted_evvars, ev_binds) } + ; return (unsolved_flats, ev_binds) } where simplifyApproxLoop :: Int -> WantedConstraints - -> TcS (CanonicalCts, Bag Implication) + -> TcS (Bag WantedEvVar, Bag Implication) simplifyApproxLoop n wanteds | n > 10 = pprPanic "simplifyApproxLoop loops!" (ppr n <+> text "iterations") @@ -255,9 +281,10 @@ simplifyAsMuchAsPossible ctxt wanteds ; let (extra_flats, thiner_unsolved_implics) = approximateImplications unsolved_implics unsolved - = mkWantedConstraints unsolved_flats thiner_unsolved_implics + = Bag.mapBag WcEvVar unsolved_flats `unionBags` + Bag.mapBag WcImplic thiner_unsolved_implics - ;-- If no new work was produced then we are done with simplifyApproxLoop + ; -- If no new work was produced then we are done with simplifyApproxLoop if isEmptyBag extra_flats then do { traceTcS "simplifyApproxLoopRes" (vcat [ ptext (sLit "Wanted = ") <+> ppr wanteds @@ -308,25 +335,37 @@ approximateImplications impls \end{code} \begin{code} -findQuantifiedTyVars :: Bool -- Apply the MR - -> Bag WantedEvVar -- Simplified constraints from RHS - -> TyVarSet -- Free in tau-type of definition - -> TyVarSet -- Free in the envt - -> TyVarSet -- Quantify over these - -findQuantifiedTyVars apply_mr wanteds tau_tvs gbl_tvs - | isEmptyBag wanteds = init_tvs - | apply_mr = init_tvs `minusVarSet` constrained_tvs - | otherwise = fixVarSet mk_next init_tvs +growWantedEVs :: TyVarSet -> Bag WantedEvVar -> TyVarSet -> TyVarSet +growWanteds :: TyVarSet -> Bag WantedConstraint -> TyVarSet -> TyVarSet +growWanteds gbl_tvs ws tvs + | isEmptyBag ws = tvs + | otherwise = fixVarSet (\tvs -> foldrBag (growWanted gbl_tvs) tvs ws) tvs +growWantedEVs gbl_tvs ws tvs + | isEmptyBag ws = tvs + | otherwise = fixVarSet (\tvs -> foldrBag (growWantedEV gbl_tvs) tvs ws) tvs + +growEvVar :: TyVarSet -> EvVar -> TyVarSet -> TyVarSet +growWantedEV :: TyVarSet -> WantedEvVar -> TyVarSet -> TyVarSet +growWanted :: TyVarSet -> WantedConstraint -> TyVarSet -> TyVarSet +-- (growX gbls wanted tvs) grows a seed 'tvs' against the +-- X-constraint 'wanted', nuking the 'gbls' at each stage + +growEvVar gbl_tvs ev tvs + = tvs `unionVarSet` (ev_tvs `minusVarSet` gbl_tvs) where - init_tvs = tau_tvs `minusVarSet` gbl_tvs - mk_next tvs = foldrBag grow_one tvs wanteds + ev_tvs = growPredTyVars (evVarPred ev) tvs - grow_one wev tvs = tvs `unionVarSet` (extra_tvs `minusVarSet` gbl_tvs) - where - extra_tvs = growPredTyVars (wantedEvVarPred wev) tvs +growWantedEV gbl_tvs wev tvs = growEvVar gbl_tvs (wantedEvVarToVar wev) tvs - constrained_tvs = tyVarsOfWantedEvVars wanteds +growWanted gbl_tvs (WcEvVar wev) tvs + = growWantedEV gbl_tvs wev tvs +growWanted gbl_tvs (WcImplic implic) tvs + = foldrBag (growWanted inner_gbl_tvs) + (foldr (growEvVar inner_gbl_tvs) tvs (ic_given implic)) + -- Must grow over inner givens too + (ic_wanted implic) + where + inner_gbl_tvs = gbl_tvs `unionVarSet` ic_skols implic -------------------- quantifyMe :: TyVarSet -- Quantifying over these @@ -337,8 +376,37 @@ quantifyMe qtvs wev | otherwise = tyVarsOfPred pred `intersectsVarSet` qtvs where pred = wantedEvVarPred wev + +quantifyMeWC :: TyVarSet -> WantedConstraint -> Bool +-- False => we can *definitely* float the WantedConstraint out +quantifyMeWC qtvs (WcImplic implic) + = (tyVarsOfEvVars (ic_given implic) `intersectsVarSet` inner_qtvs) + || anyBag (quantifyMeWC inner_qtvs) (ic_wanted implic) + where + inner_qtvs = qtvs `minusVarSet` ic_skols implic + +quantifyMeWC qtvs (WcEvVar wev) + = quantifyMe qtvs wev \end{code} +Note [Avoid unecessary constraint simplification] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +When inferring the type of a let-binding, with simplifyInfer, +try to avoid unnecessariliy simplifying class constraints. +Doing so aids sharing, but it also helps with delicate +situations like + instance C t => C [t] where .. + f :: C [t] => .... + f x = let g y = ...(constraint C [t])... + in ... +When inferring a type for 'g', we don't want to apply the +instance decl, because then we can't satisfy (C t). So we +just notice that g isn't quantified over 't' and partition +the contraints before simplifying. + +This only half-works, but then let-generalisation only half-works. + + Note [Inheriting implicit parameters] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider this: @@ -402,16 +470,16 @@ simplifySuperClass :: EvVar -- The "self" dictionary simplifySuperClass self wanteds = do { wanteds <- mapBagM zonkWanted wanteds ; loc <- getCtLoc NoScSkol - ; (unsolved, ev_binds) - <- runTcS SimplCheck emptyVarSet $ + ; ((unsolved_flats,unsolved_impls), frozen_errors, ev_binds) + <- runTcS SimplCheck NoUntouchables $ do { can_self <- canGivens loc [self] - ; let inert = foldlBag extendInertSet emptyInert can_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 } + reportUnsolved (unsolved_flats,unsolved_impls) frozen_errors } \end{code} @@ -512,7 +580,7 @@ simplifyRule name tv_bndrs lhs_wanted rhs_wanted ; rhs_binds_var@(EvBindsVar evb_ref _) <- newTcEvBinds ; loc <- getCtLoc (RuleSkol name) ; rhs_binds1 <- simplifyCheck SimplCheck $ unitBag $ WcImplic $ - Implic { ic_env_tvs = emptyVarSet -- No untouchables + Implic { ic_untch = NoUntouchables , ic_env = emptyNameEnv , ic_skols = mkVarSet tv_bndrs , ic_scoped = panic "emitImplication" @@ -556,21 +624,22 @@ simplifyCheck ctxt wanteds ; traceTc "simplifyCheck {" (vcat [ ptext (sLit "wanted =") <+> ppr wanteds ]) - ; (unsolved, ev_binds) <- runTcS ctxt emptyVarSet $ - solveWanteds emptyInert wanteds + ; (unsolved, frozen_errors, ev_binds) + <- runTcS ctxt NoUntouchables $ solveWanteds emptyInert wanteds ; traceTc "simplifyCheck }" $ ptext (sLit "unsolved =") <+> ppr unsolved - ; reportUnsolved unsolved + ; reportUnsolved unsolved frozen_errors ; return ev_binds } ---------------- -solveWanteds :: InertSet -- Given - -> WantedConstraints -- Wanted - -> TcS (CanonicalCts, -- Unsolved flats - Bag Implication) -- Unsolved implications +solveWanteds :: InertSet -- Given + -> WantedConstraints -- Wanted + -> TcS (Bag WantedEvVar, -- Unsolved constraints, but unflattened, this is why + -- they are WantedConstraints and not CanonicalCts + Bag Implication) -- Unsolved implications -- solveWanteds iterates when it is able to float equalities -- out of one or more of the implications solveWanteds inert wanteds @@ -580,60 +649,110 @@ solveWanteds inert wanteds vcat [ text "wanteds =" <+> ppr wanteds , text "inert =" <+> ppr inert ] ; (unsolved_flats, unsolved_implics) - <- simpl_loop 1 can_flats implic_wanteds + <- simpl_loop 1 inert can_flats implic_wanteds + ; bb <- getTcEvBindsBag + ; tb <- getTcSTyBindsMap ; traceTcS "solveWanteds }" $ - vcat [ text "wanteds =" <+> ppr wanteds - , text "unsolved_flats =" <+> ppr unsolved_flats - , text "unsolved_implics =" <+> ppr unsolved_implics ] - ; return (unsolved_flats, unsolved_implics) } + vcat [ text "unsolved_flats =" <+> ppr unsolved_flats + , text "unsolved_implics =" <+> ppr unsolved_implics + , text "current evbinds =" <+> vcat (map ppr (varEnvElts bb)) + , text "current tybinds =" <+> vcat (map ppr (varEnvElts tb)) + ] + + ; solveCTyFunEqs unsolved_flats unsolved_implics + -- See Note [Solving Family Equations] + } where simpl_loop :: Int + -> InertSet -> CanonicalCts -- May inlude givens (in the recursive call) -> Bag Implication -> TcS (CanonicalCts, Bag Implication) - simpl_loop n can_ws implics + simpl_loop n inert can_ws implics | n>10 = trace "solveWanteds: loop" $ -- Always bleat do { traceTcS "solveWanteds: loop" (ppr inert) -- Bleat more informatively ; return (can_ws, implics) } | otherwise - = do { inert1 <- solveInteract inert can_ws + = do { traceTcS "solveWanteds: simpl_loop start {" $ + vcat [ text "n =" <+> ppr n + , text "can_ws =" <+> ppr can_ws + , text "implics =" <+> ppr implics + , text "inert =" <+> ppr inert ] + ; inert1 <- solveInteract inert can_ws ; let (inert2, unsolved_flats) = extractUnsolved inert1 - ; traceTcS "solveWanteds/done flats" $ + -- 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) + -- Go inside each implication ; (implic_eqs, unsolved_implics) - <- flatMapBagPairM (solveImplication inert_for_implics) implics + <- solveNestedImplications inert2 unsolved_flats implics - -- Apply defaulting rules if and only if there + -- 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 + ; traceTcS "solveWanteds: simpl_loop end }" $ + vcat [ text "final_eqs =" <+> ppr final_eqs + , text "unsolved_flats =" <+> ppr unsolved_flats + , text "unsolved_implics =" <+> ppr unsolved_implics ] + ; if isEmptyBag final_eqs then return (unsolved_flats, unsolved_implics) else - do { traceTcS ("solveWanteds iteration " ++ show n) $ vcat - [ text "floated_unsolved_eqs =" <+> ppr final_eqs - , text "unsolved_implics = " <+> ppr unsolved_implics ] - ; simpl_loop (n+1) - (unsolved_flats `unionBags` final_eqs) - unsolved_implics - } } - -solveImplication :: InertSet -- Given - -> Implication -- Wanted - -> TcS (CanonicalCts, -- Unsolved unification var = type - Bag Implication) -- Unsolved rest (always empty or singleton) + 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 + -- 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 + } + } + +solveNestedImplications :: InertSet -> CanonicalCts -> 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 @@ -641,14 +760,18 @@ solveImplication :: InertSet -- Given -- 2. Maybe a unsolved implication, empty if entirely solved! -- -- Precondition: everything is zonked by now -solveImplication inert - imp@(Implic { ic_env_tvs = untch - , ic_binds = ev_binds - , ic_skols = skols - , ic_given = givens +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 $ + , ic_loc = loc }) + = 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 + -- one is bad do { traceTcS "solveImplication {" (ppr imp) -- Solve flat givens @@ -660,7 +783,8 @@ solveImplication inert ; let (res_flat_free, res_flat_bound) = floatEqualities skols givens unsolved_flats - unsolved = mkWantedConstraints res_flat_bound unsolved_implics + unsolved = Bag.mapBag WcEvVar res_flat_bound `unionBags` + Bag.mapBag WcImplic unsolved_implics ; traceTcS "solveImplication end }" $ vcat [ text "res_flat_free =" <+> ppr res_flat_free @@ -672,26 +796,61 @@ solveImplication inert ; return (res_flat_free, res_bag) } -floatEqualities :: TcTyVarSet -> [EvVar] - -> CanonicalCts -> (CanonicalCts, CanonicalCts) +floatEqualities :: TcTyVarSet -> [EvVar] + -> Bag WantedEvVar -> (Bag WantedEvVar, Bag WantedEvVar) + -- The CanonicalCts will be floated out to be used later, whereas + -- the remaining WantedEvVars will remain inside the implication. floatEqualities skols can_given wanteds | hasEqualities can_given = (emptyBag, wanteds) - | otherwise = partitionBag is_floatable wanteds - where - is_floatable :: CanonicalCt -> Bool - is_floatable (CTyEqCan { cc_tyvar = tv, cc_rhs = ty }) - | isMetaTyVar tv || isMetaTyVarTy ty - = skols `disjointVarSet` (extendVarSet (tyVarsOfType ty) tv) - is_floatable _ = False + -- Note [Float Equalities out of Implications] + | otherwise = partitionBag is_floatable wanteds + where is_floatable :: WantedEvVar -> Bool + is_floatable (WantedEvVar cv _) + | isCoVar cv = skols `disjointVarSet` predTvs_under_fsks (coVarPred cv) + is_floatable _wv = False + + tvs_under_fsks :: Type -> TyVarSet + -- ^ NB: for type synonyms tvs_under_fsks does /not/ expand the synonym + tvs_under_fsks (TyVarTy tv) + | not (isTcTyVar tv) = unitVarSet tv + | FlatSkol ty <- tcTyVarDetails tv = tvs_under_fsks ty + | otherwise = unitVarSet tv + tvs_under_fsks (TyConApp _ tys) = unionVarSets (map tvs_under_fsks tys) + tvs_under_fsks (PredTy sty) = predTvs_under_fsks sty + tvs_under_fsks (FunTy arg res) = tvs_under_fsks arg `unionVarSet` tvs_under_fsks res + tvs_under_fsks (AppTy fun arg) = tvs_under_fsks fun `unionVarSet` tvs_under_fsks arg + tvs_under_fsks (ForAllTy tv ty) -- The kind of a coercion binder + -- can mention type variables! + | isTyVar tv = inner_tvs `delVarSet` tv + | otherwise {- Coercion -} = -- ASSERT( not (tv `elemVarSet` inner_tvs) ) + inner_tvs `unionVarSet` tvs_under_fsks (tyVarKind tv) + where + inner_tvs = tvs_under_fsks ty + + predTvs_under_fsks :: PredType -> TyVarSet + predTvs_under_fsks (IParam _ ty) = tvs_under_fsks ty + predTvs_under_fsks (ClassP _ tys) = unionVarSets (map tvs_under_fsks tys) + predTvs_under_fsks (EqPred ty1 ty2) = tvs_under_fsks ty1 `unionVarSet` tvs_under_fsks ty2 + + + + \end{code} +Note [Float Equalities out of Implications] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We want to float equalities out of vanilla existentials, but *not* out +of GADT pattern matches. + 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. @@ -704,7 +863,139 @@ 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} + +solveCTyFunEqs :: CanonicalCts -> Bag Implication -> TcS (Bag WantedEvVar, Bag Implication) +-- Default equalities (F xi ~ alpha) by setting (alpha := F xi), whenever possible +-- See Note [Solving Family Equations] +-- Returns: a bunch of unsolved constraints from the original CanonicalCts and implications +-- where the newly generated equalities (alpha := F xi) have been substituted through. +solveCTyFunEqs cts implics + = do { untch <- getUntouchables + ; let (unsolved_can_cts, funeq_bnds) = getSolvableCTyFunEqs untch cts + ; traceTcS "defaultCTyFunEqs" (vcat [text "Trying to default family equations:" + , ppr funeq_bnds + ]) + ; mapM_ solve_one funeq_bnds + + -- Apply the substitution through to eliminate the flatten + -- unification variables we substituted both in the unsolved flats and implics + ; let final_unsolved + = Bag.mapBag (subst_wevar funeq_bnds . deCanonicaliseWanted) unsolved_can_cts + final_implics + = Bag.mapBag (subst_impl funeq_bnds) implics + + ; return (final_unsolved, final_implics) } + + where solve_one (tv,(ty,cv,fl)) + | not (typeKind ty `isSubKind` tyVarKind tv) + = addErrorTcS KindError fl (mkTyVarTy tv) ty + -- Must do a small kind check since TcCanonical invariants + -- on family equations only impose compatibility, not subkinding + | otherwise = setWantedTyBind tv ty >> setWantedCoBind cv ty + + subst_wanted :: FunEqBinds -> WantedConstraint -> WantedConstraint + subst_wanted funeq_bnds (WcEvVar wv) = WcEvVar (subst_wevar funeq_bnds wv) + subst_wanted funeq_bnds (WcImplic impl) = WcImplic (subst_impl funeq_bnds impl) + + subst_wevar :: FunEqBinds -> WantedEvVar -> WantedEvVar + subst_wevar funeq_bnds (WantedEvVar v loc) + = let orig_ty = varType v + new_ty = substFunEqBnds funeq_bnds orig_ty + in WantedEvVar (setVarType v new_ty) loc + + subst_impl :: FunEqBinds -> Implication -> Implication + subst_impl funeq_bnds impl@(Implic { ic_wanted = ws }) + = impl { ic_wanted = Bag.mapBag (subst_wanted funeq_bnds) ws } + + +type FunEqBinds = [(TcTyVar,(TcType,CoVar,CtFlavor))] +-- Invariant: if it contains: +-- [... a -> (ta,...) ... b -> (tb,...) ... ] +-- then 'ta' cannot mention 'b' + +getSolvableCTyFunEqs :: TcsUntouchables + -> CanonicalCts -- Precondition: all wanteds + -> (CanonicalCts, FunEqBinds) -- Postcondition: returns the unsolvables +getSolvableCTyFunEqs untch cts + = Bag.foldlBag dflt_funeq (emptyCCan, []) cts + where dflt_funeq (cts_in, extra_binds) ct@(CFunEqCan { cc_id = cv + , cc_flavor = fl + , cc_fun = tc + , cc_tyargs = xis + , cc_rhs = xi }) + | Just tv <- tcGetTyVar_maybe xi + , isTouchableMetaTyVar_InRange untch tv -- If RHS is a touchable unif. variable + , Nothing <- lookup tv extra_binds -- or in extra_binds + -- See Note [Solving Family Equations], Point 1 + = ASSERT ( isWanted fl ) + let ty_orig = mkTyConApp tc xis + ty_bind = substFunEqBnds extra_binds ty_orig + in if tv `elemVarSet` tyVarsOfType ty_bind + then (cts_in `extendCCans` ct, extra_binds) + -- See Note [Solving Family Equations], Point 2 + else (cts_in, (tv,(ty_bind,cv,fl)):extra_binds) + -- Postcondition met because extra_binds is already applied to ty_bind + + dflt_funeq (cts_in, extra_binds) ct = (cts_in `extendCCans` ct, extra_binds) + +substFunEqBnds :: FunEqBinds -> TcType -> TcType +substFunEqBnds bnds ty + = foldr (\(x,(t,_cv,_fl)) xy -> substTyWith [x] [t] xy) ty bnds + -- foldr works because of the FunEqBinds invariant + + +\end{code} + +Note [Solving Family Equations] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +After we are done with simplification we may be left with constraints of the form: + [Wanted] F xis ~ beta +If 'beta' is a touchable unification variable not already bound in the TyBinds +then we'd like to create a binding for it, effectively "defaulting" it to be 'F xis'. + +When is it ok to do so? + 1) 'beta' must not already be defaulted to something. Example: + + [Wanted] F Int ~ beta <~ Will default [beta := F Int] + [Wanted] F Char ~ beta <~ Already defaulted, can't default again. We + have to report this as unsolved. + + 2) However, we must still do an occurs check when defaulting (F xis ~ beta), to + set [beta := F xis] only if beta is not among the free variables of xis. + + 3) Notice that 'beta' can't be bound in ty binds already because we rewrite RHS + of type family equations. See Inert Set invariants in TcInteract. + ********************************************************************************* * * @@ -744,8 +1035,8 @@ Basic plan behind applyDefaulting rules: \begin{code} applyDefaultingRules :: InertSet - -> CanonicalCts -- All wanteds - -> TcS CanonicalCts + -> CanonicalCts -- All wanteds + -> TcS (Bag WantedEvVar) -- All wanteds again! -- Return some *extra* givens, which express the -- type-class-default choice @@ -753,21 +1044,21 @@ applyDefaultingRules inert wanteds | isEmptyBag wanteds = return emptyBag | otherwise - = do { untch <- getUntouchablesTcS + = do { untch <- getUntouchables ; tv_cts <- mapM (defaultTyVar untch) $ - varSetElems (tyVarsOfCanonicals wanteds) + varSetElems (tyVarsOfCDicts wanteds) ; info@(_, default_tys, _) <- getDefaultInfo ; let groups = findDefaultableGroups info untch wanteds - ; deflt_cts <- mapM (disambigGroup default_tys untch inert) groups + ; deflt_cts <- mapM (disambigGroup default_tys inert) groups ; traceTcS "deflt2" (vcat [ text "Tyvar defaults =" <+> ppr tv_cts , text "Type defaults =" <+> ppr deflt_cts]) - ; return (unionManyBags deflt_cts `andCCan` unionManyBags tv_cts) } + ; return (unionManyBags deflt_cts `unionBags` unionManyBags tv_cts) } ------------------ -defaultTyVar :: TcTyVarSet -> TcTyVar -> TcS CanonicalCts +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 @@ -783,20 +1074,13 @@ defaultTyVar :: TcTyVarSet -> TcTyVar -> TcS CanonicalCts -- whatever, because the type-class defaulting rules have yet to run. defaultTyVar untch the_tv - | isMetaTyVar the_tv - , not (the_tv `elemVarSet` untch) + | isTouchableMetaTyVar_InRange untch the_tv , not (k `eqKind` default_k) - = do { (ev, better_ty) <- TcSMonad.newKindConstraint (mkTyVarTy the_tv) default_k + = do { ev <- TcSMonad.newKindConstraint the_tv default_k ; let loc = CtLoc DefaultOrigin (getSrcSpan the_tv) [] -- Yuk - -- 'DefaultOrigin' is strictly the declaration, but it's convenient - wanted_eq = CTyEqCan { cc_id = ev - , cc_flavor = Wanted loc - , cc_tyvar = the_tv - , cc_rhs = better_ty } - ; return (unitBag wanted_eq) } - + ; return (unitBag (WantedEvVar ev loc)) } | otherwise - = return emptyCCan -- The common case + = return emptyBag -- The common case where k = tyVarKind the_tv default_k = defaultKind k @@ -807,7 +1091,7 @@ findDefaultableGroups :: ( SimplContext , [Type] , (Bool,Bool) ) -- (Overloaded strings, extended default rules) - -> TcTyVarSet -- Untouchable + -> TcsUntouchables -- Untouchable -> CanonicalCts -- Unsolved -> [[(CanonicalCt,TcTyVar)]] findDefaultableGroups (ctxt, default_tys, (ovl_strings, extended_defaults)) @@ -834,7 +1118,7 @@ findDefaultableGroups (ctxt, default_tys, (ovl_strings, extended_defaults)) is_defaultable_group ds@((_,tv):_) = isTyConableTyVar tv -- Note [Avoiding spurious errors] && not (tv `elemVarSet` bad_tvs) - && not (tv `elemVarSet` untch) -- Non untouchable + && isTouchableMetaTyVar_InRange untch tv && defaultable_classes [cc_class cc | (cc,_) <- ds] is_defaultable_group [] = panic "defaultable_group" @@ -856,43 +1140,44 @@ findDefaultableGroups (ctxt, default_tys, (ovl_strings, extended_defaults)) ------------------------------ disambigGroup :: [Type] -- The default types - -> TcTyVarSet -- Untouchables -> InertSet -- Given inert -> [(CanonicalCt, TcTyVar)] -- All classes of the form (C a) -- sharing same type variable - -> TcS CanonicalCts + -> TcS (Bag WantedEvVar) -disambigGroup [] _inert _untch _grp +disambigGroup [] _inert _grp = return emptyBag -disambigGroup (default_ty:default_tys) untch inert group +disambigGroup (default_ty:default_tys) inert group = do { traceTcS "disambigGroup" (ppr group $$ ppr default_ty) - ; ev <- newGivOrDerCoVar (mkTyVarTy the_tv) default_ty default_ty -- Refl - -- We know this equality is canonical, - -- so we directly construct it as such - ; let given_eq = CTyEqCan { cc_id = ev - , cc_flavor = mkGivenFlavor (cc_flavor the_ct) UnkSkol - , cc_tyvar = the_tv - , cc_rhs = default_ty } - - ; success <- tryTcS (extendVarSet untch the_tv) $ - do { given_inert <- solveOne inert given_eq - ; final_inert <- solveInteract given_inert (listToBag wanteds) - ; let (_, unsolved) = extractUnsolved final_inert - ; return (isEmptyBag unsolved) } + ; 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 + ; return (isEmptyBag unsolved && isEmptyBag errs) } ; case success of - True -> -- Success: record the type variable binding, and return - do { setWantedTyBind the_tv default_ty - ; wrapWarnTcS $ warnDefaulting wanted_ev_vars default_ty - ; traceTcS "disambigGoup succeeded" (ppr default_ty) - ; return (unitBag given_eq) } + True -> -- Success: record the type variable binding, and return + do { wrapWarnTcS $ warnDefaulting wanted_ev_vars default_ty + ; traceTcS "disambigGroup succeeded" (ppr default_ty) + ; return (unitBag $ WantedEvVar ev ct_loc) } False -> -- Failure: try with the next type - do { traceTcS "disambigGoup succeeded" (ppr default_ty) - ; disambigGroup default_tys untch inert group } } + do { traceTcS "disambigGroup failed, will try other default types" (ppr default_ty) + ; disambigGroup default_tys inert group } } where ((the_ct,the_tv):_) = group wanteds = map fst group wanted_ev_vars = map deCanonicaliseWanted wanteds + + get_ct_loc (Wanted l) = l + get_ct_loc _ = panic "Asked to disambiguate given or derived!" + + \end{code} Note [Avoiding spurious errors] @@ -907,5 +1192,3 @@ that g isn't polymorphic enough; but then we get another one when dealing with the (Num a) context arising from f's definition; we try to unify a with Int (to default it), but find that it's already been unified with the rigid variable from g's type sig - -