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 Merge remote branch 'origin/master' Fixed conflicts in: compiler/typecheck/TcCanonical.lhs compiler/typecheck/TcErrors.lhs compiler/typecheck/TcInteract.lhs --- febf1ced754a3996ac1a5877dcded87828560d1c diff --cc compiler/typecheck/TcCanonical.lhs index 711c356,44cff5e..2cb38a9 --- a/compiler/typecheck/TcCanonical.lhs +++ b/compiler/typecheck/TcCanonical.lhs @@@ -113,8 -112,8 +114,8 @@@ 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) } @@@ -149,43 -148,38 +150,42 @@@ flatten fl (TyConApp tc tys -- The type function might be *over* saturated -- in which case the remaining arguments should -- be dealt with by AppTys -- fam_ty = mkTyConApp tc xi_args - fam_co = fam_ty -- identity - 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) } @@@ -258,15 -249,15 +256,15 @@@ mkCanonical fl ev = case evVarPred ev o 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' } @@@ -469,11 -415,11 +426,10 @@@ canEq fl cv (FunTy s1 t1) (FunTy s2 t2 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) } @@@ -521,11 -451,11 +461,10 @@@ canEq fl cv (TyConApp tc1 tys1) (TyConA <- 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 @@@ -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,9 -723,9 +732,9 @@@ 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 @@@ -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') diff --cc compiler/typecheck/TcErrors.lhs index 0383e76,0d0a9f8..b199053 --- a/compiler/typecheck/TcErrors.lhs +++ b/compiler/typecheck/TcErrors.lhs @@@ -16,11 -16,8 +16,9 @@@ import TcSMona import TcType import TypeRep import Type( isTyVarTy ) +import Unify ( tcMatchTys ) - import Inst import InstEnv - import TyCon import Name import NameEnv @@@ -576,21 -572,9 +574,21 @@@ 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 diff --cc compiler/typecheck/TcInteract.lhs index 46eece8,fd66d0a..3833534 --- a/compiler/typecheck/TcInteract.lhs +++ b/compiler/typecheck/TcInteract.lhs @@@ -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 @@@ -1102,21 -1093,14 +1097,21 @@@ 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 }) @@@ -1812,34 -1788,18 +1808,33 @@@ doTopReact _inerts workItem@(CFunEqCan -- 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!" } @@@ -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 @@@ -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 --cc 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 diff --cc compiler/typecheck/TcSMonad.lhs index f527ff7,b2ce381..0992fb9 --- a/compiler/typecheck/TcSMonad.lhs +++ b/compiler/typecheck/TcSMonad.lhs @@@ -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