3 solveInteract, AtomicInert,
4 InertSet, emptyInert, extendInertSet, extractUnsolved, solveOne,
8 #include "HsVersions.h"
28 import Control.Monad ( when )
36 import qualified Bag as Bag
37 import Control.Monad( zipWithM, unless )
38 import FastString ( sLit )
42 Note [InsertSet invariants]
43 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
45 An InertSet is a bag of canonical constraints, with the following invariants:
47 1 No two constraints react with each other.
49 A tricky case is when there exists a given (solved) dictionary
50 constraint and a wanted identical constraint in the inert set, but do
51 not react because reaction would create loopy dictionary evidence for
52 the wanted. See note [Recursive dictionaries]
54 2 Given equalities form an idempotent substitution [none of the
55 given LHS's occur in any of the given RHS's or reactant parts]
57 3 Wanted equalities also form an idempotent substitution
58 4 The entire set of equalities is acyclic.
60 5 Wanted dictionaries are inert with the top-level axiom set
62 6 Equalities of the form tv1 ~ tv2 always have a touchable variable
63 on the left (if possible).
64 7 No wanted constraints tv1 ~ tv2 with tv1 touchable. Such constraints
65 will be marked as solved right before being pushed into the inert set.
66 See note [Touchables and givens].
68 Note that 6 and 7 are /not/ enforced by canonicalization but rather by
69 insertion in the inert list, ie by TcInteract.
71 During the process of solving, the inert set will contain some
72 previously given constraints, some wanted constraints, and some given
73 constraints which have arisen from solving wanted constraints. For
74 now we do not distinguish between given and solved constraints.
76 Note that we must switch wanted inert items to given when going under an
77 implication constraint (when in top-level inference mode).
81 -- See Note [InertSet invariants]
83 newtype InertSet = IS (Bag.Bag CanonicalCt)
84 instance Outputable InertSet where
85 ppr (IS cts) = vcat (map ppr (Bag.bagToList cts))
88 data Inert = IS { class_inerts :: FiniteMap Class Atomics
89 ip_inerts :: FiniteMap Class Atomics
90 tyfun_inerts :: FiniteMap TyCon Atomics
91 tyvar_inerts :: FiniteMap TyVar Atomics
94 Later should we also separate out givens and wanteds?
97 emptyInert :: InertSet
98 emptyInert = IS Bag.emptyBag
100 extendInertSet :: InertSet -> AtomicInert -> InertSet
101 extendInertSet (IS cts) item = IS (cts `Bag.snocBag` item)
103 foldlInertSetM :: (Monad m) => (a -> AtomicInert -> m a) -> a -> InertSet -> m a
104 foldlInertSetM k z (IS cts) = Bag.foldlBagM k z cts
106 extractUnsolved :: InertSet -> (InertSet, CanonicalCts)
107 extractUnsolved (IS cts)
108 = (IS cts', unsolved)
109 where (unsolved, cts') = Bag.partitionBag isWantedCt cts
111 isWantedCt :: CanonicalCt -> Bool
112 isWantedCt ct = isWanted (cc_flavor ct)
115 Note [Touchables and givens]
116 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
117 Touchable variables will never show up in givens which are inputs to
118 the solver. However, touchables may show up in givens generated by the flattener.
133 which can be put in the inert set. Suppose we also have a wanted
137 We cannot rewrite the given G alpha ~g b using the wanted alpha ~w
138 Int. Instead, after reacting alpha ~w Int with the whole inert set,
139 we observe that we can solve it by unifying alpha with Int, so we mark
140 it as solved and put it back in the *work list*. [We also immediately unify
141 alpha := Int, without telling anyone, see trySpontaneousSolve function, to
142 avoid doing this in the end.]
144 Later, because it is solved (given, in effect), we can use it to rewrite
145 G alpha ~g b to G Int ~g b, which gets put back in the work list. Eventually,
146 we will dispatch the remaining wanted constraints using the top-level axioms.
148 Finally, note that after reacting a wanted equality with the entire inert set
149 we may end up with something like
153 which we should flip around to generate the solved constraint alpha ~s b.
155 %*********************************************************************
157 * Main Interaction Solver *
159 **********************************************************************
163 1. Canonicalise (unary)
164 2. Pairwise interaction (binary)
165 * Take one from work list
166 * Try all pair-wise interactions with each constraint in inert
167 3. Try to solve spontaneously for equalities involving touchables
168 4. Top-level interaction (binary wrt top-level)
169 Superclass decomposition belongs in (4), see note [Superclasses]
173 type AtomicInert = CanonicalCt -- constraint pulled from InertSet
174 type WorkItem = CanonicalCt -- constraint pulled from WorkList
175 type SWorkItem = WorkItem -- a work item we know is solved
177 type WorkList = CanonicalCts -- A mixture of Given, Wanted, and Solved
180 listToWorkList :: [WorkItem] -> WorkList
181 listToWorkList = Bag.listToBag
183 unionWorkLists :: WorkList -> WorkList -> WorkList
184 unionWorkLists = Bag.unionBags
186 foldlWorkListM :: (Monad m) => (a -> WorkItem -> m a) -> a -> WorkList -> m a
187 foldlWorkListM = Bag.foldlBagM
189 isEmptyWorkList :: WorkList -> Bool
190 isEmptyWorkList = Bag.isEmptyBag
192 emptyWorkList :: WorkList
193 emptyWorkList = Bag.emptyBag
196 = Stop -- Work item is consumed
197 | ContinueWith WorkItem -- Not consumed
199 instance Outputable StopOrContinue where
200 ppr Stop = ptext (sLit "Stop")
201 ppr (ContinueWith w) = ptext (sLit "ContinueWith") <+> ppr w
203 -- Results after interacting a WorkItem as far as possible with an InertSet
205 = SR { sr_inerts :: InertSet
206 -- The new InertSet to use (REPLACES the old InertSet)
207 , sr_new_work :: WorkList
208 -- Any new work items generated (should be ADDED to the old WorkList)
210 -- sr_stop = Just workitem => workitem is *not* in sr_inerts and
211 -- workitem is inert wrt to sr_inerts
212 , sr_stop :: StopOrContinue
215 instance Outputable StageResult where
216 ppr (SR { sr_inerts = inerts, sr_new_work = work, sr_stop = stop })
217 = ptext (sLit "SR") <+>
218 braces (sep [ ptext (sLit "inerts =") <+> ppr inerts <> comma
219 , ptext (sLit "new work =") <+> ppr work <> comma
220 , ptext (sLit "stop =") <+> ppr stop])
222 type SimplifierStage = WorkItem -> InertSet -> TcS StageResult
224 -- Combine a sequence of simplifier 'stages' to create a pipeline
225 runSolverPipeline :: [(String, SimplifierStage)]
226 -> InertSet -> WorkItem
227 -> TcS (InertSet, WorkList)
228 -- Precondition: non-empty list of stages
229 runSolverPipeline pipeline inerts workItem
230 = do { traceTcS "Start solver pipeline" $
231 vcat [ ptext (sLit "work item =") <+> ppr workItem
232 , ptext (sLit "inerts =") <+> ppr inerts]
234 ; let itr_in = SR { sr_inerts = inerts
235 , sr_new_work = emptyWorkList
236 , sr_stop = ContinueWith workItem }
237 ; itr_out <- run_pipeline pipeline itr_in
239 = case sr_stop itr_out of
240 Stop -> sr_inerts itr_out
241 ContinueWith item -> sr_inerts itr_out `extendInertSet` item
242 ; return (new_inert, sr_new_work itr_out) }
244 run_pipeline :: [(String, SimplifierStage)]
245 -> StageResult -> TcS StageResult
246 run_pipeline [] itr = return itr
247 run_pipeline _ itr@(SR { sr_stop = Stop }) = return itr
249 run_pipeline ((name,stage):stages)
250 (SR { sr_new_work = accum_work
252 , sr_stop = ContinueWith work_item })
253 = do { itr <- stage work_item inerts
254 ; traceTcS ("Stage result (" ++ name ++ ")") (ppr itr)
255 ; let itr' = itr { sr_new_work = sr_new_work itr
256 `unionWorkLists` accum_work }
257 ; run_pipeline stages itr' }
261 Inert: {c ~ d, F a ~ t, b ~ Int, a ~ ty} (all given)
262 Reagent: a ~ [b] (given)
264 React with (c~d) ==> IR (ContinueWith (a~[b])) True []
265 React with (F a ~ t) ==> IR (ContinueWith (a~[b])) False [F [b] ~ t]
266 React with (b ~ Int) ==> IR (ContinueWith (a~[Int]) True []
269 Inert: {c ~w d, F a ~g t, b ~w Int, a ~w ty}
272 React with (c ~w d) ==> IR (ContinueWith (a~[b])) True []
273 React with (F a ~g t) ==> IR (ContinueWith (a~[b])) True [] (can't rewrite given with wanted!)
277 Inert: {a ~ Int, F Int ~ b} (given)
278 Reagent: F a ~ b (wanted)
280 React with (a ~ Int) ==> IR (ContinueWith (F Int ~ b)) True []
281 React with (F Int ~ b) ==> IR Stop True [] -- after substituting we re-canonicalize and get nothing
284 -- Main interaction solver: we fully solve the worklist 'in one go',
285 -- returning an extended inert set.
287 -- See Note [Touchables and givens].
288 solveInteract :: InertSet -> WorkList -> TcS InertSet
289 solveInteract inert ws
290 = do { dyn_flags <- getDynFlags
291 ; solveInteractWithDepth (ctxtStkDepth dyn_flags,0,[]) inert ws
293 solveOne :: InertSet -> WorkItem -> TcS InertSet
294 solveOne inerts workItem
295 = do { dyn_flags <- getDynFlags
296 ; solveOneWithDepth (ctxtStkDepth dyn_flags,0,[]) inerts workItem
300 solveInteractWithDepth :: (Int, Int, [WorkItem])
301 -> InertSet -> WorkList -> TcS InertSet
302 solveInteractWithDepth ctxt@(max_depth,n,stack) inert ws
307 = solverDepthErrorTcS n stack
310 = do { traceTcS "solveInteractWithDepth" $
311 vcat [ text "Current depth =" <+> ppr n
312 , text "Max depth =" <+> ppr max_depth
314 ; foldlWorkListM (solveOneWithDepth ctxt) inert ws }
317 -- Fully interact the given work item with an inert set, and return a
318 -- new inert set which has assimilated the new information.
319 solveOneWithDepth :: (Int, Int, [WorkItem])
320 -> InertSet -> WorkItem -> TcS InertSet
321 solveOneWithDepth (max_depth, n, stack) inert work
322 = do { traceTcS0 (indent ++ "Solving {") (ppr work)
323 ; (new_inert, new_work) <- runSolverPipeline thePipeline inert work
325 ; traceTcS0 (indent ++ "Subgoals:") (ppr new_work)
327 -- Recursively solve the new work generated
328 -- from workItem, with a greater depth
329 ; res_inert <- solveInteractWithDepth (max_depth, n+1, work:stack)
332 ; traceTcS0 (indent ++ "Done }") (ppr work)
335 indent = replicate (2*n) ' '
337 thePipeline :: [(String,SimplifierStage)]
338 thePipeline = [ ("interact with inerts", interactWithInertsStage)
339 , ("spontaneous solve", spontaneousSolveStage)
340 , ("top-level reactions", topReactionsStage) ]
343 *********************************************************************************
345 The spontaneous-solve Stage
347 *********************************************************************************
350 spontaneousSolveStage :: SimplifierStage
351 spontaneousSolveStage workItem inerts
352 = do { mSolve <- trySpontaneousSolve workItem
354 Nothing -> -- no spontaneous solution for him, keep going
355 return $ SR { sr_new_work = emptyWorkList
357 , sr_stop = ContinueWith workItem }
359 Just workItem' -- He has been solved; workItem' is a Given
360 | isWantedCt workItem
361 -- Original was wanted we have now made him given so
362 -- we have to ineract him with the inerts again because
363 -- of the change in his status. This may produce some work.
364 -> do { traceTcS "recursive interact with inerts {" $ vcat
365 [ text "work = " <+> ppr workItem'
366 , text "inerts = " <+> ppr inerts ]
367 ; itr_again <- interactWithInertsStage workItem' inerts
368 ; case sr_stop itr_again of
369 Stop -> pprPanic "BUG: Impossible to happen" $
370 vcat [ text "Original workitem:" <+> ppr workItem
371 , text "Spontaneously solved:" <+> ppr workItem'
372 , text "Solved was consumed, when reacting with inerts:"
373 , nest 2 (ppr inerts) ]
374 ContinueWith workItem'' -- Now *this* guy is inert wrt to inerts
375 -> do { traceTcS "end recursive interact }" $ ppr workItem''
376 ; return $ SR { sr_new_work = sr_new_work itr_again
377 , sr_inerts = sr_inerts itr_again
378 `extendInertSet` workItem''
382 -> return $ SR { sr_new_work = emptyWorkList
383 , sr_inerts = inerts `extendInertSet` workItem'
386 -- @trySpontaneousSolve wi@ solves equalities where one side is a
387 -- touchable unification variable. Returns:
388 -- * Nothing if we were not able to solve it
389 -- * Just wi' if we solved it, wi' (now a "given") should be put in the work list.
390 -- See Note [Touchables and givens]
391 trySpontaneousSolve :: WorkItem -> TcS (Maybe SWorkItem)
392 trySpontaneousSolve (CTyEqCan { cc_id = cv, cc_flavor = gw, cc_tyvar = tv1, cc_rhs = xi })
393 | Just tv2 <- tcGetTyVar_maybe xi
394 = do { tch1 <- isTouchableMetaTyVar tv1
395 ; tch2 <- isTouchableMetaTyVar tv2
396 ; case (tch1, tch2) of
397 (True, True) -> trySpontaneousEqTwoWay cv gw tv1 tv2
398 (True, False) -> trySpontaneousEqOneWay cv gw tv1 xi
399 (False, True) | tyVarKind tv1 `isSubKind` tyVarKind tv2
400 -> trySpontaneousEqOneWay cv gw tv2 (mkTyVarTy tv1)
401 _ -> return Nothing }
403 = do { tch1 <- isTouchableMetaTyVar tv1
404 ; if tch1 then trySpontaneousEqOneWay cv gw tv1 xi
405 else return Nothing }
408 -- trySpontaneousSolve (CFunEqCan ...) = ...
409 -- See Note [No touchables as FunEq RHS] in TcSMonad
410 trySpontaneousSolve _ = return Nothing
413 trySpontaneousEqOneWay :: CoVar -> CtFlavor -> TcTyVar -> Xi
414 -> TcS (Maybe SWorkItem)
415 -- tv is a MetaTyVar, not untouchable
416 -- Precondition: kind(xi) is a sub-kind of kind(tv)
417 trySpontaneousEqOneWay cv gw tv xi
418 | not (isSigTyVar tv) || isTyVarTy xi
419 = solveWithIdentity cv gw tv xi
424 trySpontaneousEqTwoWay :: CoVar -> CtFlavor -> TcTyVar -> TcTyVar
425 -> TcS (Maybe SWorkItem)
426 -- Both tyvars are *touchable* MetaTyvars
427 -- By the CTyEqCan invariant, k2 `isSubKind` k1
428 trySpontaneousEqTwoWay cv gw tv1 tv2
430 , nicer_to_update_tv2 = solveWithIdentity cv gw tv2 (mkTyVarTy tv1)
431 | otherwise = ASSERT( k2 `isSubKind` k1 )
432 solveWithIdentity cv gw tv1 (mkTyVarTy tv2)
436 nicer_to_update_tv2 = isSigTyVar tv1 || isSystemName (Var.varName tv2)
439 Note [Loopy spontaneous solving]
440 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
441 Consider the original wanted:
442 wanted : Maybe (E alpha) ~ alpha
443 where E is a type family, such that E (T x) = x. After canonicalization,
444 as a result of flattening, we will get:
445 given : E alpha ~ fsk
446 wanted : alpha ~ Maybe fsk
447 where (fsk := E alpha, on the side). Now, if we spontaneously *solve*
448 (alpha := Maybe fsk) we are in trouble! Instead, we should refrain from solving
449 it and keep it as wanted. In inference mode we'll end up quantifying over
450 (alpha ~ Maybe (E alpha))
451 Hence, 'solveWithIdentity' performs a small occurs check before
452 actually solving. But this occurs check *must look through* flatten
455 Note [Avoid double unifications]
456 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
457 The spontaneous solver has to return a given which mentions the unified unification
458 variable *on the left* of the equality. Here is what happens if not:
459 Original wanted: (a ~ alpha), (alpha ~ Int)
460 We spontaneously solve the first wanted, without changing the order!
461 given : a ~ alpha [having unifice alpha := a]
462 Now the second wanted comes along, but he cannot rewrite the given, so we simply continue.
463 At the end we spontaneously solve that guy, *reunifying* [alpha := Int]
465 We avoid this problem by orienting the given so that the unification variable is on the left.
466 [Note that alternatively we could attempt to enforce this at canonicalization]
468 Avoiding double unifications is yet another reason to disallow touchable unification variables
469 as RHS of type family equations: F xis ~ alpha. Consider having already spontaneously solved
470 a wanted (alpha ~ [b]) by setting alpha := [b]. So the inert set looks like:
472 And now a new wanted (F tau ~ alpha) comes along. Since it does not react with anything
473 we will be left with a constraint (F tau ~ alpha) that must cause a unification of
474 (alpha := F tau) at some point (either in spontaneous solving, or at the end). But alpha
475 is *already* unified so we must not do anything to it. By disallowing naked touchables in
476 the RHS of constraints (in favor of introduced flatten skolems) we do not have to worry at
477 all about unifying or spontaneously solving (F xis ~ alpha) by unification.
481 solveWithIdentity :: CoVar -> CtFlavor -> TcTyVar -> Xi -> TcS (Maybe SWorkItem)
482 -- Solve with the identity coercion
483 -- Precondition: kind(xi) is a sub-kind of kind(tv)
484 -- See [New Wanted Superclass Work] to see why we do this for *given* as well
485 solveWithIdentity cv gw tv xi
486 | tv `elemVarSet` tyVarsOfUnflattenedType xi
487 -- Beware of Note [Loopy spontaneous solving]
488 -- Can't spontaneously solve loopy equalities
489 -- though they are not a type error
491 | not (isGiven gw) -- Wanted or Derived
492 = do { traceTcS "Sneaky unification:" $
493 vcat [text "Coercion variable: " <+> ppr gw,
494 text "Coercion: " <+> pprEq (mkTyVarTy tv) xi,
495 text "Left Kind is : " <+> ppr (typeKind (mkTyVarTy tv)),
496 text "Right Kind is : " <+> ppr (typeKind xi)
498 ; setWantedTyBind tv xi -- Set tv := xi
499 ; cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi xi
500 -- Create new given with identity evidence
503 Wanted {} -> setWantedCoBind cv xi
504 Derived {} -> setDerivedCoBind cv xi
505 _ -> pprPanic "Can't spontaneously solve *given*" empty
507 ; let solved = CTyEqCan { cc_id = cv_given
508 , cc_flavor = mkGivenFlavor gw UnkSkol
509 , cc_tyvar = tv, cc_rhs = xi }
510 -- See Note [Avoid double unifications]
512 -- The reason that we create a new given variable (cv_given) instead of reusing cv
513 -- is because we do not want to end up with coercion unification variables in the givens.
514 ; return (Just solved) }
518 tyVarsOfUnflattenedType :: TcType -> TcTyVarSet
519 -- A version of tyVarsOfType which looks through flatSkols
520 tyVarsOfUnflattenedType ty
521 = foldVarSet (unionVarSet . do_tv) emptyVarSet (tyVarsOfType ty)
523 do_tv :: TyVar -> TcTyVarSet
524 do_tv tv = ASSERT( isTcTyVar tv)
525 case tcTyVarDetails tv of
526 FlatSkol ty -> tyVarsOfUnflattenedType ty
531 *********************************************************************************
533 The interact-with-inert Stage
535 *********************************************************************************
538 -- Interaction result of WorkItem <~> AtomicInert
540 = IR { ir_stop :: StopOrContinue
542 -- => Reagent (work item) consumed.
543 -- ContinueWith new_reagent
544 -- => Reagent transformed but keep gathering interactions.
545 -- The transformed item remains inert with respect
546 -- to any previously encountered inerts.
548 , ir_inert_action :: InertAction
549 -- Whether the inert item should remain in the InertSet.
551 , ir_new_work :: WorkList
552 -- new work items to add to the WorkList
555 -- What to do with the inert reactant.
556 data InertAction = KeepInert | DropInert
559 mkIRContinue :: Monad m => WorkItem -> InertAction -> WorkList -> m InteractResult
560 mkIRContinue wi keep newWork = return $ IR (ContinueWith wi) keep newWork
562 mkIRStop :: Monad m => InertAction -> WorkList -> m InteractResult
563 mkIRStop keep newWork = return $ IR Stop keep newWork
565 dischargeWorkItem :: Monad m => m InteractResult
566 dischargeWorkItem = mkIRStop KeepInert emptyCCan
568 noInteraction :: Monad m => WorkItem -> m InteractResult
569 noInteraction workItem = mkIRContinue workItem KeepInert emptyCCan
571 data WhichComesFromInert = LeftComesFromInert | RightComesFromInert
573 ---------------------------------------------------
574 -- Interact a single WorkItem with an InertSet as far as possible, i.e. until we get a Stop
575 -- result from an individual interaction (i.e. when the WorkItem is consumed), or until we've
576 -- interacted the WorkItem with the entire InertSet.
578 -- Postcondition: the new InertSet in the resulting StageResult is subset
579 -- of the input InertSet.
581 interactWithInertsStage :: SimplifierStage
582 interactWithInertsStage workItem inert
583 = foldlInertSetM interactNext initITR inert
585 initITR = SR { sr_inerts = emptyInert
586 , sr_new_work = emptyCCan
587 , sr_stop = ContinueWith workItem }
589 interactNext :: StageResult -> AtomicInert -> TcS StageResult
590 interactNext it inert
591 | ContinueWith workItem <- sr_stop it
592 = do { ir <- interactWithInert inert workItem
593 ; let inerts = sr_inerts it
594 ; return $ SR { sr_inerts = if ir_inert_action ir == KeepInert
595 then inerts `extendInertSet` inert
597 , sr_new_work = sr_new_work it `unionWorkLists` ir_new_work ir
598 , sr_stop = ir_stop ir } }
599 | otherwise = return $ itrAddInert inert it
602 itrAddInert :: AtomicInert -> StageResult -> StageResult
603 itrAddInert inert itr = itr { sr_inerts = (sr_inerts itr) `extendInertSet` inert }
605 -- Do a single interaction of two constraints.
606 interactWithInert :: AtomicInert -> WorkItem -> TcS InteractResult
607 interactWithInert inert workitem
608 = do { ctxt <- getTcSContext
609 ; let is_allowed = allowedInteraction (simplEqsOnly ctxt) inert workitem
610 inert_ev = cc_id inert
611 work_ev = cc_id workitem
613 -- Never interact a wanted and a derived where the derived's evidence
614 -- mentions the wanted evidence in an unguarded way.
615 -- See Note [Superclasses and recursive dictionaries]
616 -- and Note [New Wanted Superclass Work]
617 -- We don't have to do this for givens, as we fully know the evidence for them.
619 case (cc_flavor inert, cc_flavor workitem) of
620 (Wanted loc, Derived _) -> isGoodRecEv work_ev (WantedEvVar inert_ev loc)
621 (Derived _, Wanted loc) -> isGoodRecEv inert_ev (WantedEvVar work_ev loc)
624 ; if is_allowed && rec_ev_ok then
625 doInteractWithInert inert workitem
627 noInteraction workitem
630 allowedInteraction :: Bool -> AtomicInert -> WorkItem -> Bool
631 -- Allowed interactions
632 allowedInteraction eqs_only (CDictCan {}) (CDictCan {}) = not eqs_only
633 allowedInteraction eqs_only (CIPCan {}) (CIPCan {}) = not eqs_only
634 allowedInteraction _ _ _ = True
636 --------------------------------------------
637 doInteractWithInert :: CanonicalCt -> CanonicalCt -> TcS InteractResult
638 -- Identical class constraints.
641 (CDictCan { cc_id = d1, cc_flavor = fl1, cc_class = cls1, cc_tyargs = tys1 })
642 workItem@(CDictCan { cc_id = d2, cc_flavor = fl2, cc_class = cls2, cc_tyargs = tys2 })
643 | cls1 == cls2 && (and $ zipWith tcEqType tys1 tys2)
644 = solveOneFromTheOther (d1,fl1) workItem
646 | cls1 == cls2 && (not (isGiven fl1 && isGiven fl2))
647 = -- See Note [When improvement happens]
648 do { let work_item_pred_loc = (ClassP cls2 tys2, ppr d2)
649 inert_pred_loc = (ClassP cls1 tys1, ppr d1)
650 loc = combineCtLoc fl1 fl2
651 eqn_pred_locs = improveFromAnother work_item_pred_loc inert_pred_loc
652 ; wevvars <- mkWantedFunDepEqns loc eqn_pred_locs
653 -- See Note [Generating extra equalities]
654 ; workList <- canWanteds wevvars
655 ; mkIRContinue workItem KeepInert workList -- Keep the inert there so we avoid
656 -- re-introducing the fundep equalities
657 -- See Note [FunDep Reactions]
660 -- Class constraint and given equality: use the equality to rewrite
661 -- the class constraint.
662 doInteractWithInert (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi })
663 (CDictCan { cc_id = dv, cc_flavor = wfl, cc_class = cl, cc_tyargs = xis })
664 | ifl `canRewrite` wfl
665 , tv `elemVarSet` tyVarsOfTypes xis
666 -- substitute for tv in xis. Note that the resulting class
667 -- constraint is still canonical, since substituting xi-types in
668 -- xi-types generates xi-types. However, it may no longer be
669 -- inert with respect to the inert set items we've already seen.
670 -- For example, consider the inert set
675 -- and the work item D a (w). D a does not interact with D Int.
676 -- Next, it does interact with a ~g Int, getting rewritten to D
677 -- Int (w). But now we must go back through the rest of the inert
678 -- set again, to find that it can now be discharged by the given D
680 = do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,wfl,cl,xis)
681 ; mkIRStop KeepInert (singleCCan rewritten_dict) }
683 doInteractWithInert (CDictCan { cc_id = dv, cc_flavor = ifl, cc_class = cl, cc_tyargs = xis })
684 workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
685 | wfl `canRewrite` ifl
686 , tv `elemVarSet` tyVarsOfTypes xis
687 = do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,ifl,cl,xis)
688 ; mkIRContinue workItem DropInert (singleCCan rewritten_dict) }
690 -- Class constraint and given equality: use the equality to rewrite
691 -- the class constraint.
692 doInteractWithInert (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi })
693 (CIPCan { cc_id = ipid, cc_flavor = wfl, cc_ip_nm = nm, cc_ip_ty = ty })
694 | ifl `canRewrite` wfl
695 , tv `elemVarSet` tyVarsOfType ty
696 = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,wfl,nm,ty)
697 ; mkIRStop KeepInert (singleCCan rewritten_ip) }
699 doInteractWithInert (CIPCan { cc_id = ipid, cc_flavor = ifl, cc_ip_nm = nm, cc_ip_ty = ty })
700 workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
701 | wfl `canRewrite` ifl
702 , tv `elemVarSet` tyVarsOfType ty
703 = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,ifl,nm,ty)
704 ; mkIRContinue workItem DropInert (singleCCan rewritten_ip) }
706 -- Two implicit parameter constraints. If the names are the same,
707 -- but their types are not, we generate a wanted type equality
708 -- that equates the type (this is "improvement").
709 -- However, we don't actually need the coercion evidence,
710 -- so we just generate a fresh coercion variable that isn't used anywhere.
711 doInteractWithInert (CIPCan { cc_id = id1, cc_flavor = ifl, cc_ip_nm = nm1, cc_ip_ty = ty1 })
712 workItem@(CIPCan { cc_flavor = wfl, cc_ip_nm = nm2, cc_ip_ty = ty2 })
713 | nm1 == nm2 && isGiven wfl && isGiven ifl
714 = -- See Note [Overriding implicit parameters]
715 -- Dump the inert item, override totally with the new one
716 -- Do not require type equality
717 mkIRContinue workItem DropInert emptyCCan
719 | nm1 == nm2 && ty1 `tcEqType` ty2
720 = solveOneFromTheOther (id1,ifl) workItem
723 = -- See Note [When improvement happens]
724 do { co_var <- newWantedCoVar ty1 ty2
725 ; let flav = Wanted (combineCtLoc ifl wfl)
726 ; mkCanonical flav co_var >>= mkIRContinue workItem KeepInert }
729 -- Inert: equality, work item: function equality
731 -- Never rewrite a given with a wanted equality, and a type function
732 -- equality can never rewrite an equality. Note also that if we have
733 -- F x1 ~ x2 and a ~ x3, and a occurs in x2, we don't rewrite it. We
734 -- can wait until F x1 ~ x2 matches another F x1 ~ x4, and only then
735 -- we will ``expose'' x2 and x4 to rewriting.
737 -- Otherwise, we can try rewriting the type function equality with the equality.
738 doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi1 })
739 (CFunEqCan { cc_id = cv2, cc_flavor = wfl, cc_fun = tc
740 , cc_tyargs = args, cc_rhs = xi2 })
741 | ifl `canRewrite` wfl
742 , tv `elemVarSet` tyVarsOfTypes args
743 = do { rewritten_funeq <- rewriteFunEq (cv1,tv,xi1) (cv2,wfl,tc,args,xi2)
744 ; mkIRStop KeepInert (singleCCan rewritten_funeq) }
746 -- Inert: function equality, work item: equality
748 doInteractWithInert (CFunEqCan {cc_id = cv1, cc_flavor = ifl, cc_fun = tc
749 , cc_tyargs = args, cc_rhs = xi1 })
750 workItem@(CTyEqCan { cc_id = cv2, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi2 })
751 | wfl `canRewrite` ifl
752 , tv `elemVarSet` tyVarsOfTypes args
753 = do { rewritten_funeq <- rewriteFunEq (cv2,tv,xi2) (cv1,ifl,tc,args,xi1)
754 ; mkIRContinue workItem DropInert (singleCCan rewritten_funeq) }
756 doInteractWithInert (CFunEqCan { cc_id = cv1, cc_flavor = fl1, cc_fun = tc1
757 , cc_tyargs = args1, cc_rhs = xi1 })
758 workItem@(CFunEqCan { cc_id = cv2, cc_flavor = fl2, cc_fun = tc2
759 , cc_tyargs = args2, cc_rhs = xi2 })
760 | fl1 `canRewrite` fl2 && lhss_match
761 = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
762 ; mkIRStop KeepInert cans }
763 | fl2 `canRewrite` fl1 && lhss_match
764 = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
765 ; mkIRContinue workItem DropInert cans }
767 lhss_match = tc1 == tc2 && and (zipWith tcEqType args1 args2)
769 doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
770 workItem@(CTyEqCan { cc_id = cv2, cc_flavor = fl2, cc_tyvar = tv2, cc_rhs = xi2 })
771 -- Check for matching LHS
772 | fl1 `canRewrite` fl2 && tv1 == tv2
773 = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
774 ; mkIRStop KeepInert cans }
777 | fl1 `canRewrite` fl2 -- If at all possible, keep the inert,
778 , Just tv1_rhs <- tcGetTyVar_maybe xi1 -- special case of inert a~b
780 = do { cans <- rewriteEqLHS (mkSymCoercion (mkCoVarCoercion cv1), mkTyVarTy tv1)
782 ; mkIRStop KeepInert cans }
784 | fl2 `canRewrite` fl1 && tv1 == tv2
785 = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
786 ; mkIRContinue workItem DropInert cans }
788 -- Check for rewriting RHS
789 | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfType xi2
790 = do { rewritten_eq <- rewriteEqRHS (cv1,tv1,xi1) (cv2,fl2,tv2,xi2)
791 ; mkIRStop KeepInert rewritten_eq }
792 | fl2 `canRewrite` fl1 && tv2 `elemVarSet` tyVarsOfType xi1
793 = do { rewritten_eq <- rewriteEqRHS (cv2,tv2,xi2) (cv1,fl1,tv1,xi1)
794 ; mkIRContinue workItem DropInert rewritten_eq }
797 -- Fall-through case for all other cases
798 doInteractWithInert _ workItem = noInteraction workItem
800 --------------------------------------------
801 combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
802 -- Precondition: At least one of them should be wanted
803 combineCtLoc (Wanted loc) _ = loc
804 combineCtLoc _ (Wanted loc) = loc
805 combineCtLoc _ _ = panic "Expected one of wanted constraints (BUG)"
808 -- Equational Rewriting
809 rewriteDict :: (CoVar, TcTyVar, Xi) -> (DictId, CtFlavor, Class, [Xi]) -> TcS CanonicalCt
810 rewriteDict (cv,tv,xi) (dv,gw,cl,xis)
811 = do { let cos = substTysWith [tv] [mkCoVarCoercion cv] xis -- xis[tv] ~ xis[xi]
812 args = substTysWith [tv] [xi] xis
814 dict_co = mkTyConCoercion con cos
815 ; dv' <- newDictVar cl args
817 Wanted {} -> setDictBind dv (EvCast dv' (mkSymCoercion dict_co))
818 _given_or_derived -> setDictBind dv' (EvCast dv dict_co)
819 ; return (CDictCan { cc_id = dv'
822 , cc_tyargs = args }) }
824 rewriteIP :: (CoVar,TcTyVar,Xi) -> (EvVar,CtFlavor, IPName Name, TcType) -> TcS CanonicalCt
825 rewriteIP (cv,tv,xi) (ipid,gw,nm,ty)
826 = do { let ip_co = substTyWith [tv] [mkCoVarCoercion cv] ty -- ty[tv] ~ t[xi]
827 ty' = substTyWith [tv] [xi] ty
828 ; ipid' <- newIPVar nm ty'
830 Wanted {} -> setIPBind ipid (EvCast ipid' (mkSymCoercion ip_co))
831 _given_or_derived -> setIPBind ipid' (EvCast ipid ip_co)
832 ; return (CIPCan { cc_id = ipid'
835 , cc_ip_ty = ty' }) }
837 rewriteFunEq :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TyCon, [Xi], Xi) -> TcS CanonicalCt
838 rewriteFunEq (cv1,tv,xi1) (cv2,gw, tc,args,xi2)
839 = do { let arg_cos = substTysWith [tv] [mkCoVarCoercion cv1] args
840 args' = substTysWith [tv] [xi1] args
841 fun_co = mkTyConCoercion tc arg_cos
843 Wanted {} -> do { cv2' <- newWantedCoVar (mkTyConApp tc args') xi2
844 ; setWantedCoBind cv2 $
845 mkTransCoercion fun_co (mkCoVarCoercion cv2')
847 _giv_or_der -> newGivOrDerCoVar (mkTyConApp tc args') xi2 $
848 mkTransCoercion (mkSymCoercion fun_co) (mkCoVarCoercion cv2)
849 ; return (CFunEqCan { cc_id = cv2'
856 rewriteEqRHS :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TcTyVar,Xi) -> TcS CanonicalCts
857 -- Use the first equality to rewrite the second, flavors already checked.
858 -- E.g. c1 : tv1 ~ xi1 c2 : tv2 ~ xi2
859 -- rewrites c2 to give
860 -- c2' : tv2 ~ xi2[xi1/tv1]
861 -- We must do an occurs check to sure the new constraint is canonical
862 -- So we might return an empty bag
863 rewriteEqRHS (cv1,tv1,xi1) (cv2,gw,tv2,xi2)
864 | Just tv2' <- tcGetTyVar_maybe xi2'
865 , tv2 == tv2' -- In this case xi2[xi1/tv1] = tv2, so we have tv2~tv2
866 = do { when (isWanted gw) (setWantedCoBind cv2 (mkSymCoercion co2'))
872 -> do { cv2' <- newWantedCoVar (mkTyVarTy tv2) xi2'
873 ; setWantedCoBind cv2 $
874 mkCoVarCoercion cv2' `mkTransCoercion` mkSymCoercion co2'
877 -> newGivOrDerCoVar (mkTyVarTy tv2) xi2' $
878 mkCoVarCoercion cv2 `mkTransCoercion` co2'
880 ; xi2'' <- canOccursCheck gw tv2 xi2' -- we know xi2' is *not* tv2
881 ; return (singleCCan $ CTyEqCan { cc_id = cv2'
887 xi2' = substTyWith [tv1] [xi1] xi2
888 co2' = substTyWith [tv1] [mkCoVarCoercion cv1] xi2 -- xi2 ~ xi2[xi1/tv1]
891 rewriteEqLHS :: WhichComesFromInert -> (Coercion,Xi) -> (CoVar,CtFlavor,Xi) -> TcS CanonicalCts
892 -- Used to ineratct two equalities of the following form:
893 -- First Equality: co1: (XXX ~ xi1)
894 -- Second Equality: cv2: (XXX ~ xi2)
895 -- Where the cv1 `canRewrite` cv2 equality
896 -- We have an option of creating new work (xi1 ~ xi2) OR (xi2 ~ xi1). This
897 -- depends on whether the left or the right equality comes from the inert set.
899 -- prefer to create (xi2 ~ xi1) if the first comes from the inert
900 -- prefer to create (xi1 ~ xi2) if the second comes from the inert
901 rewriteEqLHS which (co1,xi1) (cv2,gw,xi2)
902 = do { cv2' <- case (isWanted gw, which) of
903 (True,LeftComesFromInert) ->
904 do { cv2' <- newWantedCoVar xi2 xi1
905 ; setWantedCoBind cv2 $
906 co1 `mkTransCoercion` mkSymCoercion (mkCoVarCoercion cv2')
908 (True,RightComesFromInert) ->
909 do { cv2' <- newWantedCoVar xi1 xi2
910 ; setWantedCoBind cv2 $
911 co1 `mkTransCoercion` mkCoVarCoercion cv2'
913 (False,LeftComesFromInert) ->
914 newGivOrDerCoVar xi2 xi1 $
915 mkSymCoercion (mkCoVarCoercion cv2) `mkTransCoercion` co1
916 (False,RightComesFromInert) ->
917 newGivOrDerCoVar xi1 xi2 $
918 mkSymCoercion co1 `mkTransCoercion` mkCoVarCoercion cv2
919 ; mkCanonical gw cv2' }
922 -- if isWanted gw then
923 -- do { cv2' <- newWantedCoVar xi1 xi2
924 -- ; setWantedCoBind cv2 $
925 -- co1 `mkTransCoercion` mkCoVarCoercion cv2'
927 -- else newGivOrDerCoVar xi1 xi2 $
928 -- mkSymCoercion co1 `mkTransCoercion` mkCoVarCoercion cv2
929 -- ; mkCanonical gw cv2' }
932 solveOneFromTheOther :: (EvVar, CtFlavor) -> CanonicalCt -> TcS InteractResult
933 -- First argument inert, second argument workitem. They both represent
934 -- wanted/given/derived evidence for the *same* predicate so we try here to
935 -- discharge one directly from the other.
937 -- Precondition: value evidence only (implicit parameters, classes)
939 solveOneFromTheOther (iid,ifl) workItem
940 -- Both derived needs a special case. You might think that we do not need
941 -- two evidence terms for the same claim. But, since the evidence is partial,
942 -- either evidence may do in some cases; see TcSMonad.isGoodRecEv.
943 -- See also Example 3 in Note [Superclasses and recursive dictionaries]
944 | isDerived ifl && isDerived wfl
945 = noInteraction workItem
947 | ifl `canRewrite` wfl
948 = do { unless (isGiven wfl) $ setEvBind wid (EvId iid)
949 -- Overwrite the binding, if one exists
950 -- For Givens, which are lambda-bound, nothing to overwrite,
951 ; dischargeWorkItem }
953 | otherwise -- wfl `canRewrite` ifl
954 = do { unless (isGiven ifl) $ setEvBind iid (EvId wid)
955 ; mkIRContinue workItem DropInert emptyCCan }
958 wfl = cc_flavor workItem
962 Note [Superclasses and recursive dictionaries]
963 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
964 Overlaps with Note [SUPERCLASS-LOOP 1]
965 Note [SUPERCLASS-LOOP 2]
966 Note [Recursive instances and superclases]
967 ToDo: check overlap and delete redundant stuff
969 Right before adding a given into the inert set, we must
970 produce some more work, that will bring the superclasses
971 of the given into scope. The superclass constraints go into
974 When we simplify a wanted constraint, if we first see a matching
975 instance, we may produce new wanted work. To (1) avoid doing this work
976 twice in the future and (2) to handle recursive dictionaries we may ``cache''
977 this item as solved (in effect, given) into our inert set and with that add
978 its superclass constraints (as given) in our worklist.
980 But now we have added partially solved constraints to the worklist which may
981 interact with other wanteds. Consider the example:
985 class Eq b => Foo a b --- 0-th selector
986 instance Eq a => Foo [a] a --- fooDFun
988 and wanted (Foo [t] t). We are first going to see that the instance matches
989 and create an inert set that includes the solved (Foo [t] t) and its
991 d1 :_g Foo [t] t d1 := EvDFunApp fooDFun d3
992 d2 :_g Eq t d2 := EvSuperClass d1 0
993 Our work list is going to contain a new *wanted* goal
995 It is wrong to react the wanted (Eq t) with the given (Eq t) because that would
996 construct loopy evidence. Hence the check isGoodRecEv in doInteractWithInert.
998 OK, so we have ruled out bad behaviour, but how do we ge recursive dictionaries,
1003 data D r = ZeroD | SuccD (r (D r));
1005 instance (Eq (r (D r))) => Eq (D r) where
1006 ZeroD == ZeroD = True
1007 (SuccD a) == (SuccD b) = a == b
1010 equalDC :: D [] -> D [] -> Bool;
1013 We need to prove (Eq (D [])). Here's how we go:
1017 by instance decl, holds if
1021 *BUT* we have an inert set which gives us (no superclasses):
1023 By the instance declaration of Eq we can show the 'd2' goal if
1025 where d2 = dfEqList d3
1027 Now, however this wanted can interact with our inert d1 to set:
1029 and solve the goal. Why was this interaction OK? Because, if we chase the
1030 evidence of d1 ~~> dfEqD d2 ~~-> dfEqList d3, so by setting d3 := d1 we
1032 d3 := dfEqD2 (dfEqList d3)
1033 which is FINE because the use of d3 is protected by the instance function
1036 So, our strategy is to try to put solved wanted dictionaries into the
1037 inert set along with their superclasses (when this is meaningful,
1038 i.e. when new wanted goals are generated) but solve a wanted dictionary
1039 from a given only in the case where the evidence variable of the
1040 wanted is mentioned in the evidence of the given (recursively through
1041 the evidence binds) in a protected way: more instance function applications
1042 than superclass selectors.
1044 Here are some more examples from GHC's previous type checker
1048 This code arises in the context of "Scrap Your Boilerplate with Class"
1052 instance Sat (ctx Char) => Data ctx Char -- dfunData1
1053 instance (Sat (ctx [a]), Data ctx a) => Data ctx [a] -- dfunData2
1055 class Data Maybe a => Foo a
1057 instance Foo t => Sat (Maybe t) -- dfunSat
1059 instance Data Maybe a => Foo a -- dfunFoo1
1060 instance Foo a => Foo [a] -- dfunFoo2
1061 instance Foo [Char] -- dfunFoo3
1063 Consider generating the superclasses of the instance declaration
1064 instance Foo a => Foo [a]
1066 So our problem is this
1068 d1 :_w Data Maybe [t]
1070 We may add the given in the inert set, along with its superclasses
1071 [assuming we don't fail because there is a matching instance, see
1072 tryTopReact, given case ]
1076 d01 :_g Data Maybe t -- d2 := EvDictSuperClass d0 0
1077 d1 :_w Data Maybe [t]
1078 Then d2 can readily enter the inert, and we also do solving of the wanted
1081 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1083 d2 :_w Sat (Maybe [t])
1085 d01 :_g Data Maybe t
1086 Now, we may simplify d2 more:
1089 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1090 d1 :_g Data Maybe [t]
1091 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1095 d01 :_g Data Maybe t
1097 Now, we can just solve d3.
1100 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1101 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1104 d01 :_g Data Maybe t
1105 And now we can simplify d4 again, but since it has superclasses we *add* them to the worklist:
1108 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1109 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1110 d4 :_g Foo [t] d4 := dfunFoo2 d5
1113 d6 :_g Data Maybe [t] d6 := EvDictSuperClass d4 0
1114 d01 :_g Data Maybe t
1115 Now, d5 can be solved! (and its superclass enter scope)
1118 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1119 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1120 d4 :_g Foo [t] d4 := dfunFoo2 d5
1121 d5 :_g Foo t d5 := dfunFoo1 d7
1124 d6 :_g Data Maybe [t]
1125 d8 :_g Data Maybe t d8 := EvDictSuperClass d5 0
1126 d01 :_g Data Maybe t
1129 [1] Suppose we pick d8 and we react him with d01. Which of the two givens should
1130 we keep? Well, we *MUST NOT* drop d01 because d8 contains recursive evidence
1131 that must not be used (look at case interactInert where both inert and workitem
1132 are givens). So we have several options:
1133 - Drop the workitem always (this will drop d8)
1134 This feels very unsafe -- what if the work item was the "good" one
1135 that should be used later to solve another wanted?
1136 - Don't drop anyone: the inert set may contain multiple givens!
1137 [This is currently implemented]
1139 The "don't drop anyone" seems the most safe thing to do, so now we come to problem 2:
1140 [2] We have added both d6 and d01 in the inert set, and we are interacting our wanted
1141 d7. Now the [isRecDictEv] function in the ineration solver
1142 [case inert-given workitem-wanted] will prevent us from interacting d7 := d8
1143 precisely because chasing the evidence of d8 leads us to an unguarded use of d7.
1145 So, no interaction happens there. Then we meet d01 and there is no recursion
1146 problem there [isRectDictEv] gives us the OK to interact and we do solve d7 := d01!
1148 Note [SUPERCLASS-LOOP 1]
1149 ~~~~~~~~~~~~~~~~~~~~~~~~
1150 We have to be very, very careful when generating superclasses, lest we
1151 accidentally build a loop. Here's an example:
1155 class S a => C a where { opc :: a -> a }
1156 class S b => D b where { opd :: b -> b }
1158 instance C Int where
1161 instance D Int where
1164 From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int}
1165 Simplifying, we may well get:
1166 $dfCInt = :C ds1 (opd dd)
1169 Notice that we spot that we can extract ds1 from dd.
1171 Alas! Alack! We can do the same for (instance D Int):
1173 $dfDInt = :D ds2 (opc dc)
1177 And now we've defined the superclass in terms of itself.
1178 Two more nasty cases are in
1183 - Satisfy the superclass context *all by itself*
1184 (tcSimplifySuperClasses)
1185 - And do so completely; i.e. no left-over constraints
1186 to mix with the constraints arising from method declarations
1189 Note [SUPERCLASS-LOOP 2]
1190 ~~~~~~~~~~~~~~~~~~~~~~~~
1191 We need to be careful when adding "the constaint we are trying to prove".
1192 Suppose we are *given* d1:Ord a, and want to deduce (d2:C [a]) where
1194 class Ord a => C a where
1195 instance Ord [a] => C [a] where ...
1197 Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the
1198 superclasses of C [a] to avails. But we must not overwrite the binding
1199 for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
1202 Here's another variant, immortalised in tcrun020
1203 class Monad m => C1 m
1204 class C1 m => C2 m x
1205 instance C2 Maybe Bool
1206 For the instance decl we need to build (C1 Maybe), and it's no good if
1207 we run around and add (C2 Maybe Bool) and its superclasses to the avails
1208 before we search for C1 Maybe.
1210 Here's another example
1211 class Eq b => Foo a b
1212 instance Eq a => Foo [a] a
1216 we'll first deduce that it holds (via the instance decl). We must not
1217 then overwrite the Eq t constraint with a superclass selection!
1219 At first I had a gross hack, whereby I simply did not add superclass constraints
1220 in addWanted, though I did for addGiven and addIrred. This was sub-optimal,
1221 becuase it lost legitimate superclass sharing, and it still didn't do the job:
1222 I found a very obscure program (now tcrun021) in which improvement meant the
1223 simplifier got two bites a the cherry... so something seemed to be an Stop
1224 first time, but reducible next time.
1226 Now we implement the Right Solution, which is to check for loops directly
1227 when adding superclasses. It's a bit like the occurs check in unification.
1229 Note [Recursive instances and superclases]
1230 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1231 Consider this code, which arises in the context of "Scrap Your
1232 Boilerplate with Class".
1236 instance Sat (ctx Char) => Data ctx Char
1237 instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]
1239 class Data Maybe a => Foo a
1241 instance Foo t => Sat (Maybe t)
1243 instance Data Maybe a => Foo a
1244 instance Foo a => Foo [a]
1247 In the instance for Foo [a], when generating evidence for the superclasses
1248 (ie in tcSimplifySuperClasses) we need a superclass (Data Maybe [a]).
1249 Using the instance for Data, we therefore need
1250 (Sat (Maybe [a], Data Maybe a)
1251 But we are given (Foo a), and hence its superclass (Data Maybe a).
1252 So that leaves (Sat (Maybe [a])). Using the instance for Sat means
1253 we need (Foo [a]). And that is the very dictionary we are bulding
1254 an instance for! So we must put that in the "givens". So in this
1256 Given: Foo a, Foo [a]
1257 Wanted: Data Maybe [a]
1259 BUT we must *not not not* put the *superclasses* of (Foo [a]) in
1260 the givens, which is what 'addGiven' would normally do. Why? Because
1261 (Data Maybe [a]) is the superclass, so we'd "satisfy" the wanted
1262 by selecting a superclass from Foo [a], which simply makes a loop.
1264 On the other hand we *must* put the superclasses of (Foo a) in
1265 the givens, as you can see from the derivation described above.
1267 Conclusion: in the very special case of tcSimplifySuperClasses
1268 we have one 'given' (namely the "this" dictionary) whose superclasses
1269 must not be added to 'givens' by addGiven.
1271 There is a complication though. Suppose there are equalities
1272 instance (Eq a, a~b) => Num (a,b)
1273 Then we normalise the 'givens' wrt the equalities, so the original
1274 given "this" dictionary is cast to one of a different type. So it's a
1275 bit trickier than before to identify the "special" dictionary whose
1276 superclasses must not be added. See test
1277 indexed-types/should_run/EqInInstance
1279 We need a persistent property of the dictionary to record this
1280 special-ness. Current I'm using the InstLocOrigin (a bit of a hack,
1281 but cool), which is maintained by dictionary normalisation.
1282 Specifically, the InstLocOrigin is
1284 then the no-superclass thing kicks in. WATCH OUT if you fiddle
1287 Note [MATCHING-SYNONYMS]
1288 ~~~~~~~~~~~~~~~~~~~~~~~~
1289 When trying to match a dictionary (D tau) to a top-level instance, or a
1290 type family equation (F taus_1 ~ tau_2) to a top-level family instance,
1291 we do *not* need to expand type synonyms because the matcher will do that for us.
1294 Note [RHS-FAMILY-SYNONYMS]
1295 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1296 The RHS of a family instance is represented as yet another constructor which is
1297 like a type synonym for the real RHS the programmer declared. Eg:
1298 type instance F (a,a) = [a]
1300 :R32 a = [a] -- internal type synonym introduced
1301 F (a,a) ~ :R32 a -- instance
1303 When we react a family instance with a type family equation in the work list
1304 we keep the synonym-using RHS without expansion.
1307 *********************************************************************************
1309 The top-reaction Stage
1311 *********************************************************************************
1314 -- If a work item has any form of interaction with top-level we get this
1315 data TopInteractResult
1316 = NoTopInt -- No top-level interaction
1318 { tir_new_work :: WorkList -- Sub-goals or new work (could be given,
1319 -- for superclasses)
1320 , tir_new_inert :: StopOrContinue -- The input work item, ready to become *inert* now:
1321 } -- NB: in ``given'' (solved) form if the
1322 -- original was wanted or given and instance match
1323 -- was found, but may also be in wanted form if we
1324 -- only reacted with functional dependencies
1325 -- arising from top-level instances.
1327 topReactionsStage :: SimplifierStage
1328 topReactionsStage workItem inerts
1329 = do { tir <- tryTopReact workItem
1332 return $ SR { sr_inerts = inerts
1333 , sr_new_work = emptyWorkList
1334 , sr_stop = ContinueWith workItem }
1335 SomeTopInt tir_new_work tir_new_inert ->
1336 return $ SR { sr_inerts = inerts
1337 , sr_new_work = tir_new_work
1338 , sr_stop = tir_new_inert
1342 tryTopReact :: WorkItem -> TcS TopInteractResult
1343 tryTopReact workitem
1344 = do { -- A flag controls the amount of interaction allowed
1345 -- See Note [Simplifying RULE lhs constraints]
1346 ctxt <- getTcSContext
1347 ; if allowedTopReaction (simplEqsOnly ctxt) workitem
1348 then do { traceTcS "tryTopReact / calling doTopReact" (ppr workitem)
1349 ; doTopReact workitem }
1350 else return NoTopInt
1353 allowedTopReaction :: Bool -> WorkItem -> Bool
1354 allowedTopReaction eqs_only (CDictCan {}) = not eqs_only
1355 allowedTopReaction _ _ = True
1358 doTopReact :: WorkItem -> TcS TopInteractResult
1359 -- The work item does not react with the inert set,
1360 -- so try interaction with top-level instances
1361 doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Wanted loc
1362 , cc_class = cls, cc_tyargs = xis })
1363 = do { -- See Note [MATCHING-SYNONYMS]
1364 ; lkp_inst_res <- matchClassInst cls xis loc
1365 ; case lkp_inst_res of
1366 NoInstance -> do { traceTcS "doTopReact/ no class instance for" (ppr dv)
1368 GenInst wtvs ev_term -> -- Solved
1369 -- No need to do fundeps stuff here; the instance
1370 -- matches already so we won't get any more info
1371 -- from functional dependencies
1372 do { traceTcS "doTopReact/ found class instance for" (ppr dv)
1373 ; setDictBind dv ev_term
1374 ; workList <- canWanteds wtvs
1376 -- Solved in one step and no new wanted work produced.
1377 -- i.e we directly matched a top-level instance
1378 -- No point in caching this in 'inert', nor in adding superclasses
1379 then return $ SomeTopInt { tir_new_work = emptyCCan
1380 , tir_new_inert = Stop }
1382 -- Solved and new wanted work produced, you may cache the
1383 -- (tentatively solved) dictionary as Derived and its superclasses
1384 else do { let solved = makeSolved workItem
1385 ; sc_work <- newSCWorkFromFlavored dv (Derived loc) cls xis
1386 ; return $ SomeTopInt
1387 { tir_new_work = workList `unionWorkLists` sc_work
1388 , tir_new_inert = ContinueWith solved } }
1392 -- Try for a fundep reaction beween the wanted item
1393 -- and a top-level instance declaration
1395 = do { instEnvs <- getInstEnvs
1396 ; let eqn_pred_locs = improveFromInstEnv (classInstances instEnvs)
1397 (ClassP cls xis, ppr dv)
1398 ; wevvars <- mkWantedFunDepEqns loc eqn_pred_locs
1399 -- NB: fundeps generate some wanted equalities, but
1400 -- we don't use their evidence for anything
1401 ; fd_work <- canWanteds wevvars
1402 ; sc_work <- newSCWorkFromFlavored dv (Derived loc) cls xis
1403 ; return $ SomeTopInt { tir_new_work = fd_work `unionWorkLists` sc_work
1404 , tir_new_inert = ContinueWith workItem }
1405 -- NB: workItem is inert, but it isn't solved
1406 -- keep it as inert, although it's not solved because we
1407 -- have now reacted all its top-level fundep-induced equalities!
1409 -- See Note [FunDep Reactions]
1412 -- Otherwise, we have a given or derived
1413 doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = fl
1414 , cc_class = cls, cc_tyargs = xis })
1415 = do { sc_work <- newSCWorkFromFlavored dv fl cls xis
1416 ; return $ SomeTopInt sc_work (ContinueWith workItem) }
1417 -- See Note [Given constraint that matches an instance declaration]
1420 doTopReact (CFunEqCan { cc_id = cv, cc_flavor = fl
1421 , cc_fun = tc, cc_tyargs = args, cc_rhs = xi })
1422 = ASSERT (isSynFamilyTyCon tc) -- No associated data families have reached that far
1423 do { match_res <- matchFam tc args -- See Note [MATCHING-SYNONYMS]
1427 MatchInstSingle (rep_tc, rep_tys)
1428 -> do { let Just coe_tc = tyConFamilyCoercion_maybe rep_tc
1429 Just rhs_ty = tcView (mkTyConApp rep_tc rep_tys)
1430 -- Eagerly expand away the type synonym on the
1431 -- RHS of a type function, so that it never
1432 -- appears in an error message
1433 -- See Note [Type synonym families] in TyCon
1434 coe = mkTyConApp coe_tc rep_tys
1436 Wanted {} -> do { cv' <- newWantedCoVar rhs_ty xi
1437 ; setWantedCoBind cv $
1438 coe `mkTransCoercion`
1441 _ -> newGivOrDerCoVar xi rhs_ty $
1442 mkSymCoercion (mkCoVarCoercion cv) `mkTransCoercion` coe
1444 ; workList <- mkCanonical fl cv'
1445 ; return $ SomeTopInt workList Stop }
1447 -> panicTcS $ text "TcSMonad.matchFam returned multiple instances!"
1451 -- Any other work item does not react with any top-level equations
1452 doTopReact _workItem = return NoTopInt
1455 Note [FunDep and implicit parameter reactions]
1456 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1457 Currently, our story of interacting two dictionaries (or a dictionary
1458 and top-level instances) for functional dependencies, and implicit
1459 paramters, is that we simply produce new wanted equalities. So for example
1461 class D a b | a -> b where ...
1467 We generate the extra work item
1469 where 'cv' is currently unused. However, this new item reacts with d2,
1470 discharging it in favour of a new constraint d2' thus:
1472 d2 := d2' |> D Int cv
1473 Now d2' can be discharged from d1
1475 We could be more aggressive and try to *immediately* solve the dictionary
1476 using those extra equalities. With the same inert set and work item we
1477 might dischard d2 directly:
1480 d2 := d1 |> D Int cv
1482 But in general it's a bit painful to figure out the necessary coercion,
1483 so we just take the first approach.
1485 It's exactly the same with implicit parameters, except that the
1486 "aggressive" approach would be much easier to implement.
1488 Note [When improvement happens]
1489 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1490 We fire an improvement rule when
1492 * Two constraints match (modulo the fundep)
1493 e.g. C t1 t2, C t1 t3 where C a b | a->b
1494 The two match because the first arg is identical
1496 * At least one is not Given. If they are both given, we don't fire
1497 the reaction because we have no way of constructing evidence for a
1498 new equality nor does it seem right to create a new wanted goal
1499 (because the goal will most likely contain untouchables, which
1500 can't be solved anyway)!
1502 Note that we *do* fire the improvement if one is Given and one is Derived.
1503 The latter can be a superclass of a wanted goal. Example (tcfail138)
1504 class L a b | a -> b
1505 class (G a, L a b) => C a b
1507 instance C a b' => G (Maybe a)
1508 instance C a b => C (Maybe a) a
1509 instance L (Maybe a) a
1511 When solving the superclasses of the (C (Maybe a) a) instance, we get
1512 Given: C a b ... and hance by superclasses, (G a, L a b)
1514 Use the instance decl to get
1516 The (C a b') is inert, so we generate its Derived superclasses (L a b'),
1517 and now we need improvement between that derived superclass an the Given (L a b)
1519 Note [Overriding implicit parameters]
1520 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1522 f :: (?x::a) -> Bool -> a
1524 g v = let ?x::Int = 3
1525 in (f v, let ?x::Bool = True in f v)
1527 This should probably be well typed, with
1528 g :: Bool -> (Int, Bool)
1530 So the inner binding for ?x::Bool *overrides* the outer one.
1531 Hence a work-item Given overrides an inert-item Given.
1533 Note [Given constraint that matches an instance declaration]
1534 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1535 What should we do when we discover that one (or more) top-level
1536 instances match a given (or solved) class constraint? We have
1539 1. Reject the program. The reason is that there may not be a unique
1540 best strategy for the solver. Example, from the OutsideIn(X) paper:
1541 instance P x => Q [x]
1542 instance (x ~ y) => R [x] y
1544 wob :: forall a b. (Q [b], R b a) => a -> Int
1546 g :: forall a. Q [a] => [a] -> Int
1549 will generate the impliation constraint:
1550 Q [a] => (Q [beta], R beta [a])
1551 If we react (Q [beta]) with its top-level axiom, we end up with a
1552 (P beta), which we have no way of discharging. On the other hand,
1553 if we react R beta [a] with the top-level we get (beta ~ a), which
1554 is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
1555 now solvable by the given Q [a].
1557 However, this option is restrictive, for instance [Example 3] from
1558 Note [Recursive dictionaries] will fail to work.
1560 2. Ignore the problem, hoping that the situations where there exist indeed
1561 such multiple strategies are rare: Indeed the cause of the previous
1562 problem is that (R [x] y) yields the new work (x ~ y) which can be
1563 *spontaneously* solved, not using the givens.
1565 We are choosing option 2 below but we might consider having a flag as well.
1568 Note [New Wanted Superclass Work]
1569 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1570 Even in the case of wanted constraints, we add all of its superclasses as
1571 new given work. There are several reasons for this:
1572 a) to minimise error messages;
1573 eg suppose we have wanted (Eq a, Ord a)
1574 then we report only (Ord a) unsoluble
1576 b) to make the smallest number of constraints when *inferring* a type
1577 (same Eq/Ord example)
1579 c) for recursive dictionaries we *must* add the superclasses
1580 so that we can use them when solving a sub-problem
1582 d) To allow FD-like improvement for type families. Assume that
1584 class C a b | a -> b
1585 and we have to solve the implication constraint:
1587 Then, FD improvement can help us to produce a new wanted (beta ~ b)
1589 We want to have the same effect with the type family encoding of
1590 functional dependencies. Namely, consider:
1591 class (F a ~ b) => C a b
1592 Now suppose that we have:
1595 By interacting the given we will get that (F a ~ b) which is not
1596 enough by itself to make us discharge (C a beta). However, we
1597 may create a new given equality from the super-class that we promise
1598 to solve: (F a ~ beta). Now we may interact this with the rest of
1599 constraint to finally get:
1602 But 'beta' is a touchable unification variable, and hence OK to
1603 unify it with 'b', replacing the given evidence with the identity.
1605 This requires trySpontaneousSolve to solve given equalities that
1606 have a touchable in their RHS, *in addition* to solving wanted
1609 Here is another example where this is useful.
1613 class (F a ~ b) => C a b
1614 And we are given the wanteds:
1618 We surely do *not* want to quantify over (b ~ c), since if someone provides
1619 dictionaries for (C a b) and (C a c), these dictionaries can provide a proof
1620 of (b ~ c), hence no extra evidence is necessary. Here is what will happen:
1622 Step 1: We will get new *given* superclass work,
1623 provisionally to our solving of w1 and w2
1625 g1: F a ~ b, g2 : F a ~ c,
1626 w1 : C a b, w2 : C a c, w3 : b ~ c
1628 The evidence for g1 and g2 is a superclass evidence term:
1630 g1 := sc w1, g2 := sc w2
1632 Step 2: The givens will solve the wanted w3, so that
1633 w3 := sym (sc w1) ; sc w2
1635 Step 3: Now, one may naively assume that then w2 can be solve from w1
1636 after rewriting with the (now solved equality) (b ~ c).
1638 But this rewriting is ruled out by the isGoodRectDict!
1640 Conclusion, we will (correctly) end up with the unsolved goals
1643 NB: The desugarer needs be more clever to deal with equalities
1644 that participate in recursive dictionary bindings.
1647 newSCWorkFromFlavored :: EvVar -> CtFlavor -> Class -> [Xi]
1649 newSCWorkFromFlavored ev flavor cls xis
1650 | Given loc <- flavor -- The NoScSkol says "don't add superclasses"
1651 , NoScSkol <- ctLocOrigin loc -- Very important!
1652 = return emptyWorkList
1655 = do { let (tyvars, sc_theta, _, _) = classBigSig cls
1656 sc_theta1 = substTheta (zipTopTvSubst tyvars xis) sc_theta
1657 -- Add *all* its superclasses (equalities or not) as new given work
1658 -- See Note [New Wanted Superclass Work]
1659 ; sc_vars <- zipWithM inst_one sc_theta1 [0..]
1660 ; mkCanonicals flavor sc_vars }
1662 inst_one pred n = newGivOrDerEvVar pred (EvSuperClass ev n)
1664 data LookupInstResult
1666 | GenInst [WantedEvVar] EvTerm
1668 matchClassInst :: Class -> [Type] -> WantedLoc -> TcS LookupInstResult
1669 matchClassInst clas tys loc
1670 = do { let pred = mkClassPred clas tys
1671 ; mb_result <- matchClass clas tys
1673 MatchInstNo -> return NoInstance
1674 MatchInstMany -> return NoInstance -- defer any reactions of a multitude until
1675 -- we learn more about the reagent
1676 MatchInstSingle (dfun_id, mb_inst_tys) ->
1677 do { checkWellStagedDFun pred dfun_id loc
1679 -- It's possible that not all the tyvars are in
1680 -- the substitution, tenv. For example:
1681 -- instance C X a => D X where ...
1682 -- (presumably there's a functional dependency in class C)
1683 -- Hence mb_inst_tys :: Either TyVar TcType
1685 ; tys <- instDFunTypes mb_inst_tys
1686 ; let (theta, _) = tcSplitPhiTy (applyTys (idType dfun_id) tys)
1687 ; if null theta then
1688 return (GenInst [] (EvDFunApp dfun_id tys []))
1690 { ev_vars <- instDFunConstraints theta
1691 ; let wevs = [WantedEvVar w loc | w <- ev_vars]
1692 ; return $ GenInst wevs (EvDFunApp dfun_id tys ev_vars) }