\begin{code}
module TcCanonical(
- mkCanonical, mkCanonicals, mkCanonicalFEV, canWanteds, canGivens,
- canOccursCheck, canEq,
+ mkCanonical, mkCanonicals, mkCanonicalFEV, mkCanonicalFEVs, canWanteds, canGivens,
+ canOccursCheck, canEqToWorkList,
rewriteWithFunDeps
) where
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 :: CtFlavor -> [Type] -> TcS ([Xi], [Coercion], CanonicalCts)
-- 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
+ | otherwise
= ASSERT( tyConArity tc <= length tys ) -- Type functions are saturated
do { (xis, cos, ccs) <- flattenMany fl tys
; let (xi_args, xi_rest) = splitAt (tyConArity tc) xis
-- in which case the remaining arguments should
-- be dealt with by AppTys
fam_ty = mkTyConApp tc xi_args
- fam_co = fam_ty -- identity
-
- ; (ret_co, rhs_var, ct) <-
- if isGiven fl then
- do { rhs_var <- newFlattenSkolemTy fam_ty
- ; cv <- newGivenCoVar fam_ty rhs_var fam_co
- ; let ct = CFunEqCan { cc_id = cv
- , cc_flavor = fl -- Given
- , cc_fun = tc
- , cc_tyargs = xi_args
- , cc_rhs = rhs_var }
- ; return $ (mkCoVarCoercion cv, rhs_var, ct) }
- else -- Derived or Wanted: make a new *unification* flatten variable
- do { rhs_var <- newFlexiTcSTy (typeKind fam_ty)
- ; cv <- newWantedCoVar fam_ty rhs_var
- ; let ct = CFunEqCan { cc_id = cv
- , cc_flavor = mkWantedFlavor fl
- -- Always Wanted, not Derived
- , cc_fun = tc
- , cc_tyargs = xi_args
- , cc_rhs = rhs_var }
- ; return $ (mkCoVarCoercion cv, rhs_var, ct) }
-
+ fam_co = fam_ty -- identity
+ ; (ret_co, rhs_var, ct) <-
+ do { is_cached <- lookupFlatCacheMap tc xi_args fl
+ ; case is_cached of
+ Just (rhs_var,ret_co,_fl) -> return (ret_co, rhs_var, emptyCCan)
+ Nothing
+ | isGivenOrSolved fl ->
+ do { rhs_var <- newFlattenSkolemTy fam_ty
+ ; cv <- newGivenCoVar fam_ty rhs_var fam_co
+ ; let ct = CFunEqCan { cc_id = cv
+ , cc_flavor = fl -- Given
+ , cc_fun = tc
+ , cc_tyargs = xi_args
+ , cc_rhs = rhs_var }
+ ; let ret_co = mkCoVarCoercion cv
+ ; updateFlatCacheMap tc xi_args rhs_var fl ret_co
+ ; return $ (ret_co, rhs_var, singleCCan ct) }
+ | otherwise ->
+ -- Derived or Wanted: make a new *unification* flatten variable
+ do { rhs_var <- newFlexiTcSTy (typeKind fam_ty)
+ ; cv <- newCoVar fam_ty rhs_var
+ ; let ct = CFunEqCan { cc_id = cv
+ , cc_flavor = mkWantedFlavor fl
+ -- Always Wanted, not Derived
+ , cc_fun = tc
+ , cc_tyargs = xi_args
+ , cc_rhs = rhs_var }
+ ; let ret_co = mkCoVarCoercion cv
+ ; updateFlatCacheMap tc xi_args rhs_var fl ret_co
+ ; return $ (ret_co, rhs_var, singleCCan ct) } }
; return ( foldl AppTy rhs_var xi_rest
, foldl AppTy (mkSymCoercion ret_co
- `mkTransCoercion` mkTyConCoercion tc cos_args) cos_rest
- , ccs `extendCCans` ct) }
+ `mkTransCoercion` mkTyConCoercion tc cos_args) cos_rest
+ , ccs `andCCan` ct) }
flatten ctxt (PredTy pred)
%************************************************************************
\begin{code}
-canWanteds :: [WantedEvVar] -> TcS CanonicalCts
-canWanteds = fmap andCCans . mapM (\(EvVarX ev loc) -> mkCanonical (Wanted loc) ev)
+canWanteds :: [WantedEvVar] -> TcS WorkList
+canWanteds = fmap unionWorkLists . mapM (\(EvVarX ev loc) -> mkCanonical (Wanted loc) ev)
-canGivens :: GivenLoc -> [EvVar] -> TcS CanonicalCts
-canGivens loc givens = do { ccs <- mapM (mkCanonical (Given loc)) givens
- ; return (andCCans ccs) }
+canGivens :: GivenLoc -> [EvVar] -> TcS WorkList
+canGivens loc givens = do { ccs <- mapM (mkCanonical (Given loc GivenOrig)) givens
+ ; return (unionWorkLists ccs) }
-mkCanonicals :: CtFlavor -> [EvVar] -> TcS CanonicalCts
-mkCanonicals fl vs = fmap andCCans (mapM (mkCanonical fl) vs)
+mkCanonicals :: CtFlavor -> [EvVar] -> TcS WorkList
+mkCanonicals fl vs = fmap unionWorkLists (mapM (mkCanonical fl) vs)
-mkCanonicalFEV :: FlavoredEvVar -> TcS CanonicalCts
+mkCanonicalFEV :: FlavoredEvVar -> TcS WorkList
mkCanonicalFEV (EvVarX ev fl) = mkCanonical fl ev
-mkCanonical :: CtFlavor -> EvVar -> TcS CanonicalCts
+mkCanonicalFEVs :: Bag FlavoredEvVar -> TcS WorkList
+mkCanonicalFEVs = foldrBagM canon_one emptyWorkList
+ where -- Preserves order (shouldn't be important, but curently
+ -- is important for the vectoriser)
+ canon_one fev wl = do { wl' <- mkCanonicalFEV fev
+ ; return (unionWorkList wl' wl) }
+
+
+mkCanonical :: CtFlavor -> EvVar -> TcS WorkList
mkCanonical fl ev = case evVarPred ev of
- ClassP clas tys -> canClass fl ev clas tys
- IParam ip ty -> canIP fl ev ip ty
- EqPred ty1 ty2 -> canEq fl ev ty1 ty2
+ ClassP clas tys -> canClassToWorkList fl ev clas tys
+ IParam ip ty -> canIPToWorkList fl ev ip ty
+ EqPred ty1 ty2 -> canEqToWorkList fl ev ty1 ty2
-canClass :: CtFlavor -> EvVar -> Class -> [TcType] -> TcS CanonicalCts
-canClass fl v cn tys
+canClassToWorkList :: CtFlavor -> EvVar -> Class -> [TcType] -> TcS WorkList
+canClassToWorkList fl v cn tys
= do { (xis,cos,ccs) <- flattenMany fl tys -- cos :: xis ~ tys
; let no_flattening_happened = isEmptyCCan ccs
dict_co = mkTyConCoercion (classTyCon cn) cos
- ; v_new <- if no_flattening_happened then return v
- else if isGiven fl then return v
+ ; v_new <- if no_flattening_happened then return v
+ else if isGivenOrSolved fl then return v
-- The cos are all identities if fl=Given,
-- hence nothing to do
else do { v' <- newDictVar cn xis -- D xis
; when (isWanted fl) $ setDictBind v (EvCast v' dict_co)
- ; when (isGiven fl) $ setDictBind v' (EvCast v (mkSymCoercion dict_co))
+ ; when (isGivenOrSolved fl) $ setDictBind v' (EvCast v (mkSymCoercion dict_co))
-- NB: No more setting evidence for derived now
; return v' }
-- Add the superclasses of this one here, See Note [Adding superclasses].
-- But only if we are not simplifying the LHS of a rule.
; sctx <- getTcSContext
- ; sc_cts <- if simplEqsOnly sctx then return emptyCCan
+ ; sc_cts <- if simplEqsOnly sctx then return emptyWorkList
else newSCWorkFromFlavored v_new fl cn xis
- ; return (sc_cts `andCCan` ccs `extendCCans` CDictCan { cc_id = v_new
- , cc_flavor = fl
- , cc_class = cn
- , cc_tyargs = xis }) }
+ ; return (sc_cts `unionWorkList`
+ workListFromEqs ccs `unionWorkList`
+ workListFromNonEq CDictCan { cc_id = v_new
+ , cc_flavor = fl
+ , cc_class = cn
+ , cc_tyargs = xis }) }
\end{code}
Note [Adding superclasses]
Here's an example that demonstrates why we chose to NOT add
superclasses during simplification: [Comes from ticket #4497]
-
+
class Num (RealOf t) => Normed t
type family RealOf x
\begin{code}
-newSCWorkFromFlavored :: EvVar -> CtFlavor -> Class -> [Xi] -> TcS CanonicalCts
+newSCWorkFromFlavored :: EvVar -> CtFlavor -> Class -> [Xi] -> TcS WorkList
-- Returns superclasses, see Note [Adding superclasses]
newSCWorkFromFlavored ev orig_flavor cls xis
| isDerived orig_flavor
- = return emptyCCan -- Deriveds don't yield more superclasses because we will
- -- add them transitively in the case of wanteds.
-
- | isGiven orig_flavor
- = do { let sc_theta = immSuperClasses cls xis
- flavor = orig_flavor
- ; sc_vars <- mapM newEvVar sc_theta
- ; _ <- zipWithM_ setEvBind sc_vars [EvSuperClass ev n | n <- [0..]]
- ; mkCanonicals flavor sc_vars }
-
- | isEmptyVarSet (tyVarsOfTypes xis)
- = return emptyCCan -- Wanteds with no variables yield no deriveds.
- -- See Note [Improvement from Ground Wanteds]
+ = return emptyWorkList -- Deriveds don't yield more superclasses because we will
+ -- add them transitively in the case of wanteds.
+
+ | Just gk <- isGiven_maybe orig_flavor
+ = case gk of
+ GivenOrig -> do { let sc_theta = immSuperClasses cls xis
+ flavor = orig_flavor
+ ; sc_vars <- mapM newEvVar sc_theta
+ ; _ <- zipWithM_ setEvBind sc_vars [EvSuperClass ev n | n <- [0..]]
+ ; mkCanonicals flavor sc_vars }
+ GivenSolved -> return emptyWorkList
+ -- Seems very dangerous to add the superclasses for dictionaries that may be
+ -- partially solved because we may end up with evidence loops.
+
+ | isEmptyVarSet (tyVarsOfTypes xis)
+ = return emptyWorkList -- Wanteds with no variables yield no deriveds.
+ -- See Note [Improvement from Ground Wanteds]
| otherwise -- Wanted case, just add those SC that can lead to improvement.
= do { let sc_rec_theta = transSuperClasses cls xis
-canIP :: CtFlavor -> EvVar -> IPName Name -> TcType -> TcS CanonicalCts
+canIPToWorkList :: CtFlavor -> EvVar -> IPName Name -> TcType -> TcS WorkList
-- See Note [Canonical implicit parameter constraints] to see why we don't
-- immediately canonicalize (flatten) IP constraints.
-canIP fl v nm ty
- = return $ singleCCan $ CIPCan { cc_id = v
- , cc_flavor = fl
- , cc_ip_nm = nm
- , cc_ip_ty = ty }
+canIPToWorkList fl v nm ty
+ = return $ workListFromNonEq (CIPCan { cc_id = v
+ , cc_flavor = fl
+ , cc_ip_nm = nm
+ , cc_ip_ty = ty })
-----------------
+canEqToWorkList :: CtFlavor -> EvVar -> Type -> Type -> TcS WorkList
+canEqToWorkList fl cv ty1 ty2 = do { cts <- canEq fl cv ty1 ty2
+ ; return $ workListFromEqs cts }
+
canEq :: CtFlavor -> EvVar -> Type -> Type -> TcS CanonicalCts
canEq fl cv ty1 ty2
| tcEqType ty1 ty2 -- Dealing with equality here avoids
-- later spurious occurs checks for a~a
- = do { when (isWanted fl) (setWantedCoBind cv ty1)
+ = do { when (isWanted fl) (setCoBind cv ty1)
; return emptyCCan }
-- If one side is a variable, orient and flatten,
Just (t2a,t2b,t2c) <- splitCoPredTy_maybe s2
= do { (v1,v2,v3)
<- if isWanted fl then -- Wanted
- do { v1 <- newWantedCoVar t1a t2a
- ; v2 <- newWantedCoVar t1b t2b
- ; v3 <- newWantedCoVar t1c t2c
+ do { v1 <- newCoVar t1a t2a
+ ; v2 <- newCoVar t1b t2b
+ ; v3 <- newCoVar t1c t2c
; let res_co = mkCoPredCo (mkCoVarCoercion v1)
(mkCoVarCoercion v2) (mkCoVarCoercion v3)
- ; setWantedCoBind cv res_co
+ ; setCoBind cv res_co
; return (v1,v2,v3) }
- else if isGiven fl then -- Given
+ else if isGivenOrSolved fl then -- Given
let co_orig = mkCoVarCoercion cv
coa = mkCsel1Coercion co_orig
cob = mkCsel2Coercion co_orig
canEq fl cv (FunTy s1 t1) (FunTy s2 t2)
= do { (argv, resv) <-
if isWanted fl then
- do { argv <- newWantedCoVar s1 s2
- ; resv <- newWantedCoVar t1 t2
- ; setWantedCoBind cv $
+ do { argv <- newCoVar s1 s2
+ ; resv <- newCoVar t1 t2
+ ; setCoBind cv $
mkFunCoercion (mkCoVarCoercion argv) (mkCoVarCoercion resv)
; return (argv,resv) }
- else if isGiven fl then
+ else if isGivenOrSolved fl then
let [arg,res] = decomposeCo 2 (mkCoVarCoercion cv)
in do { argv <- newGivenCoVar s1 s2 arg
; resv <- newGivenCoVar t1 t2 res
canEq fl cv (PredTy (IParam n1 t1)) (PredTy (IParam n2 t2))
| n1 == n2
= if isWanted fl then
- do { v <- newWantedCoVar t1 t2
- ; setWantedCoBind cv $ mkIParamPredCo n1 (mkCoVarCoercion cv)
+ do { v <- newCoVar t1 t2
+ ; setCoBind cv $ mkIParamPredCo n1 (mkCoVarCoercion cv)
; canEq fl v t1 t2 }
else return emptyCCan -- DV: How to decompose given IP coercions?
canEq fl cv (PredTy (ClassP c1 tys1)) (PredTy (ClassP c2 tys2))
| c1 == c2
= if isWanted fl then
- do { vs <- zipWithM newWantedCoVar tys1 tys2
- ; setWantedCoBind cv $ mkClassPPredCo c1 (map mkCoVarCoercion vs)
+ do { vs <- zipWithM newCoVar tys1 tys2
+ ; setCoBind cv $ mkClassPPredCo c1 (map mkCoVarCoercion vs)
; andCCans <$> zipWith3M (canEq fl) vs tys1 tys2
}
else return emptyCCan
= -- Generate equalities for each of the corresponding arguments
do { argsv
<- if isWanted fl then
- do { argsv <- zipWithM newWantedCoVar tys1 tys2
- ; setWantedCoBind cv $
+ do { argsv <- zipWithM newCoVar tys1 tys2
+ ; setCoBind cv $
mkTyConCoercion tc1 (map mkCoVarCoercion argsv)
; return argsv }
- else if isGiven fl then
+ else if isGivenOrSolved fl then
let cos = decomposeCo (length tys1) (mkCoVarCoercion cv)
in zipWith3M newGivenCoVar tys1 tys2 cos
, Just (s2,t2) <- tcSplitAppTy_maybe ty2
= do { (cv1,cv2) <-
if isWanted fl
- then do { cv1 <- newWantedCoVar s1 s2
- ; cv2 <- newWantedCoVar t1 t2
- ; setWantedCoBind cv $
+ then do { cv1 <- newCoVar s1 s2
+ ; cv2 <- newCoVar t1 t2
+ ; setCoBind cv $
mkAppCoercion (mkCoVarCoercion cv1) (mkCoVarCoercion cv2)
; return (cv1,cv2) }
- else if isGiven fl then
+ else if isGivenOrSolved fl then
let co1 = mkLeftCoercion $ mkCoVarCoercion cv
co2 = mkRightCoercion $ mkCoVarCoercion cv
in do { cv1 <- newGivenCoVar s1 s2 co1
canEqLeaf _untch fl cv cls1 cls2
| cls1 `re_orient` cls2
= do { cv' <- if isWanted fl
- then do { cv' <- newWantedCoVar s2 s1
- ; setWantedCoBind cv $ mkSymCoercion (mkCoVarCoercion cv')
+ then do { cv' <- newCoVar s2 s1
+ ; setCoBind cv $ mkSymCoercion (mkCoVarCoercion cv')
; return cv' }
- else if isGiven fl then
+ else if isGivenOrSolved fl then
newGivenCoVar s2 s1 (mkSymCoercion (mkCoVarCoercion cv))
else -- Derived
newDerivedId (EqPred s2 s1)
-- co2 :: xi2 ~ s2
; let ccs = ccs1 `andCCan` ccs2
no_flattening_happened = isEmptyCCan ccs
- ; cv_new <- if no_flattening_happened then return cv
- else if isGiven fl then return cv
+ ; cv_new <- if no_flattening_happened then return cv
+ else if isGivenOrSolved fl then return cv
else if isWanted fl then
- do { cv' <- newWantedCoVar (unClassify (FunCls fn xis1)) xi2
+ do { cv' <- newCoVar (unClassify (FunCls fn xis1)) xi2
-- cv' : F xis ~ xi2
; let -- fun_co :: F xis1 ~ F tys1
fun_co = mkTyConCoercion fn cos1
want_co = mkSymCoercion fun_co
`mkTransCoercion` mkCoVarCoercion cv'
`mkTransCoercion` co2
- ; setWantedCoBind cv want_co
+ ; setCoBind cv want_co
; return cv' }
else -- Derived
newDerivedId (EqPred (unClassify (FunCls fn xis1)) xi2)
Nothing -> canEqFailure fl cv ;
Just xi2' ->
do { let no_flattening_happened = isEmptyCCan ccs2
- ; cv_new <- if no_flattening_happened then return cv
- else if isGiven fl then return cv
+ ; cv_new <- if no_flattening_happened then return cv
+ else if isGivenOrSolved fl then return cv
else if isWanted fl then
- do { cv' <- newWantedCoVar (mkTyVarTy tv) xi2' -- cv' : tv ~ xi2
- ; setWantedCoBind cv (mkCoVarCoercion cv' `mkTransCoercion` co)
+ do { cv' <- newCoVar (mkTyVarTy tv) xi2' -- cv' : tv ~ xi2
+ ; setCoBind cv (mkCoVarCoercion cv' `mkTransCoercion` co)
; return cv' }
else -- Derived
newDerivedId (EqPred (mkTyVarTy tv) xi2')
\begin{code}
rewriteWithFunDeps :: [Equation]
-> [Xi] -> CtFlavor
- -> TcS (Maybe ([Xi], [Coercion], CanonicalCts))
+ -> TcS (Maybe ([Xi], [Coercion], WorkList))
rewriteWithFunDeps eqn_pred_locs xis fl
= do { fd_ev_poss <- mapM (instFunDepEqn fl) eqn_pred_locs
; let fd_ev_pos :: [(Int,FlavoredEvVar)]
fd_ev_pos = concat fd_ev_poss
(rewritten_xis, cos) = unzip (rewriteDictParams fd_ev_pos xis)
; fds <- mapM (\(_,fev) -> mkCanonicalFEV fev) fd_ev_pos
- ; let fd_work = unionManyBags fds
- ; if isEmptyBag fd_work
+ ; let fd_work = unionWorkLists fds
+ ; if isEmptyWorkList fd_work
then return Nothing
else return (Just (rewritten_xis, cos, fd_work)) }
; mapM (do_one subst) eqs }
where
fl' = case fl of
- Given _ -> panic "mkFunDepEqns"
+ Given {} -> panic "mkFunDepEqns"
Wanted loc -> Wanted (push_ctx loc)
Derived loc -> Derived (push_ctx loc)
projects / ghc-hetmet.git / blobdiff