X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcCanonical.lhs;h=59cc736083e5883ac4a0da65fd178856c59fa04a;hb=191292aaa7f56f32fc546478f43aa89ac67c95a3;hp=861b262cf011f45481d7bb37f715443f20aa0628;hpb=72c40bc5f2d193ebd89471f6e1f2a36b81042304;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs index 861b262..59cc736 100644 --- a/compiler/typecheck/TcCanonical.lhs +++ b/compiler/typecheck/TcCanonical.lhs @@ -1,7 +1,8 @@ \begin{code} module TcCanonical( - mkCanonical, mkCanonicals, mkCanonicalFEV, canWanteds, canGivens, - canOccursCheck, canEq + mkCanonical, mkCanonicals, mkCanonicalFEV, mkCanonicalFEVs, canWanteds, canGivens, + canOccursCheck, canEqToWorkList, + rewriteWithFunDeps ) where #include "HsVersions.h" @@ -9,7 +10,8 @@ module TcCanonical( import BasicTypes import Type import TcRnTypes - +import FunDeps +import qualified TcMType as TcM import TcType import TcErrors import Coercion @@ -18,6 +20,7 @@ import TyCon import TypeRep import Name import Var +import VarEnv ( TidyEnv ) import Outputable import Control.Monad ( unless, when, zipWithM, zipWithM_ ) import MonadUtils @@ -28,6 +31,7 @@ import Bag import HsBinds import TcSMonad +import FastString \end{code} Note [Canonicalisation] @@ -158,7 +162,7 @@ flatten fl (TyConApp tc tys) ; 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 + ; cv <- newCoVar fam_ty rhs_var ; let ct = CFunEqCan { cc_id = cv , cc_flavor = mkWantedFlavor fl -- Always Wanted, not Derived @@ -214,28 +218,35 @@ flattenPred ctxt (EqPred ty1 ty2) %************************************************************************ \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 :: GivenLoc -> [EvVar] -> TcS WorkList canGivens loc givens = do { ccs <- mapM (mkCanonical (Given loc)) givens - ; return (andCCans ccs) } + ; 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 @@ -252,13 +263,15 @@ canClass fl v cn tys -- 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] @@ -326,12 +339,12 @@ happen. \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. + = return emptyWorkList -- 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 @@ -341,8 +354,8 @@ newSCWorkFromFlavored ev orig_flavor cls xis ; mkCanonicals flavor sc_vars } | isEmptyVarSet (tyVarsOfTypes xis) - = return emptyCCan -- Wanteds with no variables yield no deriveds. - -- See Note [Improvement from Ground Wanteds] + = 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 @@ -362,21 +375,25 @@ is_improvement_pty _ = False -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, @@ -404,12 +421,12 @@ canEq fl cv s1 s2 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 let co_orig = mkCoVarCoercion cv @@ -435,9 +452,9 @@ canEq fl cv s1 s2 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) } @@ -459,16 +476,16 @@ canEq fl cv (FunTy s1 t1) (FunTy s2 t2) 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 @@ -488,8 +505,8 @@ canEq fl cv (TyConApp tc1 tys1) (TyConApp tc2 tys2) = -- 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 } @@ -509,9 +526,9 @@ canEq fl cv ty1 ty2 , 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) } @@ -731,8 +748,8 @@ canEqLeaf :: TcsUntouchables 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 newGivenCoVar s2 s1 (mkSymCoercion (mkCoVarCoercion cv)) @@ -770,7 +787,7 @@ canEqLeafOriented fl cv cls1@(FunCls fn tys1) s2 -- cv : F tys1 ; cv_new <- if no_flattening_happened then return cv else if isGiven 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 @@ -778,7 +795,7 @@ canEqLeafOriented fl cv cls1@(FunCls fn tys1) s2 -- cv : F tys1 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) @@ -816,8 +833,8 @@ canEqLeafTyVarLeft fl cv tv s2 -- cv : tv ~ s2 ; cv_new <- if no_flattening_happened then return cv else if isGiven 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') @@ -991,4 +1008,91 @@ a. If this turns out to be impossible, we next try expanding F itself, and so on. +%************************************************************************ +%* * +%* Functional dependencies, instantiation of equations +%* * +%************************************************************************ +When we spot an equality arising from a functional dependency, +we now use that equality (a "wanted") to rewrite the work-item +constraint right away. This avoids two dangers + + Danger 1: If we send the original constraint on down the pipeline + it may react with an instance declaration, and in delicate + situations (when a Given overlaps with an instance) that + may produce new insoluble goals: see Trac #4952 + + Danger 2: If we don't rewrite the constraint, it may re-react + with the same thing later, and produce the same equality + again --> termination worries. + +To achieve this required some refactoring of FunDeps.lhs (nicer +now!). + +\begin{code} +rewriteWithFunDeps :: [Equation] + -> [Xi] -> CtFlavor + -> 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 = unionWorkLists fds + ; if isEmptyWorkList fd_work + then return Nothing + else return (Just (rewritten_xis, cos, fd_work)) } + +instFunDepEqn :: CtFlavor -- Precondition: Only Wanted or Derived + -> Equation + -> TcS [(Int, FlavoredEvVar)] +-- Post: Returns the position index as well as the corresponding FunDep equality +instFunDepEqn fl (FDEqn { fd_qtvs = qtvs, fd_eqs = eqs + , fd_pred1 = d1, fd_pred2 = d2 }) + = do { let tvs = varSetElems qtvs + ; tvs' <- mapM instFlexiTcS tvs + ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs') + ; mapM (do_one subst) eqs } + where + fl' = case fl of + Given _ -> panic "mkFunDepEqns" + Wanted loc -> Wanted (push_ctx loc) + Derived loc -> Derived (push_ctx loc) + + push_ctx loc = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc + + do_one subst (FDEq { fd_pos = i, fd_ty_left = ty1, fd_ty_right = ty2 }) + = do { let sty1 = substTy subst ty1 + sty2 = substTy subst ty2 + ; ev <- newCoVar sty1 sty2 + ; return (i, mkEvVarX ev fl') } + +rewriteDictParams :: [(Int,FlavoredEvVar)] -- A set of coercions : (pos, ty' ~ ty) + -> [Type] -- A sequence of types: tys + -> [(Type,Coercion)] -- Returns : [(ty', co : ty' ~ ty)] +rewriteDictParams param_eqs tys + = zipWith do_one tys [0..] + where + do_one :: Type -> Int -> (Type,Coercion) + do_one ty n = case lookup n param_eqs of + Just wev -> (get_fst_ty wev, mkCoVarCoercion (evVarOf wev)) + Nothing -> (ty,ty) -- Identity + + get_fst_ty wev = case evVarOfPred wev of + EqPred ty1 _ -> ty1 + _ -> panic "rewriteDictParams: non equality fundep" + +mkEqnMsg :: (TcPredType, SDoc) -> (TcPredType, SDoc) -> TidyEnv + -> TcM (TidyEnv, SDoc) +mkEqnMsg (pred1,from1) (pred2,from2) tidy_env + = do { zpred1 <- TcM.zonkTcPredType pred1 + ; zpred2 <- TcM.zonkTcPredType pred2 + ; let { tpred1 = tidyPred tidy_env zpred1 + ; tpred2 = tidyPred tidy_env zpred2 } + ; let msg = vcat [ptext (sLit "When using functional dependencies to combine"), + nest 2 (sep [ppr tpred1 <> comma, nest 2 from1]), + nest 2 (sep [ppr tpred2 <> comma, nest 2 from2])] + ; return (tidy_env, msg) } +\end{code} \ No newline at end of file