= 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
= 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
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)
-- 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
-- in which case the remaining arguments should
-- be dealt with by AppTys
fam_ty = mkTyConApp tc xi_args
- fam_co = fam_ty -- identity
-
- ; (ret_co, rhs_var, ct) <-
- if isGiven fl then
- do { rhs_var <- newFlattenSkolemTy fam_ty
- ; cv <- 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 $ (mkCoVarCoercion 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 $ (mkCoVarCoercion cv, rhs_var, ct) }
-
+ fam_co = fam_ty -- identity
+ ; (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
+ ; 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
+ ; 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
+ ; updateFlatCacheMap tc xi_args rhs_var fl ret_co
+ ; return $ (ret_co, rhs_var, singleCCan ct) } }
; return ( foldl AppTy rhs_var xi_rest
, foldl AppTy (mkSymCoercion ret_co
- `mkTransCoercion` mkTyConCoercion tc cos_args) cos_rest
- , ccs `extendCCans` ct) }
+ `mkTransCoercion` mkTyConCoercion tc cos_args) cos_rest
+ , ccs `andCCan` ct) }
flatten ctxt (PredTy pred)
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
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
= do { (xis,cos,ccs) <- flattenMany fl tys -- cos :: xis ~ tys
; let no_flattening_happened = isEmptyCCan ccs
dict_co = mkTyConCoercion (classTyCon cn) cos
- ; v_new <- if no_flattening_happened then return v
- else if isGiven fl then return v
+ ; 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 (mkSymCoercion dict_co))
+ ; when (isGivenOrSolved fl) $ setDictBind v' (EvCast v (mkSymCoercion dict_co))
-- NB: No more setting evidence for derived now
; return v' }
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
= 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]
(mkCoVarCoercion v2) (mkCoVarCoercion v3)
; setCoBind cv res_co
; return (v1,v2,v3) }
- else if isGiven fl then -- Given
+ else if isGivenOrSolved fl then -- Given
let co_orig = mkCoVarCoercion cv
coa = mkCsel1Coercion co_orig
cob = mkCsel2Coercion co_orig
mkFunCoercion (mkCoVarCoercion argv) (mkCoVarCoercion resv)
; return (argv,resv) }
- else if isGiven fl then
+ else if isGivenOrSolved fl then
let [arg,res] = decomposeCo 2 (mkCoVarCoercion cv)
in do { argv <- newGivenCoVar s1 s2 arg
; resv <- newGivenCoVar t1 t2 res
mkTyConCoercion tc1 (map mkCoVarCoercion argsv)
; return argsv }
- else if isGiven fl then
+ else if isGivenOrSolved fl then
let cos = decomposeCo (length tys1) (mkCoVarCoercion cv)
in zipWith3M newGivenCoVar tys1 tys2 cos
mkAppCoercion (mkCoVarCoercion cv1) (mkCoVarCoercion cv2)
; return (cv1,cv2) }
- else if isGiven fl then
+ else if isGivenOrSolved fl then
let co1 = mkLeftCoercion $ mkCoVarCoercion cv
co2 = mkRightCoercion $ mkCoVarCoercion cv
in do { cv1 <- newGivenCoVar s1 s2 co1
then do { cv' <- newCoVar s2 s1
; setCoBind cv $ mkSymCoercion (mkCoVarCoercion cv')
; return cv' }
- else if isGiven fl then
+ else if isGivenOrSolved fl then
newGivenCoVar s2 s1 (mkSymCoercion (mkCoVarCoercion cv))
else -- Derived
newDerivedId (EqPred s2 s1)
-- 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
+ ; 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
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
+ ; 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)
; 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)
import TcType
import TypeRep
import Type( isTyVarTy )
+import Unify ( tcMatchTys )
import Inst
import InstEnv
-- 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
| 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
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
<+> pprPred 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
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")])]
+ 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
----------------------
\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}
%************************************************************************
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
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
import TcCanonical
import VarSet
import Type
+import Unify
import Id
import Var
import Outputable
import TcRnTypes
+import TcMType ( isSilentEvVar )
import TcErrors
import TcSMonad
import Bag
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.
, 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)
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
discharge_ct ct _rest
| evVarPred (cc_id ct) `tcEqPred` 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)
-- Deriveds need no evidence
-- For Givens, we already have evidence, and we don't need it twice
, 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.
-- 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
; when (isWanted wd) (setCoBind cv 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}
| cls1 == cls2 && (and $ zipWith tcEqType 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
-- 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
, 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)
+ , Just GivenSolved <- isGiven_maybe fl1
+ = mkIRContinue "Funeq/Funeq" workItem DropInert emptyWorkList
+ | tc1 == tc2 && and (zipWith tcEqType 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)
; mkIRStopK "FunEq/FunEq" cans }
-- 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
-- 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
}
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.
-- 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)
, 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)
-- 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
, 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)
-- appears in an error message
-- See Note [Type synonym families] in TyCon
coe = mkTyConApp coe_tc rep_tys
- ; cv' <- case fl of
- Wanted {} -> do { cv' <- newCoVar rhs_ty xi
- ; setCoBind cv $
- coe `mkTransCoercion`
- mkCoVarCoercion cv'
- ; return cv' }
- Given {} -> newGivenCoVar xi rhs_ty $
- mkSymCoercion (mkCoVarCoercion cv) `mkTransCoercion` coe
- Derived {} -> newDerivedId (EqPred xi rhs_ty)
- ; can_cts <- mkCanonical fl cv'
- ; return $ SomeTopInt can_cts Stop }
+ ; case fl of
+ Wanted {} -> do { cv' <- newCoVar rhs_ty xi
+ ; setCoBind cv $
+ coe `mkTransCoercion` mkCoVarCoercion 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
+ ; 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}
= 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)
+ , 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
-- (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 []))
; 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
+
+ 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.
+
+
+
+
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!
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
\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
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
setWantedTyBind,
+ lookupFlatCacheMap, updateFlatCacheMap,
+
getInstEnvs, getFamInstEnvs, -- Getting the environments
getTopEnv, getGblEnv, getTcEvBinds, getUntouchables,
getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsMap,
import TcRnTypes
import Data.IORef
+import qualified Data.Map as Map
+
#ifdef DEBUG
import StaticFlags( opt_PprStyle_Debug )
import Control.Monad( when )
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
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}
%************************************************************************
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
+
+instance Ord FunEqHead where
+ FunEqHead (tc1,xis1) `compare` FunEqHead (tc2,xis2)
+ = case compare tc1 tc2 of
+ EQ -> tcCmpTypes xis1 xis2
+ other -> other
+
type TcsUntouchables = (Untouchables,TcTyVarSet)
-- Like the TcM Untouchables,
-- but records extra TcsTv variables generated during simplification
= 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
, 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 -- 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)
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
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
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)
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)
| 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
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
, 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
projects / ghc-hetmet.git / commitdiff