3 solveInteract, AtomicInert,
4 InertSet, emptyInert, updInertSet, extractUnsolved, solveOne
7 #include "HsVersions.h"
30 import Control.Monad ( when )
39 import qualified Data.Map as Map
42 import Control.Monad( zipWithM, unless )
43 import FastString ( sLit )
47 Note [InertSet invariants]
48 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
50 An InertSet is a bag of canonical constraints, with the following invariants:
52 1 No two constraints react with each other.
54 A tricky case is when there exists a given (solved) dictionary
55 constraint and a wanted identical constraint in the inert set, but do
56 not react because reaction would create loopy dictionary evidence for
57 the wanted. See note [Recursive dictionaries]
59 2 Given equalities form an idempotent substitution [none of the
60 given LHS's occur in any of the given RHS's or reactant parts]
62 3 Wanted equalities also form an idempotent substitution
63 4 The entire set of equalities is acyclic.
65 5 Wanted dictionaries are inert with the top-level axiom set
67 6 Equalities of the form tv1 ~ tv2 always have a touchable variable
68 on the left (if possible).
69 7 No wanted constraints tv1 ~ tv2 with tv1 touchable. Such constraints
70 will be marked as solved right before being pushed into the inert set.
71 See note [Touchables and givens].
73 Note that 6 and 7 are /not/ enforced by canonicalization but rather by
74 insertion in the inert list, ie by TcInteract.
76 During the process of solving, the inert set will contain some
77 previously given constraints, some wanted constraints, and some given
78 constraints which have arisen from solving wanted constraints. For
79 now we do not distinguish between given and solved constraints.
81 Note that we must switch wanted inert items to given when going under an
82 implication constraint (when in top-level inference mode).
84 Note [InertSet FlattenSkolemEqClass]
85 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
86 The inert_fsks field of the inert set contains an "inverse map" of all the
87 flatten skolem equalities in the inert set. For instance, if inert_cts looks
94 Then, the inert_fsks fields holds the following map:
95 fsk2 |-> { fsk1, fsk3 }
97 Along with the necessary coercions to convert fsk1 and fsk3 back to fsk2
98 and fsk4 back to fsk5. Hence, the invariants of the inert_fsks field are:
100 (a) All TcTyVars in the domain and range of inert_fsks are flatten skolems
101 (b) All TcTyVars in the domain of inert_fsk occur naked as rhs in some
102 equalities of inert_cts
103 (c) For every mapping fsk1 |-> { (fsk2,co), ... } it must be:
106 The role of the inert_fsks is to make it easy to maintain the equivalence
107 class of each flatten skolem, which is much needed to correctly do spontaneous
108 solving. See Note [Loopy Spontaneous Solving]
111 -- See Note [InertSet invariants]
113 = IS { inert_eqs :: Bag.Bag CanonicalCt -- Equalities only (CTyEqCan,CFunEqCan)
114 , inert_cts :: Bag.Bag CanonicalCt -- Other constraints
115 , inert_fsks :: Map.Map TcTyVar [(TcTyVar,Coercion)] }
116 -- See Note [InertSet FlattenSkolemEqClass]
118 instance Outputable InertSet where
119 ppr is = vcat [ vcat (map ppr (Bag.bagToList $ inert_eqs is))
120 , vcat (map ppr (Bag.bagToList $ inert_cts is))
121 , vcat (map (\(v,rest) -> ppr v <+> text "|->" <+> hsep (map (ppr.fst) rest))
122 (Map.toList $ inert_fsks is)
126 emptyInert :: InertSet
127 emptyInert = IS { inert_eqs = Bag.emptyBag
128 , inert_cts = Bag.emptyBag, inert_fsks = Map.empty }
130 updInertSet :: InertSet -> AtomicInert -> InertSet
131 -- Introduces an element in the inert set for the first time
132 updInertSet (IS { inert_eqs = eqs, inert_cts = cts, inert_fsks = fsks })
133 item@(CTyEqCan { cc_id = cv
136 | Just tv2 <- tcGetTyVar_maybe xi,
137 FlatSkol {} <- tcTyVarDetails tv1,
138 FlatSkol {} <- tcTyVarDetails tv2
139 = let eqs' = eqs `Bag.snocBag` item
140 fsks' = Map.insertWith (++) tv2 [(tv1, mkCoVarCoercion cv)] fsks
141 -- See Note [InertSet FlattenSkolemEqClass]
142 in IS { inert_eqs = eqs', inert_cts = cts, inert_fsks = fsks' }
143 updInertSet (IS { inert_eqs = eqs, inert_cts = cts
144 , inert_fsks = fsks }) item
146 = let eqs' = eqs `Bag.snocBag` item
147 in IS { inert_eqs = eqs', inert_cts = cts, inert_fsks = fsks }
149 = let cts' = cts `Bag.snocBag` item
150 in IS { inert_eqs = eqs, inert_cts = cts', inert_fsks = fsks }
152 foldlInertSetM :: (Monad m) => (a -> AtomicInert -> m a) -> a -> InertSet -> m a
153 -- Prioritize over the equalities see Note [Prioritizing Equalities]
154 foldlInertSetM k z (IS { inert_eqs = eqs, inert_cts = cts })
155 = do { z' <- Bag.foldlBagM k z eqs
156 ; Bag.foldlBagM k z' cts }
158 extractUnsolved :: InertSet -> (InertSet, CanonicalCts)
159 extractUnsolved is@(IS {inert_eqs = eqs, inert_cts = cts})
160 = let is_init = is { inert_eqs = emptyCCan
161 , inert_cts = solved_cts, inert_fsks = Map.empty }
162 is_final = Bag.foldlBag updInertSet is_init solved_eqs -- Add equalities carefully
163 in (is_final, unsolved)
164 where (unsolved_cts, solved_cts) = Bag.partitionBag isWantedCt cts
165 (unsolved_eqs, solved_eqs) = Bag.partitionBag isWantedCt eqs
166 unsolved = unsolved_cts `unionBags` unsolved_eqs
169 getFskEqClass :: InertSet -> TcTyVar -> [(TcTyVar,Coercion)]
170 -- Precondition: tv is a FlatSkol. See Note [InertSet FlattenSkolemEqClass]
171 getFskEqClass (IS { inert_cts = cts, inert_fsks = fsks }) tv
172 = case lkpTyEqCanByLhs of
173 Nothing -> fromMaybe [] (Map.lookup tv fsks)
175 case tcGetTyVar_maybe (cc_rhs ceq) of
176 Just tv_rhs | FlatSkol {} <- tcTyVarDetails tv_rhs
177 -> let ceq_co = mkSymCoercion $ mkCoVarCoercion (cc_id ceq)
178 mk_co (v,c) = (v, mkTransCoercion c ceq_co)
179 in (tv_rhs, ceq_co): map mk_co (fromMaybe [] $ Map.lookup tv fsks)
181 where lkpTyEqCanByLhs = Bag.foldlBag lkp Nothing cts
182 lkp :: Maybe CanonicalCt -> CanonicalCt -> Maybe CanonicalCt
183 lkp Nothing ct@(CTyEqCan {cc_tyvar = tv'}) | tv' == tv = Just ct
184 lkp other _ct = other
187 isWantedCt :: CanonicalCt -> Bool
188 isWantedCt ct = isWanted (cc_flavor ct)
191 data Inert = IS { class_inerts :: FiniteMap Class Atomics
192 ip_inerts :: FiniteMap Class Atomics
193 tyfun_inerts :: FiniteMap TyCon Atomics
194 tyvar_inerts :: FiniteMap TyVar Atomics
197 Later should we also separate out givens and wanteds?
202 Note [Touchables and givens]
203 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
204 Touchable variables will never show up in givens which are inputs to
205 the solver. However, touchables may show up in givens generated by the flattener.
220 which can be put in the inert set. Suppose we also have a wanted
224 We cannot rewrite the given G alpha ~g b using the wanted alpha ~w
225 Int. Instead, after reacting alpha ~w Int with the whole inert set,
226 we observe that we can solve it by unifying alpha with Int, so we mark
227 it as solved and put it back in the *work list*. [We also immediately unify
228 alpha := Int, without telling anyone, see trySpontaneousSolve function, to
229 avoid doing this in the end.]
231 Later, because it is solved (given, in effect), we can use it to rewrite
232 G alpha ~g b to G Int ~g b, which gets put back in the work list. Eventually,
233 we will dispatch the remaining wanted constraints using the top-level axioms.
235 Finally, note that after reacting a wanted equality with the entire inert set
236 we may end up with something like
240 which we should flip around to generate the solved constraint alpha ~s b.
242 %*********************************************************************
244 * Main Interaction Solver *
246 **********************************************************************
250 1. Canonicalise (unary)
251 2. Pairwise interaction (binary)
252 * Take one from work list
253 * Try all pair-wise interactions with each constraint in inert
254 3. Try to solve spontaneously for equalities involving touchables
255 4. Top-level interaction (binary wrt top-level)
256 Superclass decomposition belongs in (4), see note [Superclasses]
260 type AtomicInert = CanonicalCt -- constraint pulled from InertSet
261 type WorkItem = CanonicalCt -- constraint pulled from WorkList
263 -- A mixture of Given, Wanted, and Derived constraints.
264 -- We split between equalities and the rest to process equalities first.
265 data WorkList = WL { wl_eqs :: CanonicalCts -- Equalities (CTyEqCan, CFunEqCan)
266 , wl_other :: CanonicalCts -- Other
268 type SWorkList = WorkList -- A worklist of solved
270 unionWorkLists :: WorkList -> WorkList -> WorkList
271 unionWorkLists wl1 wl2
272 = WL { wl_eqs = andCCan (wl_eqs wl1) (wl_eqs wl2)
273 , wl_other = andCCan (wl_other wl1) (wl_other wl2) }
275 foldlWorkListM :: (Monad m) => (a -> WorkItem -> m a) -> a -> WorkList -> m a
276 -- This fold prioritizes equalities
277 foldlWorkListM f r wl
278 = do { r' <- Bag.foldlBagM f r (wl_eqs wl)
279 ; Bag.foldlBagM f r' (wl_other wl) }
281 isEmptyWorkList :: WorkList -> Bool
282 isEmptyWorkList wl = isEmptyCCan (wl_eqs wl) && isEmptyCCan (wl_other wl)
284 emptyWorkList :: WorkList
285 emptyWorkList = WL { wl_eqs = emptyCCan, wl_other = emptyCCan }
287 mkEqWorkList :: CanonicalCts -> WorkList
288 -- Precondition: *ALL* equalities
289 mkEqWorkList eqs = WL { wl_eqs = eqs, wl_other = emptyCCan }
291 mkNonEqWorkList :: CanonicalCts -> WorkList
292 -- Precondition: *NO* equalities
293 mkNonEqWorkList cts = WL { wl_eqs = emptyCCan, wl_other = cts }
295 workListFromCCans :: CanonicalCts -> WorkList
296 -- Generic, no precondition
297 workListFromCCans cts = WL eqs others
298 where (eqs, others) = Bag.partitionBag isEqCCan cts
301 singleEqWL :: CanonicalCt -> WorkList
302 singleNonEqWL :: CanonicalCt -> WorkList
303 singleEqWL = mkEqWorkList . singleCCan
304 singleNonEqWL = mkNonEqWorkList . singleCCan
308 = Stop -- Work item is consumed
309 | ContinueWith WorkItem -- Not consumed
311 instance Outputable StopOrContinue where
312 ppr Stop = ptext (sLit "Stop")
313 ppr (ContinueWith w) = ptext (sLit "ContinueWith") <+> ppr w
315 -- Results after interacting a WorkItem as far as possible with an InertSet
317 = SR { sr_inerts :: InertSet
318 -- The new InertSet to use (REPLACES the old InertSet)
319 , sr_new_work :: WorkList
320 -- Any new work items generated (should be ADDED to the old WorkList)
322 -- sr_stop = Just workitem => workitem is *not* in sr_inerts and
323 -- workitem is inert wrt to sr_inerts
324 , sr_stop :: StopOrContinue
327 instance Outputable StageResult where
328 ppr (SR { sr_inerts = inerts, sr_new_work = work, sr_stop = stop })
329 = ptext (sLit "SR") <+>
330 braces (sep [ ptext (sLit "inerts =") <+> ppr inerts <> comma
331 , ptext (sLit "new work =") <+> ppr work <> comma
332 , ptext (sLit "stop =") <+> ppr stop])
334 instance Outputable WorkList where
335 ppr (WL eqcts othercts) = vcat [ppr eqcts, ppr othercts]
337 type SimplifierStage = WorkItem -> InertSet -> TcS StageResult
339 -- Combine a sequence of simplifier 'stages' to create a pipeline
340 runSolverPipeline :: [(String, SimplifierStage)]
341 -> InertSet -> WorkItem
342 -> TcS (InertSet, WorkList)
343 -- Precondition: non-empty list of stages
344 runSolverPipeline pipeline inerts workItem
345 = do { traceTcS "Start solver pipeline" $
346 vcat [ ptext (sLit "work item =") <+> ppr workItem
347 , ptext (sLit "inerts =") <+> ppr inerts]
349 ; let itr_in = SR { sr_inerts = inerts
350 , sr_new_work = emptyWorkList
351 , sr_stop = ContinueWith workItem }
352 ; itr_out <- run_pipeline pipeline itr_in
354 = case sr_stop itr_out of
355 Stop -> sr_inerts itr_out
356 ContinueWith item -> sr_inerts itr_out `updInertSet` item
357 ; return (new_inert, sr_new_work itr_out) }
359 run_pipeline :: [(String, SimplifierStage)]
360 -> StageResult -> TcS StageResult
361 run_pipeline [] itr = return itr
362 run_pipeline _ itr@(SR { sr_stop = Stop }) = return itr
364 run_pipeline ((name,stage):stages)
365 (SR { sr_new_work = accum_work
367 , sr_stop = ContinueWith work_item })
368 = do { itr <- stage work_item inerts
369 ; traceTcS ("Stage result (" ++ name ++ ")") (ppr itr)
370 ; let itr' = itr { sr_new_work = sr_new_work itr
371 `unionWorkLists` accum_work }
372 ; run_pipeline stages itr' }
376 Inert: {c ~ d, F a ~ t, b ~ Int, a ~ ty} (all given)
377 Reagent: a ~ [b] (given)
379 React with (c~d) ==> IR (ContinueWith (a~[b])) True []
380 React with (F a ~ t) ==> IR (ContinueWith (a~[b])) False [F [b] ~ t]
381 React with (b ~ Int) ==> IR (ContinueWith (a~[Int]) True []
384 Inert: {c ~w d, F a ~g t, b ~w Int, a ~w ty}
387 React with (c ~w d) ==> IR (ContinueWith (a~[b])) True []
388 React with (F a ~g t) ==> IR (ContinueWith (a~[b])) True [] (can't rewrite given with wanted!)
392 Inert: {a ~ Int, F Int ~ b} (given)
393 Reagent: F a ~ b (wanted)
395 React with (a ~ Int) ==> IR (ContinueWith (F Int ~ b)) True []
396 React with (F Int ~ b) ==> IR Stop True [] -- after substituting we re-canonicalize and get nothing
399 -- Main interaction solver: we fully solve the worklist 'in one go',
400 -- returning an extended inert set.
402 -- See Note [Touchables and givens].
403 solveInteract :: InertSet -> CanonicalCts -> TcS InertSet
404 solveInteract inert ws
405 = do { dyn_flags <- getDynFlags
406 ; let worklist = workListFromCCans ws
407 ; solveInteractWithDepth (ctxtStkDepth dyn_flags,0,[]) inert worklist
409 solveOne :: InertSet -> WorkItem -> TcS InertSet
410 solveOne inerts workItem
411 = do { dyn_flags <- getDynFlags
412 ; solveOneWithDepth (ctxtStkDepth dyn_flags,0,[]) inerts workItem
416 solveInteractWithDepth :: (Int, Int, [WorkItem])
417 -> InertSet -> WorkList -> TcS InertSet
418 solveInteractWithDepth ctxt@(max_depth,n,stack) inert ws
423 = solverDepthErrorTcS n stack
426 = do { traceTcS "solveInteractWithDepth" $
427 vcat [ text "Current depth =" <+> ppr n
428 , text "Max depth =" <+> ppr max_depth
430 ; foldlWorkListM (solveOneWithDepth ctxt) inert ws }
433 -- Fully interact the given work item with an inert set, and return a
434 -- new inert set which has assimilated the new information.
435 solveOneWithDepth :: (Int, Int, [WorkItem])
436 -> InertSet -> WorkItem -> TcS InertSet
437 solveOneWithDepth (max_depth, n, stack) inert work
438 = do { traceTcS0 (indent ++ "Solving {") (ppr work)
439 ; (new_inert, new_work) <- runSolverPipeline thePipeline inert work
441 ; traceTcS0 (indent ++ "Subgoals:") (ppr new_work)
443 -- Recursively solve the new work generated
444 -- from workItem, with a greater depth
445 ; res_inert <- solveInteractWithDepth (max_depth, n+1, work:stack)
448 ; traceTcS0 (indent ++ "Done }") (ppr work)
451 indent = replicate (2*n) ' '
453 thePipeline :: [(String,SimplifierStage)]
454 thePipeline = [ ("interact with inerts", interactWithInertsStage)
455 , ("spontaneous solve", spontaneousSolveStage)
456 , ("top-level reactions", topReactionsStage) ]
459 *********************************************************************************
461 The spontaneous-solve Stage
463 *********************************************************************************
466 spontaneousSolveStage :: SimplifierStage
467 spontaneousSolveStage workItem inerts
468 = do { mSolve <- trySpontaneousSolve workItem inerts
470 Nothing -> -- no spontaneous solution for him, keep going
471 return $ SR { sr_new_work = emptyWorkList
473 , sr_stop = ContinueWith workItem }
475 Just workList' -> -- He has been solved; workList' are all givens
476 return $ SR { sr_new_work = workList'
481 {-- This is all old code, but does not quite work now. The problem is that due to
482 Note [Loopy Spontaneous Solving] we may have unflattened a type, to be able to
483 perform a sneaky unification. This unflattening means that we may have to recanonicalize
484 a given (solved) equality, this is why the result of trySpontaneousSolve is now a list
485 of constraints (instead of an atomic solved constraint). We would have to react all of
486 them once again with the worklist but that is very tiresome. Instead we throw them back
489 | isWantedCt workItem
490 -- Original was wanted we have now made him given so
491 -- we have to ineract him with the inerts again because
492 -- of the change in his status. This may produce some work.
493 -> do { traceTcS "recursive interact with inerts {" $ vcat
494 [ text "work = " <+> ppr workItem'
495 , text "inerts = " <+> ppr inerts ]
496 ; itr_again <- interactWithInertsStage workItem' inerts
497 ; case sr_stop itr_again of
498 Stop -> pprPanic "BUG: Impossible to happen" $
499 vcat [ text "Original workitem:" <+> ppr workItem
500 , text "Spontaneously solved:" <+> ppr workItem'
501 , text "Solved was consumed, when reacting with inerts:"
502 , nest 2 (ppr inerts) ]
503 ContinueWith workItem'' -- Now *this* guy is inert wrt to inerts
504 -> do { traceTcS "end recursive interact }" $ ppr workItem''
505 ; return $ SR { sr_new_work = sr_new_work itr_again
506 , sr_inerts = sr_inerts itr_again
507 `extendInertSet` workItem''
511 -> return $ SR { sr_new_work = emptyWorkList
512 , sr_inerts = inerts `extendInertSet` workItem'
516 -- @trySpontaneousSolve wi@ solves equalities where one side is a
517 -- touchable unification variable. Returns:
518 -- * Nothing if we were not able to solve it
519 -- * Just wi' if we solved it, wi' (now a "given") should be put in the work list.
520 -- See Note [Touchables and givens]
521 -- NB: just passing the inerts through for the skolem equivalence classes
522 trySpontaneousSolve :: WorkItem -> InertSet -> TcS (Maybe SWorkList)
523 trySpontaneousSolve (CTyEqCan { cc_id = cv, cc_flavor = gw, cc_tyvar = tv1, cc_rhs = xi }) inerts
526 | Just tv2 <- tcGetTyVar_maybe xi
527 = do { tch1 <- isTouchableMetaTyVar tv1
528 ; tch2 <- isTouchableMetaTyVar tv2
529 ; case (tch1, tch2) of
530 (True, True) -> trySpontaneousEqTwoWay inerts cv gw tv1 tv2
531 (True, False) -> trySpontaneousEqOneWay inerts cv gw tv1 xi
532 (False, True) -> trySpontaneousEqOneWay inerts cv gw tv2 (mkTyVarTy tv1)
533 _ -> return Nothing }
535 = do { tch1 <- isTouchableMetaTyVar tv1
536 ; if tch1 then trySpontaneousEqOneWay inerts cv gw tv1 xi
537 else return Nothing }
540 -- trySpontaneousSolve (CFunEqCan ...) = ...
541 -- See Note [No touchables as FunEq RHS] in TcSMonad
542 trySpontaneousSolve _ _ = return Nothing
545 trySpontaneousEqOneWay :: InertSet -> CoVar -> CtFlavor -> TcTyVar -> Xi
546 -> TcS (Maybe SWorkList)
547 -- tv is a MetaTyVar, not untouchable
548 trySpontaneousEqOneWay inerts cv gw tv xi
549 | not (isSigTyVar tv) || isTyVarTy xi,
550 typeKind xi `isSubKind` tyVarKind tv
551 = solveWithIdentity inerts cv gw tv xi
556 trySpontaneousEqTwoWay :: InertSet -> CoVar -> CtFlavor -> TcTyVar -> TcTyVar
557 -> TcS (Maybe SWorkList)
558 -- Both tyvars are *touchable* MetaTyvars
559 -- By the CTyEqCan invariant, k2 `isSubKind` k1
560 trySpontaneousEqTwoWay inerts cv gw tv1 tv2
562 , nicer_to_update_tv2 = solveWithIdentity inerts cv gw tv2 (mkTyVarTy tv1)
564 = solveWithIdentity inerts cv gw tv1 (mkTyVarTy tv2)
565 | otherwise = return Nothing
569 nicer_to_update_tv2 = isSigTyVar tv1 || isSystemName (Var.varName tv2)
573 Note [Spontaneous solving and kind compatibility]
574 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
576 Note that our canonical constraints insist that only *given* equalities (tv ~ xi)
577 or (F xis ~ rhs) require the LHS and the RHS to have exactly the same kinds.
579 - We have to require this because:
580 Given equalities can be freely used to rewrite inside
581 other types or constraints.
582 - We do not have to do the same for wanteds because:
583 First, wanted equations (tv ~ xi) where tv is a touchable unification variable
584 may have kinds that do not agree (the kind of xi must be a sub kind of the kind of tv).
585 Second, any potential kind mismatch will result in the constraint not being soluble,
586 which will be reported anyway. This is the reason that @trySpontaneousOneWay@ and
587 @trySpontaneousTwoWay@ will perform a kind compatibility check, and only then will
588 they proceed to @solveWithIdentity@.
591 - Givens from higher-rank, such as:
592 type family T b :: * -> * -> *
593 type instance T Bool = (->)
595 f :: forall a. ((T a ~ (->)) => ...) -> a -> ...
597 Whereas we would be able to apply the type instance, we would not be able to
598 use the given (T Bool ~ (->)) in the body of 'flop'
600 Note [Loopy spontaneous solving]
601 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
602 Consider the original wanted:
603 wanted : Maybe (E alpha) ~ alpha
604 where E is a type family, such that E (T x) = x. After canonicalization,
605 as a result of flattening, we will get:
606 given : E alpha ~ fsk
607 wanted : alpha ~ Maybe fsk
608 where (fsk := E alpha, on the side). Now, if we spontaneously *solve*
609 (alpha := Maybe fsk) we are in trouble! Instead, we should refrain from solving
610 it and keep it as wanted. In inference mode we'll end up quantifying over
611 (alpha ~ Maybe (E alpha))
612 Hence, 'solveWithIdentity' performs a small occurs check before
613 actually solving. But this occurs check *must look through* flatten skolems.
615 However, it may be the case that the flatten skolem in hand is equal to some other
616 flatten skolem whith *does not* mention our unification variable. Here's a typical example:
621 After canonicalization:
626 After some reactions:
631 At this point, we will try to spontaneously solve (alpha ~ f2) which remains as yet unsolved.
632 We will look inside f2, which immediately mentions (F alpha), so it's not good to unify! However
633 by looking at the equivalence class of the flatten skolems, we can see that it is fine to
634 unify (alpha ~ f1) which solves our goals!
636 A similar problem happens because of other spontaneous solving. Suppose we have the
637 following wanteds, arriving in this exact order:
638 (first) w: beta ~ alpha
639 (second) w: alpha ~ fsk
640 (third) g: F beta ~ fsk
641 Then, we first spontaneously solve the first constraint, making (beta := alpha), and having
642 (beta ~ alpha) as given. *Then* we encounter the second wanted (alpha ~ fsk). "fsk" does not
643 obviously mention alpha, so naively we can also spontaneously solve (alpha := fsk). But
644 that is wrong since fsk mentions beta, which has already secretly been unified to alpha!
646 To avoid this problem, the same occurs check must unveil rewritings that can happen because
647 of spontaneously having solved other constraints.
650 Note [Avoid double unifications]
651 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
652 The spontaneous solver has to return a given which mentions the unified unification
653 variable *on the left* of the equality. Here is what happens if not:
654 Original wanted: (a ~ alpha), (alpha ~ Int)
655 We spontaneously solve the first wanted, without changing the order!
656 given : a ~ alpha [having unified alpha := a]
657 Now the second wanted comes along, but he cannot rewrite the given, so we simply continue.
658 At the end we spontaneously solve that guy, *reunifying* [alpha := Int]
660 We avoid this problem by orienting the given so that the unification
661 variable is on the left. [Note that alternatively we could attempt to
662 enforce this at canonicalization]
664 See also Note [No touchables as FunEq RHS] in TcSMonad; avoiding
665 double unifications is the main reason we disallow touchable
666 unification variables as RHS of type family equations: F xis ~ alpha.
670 solveWithIdentity :: InertSet
671 -> CoVar -> CtFlavor -> TcTyVar -> Xi
672 -> TcS (Maybe SWorkList)
673 -- Solve with the identity coercion
674 -- Precondition: kind(xi) is a sub-kind of kind(tv)
675 -- Precondition: CtFlavor is Wanted or Derived
676 -- See [New Wanted Superclass Work] to see why solveWithIdentity
677 -- must work for Derived as well as Wanted
678 solveWithIdentity inerts cv gw tv xi
679 = do { tybnds <- getTcSTyBindsMap
680 ; case occurCheck tybnds inerts tv xi of
681 Nothing -> return Nothing
682 Just (xi_unflat,coi) -> solve_with xi_unflat coi }
684 solve_with xi_unflat coi -- coi : xi_unflat ~ xi
685 = do { traceTcS "Sneaky unification:" $
686 vcat [text "Coercion variable: " <+> ppr gw,
687 text "Coercion: " <+> pprEq (mkTyVarTy tv) xi,
688 text "Left Kind is : " <+> ppr (typeKind (mkTyVarTy tv)),
689 text "Right Kind is : " <+> ppr (typeKind xi)
691 ; setWantedTyBind tv xi_unflat -- Set tv := xi_unflat
692 ; cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi_unflat xi_unflat
693 ; let flav = mkGivenFlavor gw UnkSkol
694 ; (cts, co) <- case coi of
695 ACo co -> do { can_eqs <- canEq flav cv_given (mkTyVarTy tv) xi_unflat
696 ; return (can_eqs, co) }
698 (singleCCan (CTyEqCan { cc_id = cv_given
699 , cc_flavor = mkGivenFlavor gw UnkSkol
700 , cc_tyvar = tv, cc_rhs = xi }
701 -- xi, *not* xi_unflat because
702 -- xi_unflat may require flattening!
705 Wanted {} -> setWantedCoBind cv co
706 Derived {} -> setDerivedCoBind cv co
707 _ -> pprPanic "Can't spontaneously solve *given*" empty
708 -- See Note [Avoid double unifications]
709 ; return $ Just (mkEqWorkList cts) }
711 occurCheck :: VarEnv (TcTyVar, TcType) -> InertSet
712 -> TcTyVar -> TcType -> Maybe (TcType,CoercionI)
713 -- Traverse @ty@ to make sure that @tv@ does not appear under some flatten skolem.
714 -- If it appears under some flatten skolem look in that flatten skolem equivalence class
715 -- (see Note [InertSet FlattenSkolemEqClass], [Loopy Spontaneous Solving]) to see if you
716 -- can find a different flatten skolem to use, that is, one that does not mention @tv@.
718 -- Postcondition: Just (ty', coi) = occurCheck binds inerts tv ty
720 -- NB: The returned type ty' may not be flat!
722 occurCheck ty_binds inerts the_tv the_ty
723 = ok emptyVarSet the_ty
725 -- If (fsk `elem` bad) then tv occurs in any rendering
726 -- of the type under the expansion of fsk
727 ok bad this_ty@(TyConApp tc tys)
728 | Just tys_cois <- allMaybes (map (ok bad) tys)
729 , (tys',cois') <- unzip tys_cois
730 = Just (TyConApp tc tys', mkTyConAppCoI tc cois')
731 | isSynTyCon tc, Just ty_expanded <- tcView this_ty
732 = ok bad ty_expanded -- See Note [Type synonyms and the occur check] in TcUnify
734 | Just (sty',coi) <- ok_pred bad sty
735 = Just (PredTy sty', coi)
736 ok bad (FunTy arg res)
737 | Just (arg', coiarg) <- ok bad arg, Just (res', coires) <- ok bad res
738 = Just (FunTy arg' res', mkFunTyCoI coiarg coires)
739 ok bad (AppTy fun arg)
740 | Just (fun', coifun) <- ok bad fun, Just (arg', coiarg) <- ok bad arg
741 = Just (AppTy fun' arg', mkAppTyCoI coifun coiarg)
742 ok bad (ForAllTy tv1 ty1)
743 -- WARNING: What if it is a (t1 ~ t2) => t3? It's not handled properly at the moment.
744 | Just (ty1', coi) <- ok bad ty1
745 = Just (ForAllTy tv1 ty1', mkForAllTyCoI tv1 coi)
748 ok bad this_ty@(TyVarTy tv)
749 | tv == the_tv = Nothing -- Occurs check error
750 | not (isTcTyVar tv) = Just (this_ty, IdCo this_ty) -- Bound var
751 | FlatSkol zty <- tcTyVarDetails tv = ok_fsk bad tv zty
752 | Just (_,ty) <- lookupVarEnv ty_binds tv = ok bad ty
753 | otherwise = Just (this_ty, IdCo this_ty)
755 -- Check if there exists a ty bind already, as a result of sneaky unification.
757 ok _bad _ty = Nothing
760 ok_pred bad (ClassP cn tys)
761 | Just tys_cois <- allMaybes $ map (ok bad) tys
762 = let (tys', cois') = unzip tys_cois
763 in Just (ClassP cn tys', mkClassPPredCoI cn cois')
764 ok_pred bad (IParam nm ty)
765 | Just (ty',co') <- ok bad ty
766 = Just (IParam nm ty', mkIParamPredCoI nm co')
767 ok_pred bad (EqPred ty1 ty2)
768 | Just (ty1',coi1) <- ok bad ty1, Just (ty2',coi2) <- ok bad ty2
769 = Just (EqPred ty1' ty2', mkEqPredCoI coi1 coi2)
770 ok_pred _ _ = Nothing
774 | fsk `elemVarSet` bad
775 -- We are already trying to find a rendering of fsk,
776 -- and to do that it seems we need a rendering, so fail
779 = firstJusts (ok new_bad zty : map (go_under_fsk new_bad) fsk_equivs)
781 fsk_equivs = getFskEqClass inerts fsk
782 new_bad = bad `extendVarSetList` (fsk : map fst fsk_equivs)
785 go_under_fsk bad_tvs (fsk,co)
786 | FlatSkol zty <- tcTyVarDetails fsk
787 = case ok bad_tvs zty of
789 Just (ty,coi') -> Just (ty, mkTransCoI coi' (ACo co))
790 | otherwise = pprPanic "go_down_equiv" (ppr fsk)
794 *********************************************************************************
796 The interact-with-inert Stage
798 *********************************************************************************
801 -- Interaction result of WorkItem <~> AtomicInert
803 = IR { ir_stop :: StopOrContinue
805 -- => Reagent (work item) consumed.
806 -- ContinueWith new_reagent
807 -- => Reagent transformed but keep gathering interactions.
808 -- The transformed item remains inert with respect
809 -- to any previously encountered inerts.
811 , ir_inert_action :: InertAction
812 -- Whether the inert item should remain in the InertSet.
814 , ir_new_work :: WorkList
815 -- new work items to add to the WorkList
818 -- What to do with the inert reactant.
819 data InertAction = KeepInert | DropInert
822 mkIRContinue :: Monad m => WorkItem -> InertAction -> WorkList -> m InteractResult
823 mkIRContinue wi keep newWork = return $ IR (ContinueWith wi) keep newWork
825 mkIRStop :: Monad m => InertAction -> WorkList -> m InteractResult
826 mkIRStop keep newWork = return $ IR Stop keep newWork
828 dischargeWorkItem :: Monad m => m InteractResult
829 dischargeWorkItem = mkIRStop KeepInert emptyWorkList
831 noInteraction :: Monad m => WorkItem -> m InteractResult
832 noInteraction workItem = mkIRContinue workItem KeepInert emptyWorkList
834 data WhichComesFromInert = LeftComesFromInert | RightComesFromInert
836 ---------------------------------------------------
837 -- Interact a single WorkItem with an InertSet as far as possible, i.e. until we get a Stop
838 -- result from an individual interaction (i.e. when the WorkItem is consumed), or until we've
839 -- interacted the WorkItem with the entire InertSet.
841 -- Postcondition: the new InertSet in the resulting StageResult is subset
842 -- of the input InertSet.
844 interactWithInertsStage :: SimplifierStage
845 interactWithInertsStage workItem inert
846 = foldlInertSetM interactNext initITR inert
848 initITR = SR { sr_inerts = emptyInert
849 , sr_new_work = emptyWorkList
850 , sr_stop = ContinueWith workItem }
853 interactNext :: StageResult -> AtomicInert -> TcS StageResult
854 interactNext it inert
855 | ContinueWith workItem <- sr_stop it
856 = do { ir <- interactWithInert inert workItem
857 ; let inerts = sr_inerts it
858 ; return $ SR { sr_inerts = if ir_inert_action ir == KeepInert
859 then inerts `updInertSet` inert
861 , sr_new_work = sr_new_work it `unionWorkLists` ir_new_work ir
862 , sr_stop = ir_stop ir } }
863 | otherwise = return $ itrAddInert inert it
866 itrAddInert :: AtomicInert -> StageResult -> StageResult
867 itrAddInert inert itr = itr { sr_inerts = (sr_inerts itr) `updInertSet` inert }
869 -- Do a single interaction of two constraints.
870 interactWithInert :: AtomicInert -> WorkItem -> TcS InteractResult
871 interactWithInert inert workitem
872 = do { ctxt <- getTcSContext
873 ; let is_allowed = allowedInteraction (simplEqsOnly ctxt) inert workitem
874 inert_ev = cc_id inert
875 work_ev = cc_id workitem
877 -- Never interact a wanted and a derived where the derived's evidence
878 -- mentions the wanted evidence in an unguarded way.
879 -- See Note [Superclasses and recursive dictionaries]
880 -- and Note [New Wanted Superclass Work]
881 -- We don't have to do this for givens, as we fully know the evidence for them.
883 case (cc_flavor inert, cc_flavor workitem) of
884 (Wanted loc, Derived _) -> isGoodRecEv work_ev (WantedEvVar inert_ev loc)
885 (Derived _, Wanted loc) -> isGoodRecEv inert_ev (WantedEvVar work_ev loc)
888 ; if is_allowed && rec_ev_ok then
889 doInteractWithInert inert workitem
891 noInteraction workitem
894 allowedInteraction :: Bool -> AtomicInert -> WorkItem -> Bool
895 -- Allowed interactions
896 allowedInteraction eqs_only (CDictCan {}) (CDictCan {}) = not eqs_only
897 allowedInteraction eqs_only (CIPCan {}) (CIPCan {}) = not eqs_only
898 allowedInteraction _ _ _ = True
900 --------------------------------------------
901 doInteractWithInert :: CanonicalCt -> CanonicalCt -> TcS InteractResult
902 -- Identical class constraints.
905 (CDictCan { cc_id = d1, cc_flavor = fl1, cc_class = cls1, cc_tyargs = tys1 })
906 workItem@(CDictCan { cc_id = d2, cc_flavor = fl2, cc_class = cls2, cc_tyargs = tys2 })
907 | cls1 == cls2 && (and $ zipWith tcEqType tys1 tys2)
908 = solveOneFromTheOther (d1,fl1) workItem
910 | cls1 == cls2 && (not (isGiven fl1 && isGiven fl2))
911 = -- See Note [When improvement happens]
912 do { let work_item_pred_loc = (ClassP cls2 tys2, ppr d2)
913 inert_pred_loc = (ClassP cls1 tys1, ppr d1)
914 loc = combineCtLoc fl1 fl2
915 eqn_pred_locs = improveFromAnother work_item_pred_loc inert_pred_loc
917 ; wevvars <- mkWantedFunDepEqns loc eqn_pred_locs
918 ; fd_cts <- canWanteds wevvars
919 ; let fd_work = mkEqWorkList fd_cts
920 -- See Note [Generating extra equalities]
921 ; if isEmptyCCan fd_cts || not (isWanted fl2) then -- || or impr. had previously kicked in
922 -- No improvement kicked in, keep going
923 mkIRContinue workItem KeepInert fd_work
924 else -- Improvement kicked in, throw him back into the worklist so that he
925 -- gets rewritten. The reason is that we do not want to let him fall off
926 -- at the end and then add its potential un-improved superclasses. This
927 -- optimisation crucially relies on prioritizing the equalities in the
930 -- The termination of this relies on wanteds being able to rewrite wanteds.
931 -- Since the class may be at the bottom of an equality worklist, which may
932 -- consist of insoluble wanteds, if these wanteds *never* become solved or given
933 -- (because they mention untouchables), the workitem will *never* be rewritten
934 -- so next time we meet him we will be once again producing FunDep equalities
935 -- for ever and ever!
936 mkIRStop KeepInert $ fd_work `unionWorkLists` singleNonEqWL workItem
938 -- See Note [FunDep Reactions]
941 -- Class constraint and given equality: use the equality to rewrite
942 -- the class constraint.
943 doInteractWithInert (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi })
944 (CDictCan { cc_id = dv, cc_flavor = wfl, cc_class = cl, cc_tyargs = xis })
945 | ifl `canRewrite` wfl
946 , tv `elemVarSet` tyVarsOfTypes xis
947 -- substitute for tv in xis. Note that the resulting class
948 -- constraint is still canonical, since substituting xi-types in
949 -- xi-types generates xi-types. However, it may no longer be
950 -- inert with respect to the inert set items we've already seen.
951 -- For example, consider the inert set
956 -- and the work item D a (w). D a does not interact with D Int.
957 -- Next, it does interact with a ~g Int, getting rewritten to D
958 -- Int (w). But now we must go back through the rest of the inert
959 -- set again, to find that it can now be discharged by the given D
961 = do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,wfl,cl,xis)
962 ; mkIRStop KeepInert $ singleNonEqWL rewritten_dict }
964 doInteractWithInert (CDictCan { cc_id = dv, cc_flavor = ifl, cc_class = cl, cc_tyargs = xis })
965 workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
966 | wfl `canRewrite` ifl
967 , tv `elemVarSet` tyVarsOfTypes xis
968 = do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,ifl,cl,xis)
969 ; mkIRContinue workItem DropInert (singleNonEqWL rewritten_dict) }
971 -- Class constraint and given equality: use the equality to rewrite
972 -- the class constraint.
973 doInteractWithInert (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi })
974 (CIPCan { cc_id = ipid, cc_flavor = wfl, cc_ip_nm = nm, cc_ip_ty = ty })
975 | ifl `canRewrite` wfl
976 , tv `elemVarSet` tyVarsOfType ty
977 = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,wfl,nm,ty)
978 ; mkIRStop KeepInert (singleNonEqWL rewritten_ip) }
980 doInteractWithInert (CIPCan { cc_id = ipid, cc_flavor = ifl, cc_ip_nm = nm, cc_ip_ty = ty })
981 workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
982 | wfl `canRewrite` ifl
983 , tv `elemVarSet` tyVarsOfType ty
984 = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,ifl,nm,ty)
985 ; mkIRContinue workItem DropInert (singleNonEqWL rewritten_ip) }
987 -- Two implicit parameter constraints. If the names are the same,
988 -- but their types are not, we generate a wanted type equality
989 -- that equates the type (this is "improvement").
990 -- However, we don't actually need the coercion evidence,
991 -- so we just generate a fresh coercion variable that isn't used anywhere.
992 doInteractWithInert (CIPCan { cc_id = id1, cc_flavor = ifl, cc_ip_nm = nm1, cc_ip_ty = ty1 })
993 workItem@(CIPCan { cc_flavor = wfl, cc_ip_nm = nm2, cc_ip_ty = ty2 })
994 | nm1 == nm2 && isGiven wfl && isGiven ifl
995 = -- See Note [Overriding implicit parameters]
996 -- Dump the inert item, override totally with the new one
997 -- Do not require type equality
998 mkIRContinue workItem DropInert emptyWorkList
1000 | nm1 == nm2 && ty1 `tcEqType` ty2
1001 = solveOneFromTheOther (id1,ifl) workItem
1004 = -- See Note [When improvement happens]
1005 do { co_var <- newWantedCoVar ty1 ty2
1006 ; let flav = Wanted (combineCtLoc ifl wfl)
1007 ; cans <- mkCanonical flav co_var
1008 ; mkIRContinue workItem KeepInert (mkEqWorkList cans) }
1011 -- Inert: equality, work item: function equality
1013 -- Never rewrite a given with a wanted equality, and a type function
1014 -- equality can never rewrite an equality. Note also that if we have
1015 -- F x1 ~ x2 and a ~ x3, and a occurs in x2, we don't rewrite it. We
1016 -- can wait until F x1 ~ x2 matches another F x1 ~ x4, and only then
1017 -- we will ``expose'' x2 and x4 to rewriting.
1019 -- Otherwise, we can try rewriting the type function equality with the equality.
1020 doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi1 })
1021 (CFunEqCan { cc_id = cv2, cc_flavor = wfl, cc_fun = tc
1022 , cc_tyargs = args, cc_rhs = xi2 })
1023 | ifl `canRewrite` wfl
1024 , tv `elemVarSet` tyVarsOfTypes args
1025 = do { rewritten_funeq <- rewriteFunEq (cv1,tv,xi1) (cv2,wfl,tc,args,xi2)
1026 ; mkIRStop KeepInert (singleEqWL rewritten_funeq) }
1028 -- Inert: function equality, work item: equality
1030 doInteractWithInert (CFunEqCan {cc_id = cv1, cc_flavor = ifl, cc_fun = tc
1031 , cc_tyargs = args, cc_rhs = xi1 })
1032 workItem@(CTyEqCan { cc_id = cv2, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi2 })
1033 | wfl `canRewrite` ifl
1034 , tv `elemVarSet` tyVarsOfTypes args
1035 = do { rewritten_funeq <- rewriteFunEq (cv2,tv,xi2) (cv1,ifl,tc,args,xi1)
1036 ; mkIRContinue workItem DropInert (singleEqWL rewritten_funeq) }
1038 doInteractWithInert (CFunEqCan { cc_id = cv1, cc_flavor = fl1, cc_fun = tc1
1039 , cc_tyargs = args1, cc_rhs = xi1 })
1040 workItem@(CFunEqCan { cc_id = cv2, cc_flavor = fl2, cc_fun = tc2
1041 , cc_tyargs = args2, cc_rhs = xi2 })
1042 | fl1 `canSolve` fl2 && lhss_match
1043 = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
1044 ; mkIRStop KeepInert (mkEqWorkList cans) }
1045 | fl2 `canSolve` fl1 && lhss_match
1046 = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
1047 ; mkIRContinue workItem DropInert (mkEqWorkList cans) }
1049 lhss_match = tc1 == tc2 && and (zipWith tcEqType args1 args2)
1052 inert@(CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
1053 workItem@(CTyEqCan { cc_id = cv2, cc_flavor = fl2, cc_tyvar = tv2, cc_rhs = xi2 })
1054 -- Check for matching LHS
1055 | fl1 `canSolve` fl2 && tv1 == tv2
1056 = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
1057 ; mkIRStop KeepInert (mkEqWorkList cans) }
1059 | fl2 `canSolve` fl1 && tv1 == tv2
1060 = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
1061 ; mkIRContinue workItem DropInert (mkEqWorkList cans) }
1063 -- Check for rewriting RHS
1064 | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfType xi2
1065 = do { rewritten_eq <- rewriteEqRHS (cv1,tv1,xi1) (cv2,fl2,tv2,xi2)
1066 ; mkIRStop KeepInert (mkEqWorkList rewritten_eq) }
1067 | fl2 `canRewrite` fl1 && tv2 `elemVarSet` tyVarsOfType xi1
1068 = do { rewritten_eq <- rewriteEqRHS (cv2,tv2,xi2) (cv1,fl1,tv1,xi1)
1069 ; mkIRContinue workItem DropInert (mkEqWorkList rewritten_eq) }
1071 -- Finally, if workitem is a Flatten Equivalence Class constraint and the
1072 -- inert is a wanted constraint, even when the workitem cannot rewrite the
1073 -- inert, drop the inert out because you may have to reconsider solving the
1074 -- inert *using* the equivalence class you created. See note [Loopy Spontaneous Solving]
1075 -- and [InertSet FlattenSkolemEqClass]
1077 | not $ isGiven fl1, -- The inert is wanted or derived
1078 isMetaTyVar tv1, -- and has a unification variable lhs
1079 FlatSkol {} <- tcTyVarDetails tv2, -- And workitem is a flatten skolem equality
1080 Just tv2' <- tcGetTyVar_maybe xi2, FlatSkol {} <- tcTyVarDetails tv2'
1081 = mkIRContinue workItem DropInert (singleEqWL inert)
1084 -- Fall-through case for all other situations
1085 doInteractWithInert _ workItem = noInteraction workItem
1087 -------------------------
1088 -- Equational Rewriting
1089 rewriteDict :: (CoVar, TcTyVar, Xi) -> (DictId, CtFlavor, Class, [Xi]) -> TcS CanonicalCt
1090 rewriteDict (cv,tv,xi) (dv,gw,cl,xis)
1091 = do { let cos = substTysWith [tv] [mkCoVarCoercion cv] xis -- xis[tv] ~ xis[xi]
1092 args = substTysWith [tv] [xi] xis
1094 dict_co = mkTyConCoercion con cos
1095 ; dv' <- newDictVar cl args
1097 Wanted {} -> setDictBind dv (EvCast dv' (mkSymCoercion dict_co))
1098 _given_or_derived -> setDictBind dv' (EvCast dv dict_co)
1099 ; return (CDictCan { cc_id = dv'
1102 , cc_tyargs = args }) }
1104 rewriteIP :: (CoVar,TcTyVar,Xi) -> (EvVar,CtFlavor, IPName Name, TcType) -> TcS CanonicalCt
1105 rewriteIP (cv,tv,xi) (ipid,gw,nm,ty)
1106 = do { let ip_co = substTyWith [tv] [mkCoVarCoercion cv] ty -- ty[tv] ~ t[xi]
1107 ty' = substTyWith [tv] [xi] ty
1108 ; ipid' <- newIPVar nm ty'
1110 Wanted {} -> setIPBind ipid (EvCast ipid' (mkSymCoercion ip_co))
1111 _given_or_derived -> setIPBind ipid' (EvCast ipid ip_co)
1112 ; return (CIPCan { cc_id = ipid'
1115 , cc_ip_ty = ty' }) }
1117 rewriteFunEq :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TyCon, [Xi], Xi) -> TcS CanonicalCt
1118 rewriteFunEq (cv1,tv,xi1) (cv2,gw, tc,args,xi2)
1119 = do { let arg_cos = substTysWith [tv] [mkCoVarCoercion cv1] args
1120 args' = substTysWith [tv] [xi1] args
1121 fun_co = mkTyConCoercion tc arg_cos
1122 ; cv2' <- case gw of
1123 Wanted {} -> do { cv2' <- newWantedCoVar (mkTyConApp tc args') xi2
1124 ; setWantedCoBind cv2 $
1125 mkTransCoercion fun_co (mkCoVarCoercion cv2')
1127 _giv_or_der -> newGivOrDerCoVar (mkTyConApp tc args') xi2 $
1128 mkTransCoercion (mkSymCoercion fun_co) (mkCoVarCoercion cv2)
1129 ; return (CFunEqCan { cc_id = cv2'
1136 rewriteEqRHS :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TcTyVar,Xi) -> TcS CanonicalCts
1137 -- Use the first equality to rewrite the second, flavors already checked.
1138 -- E.g. c1 : tv1 ~ xi1 c2 : tv2 ~ xi2
1139 -- rewrites c2 to give
1140 -- c2' : tv2 ~ xi2[xi1/tv1]
1141 -- We must do an occurs check to sure the new constraint is canonical
1142 -- So we might return an empty bag
1143 rewriteEqRHS (cv1,tv1,xi1) (cv2,gw,tv2,xi2)
1144 | Just tv2' <- tcGetTyVar_maybe xi2'
1145 , tv2 == tv2' -- In this case xi2[xi1/tv1] = tv2, so we have tv2~tv2
1146 = do { when (isWanted gw) (setWantedCoBind cv2 (mkSymCoercion co2'))
1147 ; return emptyCCan }
1152 -> do { cv2' <- newWantedCoVar (mkTyVarTy tv2) xi2'
1153 ; setWantedCoBind cv2 $
1154 mkCoVarCoercion cv2' `mkTransCoercion` mkSymCoercion co2'
1157 -> newGivOrDerCoVar (mkTyVarTy tv2) xi2' $
1158 mkCoVarCoercion cv2 `mkTransCoercion` co2'
1160 ; xi2'' <- canOccursCheck gw tv2 xi2' -- we know xi2' is *not* tv2
1161 ; return (singleCCan $ CTyEqCan { cc_id = cv2'
1167 xi2' = substTyWith [tv1] [xi1] xi2
1168 co2' = substTyWith [tv1] [mkCoVarCoercion cv1] xi2 -- xi2 ~ xi2[xi1/tv1]
1171 rewriteEqLHS :: WhichComesFromInert -> (Coercion,Xi) -> (CoVar,CtFlavor,Xi) -> TcS CanonicalCts
1172 -- Used to ineratct two equalities of the following form:
1173 -- First Equality: co1: (XXX ~ xi1)
1174 -- Second Equality: cv2: (XXX ~ xi2)
1175 -- Where the cv1 `canSolve` cv2 equality
1176 -- We have an option of creating new work (xi1 ~ xi2) OR (xi2 ~ xi1). This
1177 -- depends on whether the left or the right equality comes from the inert set.
1179 -- prefer to create (xi2 ~ xi1) if the first comes from the inert
1180 -- prefer to create (xi1 ~ xi2) if the second comes from the inert
1181 rewriteEqLHS which (co1,xi1) (cv2,gw,xi2)
1182 = do { cv2' <- case (isWanted gw, which) of
1183 (True,LeftComesFromInert) ->
1184 do { cv2' <- newWantedCoVar xi2 xi1
1185 ; setWantedCoBind cv2 $
1186 co1 `mkTransCoercion` mkSymCoercion (mkCoVarCoercion cv2')
1188 (True,RightComesFromInert) ->
1189 do { cv2' <- newWantedCoVar xi1 xi2
1190 ; setWantedCoBind cv2 $
1191 co1 `mkTransCoercion` mkCoVarCoercion cv2'
1193 (False,LeftComesFromInert) ->
1194 newGivOrDerCoVar xi2 xi1 $
1195 mkSymCoercion (mkCoVarCoercion cv2) `mkTransCoercion` co1
1196 (False,RightComesFromInert) ->
1197 newGivOrDerCoVar xi1 xi2 $
1198 mkSymCoercion co1 `mkTransCoercion` mkCoVarCoercion cv2
1199 ; mkCanonical gw cv2'
1202 solveOneFromTheOther :: (EvVar, CtFlavor) -> CanonicalCt -> TcS InteractResult
1203 -- First argument inert, second argument workitem. They both represent
1204 -- wanted/given/derived evidence for the *same* predicate so we try here to
1205 -- discharge one directly from the other.
1207 -- Precondition: value evidence only (implicit parameters, classes)
1209 solveOneFromTheOther (iid,ifl) workItem
1210 -- Both derived needs a special case. You might think that we do not need
1211 -- two evidence terms for the same claim. But, since the evidence is partial,
1212 -- either evidence may do in some cases; see TcSMonad.isGoodRecEv.
1213 -- See also Example 3 in Note [Superclasses and recursive dictionaries]
1214 | isDerived ifl && isDerived wfl
1215 = noInteraction workItem
1217 | ifl `canSolve` wfl
1218 = do { unless (isGiven wfl) $ setEvBind wid (EvId iid)
1219 -- Overwrite the binding, if one exists
1220 -- For Givens, which are lambda-bound, nothing to overwrite,
1221 ; dischargeWorkItem }
1223 | otherwise -- wfl `canSolve` ifl
1224 = do { unless (isGiven ifl) $ setEvBind iid (EvId wid)
1225 ; mkIRContinue workItem DropInert emptyWorkList }
1228 wfl = cc_flavor workItem
1229 wid = cc_id workItem
1232 Note [Superclasses and recursive dictionaries]
1233 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1234 Overlaps with Note [SUPERCLASS-LOOP 1]
1235 Note [SUPERCLASS-LOOP 2]
1236 Note [Recursive instances and superclases]
1237 ToDo: check overlap and delete redundant stuff
1239 Right before adding a given into the inert set, we must
1240 produce some more work, that will bring the superclasses
1241 of the given into scope. The superclass constraints go into
1244 When we simplify a wanted constraint, if we first see a matching
1245 instance, we may produce new wanted work. To (1) avoid doing this work
1246 twice in the future and (2) to handle recursive dictionaries we may ``cache''
1247 this item as solved (in effect, given) into our inert set and with that add
1248 its superclass constraints (as given) in our worklist.
1250 But now we have added partially solved constraints to the worklist which may
1251 interact with other wanteds. Consider the example:
1255 class Eq b => Foo a b --- 0-th selector
1256 instance Eq a => Foo [a] a --- fooDFun
1258 and wanted (Foo [t] t). We are first going to see that the instance matches
1259 and create an inert set that includes the solved (Foo [t] t) and its
1261 d1 :_g Foo [t] t d1 := EvDFunApp fooDFun d3
1262 d2 :_g Eq t d2 := EvSuperClass d1 0
1263 Our work list is going to contain a new *wanted* goal
1265 It is wrong to react the wanted (Eq t) with the given (Eq t) because that would
1266 construct loopy evidence. Hence the check isGoodRecEv in doInteractWithInert.
1268 OK, so we have ruled out bad behaviour, but how do we ge recursive dictionaries,
1273 data D r = ZeroD | SuccD (r (D r));
1275 instance (Eq (r (D r))) => Eq (D r) where
1276 ZeroD == ZeroD = True
1277 (SuccD a) == (SuccD b) = a == b
1280 equalDC :: D [] -> D [] -> Bool;
1283 We need to prove (Eq (D [])). Here's how we go:
1287 by instance decl, holds if
1291 *BUT* we have an inert set which gives us (no superclasses):
1293 By the instance declaration of Eq we can show the 'd2' goal if
1295 where d2 = dfEqList d3
1297 Now, however this wanted can interact with our inert d1 to set:
1299 and solve the goal. Why was this interaction OK? Because, if we chase the
1300 evidence of d1 ~~> dfEqD d2 ~~-> dfEqList d3, so by setting d3 := d1 we
1302 d3 := dfEqD2 (dfEqList d3)
1303 which is FINE because the use of d3 is protected by the instance function
1306 So, our strategy is to try to put solved wanted dictionaries into the
1307 inert set along with their superclasses (when this is meaningful,
1308 i.e. when new wanted goals are generated) but solve a wanted dictionary
1309 from a given only in the case where the evidence variable of the
1310 wanted is mentioned in the evidence of the given (recursively through
1311 the evidence binds) in a protected way: more instance function applications
1312 than superclass selectors.
1314 Here are some more examples from GHC's previous type checker
1318 This code arises in the context of "Scrap Your Boilerplate with Class"
1322 instance Sat (ctx Char) => Data ctx Char -- dfunData1
1323 instance (Sat (ctx [a]), Data ctx a) => Data ctx [a] -- dfunData2
1325 class Data Maybe a => Foo a
1327 instance Foo t => Sat (Maybe t) -- dfunSat
1329 instance Data Maybe a => Foo a -- dfunFoo1
1330 instance Foo a => Foo [a] -- dfunFoo2
1331 instance Foo [Char] -- dfunFoo3
1333 Consider generating the superclasses of the instance declaration
1334 instance Foo a => Foo [a]
1336 So our problem is this
1338 d1 :_w Data Maybe [t]
1340 We may add the given in the inert set, along with its superclasses
1341 [assuming we don't fail because there is a matching instance, see
1342 tryTopReact, given case ]
1346 d01 :_g Data Maybe t -- d2 := EvDictSuperClass d0 0
1347 d1 :_w Data Maybe [t]
1348 Then d2 can readily enter the inert, and we also do solving of the wanted
1351 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1353 d2 :_w Sat (Maybe [t])
1355 d01 :_g Data Maybe t
1356 Now, we may simplify d2 more:
1359 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1360 d1 :_g Data Maybe [t]
1361 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1365 d01 :_g Data Maybe t
1367 Now, we can just solve d3.
1370 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1371 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1374 d01 :_g Data Maybe t
1375 And now we can simplify d4 again, but since it has superclasses we *add* them to the worklist:
1378 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1379 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1380 d4 :_g Foo [t] d4 := dfunFoo2 d5
1383 d6 :_g Data Maybe [t] d6 := EvDictSuperClass d4 0
1384 d01 :_g Data Maybe t
1385 Now, d5 can be solved! (and its superclass enter scope)
1388 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1389 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1390 d4 :_g Foo [t] d4 := dfunFoo2 d5
1391 d5 :_g Foo t d5 := dfunFoo1 d7
1394 d6 :_g Data Maybe [t]
1395 d8 :_g Data Maybe t d8 := EvDictSuperClass d5 0
1396 d01 :_g Data Maybe t
1399 [1] Suppose we pick d8 and we react him with d01. Which of the two givens should
1400 we keep? Well, we *MUST NOT* drop d01 because d8 contains recursive evidence
1401 that must not be used (look at case interactInert where both inert and workitem
1402 are givens). So we have several options:
1403 - Drop the workitem always (this will drop d8)
1404 This feels very unsafe -- what if the work item was the "good" one
1405 that should be used later to solve another wanted?
1406 - Don't drop anyone: the inert set may contain multiple givens!
1407 [This is currently implemented]
1409 The "don't drop anyone" seems the most safe thing to do, so now we come to problem 2:
1410 [2] We have added both d6 and d01 in the inert set, and we are interacting our wanted
1411 d7. Now the [isRecDictEv] function in the ineration solver
1412 [case inert-given workitem-wanted] will prevent us from interacting d7 := d8
1413 precisely because chasing the evidence of d8 leads us to an unguarded use of d7.
1415 So, no interaction happens there. Then we meet d01 and there is no recursion
1416 problem there [isRectDictEv] gives us the OK to interact and we do solve d7 := d01!
1418 Note [SUPERCLASS-LOOP 1]
1419 ~~~~~~~~~~~~~~~~~~~~~~~~
1420 We have to be very, very careful when generating superclasses, lest we
1421 accidentally build a loop. Here's an example:
1425 class S a => C a where { opc :: a -> a }
1426 class S b => D b where { opd :: b -> b }
1428 instance C Int where
1431 instance D Int where
1434 From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int}
1435 Simplifying, we may well get:
1436 $dfCInt = :C ds1 (opd dd)
1439 Notice that we spot that we can extract ds1 from dd.
1441 Alas! Alack! We can do the same for (instance D Int):
1443 $dfDInt = :D ds2 (opc dc)
1447 And now we've defined the superclass in terms of itself.
1448 Two more nasty cases are in
1453 - Satisfy the superclass context *all by itself*
1454 (tcSimplifySuperClasses)
1455 - And do so completely; i.e. no left-over constraints
1456 to mix with the constraints arising from method declarations
1459 Note [SUPERCLASS-LOOP 2]
1460 ~~~~~~~~~~~~~~~~~~~~~~~~
1461 We need to be careful when adding "the constaint we are trying to prove".
1462 Suppose we are *given* d1:Ord a, and want to deduce (d2:C [a]) where
1464 class Ord a => C a where
1465 instance Ord [a] => C [a] where ...
1467 Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the
1468 superclasses of C [a] to avails. But we must not overwrite the binding
1469 for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
1472 Here's another variant, immortalised in tcrun020
1473 class Monad m => C1 m
1474 class C1 m => C2 m x
1475 instance C2 Maybe Bool
1476 For the instance decl we need to build (C1 Maybe), and it's no good if
1477 we run around and add (C2 Maybe Bool) and its superclasses to the avails
1478 before we search for C1 Maybe.
1480 Here's another example
1481 class Eq b => Foo a b
1482 instance Eq a => Foo [a] a
1486 we'll first deduce that it holds (via the instance decl). We must not
1487 then overwrite the Eq t constraint with a superclass selection!
1489 At first I had a gross hack, whereby I simply did not add superclass constraints
1490 in addWanted, though I did for addGiven and addIrred. This was sub-optimal,
1491 becuase it lost legitimate superclass sharing, and it still didn't do the job:
1492 I found a very obscure program (now tcrun021) in which improvement meant the
1493 simplifier got two bites a the cherry... so something seemed to be an Stop
1494 first time, but reducible next time.
1496 Now we implement the Right Solution, which is to check for loops directly
1497 when adding superclasses. It's a bit like the occurs check in unification.
1499 Note [Recursive instances and superclases]
1500 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1501 Consider this code, which arises in the context of "Scrap Your
1502 Boilerplate with Class".
1506 instance Sat (ctx Char) => Data ctx Char
1507 instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]
1509 class Data Maybe a => Foo a
1511 instance Foo t => Sat (Maybe t)
1513 instance Data Maybe a => Foo a
1514 instance Foo a => Foo [a]
1517 In the instance for Foo [a], when generating evidence for the superclasses
1518 (ie in tcSimplifySuperClasses) we need a superclass (Data Maybe [a]).
1519 Using the instance for Data, we therefore need
1520 (Sat (Maybe [a], Data Maybe a)
1521 But we are given (Foo a), and hence its superclass (Data Maybe a).
1522 So that leaves (Sat (Maybe [a])). Using the instance for Sat means
1523 we need (Foo [a]). And that is the very dictionary we are bulding
1524 an instance for! So we must put that in the "givens". So in this
1526 Given: Foo a, Foo [a]
1527 Wanted: Data Maybe [a]
1529 BUT we must *not not not* put the *superclasses* of (Foo [a]) in
1530 the givens, which is what 'addGiven' would normally do. Why? Because
1531 (Data Maybe [a]) is the superclass, so we'd "satisfy" the wanted
1532 by selecting a superclass from Foo [a], which simply makes a loop.
1534 On the other hand we *must* put the superclasses of (Foo a) in
1535 the givens, as you can see from the derivation described above.
1537 Conclusion: in the very special case of tcSimplifySuperClasses
1538 we have one 'given' (namely the "this" dictionary) whose superclasses
1539 must not be added to 'givens' by addGiven.
1541 There is a complication though. Suppose there are equalities
1542 instance (Eq a, a~b) => Num (a,b)
1543 Then we normalise the 'givens' wrt the equalities, so the original
1544 given "this" dictionary is cast to one of a different type. So it's a
1545 bit trickier than before to identify the "special" dictionary whose
1546 superclasses must not be added. See test
1547 indexed-types/should_run/EqInInstance
1549 We need a persistent property of the dictionary to record this
1550 special-ness. Current I'm using the InstLocOrigin (a bit of a hack,
1551 but cool), which is maintained by dictionary normalisation.
1552 Specifically, the InstLocOrigin is
1554 then the no-superclass thing kicks in. WATCH OUT if you fiddle
1557 Note [MATCHING-SYNONYMS]
1558 ~~~~~~~~~~~~~~~~~~~~~~~~
1559 When trying to match a dictionary (D tau) to a top-level instance, or a
1560 type family equation (F taus_1 ~ tau_2) to a top-level family instance,
1561 we do *not* need to expand type synonyms because the matcher will do that for us.
1564 Note [RHS-FAMILY-SYNONYMS]
1565 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1566 The RHS of a family instance is represented as yet another constructor which is
1567 like a type synonym for the real RHS the programmer declared. Eg:
1568 type instance F (a,a) = [a]
1570 :R32 a = [a] -- internal type synonym introduced
1571 F (a,a) ~ :R32 a -- instance
1573 When we react a family instance with a type family equation in the work list
1574 we keep the synonym-using RHS without expansion.
1577 *********************************************************************************
1579 The top-reaction Stage
1581 *********************************************************************************
1584 -- If a work item has any form of interaction with top-level we get this
1585 data TopInteractResult
1586 = NoTopInt -- No top-level interaction
1588 { tir_new_work :: WorkList -- Sub-goals or new work (could be given,
1589 -- for superclasses)
1590 , tir_new_inert :: StopOrContinue -- The input work item, ready to become *inert* now:
1591 } -- NB: in ``given'' (solved) form if the
1592 -- original was wanted or given and instance match
1593 -- was found, but may also be in wanted form if we
1594 -- only reacted with functional dependencies
1595 -- arising from top-level instances.
1597 topReactionsStage :: SimplifierStage
1598 topReactionsStage workItem inerts
1599 = do { tir <- tryTopReact workItem
1602 return $ SR { sr_inerts = inerts
1603 , sr_new_work = emptyWorkList
1604 , sr_stop = ContinueWith workItem }
1605 SomeTopInt tir_new_work tir_new_inert ->
1606 return $ SR { sr_inerts = inerts
1607 , sr_new_work = tir_new_work
1608 , sr_stop = tir_new_inert
1612 tryTopReact :: WorkItem -> TcS TopInteractResult
1613 tryTopReact workitem
1614 = do { -- A flag controls the amount of interaction allowed
1615 -- See Note [Simplifying RULE lhs constraints]
1616 ctxt <- getTcSContext
1617 ; if allowedTopReaction (simplEqsOnly ctxt) workitem
1618 then do { traceTcS "tryTopReact / calling doTopReact" (ppr workitem)
1619 ; doTopReact workitem }
1620 else return NoTopInt
1623 allowedTopReaction :: Bool -> WorkItem -> Bool
1624 allowedTopReaction eqs_only (CDictCan {}) = not eqs_only
1625 allowedTopReaction _ _ = True
1628 doTopReact :: WorkItem -> TcS TopInteractResult
1629 -- The work item does not react with the inert set,
1630 -- so try interaction with top-level instances
1631 doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Wanted loc
1632 , cc_class = cls, cc_tyargs = xis })
1633 = do { -- See Note [MATCHING-SYNONYMS]
1634 ; lkp_inst_res <- matchClassInst cls xis loc
1635 ; case lkp_inst_res of
1636 NoInstance -> do { traceTcS "doTopReact/ no class instance for" (ppr dv)
1638 GenInst wtvs ev_term -> -- Solved
1639 -- No need to do fundeps stuff here; the instance
1640 -- matches already so we won't get any more info
1641 -- from functional dependencies
1642 do { traceTcS "doTopReact/ found class instance for" (ppr dv)
1643 ; setDictBind dv ev_term
1644 ; workList <- canWanteds wtvs
1646 -- Solved in one step and no new wanted work produced.
1647 -- i.e we directly matched a top-level instance
1648 -- No point in caching this in 'inert', nor in adding superclasses
1649 then return $ SomeTopInt { tir_new_work = emptyWorkList
1650 , tir_new_inert = Stop }
1652 -- Solved and new wanted work produced, you may cache the
1653 -- (tentatively solved) dictionary as Derived and its superclasses
1654 else do { let solved = makeSolved workItem
1655 ; sc_work <- newSCWorkFromFlavored dv (Derived loc) cls xis
1656 ; let inst_work = workListFromCCans workList
1657 ; return $ SomeTopInt
1658 { tir_new_work = inst_work `unionWorkLists` sc_work
1659 , tir_new_inert = ContinueWith solved } }
1663 -- Try for a fundep reaction beween the wanted item
1664 -- and a top-level instance declaration
1666 = do { instEnvs <- getInstEnvs
1667 ; let eqn_pred_locs = improveFromInstEnv (classInstances instEnvs)
1668 (ClassP cls xis, ppr dv)
1669 ; wevvars <- mkWantedFunDepEqns loc eqn_pred_locs
1670 -- NB: fundeps generate some wanted equalities, but
1671 -- we don't use their evidence for anything
1672 ; fd_cts <- canWanteds wevvars
1673 ; let fd_work = mkEqWorkList fd_cts
1675 ; if isEmptyCCan fd_cts then
1676 do { sc_work <- newSCWorkFromFlavored dv (Derived loc) cls xis
1677 ; return $ SomeTopInt { tir_new_work = fd_work `unionWorkLists` sc_work
1678 , tir_new_inert = ContinueWith workItem }
1680 else -- More fundep work produced, don't do any superlcass stuff, just
1681 -- thow him back in the worklist prioritizing the solution of fd equalities
1683 SomeTopInt { tir_new_work = fd_work `unionWorkLists` singleNonEqWL workItem
1684 , tir_new_inert = Stop }
1686 -- NB: workItem is inert, but it isn't solved
1687 -- keep it as inert, although it's not solved because we
1688 -- have now reacted all its top-level fundep-induced equalities!
1690 -- See Note [FunDep Reactions]
1693 -- Otherwise, we have a given or derived
1694 doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = fl
1695 , cc_class = cls, cc_tyargs = xis })
1696 = do { sc_work <- newSCWorkFromFlavored dv fl cls xis
1697 ; return $ SomeTopInt sc_work (ContinueWith workItem) }
1698 -- See Note [Given constraint that matches an instance declaration]
1701 doTopReact (CFunEqCan { cc_id = cv, cc_flavor = fl
1702 , cc_fun = tc, cc_tyargs = args, cc_rhs = xi })
1703 = ASSERT (isSynFamilyTyCon tc) -- No associated data families have reached that far
1704 do { match_res <- matchFam tc args -- See Note [MATCHING-SYNONYMS]
1708 MatchInstSingle (rep_tc, rep_tys)
1709 -> do { let Just coe_tc = tyConFamilyCoercion_maybe rep_tc
1710 Just rhs_ty = tcView (mkTyConApp rep_tc rep_tys)
1711 -- Eagerly expand away the type synonym on the
1712 -- RHS of a type function, so that it never
1713 -- appears in an error message
1714 -- See Note [Type synonym families] in TyCon
1715 coe = mkTyConApp coe_tc rep_tys
1717 Wanted {} -> do { cv' <- newWantedCoVar rhs_ty xi
1718 ; setWantedCoBind cv $
1719 coe `mkTransCoercion`
1722 _ -> newGivOrDerCoVar xi rhs_ty $
1723 mkSymCoercion (mkCoVarCoercion cv) `mkTransCoercion` coe
1725 ; can_cts <- mkCanonical fl cv'
1726 ; let workList = mkEqWorkList can_cts
1727 ; return $ SomeTopInt workList Stop }
1729 -> panicTcS $ text "TcSMonad.matchFam returned multiple instances!"
1733 -- Any other work item does not react with any top-level equations
1734 doTopReact _workItem = return NoTopInt
1737 Note [FunDep and implicit parameter reactions]
1738 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1739 Currently, our story of interacting two dictionaries (or a dictionary
1740 and top-level instances) for functional dependencies, and implicit
1741 paramters, is that we simply produce new wanted equalities. So for example
1743 class D a b | a -> b where ...
1749 We generate the extra work item
1751 where 'cv' is currently unused. However, this new item reacts with d2,
1752 discharging it in favour of a new constraint d2' thus:
1754 d2 := d2' |> D Int cv
1755 Now d2' can be discharged from d1
1757 We could be more aggressive and try to *immediately* solve the dictionary
1758 using those extra equalities. With the same inert set and work item we
1759 might dischard d2 directly:
1762 d2 := d1 |> D Int cv
1764 But in general it's a bit painful to figure out the necessary coercion,
1765 so we just take the first approach. Here is a better example. Consider:
1766 class C a b c | a -> b
1768 [Given] d1 : C T Int Char
1769 [Wanted] d2 : C T beta Int
1770 In this case, it's *not even possible* to solve the wanted immediately.
1771 So we should simply output the functional dependency and add this guy
1772 [but NOT its superclasses] back in the worklist. Even worse:
1773 [Given] d1 : C T Int beta
1774 [Wanted] d2: C T beta Int
1775 Then it is solvable, but its very hard to detect this on the spot.
1777 It's exactly the same with implicit parameters, except that the
1778 "aggressive" approach would be much easier to implement.
1780 Note [When improvement happens]
1781 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1782 We fire an improvement rule when
1784 * Two constraints match (modulo the fundep)
1785 e.g. C t1 t2, C t1 t3 where C a b | a->b
1786 The two match because the first arg is identical
1788 * At least one is not Given. If they are both given, we don't fire
1789 the reaction because we have no way of constructing evidence for a
1790 new equality nor does it seem right to create a new wanted goal
1791 (because the goal will most likely contain untouchables, which
1792 can't be solved anyway)!
1794 Note that we *do* fire the improvement if one is Given and one is Derived.
1795 The latter can be a superclass of a wanted goal. Example (tcfail138)
1796 class L a b | a -> b
1797 class (G a, L a b) => C a b
1799 instance C a b' => G (Maybe a)
1800 instance C a b => C (Maybe a) a
1801 instance L (Maybe a) a
1803 When solving the superclasses of the (C (Maybe a) a) instance, we get
1804 Given: C a b ... and hance by superclasses, (G a, L a b)
1806 Use the instance decl to get
1808 The (C a b') is inert, so we generate its Derived superclasses (L a b'),
1809 and now we need improvement between that derived superclass an the Given (L a b)
1811 Note [Overriding implicit parameters]
1812 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1814 f :: (?x::a) -> Bool -> a
1816 g v = let ?x::Int = 3
1817 in (f v, let ?x::Bool = True in f v)
1819 This should probably be well typed, with
1820 g :: Bool -> (Int, Bool)
1822 So the inner binding for ?x::Bool *overrides* the outer one.
1823 Hence a work-item Given overrides an inert-item Given.
1825 Note [Given constraint that matches an instance declaration]
1826 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1827 What should we do when we discover that one (or more) top-level
1828 instances match a given (or solved) class constraint? We have
1831 1. Reject the program. The reason is that there may not be a unique
1832 best strategy for the solver. Example, from the OutsideIn(X) paper:
1833 instance P x => Q [x]
1834 instance (x ~ y) => R [x] y
1836 wob :: forall a b. (Q [b], R b a) => a -> Int
1838 g :: forall a. Q [a] => [a] -> Int
1841 will generate the impliation constraint:
1842 Q [a] => (Q [beta], R beta [a])
1843 If we react (Q [beta]) with its top-level axiom, we end up with a
1844 (P beta), which we have no way of discharging. On the other hand,
1845 if we react R beta [a] with the top-level we get (beta ~ a), which
1846 is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
1847 now solvable by the given Q [a].
1849 However, this option is restrictive, for instance [Example 3] from
1850 Note [Recursive dictionaries] will fail to work.
1852 2. Ignore the problem, hoping that the situations where there exist indeed
1853 such multiple strategies are rare: Indeed the cause of the previous
1854 problem is that (R [x] y) yields the new work (x ~ y) which can be
1855 *spontaneously* solved, not using the givens.
1857 We are choosing option 2 below but we might consider having a flag as well.
1860 Note [New Wanted Superclass Work]
1861 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1862 Even in the case of wanted constraints, we add all of its superclasses as
1863 new given work. There are several reasons for this:
1864 a) to minimise error messages;
1865 eg suppose we have wanted (Eq a, Ord a)
1866 then we report only (Ord a) unsoluble
1868 b) to make the smallest number of constraints when *inferring* a type
1869 (same Eq/Ord example)
1871 c) for recursive dictionaries we *must* add the superclasses
1872 so that we can use them when solving a sub-problem
1874 d) To allow FD-like improvement for type families. Assume that
1876 class C a b | a -> b
1877 and we have to solve the implication constraint:
1879 Then, FD improvement can help us to produce a new wanted (beta ~ b)
1881 We want to have the same effect with the type family encoding of
1882 functional dependencies. Namely, consider:
1883 class (F a ~ b) => C a b
1884 Now suppose that we have:
1887 By interacting the given we will get given (F a ~ b) which is not
1888 enough by itself to make us discharge (C a beta). However, we
1889 may create a new derived equality from the super-class of the
1890 wanted constraint (C a beta), namely derived (F a ~ beta).
1891 Now we may interact this with given (F a ~ b) to get:
1893 But 'beta' is a touchable unification variable, and hence OK to
1894 unify it with 'b', replacing the derived evidence with the identity.
1896 This requires trySpontaneousSolve to solve *derived*
1897 equalities that have a touchable in their RHS, *in addition*
1898 to solving wanted equalities.
1900 Here is another example where this is useful.
1904 class (F a ~ b) => C a b
1905 And we are given the wanteds:
1909 We surely do *not* want to quantify over (b ~ c), since if someone provides
1910 dictionaries for (C a b) and (C a c), these dictionaries can provide a proof
1911 of (b ~ c), hence no extra evidence is necessary. Here is what will happen:
1913 Step 1: We will get new *given* superclass work,
1914 provisionally to our solving of w1 and w2
1916 g1: F a ~ b, g2 : F a ~ c,
1917 w1 : C a b, w2 : C a c, w3 : b ~ c
1919 The evidence for g1 and g2 is a superclass evidence term:
1921 g1 := sc w1, g2 := sc w2
1923 Step 2: The givens will solve the wanted w3, so that
1924 w3 := sym (sc w1) ; sc w2
1926 Step 3: Now, one may naively assume that then w2 can be solve from w1
1927 after rewriting with the (now solved equality) (b ~ c).
1929 But this rewriting is ruled out by the isGoodRectDict!
1931 Conclusion, we will (correctly) end up with the unsolved goals
1934 NB: The desugarer needs be more clever to deal with equalities
1935 that participate in recursive dictionary bindings.
1938 newSCWorkFromFlavored :: EvVar -> CtFlavor -> Class -> [Xi]
1940 newSCWorkFromFlavored ev flavor cls xis
1941 | Given loc <- flavor -- The NoScSkol says "don't add superclasses"
1942 , NoScSkol <- ctLocOrigin loc -- Very important!
1943 = return emptyWorkList
1946 = do { let (tyvars, sc_theta, _, _) = classBigSig cls
1947 sc_theta1 = substTheta (zipTopTvSubst tyvars xis) sc_theta
1948 -- Add *all* its superclasses (equalities or not) as new given work
1949 -- See Note [New Wanted Superclass Work]
1950 ; sc_vars <- zipWithM inst_one sc_theta1 [0..]
1951 ; can_cts <- mkCanonicals flavor sc_vars
1952 ; return $ workListFromCCans can_cts
1955 inst_one pred n = newGivOrDerEvVar pred (EvSuperClass ev n)
1957 data LookupInstResult
1959 | GenInst [WantedEvVar] EvTerm
1961 matchClassInst :: Class -> [Type] -> WantedLoc -> TcS LookupInstResult
1962 matchClassInst clas tys loc
1963 = do { let pred = mkClassPred clas tys
1964 ; mb_result <- matchClass clas tys
1966 MatchInstNo -> return NoInstance
1967 MatchInstMany -> return NoInstance -- defer any reactions of a multitude until
1968 -- we learn more about the reagent
1969 MatchInstSingle (dfun_id, mb_inst_tys) ->
1970 do { checkWellStagedDFun pred dfun_id loc
1972 -- It's possible that not all the tyvars are in
1973 -- the substitution, tenv. For example:
1974 -- instance C X a => D X where ...
1975 -- (presumably there's a functional dependency in class C)
1976 -- Hence mb_inst_tys :: Either TyVar TcType
1978 ; tys <- instDFunTypes mb_inst_tys
1979 ; let (theta, _) = tcSplitPhiTy (applyTys (idType dfun_id) tys)
1980 ; if null theta then
1981 return (GenInst [] (EvDFunApp dfun_id tys []))
1983 { ev_vars <- instDFunConstraints theta
1984 ; let wevs = [WantedEvVar w loc | w <- ev_vars]
1985 ; return $ GenInst wevs (EvDFunApp dfun_id tys ev_vars) }