X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcCanonical.lhs;h=59d221ed08ae19a5b0bb531531c42ff240a73488;hb=63919ea06f9d4c51ca5119070336b1f9722c9852;hp=961bf45b76e631871da9dcf508768ae2f1ae48c1;hpb=27310213397bb89555bb03585e057ba1b017e895;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs index 961bf45..59d221e 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 + canOccursCheck, canEq, + 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 @@ -376,7 +380,7 @@ 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 +408,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 +439,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 +463,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 +492,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 +513,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) } @@ -683,37 +687,39 @@ classify ty | Just ty' <- tcView ty = OtherCls ty -- See note [Canonical ordering for equality constraints]. -reOrient :: TcsUntouchables -> TypeClassifier -> TypeClassifier -> Bool +reOrient :: CtFlavor -> TypeClassifier -> TypeClassifier -> Bool -- (t1 `reOrient` t2) responds True -- iff we should flip to (t2~t1) -- We try to say False if possible, to minimise evidence generation -- -- Postcondition: After re-orienting, first arg is not OTherCls -reOrient _untch (OtherCls {}) (FunCls {}) = True -reOrient _untch (OtherCls {}) (FskCls {}) = True -reOrient _untch (OtherCls {}) (VarCls {}) = True -reOrient _untch (OtherCls {}) (OtherCls {}) = panic "reOrient" -- One must be Var/Fun +reOrient _fl (OtherCls {}) (FunCls {}) = True +reOrient _fl (OtherCls {}) (FskCls {}) = True +reOrient _fl (OtherCls {}) (VarCls {}) = True +reOrient _fl (OtherCls {}) (OtherCls {}) = panic "reOrient" -- One must be Var/Fun + +reOrient _fl (FunCls {}) (VarCls _tv) = False + -- But consider the following variation: isGiven fl && isMetaTyVar tv -reOrient _untch (FunCls {}) (VarCls {}) = False -- See Note [No touchables as FunEq RHS] in TcSMonad -reOrient _untch (FunCls {}) _ = False -- Fun/Other on rhs +reOrient _fl (FunCls {}) _ = False -- Fun/Other on rhs -reOrient _untch (VarCls {}) (FunCls {}) = True +reOrient _fl (VarCls {}) (FunCls {}) = True -reOrient _untch (VarCls {}) (FskCls {}) = False +reOrient _fl (VarCls {}) (FskCls {}) = False -reOrient _untch (VarCls {}) (OtherCls {}) = False -reOrient _untch (VarCls tv1) (VarCls tv2) +reOrient _fl (VarCls {}) (OtherCls {}) = False +reOrient _fl (VarCls tv1) (VarCls tv2) | isMetaTyVar tv2 && not (isMetaTyVar tv1) = True | otherwise = False -- Just for efficiency, see CTyEqCan invariants -reOrient _untch (FskCls {}) (VarCls tv2) = isMetaTyVar tv2 +reOrient _fl (FskCls {}) (VarCls tv2) = isMetaTyVar tv2 -- Just for efficiency, see CTyEqCan invariants -reOrient _untch (FskCls {}) (FskCls {}) = False -reOrient _untch (FskCls {}) (FunCls {}) = True -reOrient _untch (FskCls {}) (OtherCls {}) = False +reOrient _fl (FskCls {}) (FskCls {}) = False +reOrient _fl (FskCls {}) (FunCls {}) = True +reOrient _fl (FskCls {}) (OtherCls {}) = False ------------------ canEqLeaf :: TcsUntouchables @@ -726,11 +732,11 @@ canEqLeaf :: TcsUntouchables -- Preconditions: -- * one of the two arguments is not OtherCls -- * the two types are not equal (looking through synonyms) -canEqLeaf untch fl cv cls1 cls2 +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)) @@ -742,7 +748,7 @@ canEqLeaf untch fl cv cls1 cls2 = do { traceTcS "canEqLeaf" (ppr (unClassify cls1) $$ ppr (unClassify cls2)) ; canEqLeafOriented fl cv cls1 s2 } where - re_orient = reOrient untch + re_orient = reOrient fl s1 = unClassify cls1 s2 = unClassify cls2 @@ -768,7 +774,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 @@ -776,7 +782,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) @@ -814,8 +820,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') @@ -989,4 +995,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], CanonicalCts)) +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 + 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