Commit 4aa0a2d8 authored by dimitris's avatar dimitris

Reintroducing isReflCo optimization: invariant

that evVarPred.cc_id must be equal to ctPred
needs no longer be true.
parent 36f8cabe
......@@ -158,6 +158,8 @@ by subst, they remain canonical and hence we will not attempt to solve them from
other hand they did get rewritten and are now non-canonical they will still not match the EvBinds, so we
are again good.
\begin{code}
-- Top-level canonicalization
......@@ -254,11 +256,13 @@ canIP d fl v nm ty
= -- Note [Canonical implicit parameter constraints] explains why it's
-- possible in principle to not flatten, but since flattening applies
-- the inert substitution we choose to flatten anyway.
do { (xi,co,no_flattening) <- flatten d fl (mkIPPred nm ty)
do { (xi,co) <- flatten d fl (mkIPPred nm ty)
; let no_flattening = isReflCo co
; if no_flattening then
continueWith $ CIPCan { cc_id = v, cc_flavor = fl
, cc_ip_nm = nm, cc_ip_ty = ty
, cc_depth = d }
let IPPred _ xi_in = classifyPredType xi
in continueWith $ CIPCan { cc_id = v, cc_flavor = fl
, cc_ip_nm = nm, cc_ip_ty = xi_in
, cc_depth = d }
else do { evc <- newEvVar fl xi
; let v_new = evc_the_evvar evc
IPPred _ ip_xi = classifyPredType xi
......@@ -296,10 +300,11 @@ canClass :: SubGoalDepth -- Depth
-- Note: Does NOT add superclasses, but the /caller/ is responsible for adding them!
canClass d fl v cls tys
= do { -- sctx <- getTcSContext
; (xis, cos, no_flattening) <- flattenMany d fl tys
; (xis, cos) <- flattenMany d fl tys
; let co = mkTyConAppCo (classTyCon cls) cos
xi = mkClassPred cls xis
; let no_flattening = all isReflCo cos
-- No flattening, continue with canonical
; if no_flattening then
continueWith $ CDictCan { cc_id = v, cc_flavor = fl
......@@ -455,7 +460,11 @@ canIrred :: SubGoalDepth -- Depth
-- Precondition: ty not a tuple and no other evidence form
canIrred d fl v ty
= do { traceTcS "can_pred" (text "IrredPred = " <+> ppr ty)
; (xi,co,no_flattening) <- flatten d fl ty -- co :: xi ~ ty
; (xi,co) <- flatten d fl ty -- co :: xi ~ ty
; let no_flattening = xi `eqType` ty
-- In this particular case it is not safe to
-- say 'isReflCo' because the new constraint may
-- be reducible!
; if no_flattening then
continueWith $ CIrredEvCan { cc_id = v, cc_flavor = fl
, cc_ty = xi, cc_depth = d }
......@@ -527,66 +536,64 @@ unexpanded synonym.
-- Flatten a bunch of types all at once.
flattenMany :: SubGoalDepth -- Depth
-> CtFlavor -> [Type] -> TcS ([Xi], [LCoercion],Bool)
-> CtFlavor -> [Type] -> TcS ([Xi], [LCoercion])
-- Coercions :: Xi ~ Type
-- Returns True iff (no flattening happened)
flattenMany d ctxt tys
= -- pprTrace "flattenMany" empty $
go tys
where go [] = return ([],[],True)
go (ty:tys) = do { (xi,co,flag_ty) <- flatten d ctxt ty
; (xis,cos,flag_tys) <- go tys
; return (xi:xis,co:cos,flag_ty && flag_tys) }
where go [] = return ([],[])
go (ty:tys) = do { (xi,co) <- flatten d ctxt ty
; (xis,cos) <- go tys
; return (xi:xis,co:cos) }
-- Flatten a type to get rid of type function applications, returning
-- the new type-function-free type, and a collection of new equality
-- constraints. See Note [Flattening] for more detail.
flatten :: SubGoalDepth -- Depth
-> CtFlavor -> TcType -> TcS (Xi, LCoercion,Bool)
-> CtFlavor -> TcType -> TcS (Xi, LCoercion)
-- Postcondition: Coercion :: Xi ~ TcType
-- Boolean flag to return: True iff (no flattening happened)
-- Notice the returned flag is NOT equal to isReflCo of the returned coercion
-- because of spontaneously solved equalities, whose evidence IS refl, but the
-- types are substituted!
flatten d ctxt ty
| Just ty' <- tcView ty
= do { (xi, co, no_flattening) <- flatten d ctxt ty'
-- Preserve type synonyms if possible
; if no_flattening
then return (ty, mkReflCo ty,no_flattening) -- Importantly, not xi!
else return (xi,co,no_flattening)
}
= do { (xi, co) <- flatten d ctxt ty'
; return (xi,co) }
-- The following is tedious to do:
-- Preserve type synonyms if possible
-- ; if no_flattening
-- then return (xi, mkReflCo xi,no_flattening) -- Importantly, not xi!
-- else return (xi,co,no_flattening)
-- }
flatten _d ctxt v@(TyVarTy _)
= do { ieqs <- getInertEqs
; let co = liftInertEqsTy ieqs ctxt v -- co :: v ~ xi
new_ty = pSnd (liftedCoercionKind co)
no_substitution = new_ty `eqType` v -- Very cheap
; return (new_ty, mkSymCo co,no_substitution) } -- return xi ~ v
; return (new_ty, mkSymCo co) } -- return xi ~ v
flatten d ctxt (AppTy ty1 ty2)
= do { (xi1,co1,no_flat1) <- flatten d ctxt ty1
; (xi2,co2,no_flat2) <- flatten d ctxt ty2
; return (mkAppTy xi1 xi2, mkAppCo co1 co2,no_flat1 && no_flat2) }
= do { (xi1,co1) <- flatten d ctxt ty1
; (xi2,co2) <- flatten d ctxt ty2
; return (mkAppTy xi1 xi2, mkAppCo co1 co2) }
flatten d ctxt (FunTy ty1 ty2)
= do { (xi1,co1,no_flat1) <- flatten d ctxt ty1
; (xi2,co2,no_flat2) <- flatten d ctxt ty2
; return (mkFunTy xi1 xi2, mkFunCo co1 co2, no_flat1 && no_flat2) }
= do { (xi1,co1) <- flatten d ctxt ty1
; (xi2,co2) <- flatten d ctxt ty2
; return (mkFunTy xi1 xi2, mkFunCo co1 co2) }
flatten d fl (TyConApp tc tys)
-- For a normal type constructor or data family application, we just
-- recursively flatten the arguments.
| not (isSynFamilyTyCon tc)
= do { (xis,cos,no_flattening) <- flattenMany d fl tys
; return (mkTyConApp tc xis, mkTyConAppCo tc cos,no_flattening) }
= do { (xis,cos) <- flattenMany d fl tys
; return (mkTyConApp tc xis, mkTyConAppCo tc cos) }
-- Otherwise, it's a type function application, and we have to
-- flatten it away as well, and generate a new given equality constraint
-- between the application and a newly generated flattening skolem variable.
| otherwise
= ASSERT( tyConArity tc <= length tys ) -- Type functions are saturated
do { (xis, cos, _no_flattening) <- flattenMany d fl tys
do { (xis, cos) <- flattenMany d fl tys
; let (xi_args, xi_rest) = splitAt (tyConArity tc) xis
-- The type function might be *over* saturated
-- in which case the remaining arguments should
......@@ -637,7 +644,7 @@ flatten d fl (TyConApp tc tys)
-- cf Trac #5655
, foldl AppCo (mkSymCo ret_co `mkTransCo` mkTyConAppCo tc cos_args)
cos_rest
, False ) } -- no_flattening is False since we ARE flattening here!
) }
flatten d ctxt ty@(ForAllTy {})
......@@ -645,8 +652,8 @@ flatten d ctxt ty@(ForAllTy {})
-- applications inside the forall involve the bound type variables.
= do { let (tvs, rho) = splitForAllTys ty
; when (under_families tvs rho) $ flattenForAllErrorTcS ctxt ty
; (rho', co, no_flattening) <- flatten d ctxt rho
; return (mkForAllTys tvs rho', foldr mkForAllCo co tvs, no_flattening) }
; (rho', co) <- flatten d ctxt rho
; return (mkForAllTys tvs rho', foldr mkForAllCo co tvs) }
where under_families tvs rho
= go (mkVarSet tvs) rho
......@@ -681,7 +688,7 @@ getCachedFlatEq tc xi_args fl feq_origin
| fl' `canRewrite` fl
, feq_origin `origin_matches` when_generated
-> do { traceTcS "getCachedFlatEq" $ text "success!"
; (xi'',co,_) <- flatten 0 fl' xi' -- co :: xi'' ~ xi'
; (xi'',co) <- flatten 0 fl' xi' -- co :: xi'' ~ xi'
-- The only purpose of this flattening is to apply the
-- inert substitution (since everything in the flat cache
-- by construction will have a family-free RHS.
......@@ -689,12 +696,6 @@ getCachedFlatEq tc xi_args fl feq_origin
_ -> do { traceTcS "getCachedFlatEq" $ text "failure!" <+> pprEvVarCache flat_cache
; return Nothing }
\end{code}
\begin{code}
-----------------
addToWork :: TcS StopOrContinue -> TcS ()
addToWork tcs_action = tcs_action >>= stop_or_emit
......@@ -1042,7 +1043,7 @@ canEqLeaf :: SubGoalDepth -- Depth
-- * the two types are not equal (looking through synonyms)
canEqLeaf d fl eqv s1 s2
| cls1 `re_orient` cls2
= do { traceTcS "canEqLeaf (reorienting)" $ ppr (evVarPred eqv)
= do { traceTcS "canEqLeaf (reorienting)" $ ppr eqv <+> dcolon <+> pprEq s1 s2
; delCachedEvVar eqv fl
; evc <- newEqVar fl s2 s1
; let eqv' = evc_the_evvar evc
......@@ -1094,8 +1095,8 @@ canEqLeafFunEqLeftRec :: SubGoalDepth
-> EqVar
-> (TyCon,[TcType]) -> TcType -> TcS StopOrContinue
canEqLeafFunEqLeftRec d fl eqv (fn,tys1) ty2 -- eqv :: F tys1 ~ ty2
= do { traceTcS "canEqLeafFunEqLeftRec" $ ppr (evVarPred eqv)
; (xis1,cos1,no_flattening) <-
= do { traceTcS "canEqLeafFunEqLeftRec" $ pprEq (mkTyConApp fn tys1) ty2
; (xis1,cos1) <-
{-# SCC "flattenMany" #-}
flattenMany d fl tys1 -- Flatten type function arguments
-- cos1 :: xis1 ~ tys1
......@@ -1111,7 +1112,8 @@ canEqLeafFunEqLeftRec d fl eqv (fn,tys1) ty2 -- eqv :: F tys1 ~ ty2
; let is_cached = {-# SCC "lookupFunEq" #-}
lookupFunEq flat_ty fl fam_eqs
-}
; let no_flattening = all isReflCo cos1
; if no_flattening && isNothing is_cached then
canEqLeafFunEqLeft d fl eqv (fn,xis1) ty2
else do
......@@ -1157,10 +1159,11 @@ canEqLeafFunEqLeft :: SubGoalDepth -- Depth
-- Precondition: No more flattening is needed for the LHS
canEqLeafFunEqLeft d fl eqv (fn,xis1) s2
= {-# SCC "canEqLeafFunEqLeft" #-}
do { traceTcS "canEqLeafFunEqLeft" $ ppr (evVarPred eqv)
; (xi2,co2,no_flattening_happened) <-
do { traceTcS "canEqLeafFunEqLeft" $ pprEq (mkTyConApp fn xis1) s2
; (xi2,co2) <-
{-# SCC "flatten" #-}
flatten d fl s2 -- co2 :: xi2 ~ s2
; let no_flattening_happened = isReflCo co2
; if no_flattening_happened then
continueWith $ CFunEqCan { cc_id = eqv
, cc_flavor = fl
......@@ -1194,23 +1197,26 @@ canEqLeafTyVarLeftRec :: SubGoalDepth
-> CtFlavor -> EqVar
-> TcTyVar -> TcType -> TcS StopOrContinue
canEqLeafTyVarLeftRec d fl eqv tv s2 -- eqv :: tv ~ s2
= do { traceTcS "canEqLeafTyVarLeftRec" $ ppr (evVarPred eqv)
; (xi1,co1,no_flattening) <- flatten d fl (mkTyVarTy tv) -- co1 :: xi1 ~ tv
; if no_flattening then
canEqLeafTyVarLeft d fl eqv tv s2
else do { delCachedEvVar eqv fl
; evc <- newEqVar fl xi1 s2 -- new_ev :: xi1 ~ s2
; let new_ev = evc_the_evvar evc
; fl' <- case fl of
= do { traceTcS "canEqLeafTyVarLeftRec" $ pprEq (mkTyVarTy tv) s2
; (xi1,co1) <- flatten d fl (mkTyVarTy tv) -- co1 :: xi1 ~ tv
; case isReflCo co1 of
True -- If reflco and variable, just go on
| Just tv' <- getTyVar_maybe xi1
-> canEqLeafTyVarLeft d fl eqv tv' s2
_ -> -- If not a variable or not refl co, must rewrite and go on
do { delCachedEvVar eqv fl
; evc <- newEqVar fl xi1 s2 -- new_ev :: xi1 ~ s2
; let new_ev = evc_the_evvar evc
; fl' <- case fl of
Wanted {} -> setEqBind eqv
(mkSymCo co1 `mkTransCo` mkEqVarLCo new_ev) fl
Given {} -> setEqBind new_ev
(co1 `mkTransCo` mkEqVarLCo eqv) fl
Derived {} -> return fl
; if isNewEvVar evc then
; if isNewEvVar evc then
do { canEq d fl' new_ev xi1 s2 }
else return Stop
}
else return Stop
}
}
canEqLeafTyVarLeft :: SubGoalDepth -- Depth
......@@ -1218,8 +1224,11 @@ canEqLeafTyVarLeft :: SubGoalDepth -- Depth
-> TcTyVar -> TcType -> TcS StopOrContinue
-- Precondition LHS is fully rewritten from inerts (but not RHS)
canEqLeafTyVarLeft d fl eqv tv s2 -- eqv : tv ~ s2
= do { traceTcS "canEqLeafTyVarLeft" (ppr (evVarPred eqv))
; (xi2, co, no_flattening_happened) <- flatten d fl s2 -- Flatten RHS co : xi2 ~ s2
= do { traceTcS "canEqLeafTyVarLeft" (pprEq (mkTyVarTy tv) s2)
; (xi2, co) <- flatten d fl s2 -- Flatten RHS co : xi2 ~ s2
; let no_flattening_happened = isReflCo co
; traceTcS "canEqLeafTyVarLeft" (nest 2 (vcat [ text "tv =" <+> ppr tv
, text "s2 =" <+> ppr s2
, text "xi2 =" <+> ppr xi2]))
......
......@@ -114,7 +114,7 @@ solveInteractCts cts
= return (ct:acc_cts, alterTM pty (\_ -> Just (ev,fl)) acc_cache)
where fl = cc_flavor ct
ev = cc_id ct
pty = evVarPred ev
pty = ctPred ct
solveInteractGiven :: GivenLoc -> [EvVar] -> TcS ()
......@@ -319,11 +319,8 @@ kickOutRewritableInerts ct
-- Step 1: Rewrite as many of the inert_eqs on the spot!
-- NB: if it is a solved constraint just use the cached evidence
; let ct_coercion
| Just (GivenSolved (Just (EvCoercionBox co))) <- isGiven_maybe (cc_flavor ct)
= co
| otherwise
= mkEqVarLCo (cc_id ct)
; let ct_coercion = getCtCoercion ct
; new_ieqs <- {-# SCC "rewriteInertEqsFromInertEq" #-}
rewriteInertEqsFromInertEq (cc_tyvar ct,ct_coercion, cc_flavor ct) ieqs
......
......@@ -55,7 +55,7 @@ module TcRnTypes(
singleCt, extendCts, isEmptyCts, isCTyEqCan,
isCDictCan_Maybe, isCIPCan_Maybe, isCFunEqCan_Maybe,
isCIrredEvCan, isCNonCanonical,
SubGoalDepth,
SubGoalDepth, ctPred,
WantedConstraints(..), insolubleWC, emptyWC, isEmptyWC,
andWC, addFlats, addImplics, mkFlatWC,
......@@ -898,10 +898,28 @@ data Ct
cc_depth :: SubGoalDepth
}
\end{code}
\begin{code}
ctPred :: Ct -> PredType
ctPred (CNonCanonical { cc_id = v }) = evVarPred v
ctPred (CDictCan { cc_class = cls, cc_tyargs = xis })
= mkClassPred cls xis
ctPred (CTyEqCan { cc_tyvar = tv, cc_rhs = xi })
= mkEqPred (mkTyVarTy tv, xi)
ctPred (CFunEqCan { cc_fun = fn, cc_tyargs = xis1, cc_rhs = xi2 })
= mkEqPred(mkTyConApp fn xis1, xi2)
ctPred (CIPCan { cc_ip_nm = nm, cc_ip_ty = xi })
= mkIPPred nm xi
ctPred (CIrredEvCan { cc_ty = xi }) = xi
\end{code}
\begin{code}
instance Outputable Ct where
ppr ct = ppr (cc_flavor ct) <> braces (ppr (cc_depth ct))
<+> ppr ev_var <+> dcolon <+> ppr (varType ev_var)
<+> ppr ev_var <+> dcolon <+> ppr (ctPred ct)
<+> parens (text ct_sort)
where ev_var = cc_id ct
ct_sort = case ct of
......
......@@ -60,7 +60,7 @@ module TcSMonad (
-- Inerts
InertSet(..),
getInertEqs, liftInertEqsTy,
getInertEqs, liftInertEqsTy, getCtCoercion,
emptyInert, getTcSInerts, updInertSet, extractUnsolved,
extractUnsolvedTcS, modifyInertTcS,
updInertSetTcS, partitionCCanMap, partitionEqMap,
......@@ -143,6 +143,7 @@ import TrieMap
\end{code}
\begin{code}
compatKind :: Kind -> Kind -> Bool
compatKind k1 k2 = k1 `isSubKind` k2 || k2 `isSubKind` k1
......@@ -496,11 +497,7 @@ updInertSet is item
]
-- If evidence is cached, pick it up from the flavor!
coercion
| Just (GivenSolved (Just (EvCoercionBox co))) <- isGiven_maybe (cc_flavor item)
= co
| otherwise
= mkEqVarLCo (cc_id item)
coercion = getCtCoercion item
eqs' = extendVarEnv_C upd_err (inert_eqs is)
(cc_tyvar item)
......@@ -1507,6 +1504,17 @@ getInertEqs :: TcS (TyVarEnv (Ct,Coercion), InScopeSet)
getInertEqs = do { inert <- getTcSInerts
; return (inert_eqs inert, inert_eq_tvs inert) }
getCtCoercion :: Ct -> Coercion
-- Precondition: A CTyEqCan.
getCtCoercion ct
| Just (GivenSolved (Just (EvCoercionBox co))) <- maybe_given
= co
| otherwise
= mkEqVarLCo (setVarType (cc_id ct) (ctPred ct))
-- NB: The variable could be rewritten by a spontaneously
-- solved, so it is not safe to simply do a mkEqVarLCo (cc_id ct)
-- Instead we use the most accurate type, given by ctPred c
where maybe_given = isGiven_maybe (cc_flavor ct)
-- See Note [LiftInertEqs]
liftInertEqsTy :: (TyVarEnv (Ct,Coercion),InScopeSet)
......
......@@ -120,7 +120,7 @@ simplifyDeriv orig pred tvs theta
get_good :: Ct -> Either PredType Ct
get_good ct | validDerivPred skol_set p = Left p
| otherwise = Right ct
where p = evVarPred (cc_id ct)
where p = ctPred ct
; reportUnsolved (residual_wanted { wc_flat = bad })
......@@ -319,7 +319,7 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
-- Step 4, zonk quantified variables
{ let minimal_flat_preds = mkMinimalBySCs $
map (evVarPred . cc_id) $ bagToList bound
map ctPred $ bagToList bound
skol_info = InferSkol [ (name, mkSigmaTy [] minimal_flat_preds ty)
| (name, ty) <- name_taus ]
-- Don't add the quantified variables here, because
......@@ -432,13 +432,13 @@ growWanteds gbl_tvs wc = fixVarSet (growWC gbl_tvs wc)
growWantedEVs :: TyVarSet -> Cts -> TyVarSet -> TyVarSet
growWantedEVs gbl_tvs ws tvs
| isEmptyBag ws = tvs
| otherwise = fixVarSet (growPreds gbl_tvs (evVarPred . cc_id) ws) tvs
| otherwise = fixVarSet (growPreds gbl_tvs ctPred ws) tvs
-------- Helper functions, do not do fixpoint ------------------------
growWC :: TyVarSet -> WantedConstraints -> TyVarSet -> TyVarSet
growWC gbl_tvs wc = growImplics gbl_tvs (wc_impl wc) .
growPreds gbl_tvs (evVarPred . cc_id) (wc_flat wc) .
growPreds gbl_tvs (evVarPred . cc_id) (wc_insol wc)
growPreds gbl_tvs ctPred (wc_flat wc) .
growPreds gbl_tvs ctPred (wc_insol wc)
growImplics :: TyVarSet -> Bag Implication -> TyVarSet -> TyVarSet
growImplics gbl_tvs implics tvs
......@@ -466,7 +466,7 @@ quantifyMe qtvs ct
| isIPPred pred = True -- Note [Inheriting implicit parameters]
| otherwise = tyVarsOfType pred `intersectsVarSet` qtvs
where
pred = evVarPred (cc_id ct)
pred = ctPred ct
\end{code}
Note [Avoid unecessary constraint simplification]
......@@ -601,7 +601,7 @@ simplifyRule name tv_bndrs lhs_wanted rhs_wanted
-- Don't quantify over equalities (judgement call here)
; let (eqs, dicts) = partitionBag (isEqPred . evVarPred . cc_id)
; let (eqs, dicts) = partitionBag (isEqPred . ctPred)
(wc_flat lhs_results)
lhs_dicts = map cc_id (bagToList dicts)
-- Dicts and implicit parameters
......@@ -822,7 +822,7 @@ solveNestedImplications implics
pushable_wanted :: Ct -> Bool
pushable_wanted cc
| isWantedCt cc
= isEqPred (evVarPred (cc_id cc)) -- see Note [Preparing inert set for implications]
= isEqPred (ctPred cc) -- see Note [Preparing inert set for implications]
| otherwise = False
solveImplication :: TcTyVarSet -- Untouchable TcS unification variables
......@@ -885,7 +885,7 @@ floatEqualities skols can_given wantders
where is_floatable :: Ct -> Bool
is_floatable ct
| ct_predty <- evVarPred (cc_id ct)
| ct_predty <- ctPred ct
, isEqPred ct_predty
= skols `disjointVarSet` tvs_under_fsks ct_predty
is_floatable _ct = False
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment