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**
114 , inert_cts :: Bag.Bag CanonicalCt -- Other constraints
115 , inert_fds :: FDImprovements -- List of pairwise improvements that have kicked in already
116 -- and reside either in the worklist or in the inerts
117 , inert_fsks :: Map.Map TcTyVar [(TcTyVar,Coercion)] }
118 -- See Note [InertSet FlattenSkolemEqClass]
120 type FDImprovement = (PredType,PredType)
121 type FDImprovements = [(PredType,PredType)]
123 instance Outputable InertSet where
124 ppr is = vcat [ vcat (map ppr (Bag.bagToList $ inert_eqs is))
125 , vcat (map ppr (Bag.bagToList $ inert_cts is))
126 , vcat (map (\(v,rest) -> ppr v <+> text "|->" <+> hsep (map (ppr.fst) rest))
127 (Map.toList $ inert_fsks is)
131 emptyInert :: InertSet
132 emptyInert = IS { inert_eqs = Bag.emptyBag
133 , inert_cts = Bag.emptyBag, inert_fsks = Map.empty, inert_fds = [] }
135 updInertSet :: InertSet -> AtomicInert -> InertSet
136 -- Introduces an element in the inert set for the first time
137 updInertSet (IS { inert_eqs = eqs, inert_cts = cts, inert_fsks = fsks, inert_fds = fdis })
138 item@(CTyEqCan { cc_id = cv
141 | Just tv2 <- tcGetTyVar_maybe xi,
142 FlatSkol {} <- tcTyVarDetails tv1,
143 FlatSkol {} <- tcTyVarDetails tv2
144 = let eqs' = eqs `Bag.snocBag` item
145 fsks' = Map.insertWith (++) tv2 [(tv1, mkCoVarCoercion cv)] fsks
146 -- See Note [InertSet FlattenSkolemEqClass]
147 in IS { inert_eqs = eqs', inert_cts = cts, inert_fsks = fsks', inert_fds = fdis }
148 updInertSet (IS { inert_eqs = eqs, inert_cts = cts
149 , inert_fsks = fsks, inert_fds = fdis }) item
151 = let eqs' = eqs `Bag.snocBag` item
152 in IS { inert_eqs = eqs', inert_cts = cts, inert_fsks = fsks, inert_fds = fdis }
154 = let cts' = cts `Bag.snocBag` item
155 in IS { inert_eqs = eqs, inert_cts = cts', inert_fsks = fsks, inert_fds = fdis }
157 updInertSetFDImprs :: InertSet -> Maybe FDImprovement -> InertSet
158 updInertSetFDImprs is (Just fdi) = is { inert_fds = fdi : inert_fds is }
159 updInertSetFDImprs is Nothing = is
161 foldISEqCtsM :: Monad m => (a -> AtomicInert -> m a) -> a -> InertSet -> m a
162 -- Fold over the equalities of the inerts
163 foldISEqCtsM k z IS { inert_eqs = eqs }
164 = Bag.foldlBagM k z eqs
166 foldISOtherCtsM :: Monad m => (a -> AtomicInert -> m a) -> a -> InertSet -> m a
167 -- Fold over other constraints in the inerts
168 foldISOtherCtsM k z IS { inert_cts = cts }
169 = Bag.foldlBagM k z cts
171 extractUnsolved :: InertSet -> (InertSet, CanonicalCts)
172 extractUnsolved is@(IS {inert_eqs = eqs, inert_cts = cts, inert_fds = fdis })
173 = let is_init = is { inert_eqs = emptyCCan
174 , inert_cts = solved_cts, inert_fsks = Map.empty, inert_fds = fdis }
175 is_final = Bag.foldlBag updInertSet is_init solved_eqs -- Add equalities carefully
176 in (is_final, unsolved)
177 where (unsolved_cts, solved_cts) = Bag.partitionBag isWantedCt cts
178 (unsolved_eqs, solved_eqs) = Bag.partitionBag isWantedCt eqs
179 unsolved = unsolved_cts `unionBags` unsolved_eqs
182 getFskEqClass :: InertSet -> TcTyVar -> [(TcTyVar,Coercion)]
183 -- Precondition: tv is a FlatSkol. See Note [InertSet FlattenSkolemEqClass]
184 getFskEqClass (IS { inert_cts = cts, inert_fsks = fsks }) tv
185 = case lkpTyEqCanByLhs of
186 Nothing -> fromMaybe [] (Map.lookup tv fsks)
188 case tcGetTyVar_maybe (cc_rhs ceq) of
189 Just tv_rhs | FlatSkol {} <- tcTyVarDetails tv_rhs
190 -> let ceq_co = mkSymCoercion $ mkCoVarCoercion (cc_id ceq)
191 mk_co (v,c) = (v, mkTransCoercion c ceq_co)
192 in (tv_rhs, ceq_co): map mk_co (fromMaybe [] $ Map.lookup tv fsks)
194 where lkpTyEqCanByLhs = Bag.foldlBag lkp Nothing cts
195 lkp :: Maybe CanonicalCt -> CanonicalCt -> Maybe CanonicalCt
196 lkp Nothing ct@(CTyEqCan {cc_tyvar = tv'}) | tv' == tv = Just ct
197 lkp other _ct = other
199 haveBeenImproved :: FDImprovements -> PredType -> PredType -> Bool
200 haveBeenImproved [] _ _ = False
201 haveBeenImproved ((pty1,pty2):fdimprs) pty1' pty2'
202 | tcEqPred pty1 pty1' && tcEqPred pty2 pty2'
204 | tcEqPred pty1 pty2' && tcEqPred pty2 pty1'
207 = haveBeenImproved fdimprs pty1' pty2'
209 getFDImprovements :: InertSet -> FDImprovements
210 -- Return a list of the improvements that have kicked in so far
211 getFDImprovements = inert_fds
214 isWantedCt :: CanonicalCt -> Bool
215 isWantedCt ct = isWanted (cc_flavor ct)
218 data Inert = IS { class_inerts :: FiniteMap Class Atomics
219 ip_inerts :: FiniteMap Class Atomics
220 tyfun_inerts :: FiniteMap TyCon Atomics
221 tyvar_inerts :: FiniteMap TyVar Atomics
224 Later should we also separate out givens and wanteds?
229 Note [Touchables and givens]
230 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
231 Touchable variables will never show up in givens which are inputs to
232 the solver. However, touchables may show up in givens generated by the flattener.
247 which can be put in the inert set. Suppose we also have a wanted
251 We cannot rewrite the given G alpha ~g b using the wanted alpha ~w
252 Int. Instead, after reacting alpha ~w Int with the whole inert set,
253 we observe that we can solve it by unifying alpha with Int, so we mark
254 it as solved and put it back in the *work list*. [We also immediately unify
255 alpha := Int, without telling anyone, see trySpontaneousSolve function, to
256 avoid doing this in the end.]
258 Later, because it is solved (given, in effect), we can use it to rewrite
259 G alpha ~g b to G Int ~g b, which gets put back in the work list. Eventually,
260 we will dispatch the remaining wanted constraints using the top-level axioms.
262 Finally, note that after reacting a wanted equality with the entire inert set
263 we may end up with something like
267 which we should flip around to generate the solved constraint alpha ~s b.
269 %*********************************************************************
271 * Main Interaction Solver *
273 **********************************************************************
277 1. Canonicalise (unary)
278 2. Pairwise interaction (binary)
279 * Take one from work list
280 * Try all pair-wise interactions with each constraint in inert
282 As an optimisation, we prioritize the equalities both in the
283 worklist and in the inerts.
285 3. Try to solve spontaneously for equalities involving touchables
286 4. Top-level interaction (binary wrt top-level)
287 Superclass decomposition belongs in (4), see note [Superclasses]
290 type AtomicInert = CanonicalCt -- constraint pulled from InertSet
291 type WorkItem = CanonicalCt -- constraint pulled from WorkList
293 -- A mixture of Given, Wanted, and Derived constraints.
294 -- We split between equalities and the rest to process equalities first.
295 type WorkList = CanonicalCts
296 type SWorkList = WorkList -- A worklist of solved
298 unionWorkLists :: WorkList -> WorkList -> WorkList
299 unionWorkLists = andCCan
301 isEmptyWorkList :: WorkList -> Bool
302 isEmptyWorkList = isEmptyCCan
304 emptyWorkList :: WorkList
305 emptyWorkList = emptyCCan
307 workListFromCCan :: CanonicalCt -> WorkList
308 workListFromCCan = singleCCan
310 ------------------------
312 = Stop -- Work item is consumed
313 | ContinueWith WorkItem -- Not consumed
315 instance Outputable StopOrContinue where
316 ppr Stop = ptext (sLit "Stop")
317 ppr (ContinueWith w) = ptext (sLit "ContinueWith") <+> ppr w
319 -- Results after interacting a WorkItem as far as possible with an InertSet
321 = SR { sr_inerts :: InertSet
322 -- The new InertSet to use (REPLACES the old InertSet)
323 , sr_new_work :: WorkList
324 -- Any new work items generated (should be ADDED to the old WorkList)
326 -- sr_stop = Just workitem => workitem is *not* in sr_inerts and
327 -- workitem is inert wrt to sr_inerts
328 , sr_stop :: StopOrContinue
331 instance Outputable StageResult where
332 ppr (SR { sr_inerts = inerts, sr_new_work = work, sr_stop = stop })
333 = ptext (sLit "SR") <+>
334 braces (sep [ ptext (sLit "inerts =") <+> ppr inerts <> comma
335 , ptext (sLit "new work =") <+> ppr work <> comma
336 , ptext (sLit "stop =") <+> ppr stop])
338 type SimplifierStage = WorkItem -> InertSet -> TcS StageResult
340 -- Combine a sequence of simplifier 'stages' to create a pipeline
341 runSolverPipeline :: [(String, SimplifierStage)]
342 -> InertSet -> WorkItem
343 -> TcS (InertSet, WorkList)
344 -- Precondition: non-empty list of stages
345 runSolverPipeline pipeline inerts workItem
346 = do { traceTcS "Start solver pipeline" $
347 vcat [ ptext (sLit "work item =") <+> ppr workItem
348 , ptext (sLit "inerts =") <+> ppr inerts]
350 ; let itr_in = SR { sr_inerts = inerts
351 , sr_new_work = emptyWorkList
352 , sr_stop = ContinueWith workItem }
353 ; itr_out <- run_pipeline pipeline itr_in
355 = case sr_stop itr_out of
356 Stop -> sr_inerts itr_out
357 ContinueWith item -> sr_inerts itr_out `updInertSet` item
358 ; return (new_inert, sr_new_work itr_out) }
360 run_pipeline :: [(String, SimplifierStage)]
361 -> StageResult -> TcS StageResult
362 run_pipeline [] itr = return itr
363 run_pipeline _ itr@(SR { sr_stop = Stop }) = return itr
365 run_pipeline ((name,stage):stages)
366 (SR { sr_new_work = accum_work
368 , sr_stop = ContinueWith work_item })
369 = do { itr <- stage work_item inerts
370 ; traceTcS ("Stage result (" ++ name ++ ")") (ppr itr)
371 ; let itr' = itr { sr_new_work = accum_work `unionWorkLists` sr_new_work itr }
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 ; solveInteractWithDepth (ctxtStkDepth dyn_flags,0,[]) inert ws
408 solveOne :: InertSet -> WorkItem -> TcS InertSet
409 solveOne inerts workItem
410 = do { dyn_flags <- getDynFlags
411 ; solveOneWithDepth (ctxtStkDepth dyn_flags,0,[]) inerts workItem
415 solveInteractWithDepth :: (Int, Int, [WorkItem])
416 -> InertSet -> WorkList -> TcS InertSet
417 solveInteractWithDepth ctxt@(max_depth,n,stack) inert ws
422 = solverDepthErrorTcS n stack
425 = do { traceTcS "solveInteractWithDepth" $
426 vcat [ text "Current depth =" <+> ppr n
427 , text "Max depth =" <+> ppr max_depth ]
429 -- Solve equalities first
430 ; let (eqs, non_eqs) = Bag.partitionBag isTyEqCCan ws
431 ; is_from_eqs <- Bag.foldlBagM (solveOneWithDepth ctxt) inert eqs
432 ; Bag.foldlBagM (solveOneWithDepth ctxt) is_from_eqs non_eqs }
435 -- Fully interact the given work item with an inert set, and return a
436 -- new inert set which has assimilated the new information.
437 solveOneWithDepth :: (Int, Int, [WorkItem])
438 -> InertSet -> WorkItem -> TcS InertSet
439 solveOneWithDepth (max_depth, n, stack) inert work
440 = do { traceTcS0 (indent ++ "Solving {") (ppr work)
441 ; (new_inert, new_work) <- runSolverPipeline thePipeline inert work
443 ; traceTcS0 (indent ++ "Subgoals:") (ppr new_work)
445 -- Recursively solve the new work generated
446 -- from workItem, with a greater depth
447 ; res_inert <- solveInteractWithDepth (max_depth, n+1, work:stack)
450 ; traceTcS0 (indent ++ "Done }") (ppr work)
453 indent = replicate (2*n) ' '
455 thePipeline :: [(String,SimplifierStage)]
456 thePipeline = [ ("interact with inert eqs", interactWithInertEqsStage)
457 , ("interact with inerts", interactWithInertsStage)
458 , ("spontaneous solve", spontaneousSolveStage)
459 , ("top-level reactions", topReactionsStage) ]
462 *********************************************************************************
464 The spontaneous-solve Stage
466 *********************************************************************************
469 spontaneousSolveStage :: SimplifierStage
470 spontaneousSolveStage workItem inerts
471 = do { mSolve <- trySpontaneousSolve workItem inerts
473 Nothing -> -- no spontaneous solution for him, keep going
474 return $ SR { sr_new_work = emptyWorkList
476 , sr_stop = ContinueWith workItem }
478 Just workList' -> -- He has been solved; workList' are all givens
479 return $ SR { sr_new_work = workList'
484 -- @trySpontaneousSolve wi@ solves equalities where one side is a
485 -- touchable unification variable. Returns:
486 -- * Nothing if we were not able to solve it
487 -- * Just wi' if we solved it, wi' (now a "given") should be put in the work list.
488 -- See Note [Touchables and givens]
489 -- NB: just passing the inerts through for the skolem equivalence classes
490 trySpontaneousSolve :: WorkItem -> InertSet -> TcS (Maybe SWorkList)
491 trySpontaneousSolve (CTyEqCan { cc_id = cv, cc_flavor = gw, cc_tyvar = tv1, cc_rhs = xi }) inerts
494 | Just tv2 <- tcGetTyVar_maybe xi
495 = do { tch1 <- isTouchableMetaTyVar tv1
496 ; tch2 <- isTouchableMetaTyVar tv2
497 ; case (tch1, tch2) of
498 (True, True) -> trySpontaneousEqTwoWay inerts cv gw tv1 tv2
499 (True, False) -> trySpontaneousEqOneWay inerts cv gw tv1 xi
500 (False, True) -> trySpontaneousEqOneWay inerts cv gw tv2 (mkTyVarTy tv1)
501 _ -> return Nothing }
503 = do { tch1 <- isTouchableMetaTyVar tv1
504 ; if tch1 then trySpontaneousEqOneWay inerts cv gw tv1 xi
505 else return Nothing }
508 -- trySpontaneousSolve (CFunEqCan ...) = ...
509 -- See Note [No touchables as FunEq RHS] in TcSMonad
510 trySpontaneousSolve _ _ = return Nothing
513 trySpontaneousEqOneWay :: InertSet -> CoVar -> CtFlavor -> TcTyVar -> Xi
514 -> TcS (Maybe SWorkList)
515 -- tv is a MetaTyVar, not untouchable
516 trySpontaneousEqOneWay inerts cv gw tv xi
517 | not (isSigTyVar tv) || isTyVarTy xi
518 = if typeKind xi `isSubKind` tyVarKind tv then
519 solveWithIdentity inerts cv gw tv xi
520 else if tyVarKind tv `isSubKind` typeKind xi then
521 return Nothing -- kinds are compatible but we can't solveWithIdentity this way
522 -- This case covers the a_touchable :: * ~ b_untouchable :: ??
523 -- which has to be deferred or floated out for someone else to solve
524 -- it in a scope where 'b' is no longer untouchable.
525 else kindErrorTcS gw (mkTyVarTy tv) xi -- See Note [Kind errors]
527 | otherwise -- Still can't solve, sig tyvar and non-variable rhs
531 trySpontaneousEqTwoWay :: InertSet -> CoVar -> CtFlavor -> TcTyVar -> TcTyVar
532 -> TcS (Maybe SWorkList)
533 -- Both tyvars are *touchable* MetaTyvars so there is only a chance for kind error here
534 trySpontaneousEqTwoWay inerts cv gw tv1 tv2
536 , nicer_to_update_tv2 = solveWithIdentity inerts cv gw tv2 (mkTyVarTy tv1)
538 = solveWithIdentity inerts cv gw tv1 (mkTyVarTy tv2)
539 | otherwise -- None is a subkind of the other, but they are both touchable!
540 = kindErrorTcS gw (mkTyVarTy tv1) (mkTyVarTy tv2) -- See Note [Kind errors]
544 nicer_to_update_tv2 = isSigTyVar tv1 || isSystemName (Var.varName tv2)
548 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
549 Consider the wanted problem:
550 alpha ~ (# Int, Int #)
551 where alpha :: ?? and (# Int, Int #) :: (#). We can't spontaneously solve this constraint,
552 but we should rather reject the program that give rise to it. If 'trySpontaneousEqTwoWay'
553 simply returns @Nothing@ then that wanted constraint is going to propagate all the way and
554 get quantified over in inference mode. That's bad because we do know at this point that the
555 constraint is insoluble. Instead, we call 'kindErrorTcS' here, which immediately fails.
557 The same applies in canonicalization code in case of kind errors in the givens.
559 Note [Spontaneous solving and kind compatibility]
560 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
562 Note that our canonical constraints insist that only *given* equalities (tv ~ xi)
563 or (F xis ~ rhs) require the LHS and the RHS to have exactly the same kinds.
565 - We have to require this because:
566 Given equalities can be freely used to rewrite inside
567 other types or constraints.
568 - We do not have to do the same for wanteds because:
569 First, wanted equations (tv ~ xi) where tv is a touchable
570 unification variable may have kinds that do not agree (the
571 kind of xi must be a sub kind of the kind of tv). Second, any
572 potential kind mismatch will result in the constraint not
573 being soluble, which will be reported anyway. This is the
574 reason that @trySpontaneousOneWay@ and @trySpontaneousTwoWay@
575 will perform a kind compatibility check, and only then will
576 they proceed to @solveWithIdentity@.
579 - Givens from higher-rank, such as:
580 type family T b :: * -> * -> *
581 type instance T Bool = (->)
583 f :: forall a. ((T a ~ (->)) => ...) -> a -> ...
585 Whereas we would be able to apply the type instance, we would not be able to
586 use the given (T Bool ~ (->)) in the body of 'flop'
588 Note [Loopy spontaneous solving]
589 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
590 Consider the original wanted:
591 wanted : Maybe (E alpha) ~ alpha
592 where E is a type family, such that E (T x) = x. After canonicalization,
593 as a result of flattening, we will get:
594 given : E alpha ~ fsk
595 wanted : alpha ~ Maybe fsk
596 where (fsk := E alpha, on the side). Now, if we spontaneously *solve*
597 (alpha := Maybe fsk) we are in trouble! Instead, we should refrain from solving
598 it and keep it as wanted. In inference mode we'll end up quantifying over
599 (alpha ~ Maybe (E alpha))
600 Hence, 'solveWithIdentity' performs a small occurs check before
601 actually solving. But this occurs check *must look through* flatten skolems.
603 However, it may be the case that the flatten skolem in hand is equal to some other
604 flatten skolem whith *does not* mention our unification variable. Here's a typical example:
609 After canonicalization:
614 After some reactions:
619 At this point, we will try to spontaneously solve (alpha ~ f2) which remains as yet unsolved.
620 We will look inside f2, which immediately mentions (F alpha), so it's not good to unify! However
621 by looking at the equivalence class of the flatten skolems, we can see that it is fine to
622 unify (alpha ~ f1) which solves our goals!
624 A similar problem happens because of other spontaneous solving. Suppose we have the
625 following wanteds, arriving in this exact order:
626 (first) w: beta ~ alpha
627 (second) w: alpha ~ fsk
628 (third) g: F beta ~ fsk
629 Then, we first spontaneously solve the first constraint, making (beta := alpha), and having
630 (beta ~ alpha) as given. *Then* we encounter the second wanted (alpha ~ fsk). "fsk" does not
631 obviously mention alpha, so naively we can also spontaneously solve (alpha := fsk). But
632 that is wrong since fsk mentions beta, which has already secretly been unified to alpha!
634 To avoid this problem, the same occurs check must unveil rewritings that can happen because
635 of spontaneously having solved other constraints.
638 Note [Avoid double unifications]
639 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
640 The spontaneous solver has to return a given which mentions the unified unification
641 variable *on the left* of the equality. Here is what happens if not:
642 Original wanted: (a ~ alpha), (alpha ~ Int)
643 We spontaneously solve the first wanted, without changing the order!
644 given : a ~ alpha [having unified alpha := a]
645 Now the second wanted comes along, but he cannot rewrite the given, so we simply continue.
646 At the end we spontaneously solve that guy, *reunifying* [alpha := Int]
648 We avoid this problem by orienting the given so that the unification
649 variable is on the left. [Note that alternatively we could attempt to
650 enforce this at canonicalization]
652 See also Note [No touchables as FunEq RHS] in TcSMonad; avoiding
653 double unifications is the main reason we disallow touchable
654 unification variables as RHS of type family equations: F xis ~ alpha.
658 solveWithIdentity :: InertSet
659 -> CoVar -> CtFlavor -> TcTyVar -> Xi
660 -> TcS (Maybe SWorkList)
661 -- Solve with the identity coercion
662 -- Precondition: kind(xi) is a sub-kind of kind(tv)
663 -- Precondition: CtFlavor is Wanted or Derived
664 -- See [New Wanted Superclass Work] to see why solveWithIdentity
665 -- must work for Derived as well as Wanted
666 solveWithIdentity inerts cv gw tv xi
667 = do { tybnds <- getTcSTyBindsMap
668 ; case occurCheck tybnds inerts tv xi of
669 Nothing -> return Nothing
670 Just (xi_unflat,coi) -> solve_with xi_unflat coi }
672 solve_with xi_unflat coi -- coi : xi_unflat ~ xi
673 = do { traceTcS "Sneaky unification:" $
674 vcat [text "Coercion variable: " <+> ppr gw,
675 text "Coercion: " <+> pprEq (mkTyVarTy tv) xi,
676 text "Left Kind is : " <+> ppr (typeKind (mkTyVarTy tv)),
677 text "Right Kind is : " <+> ppr (typeKind xi)
679 ; setWantedTyBind tv xi_unflat -- Set tv := xi_unflat
680 ; cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi_unflat xi_unflat
681 ; let flav = mkGivenFlavor gw UnkSkol
682 ; (cts, co) <- case coi of
683 ACo co -> do { can_eqs <- canEq flav cv_given (mkTyVarTy tv) xi_unflat
684 ; return (can_eqs, co) }
686 (singleCCan (CTyEqCan { cc_id = cv_given
687 , cc_flavor = mkGivenFlavor gw UnkSkol
688 , cc_tyvar = tv, cc_rhs = xi }
689 -- xi, *not* xi_unflat because
690 -- xi_unflat may require flattening!
693 Wanted {} -> setWantedCoBind cv co
694 Derived {} -> setDerivedCoBind cv co
695 _ -> pprPanic "Can't spontaneously solve *given*" empty
696 -- See Note [Avoid double unifications]
697 ; return $ Just cts }
699 occurCheck :: VarEnv (TcTyVar, TcType) -> InertSet
700 -> TcTyVar -> TcType -> Maybe (TcType,CoercionI)
701 -- Traverse @ty@ to make sure that @tv@ does not appear under some flatten skolem.
702 -- If it appears under some flatten skolem look in that flatten skolem equivalence class
703 -- (see Note [InertSet FlattenSkolemEqClass], [Loopy Spontaneous Solving]) to see if you
704 -- can find a different flatten skolem to use, that is, one that does not mention @tv@.
706 -- Postcondition: Just (ty', coi) = occurCheck binds inerts tv ty
708 -- NB: The returned type ty' may not be flat!
710 occurCheck ty_binds inerts the_tv the_ty
711 = ok emptyVarSet the_ty
713 -- If (fsk `elem` bad) then tv occurs in any rendering
714 -- of the type under the expansion of fsk
715 ok bad this_ty@(TyConApp tc tys)
716 | Just tys_cois <- allMaybes (map (ok bad) tys)
717 , (tys',cois') <- unzip tys_cois
718 = Just (TyConApp tc tys', mkTyConAppCoI tc cois')
719 | isSynTyCon tc, Just ty_expanded <- tcView this_ty
720 = ok bad ty_expanded -- See Note [Type synonyms and the occur check] in TcUnify
722 | Just (sty',coi) <- ok_pred bad sty
723 = Just (PredTy sty', coi)
724 ok bad (FunTy arg res)
725 | Just (arg', coiarg) <- ok bad arg, Just (res', coires) <- ok bad res
726 = Just (FunTy arg' res', mkFunTyCoI coiarg coires)
727 ok bad (AppTy fun arg)
728 | Just (fun', coifun) <- ok bad fun, Just (arg', coiarg) <- ok bad arg
729 = Just (AppTy fun' arg', mkAppTyCoI coifun coiarg)
730 ok bad (ForAllTy tv1 ty1)
731 -- WARNING: What if it is a (t1 ~ t2) => t3? It's not handled properly at the moment.
732 | Just (ty1', coi) <- ok bad ty1
733 = Just (ForAllTy tv1 ty1', mkForAllTyCoI tv1 coi)
736 ok bad this_ty@(TyVarTy tv)
737 | tv == the_tv = Nothing -- Occurs check error
738 | not (isTcTyVar tv) = Just (this_ty, IdCo this_ty) -- Bound var
739 | FlatSkol zty <- tcTyVarDetails tv = ok_fsk bad tv zty
740 | Just (_,ty) <- lookupVarEnv ty_binds tv = ok bad ty
741 | otherwise = Just (this_ty, IdCo this_ty)
743 -- Check if there exists a ty bind already, as a result of sneaky unification.
745 ok _bad _ty = Nothing
748 ok_pred bad (ClassP cn tys)
749 | Just tys_cois <- allMaybes $ map (ok bad) tys
750 = let (tys', cois') = unzip tys_cois
751 in Just (ClassP cn tys', mkClassPPredCoI cn cois')
752 ok_pred bad (IParam nm ty)
753 | Just (ty',co') <- ok bad ty
754 = Just (IParam nm ty', mkIParamPredCoI nm co')
755 ok_pred bad (EqPred ty1 ty2)
756 | Just (ty1',coi1) <- ok bad ty1, Just (ty2',coi2) <- ok bad ty2
757 = Just (EqPred ty1' ty2', mkEqPredCoI coi1 coi2)
758 ok_pred _ _ = Nothing
762 | fsk `elemVarSet` bad
763 -- We are already trying to find a rendering of fsk,
764 -- and to do that it seems we need a rendering, so fail
767 = firstJusts (ok new_bad zty : map (go_under_fsk new_bad) fsk_equivs)
769 fsk_equivs = getFskEqClass inerts fsk
770 new_bad = bad `extendVarSetList` (fsk : map fst fsk_equivs)
773 go_under_fsk bad_tvs (fsk,co)
774 | FlatSkol zty <- tcTyVarDetails fsk
775 = case ok bad_tvs zty of
777 Just (ty,coi') -> Just (ty, mkTransCoI coi' (ACo co))
778 | otherwise = pprPanic "go_down_equiv" (ppr fsk)
782 *********************************************************************************
784 The interact-with-inert Stage
786 *********************************************************************************
789 -- Interaction result of WorkItem <~> AtomicInert
791 = IR { ir_stop :: StopOrContinue
793 -- => Reagent (work item) consumed.
794 -- ContinueWith new_reagent
795 -- => Reagent transformed but keep gathering interactions.
796 -- The transformed item remains inert with respect
797 -- to any previously encountered inerts.
799 , ir_inert_action :: InertAction
800 -- Whether the inert item should remain in the InertSet.
802 , ir_new_work :: WorkList
803 -- new work items to add to the WorkList
805 , ir_improvement :: Maybe FDImprovement -- In case improvement kicked in
808 -- What to do with the inert reactant.
809 data InertAction = KeepInert | DropInert
812 mkIRContinue :: Monad m => WorkItem -> InertAction -> WorkList -> m InteractResult
813 mkIRContinue wi keep newWork = return $ IR (ContinueWith wi) keep newWork Nothing
815 mkIRStop :: Monad m => InertAction -> WorkList -> m InteractResult
816 mkIRStop keep newWork = return $ IR Stop keep newWork Nothing
818 mkIRStop_RecordImprovement :: Monad m => InertAction -> WorkList -> FDImprovement -> m InteractResult
819 mkIRStop_RecordImprovement keep newWork fdimpr = return $ IR Stop keep newWork (Just fdimpr)
822 dischargeWorkItem :: Monad m => m InteractResult
823 dischargeWorkItem = mkIRStop KeepInert emptyWorkList
825 noInteraction :: Monad m => WorkItem -> m InteractResult
826 noInteraction workItem = mkIRContinue workItem KeepInert emptyWorkList
828 data WhichComesFromInert = LeftComesFromInert | RightComesFromInert
831 ---------------------------------------------------
832 -- Interact a single WorkItem with the equalities of an inert set as far as possible, i.e. until we
833 -- get a Stop result from an individual reaction (i.e. when the WorkItem is consumed), or until we've
834 -- interact the WorkItem with the entire equalities of the InertSet
836 interactWithInertEqsStage :: SimplifierStage
837 interactWithInertEqsStage workItem inert
838 = foldISEqCtsM interactNext initITR inert
839 where initITR = SR { sr_inerts = IS { inert_eqs = emptyCCan -- We will fold over the equalities
840 , inert_fsks = Map.empty -- which will generate those two again
841 , inert_cts = inert_cts inert
842 , inert_fds = inert_fds inert
844 , sr_new_work = emptyWorkList
845 , sr_stop = ContinueWith workItem }
848 ---------------------------------------------------
849 -- Interact a single WorkItem with *non-equality* constraints in the inert set.
850 -- Precondition: equality interactions must have already happened, hence we have
851 -- to pick up some information from the incoming inert, before folding over the
852 -- "Other" constraints it contains!
853 interactWithInertsStage :: SimplifierStage
854 interactWithInertsStage workItem inert
855 = foldISOtherCtsM interactNext initITR inert
857 initITR = SR { -- Pick up: (1) equations, (2) FD improvements, (3) FlatSkol equiv. classes
858 sr_inerts = IS { inert_eqs = inert_eqs inert
859 , inert_cts = emptyCCan
860 , inert_fds = inert_fds inert
861 , inert_fsks = inert_fsks inert }
862 , sr_new_work = emptyWorkList
863 , sr_stop = ContinueWith workItem }
865 interactNext :: StageResult -> AtomicInert -> TcS StageResult
866 interactNext it inert
867 | ContinueWith workItem <- sr_stop it
868 = do { let inerts = sr_inerts it
869 fdimprs_old = getFDImprovements inerts
871 ; ir <- interactWithInert fdimprs_old inert workItem
873 -- New inerts depend on whether we KeepInert or not and must
874 -- be updated with FD improvement information from the interaction result (ir)
875 ; let inerts_new = updInertSetFDImprs upd_inert (ir_improvement ir)
876 upd_inert = if ir_inert_action ir == KeepInert
877 then inerts `updInertSet` inert else inerts
879 ; return $ SR { sr_inerts = inerts_new
880 , sr_new_work = sr_new_work it `unionWorkLists` ir_new_work ir
881 , sr_stop = ir_stop ir } }
883 = return $ it { sr_inerts = (sr_inerts it) `updInertSet` inert }
885 -- Do a single interaction of two constraints.
886 interactWithInert :: FDImprovements -> AtomicInert -> WorkItem -> TcS InteractResult
887 interactWithInert fdimprs inert workitem
888 = do { ctxt <- getTcSContext
889 ; let is_allowed = allowedInteraction (simplEqsOnly ctxt) inert workitem
890 inert_ev = cc_id inert
891 work_ev = cc_id workitem
893 -- Never interact a wanted and a derived where the derived's evidence
894 -- mentions the wanted evidence in an unguarded way.
895 -- See Note [Superclasses and recursive dictionaries]
896 -- and Note [New Wanted Superclass Work]
897 -- We don't have to do this for givens, as we fully know the evidence for them.
899 case (cc_flavor inert, cc_flavor workitem) of
900 (Wanted loc, Derived {}) -> isGoodRecEv work_ev (WantedEvVar inert_ev loc)
901 (Derived {}, Wanted loc) -> isGoodRecEv inert_ev (WantedEvVar work_ev loc)
904 ; if is_allowed && rec_ev_ok then
905 doInteractWithInert fdimprs inert workitem
907 noInteraction workitem
910 allowedInteraction :: Bool -> AtomicInert -> WorkItem -> Bool
911 -- Allowed interactions
912 allowedInteraction eqs_only (CDictCan {}) (CDictCan {}) = not eqs_only
913 allowedInteraction eqs_only (CIPCan {}) (CIPCan {}) = not eqs_only
914 allowedInteraction _ _ _ = True
916 --------------------------------------------
917 doInteractWithInert :: FDImprovements -> CanonicalCt -> CanonicalCt -> TcS InteractResult
918 -- Identical class constraints.
920 doInteractWithInert fdimprs
921 (CDictCan { cc_id = d1, cc_flavor = fl1, cc_class = cls1, cc_tyargs = tys1 })
922 workItem@(CDictCan { cc_id = d2, cc_flavor = fl2, cc_class = cls2, cc_tyargs = tys2 })
923 | cls1 == cls2 && (and $ zipWith tcEqType tys1 tys2)
924 = solveOneFromTheOther (d1,fl1) workItem
926 | cls1 == cls2 && (not (isGiven fl1 && isGiven fl2))
927 = -- See Note [When improvement happens]
928 do { let pty1 = ClassP cls1 tys1
929 pty2 = ClassP cls2 tys2
930 work_item_pred_loc = (pty2, ppr d2)
931 inert_pred_loc = (pty1, ppr d1)
932 loc = combineCtLoc fl1 fl2
933 eqn_pred_locs = improveFromAnother work_item_pred_loc inert_pred_loc
935 ; wevvars <- mkWantedFunDepEqns loc eqn_pred_locs
936 ; fd_work <- canWanteds wevvars
937 -- See Note [Generating extra equalities]
938 ; traceTcS "Checking if improvements existed." (ppr fdimprs)
939 ; if isEmptyWorkList fd_work || haveBeenImproved fdimprs pty1 pty2 then
941 mkIRContinue workItem KeepInert fd_work
942 else do { traceTcS "Recording improvement and throwing item back in worklist." (ppr (pty1,pty2))
943 ; mkIRStop_RecordImprovement KeepInert
944 (fd_work `unionWorkLists` workListFromCCan workItem) (pty1,pty2)
946 -- See Note [FunDep Reactions]
949 -- Class constraint and given equality: use the equality to rewrite
950 -- the class constraint.
951 doInteractWithInert _fdimprs
952 (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi })
953 (CDictCan { cc_id = dv, cc_flavor = wfl, cc_class = cl, cc_tyargs = xis })
954 | ifl `canRewrite` wfl
955 , tv `elemVarSet` tyVarsOfTypes xis
956 = if isDerivedSC wfl then
957 mkIRStop KeepInert $ emptyWorkList -- See Note [Adding Derived Superclasses]
958 else do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,wfl,cl,xis)
959 -- Continue with rewritten Dictionary because we can only be in the
960 -- interactWithEqsStage, so the dictionary is inert.
961 ; mkIRContinue rewritten_dict KeepInert emptyWorkList }
963 doInteractWithInert _fdimprs
964 (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 = if isDerivedSC ifl then
969 mkIRContinue workItem DropInert emptyWorkList -- No need to do any rewriting,
970 -- see Note [Adding Derived Superclasses]
971 else do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,ifl,cl,xis)
972 ; mkIRContinue workItem DropInert (workListFromCCan rewritten_dict) }
974 -- Class constraint and given equality: use the equality to rewrite
975 -- the class constraint.
976 doInteractWithInert _fdimprs
977 (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi })
978 (CIPCan { cc_id = ipid, cc_flavor = wfl, cc_ip_nm = nm, cc_ip_ty = ty })
979 | ifl `canRewrite` wfl
980 , tv `elemVarSet` tyVarsOfType ty
981 = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,wfl,nm,ty)
982 ; mkIRContinue rewritten_ip KeepInert emptyWorkList }
984 doInteractWithInert _fdimprs
985 (CIPCan { cc_id = ipid, cc_flavor = ifl, cc_ip_nm = nm, cc_ip_ty = ty })
986 workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
987 | wfl `canRewrite` ifl
988 , tv `elemVarSet` tyVarsOfType ty
989 = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,ifl,nm,ty)
990 ; mkIRContinue workItem DropInert (workListFromCCan rewritten_ip) }
992 -- Two implicit parameter constraints. If the names are the same,
993 -- but their types are not, we generate a wanted type equality
994 -- that equates the type (this is "improvement").
995 -- However, we don't actually need the coercion evidence,
996 -- so we just generate a fresh coercion variable that isn't used anywhere.
997 doInteractWithInert _fdimprs
998 (CIPCan { cc_id = id1, cc_flavor = ifl, cc_ip_nm = nm1, cc_ip_ty = ty1 })
999 workItem@(CIPCan { cc_flavor = wfl, cc_ip_nm = nm2, cc_ip_ty = ty2 })
1000 | nm1 == nm2 && isGiven wfl && isGiven ifl
1001 = -- See Note [Overriding implicit parameters]
1002 -- Dump the inert item, override totally with the new one
1003 -- Do not require type equality
1004 mkIRContinue workItem DropInert emptyWorkList
1006 | nm1 == nm2 && ty1 `tcEqType` ty2
1007 = solveOneFromTheOther (id1,ifl) workItem
1010 = -- See Note [When improvement happens]
1011 do { co_var <- newWantedCoVar ty1 ty2
1012 ; let flav = Wanted (combineCtLoc ifl wfl)
1013 ; cans <- mkCanonical flav co_var
1014 ; mkIRContinue workItem KeepInert cans }
1017 -- Inert: equality, work item: function equality
1019 -- Never rewrite a given with a wanted equality, and a type function
1020 -- equality can never rewrite an equality. Note also that if we have
1021 -- F x1 ~ x2 and a ~ x3, and a occurs in x2, we don't rewrite it. We
1022 -- can wait until F x1 ~ x2 matches another F x1 ~ x4, and only then
1023 -- we will ``expose'' x2 and x4 to rewriting.
1025 -- Otherwise, we can try rewriting the type function equality with the equality.
1026 doInteractWithInert _fdimprs
1027 (CTyEqCan { cc_id = cv1, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi1 })
1028 (CFunEqCan { cc_id = cv2, cc_flavor = wfl, cc_fun = tc
1029 , cc_tyargs = args, cc_rhs = xi2 })
1030 | ifl `canRewrite` wfl
1031 , tv `elemVarSet` tyVarsOfTypes args
1032 = do { rewritten_funeq <- rewriteFunEq (cv1,tv,xi1) (cv2,wfl,tc,args,xi2)
1033 ; mkIRStop KeepInert (workListFromCCan rewritten_funeq) }
1034 -- must Stop here, because we may no longer be inert after the rewritting.
1036 -- Inert: function equality, work item: equality
1037 doInteractWithInert _fdimprs
1038 (CFunEqCan {cc_id = cv1, cc_flavor = ifl, cc_fun = tc
1039 , cc_tyargs = args, cc_rhs = xi1 })
1040 workItem@(CTyEqCan { cc_id = cv2, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi2 })
1041 | wfl `canRewrite` ifl
1042 , tv `elemVarSet` tyVarsOfTypes args
1043 = do { rewritten_funeq <- rewriteFunEq (cv2,tv,xi2) (cv1,ifl,tc,args,xi1)
1044 ; mkIRContinue workItem DropInert (workListFromCCan rewritten_funeq) }
1046 doInteractWithInert _fdimprs
1047 (CFunEqCan { cc_id = cv1, cc_flavor = fl1, cc_fun = tc1
1048 , cc_tyargs = args1, cc_rhs = xi1 })
1049 workItem@(CFunEqCan { cc_id = cv2, cc_flavor = fl2, cc_fun = tc2
1050 , cc_tyargs = args2, cc_rhs = xi2 })
1051 | fl1 `canSolve` fl2 && lhss_match
1052 = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
1053 ; mkIRStop KeepInert cans }
1054 | fl2 `canSolve` fl1 && lhss_match
1055 = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
1056 ; mkIRContinue workItem DropInert cans }
1058 lhss_match = tc1 == tc2 && and (zipWith tcEqType args1 args2)
1060 doInteractWithInert _fdimprs
1061 inert@(CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
1062 workItem@(CTyEqCan { cc_id = cv2, cc_flavor = fl2, cc_tyvar = tv2, cc_rhs = xi2 })
1063 -- Check for matching LHS
1064 | fl1 `canSolve` fl2 && tv1 == tv2
1065 = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
1066 ; mkIRStop KeepInert cans }
1068 | fl2 `canSolve` fl1 && tv1 == tv2
1069 = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
1070 ; mkIRContinue workItem DropInert cans }
1072 -- Check for rewriting RHS
1073 | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfType xi2
1074 = do { rewritten_eq <- rewriteEqRHS (cv1,tv1,xi1) (cv2,fl2,tv2,xi2)
1075 ; mkIRStop KeepInert rewritten_eq }
1076 | fl2 `canRewrite` fl1 && tv2 `elemVarSet` tyVarsOfType xi1
1077 = do { rewritten_eq <- rewriteEqRHS (cv2,tv2,xi2) (cv1,fl1,tv1,xi1)
1078 ; mkIRContinue workItem DropInert rewritten_eq }
1080 -- Finally, if workitem is a Flatten Equivalence Class constraint and the
1081 -- inert is a wanted constraint, even when the workitem cannot rewrite the
1082 -- inert, drop the inert out because you may have to reconsider solving the
1083 -- inert *using* the equivalence class you created. See note [Loopy Spontaneous Solving]
1084 -- and [InertSet FlattenSkolemEqClass]
1086 | not $ isGiven fl1, -- The inert is wanted or derived
1087 isMetaTyVar tv1, -- and has a unification variable lhs
1088 FlatSkol {} <- tcTyVarDetails tv2, -- And workitem is a flatten skolem equality
1089 Just tv2' <- tcGetTyVar_maybe xi2, FlatSkol {} <- tcTyVarDetails tv2'
1090 = mkIRContinue workItem DropInert (workListFromCCan inert)
1093 -- Fall-through case for all other situations
1094 doInteractWithInert _fdimprs _ workItem = noInteraction workItem
1096 -------------------------
1097 -- Equational Rewriting
1098 rewriteDict :: (CoVar, TcTyVar, Xi) -> (DictId, CtFlavor, Class, [Xi]) -> TcS CanonicalCt
1099 rewriteDict (cv,tv,xi) (dv,gw,cl,xis)
1100 = do { let cos = substTysWith [tv] [mkCoVarCoercion cv] xis -- xis[tv] ~ xis[xi]
1101 args = substTysWith [tv] [xi] xis
1103 dict_co = mkTyConCoercion con cos
1104 ; dv' <- newDictVar cl args
1106 Wanted {} -> setDictBind dv (EvCast dv' (mkSymCoercion dict_co))
1107 _given_or_derived -> setDictBind dv' (EvCast dv dict_co)
1108 ; return (CDictCan { cc_id = dv'
1111 , cc_tyargs = args }) }
1113 rewriteIP :: (CoVar,TcTyVar,Xi) -> (EvVar,CtFlavor, IPName Name, TcType) -> TcS CanonicalCt
1114 rewriteIP (cv,tv,xi) (ipid,gw,nm,ty)
1115 = do { let ip_co = substTyWith [tv] [mkCoVarCoercion cv] ty -- ty[tv] ~ t[xi]
1116 ty' = substTyWith [tv] [xi] ty
1117 ; ipid' <- newIPVar nm ty'
1119 Wanted {} -> setIPBind ipid (EvCast ipid' (mkSymCoercion ip_co))
1120 _given_or_derived -> setIPBind ipid' (EvCast ipid ip_co)
1121 ; return (CIPCan { cc_id = ipid'
1124 , cc_ip_ty = ty' }) }
1126 rewriteFunEq :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TyCon, [Xi], Xi) -> TcS CanonicalCt
1127 rewriteFunEq (cv1,tv,xi1) (cv2,gw, tc,args,xi2)
1128 = do { let arg_cos = substTysWith [tv] [mkCoVarCoercion cv1] args
1129 args' = substTysWith [tv] [xi1] args
1130 fun_co = mkTyConCoercion tc arg_cos
1131 ; cv2' <- case gw of
1132 Wanted {} -> do { cv2' <- newWantedCoVar (mkTyConApp tc args') xi2
1133 ; setWantedCoBind cv2 $
1134 mkTransCoercion fun_co (mkCoVarCoercion cv2')
1136 _giv_or_der -> newGivOrDerCoVar (mkTyConApp tc args') xi2 $
1137 mkTransCoercion (mkSymCoercion fun_co) (mkCoVarCoercion cv2)
1138 ; return (CFunEqCan { cc_id = cv2'
1145 rewriteEqRHS :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TcTyVar,Xi) -> TcS WorkList
1146 -- Use the first equality to rewrite the second, flavors already checked.
1147 -- E.g. c1 : tv1 ~ xi1 c2 : tv2 ~ xi2
1148 -- rewrites c2 to give
1149 -- c2' : tv2 ~ xi2[xi1/tv1]
1150 -- We must do an occurs check to sure the new constraint is canonical
1151 -- So we might return an empty bag
1152 rewriteEqRHS (cv1,tv1,xi1) (cv2,gw,tv2,xi2)
1153 | Just tv2' <- tcGetTyVar_maybe xi2'
1154 , tv2 == tv2' -- In this case xi2[xi1/tv1] = tv2, so we have tv2~tv2
1155 = do { when (isWanted gw) (setWantedCoBind cv2 (mkSymCoercion co2'))
1156 ; return emptyCCan }
1161 -> do { cv2' <- newWantedCoVar (mkTyVarTy tv2) xi2'
1162 ; setWantedCoBind cv2 $
1163 mkCoVarCoercion cv2' `mkTransCoercion` mkSymCoercion co2'
1166 -> newGivOrDerCoVar (mkTyVarTy tv2) xi2' $
1167 mkCoVarCoercion cv2 `mkTransCoercion` co2'
1169 ; xi2'' <- canOccursCheck gw tv2 xi2' -- we know xi2' is *not* tv2
1170 ; return (singleCCan $ CTyEqCan { cc_id = cv2'
1176 xi2' = substTyWith [tv1] [xi1] xi2
1177 co2' = substTyWith [tv1] [mkCoVarCoercion cv1] xi2 -- xi2 ~ xi2[xi1/tv1]
1180 rewriteEqLHS :: WhichComesFromInert -> (Coercion,Xi) -> (CoVar,CtFlavor,Xi) -> TcS WorkList
1181 -- Used to ineract two equalities of the following form:
1182 -- First Equality: co1: (XXX ~ xi1)
1183 -- Second Equality: cv2: (XXX ~ xi2)
1184 -- Where the cv1 `canSolve` cv2 equality
1185 -- We have an option of creating new work (xi1 ~ xi2) OR (xi2 ~ xi1). This
1186 -- depends on whether the left or the right equality comes from the inert set.
1188 -- prefer to create (xi2 ~ xi1) if the first comes from the inert
1189 -- prefer to create (xi1 ~ xi2) if the second comes from the inert
1190 rewriteEqLHS which (co1,xi1) (cv2,gw,xi2)
1191 = do { cv2' <- case (isWanted gw, which) of
1192 (True,LeftComesFromInert) ->
1193 do { cv2' <- newWantedCoVar xi2 xi1
1194 ; setWantedCoBind cv2 $
1195 co1 `mkTransCoercion` mkSymCoercion (mkCoVarCoercion cv2')
1197 (True,RightComesFromInert) ->
1198 do { cv2' <- newWantedCoVar xi1 xi2
1199 ; setWantedCoBind cv2 $
1200 co1 `mkTransCoercion` mkCoVarCoercion cv2'
1202 (False,LeftComesFromInert) ->
1203 newGivOrDerCoVar xi2 xi1 $
1204 mkSymCoercion (mkCoVarCoercion cv2) `mkTransCoercion` co1
1205 (False,RightComesFromInert) ->
1206 newGivOrDerCoVar xi1 xi2 $
1207 mkSymCoercion co1 `mkTransCoercion` mkCoVarCoercion cv2
1208 ; mkCanonical gw cv2'
1211 solveOneFromTheOther :: (EvVar, CtFlavor) -> CanonicalCt -> TcS InteractResult
1212 -- First argument inert, second argument workitem. They both represent
1213 -- wanted/given/derived evidence for the *same* predicate so we try here to
1214 -- discharge one directly from the other.
1216 -- Precondition: value evidence only (implicit parameters, classes)
1218 solveOneFromTheOther (iid,ifl) workItem
1219 -- Both derived needs a special case. You might think that we do not need
1220 -- two evidence terms for the same claim. But, since the evidence is partial,
1221 -- either evidence may do in some cases; see TcSMonad.isGoodRecEv.
1222 -- See also Example 3 in Note [Superclasses and recursive dictionaries]
1223 | isDerived ifl && isDerived wfl
1224 = noInteraction workItem
1226 | ifl `canSolve` wfl
1227 = do { unless (isGiven wfl) $ setEvBind wid (EvId iid)
1228 -- Overwrite the binding, if one exists
1229 -- For Givens, which are lambda-bound, nothing to overwrite,
1230 ; dischargeWorkItem }
1232 | otherwise -- wfl `canSolve` ifl
1233 = do { unless (isGiven ifl) $ setEvBind iid (EvId wid)
1234 ; mkIRContinue workItem DropInert emptyWorkList }
1237 wfl = cc_flavor workItem
1238 wid = cc_id workItem
1241 Note [Superclasses and recursive dictionaries]
1242 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1243 Overlaps with Note [SUPERCLASS-LOOP 1]
1244 Note [SUPERCLASS-LOOP 2]
1245 Note [Recursive instances and superclases]
1246 ToDo: check overlap and delete redundant stuff
1248 Right before adding a given into the inert set, we must
1249 produce some more work, that will bring the superclasses
1250 of the given into scope. The superclass constraints go into
1253 When we simplify a wanted constraint, if we first see a matching
1254 instance, we may produce new wanted work. To (1) avoid doing this work
1255 twice in the future and (2) to handle recursive dictionaries we may ``cache''
1256 this item as solved (in effect, given) into our inert set and with that add
1257 its superclass constraints (as given) in our worklist.
1259 But now we have added partially solved constraints to the worklist which may
1260 interact with other wanteds. Consider the example:
1264 class Eq b => Foo a b --- 0-th selector
1265 instance Eq a => Foo [a] a --- fooDFun
1267 and wanted (Foo [t] t). We are first going to see that the instance matches
1268 and create an inert set that includes the solved (Foo [t] t) and its
1270 d1 :_g Foo [t] t d1 := EvDFunApp fooDFun d3
1271 d2 :_g Eq t d2 := EvSuperClass d1 0
1272 Our work list is going to contain a new *wanted* goal
1274 It is wrong to react the wanted (Eq t) with the given (Eq t) because that would
1275 construct loopy evidence. Hence the check isGoodRecEv in doInteractWithInert.
1277 OK, so we have ruled out bad behaviour, but how do we ge recursive dictionaries,
1282 data D r = ZeroD | SuccD (r (D r));
1284 instance (Eq (r (D r))) => Eq (D r) where
1285 ZeroD == ZeroD = True
1286 (SuccD a) == (SuccD b) = a == b
1289 equalDC :: D [] -> D [] -> Bool;
1292 We need to prove (Eq (D [])). Here's how we go:
1296 by instance decl, holds if
1300 *BUT* we have an inert set which gives us (no superclasses):
1302 By the instance declaration of Eq we can show the 'd2' goal if
1304 where d2 = dfEqList d3
1306 Now, however this wanted can interact with our inert d1 to set:
1308 and solve the goal. Why was this interaction OK? Because, if we chase the
1309 evidence of d1 ~~> dfEqD d2 ~~-> dfEqList d3, so by setting d3 := d1 we
1311 d3 := dfEqD2 (dfEqList d3)
1312 which is FINE because the use of d3 is protected by the instance function
1315 So, our strategy is to try to put solved wanted dictionaries into the
1316 inert set along with their superclasses (when this is meaningful,
1317 i.e. when new wanted goals are generated) but solve a wanted dictionary
1318 from a given only in the case where the evidence variable of the
1319 wanted is mentioned in the evidence of the given (recursively through
1320 the evidence binds) in a protected way: more instance function applications
1321 than superclass selectors.
1323 Here are some more examples from GHC's previous type checker
1327 This code arises in the context of "Scrap Your Boilerplate with Class"
1331 instance Sat (ctx Char) => Data ctx Char -- dfunData1
1332 instance (Sat (ctx [a]), Data ctx a) => Data ctx [a] -- dfunData2
1334 class Data Maybe a => Foo a
1336 instance Foo t => Sat (Maybe t) -- dfunSat
1338 instance Data Maybe a => Foo a -- dfunFoo1
1339 instance Foo a => Foo [a] -- dfunFoo2
1340 instance Foo [Char] -- dfunFoo3
1342 Consider generating the superclasses of the instance declaration
1343 instance Foo a => Foo [a]
1345 So our problem is this
1347 d1 :_w Data Maybe [t]
1349 We may add the given in the inert set, along with its superclasses
1350 [assuming we don't fail because there is a matching instance, see
1351 tryTopReact, given case ]
1355 d01 :_g Data Maybe t -- d2 := EvDictSuperClass d0 0
1356 d1 :_w Data Maybe [t]
1357 Then d2 can readily enter the inert, and we also do solving of the wanted
1360 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1362 d2 :_w Sat (Maybe [t])
1364 d01 :_g Data Maybe t
1365 Now, we may simplify d2 more:
1368 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1369 d1 :_g Data Maybe [t]
1370 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1374 d01 :_g Data Maybe t
1376 Now, we can just solve d3.
1379 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1380 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1383 d01 :_g Data Maybe t
1384 And now we can simplify d4 again, but since it has superclasses we *add* them to the worklist:
1387 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1388 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1389 d4 :_g Foo [t] d4 := dfunFoo2 d5
1392 d6 :_g Data Maybe [t] d6 := EvDictSuperClass d4 0
1393 d01 :_g Data Maybe t
1394 Now, d5 can be solved! (and its superclass enter scope)
1397 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1398 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1399 d4 :_g Foo [t] d4 := dfunFoo2 d5
1400 d5 :_g Foo t d5 := dfunFoo1 d7
1403 d6 :_g Data Maybe [t]
1404 d8 :_g Data Maybe t d8 := EvDictSuperClass d5 0
1405 d01 :_g Data Maybe t
1408 [1] Suppose we pick d8 and we react him with d01. Which of the two givens should
1409 we keep? Well, we *MUST NOT* drop d01 because d8 contains recursive evidence
1410 that must not be used (look at case interactInert where both inert and workitem
1411 are givens). So we have several options:
1412 - Drop the workitem always (this will drop d8)
1413 This feels very unsafe -- what if the work item was the "good" one
1414 that should be used later to solve another wanted?
1415 - Don't drop anyone: the inert set may contain multiple givens!
1416 [This is currently implemented]
1418 The "don't drop anyone" seems the most safe thing to do, so now we come to problem 2:
1419 [2] We have added both d6 and d01 in the inert set, and we are interacting our wanted
1420 d7. Now the [isRecDictEv] function in the ineration solver
1421 [case inert-given workitem-wanted] will prevent us from interacting d7 := d8
1422 precisely because chasing the evidence of d8 leads us to an unguarded use of d7.
1424 So, no interaction happens there. Then we meet d01 and there is no recursion
1425 problem there [isRectDictEv] gives us the OK to interact and we do solve d7 := d01!
1427 Note [SUPERCLASS-LOOP 1]
1428 ~~~~~~~~~~~~~~~~~~~~~~~~
1429 We have to be very, very careful when generating superclasses, lest we
1430 accidentally build a loop. Here's an example:
1434 class S a => C a where { opc :: a -> a }
1435 class S b => D b where { opd :: b -> b }
1437 instance C Int where
1440 instance D Int where
1443 From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int}
1444 Simplifying, we may well get:
1445 $dfCInt = :C ds1 (opd dd)
1448 Notice that we spot that we can extract ds1 from dd.
1450 Alas! Alack! We can do the same for (instance D Int):
1452 $dfDInt = :D ds2 (opc dc)
1456 And now we've defined the superclass in terms of itself.
1457 Two more nasty cases are in
1462 - Satisfy the superclass context *all by itself*
1463 (tcSimplifySuperClasses)
1464 - And do so completely; i.e. no left-over constraints
1465 to mix with the constraints arising from method declarations
1468 Note [SUPERCLASS-LOOP 2]
1469 ~~~~~~~~~~~~~~~~~~~~~~~~
1470 We need to be careful when adding "the constaint we are trying to prove".
1471 Suppose we are *given* d1:Ord a, and want to deduce (d2:C [a]) where
1473 class Ord a => C a where
1474 instance Ord [a] => C [a] where ...
1476 Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the
1477 superclasses of C [a] to avails. But we must not overwrite the binding
1478 for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
1481 Here's another variant, immortalised in tcrun020
1482 class Monad m => C1 m
1483 class C1 m => C2 m x
1484 instance C2 Maybe Bool
1485 For the instance decl we need to build (C1 Maybe), and it's no good if
1486 we run around and add (C2 Maybe Bool) and its superclasses to the avails
1487 before we search for C1 Maybe.
1489 Here's another example
1490 class Eq b => Foo a b
1491 instance Eq a => Foo [a] a
1495 we'll first deduce that it holds (via the instance decl). We must not
1496 then overwrite the Eq t constraint with a superclass selection!
1498 At first I had a gross hack, whereby I simply did not add superclass constraints
1499 in addWanted, though I did for addGiven and addIrred. This was sub-optimal,
1500 becuase it lost legitimate superclass sharing, and it still didn't do the job:
1501 I found a very obscure program (now tcrun021) in which improvement meant the
1502 simplifier got two bites a the cherry... so something seemed to be an Stop
1503 first time, but reducible next time.
1505 Now we implement the Right Solution, which is to check for loops directly
1506 when adding superclasses. It's a bit like the occurs check in unification.
1508 Note [Recursive instances and superclases]
1509 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1510 Consider this code, which arises in the context of "Scrap Your
1511 Boilerplate with Class".
1515 instance Sat (ctx Char) => Data ctx Char
1516 instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]
1518 class Data Maybe a => Foo a
1520 instance Foo t => Sat (Maybe t)
1522 instance Data Maybe a => Foo a
1523 instance Foo a => Foo [a]
1526 In the instance for Foo [a], when generating evidence for the superclasses
1527 (ie in tcSimplifySuperClasses) we need a superclass (Data Maybe [a]).
1528 Using the instance for Data, we therefore need
1529 (Sat (Maybe [a], Data Maybe a)
1530 But we are given (Foo a), and hence its superclass (Data Maybe a).
1531 So that leaves (Sat (Maybe [a])). Using the instance for Sat means
1532 we need (Foo [a]). And that is the very dictionary we are bulding
1533 an instance for! So we must put that in the "givens". So in this
1535 Given: Foo a, Foo [a]
1536 Wanted: Data Maybe [a]
1538 BUT we must *not not not* put the *superclasses* of (Foo [a]) in
1539 the givens, which is what 'addGiven' would normally do. Why? Because
1540 (Data Maybe [a]) is the superclass, so we'd "satisfy" the wanted
1541 by selecting a superclass from Foo [a], which simply makes a loop.
1543 On the other hand we *must* put the superclasses of (Foo a) in
1544 the givens, as you can see from the derivation described above.
1546 Conclusion: in the very special case of tcSimplifySuperClasses
1547 we have one 'given' (namely the "this" dictionary) whose superclasses
1548 must not be added to 'givens' by addGiven.
1550 There is a complication though. Suppose there are equalities
1551 instance (Eq a, a~b) => Num (a,b)
1552 Then we normalise the 'givens' wrt the equalities, so the original
1553 given "this" dictionary is cast to one of a different type. So it's a
1554 bit trickier than before to identify the "special" dictionary whose
1555 superclasses must not be added. See test
1556 indexed-types/should_run/EqInInstance
1558 We need a persistent property of the dictionary to record this
1559 special-ness. Current I'm using the InstLocOrigin (a bit of a hack,
1560 but cool), which is maintained by dictionary normalisation.
1561 Specifically, the InstLocOrigin is
1563 then the no-superclass thing kicks in. WATCH OUT if you fiddle
1566 Note [MATCHING-SYNONYMS]
1567 ~~~~~~~~~~~~~~~~~~~~~~~~
1568 When trying to match a dictionary (D tau) to a top-level instance, or a
1569 type family equation (F taus_1 ~ tau_2) to a top-level family instance,
1570 we do *not* need to expand type synonyms because the matcher will do that for us.
1573 Note [RHS-FAMILY-SYNONYMS]
1574 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1575 The RHS of a family instance is represented as yet another constructor which is
1576 like a type synonym for the real RHS the programmer declared. Eg:
1577 type instance F (a,a) = [a]
1579 :R32 a = [a] -- internal type synonym introduced
1580 F (a,a) ~ :R32 a -- instance
1582 When we react a family instance with a type family equation in the work list
1583 we keep the synonym-using RHS without expansion.
1586 *********************************************************************************
1588 The top-reaction Stage
1590 *********************************************************************************
1593 -- If a work item has any form of interaction with top-level we get this
1594 data TopInteractResult
1595 = NoTopInt -- No top-level interaction
1597 { tir_new_work :: WorkList -- Sub-goals or new work (could be given,
1598 -- for superclasses)
1599 , tir_new_inert :: StopOrContinue -- The input work item, ready to become *inert* now:
1600 } -- NB: in ``given'' (solved) form if the
1601 -- original was wanted or given and instance match
1602 -- was found, but may also be in wanted form if we
1603 -- only reacted with functional dependencies
1604 -- arising from top-level instances.
1606 topReactionsStage :: SimplifierStage
1607 topReactionsStage workItem inerts
1608 = do { tir <- tryTopReact workItem
1611 return $ SR { sr_inerts = inerts
1612 , sr_new_work = emptyWorkList
1613 , sr_stop = ContinueWith workItem }
1614 SomeTopInt tir_new_work tir_new_inert ->
1615 return $ SR { sr_inerts = inerts
1616 , sr_new_work = tir_new_work
1617 , sr_stop = tir_new_inert
1621 tryTopReact :: WorkItem -> TcS TopInteractResult
1622 tryTopReact workitem
1623 = do { -- A flag controls the amount of interaction allowed
1624 -- See Note [Simplifying RULE lhs constraints]
1625 ctxt <- getTcSContext
1626 ; if allowedTopReaction (simplEqsOnly ctxt) workitem
1627 then do { traceTcS "tryTopReact / calling doTopReact" (ppr workitem)
1628 ; doTopReact workitem }
1629 else return NoTopInt
1632 allowedTopReaction :: Bool -> WorkItem -> Bool
1633 allowedTopReaction eqs_only (CDictCan {}) = not eqs_only
1634 allowedTopReaction _ _ = True
1637 doTopReact :: WorkItem -> TcS TopInteractResult
1638 -- The work item does not react with the inert set,
1639 -- so try interaction with top-level instances
1641 -- Given dictionary; just add superclasses
1642 -- See Note [Given constraint that matches an instance declaration]
1643 doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Given loc
1644 , cc_class = cls, cc_tyargs = xis })
1645 = do { sc_work <- newGivenSCWork dv loc cls xis
1646 ; return $ SomeTopInt sc_work (ContinueWith workItem) }
1648 -- Derived dictionary
1649 -- Do not add any further derived superclasses; their
1650 -- full transitive closure has already been added.
1651 -- But do look for functional dependencies
1652 doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Derived loc _
1653 , cc_class = cls, cc_tyargs = xis })
1654 = do { fd_work <- findClassFunDeps dv cls xis loc
1655 ; if isEmptyWorkList fd_work then
1657 else return $ SomeTopInt { tir_new_work = fd_work
1658 , tir_new_inert = ContinueWith workItem } }
1660 doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Wanted loc
1661 , cc_class = cls, cc_tyargs = xis })
1662 = do { -- See Note [MATCHING-SYNONYMS]
1663 ; lkp_inst_res <- matchClassInst cls xis loc
1664 ; case lkp_inst_res of
1666 do { traceTcS "doTopReact/ no class instance for" (ppr dv)
1667 ; fd_work <- findClassFunDeps dv cls xis loc
1668 ; if isEmptyWorkList fd_work then
1669 do { sc_work <- newDerivedSCWork dv loc cls xis
1670 -- See Note [Adding Derived Superclasses]
1671 -- NB: workItem is inert, but it isn't solved
1672 -- keep it as inert, although it's not solved
1673 -- because we have now reacted all its
1674 -- top-level fundep-induced equalities!
1675 ; return $ SomeTopInt
1676 { tir_new_work = fd_work `unionWorkLists` sc_work
1677 , tir_new_inert = ContinueWith workItem } }
1679 else -- More fundep work produced, don't do any superclass stuff,
1680 -- just thow him back in the worklist, which will prioritize
1681 -- the solution of fd equalities
1683 { tir_new_work = fd_work `unionWorkLists`
1684 workListFromCCan workItem
1685 , tir_new_inert = Stop } }
1687 GenInst wtvs ev_term -> -- Solved
1688 -- No need to do fundeps stuff here; the instance
1689 -- matches already so we won't get any more info
1690 -- from functional dependencies
1691 do { traceTcS "doTopReact/ found class instance for" (ppr dv)
1692 ; setDictBind dv ev_term
1693 ; inst_work <- canWanteds wtvs
1695 -- Solved in one step and no new wanted work produced.
1696 -- i.e we directly matched a top-level instance
1697 -- No point in caching this in 'inert', nor in adding superclasses
1698 then return $ SomeTopInt { tir_new_work = emptyWorkList
1699 , tir_new_inert = Stop }
1701 -- Solved and new wanted work produced, you may cache the
1702 -- (tentatively solved) dictionary as Derived and its superclasses
1703 else do { let solved = makeSolvedByInst workItem
1704 ; sc_work <- newDerivedSCWork dv loc cls xis
1705 -- See Note [Adding Derived Superclasses]
1706 ; return $ SomeTopInt
1707 { tir_new_work = inst_work `unionWorkLists` sc_work
1708 , tir_new_inert = ContinueWith solved } }
1712 doTopReact (CFunEqCan { cc_id = cv, cc_flavor = fl
1713 , cc_fun = tc, cc_tyargs = args, cc_rhs = xi })
1714 = ASSERT (isSynFamilyTyCon tc) -- No associated data families have reached that far
1715 do { match_res <- matchFam tc args -- See Note [MATCHING-SYNONYMS]
1719 MatchInstSingle (rep_tc, rep_tys)
1720 -> do { let Just coe_tc = tyConFamilyCoercion_maybe rep_tc
1721 Just rhs_ty = tcView (mkTyConApp rep_tc rep_tys)
1722 -- Eagerly expand away the type synonym on the
1723 -- RHS of a type function, so that it never
1724 -- appears in an error message
1725 -- See Note [Type synonym families] in TyCon
1726 coe = mkTyConApp coe_tc rep_tys
1728 Wanted {} -> do { cv' <- newWantedCoVar rhs_ty xi
1729 ; setWantedCoBind cv $
1730 coe `mkTransCoercion`
1733 _ -> newGivOrDerCoVar xi rhs_ty $
1734 mkSymCoercion (mkCoVarCoercion cv) `mkTransCoercion` coe
1736 ; can_cts <- mkCanonical fl cv'
1737 ; return $ SomeTopInt can_cts Stop }
1739 -> panicTcS $ text "TcSMonad.matchFam returned multiple instances!"
1743 -- Any other work item does not react with any top-level equations
1744 doTopReact _workItem = return NoTopInt
1746 ----------------------
1747 findClassFunDeps :: EvVar -> Class -> [Xi] -> WantedLoc -> TcS WorkList
1748 -- Look for a fundep reaction beween the wanted item
1749 -- and a top-level instance declaration
1750 findClassFunDeps dv cls xis loc
1751 = do { instEnvs <- getInstEnvs
1752 ; let eqn_pred_locs = improveFromInstEnv (classInstances instEnvs)
1753 (ClassP cls xis, ppr dv)
1754 ; wevvars <- mkWantedFunDepEqns loc eqn_pred_locs
1755 -- NB: fundeps generate some wanted equalities, but
1756 -- we don't use their evidence for anything
1757 ; canWanteds wevvars }
1760 Note [Adding Derived Superclasses]
1761 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1762 Generally speaking, we want to be able to add derived superclasses of
1763 unsolved wanteds, and wanteds that have been partially being solved
1764 via an instance. This is important to be able to simplify the inferred
1765 constraints more (and to allow for recursive dictionaries, less
1766 importantly). Example:
1768 Inferred wanted constraint is (Eq a, Ord a), but we'd only like to
1769 quantify over Ord a, hence we would like to be able to add the
1770 superclass of Ord a as Derived and use it to solve the wanted Eq a.
1772 Hence we will add Derived superclasses in the following two cases:
1773 (1) When we meet an unsolved wanted in top-level reactions
1774 (2) When we partially solve a wanted in top-level reactions using an instance decl.
1776 At that point, we have two options:
1777 (1) Add transitively add *ALL* of the superclasses of the Derived
1778 (2) Add only the immediate ones, but whenever we meet a Derived in
1779 the future, add its own superclasses as Derived.
1781 Option (2) is terrible, because deriveds may be rewritten or kicked
1782 out of the inert set, which will result in slightly rewritten
1783 superclasses being reintroduced in the worklist and the inert set. Eg:
1786 instance Foo a => B [a]
1788 Original constraints:
1790 [Given] co : a ~ Int
1792 We apply the instance to the wanted and put it and its superclasses as
1793 as Deriveds in the inerts:
1796 [Derived] (sel d) : C [a]
1799 [Given] co : a ~ Int
1802 Now, suppose that we interact the Derived with the Given equality, and
1803 kick him out of the inert, the next time around a superclass C [Int]
1804 will be produced -- but we already *have* C [a] in the inerts which
1805 will anyway get rewritten to C [Int].
1807 So we choose (1), and *never* introduce any more superclass work from
1808 Deriveds. This enables yet another optimisation: If we ever meet an
1809 equality that can rewrite a Derived, if that Derived is a superclass
1810 derived (like C [a] above), i.e. not a partially solved one (like B
1811 [a]) above, we may simply completely *discard* that Derived. The
1812 reason is because somewhere in the inert lies the original wanted, or
1813 partially solved constraint that gave rise to that superclass, and
1814 that constraint *will* be kicked out, and *will* result in the
1815 rewritten superclass to be added in the inerts later on, anyway.
1819 Note [FunDep and implicit parameter reactions]
1820 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1821 Currently, our story of interacting two dictionaries (or a dictionary
1822 and top-level instances) for functional dependencies, and implicit
1823 paramters, is that we simply produce new wanted equalities. So for example
1825 class D a b | a -> b where ...
1831 We generate the extra work item
1833 where 'cv' is currently unused. However, this new item reacts with d2,
1834 discharging it in favour of a new constraint d2' thus:
1836 d2 := d2' |> D Int cv
1837 Now d2' can be discharged from d1
1839 We could be more aggressive and try to *immediately* solve the dictionary
1840 using those extra equalities. With the same inert set and work item we
1841 might dischard d2 directly:
1844 d2 := d1 |> D Int cv
1846 But in general it's a bit painful to figure out the necessary coercion,
1847 so we just take the first approach. Here is a better example. Consider:
1848 class C a b c | a -> b
1850 [Given] d1 : C T Int Char
1851 [Wanted] d2 : C T beta Int
1852 In this case, it's *not even possible* to solve the wanted immediately.
1853 So we should simply output the functional dependency and add this guy
1854 [but NOT its superclasses] back in the worklist. Even worse:
1855 [Given] d1 : C T Int beta
1856 [Wanted] d2: C T beta Int
1857 Then it is solvable, but its very hard to detect this on the spot.
1859 It's exactly the same with implicit parameters, except that the
1860 "aggressive" approach would be much easier to implement.
1862 Note [When improvement happens]
1863 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1864 We fire an improvement rule when
1866 * Two constraints match (modulo the fundep)
1867 e.g. C t1 t2, C t1 t3 where C a b | a->b
1868 The two match because the first arg is identical
1870 * At least one is not Given. If they are both given, we don't fire
1871 the reaction because we have no way of constructing evidence for a
1872 new equality nor does it seem right to create a new wanted goal
1873 (because the goal will most likely contain untouchables, which
1874 can't be solved anyway)!
1876 Note that we *do* fire the improvement if one is Given and one is Derived.
1877 The latter can be a superclass of a wanted goal. Example (tcfail138)
1878 class L a b | a -> b
1879 class (G a, L a b) => C a b
1881 instance C a b' => G (Maybe a)
1882 instance C a b => C (Maybe a) a
1883 instance L (Maybe a) a
1885 When solving the superclasses of the (C (Maybe a) a) instance, we get
1886 Given: C a b ... and hance by superclasses, (G a, L a b)
1888 Use the instance decl to get
1890 The (C a b') is inert, so we generate its Derived superclasses (L a b'),
1891 and now we need improvement between that derived superclass an the Given (L a b)
1893 Note [Overriding implicit parameters]
1894 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1896 f :: (?x::a) -> Bool -> a
1898 g v = let ?x::Int = 3
1899 in (f v, let ?x::Bool = True in f v)
1901 This should probably be well typed, with
1902 g :: Bool -> (Int, Bool)
1904 So the inner binding for ?x::Bool *overrides* the outer one.
1905 Hence a work-item Given overrides an inert-item Given.
1907 Note [Given constraint that matches an instance declaration]
1908 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1909 What should we do when we discover that one (or more) top-level
1910 instances match a given (or solved) class constraint? We have
1913 1. Reject the program. The reason is that there may not be a unique
1914 best strategy for the solver. Example, from the OutsideIn(X) paper:
1915 instance P x => Q [x]
1916 instance (x ~ y) => R [x] y
1918 wob :: forall a b. (Q [b], R b a) => a -> Int
1920 g :: forall a. Q [a] => [a] -> Int
1923 will generate the impliation constraint:
1924 Q [a] => (Q [beta], R beta [a])
1925 If we react (Q [beta]) with its top-level axiom, we end up with a
1926 (P beta), which we have no way of discharging. On the other hand,
1927 if we react R beta [a] with the top-level we get (beta ~ a), which
1928 is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
1929 now solvable by the given Q [a].
1931 However, this option is restrictive, for instance [Example 3] from
1932 Note [Recursive dictionaries] will fail to work.
1934 2. Ignore the problem, hoping that the situations where there exist indeed
1935 such multiple strategies are rare: Indeed the cause of the previous
1936 problem is that (R [x] y) yields the new work (x ~ y) which can be
1937 *spontaneously* solved, not using the givens.
1939 We are choosing option 2 below but we might consider having a flag as well.
1942 Note [New Wanted Superclass Work]
1943 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1944 Even in the case of wanted constraints, we add all of its superclasses as
1945 new given work. There are several reasons for this:
1946 a) to minimise error messages;
1947 eg suppose we have wanted (Eq a, Ord a)
1948 then we report only (Ord a) unsoluble
1950 b) to make the smallest number of constraints when *inferring* a type
1951 (same Eq/Ord example)
1953 c) for recursive dictionaries we *must* add the superclasses
1954 so that we can use them when solving a sub-problem
1956 d) To allow FD-like improvement for type families. Assume that
1958 class C a b | a -> b
1959 and we have to solve the implication constraint:
1961 Then, FD improvement can help us to produce a new wanted (beta ~ b)
1963 We want to have the same effect with the type family encoding of
1964 functional dependencies. Namely, consider:
1965 class (F a ~ b) => C a b
1966 Now suppose that we have:
1969 By interacting the given we will get given (F a ~ b) which is not
1970 enough by itself to make us discharge (C a beta). However, we
1971 may create a new derived equality from the super-class of the
1972 wanted constraint (C a beta), namely derived (F a ~ beta).
1973 Now we may interact this with given (F a ~ b) to get:
1975 But 'beta' is a touchable unification variable, and hence OK to
1976 unify it with 'b', replacing the derived evidence with the identity.
1978 This requires trySpontaneousSolve to solve *derived*
1979 equalities that have a touchable in their RHS, *in addition*
1980 to solving wanted equalities.
1982 Here is another example where this is useful.
1986 class (F a ~ b) => C a b
1987 And we are given the wanteds:
1991 We surely do *not* want to quantify over (b ~ c), since if someone provides
1992 dictionaries for (C a b) and (C a c), these dictionaries can provide a proof
1993 of (b ~ c), hence no extra evidence is necessary. Here is what will happen:
1995 Step 1: We will get new *given* superclass work,
1996 provisionally to our solving of w1 and w2
1998 g1: F a ~ b, g2 : F a ~ c,
1999 w1 : C a b, w2 : C a c, w3 : b ~ c
2001 The evidence for g1 and g2 is a superclass evidence term:
2003 g1 := sc w1, g2 := sc w2
2005 Step 2: The givens will solve the wanted w3, so that
2006 w3 := sym (sc w1) ; sc w2
2008 Step 3: Now, one may naively assume that then w2 can be solve from w1
2009 after rewriting with the (now solved equality) (b ~ c).
2011 But this rewriting is ruled out by the isGoodRectDict!
2013 Conclusion, we will (correctly) end up with the unsolved goals
2016 NB: The desugarer needs be more clever to deal with equalities
2017 that participate in recursive dictionary bindings.
2021 newGivenSCWork :: EvVar -> GivenLoc -> Class -> [Xi] -> TcS WorkList
2022 newGivenSCWork ev loc cls xis
2023 | NoScSkol <- ctLocOrigin loc -- Very important!
2024 = return emptyWorkList
2026 = newImmSCWorkFromFlavored ev (Given loc) cls xis >>= return
2028 newDerivedSCWork :: EvVar -> WantedLoc -> Class -> [Xi] -> TcS WorkList
2029 newDerivedSCWork ev loc cls xis
2030 = do { ims <- newImmSCWorkFromFlavored ev flavor cls xis
2033 rec_sc_work :: CanonicalCts -> TcS CanonicalCts
2035 = do { bg <- mapBagM (\c -> do { ims <- imm_sc_work c
2036 ; recs_ims <- rec_sc_work ims
2037 ; return $ consBag c recs_ims }) cts
2038 ; return $ concatBag bg }
2039 imm_sc_work (CDictCan { cc_id = dv, cc_flavor = fl, cc_class = cls, cc_tyargs = xis })
2040 = newImmSCWorkFromFlavored dv fl cls xis
2041 imm_sc_work _ct = return emptyCCan
2043 flavor = Derived loc DerSC
2045 newImmSCWorkFromFlavored :: EvVar -> CtFlavor -> Class -> [Xi] -> TcS WorkList
2046 -- Returns immediate superclasses
2047 newImmSCWorkFromFlavored ev flavor cls xis
2048 = do { let (tyvars, sc_theta, _, _) = classBigSig cls
2049 sc_theta1 = substTheta (zipTopTvSubst tyvars xis) sc_theta
2050 ; sc_vars <- zipWithM inst_one sc_theta1 [0..]
2051 ; mkCanonicals flavor sc_vars }
2053 inst_one pred n = newGivOrDerEvVar pred (EvSuperClass ev n)
2056 data LookupInstResult
2058 | GenInst [WantedEvVar] EvTerm
2060 matchClassInst :: Class -> [Type] -> WantedLoc -> TcS LookupInstResult
2061 matchClassInst clas tys loc
2062 = do { let pred = mkClassPred clas tys
2063 ; mb_result <- matchClass clas tys
2065 MatchInstNo -> return NoInstance
2066 MatchInstMany -> return NoInstance -- defer any reactions of a multitude until
2067 -- we learn more about the reagent
2068 MatchInstSingle (dfun_id, mb_inst_tys) ->
2069 do { checkWellStagedDFun pred dfun_id loc
2071 -- It's possible that not all the tyvars are in
2072 -- the substitution, tenv. For example:
2073 -- instance C X a => D X where ...
2074 -- (presumably there's a functional dependency in class C)
2075 -- Hence mb_inst_tys :: Either TyVar TcType
2077 ; tys <- instDFunTypes mb_inst_tys
2078 ; let (theta, _) = tcSplitPhiTy (applyTys (idType dfun_id) tys)
2079 ; if null theta then
2080 return (GenInst [] (EvDFunApp dfun_id tys []))
2082 { ev_vars <- instDFunConstraints theta
2083 ; let wevs = [WantedEvVar w loc | w <- ev_vars]
2084 ; return $ GenInst wevs (EvDFunApp dfun_id tys ev_vars) }