From: Dimitrios Vytiniotis Date: Wed, 18 May 2011 13:12:46 +0000 (+0100) Subject: Merge remote branch 'origin/master' X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=commitdiff_plain;h=febf1ced754a3996ac1a5877dcded87828560d1c;hp=-c Merge remote branch 'origin/master' Fixed conflicts in: compiler/typecheck/TcCanonical.lhs compiler/typecheck/TcErrors.lhs compiler/typecheck/TcInteract.lhs --- febf1ced754a3996ac1a5877dcded87828560d1c diff --combined compiler/typecheck/Inst.lhs index 05edde4,5474cfa..378bbd6 --- a/compiler/typecheck/Inst.lhs +++ b/compiler/typecheck/Inst.lhs @@@ -46,11 -46,10 +46,10 @@@ import TcMTyp import TcType import Class import Unify import HscTypes import Id import Name - import Var + import Var ( Var, TyVar, EvVar, varType, setVarType ) import VarEnv import VarSet import PrelNames @@@ -212,11 -211,8 +211,8 @@@ instCallConstraints _ [] = return idHsW instCallConstraints origin (EqPred ty1 ty2 : preds) -- Try short-cut = do { traceTc "instCallConstraints" $ ppr (EqPred ty1 ty2) - ; coi <- unifyType ty1 ty2 + ; co <- unifyType ty1 ty2 ; co_fn <- instCallConstraints origin preds - ; let co = case coi of - IdCo ty -> ty - ACo co -> co ; return (co_fn <.> WpEvApp (EvCoercion co)) } instCallConstraints origin (pred : preds) @@@ -551,7 -547,7 +547,7 @@@ tidyFlavoredEvVar env (EvVarX v fl = EvVarX (tidyEvVar env v) (tidyFlavor env fl) tidyFlavor :: TidyEnv -> CtFlavor -> CtFlavor -tidyFlavor env (Given loc) = Given (tidyGivenLoc env loc) +tidyFlavor env (Given loc gk) = Given (tidyGivenLoc env loc) gk tidyFlavor _ fl = fl tidyGivenLoc :: TidyEnv -> GivenLoc -> GivenLoc @@@ -595,8 -591,8 +591,8 @@@ substFlavoredEvVar subst (EvVarX v fl = EvVarX (substEvVar subst v) (substFlavor subst fl) substFlavor :: TvSubst -> CtFlavor -> CtFlavor -substFlavor subst (Given loc) = Given (substGivenLoc subst loc) -substFlavor _ fl = fl +substFlavor subst (Given loc gk) = Given (substGivenLoc subst loc) gk +substFlavor _ fl = fl substGivenLoc :: TvSubst -> GivenLoc -> GivenLoc substGivenLoc subst (CtLoc skol span ctxt) = CtLoc (substSkolemInfo subst skol) span ctxt @@@ -605,4 -601,4 +601,4 @@@ substSkolemInfo :: TvSubst -> SkolemInf substSkolemInfo subst (SigSkol cx ty) = SigSkol cx (substTy subst ty) substSkolemInfo subst (InferSkol ids) = InferSkol (mapSnd (substTy subst) ids) substSkolemInfo _ info = info - \end{code} + \end{code} diff --combined compiler/typecheck/TcCanonical.lhs index 711c356,44cff5e..2cb38a9 --- a/compiler/typecheck/TcCanonical.lhs +++ b/compiler/typecheck/TcCanonical.lhs @@@ -8,12 -8,13 +8,13 @@@ module TcCanonical #include "HsVersions.h" import BasicTypes - import Type + 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 @@@ -92,9 -93,7 +93,9 @@@ expansions contain any type function ap 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 @@@ -113,35 -112,35 +114,35 @@@ flatten ctxt t -- Preserve type synonyms if possible -- We can tell if ty' is function-free by -- whether there are any floated constraints - ; if isIdentityCoercion co then - return (ty, ty, emptyCCan) - ; if isEmptyCCan ccs then ++ ; 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 @@@ -149,43 -148,38 +150,42 @@@ -- 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 - fam_co = mkReflCo 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 $ (mkCoVarCo cv, rhs_var, ct) } - else -- 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 } - ; return $ (mkCoVarCo 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 fam_co ++ ; 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 = mkCoVarCoercion cv ++ ; 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 = mkCoVarCoercion cv ++ ; 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 - , foldl mkAppCo - (mkSymCo ret_co - `mkTransCo` mkTyConAppCo 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 ; return (PredTy pred', co, ccs) } @@@ -202,22 -196,20 +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} %************************************************************************ @@@ -231,7 -223,7 +229,7 @@@ canWanteds :: [WantedEvVar] -> TcS Work 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)) givens +canGivens loc givens = do { ccs <- mapM (mkCanonical (Given loc GivenOrig)) givens ; return (unionWorkLists ccs) } mkCanonicals :: CtFlavor -> [EvVar] -> TcS WorkList @@@ -247,7 -239,6 +245,7 @@@ mkCanonicalFEVs = foldrBagM canon_one e 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 -> canClassToWorkList fl ev clas tys @@@ -258,15 -249,15 +256,15 @@@ 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 = all isIdentityCoercion cos - dict_co = mkTyConCoercion (classTyCon cn) cos - ; let no_flattening_happened = isEmptyCCan ccs ++ ; let no_flattening_happened = all isReflCo cos + dict_co = mkTyConAppCo (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 (isGivenOrSolved fl) $ setDictBind v' (EvCast v (mkSymCoercion dict_co)) - ; when (isGiven fl) $ setDictBind v' (EvCast v (mkSymCo dict_co)) ++ ; when (isGivenOrSolved fl) $ setDictBind v' (EvCast v (mkSymCo dict_co)) -- NB: No more setting evidence for derived now ; return v' } @@@ -330,7 -321,7 +328,7 @@@ For Deriveds 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 @@@ -356,18 -347,14 +354,18 @@@ newSCWorkFromFlavored ev orig_flavor cl = 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 - 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) + | 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] @@@ -405,9 -392,9 +403,9 @@@ canEqToWorkList fl cv ty1 ty2 = do { ct 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) (setCoBind cv ty1) + = do { when (isWanted fl) (setCoBind cv (mkReflCo ty1)) ; return emptyCCan } -- If one side is a variable, orient and flatten, @@@ -421,47 -408,6 +419,6 @@@ 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 -- Wanted - do { v1 <- newCoVar t1a t2a - ; v2 <- newCoVar t1b t2b - ; v3 <- newCoVar t1c t2c - ; let res_co = mkCoPredCo (mkCoVarCoercion v1) - (mkCoVarCoercion v2) (mkCoVarCoercion v3) - ; setCoBind cv res_co - ; return (v1,v2,v3) } - else if isGivenOrSolved fl then -- Given - let co_orig = mkCoVarCoercion cv - coa = mkCsel1Coercion co_orig - cob = mkCsel2Coercion co_orig - coc = mkCselRCoercion co_orig - in do { v1 <- newGivenCoVar t1a t2a coa - ; v2 <- newGivenCoVar t1b t2b cob - ; v3 <- newGivenCoVar t1c t2c coc - ; return (v1,v2,v3) } - else -- Derived - do { v1 <- newDerivedId (EqPred t1a t2a) - ; v2 <- newDerivedId (EqPred t1b t2b) - ; v3 <- newDerivedId (EqPred t1c t2c) - ; 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) <- @@@ -469,11 -415,11 +426,10 @@@ do { argv <- newCoVar s1 s2 ; resv <- newCoVar t1 t2 ; setCoBind cv $ - mkFunCoercion (mkCoVarCoercion argv) (mkCoVarCoercion resv) + mkFunCo (mkCoVarCo argv) (mkCoVarCo resv) ; return (argv,resv) } -- - else if isGiven fl then + else if isGivenOrSolved fl then - let [arg,res] = decomposeCo 2 (mkCoVarCoercion cv) + let [arg,res] = decomposeCo 2 (mkCoVarCo cv) in do { argv <- newGivenCoVar s1 s2 arg ; resv <- newGivenCoVar t1 t2 res ; return (argv,resv) } @@@ -487,33 -433,17 +443,17 @@@ ; 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 <- 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 newCoVar tys1 tys2 - ; setCoBind 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 @@@ -521,11 -451,11 +461,10 @@@ <- if isWanted fl then do { argsv <- zipWithM newCoVar tys1 tys2 ; setCoBind cv $ - mkTyConCoercion tc1 (map mkCoVarCoercion argsv) - ; return argsv } - - else if isGivenOrSolved fl then - let cos = decomposeCo (length tys1) (mkCoVarCoercion cv) + mkTyConAppCo tc1 (map mkCoVarCo argsv) - ; return argsv } - - else if isGiven fl then - let cos = decomposeCo (length tys1) (mkCoVarCo cv) ++ ; return argsv } ++ else if isGivenOrSolved fl then ++ let cos = decomposeCo (length tys1) (mkCoVarCo cv) in zipWith3M newGivenCoVar tys1 tys2 cos else -- Derived @@@ -538,28 -468,24 +477,24 @@@ 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 <- newCoVar s1 s2 - ; cv2 <- newCoVar t1 t2 - ; setCoBind cv $ - mkAppCoercion (mkCoVarCoercion cv1) (mkCoVarCoercion cv2) - ; return (cv1,cv2) } - - else if isGivenOrSolved fl then - let co1 = mkLeftCoercion $ mkCoVarCoercion cv - co2 = mkRightCoercion $ mkCoVarCoercion cv - in do { cv1 <- newGivenCoVar s1 s2 co1 - ; cv2 <- newGivenCoVar t1 t2 co2 - ; return (cv1,cv2) } - else -- Derived - do { cv1 <- newDerivedId (EqPred s1 s2) - ; cv2 <- newDerivedId (EqPred t1 t2) - ; return (cv1,cv2) } - - ; cc1 <- canEq fl cv1 s1 s2 - ; cc2 <- canEq fl cv2 t1 t2 - ; return (cc1 `andCCan` cc2) } + = 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, @@@ -763,10 -689,10 +698,10 @@@ canEqLeaf _untch fl cv cls1 cls | cls1 `re_orient` cls2 = do { cv' <- if isWanted fl then do { cv' <- newCoVar s2 s1 - ; setCoBind cv $ mkSymCoercion (mkCoVarCoercion cv') + ; setCoBind cv $ mkSymCo (mkCoVarCo cv') ; return cv' } - else if isGiven fl then + else if isGivenOrSolved fl then - newGivenCoVar s2 s1 (mkSymCoercion (mkCoVarCoercion cv)) + newGivenCoVar s2 s1 (mkSymCo (mkCoVarCo cv)) else -- Derived newDerivedId (EqPred s2 s1) ; canEqLeafOriented fl cv' cls2 s1 } @@@ -797,18 -723,18 +732,18 @@@ canEqLeafOriented fl cv cls1@(FunCls f ; (xi2, co2, ccs2) <- flatten fl s2 -- Flatten entire RHS -- co2 :: xi2 ~ s2 ; let ccs = ccs1 `andCCan` ccs2 - no_flattening_happened = all isIdentityCoercion (co2:cos1) - no_flattening_happened = isEmptyCCan ccs - ; cv_new <- if no_flattening_happened then return cv - else if isGiven fl then return cv ++ 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 + fun_co = mkTyConAppCo fn cos1 -- want_co :: F tys1 ~ s2 - want_co = mkSymCoercion fun_co - `mkTransCoercion` mkCoVarCoercion cv' - `mkTransCoercion` co2 + want_co = mkSymCo fun_co + `mkTransCo` mkCoVarCo cv' + `mkTransCo` co2 ; setCoBind cv want_co ; return cv' } else -- Derived @@@ -843,12 -769,12 +778,12 @@@ canEqLeafTyVarLeft fl cv tv s2 - ; case mxi2' of { Nothing -> canEqFailure fl cv ; Just xi2' -> - do { let no_flattening_happened = isIdentityCoercion co - do { let no_flattening_happened = isEmptyCCan ccs2 - ; cv_new <- if no_flattening_happened then return cv - else if isGiven fl then 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 (mkCoVarCoercion cv' `mkTransCoercion` co) + ; setCoBind cv (mkCoVarCo cv' `mkTransCo` co) ; return cv' } else -- Derived newDerivedId (EqPred (mkTyVarTy tv) xi2') @@@ -912,7 -838,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 @@@ -1071,15 -997,15 +1006,15 @@@ instFunDepEqn fl (FDEqn { fd_qtvs = qtv ; 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) 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 + = do { let sty1 = Type.substTy subst ty1 + sty2 = Type.substTy subst ty2 ; ev <- newCoVar sty1 sty2 ; return (i, mkEvVarX ev fl') } @@@ -1091,8 -1017,8 +1026,8 @@@ rewriteDictParams param_eqs ty 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 + 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 diff --combined compiler/typecheck/TcErrors.lhs index 0383e76,0d0a9f8..b199053 --- a/compiler/typecheck/TcErrors.lhs +++ b/compiler/typecheck/TcErrors.lhs @@@ -16,15 -16,12 +16,13 @@@ import TcSMona import TcType import TypeRep import Type( isTyVarTy ) +import Unify ( tcMatchTys ) - import Inst import InstEnv import TyCon import Name import NameEnv - import Id ( idType ) + import Id ( idType, evVarPred ) import Var import VarSet import VarEnv @@@ -107,7 -104,7 +105,7 @@@ reportTidyWanteds ctxt (WC { wc_flat = -- because they are unconditionally wrong -- Moreover, if any of the insolubles are givens, stop right there -- ignoring nested errors, because the code is inaccessible - = do { let (given, other) = partitionBag (isGiven . evVarX) insols + = do { let (given, other) = partitionBag (isGivenOrSolved . evVarX) insols insol_implics = filterBag ic_insol implics ; if isEmptyBag given then do { mapBagM_ (reportInsoluble ctxt) other @@@ -155,8 -152,7 +153,8 @@@ reportInsoluble ctxt (EvVarX ev flav | otherwise = pprPanic "reportInsoluble" (pprEvVarWithType ev) where - inaccessible_msg | Given loc <- flav + inaccessible_msg | Given loc GivenOrig <- flav + -- If a GivenSolved then we should not report inaccessible code = hang (ptext (sLit "Inaccessible code in")) 2 (ppr (ctLocOrigin loc)) | otherwise = empty @@@ -225,7 -221,7 +223,7 @@@ pprWithArising ev_var where first_loc = evVarX (head ev_vars) ppr_one (EvVarX v loc) - = parens (pprPred (evVarPred v)) <+> pprArisingAt loc + = parens (pprPredTy (evVarPred v)) <+> pprArisingAt loc addErrorReport :: ReportErrCtxt -> SDoc -> TcM () addErrorReport ctxt msg = addErrTcM (cec_tidy ctxt, msg $$ cec_extra ctxt) @@@ -302,8 -298,8 +300,8 @@@ getWantedEqExtra (TypeEqOrigin (UnifyOr ty1 ty2 -- If the types in the error message are the same as the types we are unifying, -- don't add the extra expected/actual message - | act `tcEqType` ty1 && exp `tcEqType` ty2 = empty - | exp `tcEqType` ty1 && act `tcEqType` ty2 = empty + | act `eqType` ty1 && exp `eqType` ty2 = empty + | exp `eqType` ty1 && act `eqType` ty2 = empty | otherwise = mkExpectedActualMsg act exp getWantedEqExtra orig _ _ = pprArising orig @@@ -422,18 -418,18 +420,18 @@@ couldNotDeduce :: [([EvVar], GivenLoc) couldNotDeduce givens (wanteds, orig) = vcat [ hang (ptext (sLit "Could not deduce") <+> pprTheta wanteds) 2 (pprArising orig) - , vcat pp_givens ] - where - pp_givens - = case givens of + , vcat (pp_givens givens)] + +pp_givens :: [([EvVar], GivenLoc)] -> [SDoc] +pp_givens givens + = case givens of [] -> [] (g:gs) -> ppr_given (ptext (sLit "from the context")) g : map (ppr_given (ptext (sLit "or from"))) gs - - ppr_given herald (gs,loc) - = hang (herald <+> pprEvVarTheta gs) - 2 (sep [ ptext (sLit "bound by") <+> ppr (ctLocOrigin loc) - , ptext (sLit "at") <+> ppr (ctLocSpan loc)]) + where ppr_given herald (gs,loc) + = hang (herald <+> pprEvVarTheta gs) + 2 (sep [ ptext (sLit "bound by") <+> ppr (ctLocOrigin loc) + , ptext (sLit "at") <+> ppr (ctLocSpan loc)]) addExtraInfo :: ReportErrCtxt -> TcType -> TcType -> ReportErrCtxt -- Add on extra info about the types themselves @@@ -576,61 -572,21 +574,61 @@@ reportOverlap ctxt inst_envs orig pred@ mk_overlap_msg (matches, unifiers) = ASSERT( not (null matches) ) vcat [ addArising orig (ptext (sLit "Overlapping instances for") - <+> pprPred pred) + <+> pprPredTy pred) , sep [ptext (sLit "Matching instances") <> colon, nest 2 (vcat [pprInstances ispecs, pprInstances unifiers])] + + , if not (null overlapping_givens) then + sep [ptext (sLit "Matching givens (or their superclasses)") <> colon, nest 2 (vcat overlapping_givens)] + else empty + + , if null overlapping_givens && isSingleton matches && null unifiers then + -- Intuitively, some given matched the wanted in their flattened or rewritten (from given equalities) + -- form but the matcher can't figure that out because the constraints are non-flat and non-rewritten + -- so we simply report back the whole given context. Accelerate Smart.hs showed this problem. + sep [ptext (sLit "There exists a (perhaps superclass) match") <> colon, nest 2 (vcat (pp_givens givens))] + else empty + , if not (isSingleton matches) then -- Two or more matches empty else -- One match, plus some unifiers ASSERT( not (null unifiers) ) parens (vcat [ptext (sLit "The choice depends on the instantiation of") <+> - quotes (pprWithCommas ppr (varSetElems (tyVarsOfPred pred))), - ptext (sLit "To pick the first instance above, use -XIncoherentInstances"), - ptext (sLit "when compiling the other instance declarations")])] + quotes (pprWithCommas ppr (varSetElems (tyVarsOfPred pred))), + if null (overlapping_givens) then + vcat [ ptext (sLit "To pick the first instance above, use -XIncoherentInstances"), + ptext (sLit "when compiling the other instance declarations")] + else empty])] where ispecs = [ispec | (ispec, _) <- matches] + givens = getUserGivens ctxt + overlapping_givens = unifiable_givens givens + + unifiable_givens [] = [] + unifiable_givens (gg:ggs) + | Just ggdoc <- matchable gg + = ggdoc : unifiable_givens ggs + | otherwise + = unifiable_givens ggs + + matchable (evvars,gloc) + = case ev_vars_matching of + [] -> Nothing + _ -> Just $ hang (pprTheta ev_vars_matching) + 2 (sep [ ptext (sLit "bound by") <+> ppr (ctLocOrigin gloc) + , ptext (sLit "at") <+> ppr (ctLocSpan gloc)]) + where ev_vars_matching = filter ev_var_matches (map evVarPred evvars) + ev_var_matches (ClassP clas' tys') + | clas' == clas + , Just _ <- tcMatchTys (tyVarsOfTypes tys) tys tys' + = True + ev_var_matches (ClassP clas' tys') = + any ev_var_matches (immSuperClasses clas' tys') + ev_var_matches _ = False + + reportOverlap _ _ _ _ = panic "reportOverlap" -- Not a ClassP ---------------------- @@@ -876,9 -832,9 +874,9 @@@ flattenForAllErrorTcS fl ty _bad_eq \begin{code} setCtFlavorLoc :: CtFlavor -> TcM a -> TcM a -setCtFlavorLoc (Wanted loc) thing = setCtLoc loc thing -setCtFlavorLoc (Derived loc) thing = setCtLoc loc thing -setCtFlavorLoc (Given loc) thing = setCtLoc loc thing +setCtFlavorLoc (Wanted loc) thing = setCtLoc loc thing +setCtFlavorLoc (Derived loc) thing = setCtLoc loc thing +setCtFlavorLoc (Given loc _gk) thing = setCtLoc loc thing \end{code} %************************************************************************ diff --combined compiler/typecheck/TcInstDcls.lhs index ecdda43,503812a..954471f --- a/compiler/typecheck/TcInstDcls.lhs +++ b/compiler/typecheck/TcInstDcls.lhs @@@ -16,22 -16,24 +16,24 @@@ import TcPat( addInlinePrags import TcRnMonad import TcMType import TcType + import BuildTyCl import Inst import InstEnv import FamInst import FamInstEnv - import MkCore ( nO_METHOD_BINDING_ERROR_ID ) import TcDeriv import TcEnv import RnSource ( addTcgDUs ) import TcHsType import TcUnify + import MkCore ( nO_METHOD_BINDING_ERROR_ID ) import Type import Coercion import TyCon import DataCon import Class import Var + import Pair import VarSet import CoreUtils ( mkPiTypes ) import CoreUnfold ( mkDFunUnfolding ) @@@ -549,8 -551,8 +551,8 @@@ tcLocalInstDecl1 (L loc (InstDecl poly_ | isTyVarTy ty = return () | otherwise = addErrTc $ mustBeVarArgErr ty checkIndex ty (Just instTy) - | ty `tcEqType` instTy = return () - | otherwise = addErrTc $ wrongATArgErr ty instTy + | ty `eqType` instTy = return () + | otherwise = addErrTc $ wrongATArgErr ty instTy listToNameSet = addListToNameSet emptyNameSet @@@ -563,7 -565,183 +565,183 @@@ tv1 `sameLexeme` tv2 = nameOccName (tyVarName tv1) == nameOccName (tyVarName tv2) in - extendTvSubst (substSameTyVar tvs replacingTvs) tv replacement + TcType.extendTvSubst (substSameTyVar tvs replacingTvs) tv replacement + \end{code} + + + %************************************************************************ + %* * + Type checking family instances + %* * + %************************************************************************ + + Family instances are somewhat of a hybrid. They are processed together with + class instance heads, but can contain data constructors and hence they share a + lot of kinding and type checking code with ordinary algebraic data types (and + GADTs). + + \begin{code} + tcFamInstDecl :: TopLevelFlag -> LTyClDecl Name -> TcM TyThing + tcFamInstDecl top_lvl (L loc decl) + = -- Prime error recovery, set source location + setSrcSpan loc $ + tcAddDeclCtxt decl $ + do { -- type family instances require -XTypeFamilies + -- and can't (currently) be in an hs-boot file + ; type_families <- xoptM Opt_TypeFamilies + ; is_boot <- tcIsHsBoot -- Are we compiling an hs-boot file? + ; checkTc type_families $ badFamInstDecl (tcdLName decl) + ; checkTc (not is_boot) $ badBootFamInstDeclErr + + -- Perform kind and type checking + ; tc <- tcFamInstDecl1 decl + ; checkValidTyCon tc -- Remember to check validity; + -- no recursion to worry about here + + -- Check that toplevel type instances are not for associated types. + ; when (isTopLevel top_lvl && isAssocFamily tc) + (addErr $ assocInClassErr (tcdName decl)) + + ; return (ATyCon tc) } + + isAssocFamily :: TyCon -> Bool -- Is an assocaited type + isAssocFamily tycon + = case tyConFamInst_maybe tycon of + Nothing -> panic "isAssocFamily: no family?!?" + Just (fam, _) -> isTyConAssoc fam + + assocInClassErr :: Name -> SDoc + assocInClassErr name + = ptext (sLit "Associated type") <+> quotes (ppr name) <+> + ptext (sLit "must be inside a class instance") + + + + tcFamInstDecl1 :: TyClDecl Name -> TcM TyCon + + -- "type instance" + tcFamInstDecl1 (decl@TySynonym {tcdLName = L loc tc_name}) + = kcIdxTyPats decl $ \k_tvs k_typats resKind family -> + do { -- check that the family declaration is for a synonym + checkTc (isFamilyTyCon family) (notFamily family) + ; checkTc (isSynTyCon family) (wrongKindOfFamily family) + + ; -- (1) kind check the right-hand side of the type equation + ; k_rhs <- kcCheckLHsType (tcdSynRhs decl) (EK resKind EkUnk) + -- ToDo: the ExpKind could be better + + -- we need the exact same number of type parameters as the family + -- declaration + ; let famArity = tyConArity family + ; checkTc (length k_typats == famArity) $ + wrongNumberOfParmsErr famArity + + -- (2) type check type equation + ; tcTyVarBndrs k_tvs $ \t_tvs -> do { -- turn kinded into proper tyvars + ; t_typats <- mapM tcHsKindedType k_typats + ; t_rhs <- tcHsKindedType k_rhs + + -- (3) check the well-formedness of the instance + ; checkValidTypeInst t_typats t_rhs + + -- (4) construct representation tycon + ; rep_tc_name <- newFamInstTyConName tc_name t_typats loc + ; buildSynTyCon rep_tc_name t_tvs (SynonymTyCon t_rhs) + (typeKind t_rhs) + NoParentTyCon (Just (family, t_typats)) + }} + + -- "newtype instance" and "data instance" + tcFamInstDecl1 (decl@TyData {tcdND = new_or_data, tcdLName = L loc tc_name, + tcdCons = cons}) + = kcIdxTyPats decl $ \k_tvs k_typats resKind fam_tycon -> + do { -- check that the family declaration is for the right kind + checkTc (isFamilyTyCon fam_tycon) (notFamily fam_tycon) + ; checkTc (isAlgTyCon fam_tycon) (wrongKindOfFamily fam_tycon) + + ; -- (1) kind check the data declaration as usual + ; k_decl <- kcDataDecl decl k_tvs + ; let k_ctxt = tcdCtxt k_decl + k_cons = tcdCons k_decl + + -- result kind must be '*' (otherwise, we have too few patterns) + ; checkTc (isLiftedTypeKind resKind) $ tooFewParmsErr (tyConArity fam_tycon) + + -- (2) type check indexed data type declaration + ; tcTyVarBndrs k_tvs $ \t_tvs -> do { -- turn kinded into proper tyvars + ; unbox_strict <- doptM Opt_UnboxStrictFields + + -- kind check the type indexes and the context + ; t_typats <- mapM tcHsKindedType k_typats + ; stupid_theta <- tcHsKindedContext k_ctxt + + -- (3) Check that + -- (a) left-hand side contains no type family applications + -- (vanilla synonyms are fine, though, and we checked for + -- foralls earlier) + ; mapM_ checkTyFamFreeness t_typats + + ; dataDeclChecks tc_name new_or_data stupid_theta k_cons + + -- (4) construct representation tycon + ; rep_tc_name <- newFamInstTyConName tc_name t_typats loc + ; let ex_ok = True -- Existentials ok for type families! + ; fixM (\ rep_tycon -> do + { let orig_res_ty = mkTyConApp fam_tycon t_typats + ; data_cons <- tcConDecls unbox_strict ex_ok rep_tycon + (t_tvs, orig_res_ty) k_cons + ; tc_rhs <- + case new_or_data of + DataType -> return (mkDataTyConRhs data_cons) + NewType -> ASSERT( not (null data_cons) ) + mkNewTyConRhs rep_tc_name rep_tycon (head data_cons) + ; buildAlgTyCon rep_tc_name t_tvs stupid_theta tc_rhs Recursive + False h98_syntax NoParentTyCon (Just (fam_tycon, t_typats)) + -- We always assume that indexed types are recursive. Why? + -- (1) Due to their open nature, we can never be sure that a + -- further instance might not introduce a new recursive + -- dependency. (2) They are always valid loop breakers as + -- they involve a coercion. + }) + }} + where + h98_syntax = case cons of -- All constructors have same shape + L _ (ConDecl { con_res = ResTyGADT _ }) : _ -> False + _ -> True + + tcFamInstDecl1 d = pprPanic "tcFamInstDecl1" (ppr d) + + -- Kind checking of indexed types + -- - + + -- Kind check type patterns and kind annotate the embedded type variables. + -- + -- * Here we check that a type instance matches its kind signature, but we do + -- not check whether there is a pattern for each type index; the latter + -- check is only required for type synonym instances. + + kcIdxTyPats :: TyClDecl Name + -> ([LHsTyVarBndr Name] -> [LHsType Name] -> Kind -> TyCon -> TcM a) + -- ^^kinded tvs ^^kinded ty pats ^^res kind + -> TcM a + kcIdxTyPats decl thing_inside + = kcHsTyVars (tcdTyVars decl) $ \tvs -> + do { let tc_name = tcdLName decl + ; fam_tycon <- tcLookupLocatedTyCon tc_name + ; let { (kinds, resKind) = splitKindFunTys (tyConKind fam_tycon) + ; hs_typats = fromJust $ tcdTyPats decl } + + -- we may not have more parameters than the kind indicates + ; checkTc (length kinds >= length hs_typats) $ + tooManyParmsErr (tcdLName decl) + + -- type functions can have a higher-kinded result + ; let resultKind = mkArrowKinds (drop (length hs_typats) kinds) resKind + ; typats <- zipWithM kcCheckLHsType hs_typats + [ EK kind (EkArg (ppr tc_name) n) + | (kind,n) <- kinds `zip` [1..]] + ; thing_inside tvs typats resultKind fam_tycon + } \end{code} @@@ -621,9 -799,6 +799,9 @@@ tcInstDecl2 (InstInfo { iSpec = ispec, addErrCtxt (instDeclCtxt2 (idType dfun_id)) $ do { -- Instantiate the instance decl with skolem constants ; (inst_tyvars, dfun_theta, inst_head) <- tcSkolDFunType (idType dfun_id) + -- We instantiate the dfun_id with superSkolems. + -- See Note [Subtle interaction of recursion and overlap] + -- and Note [Binding when looking up instances] ; let (clas, inst_tys) = tcSplitDFunHead inst_head (class_tyvars, sc_theta, _, op_items) = classBigSig clas sc_theta' = substTheta (zipOpenTvSubst class_tyvars inst_tys) sc_theta @@@ -702,7 -877,7 +880,7 @@@ listToBag meth_binds) } where - skol_info = InstSkol -- See Note [Subtle interaction of recursion and overlap] + skol_info = InstSkol dfun_ty = idType dfun_id dfun_id = instanceDFunId ispec loc = getSrcSpan dfun_id @@@ -721,8 -896,8 +899,8 @@@ tcSuperClass n_ty_args ev_vars pre ; return (sc_dict, DFunConstArg (Var sc_dict)) } where find _ [] = Nothing - find i (ev:evs) | pred `tcEqPred` evVarPred ev = Just (ev, i) - | otherwise = find (i+1) evs + find i (ev:evs) | pred `eqPred` evVarPred ev = Just (ev, i) + | otherwise = find (i+1) evs ------------------------------ tcSpecInstPrags :: DFunId -> InstBindings Name @@@ -1045,13 -1220,12 +1223,12 @@@ tcInstanceMethods dfun_id clas tyvars d inst_tvs = fst (tcSplitForAllTys (idType dfun_id)) Just (init_inst_tys, _) = snocView inst_tys - rep_ty = fst (coercionKind co) -- [p] + rep_ty = pFst (coercionKind co) -- [p] rep_pred = mkClassPred clas (init_inst_tys ++ [rep_ty]) -- co : [p] ~ T p - co = substTyWith inst_tvs (mkTyVarTys tyvars) $ - case coi of { IdCo ty -> ty ; - ACo co -> mkSymCoercion co } + co = substCoWithTys inst_tvs (mkTyVarTys tyvars) $ + mkSymCo coi ---------------- tc_item :: (TcEvBinds, EvVar) -> (Id, DefMeth) -> TcM (TcId, LHsBind TcId) @@@ -1075,7 -1249,8 +1252,8 @@@ ---------------- mk_op_wrapper :: Id -> EvVar -> HsWrapper mk_op_wrapper sel_id rep_d - = WpCast (substTyWith sel_tvs (init_inst_tys ++ [co]) local_meth_ty) + = WpCast (liftCoSubstWith sel_tvs (map mkReflCo init_inst_tys ++ [co]) + local_meth_ty) <.> WpEvApp (EvId rep_d) <.> mkWpTyApps (init_inst_tys ++ [rep_ty]) where @@@ -1265,4 -1440,37 +1443,37 @@@ wrongATArgErr ty instTy , ptext (sLit "Found") <+> quotes (ppr ty) <+> ptext (sLit "but expected") <+> quotes (ppr instTy) ] + + tooManyParmsErr :: Located Name -> SDoc + tooManyParmsErr tc_name + = ptext (sLit "Family instance has too many parameters:") <+> + quotes (ppr tc_name) + + tooFewParmsErr :: Arity -> SDoc + tooFewParmsErr arity + = ptext (sLit "Family instance has too few parameters; expected") <+> + ppr arity + + wrongNumberOfParmsErr :: Arity -> SDoc + wrongNumberOfParmsErr exp_arity + = ptext (sLit "Number of parameters must match family declaration; expected") + <+> ppr exp_arity + + badBootFamInstDeclErr :: SDoc + badBootFamInstDeclErr + = ptext (sLit "Illegal family instance in hs-boot file") + + notFamily :: TyCon -> SDoc + notFamily tycon + = vcat [ ptext (sLit "Illegal family instance for") <+> quotes (ppr tycon) + , nest 2 $ parens (ppr tycon <+> ptext (sLit "is not an indexed type family"))] + + wrongKindOfFamily :: TyCon -> SDoc + wrongKindOfFamily family + = ptext (sLit "Wrong category of family instance; declaration was for a") + <+> kindOfFamily + where + kindOfFamily | isSynTyCon family = ptext (sLit "type synonym") + | isAlgTyCon family = ptext (sLit "data type") + | otherwise = pprPanic "wrongKindOfFamily" (ppr family) \end{code} diff --combined compiler/typecheck/TcInteract.lhs index 46eece8,fd66d0a..3833534 --- a/compiler/typecheck/TcInteract.lhs +++ b/compiler/typecheck/TcInteract.lhs @@@ -12,7 -12,6 +12,7 @@@ import BasicType import TcCanonical import VarSet import Type +import Unify import Id import Var @@@ -31,7 -30,6 +31,7 @@@ import Coercio import Outputable import TcRnTypes +import TcMType ( isSilentEvVar ) import TcErrors import TcSMonad import Bag @@@ -70,11 -68,8 +70,11 @@@ An InertSet is a bag of canonical const will be marked as solved right before being pushed into the inert set. See note [Touchables and givens]. - 8 No Given constraint mentions a touchable unification variable, - except if the + 8 No Given constraint mentions a touchable unification variable, but + Given/Solved may do so. + + 9 Given constraints will also have their superclasses in the inert set, + but Given/Solved will not. Note that 6 and 7 are /not/ enforced by canonicalization but rather by insertion in the inert list, ie by TcInteract. @@@ -197,7 -192,7 +197,7 @@@ extractUnsolved is@(IS {inert_eqs = eqs , inert_funeqs = solved_funeqs } in (is_solved, unsolved) - where (unsolved_eqs, solved_eqs) = Bag.partitionBag (not.isGivenCt) eqs + where (unsolved_eqs, solved_eqs) = Bag.partitionBag (not.isGivenOrSolvedCt) eqs (unsolved_ips, solved_ips) = extractUnsolvedCMap (inert_ips is) (unsolved_dicts, solved_dicts) = extractUnsolvedCMap (inert_dicts is) (unsolved_funeqs, solved_funeqs) = extractUnsolvedCMap (inert_funeqs is) @@@ -332,7 -327,7 +332,7 @@@ solveInteractGiven inert gloc ev map mk_given evs ; return inert_ret } where - flav = Given gloc + flav = Given gloc GivenOrig mk_given ev = mkEvVarX ev flav solveInteractWanted :: InertSet -> [WantedEvVar] -> TcS InertSet @@@ -413,18 -408,12 +413,12 @@@ dischargeFromCCans cans ev f discharge_ct :: CanonicalCt -> TcS Bool -> TcS Bool discharge_ct ct _rest - | evVarPred (cc_id ct) `tcEqPred` the_pred + | evVarPred (cc_id ct) `eqPred` the_pred , cc_flavor ct `canSolve` fl - -- DV: No special care should be taken for Given/Solveds, we will - -- never encounter a Given entering the constraint bag after a Given/Solved - = do { when (isWanted fl) $ set_ev_bind ev (cc_id ct) + = do { when (isWanted fl) $ setEvBind ev (evVarTerm (cc_id ct)) -- Deriveds need no evidence -- For Givens, we already have evidence, and we don't need it twice ; return True } - where - set_ev_bind x y - | EqPred {} <- evVarPred y = setEvBind x (EvCoercion (mkCoVarCoercion y)) - | otherwise = setEvBind x (EvId y) discharge_ct _ct rest = rest \end{code} @@@ -538,7 -527,7 +532,7 @@@ spontaneousSolveStage depth workItem in , sr_stop = ContinueWith workItem } SPSolved workItem' - | not (isGivenCt workItem) + | not (isGivenOrSolvedCt workItem) -- Original was wanted or derived but we have now made him -- given so we have to interact him with the inerts due to -- its status change. This in turn may produce more work. @@@ -579,7 -568,7 +573,7 @@@ data SPSolveResult = SPCantSolve | SPSo -- See Note [Touchables and givens] trySpontaneousSolve :: WorkItem -> TcS SPSolveResult trySpontaneousSolve workItem@(CTyEqCan { cc_id = cv, cc_flavor = gw, cc_tyvar = tv1, cc_rhs = xi }) - | isGiven gw + | isGivenOrSolved gw = return SPCantSolve | Just tv2 <- tcGetTyVar_maybe xi = do { tch1 <- isTouchableMetaTyVar tv1 @@@ -732,12 -721,14 +726,13 @@@ solveWithIdentity cv wd tv x ] ; setWantedTyBind tv xi - ; cv_given <- newGivenCoVar (mkTyVarTy tv) xi xi + ; let refl_xi = mkReflCo xi + ; cv_given <- newGivenCoVar (mkTyVarTy tv) xi refl_xi - ; when (isWanted wd) (setCoBind cv xi) + ; when (isWanted wd) (setCoBind cv refl_xi) -- We don't want to do this for Derived, that's why we use 'when (isWanted wd)' - ; return $ SPSolved (CTyEqCan { cc_id = cv_given - , cc_flavor = mkGivenFlavor wd UnkSkol + , cc_flavor = mkSolvedFlavor wd UnkSkol , cc_tyvar = tv, cc_rhs = xi }) } \end{code} @@@ -934,10 -925,10 +929,10 @@@ doInteractWithInert :: CanonicalCt -> C doInteractWithInert inertItem@(CDictCan { cc_id = d1, cc_flavor = fl1, cc_class = cls1, cc_tyargs = tys1 }) workItem@(CDictCan { cc_id = d2, cc_flavor = fl2, cc_class = cls2, cc_tyargs = tys2 }) - | cls1 == cls2 && (and $ zipWith tcEqType tys1 tys2) + | cls1 == cls2 && eqTypes tys1 tys2 = solveOneFromTheOther "Cls/Cls" (EvId d1,fl1) workItem - | cls1 == cls2 && (not (isGiven fl1 && isGiven fl2)) + | cls1 == cls2 && (not (isGivenOrSolved fl1 && isGivenOrSolved fl2)) = -- See Note [When improvement happens] do { let pty1 = ClassP cls1 tys1 pty2 = ClassP cls2 tys2 @@@ -952,7 -943,7 +947,7 @@@ ; case m of Nothing -> noInteraction workItem Just (rewritten_tys2, cos2, fd_work) - | tcEqTypes tys1 rewritten_tys2 + | eqTypes tys1 rewritten_tys2 -> -- Solve him on the spot in this case case fl2 of Given {} -> pprPanic "Unexpected given" (ppr inertItem $$ ppr workItem) @@@ -997,7 -988,7 +992,7 @@@ workListFromNonEq workItem' `unionWorkList` fd_work } where - dict_co = mkTyConCoercion (classTyCon cls1) cos2 + dict_co = mkTyConAppCo (classTyCon cls1) cos2 } -- Class constraint and given equality: use the equality to rewrite @@@ -1041,7 -1032,7 +1036,7 @@@ doInteractWithInert (CIPCan { cc_id = i -- so we just generate a fresh coercion variable that isn't used anywhere. doInteractWithInert (CIPCan { cc_id = id1, cc_flavor = ifl, cc_ip_nm = nm1, cc_ip_ty = ty1 }) workItem@(CIPCan { cc_flavor = wfl, cc_ip_nm = nm2, cc_ip_ty = ty2 }) - | nm1 == nm2 && isGiven wfl && isGiven ifl + | nm1 == nm2 && isGivenOrSolved wfl && isGivenOrSolved ifl = -- See Note [Overriding implicit parameters] -- Dump the inert item, override totally with the new one -- Do not require type equality @@@ -1049,7 -1040,7 +1044,7 @@@ -- we must *override* the outer one with the inner one mkIRContinue "IP/IP override" workItem DropInert emptyWorkList - | nm1 == nm2 && ty1 `tcEqType` ty2 + | nm1 == nm2 && ty1 `eqType` ty2 = solveOneFromTheOther "IP/IP" (EvId id1,ifl) workItem | nm1 == nm2 @@@ -1062,7 -1053,7 +1057,7 @@@ Derived {} -> pprPanic "Unexpected derived IP" (ppr workItem) Wanted {} -> do { setIPBind (cc_id workItem) $ - EvCast id1 (mkSymCoercion (mkCoVarCoercion co_var)) + EvCast id1 (mkSymCo (mkCoVarCo co_var)) ; mkIRStopK "IP/IP interaction (solved)" cans } } @@@ -1102,31 -1093,24 +1097,31 @@@ doInteractWithInert (CFunEqCan { cc_id , cc_tyargs = args1, cc_rhs = xi1 }) workItem@(CFunEqCan { cc_id = cv2, cc_flavor = fl2, cc_fun = tc2 , cc_tyargs = args2, cc_rhs = xi2 }) - | tc1 == tc2 && and (zipWith tcEqType args1 args2) ++ | tc1 == tc2 && and (zipWith eqType args1 args2) + , Just GivenSolved <- isGiven_maybe fl1 + = mkIRContinue "Funeq/Funeq" workItem DropInert emptyWorkList - | tc1 == tc2 && and (zipWith tcEqType args1 args2) ++ | tc1 == tc2 && and (zipWith eqType args1 args2) + , Just GivenSolved <- isGiven_maybe fl2 + = mkIRStopK "Funeq/Funeq" emptyWorkList + | fl1 `canSolve` fl2 && lhss_match - = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2) + = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCo cv1,xi1) (cv2,fl2,xi2) ; mkIRStopK "FunEq/FunEq" cans } | fl2 `canSolve` fl1 && lhss_match - = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1) + = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCo cv2,xi2) (cv1,fl1,xi1) ; mkIRContinue "FunEq/FunEq" workItem DropInert cans } where - lhss_match = tc1 == tc2 && and (zipWith tcEqType args1 args2) + lhss_match = tc1 == tc2 && eqTypes args1 args2 doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 }) workItem@(CTyEqCan { cc_id = cv2, cc_flavor = fl2, cc_tyvar = tv2, cc_rhs = xi2 }) -- Check for matching LHS | fl1 `canSolve` fl2 && tv1 == tv2 - = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2) + = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCo cv1,xi1) (cv2,fl2,xi2) ; mkIRStopK "Eq/Eq lhs" cans } | fl2 `canSolve` fl1 && tv1 == tv2 - = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1) + = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCo cv2,xi2) (cv1,fl1,xi1) ; mkIRContinue "Eq/Eq lhs" workItem DropInert cans } -- Check for rewriting RHS @@@ -1157,13 -1141,13 +1152,13 @@@ doInteractWithInert _ workItem = noInte -- Equational Rewriting rewriteDict :: (CoVar, TcTyVar, Xi) -> (DictId, CtFlavor, Class, [Xi]) -> TcS CanonicalCt rewriteDict (cv,tv,xi) (dv,gw,cl,xis) - = do { let cos = substTysWith [tv] [mkCoVarCoercion cv] xis -- xis[tv] ~ xis[xi] + = do { let cos = map (liftCoSubstWith [tv] [mkCoVarCo cv]) xis -- xis[tv] ~ xis[xi] args = substTysWith [tv] [xi] xis con = classTyCon cl - dict_co = mkTyConCoercion con cos + dict_co = mkTyConAppCo con cos ; dv' <- newDictVar cl args ; case gw of - Wanted {} -> setDictBind dv (EvCast dv' (mkSymCoercion dict_co)) + Wanted {} -> setDictBind dv (EvCast dv' (mkSymCo dict_co)) Given {} -> setDictBind dv' (EvCast dv dict_co) Derived {} -> return () -- Derived dicts we don't set any evidence @@@ -1174,11 -1158,11 +1169,11 @@@ rewriteIP :: (CoVar,TcTyVar,Xi) -> (EvVar,CtFlavor, IPName Name, TcType) -> TcS CanonicalCt rewriteIP (cv,tv,xi) (ipid,gw,nm,ty) - = do { let ip_co = substTyWith [tv] [mkCoVarCoercion cv] ty -- ty[tv] ~ t[xi] - ty' = substTyWith [tv] [xi] ty + = do { let ip_co = liftCoSubstWith [tv] [mkCoVarCo cv] ty -- ty[tv] ~ t[xi] + ty' = substTyWith [tv] [xi] ty ; ipid' <- newIPVar nm ty' ; case gw of - Wanted {} -> setIPBind ipid (EvCast ipid' (mkSymCoercion ip_co)) + Wanted {} -> setIPBind ipid (EvCast ipid' (mkSymCo ip_co)) Given {} -> setIPBind ipid' (EvCast ipid ip_co) Derived {} -> return () -- Derived ips: we don't set any evidence @@@ -1189,20 -1173,21 +1184,21 @@@ rewriteFunEq :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TyCon, [Xi], Xi) -> TcS CanonicalCt rewriteFunEq (cv1,tv,xi1) (cv2,gw, tc,args,xi2) -- cv2 :: F args ~ xi2 - = do { let arg_cos = substTysWith [tv] [mkCoVarCoercion cv1] args - args' = substTysWith [tv] [xi1] args - fun_co = mkTyConCoercion tc arg_cos -- fun_co :: F args ~ F args' + = do { let co_subst = liftCoSubstWith [tv] [mkCoVarCo cv1] + arg_cos = map co_subst args + args' = substTysWith [tv] [xi1] args + fun_co = mkTyConAppCo tc arg_cos -- fun_co :: F args ~ F args' xi2' = substTyWith [tv] [xi1] xi2 - xi2_co = substTyWith [tv] [mkCoVarCoercion cv1] xi2 -- xi2_co :: xi2 ~ xi2' + xi2_co = co_subst xi2 -- xi2_co :: xi2 ~ xi2' ; cv2' <- newCoVar (mkTyConApp tc args') xi2' ; case gw of - Wanted {} -> setCoBind cv2 (fun_co `mkTransCoercion` - mkCoVarCoercion cv2' `mkTransCoercion` - mkSymCoercion xi2_co) - Given {} -> setCoBind cv2' (mkSymCoercion fun_co `mkTransCoercion` - mkCoVarCoercion cv2 `mkTransCoercion` + Wanted {} -> setCoBind cv2 (fun_co `mkTransCo` + mkCoVarCo cv2' `mkTransCo` + mkSymCo xi2_co) + Given {} -> setCoBind cv2' (mkSymCo fun_co `mkTransCo` + mkCoVarCo cv2 `mkTransCo` xi2_co) Derived {} -> return () @@@ -1223,20 -1208,20 +1219,20 @@@ rewriteEqRHS :: (CoVar,TcTyVar,Xi) -> ( rewriteEqRHS (cv1,tv1,xi1) (cv2,gw,tv2,xi2) | Just tv2' <- tcGetTyVar_maybe xi2' , tv2 == tv2' -- In this case xi2[xi1/tv1] = tv2, so we have tv2~tv2 - = do { when (isWanted gw) (setCoBind cv2 (mkSymCoercion co2')) + = do { when (isWanted gw) (setCoBind cv2 (mkSymCo co2')) ; return emptyWorkList } | otherwise = do { cv2' <- newCoVar (mkTyVarTy tv2) xi2' ; case gw of - Wanted {} -> setCoBind cv2 $ mkCoVarCoercion cv2' `mkTransCoercion` - mkSymCoercion co2' - Given {} -> setCoBind cv2' $ mkCoVarCoercion cv2 `mkTransCoercion` + Wanted {} -> setCoBind cv2 $ mkCoVarCo cv2' `mkTransCo` + mkSymCo co2' + Given {} -> setCoBind cv2' $ mkCoVarCo cv2 `mkTransCo` co2' Derived {} -> return () ; canEqToWorkList gw cv2' (mkTyVarTy tv2) xi2' } where xi2' = substTyWith [tv1] [xi1] xi2 - co2' = substTyWith [tv1] [mkCoVarCoercion cv1] xi2 -- xi2 ~ xi2[xi1/tv1] + co2' = liftCoSubstWith [tv1] [mkCoVarCo cv1] xi2 -- xi2 ~ xi2[xi1/tv1] rewriteEqLHS :: WhichComesFromInert -> (Coercion,Xi) -> (CoVar,CtFlavor,Xi) -> TcS WorkList -- Used to ineract two equalities of the following form: @@@ -1249,9 -1234,9 +1245,9 @@@ rewriteEqLHS LeftComesFromInert (co1,xi = do { cv2' <- newCoVar xi2 xi1 ; case gw of Wanted {} -> setCoBind cv2 $ - co1 `mkTransCoercion` mkSymCoercion (mkCoVarCoercion cv2') + co1 `mkTransCo` mkSymCo (mkCoVarCo cv2') Given {} -> setCoBind cv2' $ - mkSymCoercion (mkCoVarCoercion cv2) `mkTransCoercion` co1 + mkSymCo (mkCoVarCo cv2) `mkTransCo` co1 Derived {} -> return () ; mkCanonical gw cv2' } @@@ -1259,9 -1244,9 +1255,9 @@@ rewriteEqLHS RightComesFromInert (co1,x = do { cv2' <- newCoVar xi1 xi2 ; case gw of Wanted {} -> setCoBind cv2 $ - co1 `mkTransCoercion` mkCoVarCoercion cv2' + co1 `mkTransCo` mkCoVarCo cv2' Given {} -> setCoBind cv2' $ - mkSymCoercion co1 `mkTransCoercion` mkCoVarCoercion cv2 + mkSymCo co1 `mkTransCo` mkCoVarCo cv2 Derived {} -> return () ; mkCanonical gw cv2' } @@@ -1269,12 -1254,12 +1265,12 @@@ rewriteFrozen :: (CoVar,TcTyVar,Xi) -> rewriteFrozen (cv1, tv1, xi1) (cv2, fl2) = do { cv2' <- newCoVar ty2a' ty2b' -- ty2a[xi1/tv1] ~ ty2b[xi1/tv1] ; case fl2 of - Wanted {} -> setCoBind cv2 $ co2a' `mkTransCoercion` - mkCoVarCoercion cv2' `mkTransCoercion` - mkSymCoercion co2b' + Wanted {} -> setCoBind cv2 $ co2a' `mkTransCo` + mkCoVarCo cv2' `mkTransCo` + mkSymCo co2b' - Given {} -> setCoBind cv2' $ mkSymCoercion co2a' `mkTransCoercion` - mkCoVarCoercion cv2 `mkTransCoercion` + Given {} -> setCoBind cv2' $ mkSymCo co2a' `mkTransCo` + mkCoVarCo cv2 `mkTransCo` co2b' Derived {} -> return () @@@ -1285,8 -1270,8 +1281,8 @@@ ty2a' = substTyWith [tv1] [xi1] ty2a ty2b' = substTyWith [tv1] [xi1] ty2b - co2a' = substTyWith [tv1] [mkCoVarCoercion cv1] ty2a -- ty2a ~ ty2a[xi1/tv1] - co2b' = substTyWith [tv1] [mkCoVarCoercion cv1] ty2b -- ty2b ~ ty2b[xi1/tv1] + co2a' = liftCoSubstWith [tv1] [mkCoVarCo cv1] ty2a -- ty2a ~ ty2a[xi1/tv1] + co2b' = liftCoSubstWith [tv1] [mkCoVarCo cv1] ty2b -- ty2b ~ ty2b[xi1/tv1] solveOneFromTheOther :: String -> (EvTerm, CtFlavor) -> CanonicalCt -> TcS InteractResult -- First argument inert, second argument work-item. They both represent @@@ -1304,10 -1289,6 +1300,10 @@@ solveOneFromTheOther info (ev_term,ifl -- so it's safe to continue on from this point = mkIRContinue ("Solved[DI] " ++ info) workItem DropInert emptyWorkList + | Just GivenSolved <- isGiven_maybe ifl, isGivenOrSolved wfl + -- Same if the inert is a GivenSolved -- just get rid of it + = mkIRContinue ("Solved[SI] " ++ info) workItem DropInert emptyWorkList + | otherwise = ASSERT( ifl `canSolve` wfl ) -- Because of Note [The Solver Invariant], plus Derived dealt with @@@ -1682,34 -1663,33 +1678,34 @@@ data TopInteractResul -- only reacted with functional dependencies -- arising from top-level instances. -topReactionsStage :: SimplifierStage -topReactionsStage depth workItem inerts - = do { tir <- tryTopReact workItem - ; case tir of - NoTopInt -> - return $ SR { sr_inerts = inerts - , sr_new_work = emptyWorkList - , sr_stop = ContinueWith workItem } - SomeTopInt tir_new_work tir_new_inert -> +topReactionsStage :: SimplifierStage +topReactionsStage depth workItem inerts + = do { tir <- tryTopReact inerts workItem + -- NB: we pass the inerts as well. See Note [Instance and Given overlap] + ; case tir of + NoTopInt -> + return $ SR { sr_inerts = inerts + , sr_new_work = emptyWorkList + , sr_stop = ContinueWith workItem } + SomeTopInt tir_new_work tir_new_inert -> do { bumpStepCountTcS ; traceFireTcS depth (ptext (sLit "Top react") <+> vcat [ ptext (sLit "Work =") <+> ppr workItem , ptext (sLit "New =") <+> ppr tir_new_work ]) - ; return $ SR { sr_inerts = inerts + ; return $ SR { sr_inerts = inerts , sr_new_work = tir_new_work , sr_stop = tir_new_inert } } } -tryTopReact :: WorkItem -> TcS TopInteractResult -tryTopReact workitem +tryTopReact :: InertSet -> WorkItem -> TcS TopInteractResult +tryTopReact inerts workitem = do { -- A flag controls the amount of interaction allowed -- See Note [Simplifying RULE lhs constraints] ctxt <- getTcSContext ; if allowedTopReaction (simplEqsOnly ctxt) workitem then do { traceTcS "tryTopReact / calling doTopReact" (ppr workitem) - ; doTopReact workitem } + ; doTopReact inerts workitem } else return NoTopInt } @@@ -1717,7 -1697,7 +1713,7 @@@ allowedTopReaction :: Bool -> WorkItem allowedTopReaction eqs_only (CDictCan {}) = not eqs_only allowedTopReaction _ _ = True -doTopReact :: WorkItem -> TcS TopInteractResult +doTopReact :: InertSet -> WorkItem -> TcS TopInteractResult -- The work item does not react with the inert set, so try interaction with top-level instances -- NB: The place to add superclasses in *not* in doTopReact stage. Instead superclasses are -- added in the worklist as part of the canonicalisation process. @@@ -1725,12 -1705,12 +1721,12 @@@ -- Given dictionary -- See Note [Given constraint that matches an instance declaration] -doTopReact (CDictCan { cc_flavor = Given {} }) +doTopReact _inerts (CDictCan { cc_flavor = Given {} }) = return NoTopInt -- NB: Superclasses already added since it's canonical -- Derived dictionary: just look for functional dependencies -doTopReact workItem@(CDictCan { cc_flavor = fl@(Derived loc) - , cc_class = cls, cc_tyargs = xis }) +doTopReact _inerts workItem@(CDictCan { cc_flavor = fl@(Derived loc) + , cc_class = cls, cc_tyargs = xis }) = do { instEnvs <- getInstEnvs ; let fd_eqns = improveFromInstEnv instEnvs (ClassP cls xis, pprArisingAt loc) @@@ -1744,10 -1724,10 +1740,10 @@@ , tir_new_inert = ContinueWith workItem' } } -- Wanted dictionary -doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = fl@(Wanted loc) - , cc_class = cls, cc_tyargs = xis }) +doTopReact inerts workItem@(CDictCan { cc_id = dv, cc_flavor = fl@(Wanted loc) + , cc_class = cls, cc_tyargs = xis }) = do { -- See Note [MATCHING-SYNONYMS] - ; lkp_inst_res <- matchClassInst cls xis loc + ; lkp_inst_res <- matchClassInst inerts cls xis loc ; case lkp_inst_res of NoInstance -> do { traceTcS "doTopReact/ no class instance for" (ppr dv) @@@ -1759,7 -1739,7 +1755,7 @@@ ; case m of Nothing -> return NoTopInt Just (xis',cos,fd_work) -> - do { let dict_co = mkTyConCoercion (classTyCon cls) cos + do { let dict_co = mkTyConAppCo (classTyCon cls) cos ; dv'<- newDictVar cls xis' ; setDictBind dv (EvCast dv' dict_co) ; let workItem' = CDictCan { cc_id = dv', cc_flavor = fl, @@@ -1773,7 -1753,7 +1769,7 @@@ -- matches already so we won't get any more info -- from functional dependencies | null wtvs - -> do { traceTcS "doTopReact/ found nullary class instance for" (ppr dv) + -> do { traceTcS "doTopReact/found nullary class instance for" (ppr dv) ; setDictBind dv ev_term -- Solved in one step and no new wanted work produced. -- i.e we directly matched a top-level instance @@@ -1782,29 -1762,25 +1778,29 @@@ , tir_new_inert = Stop } } | otherwise - -> do { traceTcS "doTopReact/ found nullary class instance for" (ppr dv) + -> do { traceTcS "doTopReact/found non-nullary class instance for" (ppr dv) ; setDictBind dv ev_term -- Solved and new wanted work produced, you may cache the - -- (tentatively solved) dictionary as Given! (used to be: Derived) - ; let solved = workItem { cc_flavor = given_fl } - given_fl = Given (setCtLocOrigin loc UnkSkol) + -- (tentatively solved) dictionary as Solved given. + ; let solved = workItem { cc_flavor = solved_fl } + solved_fl = mkSolvedFlavor fl UnkSkol ; inst_work <- canWanteds wtvs ; return $ SomeTopInt { tir_new_work = inst_work , tir_new_inert = ContinueWith solved } } } -- Type functions -doTopReact (CFunEqCan { cc_id = cv, cc_flavor = fl - , cc_fun = tc, cc_tyargs = args, cc_rhs = xi }) +doTopReact _inerts (CFunEqCan { cc_flavor = fl }) + | Just GivenSolved <- isGiven_maybe fl + = return NoTopInt -- If Solved, no more interactions should happen + +-- Otherwise, it's a Given, Derived, or Wanted +doTopReact _inerts workItem@(CFunEqCan { cc_id = cv, cc_flavor = fl + , cc_fun = tc, cc_tyargs = args, cc_rhs = xi }) = ASSERT (isSynFamilyTyCon tc) -- No associated data families have reached that far do { match_res <- matchFam tc args -- See Note [MATCHING-SYNONYMS] ; case match_res of - MatchInstNo - -> return NoTopInt + MatchInstNo -> return NoTopInt MatchInstSingle (rep_tc, rep_tys) -> do { let Just coe_tc = tyConFamilyCoercion_maybe rep_tc Just rhs_ty = tcView (mkTyConApp rep_tc rep_tys) @@@ -1812,41 -1788,25 +1808,40 @@@ -- RHS of a type function, so that it never -- appears in an error message -- See Note [Type synonym families] in TyCon - coe = mkTyConApp coe_tc rep_tys - coe = mkAxInstCo coe_tc rep_tys - ; cv' <- case fl of - Wanted {} -> do { cv' <- newCoVar rhs_ty xi - ; setCoBind cv $ - coe `mkTransCo` - mkCoVarCo cv' - ; return cv' } - Given {} -> newGivenCoVar xi rhs_ty $ - mkSymCo (mkCoVarCo cv) `mkTransCo` coe - Derived {} -> newDerivedId (EqPred xi rhs_ty) - ; can_cts <- mkCanonical fl cv' - ; return $ SomeTopInt can_cts Stop } ++ coe = mkAxInstCo coe_tc rep_tys + ; case fl of + Wanted {} -> do { cv' <- newCoVar rhs_ty xi - ; setCoBind cv $ - coe `mkTransCoercion` mkCoVarCoercion cv' ++ ; setCoBind cv $ coe `mkTransCo` mkCoVarCo cv' + ; can_cts <- mkCanonical fl cv' + ; let solved = workItem { cc_flavor = solved_fl } + solved_fl = mkSolvedFlavor fl UnkSkol + ; if isEmptyWorkList can_cts then + return (SomeTopInt can_cts Stop) -- No point in caching + else return $ + SomeTopInt { tir_new_work = can_cts + , tir_new_inert = ContinueWith solved } + } + Given {} -> do { cv' <- newGivenCoVar xi rhs_ty $ - mkSymCoercion (mkCoVarCoercion cv) `mkTransCoercion` coe ++ mkSymCo (mkCoVarCo cv) `mkTransCo` coe + ; can_cts <- mkCanonical fl cv' + ; return $ + SomeTopInt { tir_new_work = can_cts + , tir_new_inert = Stop } + } + Derived {} -> do { cv' <- newDerivedId (EqPred xi rhs_ty) + ; can_cts <- mkCanonical fl cv' + ; return $ + SomeTopInt { tir_new_work = can_cts + , tir_new_inert = Stop } + } + } _ -> panicTcS $ text "TcSMonad.matchFam returned multiple instances!" } -- Any other work item does not react with any top-level equations -doTopReact _workItem = return NoTopInt +doTopReact _inerts _workItem = return NoTopInt \end{code} @@@ -2050,25 -2010,15 +2045,25 @@@ data LookupInstResul = NoInstance | GenInst [WantedEvVar] EvTerm -matchClassInst :: Class -> [Type] -> WantedLoc -> TcS LookupInstResult -matchClassInst clas tys loc +matchClassInst :: InertSet -> Class -> [Type] -> WantedLoc -> TcS LookupInstResult +matchClassInst inerts clas tys loc = do { let pred = mkClassPred clas tys ; mb_result <- matchClass clas tys + ; untch <- getUntouchables ; case mb_result of MatchInstNo -> return NoInstance - MatchInstMany -> return NoInstance -- defer any reactions of a multitude until + MatchInstMany -> return NoInstance -- defer any reactions of a multitude until -- we learn more about the reagent - MatchInstSingle (dfun_id, mb_inst_tys) -> + MatchInstSingle (_,_) + | given_overlap untch -> + do { traceTcS "Delaying instance application" $ - vcat [ text "Workitem=" <+> pprPred (ClassP clas tys) ++ vcat [ text "Workitem=" <+> pprPredTy (ClassP clas tys) + , text "Silents and their superclasses=" <+> ppr silents_and_their_scs + , text "All given dictionaries=" <+> ppr all_given_dicts ] + ; return NoInstance -- see Note [Instance and Given overlap] + } + + MatchInstSingle (dfun_id, mb_inst_tys) -> do { checkWellStagedDFun pred dfun_id loc -- It's possible that not all the tyvars are in @@@ -2077,7 -2027,7 +2072,7 @@@ -- (presumably there's a functional dependency in class C) -- Hence mb_inst_tys :: Either TyVar TcType - ; tys <- instDFunTypes mb_inst_tys + ; tys <- instDFunTypes mb_inst_tys ; let (theta, _) = tcSplitPhiTy (applyTys (idType dfun_id) tys) ; if null theta then return (GenInst [] (EvDFunApp dfun_id tys [])) @@@ -2087,94 -2037,4 +2082,94 @@@ ; return $ GenInst wevs (EvDFunApp dfun_id tys ev_vars) } } } + where given_overlap :: TcsUntouchables -> Bool + given_overlap untch + = foldlBag (\r d -> r || matchable untch d) False all_given_dicts + + matchable untch (CDictCan { cc_class = clas', cc_tyargs = sys, cc_flavor = fl }) + | Just GivenOrig <- isGiven_maybe fl + , clas' == clas + , does_not_originate_in_a_silent clas' sys + = case tcUnifyTys (\tv -> if isTouchableMetaTyVar_InRange untch tv && + tv `elemVarSet` tyVarsOfTypes tys + then BindMe else Skolem) tys sys of + -- We can't learn anything more about any variable at this point, so the only + -- cause of overlap can be by an instantiation of a touchable unification + -- variable. Hence we only bind touchable unification variables. In addition, + -- we use tcUnifyTys instead of tcMatchTys to rule out cyclic substitutions. + Nothing -> False + Just _ -> True + | otherwise = False -- No overlap with a solved, already been taken care of + -- by the overlap check with the instance environment. + matchable _tys ct = pprPanic "Expecting dictionary!" (ppr ct) + + does_not_originate_in_a_silent clas sys + -- UGLY: See Note [Silent parameters overlapping] - = null $ filter (tcEqPred (ClassP clas sys)) silents_and_their_scs ++ = null $ filter (eqPred (ClassP clas sys)) silents_and_their_scs + + silents_and_their_scs + = foldlBag (\acc rvnt -> case rvnt of + CDictCan { cc_id = d, cc_class = c, cc_tyargs = s } + | isSilentEvVar d -> (ClassP c s) : (transSuperClasses c s) ++ acc + _ -> acc) [] all_given_dicts + + -- TODO: + -- When silent parameters will go away we should simply select from + -- the given map of the inert set. + all_given_dicts = Map.fold unionBags emptyCCan (cts_given $ inert_dicts inerts) + \end{code} + +Note [Silent parameters overlapping] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +DV 12/05/2011: +The long-term goal is to completely remove silent superclass +parameters when checking instance declarations. But until then we must +make sure that we never prevent the application of an instance +declaration because of a potential match from a silent parameter -- +after all we are supposed to have solved that silent parameter from +some instance, anyway! In effect silent parameters behave more like +Solved than like Given. + +A concrete example appears in typecheck/SilentParametersOverlapping.hs + +Note [Instance and Given overlap] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Assume that we have an inert set that looks as follows: + [Given] D [Int] +And an instance declaration: + instance C a => D [a] +A new wanted comes along of the form: + [Wanted] D [alpha] + +One possibility is to apply the instance declaration which will leave us +with an unsolvable goal (C alpha). However, later on a new constraint may +arise (for instance due to a functional dependency between two later dictionaries), +that will add the equality (alpha ~ Int), in which case our ([Wanted] D [alpha]) +will be transformed to [Wanted] D [Int], which could have been discharged by the given. + +The solution is that in matchClassInst and eventually in topReact, we get back with +a matching instance, only when there is no Given in the inerts which is unifiable to +this particular dictionary. + +The end effect is that, much as we do for overlapping instances, we delay choosing a +class instance if there is a possibility of another instance OR a given to match our +constraint later on. This fixes bugs #4981 and #5002. + +This is arguably not easy to appear in practice due to our aggressive prioritization +of equality solving over other constraints, but it is possible. I've added a test case +in typecheck/should-compile/GivenOverlapping.hs + +Moreover notice that our goals here are different than the goals of the top-level +overlapping checks. There we are interested in validating the following principle: + + If we inline a function f at a site where the same global instance environment + is available as the instance environment at the definition site of f then we + should get the same behaviour. + +But for the Given Overlap check our goal is just related to completeness of +constraint solving. + + + + diff --combined compiler/typecheck/TcMType.lhs index fb5d8fb,531ee44..2c01d23 --- a/compiler/typecheck/TcMType.lhs +++ b/compiler/typecheck/TcMType.lhs @@@ -26,7 -26,6 +26,6 @@@ module TcMType -------------------------------- -- Creating new evidence variables newEvVar, newCoVar, newEvVars, - writeWantedCoVar, readWantedCoVar, newIP, newDict, newSilentGiven, isSilentEvVar, newWantedEvVar, newWantedEvVars, @@@ -43,16 -42,15 +42,15 @@@ -- Checking type validity Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType, SourceTyCtxt(..), checkValidTheta, - checkValidInstance, - checkValidTypeInst, checkTyFamFreeness, + checkValidInstHead, checkValidInstance, + checkInstTermination, checkValidTypeInst, checkTyFamFreeness, arityErr, growPredTyVars, growThetaTyVars, validDerivPred, -------------------------------- -- Zonking zonkType, mkZonkTcTyVar, zonkTcPredType, - zonkTcTypeCarefully, - skolemiseUnboundMetaTyVar, + zonkTcTypeCarefully, skolemiseUnboundMetaTyVar, zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkSigTyVar, zonkQuantifiedTyVar, zonkQuantifiedTyVars, zonkTcType, zonkTcTypes, zonkTcThetaType, @@@ -72,7 -70,6 +70,6 @@@ import TypeRep import TcType import Type - import Coercion import Class import TyCon import Var @@@ -145,7 -142,7 +142,7 @@@ newEvVar (IParam ip ty) = newIP i newCoVar :: TcType -> TcType -> TcM CoVar newCoVar ty1 ty2 - = do { name <- newName (mkTyVarOccFS (fsLit "co")) + = do { name <- newName (mkVarOccFS (fsLit "co")) ; return (mkCoVar name (mkPredTy (EqPred ty1 ty2))) } newIP :: IPName Name -> TcType -> TcM IpId @@@ -300,10 -297,6 +297,6 @@@ readMetaTyVar :: TyVar -> TcM MetaDetai readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar ) readMutVar (metaTvRef tyvar) - readWantedCoVar :: CoVar -> TcM MetaDetails - readWantedCoVar covar = ASSERT2( isMetaTyVar covar, ppr covar ) - readMutVar (metaTvRef covar) - isFilledMetaTyVar :: TyVar -> TcM Bool -- True of a filled-in (Indirect) meta type variable isFilledMetaTyVar tv @@@ -342,9 -335,6 +335,6 @@@ writeMetaTyVar tyvar t = WARN( True, text "Writing to non-meta tyvar" <+> ppr tyvar ) return () - writeWantedCoVar :: CoVar -> Coercion -> TcM () - writeWantedCoVar cv co = writeMetaTyVar cv co - -------------------- writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM () -- Here the tyvar is for error checking only; @@@ -627,8 -617,8 +617,8 @@@ zonkWantedEvVar :: WantedEvVar -> TcM W zonkWantedEvVar (EvVarX v l) = do { v' <- zonkEvVar v; return (EvVarX v' l) } zonkFlavor :: CtFlavor -> TcM CtFlavor -zonkFlavor (Given loc) = do { loc' <- zonkGivenLoc loc; return (Given loc') } -zonkFlavor fl = return fl +zonkFlavor (Given loc gk) = do { loc' <- zonkGivenLoc loc; return (Given loc' gk) } +zonkFlavor fl = return fl zonkGivenLoc :: GivenLoc -> TcM GivenLoc -- GivenLocs may have unification variables inside them! @@@ -750,13 -740,12 +740,12 @@@ zonkType zonk_tc_tyvar t -- The two interesting cases! go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar tyvar - | otherwise = liftM TyVarTy $ - zonkTyVar zonk_tc_tyvar tyvar + | otherwise = return (TyVarTy tyvar) -- Ordinary (non Tc) tyvars occur inside quantified types go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar ) do ty' <- go ty - tyvar' <- zonkTyVar zonk_tc_tyvar tyvar + tyvar' <- return tyvar return (ForAllTy tyvar' ty') go_pred (ClassP c tys) = do tys' <- mapM go tys @@@ -779,16 -768,6 +768,6 @@@ mkZonkTcTyVar unbound_var_fn tyva ; case cts of Flexi -> unbound_var_fn tyvar Indirect ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty } - - -- Zonk the kind of a non-TC tyvar in case it is a coercion variable - -- (their kind contains types). - zonkTyVar :: (TcTyVar -> TcM Type) -- What to do for a TcTyVar - -> TyVar -> TcM TyVar - zonkTyVar zonk_tc_tyvar tv - | isCoVar tv - = do { kind <- zonkType zonk_tc_tyvar (tyVarKind tv) - ; return $ setTyVarKind tv kind } - | otherwise = return tv \end{code} @@@ -1159,7 -1138,7 +1138,7 @@@ check_valid_theta ctxt theta = d warnTc (notNull dups) (dupPredWarn dups) mapM_ (check_pred_ty dflags ctxt) theta where - (_,dups) = removeDups tcCmpPred theta + (_,dups) = removeDups cmpPred theta ------------------------- check_pred_ty :: DynFlags -> SourceTyCtxt -> PredType -> TcM () @@@ -1281,7 -1260,7 +1260,7 @@@ checkAmbiguity forall_tyvars theta tau_ ambigErr :: PredType -> SDoc ambigErr pred - = sep [ptext (sLit "Ambiguous constraint") <+> quotes (pprPred pred), + = sep [ptext (sLit "Ambiguous constraint") <+> quotes (pprPredTy pred), nest 2 (ptext (sLit "At least one of the forall'd type variables mentioned by the constraint") $$ ptext (sLit "must be reachable from the type after the '=>'"))] \end{code} @@@ -1348,14 -1327,14 +1327,14 @@@ eqSuperClassErr pre 2 (ppr pred) badPredTyErr, eqPredTyErr, predTyVarErr :: PredType -> SDoc - badPredTyErr pred = ptext (sLit "Illegal constraint") <+> pprPred pred - eqPredTyErr pred = ptext (sLit "Illegal equational constraint") <+> pprPred pred + badPredTyErr pred = ptext (sLit "Illegal constraint") <+> pprPredTy pred + eqPredTyErr pred = ptext (sLit "Illegal equational constraint") <+> pprPredTy pred $$ parens (ptext (sLit "Use -XTypeFamilies to permit this")) predTyVarErr pred = sep [ptext (sLit "Non type-variable argument"), - nest 2 (ptext (sLit "in the constraint:") <+> pprPred pred)] + nest 2 (ptext (sLit "in the constraint:") <+> pprPredTy pred)] dupPredWarn :: [[PredType]] -> SDoc - dupPredWarn dups = ptext (sLit "Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups) + dupPredWarn dups = ptext (sLit "Duplicate constraint(s):") <+> pprWithCommas pprPredTy (map head dups) arityErr :: Outputable a => String -> a -> Int -> Int -> SDoc arityErr kind name n m @@@ -1503,7 -1482,7 +1482,7 @@@ checkInstTermination tys thet predUndecErr :: PredType -> SDoc -> SDoc predUndecErr pred msg = sep [msg, - nest 2 (ptext (sLit "in the constraint:") <+> pprPred pred)] + nest 2 (ptext (sLit "in the constraint:") <+> pprPredTy pred)] nomoreMsg, smallerMsg, undecidableMsg :: SDoc nomoreMsg = ptext (sLit "Variable occurs more often in a constraint than in the instance head") diff --combined compiler/typecheck/TcRnTypes.lhs index 40f6a8d,7d761eb..17e5dcb --- a/compiler/typecheck/TcRnTypes.lhs +++ b/compiler/typecheck/TcRnTypes.lhs @@@ -40,13 -40,11 +40,13 @@@ module TcRnTypes Implication(..), CtLoc(..), ctLocSpan, ctLocOrigin, setCtLocOrigin, CtOrigin(..), EqOrigin(..), - WantedLoc, GivenLoc, pushErrCtxt, + WantedLoc, GivenLoc, GivenKind(..), pushErrCtxt, - SkolemInfo(..), + SkolemInfo(..), - CtFlavor(..), pprFlavorArising, isWanted, isGiven, isDerived, + CtFlavor(..), pprFlavorArising, isWanted, + isGivenOrSolved, isGiven_maybe, + isDerived, FlavoredEvVar, -- Pretty printing @@@ -64,6 -62,7 +64,7 @@@ import HsSyn import HscTypes import Type + import Id ( evVarPred ) import Class ( Class ) import DataCon ( DataCon, dataConUserType ) import TcType @@@ -326,6 -325,7 +327,7 @@@ data IfLclEn -- plus which bit is currently being examined if_tv_env :: UniqFM TyVar, -- Nested tyvar bindings + -- (and coercions) if_id_env :: UniqFM Id -- Nested id binding } \end{code} @@@ -676,7 -676,6 +678,6 @@@ instance Outputable WhereFrom wher %************************************************************************ %* * Wanted constraints - These are forced to be in TcRnTypes because TcLclEnv mentions WantedConstraints WantedConstraint mentions CtLoc @@@ -903,7 -902,7 +904,7 @@@ pprEvVarTheta :: [EvVar] -> SDo pprEvVarTheta ev_vars = pprTheta (map evVarPred ev_vars) pprEvVarWithType :: EvVar -> SDoc - pprEvVarWithType v = ppr v <+> dcolon <+> pprPred (evVarPred v) + pprEvVarWithType v = ppr v <+> dcolon <+> pprPredTy (evVarPred v) pprWantedsWithLocs :: WantedConstraints -> SDoc pprWantedsWithLocs wcs @@@ -925,37 -924,35 +926,37 @@@ pprWantedEvVar (EvVarX v _) = \begin{code} data CtFlavor - = Given GivenLoc -- We have evidence for this constraint in TcEvBinds - | Derived WantedLoc - -- We have evidence for this constraint in TcEvBinds; - -- *however* this evidence can contain wanteds, so - -- it's valid only provisionally to the solution of - -- these wanteds - | Wanted WantedLoc -- We have no evidence bindings for this constraint. - --- data DerivedOrig = DerSC | DerInst | DerSelf --- Deriveds are either superclasses of other wanteds or deriveds, or partially --- solved wanteds from instances, or 'self' dictionaries containing yet wanted --- superclasses. + = Given GivenLoc GivenKind -- We have evidence for this constraint in TcEvBinds + | Derived WantedLoc -- Derived's are just hints for unifications + | Wanted WantedLoc -- We have no evidence bindings for this constraint. + +data GivenKind + = GivenOrig -- Originates in some given, such as signature or pattern match + | GivenSolved -- Is given as result of being solved, maybe provisionally on + -- some other wanted constraints. instance Outputable CtFlavor where - ppr (Given {}) = ptext (sLit "[G]") - ppr (Wanted {}) = ptext (sLit "[W]") - ppr (Derived {}) = ptext (sLit "[D]") + ppr (Given _ GivenOrig) = ptext (sLit "[G]") + ppr (Given _ GivenSolved) = ptext (sLit "[S]") -- Print [S] for Given/Solved's + ppr (Wanted {}) = ptext (sLit "[W]") + ppr (Derived {}) = ptext (sLit "[D]") + pprFlavorArising :: CtFlavor -> SDoc -pprFlavorArising (Derived wl ) = pprArisingAt wl +pprFlavorArising (Derived wl) = pprArisingAt wl pprFlavorArising (Wanted wl) = pprArisingAt wl -pprFlavorArising (Given gl) = pprArisingAt gl +pprFlavorArising (Given gl _) = pprArisingAt gl isWanted :: CtFlavor -> Bool isWanted (Wanted {}) = True isWanted _ = False -isGiven :: CtFlavor -> Bool -isGiven (Given {}) = True -isGiven _ = False +isGivenOrSolved :: CtFlavor -> Bool +isGivenOrSolved (Given {}) = True +isGivenOrSolved _ = False + +isGiven_maybe :: CtFlavor -> Maybe GivenKind +isGiven_maybe (Given _ gk) = Just gk +isGiven_maybe _ = Nothing isDerived :: CtFlavor -> Bool isDerived (Derived {}) = True diff --combined compiler/typecheck/TcSMonad.lhs index f527ff7,b2ce381..0992fb9 --- a/compiler/typecheck/TcSMonad.lhs +++ b/compiler/typecheck/TcSMonad.lhs @@@ -15,15 -15,13 +15,15 @@@ module TcSMonad CanonicalCt(..), Xi, tyVarsOfCanonical, tyVarsOfCanonicals, tyVarsOfCDicts, deCanonicalise, mkFrozenError, - isWanted, isGiven, isDerived, - isGivenCt, isWantedCt, isDerivedCt, pprFlavorArising, + isWanted, isGivenOrSolved, isDerived, + isGivenOrSolvedCt, isGivenCt_maybe, + isWantedCt, isDerivedCt, pprFlavorArising, isFlexiTcsTv, canRewrite, canSolve, - combineCtLoc, mkGivenFlavor, mkWantedFlavor, + combineCtLoc, mkSolvedFlavor, mkGivenFlavor, + mkWantedFlavor, getWantedLoc, TcS, runTcS, failTcS, panicTcS, traceTcS, -- Basic functionality @@@ -41,8 -39,6 +41,8 @@@ setWantedTyBind, + lookupFlatCacheMap, updateFlatCacheMap, + getInstEnvs, getFamInstEnvs, -- Getting the environments getTopEnv, getGblEnv, getTcEvBinds, getUntouchables, getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsMap, @@@ -86,6 -82,7 +86,7 @@@ import qualified TcRnMonad as Tc import qualified TcMType as TcM import qualified TcEnv as TcM ( checkWellStaged, topIdLvl, tcLookupFamInst, tcGetDefaultTys ) + import Kind import TcType import DynFlags @@@ -101,6 -98,7 +102,7 @@@ import Outputabl import Bag import MonadUtils import VarSet + import Pair import FastString import HsBinds -- for TcEvBinds stuff @@@ -108,8 -106,6 +110,8 @@@ import I import TcRnTypes import Data.IORef +import qualified Data.Map as Map + #ifdef DEBUG import StaticFlags( opt_PprStyle_Debug ) import Control.Monad( when ) @@@ -213,9 -209,9 +215,9 @@@ instance Outputable CanonicalCt wher ppr (CIPCan ip fl ip_nm ty) = ppr fl <+> ppr ip <+> dcolon <+> parens (ppr ip_nm <> dcolon <> ppr ty) ppr (CTyEqCan co fl tv ty) - = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyVarTy tv, ty) + = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (Pair (mkTyVarTy tv) ty) ppr (CFunEqCan co fl tc tys ty) - = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyConApp tc tys, ty) + = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (Pair (mkTyConApp tc tys) ty) ppr (CFrozenErr co fl) = ppr fl <+> pprEvVarWithType co \end{code} @@@ -339,16 -335,11 +341,16 @@@ getWantedLoc c isWantedCt :: CanonicalCt -> Bool isWantedCt ct = isWanted (cc_flavor ct) isDerivedCt :: CanonicalCt -> Bool isDerivedCt ct = isDerived (cc_flavor ct) +isGivenCt_maybe :: CanonicalCt -> Maybe GivenKind +isGivenCt_maybe ct = isGiven_maybe (cc_flavor ct) + +isGivenOrSolvedCt :: CanonicalCt -> Bool +isGivenOrSolvedCt ct = isGivenOrSolved (cc_flavor ct) + + canSolve :: CtFlavor -> CtFlavor -> Bool -- canSolve ctid1 ctid2 -- The constraint ctid1 can be used to solve ctid2 @@@ -373,27 -364,22 +375,27 @@@ canRewrite = canSolv combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc -- Precondition: At least one of them should be wanted -combineCtLoc (Wanted loc) _ = loc -combineCtLoc _ (Wanted loc) = loc -combineCtLoc (Derived loc ) _ = loc -combineCtLoc _ (Derived loc ) = loc +combineCtLoc (Wanted loc) _ = loc +combineCtLoc _ (Wanted loc) = loc +combineCtLoc (Derived loc ) _ = loc +combineCtLoc _ (Derived loc ) = loc combineCtLoc _ _ = panic "combineCtLoc: both given" -mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor -mkGivenFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk) -mkGivenFlavor (Derived loc) sk = Given (setCtLocOrigin loc sk) -mkGivenFlavor (Given loc) sk = Given (setCtLocOrigin loc sk) +mkSolvedFlavor :: CtFlavor -> SkolemInfo -> CtFlavor +-- To be called when we actually solve a wanted/derived (perhaps leaving residual goals) +mkSolvedFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk) GivenSolved +mkSolvedFlavor (Derived loc) sk = Given (setCtLocOrigin loc sk) GivenSolved +mkSolvedFlavor fl@(Given {}) _sk = pprPanic "Solving a given constraint!" $ ppr fl +mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor +mkGivenFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk) GivenOrig +mkGivenFlavor (Derived loc) sk = Given (setCtLocOrigin loc sk) GivenOrig +mkGivenFlavor fl@(Given {}) _sk = pprPanic "Solving a given constraint!" $ ppr fl mkWantedFlavor :: CtFlavor -> CtFlavor mkWantedFlavor (Wanted loc) = Wanted loc mkWantedFlavor (Derived loc) = Wanted loc -mkWantedFlavor fl@(Given {}) = pprPanic "mkWantedFlavour" (ppr fl) +mkWantedFlavor fl@(Given {}) = pprPanic "mkWantedFlavor" (ppr fl) \end{code} %************************************************************************ @@@ -428,33 -414,10 +430,33 @@@ data TcSEn tcs_untch :: TcsUntouchables, - tcs_ic_depth :: Int, -- Implication nesting depth - tcs_count :: IORef Int -- Global step count + tcs_ic_depth :: Int, -- Implication nesting depth + tcs_count :: IORef Int, -- Global step count + + tcs_flat_map :: IORef FlatCache } +data FlatCache + = FlatCache { givenFlatCache :: Map.Map FunEqHead (TcType,Coercion,CtFlavor) + -- Invariant: all CtFlavors here satisfy isGiven + , wantedFlatCache :: Map.Map FunEqHead (TcType,Coercion,CtFlavor) } + -- Invariant: all CtFlavors here satisfy isWanted + +emptyFlatCache :: FlatCache +emptyFlatCache + = FlatCache { givenFlatCache = Map.empty, wantedFlatCache = Map.empty } + +newtype FunEqHead = FunEqHead (TyCon,[Xi]) + +instance Eq FunEqHead where - FunEqHead (tc1,xis1) == FunEqHead (tc2,xis2) = tc1 == tc2 && tcEqTypes xis1 xis2 ++ FunEqHead (tc1,xis1) == FunEqHead (tc2,xis2) = tc1 == tc2 && eqTypes xis1 xis2 + +instance Ord FunEqHead where + FunEqHead (tc1,xis1) `compare` FunEqHead (tc2,xis2) + = case compare tc1 tc2 of - EQ -> tcCmpTypes xis1 xis2 ++ EQ -> cmpTypes xis1 xis2 + other -> other + type TcsUntouchables = (Untouchables,TcTyVarSet) -- Like the TcM Untouchables, -- but records extra TcsTv variables generated during simplification @@@ -551,14 -514,12 +553,14 @@@ runTcS context untouch tc = do { ty_binds_var <- TcM.newTcRef emptyVarEnv ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds ; step_count <- TcM.newTcRef 0 + ; flat_cache_var <- TcM.newTcRef emptyFlatCache ; let env = TcSEnv { tcs_ev_binds = ev_binds_var , tcs_ty_binds = ty_binds_var , tcs_context = context , tcs_untch = (untouch, emptyVarSet) -- No Tcs untouchables yet , tcs_count = step_count , tcs_ic_depth = 0 + , tcs_flat_map = flat_cache_var } -- Run the computation @@@ -585,31 -546,21 +587,31 @@@ nestImplicTcS ref (inner_range, inner_t , tcs_untch = (_outer_range, outer_tcs) , tcs_count = count , tcs_ic_depth = idepth - , tcs_context = ctxt } -> - let - inner_untch = (inner_range, outer_tcs `unionVarSet` inner_tcs) + , tcs_context = ctxt + , tcs_flat_map = orig_flat_cache_var + } -> + do { let inner_untch = (inner_range, outer_tcs `unionVarSet` inner_tcs) -- The inner_range should be narrower than the outer one -- (thus increasing the set of untouchables) but -- the inner Tcs-untouchables must be unioned with the -- outer ones! - nest_env = TcSEnv { tcs_ev_binds = ref - , tcs_ty_binds = ty_binds - , tcs_untch = inner_untch - , tcs_count = count - , tcs_ic_depth = idepth+1 - , tcs_context = ctxtUnderImplic ctxt } - in - thing_inside nest_env + + ; orig_flat_cache <- TcM.readTcRef orig_flat_cache_var + ; flat_cache_var <- TcM.newTcRef orig_flat_cache + -- One could be more conservative as well: + -- ; flat_cache_var <- TcM.newTcRef emptyFlatCache + + -- Consider copying the results the tcs_flat_map of the + -- incomping constraint, but we must make sure that we + -- have pushed everything in, which seems somewhat fragile + ; let nest_env = TcSEnv { tcs_ev_binds = ref + , tcs_ty_binds = ty_binds + , tcs_untch = inner_untch + , tcs_count = count + , tcs_ic_depth = idepth+1 + , tcs_context = ctxtUnderImplic ctxt + , tcs_flat_map = flat_cache_var } + ; thing_inside nest_env } recoverTcS :: TcS a -> TcS a -> TcS a recoverTcS (TcS recovery_code) (TcS thing_inside) @@@ -623,16 -574,14 +625,16 @@@ ctxtUnderImplic (SimplRuleLhs n) = Simp ctxtUnderImplic ctxt = ctxt tryTcS :: TcS a -> TcS a --- Like runTcS, but from within the TcS monad +-- Like runTcS, but from within the TcS monad -- Ignore all the evidence generated, and do not affect caller's evidence! -tryTcS tcs +tryTcS tcs = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv ; ev_binds_var <- TcM.newTcEvBinds + ; flat_cache_var <- TcM.newTcRef emptyFlatCache ; let env1 = env { tcs_ev_binds = ev_binds_var - , tcs_ty_binds = ty_binds_var } - ; unTcS tcs env1 }) + , tcs_ty_binds = ty_binds_var + , tcs_flat_map = flat_cache_var } + ; unTcS tcs env1 }) -- Update TcEvBinds -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@@ -655,51 -604,12 +657,51 @@@ getTcSTyBinds = TcS (return . tcs_ty_bi getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType)) getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef) +getFlatCacheMapVar :: TcS (IORef FlatCache) +getFlatCacheMapVar + = TcS (return . tcs_flat_map) + +lookupFlatCacheMap :: TyCon -> [Xi] -> CtFlavor + -> TcS (Maybe (TcType,Coercion,CtFlavor)) +-- For givens, we lookup in given flat cache +lookupFlatCacheMap tc xis (Given {}) + = do { cache_ref <- getFlatCacheMapVar + ; cache_map <- wrapTcS $ TcM.readTcRef cache_ref + ; return $ Map.lookup (FunEqHead (tc,xis)) (givenFlatCache cache_map) } +-- For wanteds, we first lookup in givenFlatCache. +-- If we get nothing back then we lookup in wantedFlatCache. +lookupFlatCacheMap tc xis (Wanted {}) + = do { cache_ref <- getFlatCacheMapVar + ; cache_map <- wrapTcS $ TcM.readTcRef cache_ref + ; case Map.lookup (FunEqHead (tc,xis)) (givenFlatCache cache_map) of + Nothing -> return $ Map.lookup (FunEqHead (tc,xis)) (wantedFlatCache cache_map) + other -> return other } +lookupFlatCacheMap _tc _xis (Derived {}) = return Nothing + +updateFlatCacheMap :: TyCon -> [Xi] + -> TcType -> CtFlavor -> Coercion -> TcS () +updateFlatCacheMap _tc _xis _tv (Derived {}) _co + = return () -- Not caching deriveds +updateFlatCacheMap tc xis ty fl co + = do { cache_ref <- getFlatCacheMapVar + ; cache_map <- wrapTcS $ TcM.readTcRef cache_ref + ; let new_cache_map + | isGivenOrSolved fl + = cache_map { givenFlatCache = Map.insert (FunEqHead (tc,xis)) (ty,co,fl) $ + givenFlatCache cache_map } + | isWanted fl + = cache_map { wantedFlatCache = Map.insert (FunEqHead (tc,xis)) (ty,co,fl) $ + wantedFlatCache cache_map } + | otherwise = pprPanic "updateFlatCacheMap, met Derived!" $ empty + ; wrapTcS $ TcM.writeTcRef cache_ref new_cache_map } + getTcEvBindsBag :: TcS EvBindMap getTcEvBindsBag = do { EvBindsVar ev_ref _ <- getTcEvBinds ; wrapTcS $ TcM.readTcRef ev_ref } + setCoBind :: CoVar -> Coercion -> TcS () setCoBind cv co = setEvBind cv (EvCoercion co) @@@ -769,7 -679,7 +771,7 @@@ checkWellStagedDFun pred dfun_id lo bind_lvl = TcM.topIdLvl dfun_id pprEq :: TcType -> TcType -> SDoc - pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2) + pprEq ty1 ty2 = pprPredTy $ mkEqPred (ty1,ty2) isTouchableMetaTyVar :: TcTyVar -> TcS Bool isTouchableMetaTyVar tv diff --combined compiler/typecheck/TcSimplify.lhs index 0b9bfaf,57ff636..bed0932 --- a/compiler/typecheck/TcSimplify.lhs +++ b/compiler/typecheck/TcSimplify.lhs @@@ -1,7 -1,7 +1,7 @@@ \begin{code} module TcSimplify( simplifyInfer, - simplifyDefault, simplifyDeriv, + simplifyDefault, simplifyDeriv, simplifyRule, simplifyTop, simplifyInteractive ) where @@@ -15,10 -15,12 +15,12 @@@ import TcTyp import TcSMonad import TcInteract import Inst - import Unify( niFixTvSubst, niSubstTvSet ) + import Id ( evVarPred ) + import Unify ( niFixTvSubst, niSubstTvSet ) import Var import VarSet import VarEnv + import Coercion import TypeRep import Name @@@ -747,26 -749,22 +749,26 @@@ solve_wanteds inert wanted@(WC { wc_fla unsolved_implics } -givensFromWanteds :: CanonicalCts -> Bag FlavoredEvVar --- Extract the *wanted* ones from CanonicalCts --- and make them into *givens* -givensFromWanteds = foldrBag getWanted emptyBag +givensFromWanteds :: SimplContext -> CanonicalCts -> Bag FlavoredEvVar +-- Extract the Wanted ones from CanonicalCts and conver to +-- Givens; not Given/Solved, see Note [Preparing inert set for implications] +givensFromWanteds _ctxt = foldrBag getWanted emptyBag where getWanted :: CanonicalCt -> Bag FlavoredEvVar -> Bag FlavoredEvVar getWanted cc givens - | not (isCFrozenErr cc) - , Wanted loc <- cc_flavor cc - , let given = mkEvVarX (cc_id cc) (Given (setCtLocOrigin loc UnkSkol)) - = given `consBag` givens - | otherwise - = givens -- We are not helping anyone by pushing a Derived in! - -- Because if we could not solve it to start with - -- we are not going to do either inside the impl constraint - + | pushable_wanted cc + = let given = mkEvVarX (cc_id cc) (mkGivenFlavor (cc_flavor cc) UnkSkol) + in given `consBag` givens -- and not mkSolvedFlavor, + -- see Note [Preparing inert set for implications] + | otherwise = givens + + pushable_wanted :: CanonicalCt -> Bool + pushable_wanted cc + | not (isCFrozenErr cc) + , isWantedCt cc + = isEqPred (evVarPred (cc_id cc)) -- see Note [Preparing inert set for implications] + | otherwise = False + solveNestedImplications :: InertSet -> CanonicalCts -> Bag Implication -> TcS (Bag FlavoredEvVar, Bag Implication) @@@ -776,18 -774,15 +778,18 @@@ solveNestedImplications just_given_iner | otherwise = do { -- See Note [Preparing inert set for implications] -- Push the unsolved wanteds inwards, but as givens - let pushed_givens = givensFromWanteds unsolved_cans + + ; simpl_ctx <- getTcSContext + + ; let pushed_givens = givensFromWanteds simpl_ctx unsolved_cans tcs_untouchables = filterVarSet isFlexiTcsTv $ tyVarsOfEvVarXs pushed_givens -- See Note [Extra TcsTv untouchables] ; traceTcS "solveWanteds: preparing inerts for implications {" (vcat [ppr tcs_untouchables, ppr pushed_givens]) - - ; (_, inert_for_implics) <- solveInteract just_given_inert pushed_givens + + ; (_, inert_for_implics) <- solveInteract just_given_inert pushed_givens ; traceTcS "solveWanteds: } now doing nested implications {" $ vcat [ text "inerts_for_implics =" <+> ppr inert_for_implics @@@ -938,42 -933,6 +940,42 @@@ We were not able to solve (a ~w [beta] given because the resulting set is not inert. Hence we have to do a 'solveInteract' step first. +Finally, note that we convert them to [Given] and NOT [Given/Solved]. +The reason is that Given/Solved are weaker than Givens and may be discarded. +As an example consider the inference case, where we may have, the following +original constraints: + [Wanted] F Int ~ Int + (F Int ~ a => F Int ~ a) +If we convert F Int ~ Int to [Given/Solved] instead of Given, then the next +given (F Int ~ a) is going to cause the Given/Solved to be ignored, casting +the (F Int ~ a) insoluble. Hence we should really convert the residual +wanteds to plain old Given. + +We need only push in unsolved equalities both in checking mode and inference mode: + + (1) In checking mode we should not push given dictionaries in because of +example LongWayOverlapping.hs, where we might get strange overlap +errors between far-away constraints in the program. But even in +checking mode, we must still push type family equations. Consider: + + type instance F True a b = a + type instance F False a b = b + + [w] F c a b ~ gamma + (c ~ True) => a ~ gamma + (c ~ False) => b ~ gamma + +Since solveCTyFunEqs happens at the very end of solving, the only way to solve +the two implications is temporarily consider (F c a b ~ gamma) as Given (NB: not +merely Given/Solved because it has to interact with the top-level instance +environment) and push it inside the implications. Now, when we come out again at +the end, having solved the implications solveCTyFunEqs will solve this equality. + + (2) In inference mode, we recheck the final constraint in checking mode and +hence we will be able to solve inner implications from top-level quantified +constraints nonetheless. + + Note [Extra TcsTv untouchables] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Furthemore, we record the inert set simplifier-generated unification @@@ -1029,7 -988,8 +1031,8 @@@ solveCTyFunEqs ct ; return (niFixTvSubst ni_subst, unsolved_can_cts) } where - solve_one (cv,tv,ty) = setWantedTyBind tv ty >> setCoBind cv ty + solve_one (cv,tv,ty) = do { setWantedTyBind tv ty + ; setCoBind cv (mkReflCo ty) } ------------ type FunEqBinds = (TvSubstEnv, [(CoVar, TcTyVar, TcType)]) @@@ -1072,7 -1032,7 +1075,7 @@@ getSolvableCTyFunEqs untch ct , not (tv `elemVarSet` niSubstTvSet tv_subst (tyVarsOfTypes xis)) -- Occurs check: see Note [Solving Family Equations], Point 2 - = ASSERT ( not (isGiven fl) ) + = ASSERT ( not (isGivenOrSolved fl) ) (cts_in, extendFunEqBinds feb cv tv (mkTyConApp tc xis)) dflt_funeq (cts_in, fun_eq_binds) ct