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=58339b06aff704834e8553faaa2db00d746b26f3 Merge remote branch 'origin/master' Fixed conflicts in: compiler/typecheck/TcCanonical.lhs compiler/typecheck/TcErrors.lhs compiler/typecheck/TcInteract.lhs --- diff --git a/compiler/typecheck/Inst.lhs b/compiler/typecheck/Inst.lhs index 5474cfa..378bbd6 100644 --- a/compiler/typecheck/Inst.lhs +++ b/compiler/typecheck/Inst.lhs @@ -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 @@ -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 diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs index 44cff5e..2cb38a9 100644 --- a/compiler/typecheck/TcCanonical.lhs +++ b/compiler/typecheck/TcCanonical.lhs @@ -93,7 +93,9 @@ expansions contain any type function applications would speed things up a bit; right now we waste a lot of energy traversing the same types multiple times. + \begin{code} + -- Flatten a bunch of types all at once. flattenMany :: CtFlavor -> [Type] -> TcS ([Xi], [Coercion], CanonicalCts) -- Coercions :: Xi ~ Type @@ -112,7 +114,7 @@ flatten ctxt ty -- Preserve type synonyms if possible -- We can tell if ty' is function-free by -- whether there are any floated constraints - ; if isEmptyCCan ccs then + ; if isReflCo co then return (ty, mkReflCo ty, emptyCCan) else return (xi, co, ccs) } @@ -140,7 +142,7 @@ flatten fl (TyConApp tc tys) -- 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 @@ -148,37 +150,41 @@ flatten fl (TyConApp tc tys) -- The type function might be *over* saturated -- in which case the remaining arguments should -- be dealt with by AppTys - fam_ty = mkTyConApp tc xi_args - fam_co = 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 (mkReflCo fam_ty) + ; let ct = CFunEqCan { cc_id = cv + , cc_flavor = fl -- Given + , cc_fun = tc + , cc_tyargs = xi_args + , cc_rhs = rhs_var } + ; let ret_co = mkCoVarCo cv + ; updateFlatCacheMap tc xi_args rhs_var fl ret_co + ; return $ (ret_co, rhs_var, singleCCan ct) } + | otherwise -> + -- Derived or Wanted: make a new *unification* flatten variable + do { rhs_var <- newFlexiTcSTy (typeKind fam_ty) + ; cv <- newCoVar fam_ty rhs_var + ; let ct = CFunEqCan { cc_id = cv + , cc_flavor = mkWantedFlavor fl + -- Always Wanted, not Derived + , cc_fun = tc + , cc_tyargs = xi_args + , cc_rhs = rhs_var } + ; let ret_co = mkCoVarCo cv + ; updateFlatCacheMap tc xi_args rhs_var fl ret_co + ; return $ (ret_co, rhs_var, singleCCan ct) } } ; return ( foldl AppTy rhs_var xi_rest - , foldl 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 @@ -223,7 +229,7 @@ canWanteds :: [WantedEvVar] -> TcS WorkList canWanteds = fmap unionWorkLists . mapM (\(EvVarX ev loc) -> mkCanonical (Wanted loc) ev) canGivens :: GivenLoc -> [EvVar] -> TcS WorkList -canGivens loc givens = do { ccs <- mapM (mkCanonical (Given loc)) givens +canGivens loc givens = do { ccs <- mapM (mkCanonical (Given loc GivenOrig)) givens ; return (unionWorkLists ccs) } mkCanonicals :: CtFlavor -> [EvVar] -> TcS WorkList @@ -239,6 +245,7 @@ mkCanonicalFEVs = foldrBagM canon_one emptyWorkList 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 @@ -249,15 +256,15 @@ mkCanonical fl ev = case evVarPred ev of canClassToWorkList :: CtFlavor -> EvVar -> Class -> [TcType] -> TcS WorkList canClassToWorkList fl v cn tys = do { (xis,cos,ccs) <- flattenMany fl tys -- cos :: xis ~ tys - ; let no_flattening_happened = isEmptyCCan ccs + ; 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 (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' } @@ -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 @@ -347,14 +354,18 @@ newSCWorkFromFlavored ev orig_flavor cls xis = 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] @@ -417,8 +428,7 @@ canEq fl cv (FunTy s1 t1) (FunTy s2 t2) ; setCoBind cv $ mkFunCo (mkCoVarCo argv) (mkCoVarCo resv) ; return (argv,resv) } - - else if isGiven fl then + else if isGivenOrSolved fl then let [arg,res] = decomposeCo 2 (mkCoVarCo cv) in do { argv <- newGivenCoVar s1 s2 arg ; resv <- newGivenCoVar t1 t2 res @@ -452,10 +462,9 @@ canEq fl cv (TyConApp tc1 tys1) (TyConApp tc2 tys2) do { argsv <- zipWithM newCoVar tys1 tys2 ; setCoBind 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 @@ -691,7 +700,7 @@ canEqLeaf _untch fl cv cls1 cls2 then do { cv' <- newCoVar s2 s1 ; setCoBind cv $ mkSymCo (mkCoVarCo cv') ; return cv' } - else if isGiven fl then + else if isGivenOrSolved fl then newGivenCoVar s2 s1 (mkSymCo (mkCoVarCo cv)) else -- Derived newDerivedId (EqPred s2 s1) @@ -723,9 +732,9 @@ canEqLeafOriented fl cv cls1@(FunCls fn tys1) s2 -- cv : F tys1 ; (xi2, co2, ccs2) <- flatten fl s2 -- Flatten entire RHS -- co2 :: xi2 ~ s2 ; let ccs = ccs1 `andCCan` ccs2 - no_flattening_happened = isEmptyCCan ccs - ; cv_new <- if no_flattening_happened then return cv - else if isGiven fl then return cv + 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 @@ -769,9 +778,9 @@ canEqLeafTyVarLeft fl cv tv s2 -- cv : tv ~ s2 ; case mxi2' of { Nothing -> canEqFailure fl cv ; Just xi2' -> - do { let no_flattening_happened = isEmptyCCan ccs2 - ; cv_new <- if no_flattening_happened then return cv - else if isGiven fl then return cv + do { let no_flattening_happened = isReflCo co + ; cv_new <- if no_flattening_happened then return cv + else if isGivenOrSolved fl then return cv else if isWanted fl then do { cv' <- newCoVar (mkTyVarTy tv) xi2' -- cv' : tv ~ xi2 ; setCoBind cv (mkCoVarCo cv' `mkTransCo` co) @@ -997,7 +1006,7 @@ instFunDepEqn fl (FDEqn { fd_qtvs = qtvs, fd_eqs = eqs ; 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) diff --git a/compiler/typecheck/TcErrors.lhs b/compiler/typecheck/TcErrors.lhs index 0d0a9f8..b199053 100644 --- a/compiler/typecheck/TcErrors.lhs +++ b/compiler/typecheck/TcErrors.lhs @@ -16,6 +16,7 @@ import TcSMonad import TcType import TypeRep import Type( isTyVarTy ) +import Unify ( tcMatchTys ) import Inst import InstEnv import TyCon @@ -104,7 +105,7 @@ reportTidyWanteds ctxt (WC { wc_flat = flats, wc_insol = insols, wc_impl = impli -- 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 @@ -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 @@ -418,18 +420,18 @@ couldNotDeduce :: [([EvVar], GivenLoc)] -> (ThetaType, CtOrigin) -> SDoc 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 @@ -575,18 +577,58 @@ reportOverlap ctxt inst_envs orig pred@(ClassP clas tys) <+> 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 ---------------------- @@ -832,9 +874,9 @@ flattenForAllErrorTcS fl ty _bad_eqs \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 --git a/compiler/typecheck/TcInstDcls.lhs b/compiler/typecheck/TcInstDcls.lhs index 503812a..954471f 100644 --- a/compiler/typecheck/TcInstDcls.lhs +++ b/compiler/typecheck/TcInstDcls.lhs @@ -799,6 +799,9 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds }) 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 @@ -877,7 +880,7 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds }) 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 diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs index fd66d0a..3833534 100644 --- a/compiler/typecheck/TcInteract.lhs +++ b/compiler/typecheck/TcInteract.lhs @@ -12,6 +12,7 @@ import BasicTypes import TcCanonical import VarSet import Type +import Unify import Id import Var @@ -30,6 +31,7 @@ import Coercion import Outputable import TcRnTypes +import TcMType ( isSilentEvVar ) import TcErrors import TcSMonad import Bag @@ -68,8 +70,11 @@ An InertSet is a bag of canonical constraints, with the following invariants: 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. @@ -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) @@ -327,7 +332,7 @@ solveInteractGiven inert gloc evs 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 @@ -527,7 +532,7 @@ spontaneousSolveStage depth workItem inerts , 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. @@ -568,7 +573,7 @@ data SPSolveResult = SPCantSolve | SPSolved WorkItem | SPError -- 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 @@ -726,9 +731,8 @@ solveWithIdentity cv wd tv 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} @@ -928,7 +932,7 @@ doInteractWithInert | 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 @@ -1032,7 +1036,7 @@ doInteractWithInert (CIPCan { cc_id = ipid, cc_flavor = ifl, cc_ip_nm = nm, cc_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 @@ -1093,6 +1097,13 @@ doInteractWithInert (CFunEqCan { cc_id = cv1, cc_flavor = fl1, cc_fun = tc1 , 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 eqType args1 args2) + , Just GivenSolved <- isGiven_maybe fl1 + = mkIRContinue "Funeq/Funeq" workItem DropInert emptyWorkList + | 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 (mkCoVarCo cv1,xi1) (cv2,fl2,xi2) ; mkIRStopK "FunEq/FunEq" cans } @@ -1289,6 +1300,10 @@ solveOneFromTheOther info (ev_term,ifl) workItem -- 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 @@ -1663,33 +1678,34 @@ data TopInteractResult -- 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 } @@ -1697,7 +1713,7 @@ allowedTopReaction :: Bool -> WorkItem -> Bool 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. @@ -1705,12 +1721,12 @@ doTopReact :: WorkItem -> TcS TopInteractResult -- 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) @@ -1724,10 +1740,10 @@ doTopReact workItem@(CDictCan { cc_flavor = fl@(Derived loc) , 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) @@ -1753,7 +1769,7 @@ doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = fl@(Wanted loc) -- 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 @@ -1762,25 +1778,29 @@ doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = fl@(Wanted loc) , 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) @@ -1788,25 +1808,40 @@ doTopReact (CFunEqCan { cc_id = cv, cc_flavor = fl -- RHS of a type function, so that it never -- appears in an error message -- See Note [Type synonym families] in TyCon - 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 `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 $ + 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} @@ -2010,15 +2045,25 @@ data LookupInstResult = 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=" <+> 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 @@ -2027,7 +2072,7 @@ matchClassInst clas tys loc -- (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 [])) @@ -2037,4 +2082,94 @@ matchClassInst clas tys loc ; 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 (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 --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs index 531ee44..2c01d23 100644 --- a/compiler/typecheck/TcMType.lhs +++ b/compiler/typecheck/TcMType.lhs @@ -617,8 +617,8 @@ zonkWantedEvVar :: WantedEvVar -> TcM WantedEvVar 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! diff --git a/compiler/typecheck/TcRnTypes.lhs b/compiler/typecheck/TcRnTypes.lhs index 7d761eb..17e5dcb 100644 --- a/compiler/typecheck/TcRnTypes.lhs +++ b/compiler/typecheck/TcRnTypes.lhs @@ -40,11 +40,13 @@ module TcRnTypes( Implication(..), CtLoc(..), ctLocSpan, ctLocOrigin, setCtLocOrigin, CtOrigin(..), EqOrigin(..), - WantedLoc, GivenLoc, pushErrCtxt, + WantedLoc, GivenLoc, GivenKind(..), pushErrCtxt, SkolemInfo(..), - CtFlavor(..), pprFlavorArising, isWanted, isGiven, isDerived, + CtFlavor(..), pprFlavorArising, isWanted, + isGivenOrSolved, isGiven_maybe, + isDerived, FlavoredEvVar, -- Pretty printing @@ -924,35 +926,37 @@ pprWantedEvVar (EvVarX v _) = pprEvVarWithType 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 --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs index b2ce381..0992fb9 100644 --- a/compiler/typecheck/TcSMonad.lhs +++ b/compiler/typecheck/TcSMonad.lhs @@ -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 @@ -39,6 +41,8 @@ module TcSMonad ( setWantedTyBind, + lookupFlatCacheMap, updateFlatCacheMap, + getInstEnvs, getFamInstEnvs, -- Getting the environments getTopEnv, getGblEnv, getTcEvBinds, getUntouchables, getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsMap, @@ -106,6 +110,8 @@ import Id import TcRnTypes import Data.IORef +import qualified Data.Map as Map + #ifdef DEBUG import StaticFlags( opt_PprStyle_Debug ) import Control.Monad( when ) @@ -335,11 +341,16 @@ getWantedLoc ct isWantedCt :: CanonicalCt -> Bool isWantedCt ct = isWanted (cc_flavor ct) -isGivenCt :: CanonicalCt -> Bool -isGivenCt ct = isGiven (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 @@ -364,22 +375,27 @@ canRewrite = canSolve 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} %************************************************************************ @@ -414,10 +430,33 @@ data TcSEnv 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 && eqTypes xis1 xis2 + +instance Ord FunEqHead where + FunEqHead (tc1,xis1) `compare` FunEqHead (tc2,xis2) + = case compare tc1 tc2 of + EQ -> cmpTypes xis1 xis2 + other -> other + type TcsUntouchables = (Untouchables,TcTyVarSet) -- Like the TcM Untouchables, -- but records extra TcsTv variables generated during simplification @@ -514,12 +553,14 @@ runTcS context untouch tcs = 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 @@ -546,21 +587,31 @@ nestImplicTcS ref (inner_range, inner_tcs) (TcS thing_inside) , 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) @@ -574,14 +625,16 @@ ctxtUnderImplic (SimplRuleLhs n) = SimplCheck (ptext (sLit "lhs of rule") 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 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -604,12 +657,51 @@ getTcSTyBinds = TcS (return . tcs_ty_binds) 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) diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs index 57ff636..bed0932 100644 --- a/compiler/typecheck/TcSimplify.lhs +++ b/compiler/typecheck/TcSimplify.lhs @@ -749,22 +749,26 @@ solve_wanteds inert wanted@(WC { wc_flat = flats, wc_impl = implics, wc_insol = 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) @@ -774,15 +778,18 @@ solveNestedImplications just_given_inert unsolved_cans implics | 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 @@ -933,6 +940,42 @@ We were not able to solve (a ~w [beta]) but we can't just assume it as 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 @@ -1032,7 +1075,7 @@ getSolvableCTyFunEqs untch cts , 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