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 && isGiven wfl && isGiven ifl
713 = -- See Note [Overriding implicit parameters]
714 -- Dump the inert item, override totally with the new one
715 -- Do not require type equality
716 mkIRContinue workItem DropInert emptyCCan
718 | nm1 == nm2 && ty1 `tcEqType` ty2
719 = solveOneFromTheOther (id1,ifl) workItem
722 = -- See Note [When improvement happens]
723 do { co_var <- newWantedCoVar ty1 ty2
724 ; let flav = Wanted (combineCtLoc ifl wfl)
725 ; mkCanonical flav co_var >>= mkIRContinue workItem KeepInert }
728 -- Inert: equality, work item: function equality
730 -- Never rewrite a given with a wanted equality, and a type function
731 -- equality can never rewrite an equality. Note also that if we have
732 -- F x1 ~ x2 and a ~ x3, and a occurs in x2, we don't rewrite it. We
733 -- can wait until F x1 ~ x2 matches another F x1 ~ x4, and only then
734 -- we will ``expose'' x2 and x4 to rewriting.
736 -- Otherwise, we can try rewriting the type function equality with the equality.
737 doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi1 })
738 (CFunEqCan { cc_id = cv2, cc_flavor = wfl, cc_fun = tc
739 , cc_tyargs = args, cc_rhs = xi2 })
740 | ifl `canRewrite` wfl
741 , tv `elemVarSet` tyVarsOfTypes args
742 = do { rewritten_funeq <- rewriteFunEq (cv1,tv,xi1) (cv2,wfl,tc,args,xi2)
743 ; mkIRStop KeepInert (singleCCan rewritten_funeq) }
745 -- Inert: function equality, work item: equality
747 doInteractWithInert (CFunEqCan {cc_id = cv1, cc_flavor = ifl, cc_fun = tc
748 , cc_tyargs = args, cc_rhs = xi1 })
749 workItem@(CTyEqCan { cc_id = cv2, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi2 })
750 | wfl `canRewrite` ifl
751 , tv `elemVarSet` tyVarsOfTypes args
752 = do { rewritten_funeq <- rewriteFunEq (cv2,tv,xi2) (cv1,ifl,tc,args,xi1)
753 ; mkIRContinue workItem DropInert (singleCCan rewritten_funeq) }
755 doInteractWithInert (CFunEqCan { cc_id = cv1, cc_flavor = fl1, cc_fun = tc1
756 , cc_tyargs = args1, cc_rhs = xi1 })
757 workItem@(CFunEqCan { cc_id = cv2, cc_flavor = fl2, cc_fun = tc2
758 , cc_tyargs = args2, cc_rhs = xi2 })
759 | fl1 `canRewrite` fl2 && lhss_match
760 = do { cans <- rewriteEqLHS (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
761 ; mkIRStop KeepInert cans }
762 | fl2 `canRewrite` fl1 && lhss_match
763 = do { cans <- rewriteEqLHS (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
764 ; mkIRContinue workItem DropInert cans }
766 lhss_match = tc1 == tc2 && and (zipWith tcEqType args1 args2)
768 doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
769 workItem@(CTyEqCan { cc_id = cv2, cc_flavor = fl2, cc_tyvar = tv2, cc_rhs = xi2 })
770 -- Check for matching LHS
771 | fl1 `canRewrite` fl2 && tv1 == tv2
772 = do { cans <- rewriteEqLHS (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
773 ; mkIRStop KeepInert cans }
776 | fl1 `canRewrite` fl2 -- If at all possible, keep the inert,
777 , Just tv1_rhs <- tcGetTyVar_maybe xi1 -- special case of inert a~b
779 = do { cans <- rewriteEqLHS (mkSymCoercion (mkCoVarCoercion cv1), mkTyVarTy tv1)
781 ; mkIRStop KeepInert cans }
783 | fl2 `canRewrite` fl1 && tv1 == tv2
784 = do { cans <- rewriteEqLHS (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
785 ; mkIRContinue workItem DropInert cans }
787 -- Check for rewriting RHS
788 | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfType xi2
789 = do { rewritten_eq <- rewriteEqRHS (cv1,tv1,xi1) (cv2,fl2,tv2,xi2)
790 ; mkIRStop KeepInert rewritten_eq }
791 | fl2 `canRewrite` fl1 && tv2 `elemVarSet` tyVarsOfType xi1
792 = do { rewritten_eq <- rewriteEqRHS (cv2,tv2,xi2) (cv1,fl1,tv1,xi1)
793 ; mkIRContinue workItem DropInert rewritten_eq }
796 -- Fall-through case for all other cases
797 doInteractWithInert _ workItem = noInteraction workItem
799 --------------------------------------------
800 combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
801 -- Precondition: At least one of them should be wanted
802 combineCtLoc (Wanted loc) _ = loc
803 combineCtLoc _ (Wanted loc) = loc
804 combineCtLoc _ _ = panic "Expected one of wanted constraints (BUG)"
807 -- Equational Rewriting
808 rewriteDict :: (CoVar, TcTyVar, Xi) -> (DictId, CtFlavor, Class, [Xi]) -> TcS CanonicalCt
809 rewriteDict (cv,tv,xi) (dv,gw,cl,xis)
810 = do { let cos = substTysWith [tv] [mkCoVarCoercion cv] xis -- xis[tv] ~ xis[xi]
811 args = substTysWith [tv] [xi] xis
813 dict_co = mkTyConCoercion con cos
814 ; dv' <- newDictVar cl args
816 Wanted {} -> setDictBind dv (EvCast dv' (mkSymCoercion dict_co))
817 _given_or_derived -> setDictBind dv' (EvCast dv dict_co)
818 ; return (CDictCan { cc_id = dv'
821 , cc_tyargs = args }) }
823 rewriteIP :: (CoVar,TcTyVar,Xi) -> (EvVar,CtFlavor, IPName Name, TcType) -> TcS CanonicalCt
824 rewriteIP (cv,tv,xi) (ipid,gw,nm,ty)
825 = do { let ip_co = substTyWith [tv] [mkCoVarCoercion cv] ty -- ty[tv] ~ t[xi]
826 ty' = substTyWith [tv] [xi] ty
827 ; ipid' <- newIPVar nm ty'
829 Wanted {} -> setIPBind ipid (EvCast ipid' (mkSymCoercion ip_co))
830 _given_or_derived -> setIPBind ipid' (EvCast ipid ip_co)
831 ; return (CIPCan { cc_id = ipid'
834 , cc_ip_ty = ty' }) }
836 rewriteFunEq :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TyCon, [Xi], Xi) -> TcS CanonicalCt
837 rewriteFunEq (cv1,tv,xi1) (cv2,gw, tc,args,xi2)
838 = do { let arg_cos = substTysWith [tv] [mkCoVarCoercion cv1] args
839 args' = substTysWith [tv] [xi1] args
840 fun_co = mkTyConCoercion tc arg_cos
842 Wanted {} -> do { cv2' <- newWantedCoVar (mkTyConApp tc args') xi2
843 ; setWantedCoBind cv2 $
844 mkTransCoercion fun_co (mkCoVarCoercion cv2')
846 _giv_or_der -> newGivOrDerCoVar (mkTyConApp tc args') xi2 $
847 mkTransCoercion (mkSymCoercion fun_co) (mkCoVarCoercion cv2)
848 ; return (CFunEqCan { cc_id = cv2'
855 rewriteEqRHS :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TcTyVar,Xi) -> TcS CanonicalCts
856 -- Use the first equality to rewrite the second, flavors already checked.
857 -- E.g. c1 : tv1 ~ xi1 c2 : tv2 ~ xi2
858 -- rewrites c2 to give
859 -- c2' : tv2 ~ xi2[xi1/tv1]
860 -- We must do an occurs check to sure the new constraint is canonical
861 -- So we might return an empty bag
862 rewriteEqRHS (cv1,tv1,xi1) (cv2,gw,tv2,xi2)
863 | Just tv2' <- tcGetTyVar_maybe xi2'
864 , tv2 == tv2' -- In this case xi2[xi1/tv1] = tv2, so we have tv2~tv2
865 = do { when (isWanted gw) (setWantedCoBind cv2 (mkSymCoercion co2'))
871 -> do { cv2' <- newWantedCoVar (mkTyVarTy tv2) xi2'
872 ; setWantedCoBind cv2 $
873 mkCoVarCoercion cv2' `mkTransCoercion` mkSymCoercion co2'
876 -> newGivOrDerCoVar (mkTyVarTy tv2) xi2' $
877 mkCoVarCoercion cv2 `mkTransCoercion` co2'
879 ; xi2'' <- canOccursCheck gw tv2 xi2' -- we know xi2' is *not* tv2
880 ; return (singleCCan $ CTyEqCan { cc_id = cv2'
886 xi2' = substTyWith [tv1] [xi1] xi2
887 co2' = substTyWith [tv1] [mkCoVarCoercion cv1] xi2 -- xi2 ~ xi2[xi1/tv1]
889 rewriteEqLHS :: (Coercion,Xi) -> (CoVar,CtFlavor,Xi) -> TcS CanonicalCts
890 -- Used to ineratct two equalities of the following form:
891 -- First Equality: co1: (XXX ~ xi1)
892 -- Second Equality: cv2: (XXX ~ xi2)
893 -- Where the cv1 `canRewrite` cv2 equality
894 rewriteEqLHS (co1,xi1) (cv2,gw,xi2)
895 = do { cv2' <- if isWanted gw then
896 do { cv2' <- newWantedCoVar xi1 xi2
897 ; setWantedCoBind cv2 $
898 co1 `mkTransCoercion` mkCoVarCoercion cv2'
900 else newGivOrDerCoVar xi1 xi2 $
901 mkSymCoercion co1 `mkTransCoercion` mkCoVarCoercion cv2
902 ; mkCanonical gw cv2' }
905 solveOneFromTheOther :: (EvVar, CtFlavor) -> CanonicalCt -> TcS InteractResult
906 -- First argument inert, second argument workitem. They both represent
907 -- wanted/given/derived evidence for the *same* predicate so we try here to
908 -- discharge one directly from the other.
910 -- Precondition: value evidence only (implicit parameters, classes)
912 solveOneFromTheOther (iid,ifl) workItem
913 -- Both derived needs a special case. You might think that we do not need
914 -- two evidence terms for the same claim. But, since the evidence is partial,
915 -- either evidence may do in some cases; see TcSMonad.isGoodRecEv.
916 -- See also Example 3 in Note [Superclasses and recursive dictionaries]
917 | isDerived ifl && isDerived wfl
918 = noInteraction workItem
920 | ifl `canRewrite` wfl
921 = do { unless (isGiven wfl) $ setEvBind wid (EvId iid)
922 -- Overwrite the binding, if one exists
923 -- For Givens, which are lambda-bound, nothing to overwrite,
924 ; dischargeWorkItem }
926 | otherwise -- wfl `canRewrite` ifl
927 = do { unless (isGiven ifl) $ setEvBind iid (EvId wid)
928 ; mkIRContinue workItem DropInert emptyCCan }
931 wfl = cc_flavor workItem
935 Note [Superclasses and recursive dictionaries]
936 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
937 Overlaps with Note [SUPERCLASS-LOOP 1]
938 Note [SUPERCLASS-LOOP 2]
939 Note [Recursive instances and superclases]
940 ToDo: check overlap and delete redundant stuff
942 Right before adding a given into the inert set, we must
943 produce some more work, that will bring the superclasses
944 of the given into scope. The superclass constraints go into
947 When we simplify a wanted constraint, if we first see a matching
948 instance, we may produce new wanted work. To (1) avoid doing this work
949 twice in the future and (2) to handle recursive dictionaries we may ``cache''
950 this item as solved (in effect, given) into our inert set and with that add
951 its superclass constraints (as given) in our worklist.
953 But now we have added partially solved constraints to the worklist which may
954 interact with other wanteds. Consider the example:
958 class Eq b => Foo a b --- 0-th selector
959 instance Eq a => Foo [a] a --- fooDFun
961 and wanted (Foo [t] t). We are first going to see that the instance matches
962 and create an inert set that includes the solved (Foo [t] t) and its
964 d1 :_g Foo [t] t d1 := EvDFunApp fooDFun d3
965 d2 :_g Eq t d2 := EvSuperClass d1 0
966 Our work list is going to contain a new *wanted* goal
968 It is wrong to react the wanted (Eq t) with the given (Eq t) because that would
969 construct loopy evidence. Hence the check isGoodRecEv in doInteractWithInert.
971 OK, so we have ruled out bad behaviour, but how do we ge recursive dictionaries,
976 data D r = ZeroD | SuccD (r (D r));
978 instance (Eq (r (D r))) => Eq (D r) where
979 ZeroD == ZeroD = True
980 (SuccD a) == (SuccD b) = a == b
983 equalDC :: D [] -> D [] -> Bool;
986 We need to prove (Eq (D [])). Here's how we go:
990 by instance decl, holds if
994 *BUT* we have an inert set which gives us (no superclasses):
996 By the instance declaration of Eq we can show the 'd2' goal if
998 where d2 = dfEqList d3
1000 Now, however this wanted can interact with our inert d1 to set:
1002 and solve the goal. Why was this interaction OK? Because, if we chase the
1003 evidence of d1 ~~> dfEqD d2 ~~-> dfEqList d3, so by setting d3 := d1 we
1005 d3 := dfEqD2 (dfEqList d3)
1006 which is FINE because the use of d3 is protected by the instance function
1009 So, our strategy is to try to put solved wanted dictionaries into the
1010 inert set along with their superclasses (when this is meaningful,
1011 i.e. when new wanted goals are generated) but solve a wanted dictionary
1012 from a given only in the case where the evidence variable of the
1013 wanted is mentioned in the evidence of the given (recursively through
1014 the evidence binds) in a protected way: more instance function applications
1015 than superclass selectors.
1017 Here are some more examples from GHC's previous type checker
1021 This code arises in the context of "Scrap Your Boilerplate with Class"
1025 instance Sat (ctx Char) => Data ctx Char -- dfunData1
1026 instance (Sat (ctx [a]), Data ctx a) => Data ctx [a] -- dfunData2
1028 class Data Maybe a => Foo a
1030 instance Foo t => Sat (Maybe t) -- dfunSat
1032 instance Data Maybe a => Foo a -- dfunFoo1
1033 instance Foo a => Foo [a] -- dfunFoo2
1034 instance Foo [Char] -- dfunFoo3
1036 Consider generating the superclasses of the instance declaration
1037 instance Foo a => Foo [a]
1039 So our problem is this
1041 d1 :_w Data Maybe [t]
1043 We may add the given in the inert set, along with its superclasses
1044 [assuming we don't fail because there is a matching instance, see
1045 tryTopReact, given case ]
1049 d01 :_g Data Maybe t -- d2 := EvDictSuperClass d0 0
1050 d1 :_w Data Maybe [t]
1051 Then d2 can readily enter the inert, and we also do solving of the wanted
1054 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1056 d2 :_w Sat (Maybe [t])
1058 d01 :_g Data Maybe t
1059 Now, we may simplify d2 more:
1062 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1063 d1 :_g Data Maybe [t]
1064 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1068 d01 :_g Data Maybe t
1070 Now, we can just solve d3.
1073 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1074 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1077 d01 :_g Data Maybe t
1078 And now we can simplify d4 again, but since it has superclasses we *add* them to the worklist:
1081 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1082 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1083 d4 :_g Foo [t] d4 := dfunFoo2 d5
1086 d6 :_g Data Maybe [t] d6 := EvDictSuperClass d4 0
1087 d01 :_g Data Maybe t
1088 Now, d5 can be solved! (and its superclass enter scope)
1091 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1092 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1093 d4 :_g Foo [t] d4 := dfunFoo2 d5
1094 d5 :_g Foo t d5 := dfunFoo1 d7
1097 d6 :_g Data Maybe [t]
1098 d8 :_g Data Maybe t d8 := EvDictSuperClass d5 0
1099 d01 :_g Data Maybe t
1102 [1] Suppose we pick d8 and we react him with d01. Which of the two givens should
1103 we keep? Well, we *MUST NOT* drop d01 because d8 contains recursive evidence
1104 that must not be used (look at case interactInert where both inert and workitem
1105 are givens). So we have several options:
1106 - Drop the workitem always (this will drop d8)
1107 This feels very unsafe -- what if the work item was the "good" one
1108 that should be used later to solve another wanted?
1109 - Don't drop anyone: the inert set may contain multiple givens!
1110 [This is currently implemented]
1112 The "don't drop anyone" seems the most safe thing to do, so now we come to problem 2:
1113 [2] We have added both d6 and d01 in the inert set, and we are interacting our wanted
1114 d7. Now the [isRecDictEv] function in the ineration solver
1115 [case inert-given workitem-wanted] will prevent us from interacting d7 := d8
1116 precisely because chasing the evidence of d8 leads us to an unguarded use of d7.
1118 So, no interaction happens there. Then we meet d01 and there is no recursion
1119 problem there [isRectDictEv] gives us the OK to interact and we do solve d7 := d01!
1121 Note [SUPERCLASS-LOOP 1]
1122 ~~~~~~~~~~~~~~~~~~~~~~~~
1123 We have to be very, very careful when generating superclasses, lest we
1124 accidentally build a loop. Here's an example:
1128 class S a => C a where { opc :: a -> a }
1129 class S b => D b where { opd :: b -> b }
1131 instance C Int where
1134 instance D Int where
1137 From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int}
1138 Simplifying, we may well get:
1139 $dfCInt = :C ds1 (opd dd)
1142 Notice that we spot that we can extract ds1 from dd.
1144 Alas! Alack! We can do the same for (instance D Int):
1146 $dfDInt = :D ds2 (opc dc)
1150 And now we've defined the superclass in terms of itself.
1151 Two more nasty cases are in
1156 - Satisfy the superclass context *all by itself*
1157 (tcSimplifySuperClasses)
1158 - And do so completely; i.e. no left-over constraints
1159 to mix with the constraints arising from method declarations
1162 Note [SUPERCLASS-LOOP 2]
1163 ~~~~~~~~~~~~~~~~~~~~~~~~
1164 We need to be careful when adding "the constaint we are trying to prove".
1165 Suppose we are *given* d1:Ord a, and want to deduce (d2:C [a]) where
1167 class Ord a => C a where
1168 instance Ord [a] => C [a] where ...
1170 Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the
1171 superclasses of C [a] to avails. But we must not overwrite the binding
1172 for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
1175 Here's another variant, immortalised in tcrun020
1176 class Monad m => C1 m
1177 class C1 m => C2 m x
1178 instance C2 Maybe Bool
1179 For the instance decl we need to build (C1 Maybe), and it's no good if
1180 we run around and add (C2 Maybe Bool) and its superclasses to the avails
1181 before we search for C1 Maybe.
1183 Here's another example
1184 class Eq b => Foo a b
1185 instance Eq a => Foo [a] a
1189 we'll first deduce that it holds (via the instance decl). We must not
1190 then overwrite the Eq t constraint with a superclass selection!
1192 At first I had a gross hack, whereby I simply did not add superclass constraints
1193 in addWanted, though I did for addGiven and addIrred. This was sub-optimal,
1194 becuase it lost legitimate superclass sharing, and it still didn't do the job:
1195 I found a very obscure program (now tcrun021) in which improvement meant the
1196 simplifier got two bites a the cherry... so something seemed to be an Stop
1197 first time, but reducible next time.
1199 Now we implement the Right Solution, which is to check for loops directly
1200 when adding superclasses. It's a bit like the occurs check in unification.
1202 Note [Recursive instances and superclases]
1203 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1204 Consider this code, which arises in the context of "Scrap Your
1205 Boilerplate with Class".
1209 instance Sat (ctx Char) => Data ctx Char
1210 instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]
1212 class Data Maybe a => Foo a
1214 instance Foo t => Sat (Maybe t)
1216 instance Data Maybe a => Foo a
1217 instance Foo a => Foo [a]
1220 In the instance for Foo [a], when generating evidence for the superclasses
1221 (ie in tcSimplifySuperClasses) we need a superclass (Data Maybe [a]).
1222 Using the instance for Data, we therefore need
1223 (Sat (Maybe [a], Data Maybe a)
1224 But we are given (Foo a), and hence its superclass (Data Maybe a).
1225 So that leaves (Sat (Maybe [a])). Using the instance for Sat means
1226 we need (Foo [a]). And that is the very dictionary we are bulding
1227 an instance for! So we must put that in the "givens". So in this
1229 Given: Foo a, Foo [a]
1230 Wanted: Data Maybe [a]
1232 BUT we must *not not not* put the *superclasses* of (Foo [a]) in
1233 the givens, which is what 'addGiven' would normally do. Why? Because
1234 (Data Maybe [a]) is the superclass, so we'd "satisfy" the wanted
1235 by selecting a superclass from Foo [a], which simply makes a loop.
1237 On the other hand we *must* put the superclasses of (Foo a) in
1238 the givens, as you can see from the derivation described above.
1240 Conclusion: in the very special case of tcSimplifySuperClasses
1241 we have one 'given' (namely the "this" dictionary) whose superclasses
1242 must not be added to 'givens' by addGiven.
1244 There is a complication though. Suppose there are equalities
1245 instance (Eq a, a~b) => Num (a,b)
1246 Then we normalise the 'givens' wrt the equalities, so the original
1247 given "this" dictionary is cast to one of a different type. So it's a
1248 bit trickier than before to identify the "special" dictionary whose
1249 superclasses must not be added. See test
1250 indexed-types/should_run/EqInInstance
1252 We need a persistent property of the dictionary to record this
1253 special-ness. Current I'm using the InstLocOrigin (a bit of a hack,
1254 but cool), which is maintained by dictionary normalisation.
1255 Specifically, the InstLocOrigin is
1257 then the no-superclass thing kicks in. WATCH OUT if you fiddle
1260 Note [MATCHING-SYNONYMS]
1261 ~~~~~~~~~~~~~~~~~~~~~~~~
1262 When trying to match a dictionary (D tau) to a top-level instance, or a
1263 type family equation (F taus_1 ~ tau_2) to a top-level family instance,
1264 we do *not* need to expand type synonyms because the matcher will do that for us.
1267 Note [RHS-FAMILY-SYNONYMS]
1268 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1269 The RHS of a family instance is represented as yet another constructor which is
1270 like a type synonym for the real RHS the programmer declared. Eg:
1271 type instance F (a,a) = [a]
1273 :R32 a = [a] -- internal type synonym introduced
1274 F (a,a) ~ :R32 a -- instance
1276 When we react a family instance with a type family equation in the work list
1277 we keep the synonym-using RHS without expansion.
1280 *********************************************************************************
1282 The top-reaction Stage
1284 *********************************************************************************
1287 -- If a work item has any form of interaction with top-level we get this
1288 data TopInteractResult
1289 = NoTopInt -- No top-level interaction
1291 { tir_new_work :: WorkList -- Sub-goals or new work (could be given,
1292 -- for superclasses)
1293 , tir_new_inert :: StopOrContinue -- The input work item, ready to become *inert* now:
1294 } -- NB: in ``given'' (solved) form if the
1295 -- original was wanted or given and instance match
1296 -- was found, but may also be in wanted form if we
1297 -- only reacted with functional dependencies
1298 -- arising from top-level instances.
1300 topReactionsStage :: SimplifierStage
1301 topReactionsStage workItem inerts
1302 = do { tir <- tryTopReact workItem
1305 return $ SR { sr_inerts = inerts
1306 , sr_new_work = emptyWorkList
1307 , sr_stop = ContinueWith workItem }
1308 SomeTopInt tir_new_work tir_new_inert ->
1309 return $ SR { sr_inerts = inerts
1310 , sr_new_work = tir_new_work
1311 , sr_stop = tir_new_inert
1315 tryTopReact :: WorkItem -> TcS TopInteractResult
1316 tryTopReact workitem
1317 = do { -- A flag controls the amount of interaction allowed
1318 -- See Note [Simplifying RULE lhs constraints]
1319 ctxt <- getTcSContext
1320 ; if allowedTopReaction (simplEqsOnly ctxt) workitem
1321 then do { traceTcS "tryTopReact / calling doTopReact" (ppr workitem)
1322 ; doTopReact workitem }
1323 else return NoTopInt
1326 allowedTopReaction :: Bool -> WorkItem -> Bool
1327 allowedTopReaction eqs_only (CDictCan {}) = not eqs_only
1328 allowedTopReaction _ _ = True
1331 doTopReact :: WorkItem -> TcS TopInteractResult
1332 -- The work item does not react with the inert set,
1333 -- so try interaction with top-level instances
1334 doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Wanted loc
1335 , cc_class = cls, cc_tyargs = xis })
1336 = do { -- See Note [MATCHING-SYNONYMS]
1337 ; lkp_inst_res <- matchClassInst cls xis loc
1338 ; case lkp_inst_res of
1339 NoInstance -> do { traceTcS "doTopReact/ no class instance for" (ppr dv)
1341 GenInst wtvs ev_term -> -- Solved
1342 -- No need to do fundeps stuff here; the instance
1343 -- matches already so we won't get any more info
1344 -- from functional dependencies
1345 do { traceTcS "doTopReact/ found class instance for" (ppr dv)
1346 ; setDictBind dv ev_term
1347 ; workList <- canWanteds wtvs
1349 -- Solved in one step and no new wanted work produced.
1350 -- i.e we directly matched a top-level instance
1351 -- No point in caching this in 'inert', nor in adding superclasses
1352 then return $ SomeTopInt { tir_new_work = emptyCCan
1353 , tir_new_inert = Stop }
1355 -- Solved and new wanted work produced, you may cache the
1356 -- (tentatively solved) dictionary as Derived and its superclasses
1357 else do { let solved = makeSolved workItem
1358 ; sc_work <- newSCWorkFromFlavored dv (Derived loc) cls xis
1359 ; return $ SomeTopInt
1360 { tir_new_work = workList `unionWorkLists` sc_work
1361 , tir_new_inert = ContinueWith solved } }
1365 -- Try for a fundep reaction beween the wanted item
1366 -- and a top-level instance declaration
1368 = do { instEnvs <- getInstEnvs
1369 ; let eqn_pred_locs = improveFromInstEnv (classInstances instEnvs)
1370 (ClassP cls xis, ppr dv)
1371 ; wevvars <- mkWantedFunDepEqns loc eqn_pred_locs
1372 -- NB: fundeps generate some wanted equalities, but
1373 -- we don't use their evidence for anything
1374 ; fd_work <- canWanteds wevvars
1375 ; sc_work <- newSCWorkFromFlavored dv (Derived loc) cls xis
1376 ; return $ SomeTopInt { tir_new_work = fd_work `unionWorkLists` sc_work
1377 , tir_new_inert = ContinueWith workItem }
1378 -- NB: workItem is inert, but it isn't solved
1379 -- keep it as inert, although it's not solved because we
1380 -- have now reacted all its top-level fundep-induced equalities!
1382 -- See Note [FunDep Reactions]
1385 -- Otherwise, we have a given or derived
1386 doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = fl
1387 , cc_class = cls, cc_tyargs = xis })
1388 = do { sc_work <- newSCWorkFromFlavored dv fl cls xis
1389 ; return $ SomeTopInt sc_work (ContinueWith workItem) }
1390 -- See Note [Given constraint that matches an instance declaration]
1393 doTopReact (CFunEqCan { cc_id = cv, cc_flavor = fl
1394 , cc_fun = tc, cc_tyargs = args, cc_rhs = xi })
1395 = ASSERT (isSynFamilyTyCon tc) -- No associated data families have reached that far
1396 do { match_res <- matchFam tc args -- See Note [MATCHING-SYNONYMS]
1400 MatchInstSingle (rep_tc, rep_tys)
1401 -> do { let Just coe_tc = tyConFamilyCoercion_maybe rep_tc
1402 Just rhs_ty = tcView (mkTyConApp rep_tc rep_tys)
1403 -- Eagerly expand away the type synonym on the
1404 -- RHS of a type function, so that it never
1405 -- appears in an error message
1406 -- See Note [Type synonym families] in TyCon
1407 coe = mkTyConApp coe_tc rep_tys
1409 Wanted {} -> do { cv' <- newWantedCoVar rhs_ty xi
1410 ; setWantedCoBind cv $
1411 coe `mkTransCoercion`
1414 _ -> newGivOrDerCoVar xi rhs_ty $
1415 mkSymCoercion (mkCoVarCoercion cv) `mkTransCoercion` coe
1417 ; workList <- mkCanonical fl cv'
1418 ; return $ SomeTopInt workList Stop }
1420 -> panicTcS $ text "TcSMonad.matchFam returned multiple instances!"
1424 -- Any other work item does not react with any top-level equations
1425 doTopReact _workItem = return NoTopInt
1428 Note [FunDep and implicit parameter reactions]
1429 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1430 Currently, our story of interacting two dictionaries (or a dictionary
1431 and top-level instances) for functional dependencies, and implicit
1432 paramters, is that we simply produce new wanted equalities. So for example
1434 class D a b | a -> b where ...
1440 We generate the extra work item
1442 where 'cv' is currently unused. However, this new item reacts with d2,
1443 discharging it in favour of a new constraint d2' thus:
1445 d2 := d2' |> D Int cv
1446 Now d2' can be discharged from d1
1448 We could be more aggressive and try to *immediately* solve the dictionary
1449 using those extra equalities. With the same inert set and work item we
1450 might dischard d2 directly:
1453 d2 := d1 |> D Int cv
1455 But in general it's a bit painful to figure out the necessary coercion,
1456 so we just take the first approach.
1458 It's exactly the same with implicit parameters, except that the
1459 "aggressive" approach would be much easier to implement.
1461 Note [When improvement happens]
1462 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1463 We fire an improvement rule when
1465 * Two constraints match (modulo the fundep)
1466 e.g. C t1 t2, C t1 t3 where C a b | a->b
1467 The two match because the first arg is identical
1469 * At least one is not Given. If they are both given, we don't fire
1470 the reaction because we have no way of constructing evidence for a
1471 new equality nor does it seem right to create a new wanted goal
1472 (because the goal will most likely contain untouchables, which
1473 can't be solved anyway)!
1475 Note that we *do* fire the improvement if one is Given and one is Derived.
1476 The latter can be a superclass of a wanted goal. Example (tcfail138)
1477 class L a b | a -> b
1478 class (G a, L a b) => C a b
1480 instance C a b' => G (Maybe a)
1481 instance C a b => C (Maybe a) a
1482 instance L (Maybe a) a
1484 When solving the superclasses of the (C (Maybe a) a) instance, we get
1485 Given: C a b ... and hance by superclasses, (G a, L a b)
1487 Use the instance decl to get
1489 The (C a b') is inert, so we generate its Derived superclasses (L a b'),
1490 and now we need improvement between that derived superclass an the Given (L a b)
1492 Note [Overriding implicit parameters]
1493 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1495 f :: (?x::a) -> Bool -> a
1497 g v = let ?x::Int = 3
1498 in (f v, let ?x::Bool = True in f v)
1500 This should probably be well typed, with
1501 g :: Bool -> (Int, Bool)
1503 So the inner binding for ?x::Bool *overrides* the outer one.
1504 Hence a work-item Given overrides an inert-item Given.
1506 Note [Given constraint that matches an instance declaration]
1507 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1508 What should we do when we discover that one (or more) top-level
1509 instances match a given (or solved) class constraint? We have
1512 1. Reject the program. The reason is that there may not be a unique
1513 best strategy for the solver. Example, from the OutsideIn(X) paper:
1514 instance P x => Q [x]
1515 instance (x ~ y) => R [x] y
1517 wob :: forall a b. (Q [b], R b a) => a -> Int
1519 g :: forall a. Q [a] => [a] -> Int
1522 will generate the impliation constraint:
1523 Q [a] => (Q [beta], R beta [a])
1524 If we react (Q [beta]) with its top-level axiom, we end up with a
1525 (P beta), which we have no way of discharging. On the other hand,
1526 if we react R beta [a] with the top-level we get (beta ~ a), which
1527 is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
1528 now solvable by the given Q [a].
1530 However, this option is restrictive, for instance [Example 3] from
1531 Note [Recursive dictionaries] will fail to work.
1533 2. Ignore the problem, hoping that the situations where there exist indeed
1534 such multiple strategies are rare: Indeed the cause of the previous
1535 problem is that (R [x] y) yields the new work (x ~ y) which can be
1536 *spontaneously* solved, not using the givens.
1538 We are choosing option 2 below but we might consider having a flag as well.
1541 Note [New Wanted Superclass Work]
1542 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1543 Even in the case of wanted constraints, we add all of its superclasses as
1544 new given work. There are several reasons for this:
1545 a) to minimise error messages;
1546 eg suppose we have wanted (Eq a, Ord a)
1547 then we report only (Ord a) unsoluble
1549 b) to make the smallest number of constraints when *inferring* a type
1550 (same Eq/Ord example)
1552 c) for recursive dictionaries we *must* add the superclasses
1553 so that we can use them when solving a sub-problem
1555 d) To allow FD-like improvement for type families. Assume that
1557 class C a b | a -> b
1558 and we have to solve the implication constraint:
1560 Then, FD improvement can help us to produce a new wanted (beta ~ b)
1562 We want to have the same effect with the type family encoding of
1563 functional dependencies. Namely, consider:
1564 class (F a ~ b) => C a b
1565 Now suppose that we have:
1568 By interacting the given we will get that (F a ~ b) which is not
1569 enough by itself to make us discharge (C a beta). However, we
1570 may create a new given equality from the super-class that we promise
1571 to solve: (F a ~ beta). Now we may interact this with the rest of
1572 constraint to finally get:
1575 But 'beta' is a touchable unification variable, and hence OK to
1576 unify it with 'b', replacing the given evidence with the identity.
1578 This requires trySpontaneousSolve to solve given equalities that
1579 have a touchable in their RHS, *in addition* to solving wanted
1582 Here is another example where this is useful.
1586 class (F a ~ b) => C a b
1587 And we are given the wanteds:
1591 We surely do *not* want to quantify over (b ~ c), since if someone provides
1592 dictionaries for (C a b) and (C a c), these dictionaries can provide a proof
1593 of (b ~ c), hence no extra evidence is necessary. Here is what will happen:
1595 Step 1: We will get new *given* superclass work,
1596 provisionally to our solving of w1 and w2
1598 g1: F a ~ b, g2 : F a ~ c,
1599 w1 : C a b, w2 : C a c, w3 : b ~ c
1601 The evidence for g1 and g2 is a superclass evidence term:
1603 g1 := sc w1, g2 := sc w2
1605 Step 2: The givens will solve the wanted w3, so that
1606 w3 := sym (sc w1) ; sc w2
1608 Step 3: Now, one may naively assume that then w2 can be solve from w1
1609 after rewriting with the (now solved equality) (b ~ c).
1611 But this rewriting is ruled out by the isGoodRectDict!
1613 Conclusion, we will (correctly) end up with the unsolved goals
1616 NB: The desugarer needs be more clever to deal with equalities
1617 that participate in recursive dictionary bindings.
1620 newSCWorkFromFlavored :: EvVar -> CtFlavor -> Class -> [Xi]
1622 newSCWorkFromFlavored ev flavor cls xis
1623 | Given loc <- flavor -- The NoScSkol says "don't add superclasses"
1624 , NoScSkol <- ctLocOrigin loc -- Very important!
1625 = return emptyWorkList
1628 = do { let (tyvars, sc_theta, _, _) = classBigSig cls
1629 sc_theta1 = substTheta (zipTopTvSubst tyvars xis) sc_theta
1630 -- Add *all* its superclasses (equalities or not) as new given work
1631 -- See Note [New Wanted Superclass Work]
1632 ; sc_vars <- zipWithM inst_one sc_theta1 [0..]
1633 ; mkCanonicals flavor sc_vars }
1635 inst_one pred n = newGivOrDerEvVar pred (EvSuperClass ev n)
1637 data LookupInstResult
1639 | GenInst [WantedEvVar] EvTerm
1641 matchClassInst :: Class -> [Type] -> WantedLoc -> TcS LookupInstResult
1642 matchClassInst clas tys loc
1643 = do { let pred = mkClassPred clas tys
1644 ; mb_result <- matchClass clas tys
1646 MatchInstNo -> return NoInstance
1647 MatchInstMany -> return NoInstance -- defer any reactions of a multitude until
1648 -- we learn more about the reagent
1649 MatchInstSingle (dfun_id, mb_inst_tys) ->
1650 do { checkWellStagedDFun pred dfun_id loc
1652 -- It's possible that not all the tyvars are in
1653 -- the substitution, tenv. For example:
1654 -- instance C X a => D X where ...
1655 -- (presumably there's a functional dependency in class C)
1656 -- Hence mb_inst_tys :: Either TyVar TcType
1658 ; tys <- instDFunTypes mb_inst_tys
1659 ; let (theta, _) = tcSplitPhiTy (applyTys (idType dfun_id) tys)
1660 ; if null theta then
1661 return (GenInst [] (EvDFunApp dfun_id tys []))
1663 { ev_vars <- instDFunConstraints theta
1664 ; let wevs = [WantedEvVar w loc | w <- ev_vars]
1665 ; return $ GenInst wevs (EvDFunApp dfun_id tys ev_vars) }