Commit e5449309 authored by dimitris's avatar dimitris

isReflCo no longer reliable for detection of type identity.

Details:
isReflCo is no longer reliable for detection of no-rewriting/flattening
since we are using cached reflexivity solved goals. Introduced a boolean
flag in the flattener for this purpose, instead.
parent cae91683
......@@ -254,8 +254,8 @@ 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) <- flatten d fl (mkIPPred nm ty)
; if isReflCo co then
do { (xi,co,no_flattening) <- flatten d fl (mkIPPred nm ty)
; if no_flattening then
continueWith $ CIPCan { cc_id = v, cc_flavor = fl
, cc_ip_nm = nm, cc_ip_ty = ty
, cc_depth = d }
......@@ -296,12 +296,12 @@ 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) <- flattenMany d fl tys
; (xis, cos, no_flattening) <- flattenMany d fl tys
; let co = mkTyConAppCo (classTyCon cls) cos
xi = mkClassPred cls xis
-- No flattening, continue with canonical
; if isReflCo co then
; if no_flattening then
continueWith $ CDictCan { cc_id = v, cc_flavor = fl
, cc_tyargs = xis, cc_class = cls
, cc_depth = d }
......@@ -455,8 +455,7 @@ 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) <- flatten d fl ty -- co :: xi ~ ty
; let no_flattening = isReflCo co
; (xi,co,no_flattening) <- flatten d fl ty -- co :: xi ~ ty
; if no_flattening then
continueWith $ CIrredEvCan { cc_id = v, cc_flavor = fl
, cc_ty = xi, cc_depth = d }
......@@ -524,64 +523,70 @@ transitive expansion contains any type function applications. If so,
it expands the synonym and proceeds; if not, it simply returns the
unexpanded synonym.
TODO: caching the information about whether transitive synonym
expansions contain any type function applications would speed things
up a bit; right now we waste a lot of energy traversing the same types
multiple times.
\begin{code}
-- Flatten a bunch of types all at once.
flattenMany :: SubGoalDepth -- Depth
-> CtFlavor -> [Type] -> TcS ([Xi], [LCoercion])
-> CtFlavor -> [Type] -> TcS ([Xi], [LCoercion],Bool)
-- Coercions :: Xi ~ Type
-- Returns True iff (no flattening happened)
flattenMany d ctxt tys
= do { (xis, cos) <- mapAndUnzipM (flatten d ctxt) tys
; return (xis, cos) }
= -- 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) }
-- 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)
-> CtFlavor -> TcType -> TcS (Xi, LCoercion,Bool)
-- 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) <- flatten d ctxt ty'
= do { (xi, co, no_flattening) <- flatten d ctxt ty'
-- Preserve type synonyms if possible
; if isReflCo co
then return (ty, mkReflCo ty) -- Importantly, not xi!
else return (xi, co)
; if no_flattening
then return (ty, mkReflCo ty,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
; return (pSnd (liftedCoercionKind co), mkSymCo co) } -- return xi ~ v
; 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
flatten d ctxt (AppTy ty1 ty2)
= do { (xi1,co1) <- flatten d ctxt ty1
; (xi2,co2) <- flatten d ctxt ty2
; return (mkAppTy xi1 xi2, mkAppCo co1 co2) }
= 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) }
flatten d ctxt (FunTy ty1 ty2)
= do { (xi1,co1) <- flatten d ctxt ty1
; (xi2,co2) <- flatten d ctxt ty2
; return (mkFunTy xi1 xi2, mkFunCo co1 co2) }
= 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) }
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) <- flattenMany d fl tys
; return (mkTyConApp tc xis, mkTyConAppCo tc cos) }
= do { (xis,cos,no_flattening) <- flattenMany d fl tys
; return (mkTyConApp tc xis, mkTyConAppCo tc cos,no_flattening) }
-- 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) <- flattenMany d fl tys
do { (xis, cos, _no_flattening) <- 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
......@@ -605,7 +610,7 @@ flatten d fl (TyConApp tc tys)
, cc_rhs = rhs_xi_var
, cc_depth = d }
-- Update the flat cache: just an optimisation!
; updateFlatCache eqv fl tc xi_args rhs_xi_var WhileFlattening
; updateFlatCache eqv fl' tc xi_args rhs_xi_var WhileFlattening
; return (mkEqVarLCo eqv, rhs_xi_var, [ct]) }
| otherwise ->
-- Derived or Wanted: make a new /unification/ flatten variable
......@@ -631,7 +636,8 @@ flatten d fl (TyConApp tc tys)
; return ( mkAppTys rhs_xi xi_rest -- NB mkAppTys: rhs_xi might not be a type variable
-- cf Trac #5655
, foldl AppCo (mkSymCo ret_co `mkTransCo` mkTyConAppCo tc cos_args)
cos_rest) }
cos_rest
, False ) } -- no_flattening is False since we ARE flattening here!
flatten d ctxt ty@(ForAllTy {})
......@@ -639,8 +645,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) <- flatten d ctxt rho
; return (mkForAllTys tvs rho', foldr mkForAllCo co tvs) }
; (rho', co, no_flattening) <- flatten d ctxt rho
; return (mkForAllTys tvs rho', foldr mkForAllCo co tvs, no_flattening) }
where under_families tvs rho
= go (mkVarSet tvs) rho
......@@ -675,7 +681,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.
......@@ -1089,13 +1095,11 @@ canEqLeafFunEqLeftRec :: SubGoalDepth
-> (TyCon,[TcType]) -> TcType -> TcS StopOrContinue
canEqLeafFunEqLeftRec d fl eqv (fn,tys1) ty2 -- eqv :: F tys1 ~ ty2
= do { traceTcS "canEqLeafFunEqLeftRec" $ ppr (evVarPred eqv)
; (xis1,cos1) <-
; (xis1,cos1,no_flattening) <-
{-# SCC "flattenMany" #-}
flattenMany d fl tys1 -- Flatten type function arguments
-- cos1 :: xis1 ~ tys1
; let no_flattening = all isReflCo cos1
-- ; inerts <- getTcSInerts
-- ; let fam_eqs = inert_funeqs inerts
......@@ -1147,26 +1151,6 @@ lookupFunEq pty fl fam_eqs = lookup_funeq pty fam_eqs
| otherwise
= Nothing
{- Original, not using inert family equations:
; if no_flattening then
canEqLeafFunEqLeft d fl eqv (fn,xis1) ty2
else do -- There was flattening
{ let (final_co, final_ty) = (mkTyConAppCo fn cos1, mkTyConApp fn xis1)
; delCachedEvVar eqv
; evc <- newEqVar fl final_ty ty2
; let new_eqv = evc_the_evvar evc
; case fl of
Wanted {} -> setEqBind eqv $ mkSymCo final_co `mkTransCo` (mkEqVarLCo new_eqv)
Given {} -> setEqBind new_eqv $ final_co `mkTransCo` (mkEqVarLCo eqv)
Derived {} -> return ()
; if isNewEvVar evc then
canEqLeafFunEqLeft d fl new_eqv (fn,xis1) ty2
else return Stop
}
}
-}
canEqLeafFunEqLeft :: SubGoalDepth -- Depth
-> CtFlavor -> EqVar -> (TyCon,[Xi])
-> TcType -> TcS StopOrContinue
......@@ -1174,10 +1158,9 @@ canEqLeafFunEqLeft :: SubGoalDepth -- Depth
canEqLeafFunEqLeft d fl eqv (fn,xis1) s2
= {-# SCC "canEqLeafFunEqLeft" #-}
do { traceTcS "canEqLeafFunEqLeft" $ ppr (evVarPred eqv)
; (xi2,co2) <-
; (xi2,co2,no_flattening_happened) <-
{-# 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
......@@ -1212,8 +1195,8 @@ canEqLeafTyVarLeftRec :: SubGoalDepth
-> TcTyVar -> TcType -> TcS StopOrContinue
canEqLeafTyVarLeftRec d fl eqv tv s2 -- eqv :: tv ~ s2
= do { traceTcS "canEqLeafTyVarLeftRec" $ ppr (evVarPred eqv)
; (xi1,co1) <- flatten d fl (mkTyVarTy tv) -- co1 :: xi1 ~ tv
; if isReflCo co1 then
; (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
......@@ -1236,7 +1219,7 @@ canEqLeafTyVarLeft :: SubGoalDepth -- Depth
-- 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) <- flatten d fl s2 -- Flatten RHS co : xi2 ~ s2
; (xi2, co, no_flattening_happened) <- flatten d fl s2 -- Flatten RHS co : xi2 ~ s2
; traceTcS "canEqLeafTyVarLeft" (nest 2 (vcat [ text "tv =" <+> ppr tv
, text "s2 =" <+> ppr s2
, text "xi2 =" <+> ppr xi2]))
......@@ -1263,7 +1246,6 @@ canEqLeafTyVarLeft d fl eqv tv s2 -- eqv : tv ~ s2
= xi2_unfolded
| otherwise = xi2
; let no_flattening_happened = isReflCo co
; if no_flattening_happened then
if isNothing occ_check_result then
......
......@@ -339,72 +339,57 @@ rewriteInertEqsFromInertEq :: (TcTyVar,Coercion, CtFlavor) -- A new substitution
-> TyVarEnv (Ct,Coercion) -- All inert equalities
-> TcS (TyVarEnv (Ct,Coercion)) -- The new inert equalities
rewriteInertEqsFromInertEq (subst_tv,subst_co, subst_fl) ieqs
-- The goal: traverse the inert equalities:
-- 1) If current inert element cannot itself rewrite subst_fl then:
-- a) if it is rewritable by subst fl throw him out
-- b) if it is not rewritable by subst keep him in as is
-- 2) otherwise
-- a) if it is rewritable by subst fl rewrite him on the spot
-- b) if it is not rewritable by subst fl then keep him as is
= do { mieqs <- Traversable.mapM do_one ieqs -- mieqs :: TyVarEnv (Maybe (Ct,Coercion))
; case Traversable.sequence mieqs of
Nothing -> return emptyVarEnv
Just final_ieqs -> return final_ieqs }
-- The goal: traverse the inert equalities and rewrite some of them, dropping some others
-- back to the worklist. This is delicate, see Note [Delicate equality kick-out]
= do { mieqs <- Traversable.mapM do_one ieqs
; traceTcS "Original inert equalities:" (ppr ieqs)
; let flatten_justs elem venv
| Just (act,aco) <- elem = extendVarEnv venv (cc_tyvar act) (act,aco)
| otherwise = venv
final_ieqs = foldVarEnv flatten_justs emptyVarEnv mieqs
; traceTcS "Remaining inert equalities:" (ppr final_ieqs)
; return final_ieqs }
where do_one (ct,inert_co)
| (not (subst_fl `canRewrite` fl)) || isReflCo co
-- If the inert is not rewritable we just keep it
= return (Just (ct,inert_co))
-- Inert is definitely rewritable
| not (fl `canRewrite` subst_fl) -- But the inert cannot itself rewrite the subst item
-- so there is need for recanonicalization.
= do { updWorkListTcS (extendWorkListEq ct)
; return Nothing }
| otherwise -- Or the inert can rewrite subst as well, so it's safe to rewrite on-the-spot
= do { let rhs' = pSnd (liftedCoercionKind co)
; delCachedEvVar ev fl
; evc <- newEqVar fl (mkTyVarTy tv) rhs'
; let ev' = evc_the_evvar evc
; let evco' = mkEqVarLCo ev'
; fl' <- if isNewEvVar evc then
do { case fl of
Wanted {} -> setEqBind ev
(evco' `mkTransCo` mkSymCo co) fl
Given {} -> setEqBind ev'
(mkEqVarLCo ev `mkTransCo` co) fl
Derived {} -> return fl }
else
if (isWanted fl) then
setEqBind ev (evco' `mkTransCo` mkSymCo co) fl
else
return fl
; let ct' = ct { cc_id = ev', cc_flavor = fl', cc_rhs = rhs' }
; return (Just (ct',evco')) }
where ev = cc_id ct
fl = cc_flavor ct
tv = cc_tyvar ct
rhs = cc_rhs ct
co = liftCoSubstWith [subst_tv] [subst_co] rhs
-- (eqs_out, eqs_in) = partitionEqMap
-- (\inert_ct -> (not (cc_flavor inert_ct `canRewrite` fl)) &&
-- rewritable inert_ct) eqmap
-- -- Why not just (rewritable_inert ct)? Check out Note [Delicate equality kick-out]
-- {-
-- traceTcS "rewriteInertEqsFromInertEq" $
-- vcat [ text "rewriting equality: " <+> ppr ct
-- , text "from: " <+> ppr subst_co <+> text "of flavor: " <+> ppr subst_fl
-- , text "can rewrite? " <+> ppr (subst_fl `canRewrite` fl) ]
-- -}
| subst_fl `canRewrite` fl && (subst_tv `elemVarSet` tyVarsOfCt ct)
-- Annoyingly inefficient, but we can't simply check
-- that isReflCo co because of cached solved ReflCo evidence.
= if fl `canRewrite` subst_fl then
-- If also the inert can rewrite the subst it's totally safe
-- to rewrite on the spot
do { (ct',inert_co') <- rewrite_on_the_spot (ct,inert_co)
; return $ Just (ct',inert_co') }
else -- We have to throw inert back to worklist for occurs checks
do { updWorkListTcS (extendWorkListEq ct)
; return Nothing }
| otherwise -- Just keep it there
= return $ Just (ct,inert_co)
where
rewrite_on_the_spot (ct,_inert_co)
= do { let rhs' = pSnd (liftedCoercionKind co)
; delCachedEvVar ev fl
; evc <- newEqVar fl (mkTyVarTy tv) rhs'
; let ev' = evc_the_evvar evc
; let evco' = mkEqVarLCo ev'
; fl' <- if isNewEvVar evc then
do { case fl of
Wanted {}
-> setEqBind ev (evco' `mkTransCo` mkSymCo co) fl
Given {}
-> setEqBind ev' (mkEqVarLCo ev `mkTransCo` co) fl
Derived {}
-> return fl }
else
if isWanted fl then
setEqBind ev (evco' `mkTransCo` mkSymCo co) fl
else return fl
; let ct' = ct { cc_id = ev', cc_flavor = fl', cc_rhs = rhs' }
; return (ct',evco') }
ev = cc_id ct
fl = cc_flavor ct
tv = cc_tyvar ct
rhs = cc_rhs ct
co = liftCoSubstWith [subst_tv] [subst_co] rhs
kick_out_rewritable :: Ct -> InertSet -> ((WorkList,TyVarEnv (Ct,Coercion)), InertSet)
-- Returns ALL equalities, to be dealt with later
......
......@@ -489,8 +489,11 @@ updInertSet :: InertSet -> AtomicInert -> InertSet
-- Add a new inert element to the inert set.
updInertSet is item
| isCTyEqCan item
= let upd_err a b = pprPanic "updInertSet" $
vcat [text "Multiple inert equalities:", ppr a, ppr b]
= let upd_err a b = pprPanic "updInertSet" $
vcat [ text "Multiple inert equalities:"
, text "Old (already inert):" <+> ppr a
, text "Trying to insert :" <+> ppr b
]
-- If evidence is cached, pick it up from the flavor!
coercion
......@@ -1084,6 +1087,7 @@ setWantedTyBind tv ty
setEvBind :: EvVar -> EvTerm -> CtFlavor -> TcS CtFlavor
-- If the flavor is Solved, we cache the new evidence term inside the returned flavor
-- see Note [Optimizing Spontaneously Solved Coercions]
setEvBind ev t fl
= do { tc_evbinds <- getTcEvBinds
; wrapTcS $ TcM.addTcEvBind tc_evbinds ev t
......@@ -1124,6 +1128,51 @@ setEvBind ev t fl
evterm_evs (EvTupleMk evs) = evs
#endif
\end{code}
Note [Optimizing Spontaneously Solved Coercions]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Spontaneously solved coercions such as alpha := tau used to be bound as everything else
in the evidence binds. Subsequently they were used for rewriting other wanted or solved
goals. For instance:
WorkItem = [S] g1 : a ~ tau
Inerts = [S] g2 : b ~ [a]
[S] g3 : c ~ [(a,a)]
Would result, eventually, after the workitem rewrites the inerts, in the
following evidence bindings:
g1 = ReflCo tau
g2 = ReflCo [a]
g3 = ReflCo [(a,a)]
g2' = g2 ; [g1]
g3' = g3 ; [(g1,g1)]
This ia annoying because it puts way too much stress to the zonker and
desugarer, since we /know/ at the generation time (spontaneously
solving) that the evidence for a particular evidence variable is the
identity.
For this reason, our solution is to cache inside the GivenSolved
flavor of a constraint the term which is actually solving this
constraint. Whenever we perform a setEvBind, a new flavor is returned
so that if it was a GivenSolved to start with, it remains a
GivenSolved with a new evidence term inside. Then, when we use solved
goals to rewrite other constraints we simply use whatever is in the
GivenSolved flavor and not the constraint cc_id.
In our particular case we'd get the following evidence bindings, eventually:
g1 = ReflCo tau
g2 = ReflCo [a]
g3 = ReflCo [(a,a)]
g2'= ReflCo [a]
g3'= ReflCo [(a,a)]
Since we use smart constructors to get rid of g;ReflCo t ~~> g etc.
\begin{code}
warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
......@@ -1458,37 +1507,6 @@ getInertEqs :: TcS (TyVarEnv (Ct,Coercion), InScopeSet)
getInertEqs = do { inert <- getTcSInerts
; return (inert_eqs inert, inert_eq_tvs inert) }
{-- UNSAFE in the prsence of Solved flavors! Don't use!
rewriteFromInertEqs :: (TyVarEnv (Ct,Coercion), InScopeSet)
-- Precondition: Ct are CTyEqCans only!
-> CtFlavor
-> EvVar
-> TcS (EvVar,Bool)
-- Boolean flag returned: True <-> no rewriting happened
rewriteFromInertEqs (subst,inscope) fl v
= do { let co = liftInertEqsTy (subst,inscope) fl (evVarPred v)
; if isReflCo co then return (v,True)
else do { traceTcS "rewriteFromInertEqs" $
text "Original item =" <+> ppr v <+> dcolon <+> ppr (evVarPred v)
; delCachedEvVar v fl
; evc <- newEvVar fl (pSnd (liftedCoercionKind co))
; let v' = evc_the_evvar evc
; if isNewEvVar evc then
do { case fl of
Wanted {} -> setEvBind v (EvCast v' (mkSymCo co))
Given {} -> setEvBind v' (EvCast v co)
Derived {} -> return ()
; traceTcS "rewriteFromInertEqs" $
text "Rewritten item =" <+> ppr v' <+>
dcolon <+> ppr (evVarPred v')
; return (v',False) }
else -- Maybe given, but when wanted set bind
do { case fl of
Wanted {} -> setEvBind v (EvCast v' (mkSymCo co))
_ -> return ()
; return (v',True) } -- As if rewriting never happened?
} }
--}
-- See Note [LiftInertEqs]
liftInertEqsTy :: (TyVarEnv (Ct,Coercion),InScopeSet)
......@@ -1544,7 +1562,7 @@ ty_cts_subst subst inscope fl ty
unused_evvar = panic "ty_cts_subst: This var is just an alpha-renaming!"
\end{code}
Note [LiftInertEqsPred]
Note [LiftInertEqsTy]
~~~~~~~~~~~~~~~~~~~~~~~
The function liftInertEqPred behaves almost like liftCoSubst (in
Coercion), but accepts a map TyVarEnv (Ct,Coercion) instead of a
......
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