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
572 ---------------------------------------------------
573 -- Interact a single WorkItem with an InertSet as far as possible, i.e. until we get a Stop
574 -- result from an individual interaction (i.e. when the WorkItem is consumed), or until we've
575 -- interacted the WorkItem with the entire InertSet.
577 -- Postcondition: the new InertSet in the resulting StageResult is subset
578 -- of the input InertSet.
580 interactWithInertsStage :: SimplifierStage
581 interactWithInertsStage workItem inert
582 = foldlInertSetM interactNext initITR inert
584 initITR = SR { sr_inerts = emptyInert
585 , sr_new_work = emptyCCan
586 , sr_stop = ContinueWith workItem }
588 interactNext :: StageResult -> AtomicInert -> TcS StageResult
589 interactNext it inert
590 | ContinueWith workItem <- sr_stop it
591 = do { ir <- interactWithInert inert workItem
592 ; let inerts = sr_inerts it
593 ; return $ SR { sr_inerts = if ir_inert_action ir == KeepInert
594 then inerts `extendInertSet` inert
596 , sr_new_work = sr_new_work it `unionWorkLists` ir_new_work ir
597 , sr_stop = ir_stop ir } }
598 | otherwise = return $ itrAddInert inert it
601 itrAddInert :: AtomicInert -> StageResult -> StageResult
602 itrAddInert inert itr = itr { sr_inerts = (sr_inerts itr) `extendInertSet` inert }
604 -- Do a single interaction of two constraints.
605 interactWithInert :: AtomicInert -> WorkItem -> TcS InteractResult
606 interactWithInert inert workitem
607 = do { ctxt <- getTcSContext
608 ; let is_allowed = allowedInteraction (simplEqsOnly ctxt) inert workitem
609 inert_ev = cc_id inert
610 work_ev = cc_id workitem
612 -- Never interact a wanted and a derived where the derived's evidence
613 -- mentions the wanted evidence in an unguarded way.
614 -- See Note [Superclasses and recursive dictionaries]
615 -- and Note [New Wanted Superclass Work]
616 -- We don't have to do this for givens, as we fully know the evidence for them.
618 case (cc_flavor inert, cc_flavor workitem) of
619 (Wanted loc, Derived _) -> isGoodRecEv work_ev (WantedEvVar inert_ev loc)
620 (Derived _, Wanted loc) -> isGoodRecEv inert_ev (WantedEvVar work_ev loc)
623 ; if is_allowed && rec_ev_ok then
624 doInteractWithInert inert workitem
626 noInteraction workitem
629 allowedInteraction :: Bool -> AtomicInert -> WorkItem -> Bool
630 -- Allowed interactions
631 allowedInteraction eqs_only (CDictCan {}) (CDictCan {}) = not eqs_only
632 allowedInteraction eqs_only (CIPCan {}) (CIPCan {}) = not eqs_only
633 allowedInteraction _ _ _ = True
635 --------------------------------------------
636 doInteractWithInert :: CanonicalCt -> CanonicalCt -> TcS InteractResult
637 -- Identical class constraints.
640 (CDictCan { cc_id = d1, cc_flavor = fl1, cc_class = cls1, cc_tyargs = tys1 })
641 workItem@(CDictCan { cc_id = d2, cc_flavor = fl2, cc_class = cls2, cc_tyargs = tys2 })
642 | cls1 == cls2 && (and $ zipWith tcEqType tys1 tys2)
643 = solveOneFromTheOther (d1,fl1) workItem
645 | cls1 == cls2 && (not (isGiven fl1 && isGiven fl2))
646 = -- See Note [When improvement happens]
647 do { let work_item_pred_loc = (ClassP cls2 tys2, ppr d2)
648 inert_pred_loc = (ClassP cls1 tys1, ppr d1)
649 loc = combineCtLoc fl1 fl2
650 eqn_pred_locs = improveFromAnother work_item_pred_loc inert_pred_loc
651 ; wevvars <- mkWantedFunDepEqns loc eqn_pred_locs
652 -- See Note [Generating extra equalities]
653 ; workList <- canWanteds wevvars
654 ; mkIRContinue workItem KeepInert workList -- Keep the inert there so we avoid
655 -- re-introducing the fundep equalities
656 -- See Note [FunDep Reactions]
659 -- Class constraint and given equality: use the equality to rewrite
660 -- the class constraint.
661 doInteractWithInert (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi })
662 (CDictCan { cc_id = dv, cc_flavor = wfl, cc_class = cl, cc_tyargs = xis })
663 | ifl `canRewrite` wfl
664 , tv `elemVarSet` tyVarsOfTypes xis
665 -- substitute for tv in xis. Note that the resulting class
666 -- constraint is still canonical, since substituting xi-types in
667 -- xi-types generates xi-types. However, it may no longer be
668 -- inert with respect to the inert set items we've already seen.
669 -- For example, consider the inert set
674 -- and the work item D a (w). D a does not interact with D Int.
675 -- Next, it does interact with a ~g Int, getting rewritten to D
676 -- Int (w). But now we must go back through the rest of the inert
677 -- set again, to find that it can now be discharged by the given D
679 = do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,wfl,cl,xis)
680 ; mkIRStop KeepInert (singleCCan rewritten_dict) }
682 doInteractWithInert (CDictCan { cc_id = dv, cc_flavor = ifl, cc_class = cl, cc_tyargs = xis })
683 workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
684 | wfl `canRewrite` ifl
685 , tv `elemVarSet` tyVarsOfTypes xis
686 = do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,ifl,cl,xis)
687 ; mkIRContinue workItem DropInert (singleCCan rewritten_dict) }
689 -- Class constraint and given equality: use the equality to rewrite
690 -- the class constraint.
691 doInteractWithInert (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi })
692 (CIPCan { cc_id = ipid, cc_flavor = wfl, cc_ip_nm = nm, cc_ip_ty = ty })
693 | ifl `canRewrite` wfl
694 , tv `elemVarSet` tyVarsOfType ty
695 = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,wfl,nm,ty)
696 ; mkIRStop KeepInert (singleCCan rewritten_ip) }
698 doInteractWithInert (CIPCan { cc_id = ipid, cc_flavor = ifl, cc_ip_nm = nm, cc_ip_ty = ty })
699 workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
700 | wfl `canRewrite` ifl
701 , tv `elemVarSet` tyVarsOfType ty
702 = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,ifl,nm,ty)
703 ; mkIRContinue workItem DropInert (singleCCan rewritten_ip) }
705 -- Two implicit parameter constraints. If the names are the same,
706 -- but their types are not, we generate a wanted type equality
707 -- that equates the type (this is "improvement").
708 -- However, we don't actually need the coercion evidence,
709 -- so we just generate a fresh coercion variable that isn't used anywhere.
710 doInteractWithInert (CIPCan { cc_id = id1, cc_flavor = ifl, cc_ip_nm = nm1, cc_ip_ty = ty1 })
711 workItem@(CIPCan { cc_flavor = wfl, cc_ip_nm = nm2, cc_ip_ty = ty2 })
712 | nm1 == nm2 && ty1 `tcEqType` ty2
713 = solveOneFromTheOther (id1,ifl) workItem
715 | nm1 == nm2 && (not (isGiven ifl && isGiven wfl))
716 = -- See Note [When improvement happens]
717 do { co_var <- newWantedCoVar ty1 ty2
718 ; let flav = Wanted (combineCtLoc ifl wfl)
719 ; mkCanonical flav co_var >>= mkIRContinue workItem KeepInert }
722 -- Inert: equality, work item: function equality
724 -- Never rewrite a given with a wanted equality, and a type function
725 -- equality can never rewrite an equality. Note also that if we have
726 -- F x1 ~ x2 and a ~ x3, and a occurs in x2, we don't rewrite it. We
727 -- can wait until F x1 ~ x2 matches another F x1 ~ x4, and only then
728 -- we will ``expose'' x2 and x4 to rewriting.
730 -- Otherwise, we can try rewriting the type function equality with the equality.
731 doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi1 })
732 (CFunEqCan { cc_id = cv2, cc_flavor = wfl, cc_fun = tc
733 , cc_tyargs = args, cc_rhs = xi2 })
734 | ifl `canRewrite` wfl
735 , tv `elemVarSet` tyVarsOfTypes args
736 = do { rewritten_funeq <- rewriteFunEq (cv1,tv,xi1) (cv2,wfl,tc,args,xi2)
737 ; mkIRStop KeepInert (singleCCan rewritten_funeq) }
739 -- Inert: function equality, work item: equality
741 doInteractWithInert (CFunEqCan {cc_id = cv1, cc_flavor = ifl, cc_fun = tc
742 , cc_tyargs = args, cc_rhs = xi1 })
743 workItem@(CTyEqCan { cc_id = cv2, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi2 })
744 | wfl `canRewrite` ifl
745 , tv `elemVarSet` tyVarsOfTypes args
746 = do { rewritten_funeq <- rewriteFunEq (cv2,tv,xi2) (cv1,ifl,tc,args,xi1)
747 ; mkIRContinue workItem DropInert (singleCCan rewritten_funeq) }
749 doInteractWithInert (CFunEqCan { cc_id = cv1, cc_flavor = fl1, cc_fun = tc1
750 , cc_tyargs = args1, cc_rhs = xi1 })
751 workItem@(CFunEqCan { cc_id = cv2, cc_flavor = fl2, cc_fun = tc2
752 , cc_tyargs = args2, cc_rhs = xi2 })
753 | fl1 `canRewrite` fl2 && lhss_match
754 = do { cans <- rewriteEqLHS (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
755 ; mkIRStop KeepInert cans }
756 | fl2 `canRewrite` fl1 && lhss_match
757 = do { cans <- rewriteEqLHS (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
758 ; mkIRContinue workItem DropInert cans }
760 lhss_match = tc1 == tc2 && and (zipWith tcEqType args1 args2)
762 doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
763 workItem@(CTyEqCan { cc_id = cv2, cc_flavor = fl2, cc_tyvar = tv2, cc_rhs = xi2 })
764 -- Check for matching LHS
765 | fl1 `canRewrite` fl2 && tv1 == tv2
766 = do { cans <- rewriteEqLHS (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
767 ; mkIRStop KeepInert cans }
770 | fl1 `canRewrite` fl2 -- If at all possible, keep the inert,
771 , Just tv1_rhs <- tcGetTyVar_maybe xi1 -- special case of inert a~b
773 = do { cans <- rewriteEqLHS (mkSymCoercion (mkCoVarCoercion cv1), mkTyVarTy tv1)
775 ; mkIRStop KeepInert cans }
777 | fl2 `canRewrite` fl1 && tv1 == tv2
778 = do { cans <- rewriteEqLHS (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
779 ; mkIRContinue workItem DropInert cans }
781 -- Check for rewriting RHS
782 | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfType xi2
783 = do { rewritten_eq <- rewriteEqRHS (cv1,tv1,xi1) (cv2,fl2,tv2,xi2)
784 ; mkIRStop KeepInert rewritten_eq }
785 | fl2 `canRewrite` fl1 && tv2 `elemVarSet` tyVarsOfType xi1
786 = do { rewritten_eq <- rewriteEqRHS (cv2,tv2,xi2) (cv1,fl1,tv1,xi1)
787 ; mkIRContinue workItem DropInert rewritten_eq }
790 -- Fall-through case for all other cases
791 doInteractWithInert _ workItem = noInteraction workItem
793 --------------------------------------------
794 combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
795 -- Precondition: At least one of them should be wanted
796 combineCtLoc (Wanted loc) _ = loc
797 combineCtLoc _ (Wanted loc) = loc
798 combineCtLoc _ _ = panic "Expected one of wanted constraints (BUG)"
801 -- Equational Rewriting
802 rewriteDict :: (CoVar, TcTyVar, Xi) -> (DictId, CtFlavor, Class, [Xi]) -> TcS CanonicalCt
803 rewriteDict (cv,tv,xi) (dv,gw,cl,xis)
804 = do { let cos = substTysWith [tv] [mkCoVarCoercion cv] xis -- xis[tv] ~ xis[xi]
805 args = substTysWith [tv] [xi] xis
807 dict_co = mkTyConCoercion con cos
808 ; dv' <- newDictVar cl args
810 Wanted {} -> setDictBind dv (EvCast dv' (mkSymCoercion dict_co))
811 _given_or_derived -> setDictBind dv' (EvCast dv dict_co)
812 ; return (CDictCan { cc_id = dv'
815 , cc_tyargs = args }) }
817 rewriteIP :: (CoVar,TcTyVar,Xi) -> (EvVar,CtFlavor, IPName Name, TcType) -> TcS CanonicalCt
818 rewriteIP (cv,tv,xi) (ipid,gw,nm,ty)
819 = do { let ip_co = substTyWith [tv] [mkCoVarCoercion cv] ty -- ty[tv] ~ t[xi]
820 ty' = substTyWith [tv] [xi] ty
821 ; ipid' <- newIPVar nm ty'
823 Wanted {} -> setIPBind ipid (EvCast ipid' (mkSymCoercion ip_co))
824 _given_or_derived -> setIPBind ipid' (EvCast ipid ip_co)
825 ; return (CIPCan { cc_id = ipid'
828 , cc_ip_ty = ty' }) }
830 rewriteFunEq :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TyCon, [Xi], Xi) -> TcS CanonicalCt
831 rewriteFunEq (cv1,tv,xi1) (cv2,gw, tc,args,xi2)
832 = do { let arg_cos = substTysWith [tv] [mkCoVarCoercion cv1] args
833 args' = substTysWith [tv] [xi1] args
834 fun_co = mkTyConCoercion tc arg_cos
836 Wanted {} -> do { cv2' <- newWantedCoVar (mkTyConApp tc args') xi2
837 ; setWantedCoBind cv2 $
838 mkTransCoercion fun_co (mkCoVarCoercion cv2')
840 _giv_or_der -> newGivOrDerCoVar (mkTyConApp tc args') xi2 $
841 mkTransCoercion (mkSymCoercion fun_co) (mkCoVarCoercion cv2)
842 ; return (CFunEqCan { cc_id = cv2'
849 rewriteEqRHS :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TcTyVar,Xi) -> TcS CanonicalCts
850 -- Use the first equality to rewrite the second, flavors already checked.
851 -- E.g. c1 : tv1 ~ xi1 c2 : tv2 ~ xi2
852 -- rewrites c2 to give
853 -- c2' : tv2 ~ xi2[xi1/tv1]
854 -- We must do an occurs check to sure the new constraint is canonical
855 -- So we might return an empty bag
856 rewriteEqRHS (cv1,tv1,xi1) (cv2,gw,tv2,xi2)
857 | Just tv2' <- tcGetTyVar_maybe xi2'
858 , tv2 == tv2' -- In this case xi2[xi1/tv1] = tv2, so we have tv2~tv2
859 = do { when (isWanted gw) (setWantedCoBind cv2 (mkSymCoercion co2'))
865 -> do { cv2' <- newWantedCoVar (mkTyVarTy tv2) xi2'
866 ; setWantedCoBind cv2 $
867 mkCoVarCoercion cv2' `mkTransCoercion` mkSymCoercion co2'
870 -> newGivOrDerCoVar (mkTyVarTy tv2) xi2' $
871 mkCoVarCoercion cv2 `mkTransCoercion` co2'
873 ; xi2'' <- canOccursCheck gw tv2 xi2' -- we know xi2' is *not* tv2
874 ; return (singleCCan $ CTyEqCan { cc_id = cv2'
880 xi2' = substTyWith [tv1] [xi1] xi2
881 co2' = substTyWith [tv1] [mkCoVarCoercion cv1] xi2 -- xi2 ~ xi2[xi1/tv1]
883 rewriteEqLHS :: (Coercion,Xi) -> (CoVar,CtFlavor,Xi) -> TcS CanonicalCts
884 -- Used to ineratct two equalities of the following form:
885 -- First Equality: co1: (XXX ~ xi1)
886 -- Second Equality: cv2: (XXX ~ xi2)
887 -- Where the cv1 `canRewrite` cv2 equality
888 rewriteEqLHS (co1,xi1) (cv2,gw,xi2)
889 = do { cv2' <- if isWanted gw then
890 do { cv2' <- newWantedCoVar xi1 xi2
891 ; setWantedCoBind cv2 $
892 co1 `mkTransCoercion` mkCoVarCoercion cv2'
894 else newGivOrDerCoVar xi1 xi2 $
895 mkSymCoercion co1 `mkTransCoercion` mkCoVarCoercion cv2
896 ; mkCanonical gw cv2' }
899 solveOneFromTheOther :: (EvVar, CtFlavor) -> CanonicalCt -> TcS InteractResult
900 -- First argument inert, second argument workitem. They both represent
901 -- wanted/given/derived evidence for the *same* predicate so we try here to
902 -- discharge one directly from the other.
904 -- Precondition: value evidence only (implicit parameters, classes)
906 solveOneFromTheOther (iid,ifl) workItem
907 -- Both derived needs a special case. You might think that we do not need
908 -- two evidence terms for the same claim. But, since the evidence is partial,
909 -- either evidence may do in some cases; see TcSMonad.isGoodRecEv.
910 -- See also Example 3 in Note [Superclasses and recursive dictionaries]
911 | isDerived ifl && isDerived wfl
912 = noInteraction workItem
914 | wfl `canRewrite` ifl
915 = do { unless (isGiven ifl) $ setEvBind iid (EvId wid)
916 -- Overwrite the binding, if one exists
917 -- (For Givens, they are lambda-bound so nothing to overwrite,
918 -- but we still drop the overridden one and replace it in
919 -- the inert set with the new one
920 ; mkIRContinue workItem DropInert emptyCCan }
921 -- The order is important here: must do (wfl `canRewrite` ifl) first
922 -- so that we override the inert item with an inner given if possible.
923 -- See Note [Overriding implicit parameters]
925 | otherwise -- ifl `canRewrite` wfl
926 = do { unless (isGiven wfl) $ setEvBind wid (EvId iid)
927 ; dischargeWorkItem }
929 wfl = cc_flavor workItem
933 Note [Superclasses and recursive dictionaries]
934 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
935 Overlaps with Note [SUPERCLASS-LOOP 1]
936 Note [SUPERCLASS-LOOP 2]
937 Note [Recursive instances and superclases]
938 ToDo: check overlap and delete redundant stuff
940 Right before adding a given into the inert set, we must
941 produce some more work, that will bring the superclasses
942 of the given into scope. The superclass constraints go into
945 When we simplify a wanted constraint, if we first see a matching
946 instance, we may produce new wanted work. To (1) avoid doing this work
947 twice in the future and (2) to handle recursive dictionaries we may ``cache''
948 this item as solved (in effect, given) into our inert set and with that add
949 its superclass constraints (as given) in our worklist.
951 But now we have added partially solved constraints to the worklist which may
952 interact with other wanteds. Consider the example:
956 class Eq b => Foo a b --- 0-th selector
957 instance Eq a => Foo [a] a --- fooDFun
959 and wanted (Foo [t] t). We are first going to see that the instance matches
960 and create an inert set that includes the solved (Foo [t] t) and its
962 d1 :_g Foo [t] t d1 := EvDFunApp fooDFun d3
963 d2 :_g Eq t d2 := EvSuperClass d1 0
964 Our work list is going to contain a new *wanted* goal
966 It is wrong to react the wanted (Eq t) with the given (Eq t) because that would
967 construct loopy evidence. Hence the check isGoodRecEv in doInteractWithInert.
969 OK, so we have ruled out bad behaviour, but how do we ge recursive dictionaries,
974 data D r = ZeroD | SuccD (r (D r));
976 instance (Eq (r (D r))) => Eq (D r) where
977 ZeroD == ZeroD = True
978 (SuccD a) == (SuccD b) = a == b
981 equalDC :: D [] -> D [] -> Bool;
984 We need to prove (Eq (D [])). Here's how we go:
988 by instance decl, holds if
992 *BUT* we have an inert set which gives us (no superclasses):
994 By the instance declaration of Eq we can show the 'd2' goal if
996 where d2 = dfEqList d3
998 Now, however this wanted can interact with our inert d1 to set:
1000 and solve the goal. Why was this interaction OK? Because, if we chase the
1001 evidence of d1 ~~> dfEqD d2 ~~-> dfEqList d3, so by setting d3 := d1 we
1003 d3 := dfEqD2 (dfEqList d3)
1004 which is FINE because the use of d3 is protected by the instance function
1007 So, our strategy is to try to put solved wanted dictionaries into the
1008 inert set along with their superclasses (when this is meaningful,
1009 i.e. when new wanted goals are generated) but solve a wanted dictionary
1010 from a given only in the case where the evidence variable of the
1011 wanted is mentioned in the evidence of the given (recursively through
1012 the evidence binds) in a protected way: more instance function applications
1013 than superclass selectors.
1015 Here are some more examples from GHC's previous type checker
1019 This code arises in the context of "Scrap Your Boilerplate with Class"
1023 instance Sat (ctx Char) => Data ctx Char -- dfunData1
1024 instance (Sat (ctx [a]), Data ctx a) => Data ctx [a] -- dfunData2
1026 class Data Maybe a => Foo a
1028 instance Foo t => Sat (Maybe t) -- dfunSat
1030 instance Data Maybe a => Foo a -- dfunFoo1
1031 instance Foo a => Foo [a] -- dfunFoo2
1032 instance Foo [Char] -- dfunFoo3
1034 Consider generating the superclasses of the instance declaration
1035 instance Foo a => Foo [a]
1037 So our problem is this
1039 d1 :_w Data Maybe [t]
1041 We may add the given in the inert set, along with its superclasses
1042 [assuming we don't fail because there is a matching instance, see
1043 tryTopReact, given case ]
1047 d01 :_g Data Maybe t -- d2 := EvDictSuperClass d0 0
1048 d1 :_w Data Maybe [t]
1049 Then d2 can readily enter the inert, and we also do solving of the wanted
1052 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1054 d2 :_w Sat (Maybe [t])
1056 d01 :_g Data Maybe t
1057 Now, we may simplify d2 more:
1060 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1061 d1 :_g Data Maybe [t]
1062 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1066 d01 :_g Data Maybe t
1068 Now, we can just solve d3.
1071 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1072 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1075 d01 :_g Data Maybe t
1076 And now we can simplify d4 again, but since it has superclasses we *add* them to the worklist:
1079 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1080 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1081 d4 :_g Foo [t] d4 := dfunFoo2 d5
1084 d6 :_g Data Maybe [t] d6 := EvDictSuperClass d4 0
1085 d01 :_g Data Maybe t
1086 Now, d5 can be solved! (and its superclass enter scope)
1089 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1090 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1091 d4 :_g Foo [t] d4 := dfunFoo2 d5
1092 d5 :_g Foo t d5 := dfunFoo1 d7
1095 d6 :_g Data Maybe [t]
1096 d8 :_g Data Maybe t d8 := EvDictSuperClass d5 0
1097 d01 :_g Data Maybe t
1100 [1] Suppose we pick d8 and we react him with d01. Which of the two givens should
1101 we keep? Well, we *MUST NOT* drop d01 because d8 contains recursive evidence
1102 that must not be used (look at case interactInert where both inert and workitem
1103 are givens). So we have several options:
1104 - Drop the workitem always (this will drop d8)
1105 This feels very unsafe -- what if the work item was the "good" one
1106 that should be used later to solve another wanted?
1107 - Don't drop anyone: the inert set may contain multiple givens!
1108 [This is currently implemented]
1110 The "don't drop anyone" seems the most safe thing to do, so now we come to problem 2:
1111 [2] We have added both d6 and d01 in the inert set, and we are interacting our wanted
1112 d7. Now the [isRecDictEv] function in the ineration solver
1113 [case inert-given workitem-wanted] will prevent us from interacting d7 := d8
1114 precisely because chasing the evidence of d8 leads us to an unguarded use of d7.
1116 So, no interaction happens there. Then we meet d01 and there is no recursion
1117 problem there [isRectDictEv] gives us the OK to interact and we do solve d7 := d01!
1119 Note [SUPERCLASS-LOOP 1]
1120 ~~~~~~~~~~~~~~~~~~~~~~~~
1121 We have to be very, very careful when generating superclasses, lest we
1122 accidentally build a loop. Here's an example:
1126 class S a => C a where { opc :: a -> a }
1127 class S b => D b where { opd :: b -> b }
1129 instance C Int where
1132 instance D Int where
1135 From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int}
1136 Simplifying, we may well get:
1137 $dfCInt = :C ds1 (opd dd)
1140 Notice that we spot that we can extract ds1 from dd.
1142 Alas! Alack! We can do the same for (instance D Int):
1144 $dfDInt = :D ds2 (opc dc)
1148 And now we've defined the superclass in terms of itself.
1149 Two more nasty cases are in
1154 - Satisfy the superclass context *all by itself*
1155 (tcSimplifySuperClasses)
1156 - And do so completely; i.e. no left-over constraints
1157 to mix with the constraints arising from method declarations
1160 Note [SUPERCLASS-LOOP 2]
1161 ~~~~~~~~~~~~~~~~~~~~~~~~
1162 We need to be careful when adding "the constaint we are trying to prove".
1163 Suppose we are *given* d1:Ord a, and want to deduce (d2:C [a]) where
1165 class Ord a => C a where
1166 instance Ord [a] => C [a] where ...
1168 Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the
1169 superclasses of C [a] to avails. But we must not overwrite the binding
1170 for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
1173 Here's another variant, immortalised in tcrun020
1174 class Monad m => C1 m
1175 class C1 m => C2 m x
1176 instance C2 Maybe Bool
1177 For the instance decl we need to build (C1 Maybe), and it's no good if
1178 we run around and add (C2 Maybe Bool) and its superclasses to the avails
1179 before we search for C1 Maybe.
1181 Here's another example
1182 class Eq b => Foo a b
1183 instance Eq a => Foo [a] a
1187 we'll first deduce that it holds (via the instance decl). We must not
1188 then overwrite the Eq t constraint with a superclass selection!
1190 At first I had a gross hack, whereby I simply did not add superclass constraints
1191 in addWanted, though I did for addGiven and addIrred. This was sub-optimal,
1192 becuase it lost legitimate superclass sharing, and it still didn't do the job:
1193 I found a very obscure program (now tcrun021) in which improvement meant the
1194 simplifier got two bites a the cherry... so something seemed to be an Stop
1195 first time, but reducible next time.
1197 Now we implement the Right Solution, which is to check for loops directly
1198 when adding superclasses. It's a bit like the occurs check in unification.
1200 Note [Recursive instances and superclases]
1201 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1202 Consider this code, which arises in the context of "Scrap Your
1203 Boilerplate with Class".
1207 instance Sat (ctx Char) => Data ctx Char
1208 instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]
1210 class Data Maybe a => Foo a
1212 instance Foo t => Sat (Maybe t)
1214 instance Data Maybe a => Foo a
1215 instance Foo a => Foo [a]
1218 In the instance for Foo [a], when generating evidence for the superclasses
1219 (ie in tcSimplifySuperClasses) we need a superclass (Data Maybe [a]).
1220 Using the instance for Data, we therefore need
1221 (Sat (Maybe [a], Data Maybe a)
1222 But we are given (Foo a), and hence its superclass (Data Maybe a).
1223 So that leaves (Sat (Maybe [a])). Using the instance for Sat means
1224 we need (Foo [a]). And that is the very dictionary we are bulding
1225 an instance for! So we must put that in the "givens". So in this
1227 Given: Foo a, Foo [a]
1228 Wanted: Data Maybe [a]
1230 BUT we must *not not not* put the *superclasses* of (Foo [a]) in
1231 the givens, which is what 'addGiven' would normally do. Why? Because
1232 (Data Maybe [a]) is the superclass, so we'd "satisfy" the wanted
1233 by selecting a superclass from Foo [a], which simply makes a loop.
1235 On the other hand we *must* put the superclasses of (Foo a) in
1236 the givens, as you can see from the derivation described above.
1238 Conclusion: in the very special case of tcSimplifySuperClasses
1239 we have one 'given' (namely the "this" dictionary) whose superclasses
1240 must not be added to 'givens' by addGiven.
1242 There is a complication though. Suppose there are equalities
1243 instance (Eq a, a~b) => Num (a,b)
1244 Then we normalise the 'givens' wrt the equalities, so the original
1245 given "this" dictionary is cast to one of a different type. So it's a
1246 bit trickier than before to identify the "special" dictionary whose
1247 superclasses must not be added. See test
1248 indexed-types/should_run/EqInInstance
1250 We need a persistent property of the dictionary to record this
1251 special-ness. Current I'm using the InstLocOrigin (a bit of a hack,
1252 but cool), which is maintained by dictionary normalisation.
1253 Specifically, the InstLocOrigin is
1255 then the no-superclass thing kicks in. WATCH OUT if you fiddle
1258 Note [MATCHING-SYNONYMS]
1259 ~~~~~~~~~~~~~~~~~~~~~~~~
1260 When trying to match a dictionary (D tau) to a top-level instance, or a
1261 type family equation (F taus_1 ~ tau_2) to a top-level family instance,
1262 we do *not* need to expand type synonyms because the matcher will do that for us.
1265 Note [RHS-FAMILY-SYNONYMS]
1266 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1267 The RHS of a family instance is represented as yet another constructor which is
1268 like a type synonym for the real RHS the programmer declared. Eg:
1269 type instance F (a,a) = [a]
1271 :R32 a = [a] -- internal type synonym introduced
1272 F (a,a) ~ :R32 a -- instance
1274 When we react a family instance with a type family equation in the work list
1275 we keep the synonym-using RHS without expansion.
1278 *********************************************************************************
1280 The top-reaction Stage
1282 *********************************************************************************
1285 -- If a work item has any form of interaction with top-level we get this
1286 data TopInteractResult
1287 = NoTopInt -- No top-level interaction
1289 { tir_new_work :: WorkList -- Sub-goals or new work (could be given,
1290 -- for superclasses)
1291 , tir_new_inert :: StopOrContinue -- The input work item, ready to become *inert* now:
1292 } -- NB: in ``given'' (solved) form if the
1293 -- original was wanted or given and instance match
1294 -- was found, but may also be in wanted form if we
1295 -- only reacted with functional dependencies
1296 -- arising from top-level instances.
1298 topReactionsStage :: SimplifierStage
1299 topReactionsStage workItem inerts
1300 = do { tir <- tryTopReact workItem
1303 return $ SR { sr_inerts = inerts
1304 , sr_new_work = emptyWorkList
1305 , sr_stop = ContinueWith workItem }
1306 SomeTopInt tir_new_work tir_new_inert ->
1307 return $ SR { sr_inerts = inerts
1308 , sr_new_work = tir_new_work
1309 , sr_stop = tir_new_inert
1313 tryTopReact :: WorkItem -> TcS TopInteractResult
1314 tryTopReact workitem
1315 = do { -- A flag controls the amount of interaction allowed
1316 -- See Note [Simplifying RULE lhs constraints]
1317 ctxt <- getTcSContext
1318 ; if allowedTopReaction (simplEqsOnly ctxt) workitem
1319 then do { traceTcS "tryTopReact / calling doTopReact" (ppr workitem)
1320 ; doTopReact workitem }
1321 else return NoTopInt
1324 allowedTopReaction :: Bool -> WorkItem -> Bool
1325 allowedTopReaction eqs_only (CDictCan {}) = not eqs_only
1326 allowedTopReaction _ _ = True
1329 doTopReact :: WorkItem -> TcS TopInteractResult
1330 -- The work item does not react with the inert set,
1331 -- so try interaction with top-level instances
1332 doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Wanted loc
1333 , cc_class = cls, cc_tyargs = xis })
1334 = do { -- See Note [MATCHING-SYNONYMS]
1335 ; lkp_inst_res <- matchClassInst cls xis loc
1336 ; case lkp_inst_res of
1337 NoInstance -> do { traceTcS "doTopReact/ no class instance for" (ppr dv)
1339 GenInst wtvs ev_term -> -- Solved
1340 -- No need to do fundeps stuff here; the instance
1341 -- matches already so we won't get any more info
1342 -- from functional dependencies
1343 do { traceTcS "doTopReact/ found class instance for" (ppr dv)
1344 ; setDictBind dv ev_term
1345 ; workList <- canWanteds wtvs
1347 -- Solved in one step and no new wanted work produced.
1348 -- i.e we directly matched a top-level instance
1349 -- No point in caching this in 'inert', nor in adding superclasses
1350 then return $ SomeTopInt { tir_new_work = emptyCCan
1351 , tir_new_inert = Stop }
1353 -- Solved and new wanted work produced, you may cache the
1354 -- (tentatively solved) dictionary as Derived and its superclasses
1355 else do { let solved = makeSolved workItem
1356 ; sc_work <- newSCWorkFromFlavored dv (Derived loc) cls xis
1357 ; return $ SomeTopInt
1358 { tir_new_work = workList `unionWorkLists` sc_work
1359 , tir_new_inert = ContinueWith solved } }
1363 -- Try for a fundep reaction beween the wanted item
1364 -- and a top-level instance declaration
1366 = do { instEnvs <- getInstEnvs
1367 ; let eqn_pred_locs = improveFromInstEnv (classInstances instEnvs)
1368 (ClassP cls xis, ppr dv)
1369 ; wevvars <- mkWantedFunDepEqns loc eqn_pred_locs
1370 -- NB: fundeps generate some wanted equalities, but
1371 -- we don't use their evidence for anything
1372 ; fd_work <- canWanteds wevvars
1373 ; sc_work <- newSCWorkFromFlavored dv (Derived loc) cls xis
1374 ; return $ SomeTopInt { tir_new_work = fd_work `unionWorkLists` sc_work
1375 , tir_new_inert = ContinueWith workItem }
1376 -- NB: workItem is inert, but it isn't solved
1377 -- keep it as inert, although it's not solved because we
1378 -- have now reacted all its top-level fundep-induced equalities!
1380 -- See Note [FunDep Reactions]
1383 -- Otherwise, we have a given or derived
1384 doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = fl
1385 , cc_class = cls, cc_tyargs = xis })
1386 = do { sc_work <- newSCWorkFromFlavored dv fl cls xis
1387 ; return $ SomeTopInt sc_work (ContinueWith workItem) }
1388 -- See Note [Given constraint that matches an instance declaration]
1391 doTopReact (CFunEqCan { cc_id = cv, cc_flavor = fl
1392 , cc_fun = tc, cc_tyargs = args, cc_rhs = xi })
1393 = ASSERT (isSynFamilyTyCon tc) -- No associated data families have reached that far
1394 do { match_res <- matchFam tc args -- See Note [MATCHING-SYNONYMS]
1398 MatchInstSingle (rep_tc, rep_tys)
1399 -> do { let Just coe_tc = tyConFamilyCoercion_maybe rep_tc
1400 Just rhs_ty = tcView (mkTyConApp rep_tc rep_tys)
1401 -- Eagerly expand away the type synonym on the
1402 -- RHS of a type function, so that it never
1403 -- appears in an error message
1404 -- See Note [Type synonym families] in TyCon
1405 coe = mkTyConApp coe_tc rep_tys
1407 Wanted {} -> do { cv' <- newWantedCoVar rhs_ty xi
1408 ; setWantedCoBind cv $
1409 coe `mkTransCoercion`
1412 _ -> newGivOrDerCoVar xi rhs_ty $
1413 mkSymCoercion (mkCoVarCoercion cv) `mkTransCoercion` coe
1415 ; workList <- mkCanonical fl cv'
1416 ; return $ SomeTopInt workList Stop }
1418 -> panicTcS $ text "TcSMonad.matchFam returned multiple instances!"
1422 -- Any other work item does not react with any top-level equations
1423 doTopReact _workItem = return NoTopInt
1426 Note [FunDep and implicit parameter reactions]
1427 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1428 Currently, our story of interacting two dictionaries (or a dictionary
1429 and top-level instances) for functional dependencies, and implicit
1430 paramters, is that we simply produce new wanted equalities. So for example
1432 class D a b | a -> b where ...
1438 We generate the extra work item
1440 where 'cv' is currently unused. However, this new item reacts with d2,
1441 discharging it in favour of a new constraint d2' thus:
1443 d2 := d2' |> D Int cv
1444 Now d2' can be discharged from d1
1446 We could be more aggressive and try to *immediately* solve the dictionary
1447 using those extra equalities. With the same inert set and work item we
1448 might dischard d2 directly:
1451 d2 := d1 |> D Int cv
1453 But in general it's a bit painful to figure out the necessary coercion,
1454 so we just take the first approach.
1456 It's exactly the same with implicit parameters, except that the
1457 "aggressive" approach would be much easier to implement.
1459 Note [When improvement happens]
1460 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1461 We fire an improvement rule when
1463 * Two constraints match (modulo the fundep)
1464 e.g. C t1 t2, C t1 t3 where C a b | a->b
1465 The two match because the first arg is identical
1467 * At least one is not Given. If they are both given, we don't fire
1468 the reaction because we have no way of constructing evidence for a
1469 new equality nor does it seem right to create a new wanted goal
1470 (because the goal will most likely contain untouchables, which
1471 can't be solved anyway)!
1473 Note that we *do* fire the improvement if one is Given and one is Derived.
1474 The latter can be a superclass of a wanted goal. Example (tcfail138)
1475 class L a b | a -> b
1476 class (G a, L a b) => C a b
1478 instance C a b' => G (Maybe a)
1479 instance C a b => C (Maybe a) a
1480 instance L (Maybe a) a
1482 When solving the superclasses of the (C (Maybe a) a) instance, we get
1483 Given: C a b ... and hance by superclasses, (G a, L a b)
1485 Use the instance decl to get
1487 The (C a b') is inert, so we generate its Derived superclasses (L a b'),
1488 and now we need improvement between that derived superclass an the Given (L a b)
1490 Note [Overriding implicit parameters]
1491 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1493 f :: (?x::a) -> Bool -> a
1495 g v = let ?x::Int = 3
1496 in (f v, let ?x::Bool = True in f v)
1498 This should probably be well typed, with
1499 g :: Bool -> (Int, Bool)
1501 So the inner binding for ?x::Bool *overrides* the outer one.
1502 Hence a work-item Given overrides an inert-item Given.
1504 Note [Given constraint that matches an instance declaration]
1505 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1506 What should we do when we discover that one (or more) top-level
1507 instances match a given (or solved) class constraint? We have
1510 1. Reject the program. The reason is that there may not be a unique
1511 best strategy for the solver. Example, from the OutsideIn(X) paper:
1512 instance P x => Q [x]
1513 instance (x ~ y) => R [x] y
1515 wob :: forall a b. (Q [b], R b a) => a -> Int
1517 g :: forall a. Q [a] => [a] -> Int
1520 will generate the impliation constraint:
1521 Q [a] => (Q [beta], R beta [a])
1522 If we react (Q [beta]) with its top-level axiom, we end up with a
1523 (P beta), which we have no way of discharging. On the other hand,
1524 if we react R beta [a] with the top-level we get (beta ~ a), which
1525 is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
1526 now solvable by the given Q [a].
1528 However, this option is restrictive, for instance [Example 3] from
1529 Note [Recursive dictionaries] will fail to work.
1531 2. Ignore the problem, hoping that the situations where there exist indeed
1532 such multiple strategies are rare: Indeed the cause of the previous
1533 problem is that (R [x] y) yields the new work (x ~ y) which can be
1534 *spontaneously* solved, not using the givens.
1536 We are choosing option 2 below but we might consider having a flag as well.
1539 Note [New Wanted Superclass Work]
1540 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1541 Even in the case of wanted constraints, we add all of its superclasses as
1542 new given work. There are several reasons for this:
1543 a) to minimise error messages;
1544 eg suppose we have wanted (Eq a, Ord a)
1545 then we report only (Ord a) unsoluble
1547 b) to make the smallest number of constraints when *inferring* a type
1548 (same Eq/Ord example)
1550 c) for recursive dictionaries we *must* add the superclasses
1551 so that we can use them when solving a sub-problem
1553 d) To allow FD-like improvement for type families. Assume that
1555 class C a b | a -> b
1556 and we have to solve the implication constraint:
1558 Then, FD improvement can help us to produce a new wanted (beta ~ b)
1560 We want to have the same effect with the type family encoding of
1561 functional dependencies. Namely, consider:
1562 class (F a ~ b) => C a b
1563 Now suppose that we have:
1566 By interacting the given we will get that (F a ~ b) which is not
1567 enough by itself to make us discharge (C a beta). However, we
1568 may create a new given equality from the super-class that we promise
1569 to solve: (F a ~ beta). Now we may interact this with the rest of
1570 constraint to finally get:
1573 But 'beta' is a touchable unification variable, and hence OK to
1574 unify it with 'b', replacing the given evidence with the identity.
1576 This requires trySpontaneousSolve to solve given equalities that
1577 have a touchable in their RHS, *in addition* to solving wanted
1580 Here is another example where this is useful.
1584 class (F a ~ b) => C a b
1585 And we are given the wanteds:
1589 We surely do *not* want to quantify over (b ~ c), since if someone provides
1590 dictionaries for (C a b) and (C a c), these dictionaries can provide a proof
1591 of (b ~ c), hence no extra evidence is necessary. Here is what will happen:
1593 Step 1: We will get new *given* superclass work,
1594 provisionally to our solving of w1 and w2
1596 g1: F a ~ b, g2 : F a ~ c,
1597 w1 : C a b, w2 : C a c, w3 : b ~ c
1599 The evidence for g1 and g2 is a superclass evidence term:
1601 g1 := sc w1, g2 := sc w2
1603 Step 2: The givens will solve the wanted w3, so that
1604 w3 := sym (sc w1) ; sc w2
1606 Step 3: Now, one may naively assume that then w2 can be solve from w1
1607 after rewriting with the (now solved equality) (b ~ c).
1609 But this rewriting is ruled out by the isGoodRectDict!
1611 Conclusion, we will (correctly) end up with the unsolved goals
1614 NB: The desugarer needs be more clever to deal with equalities
1615 that participate in recursive dictionary bindings.
1618 newSCWorkFromFlavored :: EvVar -> CtFlavor -> Class -> [Xi]
1620 newSCWorkFromFlavored ev flavor cls xis
1621 | Given loc <- flavor -- The NoScSkol says "don't add superclasses"
1622 , NoScSkol <- ctLocOrigin loc -- Very important!
1623 = return emptyWorkList
1626 = do { let (tyvars, sc_theta, _, _) = classBigSig cls
1627 sc_theta1 = substTheta (zipTopTvSubst tyvars xis) sc_theta
1628 -- Add *all* its superclasses (equalities or not) as new given work
1629 -- See Note [New Wanted Superclass Work]
1630 ; sc_vars <- zipWithM inst_one sc_theta1 [0..]
1631 ; mkCanonicals flavor sc_vars }
1633 inst_one pred n = newGivOrDerEvVar pred (EvSuperClass ev n)
1635 data LookupInstResult
1637 | GenInst [WantedEvVar] EvTerm
1639 matchClassInst :: Class -> [Type] -> WantedLoc -> TcS LookupInstResult
1640 matchClassInst clas tys loc
1641 = do { let pred = mkClassPred clas tys
1642 ; mb_result <- matchClass clas tys
1644 MatchInstNo -> return NoInstance
1645 MatchInstMany -> return NoInstance -- defer any reactions of a multitude until
1646 -- we learn more about the reagent
1647 MatchInstSingle (dfun_id, mb_inst_tys) ->
1648 do { checkWellStagedDFun pred dfun_id loc
1650 -- It's possible that not all the tyvars are in
1651 -- the substitution, tenv. For example:
1652 -- instance C X a => D X where ...
1653 -- (presumably there's a functional dependency in class C)
1654 -- Hence mb_inst_tys :: Either TyVar TcType
1656 ; tys <- instDFunTypes mb_inst_tys
1657 ; let (theta, _) = tcSplitPhiTy (applyTys (idType dfun_id) tys)
1658 ; if null theta then
1659 return (GenInst [] (EvDFunApp dfun_id tys []))
1661 { ev_vars <- instDFunConstraints theta
1662 ; let wevs = [WantedEvVar w loc | w <- ev_vars]
1663 ; return $ GenInst wevs (EvDFunApp dfun_id tys ev_vars) }