import TcCanonical
import VarSet
import Type
+import Unify
import Id
import Var
import HsBinds
import Inst( tyVarsOfEvVar )
-import InstEnv
import Class
import TyCon
import Name
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)
type AtomicInert = CanonicalCt -- constraint pulled from InertSet
type WorkItem = CanonicalCt -- constraint pulled from WorkList
--- A mixture of Given, Wanted, and Derived constraints.
--- We split between equalities and the rest to process equalities first.
-type WorkList = CanonicalCts
-
-unionWorkLists :: WorkList -> WorkList -> WorkList
-unionWorkLists = andCCan
-
-isEmptyWorkList :: WorkList -> Bool
-isEmptyWorkList = isEmptyCCan
-
-emptyWorkList :: WorkList
-emptyWorkList = emptyCCan
-
-workListFromCCan :: CanonicalCt -> WorkList
-workListFromCCan = singleCCan
-
------------------------
data StopOrContinue
= Stop -- Work item is consumed
, ptext (sLit "new work =") <+> ppr work <> comma
, ptext (sLit "stop =") <+> ppr stop])
-type SimplifierStage = WorkItem -> InertSet -> TcS StageResult
+type SubGoalDepth = Int -- Starts at zero; used to limit infinite
+ -- recursion of sub-goals
+type SimplifierStage = SubGoalDepth -> WorkItem -> InertSet -> TcS StageResult
-- Combine a sequence of simplifier 'stages' to create a pipeline
-runSolverPipeline :: [(String, SimplifierStage)]
- -> InertSet -> WorkItem
+runSolverPipeline :: SubGoalDepth
+ -> [(String, SimplifierStage)]
+ -> InertSet -> WorkItem
-> TcS (InertSet, WorkList)
-- Precondition: non-empty list of stages
-runSolverPipeline pipeline inerts workItem
+runSolverPipeline depth pipeline inerts workItem
= do { traceTcS "Start solver pipeline" $
vcat [ ptext (sLit "work item =") <+> ppr workItem
, ptext (sLit "inerts =") <+> ppr inerts]
; let itr_in = SR { sr_inerts = inerts
- , sr_new_work = emptyWorkList
- , sr_stop = ContinueWith workItem }
+ , sr_new_work = emptyWorkList
+ , sr_stop = ContinueWith workItem }
; itr_out <- run_pipeline pipeline itr_in
; let new_inert
= case sr_stop itr_out of
(SR { sr_new_work = accum_work
, sr_inerts = inerts
, sr_stop = ContinueWith work_item })
- = do { itr <- stage work_item inerts
+ = do { itr <- stage depth work_item inerts
; traceTcS ("Stage result (" ++ name ++ ")") (ppr itr)
- ; let itr' = itr { sr_new_work = accum_work `unionWorkLists` sr_new_work itr }
+ ; let itr' = itr { sr_new_work = accum_work `unionWorkList` sr_new_work itr }
; run_pipeline stages itr' }
\end{code}
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
-> (ct,evVarPred ev)) ws)
, text "inert = " <+> ppr inert ]
- ; (flag, inert_ret) <- foldlBagM (tryPreSolveAndInteract sctx dyn_flags) (True,inert) ws
+ ; can_ws <- mkCanonicalFEVs ws
+
+ ; (flag, inert_ret)
+ <- foldrWorkListM (tryPreSolveAndInteract sctx dyn_flags) (True,inert) can_ws
; traceTcS "solveInteract, after clever canonicalization (and interaction):" $
vcat [ text "No interaction happened = " <+> ppr flag
; return (flag, inert_ret) }
-
tryPreSolveAndInteract :: SimplContext
-> DynFlags
+ -> CanonicalCt
-> (Bool, InertSet)
- -> FlavoredEvVar
-> TcS (Bool, InertSet)
-- Returns: True if it was able to discharge this constraint AND all previous ones
-tryPreSolveAndInteract sctx dyn_flags (all_previous_discharged, inert)
- flavev@(EvVarX ev_var fl)
+tryPreSolveAndInteract sctx dyn_flags ct (all_previous_discharged, inert)
= do { let inert_cts = get_inert_cts (evVarPred ev_var)
- ; this_one_discharged <- dischargeFromCCans inert_cts flavev
+ ; this_one_discharged <-
+ if isCFrozenErr ct then
+ return False
+ else
+ dischargeFromCCans inert_cts ev_var fl
; if this_one_discharged
then return (all_previous_discharged, inert)
else do
- { extra_cts <- mkCanonical fl ev_var
- ; inert_ret <- solveInteractWithDepth (ctxtStkDepth dyn_flags,0,[])
- inert extra_cts
+ { inert_ret <- solveOneWithDepth (ctxtStkDepth dyn_flags,0,[]) ct inert
; return (False, inert_ret) } }
where
+ ev_var = cc_id ct
+ fl = cc_flavor ct
+
get_inert_cts (ClassP clas _)
| simplEqsOnly sctx = emptyCCan
| otherwise = fst (getRelevantCts clas (inert_dicts inert))
get_inert_cts (EqPred {})
= inert_eqs inert `unionBags` cCanMapToBag (inert_funeqs inert)
-dischargeFromCCans :: CanonicalCts -> FlavoredEvVar -> TcS Bool
-dischargeFromCCans cans (EvVarX ev fl)
- = Bag.foldlBagM discharge_ct False cans
- where discharge_ct :: Bool -> CanonicalCt -> TcS Bool
- discharge_ct True _ct = return True
- discharge_ct False ct
- | evVarPred (cc_id ct) `tcEqPred` evVarPred ev
- , cc_flavor ct `canSolve` fl
- = do { when (isWanted fl) $ set_ev_bind ev (cc_id ct)
- ; return True }
- where set_ev_bind x y
- | EqPred {} <- evVarPred y
- = setEvBind x (EvCoercion (mkCoVarCoercion y))
- | otherwise = setEvBind x (EvId y)
- discharge_ct False _ct = return False
+dischargeFromCCans :: CanonicalCts -> EvVar -> CtFlavor -> TcS Bool
+-- See if this (pre-canonicalised) work-item is identical to a
+-- one already in the inert set. Reasons:
+-- a) Avoid creating superclass constraints for millions of incoming (Num a) constraints
+-- b) Termination for improve_eqs in TcSimplify.simpl_loop
+dischargeFromCCans cans ev fl
+ = Bag.foldrBag discharge_ct (return False) cans
+ where
+ the_pred = evVarPred ev
+
+ discharge_ct :: CanonicalCt -> TcS Bool -> TcS Bool
+ discharge_ct ct _rest
+ | evVarPred (cc_id ct) `eqPred` the_pred
+ , cc_flavor ct `canSolve` fl
+ = do { when (isWanted fl) $ setEvBind ev (evVarTerm (cc_id ct))
+ -- Deriveds need no evidence
+ -- For Givens, we already have evidence, and we don't need it twice
+ ; return True }
+
+ discharge_ct _ct rest = rest
\end{code}
Note [Avoiding the superclass explosion]
constraints.
\begin{code}
-solveOne :: InertSet -> WorkItem -> TcS InertSet
-solveOne inerts workItem
+solveOne :: WorkItem -> InertSet -> TcS InertSet
+solveOne workItem inerts
= do { dyn_flags <- getDynFlags
- ; solveOneWithDepth (ctxtStkDepth dyn_flags,0,[]) inerts workItem
+ ; solveOneWithDepth (ctxtStkDepth dyn_flags,0,[]) workItem inerts
}
-----------------
solveInteractWithDepth :: (Int, Int, [WorkItem])
- -> InertSet -> WorkList -> TcS InertSet
-solveInteractWithDepth ctxt@(max_depth,n,stack) inert ws
+ -> WorkList -> InertSet -> TcS InertSet
+solveInteractWithDepth ctxt@(max_depth,n,stack) ws inert
| isEmptyWorkList ws
= return inert
| otherwise
= do { traceTcS "solveInteractWithDepth" $
vcat [ text "Current depth =" <+> ppr n
- , text "Max depth =" <+> ppr max_depth ]
+ , text "Max depth =" <+> ppr max_depth
+ , text "ws =" <+> ppr ws ]
+
- -- Solve equalities first
- ; let (eqs, non_eqs) = Bag.partitionBag isCTyEqCan ws
- ; is_from_eqs <- Bag.foldlBagM (solveOneWithDepth ctxt) inert eqs
- ; Bag.foldlBagM (solveOneWithDepth ctxt) is_from_eqs non_eqs }
+ ; foldrWorkListM (solveOneWithDepth ctxt) inert ws }
+ -- use foldr to preserve the order
------------------
-- Fully interact the given work item with an inert set, and return a
-- new inert set which has assimilated the new information.
solveOneWithDepth :: (Int, Int, [WorkItem])
- -> InertSet -> WorkItem -> TcS InertSet
-solveOneWithDepth (max_depth, n, stack) inert work
- = do { traceTcS0 (indent ++ "Solving {") (ppr work)
- ; (new_inert, new_work) <- runSolverPipeline thePipeline inert work
+ -> WorkItem -> InertSet -> TcS InertSet
+solveOneWithDepth (max_depth, depth, stack) work inert
+ = do { traceFireTcS depth (text "Solving {" <+> ppr work)
+ ; (new_inert, new_work) <- runSolverPipeline depth thePipeline inert work
- ; traceTcS0 (indent ++ "Subgoals:") (ppr new_work)
-
-- Recursively solve the new work generated
-- from workItem, with a greater depth
- ; res_inert <- solveInteractWithDepth (max_depth, n+1, work:stack)
- new_inert new_work
+ ; res_inert <- solveInteractWithDepth (max_depth, depth+1, work:stack) new_work new_inert
+
+ ; traceFireTcS depth (text "Done }" <+> ppr work)
- ; traceTcS0 (indent ++ "Done }") (ppr work)
; return res_inert }
- where
- indent = replicate (2*n) ' '
thePipeline :: [(String,SimplifierStage)]
thePipeline = [ ("interact with inert eqs", interactWithInertEqsStage)
\begin{code}
spontaneousSolveStage :: SimplifierStage
-spontaneousSolveStage workItem inerts
+spontaneousSolveStage depth workItem inerts
= do { mSolve <- trySpontaneousSolve workItem
; case mSolve of
, 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.
-- We do this *right now* (rather than just putting workItem'
-- back into the work-list) because we've solved
- -> do { (new_inert, new_work) <- runSolverPipeline
+ -> do { bumpStepCountTcS
+ ; traceFireTcS depth (ptext (sLit "Spontaneous (w/d)") <+> ppr workItem)
+ ; (new_inert, new_work) <- runSolverPipeline depth
[ ("recursive interact with inert eqs", interactWithInertEqsStage)
, ("recursive interact with inerts", interactWithInertsStage)
] inerts workItem'
| otherwise
-> -- Original was given; he must then be inert all right, and
-- workList' are all givens from flattening
- return $ SR { sr_new_work = emptyWorkList
- , sr_inerts = inerts `updInertSet` workItem'
- , sr_stop = Stop }
+ do { bumpStepCountTcS
+ ; traceFireTcS depth (ptext (sLit "Spontaneous (g)") <+> ppr workItem)
+ ; return $ SR { sr_new_work = emptyWorkList
+ , sr_inerts = inerts `updInertSet` workItem'
+ , sr_stop = Stop } }
SPError -> -- Return with no new work
return $ SR { sr_new_work = emptyWorkList
, sr_inerts = inerts
-- 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
| otherwise
= do { tch1 <- isTouchableMetaTyVar tv1
; if tch1 then trySpontaneousEqOneWay cv gw tv1 xi
- else do { traceTcS "Untouchable LHS, can't spontaneously solve workitem:" (ppr workItem)
+ else do { traceTcS "Untouchable LHS, can't spontaneously solve workitem:"
+ (ppr workItem)
; return SPCantSolve }
}
]
; 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) (setWantedCoBind 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}
-
-
*********************************************************************************
* *
The interact-with-inert Stage
* *
*********************************************************************************
+Note [The Solver Invariant]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We always add Givens first. So you might think that the solver has
+the invariant
+
+ If the work-item is Given,
+ then the inert item must Given
+
+But this isn't quite true. Suppose we have,
+ c1: [W] beta ~ [alpha], c2 : [W] blah, c3 :[W] alpha ~ Int
+After processing the first two, we get
+ c1: [G] beta ~ [alpha], c2 : [W] blah
+Now, c3 does not interact with the the given c1, so when we spontaneously
+solve c3, we must re-react it with the inert set. So we can attempt a
+reaction between inert c2 [W] and work-item c3 [G].
+
+It *is* true that [Solver Invariant]
+ If the work-item is Given,
+ AND there is a reaction
+ then the inert item must Given
+or, equivalently,
+ If the work-item is Given,
+ and the inert item is Wanted/Derived
+ then there is no reaction
+
\begin{code}
-- Interaction result of WorkItem <~> AtomicInert
data InteractResult
, ir_new_work :: WorkList
-- new work items to add to the WorkList
+
+ , ir_fire :: Maybe String -- Tells whether a rule fired, and if so what
}
-- What to do with the inert reactant.
-data InertAction = KeepInert
- | DropInert
- | KeepTransformedInert CanonicalCt -- Keep a slightly transformed inert
+data InertAction = KeepInert | DropInert
-mkIRContinue :: Monad m => WorkItem -> InertAction -> WorkList -> m InteractResult
-mkIRContinue wi keep newWork = return $ IR (ContinueWith wi) keep newWork
+mkIRContinue :: String -> WorkItem -> InertAction -> WorkList -> TcS InteractResult
+mkIRContinue rule wi keep newWork
+ = return $ IR { ir_stop = ContinueWith wi, ir_inert_action = keep
+ , ir_new_work = newWork, ir_fire = Just rule }
-mkIRStop :: Monad m => InertAction -> WorkList -> m InteractResult
-mkIRStop keep newWork = return $ IR Stop keep newWork
+mkIRStopK :: String -> WorkList -> TcS InteractResult
+mkIRStopK rule newWork
+ = return $ IR { ir_stop = Stop, ir_inert_action = KeepInert
+ , ir_new_work = newWork, ir_fire = Just rule }
-dischargeWorkItem :: Monad m => m InteractResult
-dischargeWorkItem = mkIRStop KeepInert emptyWorkList
+mkIRStopD :: String -> WorkList -> TcS InteractResult
+mkIRStopD rule newWork
+ = return $ IR { ir_stop = Stop, ir_inert_action = DropInert
+ , ir_new_work = newWork, ir_fire = Just rule }
noInteraction :: Monad m => WorkItem -> m InteractResult
-noInteraction workItem = mkIRContinue workItem KeepInert emptyWorkList
+noInteraction wi
+ = return $ IR { ir_stop = ContinueWith wi, ir_inert_action = KeepInert
+ , ir_new_work = emptyWorkList, ir_fire = Nothing }
data WhichComesFromInert = LeftComesFromInert | RightComesFromInert
-- See Note [Efficient Orientation]
-- interact the WorkItem with the entire equalities of the InertSet
interactWithInertEqsStage :: SimplifierStage
-interactWithInertEqsStage workItem inert
- = Bag.foldlBagM interactNext initITR (inert_eqs inert)
+interactWithInertEqsStage depth workItem inert
+ = Bag.foldrBagM (interactNext depth) initITR (inert_eqs inert)
+ -- use foldr to preserve the order
where
initITR = SR { sr_inerts = inert { inert_eqs = emptyCCan }
, sr_new_work = emptyWorkList
-- "Other" constraints it contains!
interactWithInertsStage :: SimplifierStage
-interactWithInertsStage workItem inert
+interactWithInertsStage depth workItem inert
= let (relevant, inert_residual) = getISRelevant workItem inert
initITR = SR { sr_inerts = inert_residual
, sr_new_work = emptyWorkList
, sr_stop = ContinueWith workItem }
- in Bag.foldlBagM interactNext initITR relevant
+ in Bag.foldrBagM (interactNext depth) initITR relevant
+ -- use foldr to preserve the order
where
getISRelevant :: CanonicalCt -> InertSet -> (CanonicalCts, InertSet)
getISRelevant (CFrozenErr {}) is = (emptyCCan, is)
, inert_ips = emptyCCanMap
, inert_funeqs = emptyCCanMap })
-interactNext :: StageResult -> AtomicInert -> TcS StageResult
-interactNext it inert
- | ContinueWith workItem <- sr_stop it
- = do { let inerts = sr_inerts it
-
- ; ir <- interactWithInert inert workItem
-
- -- New inerts depend on whether we KeepInert or not and must
- -- be updated with FD improvement information from the interaction result (ir)
- ; let inerts_new = case ir_inert_action ir of
- KeepInert -> inerts `updInertSet` inert
- DropInert -> inerts
- KeepTransformedInert inert' -> inerts `updInertSet` inert'
+interactNext :: SubGoalDepth -> AtomicInert -> StageResult -> TcS StageResult
+interactNext depth inert it
+ | ContinueWith work_item <- sr_stop it
+ = do { let inerts = sr_inerts it
+
+ ; IR { ir_new_work = new_work, ir_inert_action = inert_action
+ , ir_fire = fire_info, ir_stop = stop }
+ <- interactWithInert inert work_item
+
+ ; let mk_msg rule
+ = text rule <+> keep_doc
+ <+> vcat [ ptext (sLit "Inert =") <+> ppr inert
+ , ptext (sLit "Work =") <+> ppr work_item
+ , ppUnless (isEmptyWorkList new_work) $
+ ptext (sLit "New =") <+> ppr new_work ]
+ keep_doc = case inert_action of
+ KeepInert -> ptext (sLit "[keep]")
+ DropInert -> ptext (sLit "[drop]")
+ ; case fire_info of
+ Just rule -> do { bumpStepCountTcS
+ ; traceFireTcS depth (mk_msg rule) }
+ Nothing -> return ()
+
+ -- New inerts depend on whether we KeepInert or not
+ ; let inerts_new = case inert_action of
+ KeepInert -> inerts `updInertSet` inert
+ DropInert -> inerts
; return $ SR { sr_inerts = inerts_new
- , sr_new_work = sr_new_work it `unionWorkLists` ir_new_work ir
- , sr_stop = ir_stop ir } }
+ , sr_new_work = sr_new_work it `unionWorkList` new_work
+ , sr_stop = stop } }
| otherwise
= return $ it { sr_inerts = (sr_inerts it) `updInertSet` inert }
-- Do a single interaction of two constraints.
interactWithInert :: AtomicInert -> WorkItem -> TcS InteractResult
-interactWithInert inert workitem
- = do { ctxt <- getTcSContext
- ; let is_allowed = allowedInteraction (simplEqsOnly ctxt) inert workitem
+interactWithInert inert workItem
+ = do { ctxt <- getTcSContext
+ ; let is_allowed = allowedInteraction (simplEqsOnly ctxt) inert workItem
- ; if is_allowed then
- doInteractWithInert inert workitem
+ ; if is_allowed then
+ doInteractWithInert inert workItem
else
- noInteraction workitem
- }
+ noInteraction workItem
+ }
allowedInteraction :: Bool -> AtomicInert -> WorkItem -> Bool
-- Allowed interactions
-- Identical class constraints.
doInteractWithInert
- (CDictCan { cc_id = d1, cc_flavor = fl1, cc_class = cls1, cc_tyargs = tys1 })
- workItem@(CDictCan { cc_flavor = fl2, cc_class = cls2, cc_tyargs = tys2 })
- | cls1 == cls2 && (and $ zipWith tcEqType tys1 tys2)
- = solveOneFromTheOther (d1,fl1) workItem
+ 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 && 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
- work_item_pred_loc = (pty2, pprFlavorArising fl2)
inert_pred_loc = (pty1, pprFlavorArising fl1)
- loc = combineCtLoc fl1 fl2
- eqn_pred_locs = improveFromAnother work_item_pred_loc inert_pred_loc
- -- See Note [Efficient Orientation]
-
- ; derived_evs <- mkDerivedFunDepEqns loc eqn_pred_locs
- ; fd_work <- mapM mkCanonicalFEV derived_evs
- -- See Note [Generating extra equalities]
-
- ; mkIRContinue workItem KeepInert (unionManyBags fd_work)
- }
+ work_item_pred_loc = (pty2, pprFlavorArising fl2)
+ fd_eqns = improveFromAnother
+ inert_pred_loc -- the template
+ work_item_pred_loc -- the one we aim to rewrite
+ -- See Note [Efficient Orientation]
+
+ ; m <- rewriteWithFunDeps fd_eqns tys2 fl2
+ ; case m of
+ Nothing -> noInteraction workItem
+ Just (rewritten_tys2, cos2, fd_work)
+ | eqTypes tys1 rewritten_tys2
+ -> -- Solve him on the spot in this case
+ case fl2 of
+ Given {} -> pprPanic "Unexpected given" (ppr inertItem $$ ppr workItem)
+ Derived {} -> mkIRStopK "Cls/Cls fundep (solved)" fd_work
+ Wanted {}
+ | isDerived fl1
+ -> do { setDictBind d2 (EvCast d1 dict_co)
+ ; let inert_w = inertItem { cc_flavor = fl2 }
+ -- A bit naughty: we take the inert Derived,
+ -- turn it into a Wanted, use it to solve the work-item
+ -- and put it back into the work-list
+ -- Maybe rather than starting again, we could *replace* the
+ -- inert item, but its safe and simple to restart
+ ; mkIRStopD "Cls/Cls fundep (solved)" $
+ workListFromNonEq inert_w `unionWorkList` fd_work }
+ | otherwise
+ -> do { setDictBind d2 (EvCast d1 dict_co)
+ ; mkIRStopK "Cls/Cls fundep (solved)" fd_work }
+
+ | otherwise
+ -> -- We could not quite solve him, but we still rewrite him
+ -- Example: class C a b c | a -> b
+ -- Given: C Int Bool x, Wanted: C Int beta y
+ -- Then rewrite the wanted to C Int Bool y
+ -- but note that is still not identical to the given
+ -- The important thing is that the rewritten constraint is
+ -- inert wrt the given.
+ -- However it is not necessarily inert wrt previous inert-set items.
+ -- class C a b c d | a -> b, b c -> d
+ -- Inert: c1: C b Q R S, c2: C P Q a b
+ -- Work: C P alpha R beta
+ -- Does not react with c1; reacts with c2, with alpha:=Q
+ -- NOW it reacts with c1!
+ -- So we must stop, and put the rewritten constraint back in the work list
+ do { d2' <- newDictVar cls1 rewritten_tys2
+ ; case fl2 of
+ Given {} -> pprPanic "Unexpected given" (ppr inertItem $$ ppr workItem)
+ Wanted {} -> setDictBind d2 (EvCast d2' dict_co)
+ Derived {} -> return ()
+ ; let workItem' = workItem { cc_id = d2', cc_tyargs = rewritten_tys2 }
+ ; mkIRStopK "Cls/Cls fundep (partial)" $
+ workListFromNonEq workItem' `unionWorkList` fd_work }
+
+ where
+ dict_co = mkTyConAppCo (classTyCon cls1) cos2
+ }
-- Class constraint and given equality: use the equality to rewrite
-- the class constraint.
= do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,wfl,cl,xis)
-- Continue with rewritten Dictionary because we can only be in the
-- interactWithEqsStage, so the dictionary is inert.
- ; mkIRContinue rewritten_dict KeepInert emptyWorkList }
+ ; mkIRContinue "Eq/Cls" rewritten_dict KeepInert emptyWorkList }
doInteractWithInert (CDictCan { cc_id = dv, cc_flavor = ifl, cc_class = cl, cc_tyargs = xis })
workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
| wfl `canRewrite` ifl
, tv `elemVarSet` tyVarsOfTypes xis
= do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,ifl,cl,xis)
- ; mkIRContinue workItem DropInert (workListFromCCan rewritten_dict) }
+ ; mkIRContinue "Cls/Eq" workItem DropInert (workListFromNonEq rewritten_dict) }
-- Class constraint and given equality: use the equality to rewrite
-- the class constraint.
| ifl `canRewrite` wfl
, tv `elemVarSet` tyVarsOfType ty
= do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,wfl,nm,ty)
- ; mkIRContinue rewritten_ip KeepInert emptyWorkList }
+ ; mkIRContinue "Eq/IP" rewritten_ip KeepInert emptyWorkList }
doInteractWithInert (CIPCan { cc_id = ipid, cc_flavor = ifl, cc_ip_nm = nm, cc_ip_ty = ty })
workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
| wfl `canRewrite` ifl
, tv `elemVarSet` tyVarsOfType ty
= do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,ifl,nm,ty)
- ; mkIRContinue workItem DropInert (workListFromCCan rewritten_ip) }
+ ; mkIRContinue "IP/Eq" workItem DropInert (workListFromNonEq rewritten_ip) }
-- Two implicit parameter constraints. If the names are the same,
-- but their types are not, we generate a wanted type equality
-- 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
- mkIRContinue workItem DropInert emptyWorkList
+ -- For example, given let ?x::Int = 3 in let ?x::Bool = True in ...
+ -- we must *override* the outer one with the inner one
+ mkIRContinue "IP/IP override" workItem DropInert emptyWorkList
- | nm1 == nm2 && ty1 `tcEqType` ty2
- = solveOneFromTheOther (id1,ifl) workItem
+ | nm1 == nm2 && ty1 `eqType` ty2
+ = solveOneFromTheOther "IP/IP" (EvId id1,ifl) workItem
| nm1 == nm2
= -- See Note [When improvement happens]
- do { co_var <- newWantedCoVar ty2 ty1 -- See Note [Efficient Orientation]
- ; let flav = Wanted (combineCtLoc ifl wfl)
- ; cans <- mkCanonical flav co_var
- ; mkIRContinue workItem KeepInert cans }
-
-
+ do { co_var <- newCoVar ty2 ty1 -- See Note [Efficient Orientation]
+ ; let flav = Wanted (combineCtLoc ifl wfl)
+ ; cans <- mkCanonical flav co_var
+ ; case wfl of
+ Given {} -> pprPanic "Unexpected given IP" (ppr workItem)
+ Derived {} -> pprPanic "Unexpected derived IP" (ppr workItem)
+ Wanted {} ->
+ do { setIPBind (cc_id workItem) $
+ EvCast id1 (mkSymCo (mkCoVarCo co_var))
+ ; mkIRStopK "IP/IP interaction (solved)" cans }
+ }
-- Never rewrite a given with a wanted equality, and a type function
-- equality can never rewrite an equality. We rewrite LHS *and* RHS
| ifl `canRewrite` wfl
, tv `elemVarSet` tyVarsOfTypes (xi2:args) -- Rewrite RHS as well
= do { rewritten_funeq <- rewriteFunEq (cv1,tv,xi1) (cv2,wfl,tc,args,xi2)
- ; mkIRStop KeepInert (workListFromCCan rewritten_funeq) }
+ ; mkIRStopK "Eq/FunEq" (workListFromEq rewritten_funeq) }
-- Must Stop here, because we may no longer be inert after the rewritting.
-- Inert: function equality, work item: equality
| wfl `canRewrite` ifl
, tv `elemVarSet` tyVarsOfTypes (xi1:args) -- Rewrite RHS as well
= do { rewritten_funeq <- rewriteFunEq (cv2,tv,xi2) (cv1,ifl,tc,args,xi1)
- ; mkIRContinue workItem DropInert (workListFromCCan rewritten_funeq) }
+ ; mkIRContinue "FunEq/Eq" workItem DropInert (workListFromEq rewritten_funeq) }
-- One may think that we could (KeepTransformedInert rewritten_funeq)
-- but that is wrong, because it may end up not being inert with respect
-- to future inerts. Example:
, 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 (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
- ; mkIRStop KeepInert cans }
+ = 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)
- ; mkIRContinue workItem DropInert cans }
+ = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCo cv2,xi2) (cv1,fl1,xi1)
+ ; mkIRContinue "FunEq/FunEq" workItem DropInert cans }
where
- lhss_match = tc1 == tc2 && and (zipWith tcEqType args1 args2)
+ lhss_match = tc1 == tc2 && eqTypes args1 args2
doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
workItem@(CTyEqCan { cc_id = cv2, cc_flavor = fl2, cc_tyvar = tv2, cc_rhs = xi2 })
-- Check for matching LHS
| fl1 `canSolve` fl2 && tv1 == tv2
- = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
- ; mkIRStop KeepInert cans }
+ = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCo cv1,xi1) (cv2,fl2,xi2)
+ ; mkIRStopK "Eq/Eq lhs" cans }
| fl2 `canSolve` fl1 && tv1 == tv2
- = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
- ; mkIRContinue workItem DropInert cans }
+ = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCo cv2,xi2) (cv1,fl1,xi1)
+ ; mkIRContinue "Eq/Eq lhs" workItem DropInert cans }
+
-- Check for rewriting RHS
| fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfType xi2
= do { rewritten_eq <- rewriteEqRHS (cv1,tv1,xi1) (cv2,fl2,tv2,xi2)
- ; mkIRStop KeepInert rewritten_eq }
+ ; mkIRStopK "Eq/Eq rhs" rewritten_eq }
+
| fl2 `canRewrite` fl1 && tv2 `elemVarSet` tyVarsOfType xi1
= do { rewritten_eq <- rewriteEqRHS (cv2,tv2,xi2) (cv1,fl1,tv1,xi1)
- ; mkIRContinue workItem DropInert rewritten_eq }
+ ; mkIRContinue "Eq/Eq rhs" workItem DropInert rewritten_eq }
doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
(CFrozenErr { cc_id = cv2, cc_flavor = fl2 })
| fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfEvVar cv2
= do { rewritten_frozen <- rewriteFrozen (cv1, tv1, xi1) (cv2, fl2)
- ; mkIRStop KeepInert rewritten_frozen }
+ ; mkIRStopK "Frozen/Eq" rewritten_frozen }
doInteractWithInert (CFrozenErr { cc_id = cv2, cc_flavor = fl2 })
workItem@(CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
| fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfEvVar cv2
= do { rewritten_frozen <- rewriteFrozen (cv1, tv1, xi1) (cv2, fl2)
- ; mkIRContinue workItem DropInert rewritten_frozen }
+ ; mkIRContinue "Frozen/Eq" workItem DropInert rewritten_frozen }
-- Fall-through case for all other situations
doInteractWithInert _ workItem = noInteraction workItem
-- Equational Rewriting
rewriteDict :: (CoVar, TcTyVar, Xi) -> (DictId, CtFlavor, Class, [Xi]) -> TcS CanonicalCt
rewriteDict (cv,tv,xi) (dv,gw,cl,xis)
- = do { let cos = substTysWith [tv] [mkCoVarCoercion cv] xis -- xis[tv] ~ xis[xi]
+ = do { let cos = map (liftCoSubstWith [tv] [mkCoVarCo cv]) xis -- xis[tv] ~ xis[xi]
args = substTysWith [tv] [xi] xis
con = classTyCon cl
- dict_co = mkTyConCoercion con cos
+ dict_co = mkTyConAppCo con cos
; dv' <- newDictVar cl args
; case gw of
- Wanted {} -> setDictBind dv (EvCast dv' (mkSymCoercion dict_co))
+ Wanted {} -> setDictBind dv (EvCast dv' (mkSymCo dict_co))
Given {} -> setDictBind dv' (EvCast dv dict_co)
Derived {} -> return () -- Derived dicts we don't set any evidence
rewriteIP :: (CoVar,TcTyVar,Xi) -> (EvVar,CtFlavor, IPName Name, TcType) -> TcS CanonicalCt
rewriteIP (cv,tv,xi) (ipid,gw,nm,ty)
- = do { let ip_co = substTyWith [tv] [mkCoVarCoercion cv] ty -- ty[tv] ~ t[xi]
- ty' = substTyWith [tv] [xi] ty
+ = do { let ip_co = liftCoSubstWith [tv] [mkCoVarCo cv] ty -- ty[tv] ~ t[xi]
+ ty' = substTyWith [tv] [xi] ty
; ipid' <- newIPVar nm ty'
; case gw of
- Wanted {} -> setIPBind ipid (EvCast ipid' (mkSymCoercion ip_co))
+ Wanted {} -> setIPBind ipid (EvCast ipid' (mkSymCo ip_co))
Given {} -> setIPBind ipid' (EvCast ipid ip_co)
Derived {} -> return () -- Derived ips: we don't set any evidence
rewriteFunEq :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TyCon, [Xi], Xi) -> TcS CanonicalCt
rewriteFunEq (cv1,tv,xi1) (cv2,gw, tc,args,xi2) -- cv2 :: F args ~ xi2
- = do { let arg_cos = substTysWith [tv] [mkCoVarCoercion cv1] args
- args' = substTysWith [tv] [xi1] args
- fun_co = mkTyConCoercion tc arg_cos -- fun_co :: F args ~ F args'
+ = do { let co_subst = liftCoSubstWith [tv] [mkCoVarCo cv1]
+ arg_cos = map co_subst args
+ args' = substTysWith [tv] [xi1] args
+ fun_co = mkTyConAppCo tc arg_cos -- fun_co :: F args ~ F args'
xi2' = substTyWith [tv] [xi1] xi2
- xi2_co = substTyWith [tv] [mkCoVarCoercion cv1] xi2 -- xi2_co :: xi2 ~ xi2'
- ; cv2' <- case gw of
- Wanted {} -> do { cv2' <- newWantedCoVar (mkTyConApp tc args') xi2'
- ; setWantedCoBind cv2 $
- fun_co `mkTransCoercion`
- mkCoVarCoercion cv2' `mkTransCoercion` mkSymCoercion xi2_co
- ; return cv2' }
- Given {} -> newGivenCoVar (mkTyConApp tc args') xi2' $
- mkSymCoercion fun_co `mkTransCoercion`
- mkCoVarCoercion cv2 `mkTransCoercion` xi2_co
- Derived {} -> newDerivedId (EqPred (mkTyConApp tc args') xi2')
+ xi2_co = co_subst xi2 -- xi2_co :: xi2 ~ xi2'
+
+ ; cv2' <- newCoVar (mkTyConApp tc args') xi2'
+ ; case gw of
+ Wanted {} -> setCoBind cv2 (fun_co `mkTransCo`
+ mkCoVarCo cv2' `mkTransCo`
+ mkSymCo xi2_co)
+ Given {} -> setCoBind cv2' (mkSymCo fun_co `mkTransCo`
+ mkCoVarCo cv2 `mkTransCo`
+ xi2_co)
+ Derived {} -> return ()
; return (CFunEqCan { cc_id = cv2'
, cc_flavor = gw
rewriteEqRHS (cv1,tv1,xi1) (cv2,gw,tv2,xi2)
| Just tv2' <- tcGetTyVar_maybe xi2'
, tv2 == tv2' -- In this case xi2[xi1/tv1] = tv2, so we have tv2~tv2
- = do { when (isWanted gw) (setWantedCoBind cv2 (mkSymCoercion co2'))
- ; return emptyCCan }
+ = do { when (isWanted gw) (setCoBind cv2 (mkSymCo co2'))
+ ; return emptyWorkList }
| otherwise
- = do { cv2' <-
- case gw of
- Wanted {}
- -> do { cv2' <- newWantedCoVar (mkTyVarTy tv2) xi2'
- ; setWantedCoBind cv2 $
- mkCoVarCoercion cv2' `mkTransCoercion` mkSymCoercion co2'
- ; return cv2' }
- Given {}
- -> newGivenCoVar (mkTyVarTy tv2) xi2' $
- mkCoVarCoercion cv2 `mkTransCoercion` co2'
- Derived {}
- -> newDerivedId (EqPred (mkTyVarTy tv2) xi2')
-
- ; canEq gw cv2' (mkTyVarTy tv2) xi2'
- }
+ = do { cv2' <- newCoVar (mkTyVarTy tv2) xi2'
+ ; case gw of
+ Wanted {} -> setCoBind cv2 $ mkCoVarCo cv2' `mkTransCo`
+ mkSymCo co2'
+ Given {} -> setCoBind cv2' $ mkCoVarCo cv2 `mkTransCo`
+ co2'
+ Derived {} -> return ()
+ ; canEqToWorkList gw cv2' (mkTyVarTy tv2) xi2' }
where
xi2' = substTyWith [tv1] [xi1] xi2
- co2' = substTyWith [tv1] [mkCoVarCoercion cv1] xi2 -- xi2 ~ xi2[xi1/tv1]
-
+ co2' = liftCoSubstWith [tv1] [mkCoVarCo cv1] xi2 -- xi2 ~ xi2[xi1/tv1]
rewriteEqLHS :: WhichComesFromInert -> (Coercion,Xi) -> (CoVar,CtFlavor,Xi) -> TcS WorkList
-- Used to ineract two equalities of the following form:
-- First Equality: co1: (XXX ~ xi1)
-- Second Equality: cv2: (XXX ~ xi2)
--- Where the cv1 `canSolve` cv2 equality
+-- Where the cv1 `canRewrite` cv2 equality
-- We have an option of creating new work (xi1 ~ xi2) OR (xi2 ~ xi1),
-- See Note [Efficient Orientation] for that
-rewriteEqLHS which (co1,xi1) (cv2,gw,xi2)
- = do { cv2' <- case (isWanted gw, which) of
- (True,LeftComesFromInert) ->
- do { cv2' <- newWantedCoVar xi2 xi1
- ; setWantedCoBind cv2 $
- co1 `mkTransCoercion` mkSymCoercion (mkCoVarCoercion cv2')
- ; return cv2' }
- (True,RightComesFromInert) ->
- do { cv2' <- newWantedCoVar xi1 xi2
- ; setWantedCoBind cv2 $
- co1 `mkTransCoercion` mkCoVarCoercion cv2'
- ; return cv2' }
- (False,LeftComesFromInert) ->
- if isGiven gw then
- newGivenCoVar xi2 xi1 $
- mkSymCoercion (mkCoVarCoercion cv2) `mkTransCoercion` co1
- else newDerivedId (EqPred xi2 xi1)
- (False,RightComesFromInert) ->
- if isGiven gw then
- newGivenCoVar xi1 xi2 $
- mkSymCoercion co1 `mkTransCoercion` mkCoVarCoercion cv2
- else newDerivedId (EqPred xi1 xi2)
+rewriteEqLHS LeftComesFromInert (co1,xi1) (cv2,gw,xi2)
+ = do { cv2' <- newCoVar xi2 xi1
+ ; case gw of
+ Wanted {} -> setCoBind cv2 $
+ co1 `mkTransCo` mkSymCo (mkCoVarCo cv2')
+ Given {} -> setCoBind cv2' $
+ mkSymCo (mkCoVarCo cv2) `mkTransCo` co1
+ Derived {} -> return ()
+ ; mkCanonical gw cv2' }
+
+rewriteEqLHS RightComesFromInert (co1,xi1) (cv2,gw,xi2)
+ = do { cv2' <- newCoVar xi1 xi2
+ ; case gw of
+ Wanted {} -> setCoBind cv2 $
+ co1 `mkTransCo` mkCoVarCo cv2'
+ Given {} -> setCoBind cv2' $
+ mkSymCo co1 `mkTransCo` mkCoVarCo cv2
+ Derived {} -> return ()
; mkCanonical gw cv2' }
-
+
rewriteFrozen :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor) -> TcS WorkList
rewriteFrozen (cv1, tv1, xi1) (cv2, fl2)
- = do { cv2' <-
- case fl2 of
- Wanted {} -> do { cv2' <- newWantedCoVar ty2a' ty2b'
- -- ty2a[xi1/tv1] ~ ty2b[xi1/tv1]
- ; setWantedCoBind cv2 $
- co2a' `mkTransCoercion`
- mkCoVarCoercion cv2' `mkTransCoercion`
- mkSymCoercion co2b'
- ; return cv2' }
-
- Given {} -> newGivenCoVar ty2a' ty2b' $
- mkSymCoercion co2a' `mkTransCoercion`
- mkCoVarCoercion cv2 `mkTransCoercion`
- co2b'
-
- Derived {} -> newDerivedId (EqPred ty2a' ty2b')
- ; return (singleCCan $ CFrozenErr { cc_id = cv2', cc_flavor = fl2 }) }
+ = do { cv2' <- newCoVar ty2a' ty2b' -- ty2a[xi1/tv1] ~ ty2b[xi1/tv1]
+ ; case fl2 of
+ Wanted {} -> setCoBind cv2 $ co2a' `mkTransCo`
+ mkCoVarCo cv2' `mkTransCo`
+ mkSymCo co2b'
+
+ Given {} -> setCoBind cv2' $ mkSymCo co2a' `mkTransCo`
+ mkCoVarCo cv2 `mkTransCo`
+ co2b'
+
+ Derived {} -> return ()
+
+ ; return (workListFromNonEq $ CFrozenErr { cc_id = cv2', cc_flavor = fl2 }) }
where
(ty2a, ty2b) = coVarKind cv2 -- cv2 : ty2a ~ ty2b
ty2a' = substTyWith [tv1] [xi1] ty2a
ty2b' = substTyWith [tv1] [xi1] ty2b
- co2a' = substTyWith [tv1] [mkCoVarCoercion cv1] ty2a -- ty2a ~ ty2a[xi1/tv1]
- co2b' = substTyWith [tv1] [mkCoVarCoercion cv1] ty2b -- ty2b ~ ty2b[xi1/tv1]
+ co2a' = liftCoSubstWith [tv1] [mkCoVarCo cv1] ty2a -- ty2a ~ ty2a[xi1/tv1]
+ co2b' = liftCoSubstWith [tv1] [mkCoVarCo cv1] ty2b -- ty2b ~ ty2b[xi1/tv1]
-solveOneFromTheOther :: (EvVar, CtFlavor) -> CanonicalCt -> TcS InteractResult
--- First argument inert, second argument workitem. They both represent
--- wanted/given/derived evidence for the *same* predicate so we try here to
--- discharge one directly from the other.
+solveOneFromTheOther :: String -> (EvTerm, CtFlavor) -> CanonicalCt -> TcS InteractResult
+-- First argument inert, second argument work-item. They both represent
+-- wanted/given/derived evidence for the *same* predicate so
+-- we can discharge one directly from the other.
--
-- Precondition: value evidence only (implicit parameters, classes)
-- not coercion
-solveOneFromTheOther (iid,ifl) workItem
- | ifl `canSolve` wfl
- = do { when (isWanted wfl) $ setEvBind wid (EvId iid)
- -- Overwrite the binding, if one exists
- -- For Givens, which are lambda-bound, nothing to overwrite,
- ; dischargeWorkItem }
- | wfl `canSolve` ifl
- = do { when (isWanted ifl) $ setEvBind iid (EvId wid)
- ; mkIRContinue workItem DropInert emptyWorkList }
-
- | otherwise -- One of the two is Derived, we can just throw it away,
- -- preferrably the work item.
- = if isDerived wfl then dischargeWorkItem
- else mkIRContinue workItem DropInert emptyWorkList
+solveOneFromTheOther info (ev_term,ifl) workItem
+ | isDerived wfl
+ = mkIRStopK ("Solved[DW] " ++ info) emptyWorkList
+
+ | isDerived ifl -- The inert item is Derived, we can just throw it away,
+ -- The workItem is inert wrt earlier inert-set items,
+ -- 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
+ do { when (isWanted wfl) $ setEvBind wid ev_term
+ -- Overwrite the binding, if one exists
+ -- If both are Given, we already have evidence; no need to duplicate
+ ; mkIRStopK ("Solved " ++ info) emptyWorkList }
where
wfl = cc_flavor workItem
wid = cc_id workItem
-- only reacted with functional dependencies
-- arising from top-level instances.
-topReactionsStage :: SimplifierStage
-topReactionsStage 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 ->
- return $ SR { sr_inerts = inerts
- , sr_new_work = tir_new_work
- , sr_stop = 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
+ , 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 = Derived loc
- , cc_class = cls, cc_tyargs = xis })
- = do { fd_work <- findClassFunDeps cls xis loc
- ; if isEmptyWorkList fd_work then
- return NoTopInt
- else return $ SomeTopInt { tir_new_work = fd_work
- , tir_new_inert = ContinueWith workItem } }
+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)
+ ; m <- rewriteWithFunDeps fd_eqns xis fl
+ ; case m of
+ Nothing -> return NoTopInt
+ Just (xis',_,fd_work) ->
+ let workItem' = workItem { cc_tyargs = xis' }
+ -- Deriveds are not supposed to have identity (cc_id is unused!)
+ in return $ SomeTopInt { tir_new_work = fd_work
+ , tir_new_inert = ContinueWith workItem' } }
+
-- Wanted dictionary
-doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = 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
- ; case lkp_inst_res of
- NoInstance ->
- do { traceTcS "doTopReact/ no class instance for" (ppr dv)
- ; fd_work <- findClassFunDeps cls xis loc
- ; return $ SomeTopInt
- { tir_new_work = fd_work
- , tir_new_inert = ContinueWith workItem } }
-
- GenInst wtvs ev_term -> -- Solved
+ ; lkp_inst_res <- matchClassInst inerts cls xis loc
+ ; case lkp_inst_res of
+ NoInstance ->
+ do { traceTcS "doTopReact/ no class instance for" (ppr dv)
+
+ ; instEnvs <- getInstEnvs
+ ; let fd_eqns = improveFromInstEnv instEnvs
+ (ClassP cls xis, pprArisingAt loc)
+ ; m <- rewriteWithFunDeps fd_eqns xis fl
+ ; case m of
+ Nothing -> return NoTopInt
+ Just (xis',cos,fd_work) ->
+ do { let dict_co = mkTyConAppCo (classTyCon cls) cos
+ ; dv'<- newDictVar cls xis'
+ ; setDictBind dv (EvCast dv' dict_co)
+ ; let workItem' = CDictCan { cc_id = dv', cc_flavor = fl,
+ cc_class = cls, cc_tyargs = xis' }
+ ; return $
+ SomeTopInt { tir_new_work = workListFromNonEq workItem' `unionWorkList` fd_work
+ , tir_new_inert = Stop } } }
+
+ GenInst wtvs ev_term -- Solved
-- No need to do fundeps stuff here; the instance
-- matches already so we won't get any more info
-- from functional dependencies
- do { traceTcS "doTopReact/ found class instance for" (ppr dv)
- ; setDictBind dv ev_term
- ; inst_work <- canWanteds wtvs
- ; if null wtvs
+ | null wtvs
+ -> 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
-- No point in caching this in 'inert'; hence Stop
- then return $ SomeTopInt { tir_new_work = emptyWorkList
- , tir_new_inert = Stop }
-
- -- Solved and new wanted work produced, you may cache the
- -- (tentatively solved) dictionary as Given! (used to be: Derived)
- else do { let solved = makeSolvedByInst workItem
- ; return $ SomeTopInt
- { tir_new_work = inst_work
- , tir_new_inert = ContinueWith solved } }
- } }
+ ; return $ SomeTopInt { tir_new_work = emptyWorkList
+ , tir_new_inert = Stop } }
+
+ | otherwise
+ -> 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 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)
-- 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
- ; cv' <- case fl of
- Wanted {} -> do { cv' <- newWantedCoVar rhs_ty xi
- ; setWantedCoBind 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 }
+ 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
-
-----------------------
-findClassFunDeps :: Class -> [Xi] -> WantedLoc -> TcS WorkList
--- Look for a fundep reaction beween the wanted item
--- and a top-level instance declaration
-findClassFunDeps cls xis loc
- = do { instEnvs <- getInstEnvs
- ; let eqn_pred_locs = improveFromInstEnv (classInstances instEnvs)
- (ClassP cls xis, pprArisingAt loc)
- ; derived_evs <- mkDerivedFunDepEqns loc eqn_pred_locs
- -- NB: fundeps generate some wanted equalities, but
- -- we don't use their evidence for anything
- ; cts <- mapM mkCanonicalFEV derived_evs
- ; return $ unionManyBags cts }
+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=" <+> 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
-- (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 (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.
+
+
+
+
projects / ghc-hetmet.git / blobdiff