X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcCanonical.lhs;h=2cb38a908aba5a41baf25ba54868e97bb3a9b915;hp=7fdb63ed855ea8e19260c204282fcd42319baa23;hb=febf1ced754a3996ac1a5877dcded87828560d1c;hpb=62f76a3cbced691b60f511fb83547a5d62653252 diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs index 7fdb63e..2cb38a9 100644 --- a/compiler/typecheck/TcCanonical.lhs +++ b/compiler/typecheck/TcCanonical.lhs @@ -1,34 +1,38 @@ \begin{code} module TcCanonical( - mkCanonical, mkCanonicals, canWanteds, canGivens, canOccursCheck, canEq, + mkCanonical, mkCanonicals, mkCanonicalFEV, mkCanonicalFEVs, canWanteds, canGivens, + canOccursCheck, canEqToWorkList, + rewriteWithFunDeps ) where #include "HsVersions.h" -import BasicTypes -import Type +import BasicTypes +import Id ( evVarPred ) +import TcErrors import TcRnTypes - +import FunDeps +import qualified TcMType as TcM import TcType -import TcErrors +import Type import Coercion import Class import TyCon import TypeRep import Name import Var +import VarEnv ( TidyEnv ) import Outputable -import Control.Monad ( when, zipWithM ) +import Control.Monad ( unless, when, zipWithM, zipWithM_ ) import MonadUtils import Control.Applicative ( (<|>) ) import VarSet import Bag -import HsBinds - -import Control.Monad ( unless ) -import TcSMonad -- The TcS Monad +import HsBinds +import TcSMonad +import FastString \end{code} Note [Canonicalisation] @@ -89,7 +93,9 @@ 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 :: CtFlavor -> [Type] -> TcS ([Xi], [Coercion], CanonicalCts) -- Coercions :: Xi ~ Type @@ -108,35 +114,35 @@ flatten ctxt ty -- Preserve type synonyms if possible -- We can tell if ty' is function-free by -- whether there are any floated constraints - ; if isEmptyCCan ccs then - return (ty, ty, emptyCCan) + ; if isReflCo co then + return (ty, mkReflCo ty, emptyCCan) else return (xi, co, ccs) } flatten _ v@(TyVarTy _) - = return (v, v, emptyCCan) + = return (v, mkReflCo v, emptyCCan) flatten ctxt (AppTy ty1 ty2) = do { (xi1,co1,c1) <- flatten ctxt ty1 ; (xi2,co2,c2) <- flatten ctxt ty2 - ; return (mkAppTy xi1 xi2, mkAppCoercion co1 co2, c1 `andCCan` c2) } + ; return (mkAppTy xi1 xi2, mkAppCo co1 co2, c1 `andCCan` c2) } flatten ctxt (FunTy ty1 ty2) = do { (xi1,co1,c1) <- flatten ctxt ty1 ; (xi2,co2,c2) <- flatten ctxt ty2 - ; return (mkFunTy xi1 xi2, mkFunCoercion co1 co2, c1 `andCCan` c2) } + ; return (mkFunTy xi1 xi2, mkFunCo co1 co2, c1 `andCCan` c2) } flatten 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,ccs) <- flattenMany fl tys - ; return (mkTyConApp tc xis, mkTyConCoercion tc cos, ccs) } + ; return (mkTyConApp tc xis, mkTyConAppCo tc cos, ccs) } -- 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 @@ -144,35 +150,41 @@ flatten fl (TyConApp tc tys) -- The type function might be *over* saturated -- 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 <- newGivOrDerCoVar 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_ty = mkTyConApp tc xi_args + ; (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 (mkReflCo fam_ty) + ; let ct = CFunEqCan { cc_id = cv + , cc_flavor = fl -- Given + , cc_fun = tc + , cc_tyargs = xi_args + , cc_rhs = rhs_var } + ; let ret_co = mkCoVarCo 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 = mkCoVarCo 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) } - + , foldl AppCo (mkSymCo ret_co + `mkTransCo` mkTyConAppCo tc cos_args) + cos_rest + , ccs `andCCan` ct) } flatten ctxt (PredTy pred) = do { (pred', co, ccs) <- flattenPred ctxt pred @@ -190,22 +202,20 @@ flatten ctxt ty@(ForAllTy {}) tv_set = mkVarSet tvs ; unless (isEmptyBag bad_eqs) (flattenForAllErrorTcS ctxt ty bad_eqs) - ; return (mkForAllTys tvs rho', mkForAllTys tvs co, ccs) } + ; return (mkForAllTys tvs rho', foldr mkForAllCo co tvs, ccs) } --------------- flattenPred :: CtFlavor -> TcPredType -> TcS (TcPredType, Coercion, CanonicalCts) flattenPred ctxt (ClassP cls tys) = do { (tys', cos, ccs) <- flattenMany ctxt tys - ; return (ClassP cls tys', mkClassPPredCo cls cos, ccs) } + ; return (ClassP cls tys', mkPredCo $ ClassP cls cos, ccs) } flattenPred ctxt (IParam nm ty) = do { (ty', co, ccs) <- flatten ctxt ty - ; return (IParam nm ty', mkIParamPredCo nm co, ccs) } --- TODO: Handling of coercions between EqPreds must be revisited once the New Coercion API is ready! + ; return (IParam nm ty', mkPredCo $ IParam nm co, ccs) } flattenPred ctxt (EqPred ty1 ty2) = do { (ty1', co1, ccs1) <- flatten ctxt ty1 ; (ty2', co2, ccs2) <- flatten ctxt ty2 - ; return (EqPred ty1' ty2', mkEqPredCo co1 co2, ccs1 `andCCan` ccs2) } - + ; return (EqPred ty1' ty2', mkPredCo $ EqPred co1 co2, ccs1 `andCCan` ccs2) } \end{code} %************************************************************************ @@ -215,49 +225,61 @@ flattenPred ctxt (EqPred ty1 ty2) %************************************************************************ \begin{code} -canWanteds :: [WantedEvVar] -> TcS CanonicalCts -canWanteds = fmap andCCans . mapM (\(WantedEvVar 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 WorkList +canGivens loc givens = do { ccs <- mapM (mkCanonical (Given loc GivenOrig)) givens + ; return (unionWorkLists ccs) } -canGivens :: GivenLoc -> [EvVar] -> TcS CanonicalCts -canGivens loc givens = do { ccs <- mapM (mkCanonical (Given loc)) givens - ; return (andCCans ccs) } +mkCanonicals :: CtFlavor -> [EvVar] -> TcS WorkList +mkCanonicals fl vs = fmap unionWorkLists (mapM (mkCanonical fl) vs) -mkCanonicals :: CtFlavor -> [EvVar] -> TcS CanonicalCts -mkCanonicals fl vs = fmap andCCans (mapM (mkCanonical fl) vs) +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 + ; let no_flattening_happened = all isReflCo cos + dict_co = mkTyConAppCo (classTyCon cn) cos + ; 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 - ; if isWanted fl - then setDictBind v (EvCast v' dict_co) - else setDictBind v' (EvCast v (mkSymCoercion dict_co)) + ; when (isWanted fl) $ setDictBind v (EvCast v' dict_co) + ; when (isGivenOrSolved fl) $ setDictBind v' (EvCast v (mkSymCo 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] @@ -272,34 +294,41 @@ For Givens: We add all their superclasses as Givens. For Wanteds: - Generally speaking, we want to be able to add derived - superclasses of unsolved wanteds, and wanteds that have been - partially being solved via an instance. This is important to be - able to simplify the inferred constraints more (and to allow - for recursive dictionaries, less importantly). + Generally speaking we want to be able to add superclasses of + wanteds for two reasons: - Example: Inferred wanted constraint is (Eq a, Ord a), but we'd - only like to quantify over Ord a, hence we would like to be - able to add the superclass of Ord a as Derived and use it to - solve the wanted Eq a. + (1) Oportunities for improvement. Example: + class (a ~ b) => C a b + Wanted constraint is: C alpha beta + We'd like to simply have C alpha alpha. Similar + situations arise in relation to functional dependencies. + + (2) To have minimal constraints to quantify over: + For instance, if our wanted constraint is (Eq a, Ord a) + we'd only like to quantify over Ord a. -For Deriveds: - Deriveds either arise as wanteds that have been partially - solved, or as superclasses of other wanteds or deriveds. Hence, - their superclasses must be already there so we must do nothing - at al. + To deal with (1) above we only add the superclasses of wanteds + which may lead to improvement, that is: equality superclasses or + superclasses with functional dependencies. - DV: In fact, it is probably true that the canonicaliser is - *never* asked to canonicalise Derived dictionaries + We deal with (2) completely independently in TcSimplify. See + Note [Minimize by SuperClasses] in TcSimplify. -There is one disadvantage to this. Suppose the wanted constraints are -(Num a, Num a). Then we'll add all the superclasses of both during -canonicalisation, only to eliminate them later when they are -interacted. That seems like a waste of work. Still, it's simple. + + Moreover, in all cases the extra improvement constraints are + Derived. Derived constraints have an identity (for now), but + we don't do anything with their evidence. For instance they + are never used to rewrite other constraints. + + See also [New Wanted Superclass Work] in TcInteract. + + +For Deriveds: + We do nothing. 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 @@ -317,39 +346,66 @@ By adding superclasses definitely only once, during canonicalisation, this situa 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 - = do { let (tyvars, sc_theta, _, _) = classBigSig cls - sc_theta1 = substTheta (zipTopTvSubst tyvars xis) sc_theta - ; sc_vars <- zipWithM inst_one sc_theta1 [0..] - ; mkCanonicals flavor sc_vars } - -- NB: Since there is a call to mkCanonicals, - -- this will add *recursively* all superclasses - where - inst_one pred n = newGivOrDerEvVar pred (EvSuperClass ev n) - flavor = case orig_flavor of - Given loc -> Given loc - Wanted loc -> Derived loc DerSC - Derived {} -> orig_flavor - -- NB: the non-immediate superclasses will show up as - -- Derived, and we want their superclasses too! - -canIP :: CtFlavor -> EvVar -> IPName Name -> TcType -> TcS CanonicalCts + | isDerived orig_flavor + = 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 + impr_theta = filter is_improvement_pty sc_rec_theta + Wanted wloc = orig_flavor + ; der_ids <- mapM newDerivedId impr_theta + ; mkCanonicals (Derived wloc) der_ids } + + +is_improvement_pty :: PredType -> Bool +-- Either it's an equality, or has some functional dependency +is_improvement_pty (EqPred {}) = True +is_improvement_pty (ClassP cls _ty) = not $ null fundeps + where (_,fundeps,_,_,_,_) = classExtraBigSig cls +is_improvement_pty _ = False + + + + +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 + | eqType 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 (mkReflCo ty1)) ; return emptyCCan } -- If one side is a variable, orient and flatten, @@ -363,94 +419,57 @@ canEq fl cv ty1 ty2@(TyVarTy {}) ; canEqLeaf untch fl cv (classify ty1) (classify ty2) } -- NB: don't use VarCls directly because tv1 or tv2 may be scolems! -canEq fl cv (TyConApp fn tys) ty2 - | isSynFamilyTyCon fn, length tys == tyConArity fn - = do { untch <- getUntouchables - ; canEqLeaf untch fl cv (FunCls fn tys) (classify ty2) } -canEq fl cv ty1 (TyConApp fn tys) - | isSynFamilyTyCon fn, length tys == tyConArity fn - = do { untch <- getUntouchables - ; canEqLeaf untch fl cv (classify ty1) (FunCls fn tys) } - -canEq fl cv s1 s2 - | Just (t1a,t1b,t1c) <- splitCoPredTy_maybe s1, - Just (t2a,t2b,t2c) <- splitCoPredTy_maybe s2 - = do { (v1,v2,v3) <- if isWanted fl then - do { v1 <- newWantedCoVar t1a t2a - ; v2 <- newWantedCoVar t1b t2b - ; v3 <- newWantedCoVar t1c t2c - ; let res_co = mkCoPredCo (mkCoVarCoercion v1) - (mkCoVarCoercion v2) (mkCoVarCoercion v3) - ; setWantedCoBind cv res_co - ; return (v1,v2,v3) } - else let co_orig = mkCoVarCoercion cv - coa = mkCsel1Coercion co_orig - cob = mkCsel2Coercion co_orig - coc = mkCselRCoercion co_orig - in do { v1 <- newGivOrDerCoVar t1a t2a coa - ; v2 <- newGivOrDerCoVar t1b t2b cob - ; v3 <- newGivOrDerCoVar t1c t2c coc - ; return (v1,v2,v3) } - ; cc1 <- canEq fl v1 t1a t2a - ; cc2 <- canEq fl v2 t1b t2b - ; cc3 <- canEq fl v3 t1c t2c - ; return (cc1 `andCCan` cc2 `andCCan` cc3) } - - -- Split up an equality between function types into two equalities. 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 $ - mkFunCoercion (mkCoVarCoercion argv) (mkCoVarCoercion resv) + do { argv <- newCoVar s1 s2 + ; resv <- newCoVar t1 t2 + ; setCoBind cv $ + mkFunCo (mkCoVarCo argv) (mkCoVarCo resv) ; return (argv,resv) } - else let [arg,res] = decomposeCo 2 (mkCoVarCoercion cv) - in do { argv <- newGivOrDerCoVar s1 s2 arg - ; resv <- newGivOrDerCoVar t1 t2 res - ; return (argv,resv) } + else if isGivenOrSolved fl then + let [arg,res] = decomposeCo 2 (mkCoVarCo cv) + in do { argv <- newGivenCoVar s1 s2 arg + ; resv <- newGivenCoVar t1 t2 res + ; return (argv,resv) } + + else -- Derived + do { argv <- newDerivedId (EqPred s1 s2) + ; resv <- newDerivedId (EqPred t1 t2) + ; return (argv,resv) } + ; cc1 <- canEq fl argv s1 s2 -- inherit original kinds and locations ; cc2 <- canEq fl resv t1 t2 ; return (cc1 `andCCan` cc2) } -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) - ; 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) - ; andCCans <$> zipWith3M (canEq fl) vs tys1 tys2 - } - else return emptyCCan - -- How to decompose given dictionary (and implicit parameter) coercions? - -- You may think that the following is right: - -- let cos = decomposeCo (length tys1) (mkCoVarCoercion cv) - -- in zipWith3M newGivOrDerCoVar tys1 tys2 cos - -- But this assumes that the coercion is a type constructor-based - -- coercion, and not a PredTy (ClassP cn cos) coercion. So we chose - -- to not decompose these coercions. We have to get back to this - -- when we clean up the Coercion API. +canEq fl cv (TyConApp fn tys) ty2 + | isSynFamilyTyCon fn, length tys == tyConArity fn + = do { untch <- getUntouchables + ; canEqLeaf untch fl cv (FunCls fn tys) (classify ty2) } +canEq fl cv ty1 (TyConApp fn tys) + | isSynFamilyTyCon fn, length tys == tyConArity fn + = do { untch <- getUntouchables + ; canEqLeaf untch fl cv (classify ty1) (FunCls fn tys) } canEq fl cv (TyConApp tc1 tys1) (TyConApp tc2 tys2) - | isAlgTyCon tc1 && isAlgTyCon tc2 + | isDecomposableTyCon tc1 && isDecomposableTyCon tc2 , tc1 == tc2 , length tys1 == length tys2 = -- Generate equalities for each of the corresponding arguments - do { argsv <- if isWanted fl then - do { argsv <- zipWithM newWantedCoVar tys1 tys2 - ; setWantedCoBind cv $ mkTyConCoercion tc1 (map mkCoVarCoercion argsv) - ; return argsv } - else - let cos = decomposeCo (length tys1) (mkCoVarCoercion cv) - in zipWith3M newGivOrDerCoVar tys1 tys2 cos + do { argsv + <- if isWanted fl then + do { argsv <- zipWithM newCoVar tys1 tys2 + ; setCoBind cv $ + mkTyConAppCo tc1 (map mkCoVarCo argsv) + ; return argsv } + else if isGivenOrSolved fl then + let cos = decomposeCo (length tys1) (mkCoVarCo cv) + in zipWith3M newGivenCoVar tys1 tys2 cos + + else -- Derived + zipWithM (\t1 t2 -> newDerivedId (EqPred t1 t2)) tys1 tys2 + ; andCCans <$> zipWith3M (canEq fl) argsv tys1 tys2 } -- See Note [Equality between type applications] @@ -458,26 +477,29 @@ canEq fl cv (TyConApp tc1 tys1) (TyConApp tc2 tys2) canEq fl cv ty1 ty2 | Just (s1,t1) <- tcSplitAppTy_maybe ty1 , Just (s2,t2) <- tcSplitAppTy_maybe ty2 - = do { (cv1,cv2) <- - if isWanted fl - then do { cv1 <- newWantedCoVar s1 s2 - ; cv2 <- newWantedCoVar t1 t2 - ; setWantedCoBind cv $ - mkAppCoercion (mkCoVarCoercion cv1) (mkCoVarCoercion cv2) - ; return (cv1,cv2) } - else let co1 = mkLeftCoercion $ mkCoVarCoercion cv - co2 = mkRightCoercion $ mkCoVarCoercion cv - in do { cv1 <- newGivOrDerCoVar s1 s2 co1 - ; cv2 <- newGivOrDerCoVar t1 t2 co2 - ; return (cv1,cv2) } - ; cc1 <- canEq fl cv1 s1 s2 - ; cc2 <- canEq fl cv2 t1 t2 - ; return (cc1 `andCCan` cc2) } - -canEq fl _ s1@(ForAllTy {}) s2@(ForAllTy {}) + = if isWanted fl + then do { cv1 <- newCoVar s1 s2 + ; cv2 <- newCoVar t1 t2 + ; setCoBind cv $ + mkAppCo (mkCoVarCo cv1) (mkCoVarCo cv2) + ; cc1 <- canEq fl cv1 s1 s2 + ; cc2 <- canEq fl cv2 t1 t2 + ; return (cc1 `andCCan` cc2) } + + else if isDerived fl + then do { cv1 <- newDerivedId (EqPred s1 s2) + ; cv2 <- newDerivedId (EqPred t1 t2) + ; cc1 <- canEq fl cv1 s1 s2 + ; cc2 <- canEq fl cv2 t1 t2 + ; return (cc1 `andCCan` cc2) } + + else return emptyCCan -- We cannot decompose given applications + -- because we no longer have 'left' and 'right' + +canEq fl cv s1@(ForAllTy {}) s2@(ForAllTy {}) | tcIsForAllTy s1, tcIsForAllTy s2, Wanted {} <- fl - = canEqFailure fl s1 s2 + = canEqFailure fl cv | otherwise = do { traceTcS "Ommitting decomposition of given polytype equality" (pprEq s1 s2) ; return emptyCCan } @@ -485,12 +507,10 @@ canEq fl _ s1@(ForAllTy {}) s2@(ForAllTy {}) -- Finally expand any type synonym applications. canEq fl cv ty1 ty2 | Just ty1' <- tcView ty1 = canEq fl cv ty1' ty2 canEq fl cv ty1 ty2 | Just ty2' <- tcView ty2 = canEq fl cv ty1 ty2' -canEq fl _ ty1 ty2 = canEqFailure fl ty1 ty2 +canEq fl cv _ _ = canEqFailure fl cv -canEqFailure :: CtFlavor -> Type -> Type -> TcS CanonicalCts -canEqFailure fl ty1 ty2 - = do { addErrorTcS MisMatchError fl ty1 ty2 - ; return emptyCCan } +canEqFailure :: CtFlavor -> EvVar -> TcS CanonicalCts +canEqFailure fl cv = return (singleCCan (mkFrozenError fl cv)) \end{code} Note [Equality between type applications] @@ -629,37 +649,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 @@ -672,19 +694,23 @@ 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 $ mkSymCo (mkCoVarCo cv') ; return cv' } - else newGivOrDerCoVar s2 s1 (mkSymCoercion (mkCoVarCoercion cv)) + else if isGivenOrSolved fl then + newGivenCoVar s2 s1 (mkSymCo (mkCoVarCo cv)) + else -- Derived + newDerivedId (EqPred s2 s1) ; canEqLeafOriented fl cv' cls2 s1 } | otherwise - = canEqLeafOriented fl cv cls1 s2 + = 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 @@ -695,8 +721,8 @@ canEqLeafOriented :: CtFlavor -> CoVar canEqLeafOriented fl cv cls1@(FunCls fn tys1) s2 -- cv : F tys1 | let k1 = kindAppResult (tyConKind fn) tys1, let k2 = typeKind s2, - isGiven fl && not (k1 `compatKind` k2) -- Establish the kind invariant for CFunEqCan - = addErrorTcS KindError fl (unClassify cls1) s2 >> return emptyCCan + not (k1 `compatKind` k2) -- Establish the kind invariant for CFunEqCan + = canEqFailure fl cv -- Eagerly fails, see Note [Kind errors] in TcInteract | otherwise @@ -706,25 +732,22 @@ canEqLeafOriented fl cv cls1@(FunCls fn tys1) s2 -- cv : F tys1 ; (xi2, co2, ccs2) <- flatten fl s2 -- Flatten entire RHS -- 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 - else do { cv' <- newWantedCoVar (unClassify (FunCls fn xis1)) xi2 + no_flattening_happened = all isReflCo (co2:cos1) + ; cv_new <- if no_flattening_happened then return cv + else if isGivenOrSolved fl then return cv + else if isWanted fl then + do { cv' <- newCoVar (unClassify (FunCls fn xis1)) xi2 -- cv' : F xis ~ xi2 - ; let -- fun_co :: F xis1 ~ F tys1 - fun_co = mkTyConCoercion fn cos1 + ; let -- fun_co :: F xis1 ~ F tys1 + fun_co = mkTyConAppCo fn cos1 -- want_co :: F tys1 ~ s2 - want_co = mkSymCoercion fun_co - `mkTransCoercion` mkCoVarCoercion cv' - `mkTransCoercion` co2 - -- der_co :: F xis1 ~ xi2 - der_co = fun_co - `mkTransCoercion` mkCoVarCoercion cv - `mkTransCoercion` mkSymCoercion co2 - ; if isWanted fl - then setWantedCoBind cv want_co - else setWantedCoBind cv' der_co - ; return cv' } + want_co = mkSymCo fun_co + `mkTransCo` mkCoVarCo cv' + `mkTransCo` co2 + ; setCoBind cv want_co + ; return cv' } + else -- Derived + newDerivedId (EqPred (unClassify (FunCls fn xis1)) xi2) ; let final_cc = CFunEqCan { cc_id = cv_new , cc_flavor = fl @@ -744,8 +767,8 @@ canEqLeafOriented _ cv (OtherCls ty1) ty2 canEqLeafTyVarLeft :: CtFlavor -> CoVar -> TcTyVar -> TcType -> TcS CanonicalCts -- Establish invariants of CTyEqCans canEqLeafTyVarLeft fl cv tv s2 -- cv : tv ~ s2 - | isGiven fl && not (k1 `compatKind` k2) -- Establish the kind invariant for CTyEqCan - = addErrorTcS KindError fl (mkTyVarTy tv) s2 >> return emptyCCan + | not (k1 `compatKind` k2) -- Establish the kind invariant for CTyEqCan + = canEqFailure fl cv -- Eagerly fails, see Note [Kind errors] in TcInteract | otherwise = do { (xi2, co, ccs2) <- flatten fl s2 -- Flatten RHS co : xi2 ~ s2 @@ -753,17 +776,17 @@ canEqLeafTyVarLeft fl cv tv s2 -- cv : tv ~ s2 -- unfolded version of the RHS, if we had to -- unfold any type synonyms to get rid of tv. ; case mxi2' of { - Nothing -> addErrorTcS OccCheckError fl (mkTyVarTy tv) xi2 >> return emptyCCan ; + 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 - else do { cv' <- newWantedCoVar (mkTyVarTy tv) xi2' -- cv' : tv ~ xi2 - ; if isWanted fl - then setWantedCoBind cv (mkCoVarCoercion cv' `mkTransCoercion` co) - else setWantedCoBind cv' (mkCoVarCoercion cv `mkTransCoercion` - mkSymCoercion co) - ; return cv' } + do { let no_flattening_happened = isReflCo co + ; cv_new <- if no_flattening_happened then return cv + else if isGivenOrSolved fl then return cv + else if isWanted fl then + do { cv' <- newCoVar (mkTyVarTy tv) xi2' -- cv' : tv ~ xi2 + ; setCoBind cv (mkCoVarCo cv' `mkTransCo` co) + ; return cv' } + else -- Derived + newDerivedId (EqPred (mkTyVarTy tv) xi2') ; return $ ccs2 `extendCCans` CTyEqCan { cc_id = cv_new , cc_flavor = fl @@ -824,7 +847,7 @@ expandAway tv (FunTy ty1 ty2) expandAway tv ty@(ForAllTy {}) = let (tvs,rho) = splitForAllTys ty tvs_knds = map tyVarKind tvs - in if tv `elemVarSet` tyVarsOfTypes tvs_knds then + in if tv `elemVarSet` tyVarsOfTypes tvs_knds then -- Can't expand away the kinds unless we create -- fresh variables which we don't want to do at this point. Nothing @@ -934,4 +957,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 = Type.substTy subst ty1 + sty2 = Type.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, mkCoVarCo (evVarOf wev)) + Nothing -> (ty, mkReflCo 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