diff options
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/typecheck/TcCanonical.hs | 2 | ||||
| -rw-r--r-- | compiler/typecheck/TcFlatten.hs | 22 | ||||
| -rw-r--r-- | compiler/typecheck/TcInteract.hs | 24 |
3 files changed, 30 insertions, 18 deletions
diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs index 5232e77782..13aa8e724f 100644 --- a/compiler/typecheck/TcCanonical.hs +++ b/compiler/typecheck/TcCanonical.hs @@ -670,7 +670,7 @@ canEqTyVar ev swapped tv1 ty2 ps_ty2 -- ev :: tv ~ s2 = do { traceTcS "canEqTyVar" (ppr tv1 $$ ppr ty2 $$ ppr swapped) ; mb_yes <- flattenTyVarOuter ev tv1 ; case mb_yes of - Right (ty1, co1, _) -- co1 :: ty1 ~ tv1 + Right (ty1, co1) -- co1 :: ty1 ~ tv1 -> do { mb <- rewriteEqEvidence ev swapped ty1 ps_ty2 co1 (mkTcNomReflCo ps_ty2) ; traceTcS "canEqTyVar2" (vcat [ppr tv1, ppr ty2, ppr swapped, ppr ty1, diff --git a/compiler/typecheck/TcFlatten.hs b/compiler/typecheck/TcFlatten.hs index 10adc9432a..01d5a101ab 100644 --- a/compiler/typecheck/TcFlatten.hs +++ b/compiler/typecheck/TcFlatten.hs @@ -826,11 +826,7 @@ flattenTyVar fmode tv where ty' = mkTyVarTy tv' - Right (ty1, co1, True) -- No need to recurse - -> do { traceTcS "flattenTyVar2" (ppr tv $$ ppr ty1) - ; return (ty1, co1) } - - Right (ty1, co1, False) -- Recurse + Right (ty1, co1) -- Recurse -> do { (ty2, co2) <- flatten fmode ty1 ; traceTcS "flattenTyVar3" (ppr tv $$ ppr ty2) ; return (ty2, co2 `mkTcTransCo` co1) } @@ -838,14 +834,13 @@ flattenTyVar fmode tv flattenTyVarOuter, flattenTyVarFinal :: CtEvidence -> TcTyVar - -> TcS (Either TyVar (TcType, TcCoercion, Bool)) + -> TcS (Either TyVar (TcType, TcCoercion)) -- Look up the tyvar in -- a) the internal MetaTyVar box -- b) the tyvar binds -- c) the inerts --- Return (Left tv') if it is not found, tv' has a properly zonked kind --- (Right (ty, co, is_flat)) if found, with co :: ty ~ tv; --- is_flat says if the result is guaranteed flattened +-- Return (Left tv') if it is not found, tv' has a properly zonked kind +-- (Right (ty, co) if found, with co :: ty ~ tv; flattenTyVarOuter ctxt_ev tv | not (isTcTyVar tv) -- Happens when flatten under a (forall a. ty) @@ -854,7 +849,7 @@ flattenTyVarOuter ctxt_ev tv = do { mb_ty <- isFilledMetaTyVar_maybe tv ; case mb_ty of { Just ty -> do { traceTcS "Following filled tyvar" (ppr tv <+> equals <+> ppr ty) - ; return (Right (ty, mkTcNomReflCo ty, False)) } ; + ; return (Right (ty, mkTcNomReflCo ty)) } ; Nothing -> -- Try in the inert equalities @@ -866,7 +861,7 @@ flattenTyVarOuter ctxt_ev tv | CTyEqCan { cc_ev = ctev, cc_tyvar = tv, cc_rhs = rhs_ty } <- ct , eqCanRewrite ctev ctxt_ev -> do { traceTcS "Following inert tyvar" (ppr tv <+> equals <+> ppr rhs_ty $$ ppr ctev) - ; return (Right (rhs_ty, mkTcSymCo (ctEvCoercion ctev), True)) } + ; return (Right (rhs_ty, mkTcSymCo (ctEvCoercion ctev))) } -- NB: ct is Derived then (fe_ev fmode) must be also, hence -- we are not going to touch the returned coercion -- so ctEvCoercion is fine. @@ -884,9 +879,12 @@ flattenTyVarFinal ctxt_ev tv {- Note [Applying the inert substitution] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + -- NB: 8 Dec 14: These notes are now not correct + -- Need to rewrite then when matters have settled + The inert CTyEqCans (a ~ ty), inert_eqs, can be treated as a substitution, and indeed flattenTyVarOuter applies it to the type -being flattened. It has the following properties: +being flattened (recursively). This process should terminate. * 'a' is not in fvs(ty) * They are *inert*; that is the eqCanRewrite relation is everywhere false diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs index a9ed64acfb..c6e9fb6324 100644 --- a/compiler/typecheck/TcInteract.hs +++ b/compiler/typecheck/TcInteract.hs @@ -42,7 +42,7 @@ import Data.List( partition, foldl', deleteFirstsBy ) import VarEnv -import Control.Monad( when, unless, forM, foldM ) +import Control.Monad import Pair (Pair(..)) import Unique( hasKey ) import FastString ( sLit ) @@ -952,7 +952,9 @@ kickOutRewritable new_ev new_tv ; unless (isEmptyWorkList kicked_out) $ csTraceTcS $ hang (ptext (sLit "Kick out, tv =") <+> ppr new_tv) - 2 (ppr kicked_out) + 2 (vcat [ text "n-kicked =" <+> int (workListSize kicked_out) + , text "n-kept fun-eqs =" <+> int (sizeFunEqMap (inert_funeqs ics')) + , ppr kicked_out ]) ; return (workListSize kicked_out) } kick_out :: CtEvidence -> TcTyVar -> InertCans -> (WorkList, InertCans) @@ -987,8 +989,10 @@ kick_out new_ev new_tv (IC { inert_eqs = tv_eqs -- Kick out even insolubles; see Note [Kick out insolubles] kick_out_ct :: Ct -> Bool - kick_out_ct ct = eqCanRewrite new_ev (ctEvidence ct) - && new_tv `elemVarSet` tyVarsOfCt ct + kick_out_ct ct = kick_out_ctev (ctEvidence ct) + + kick_out_ctev ev = eqCanRewrite new_ev ev + && new_tv `elemVarSet` tyVarsOfType (ctEvPred ev) -- See Note [Kicking out inert constraints] kick_out_irred :: Ct -> Bool @@ -1003,7 +1007,17 @@ kick_out new_ev new_tv (IC { inert_eqs = tv_eqs [] -> acc_in (eq1:_) -> extendVarEnv acc_in (cc_tyvar eq1) eqs_in) where - (eqs_out, eqs_in) = partition kick_out_ct eqs + (eqs_out, eqs_in) = partition kick_out_eq eqs + + kick_out_eq (CTyEqCan { cc_tyvar = tv, cc_rhs = rhs_ty, cc_ev = ev }) + = eqCanRewrite new_ev ev + && (tv == new_tv + || (ev `eqCanRewrite` ev && new_tv `elemVarSet` tyVarsOfType rhs_ty) + || case getTyVar_maybe rhs_ty of { Just tv_r -> tv_r == new_tv; Nothing -> False }) + kick_out_eq ct = pprPanic "kick_out_eq" (ppr ct) + -- SLPJ new piece: Don't kick out a constraint unless it can rewrite itself, + -- If not, it can't rewrite anything else, so no point in + -- kicking it out {- Note [Kicking out inert constraints] |