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]
291 type AtomicInert = CanonicalCt -- constraint pulled from InertSet
292 type WorkItem = CanonicalCt -- constraint pulled from WorkList
294 -- A mixture of Given, Wanted, and Derived constraints.
295 -- We split between equalities and the rest to process equalities first.
296 data WorkList = WL { wl_eqs :: CanonicalCts -- Equalities (CTyEqCan, CFunEqCan)
297 , wl_other :: CanonicalCts -- Other
299 type SWorkList = WorkList -- A worklist of solved
301 unionWorkLists :: WorkList -> WorkList -> WorkList
302 unionWorkLists wl1 wl2
303 = WL { wl_eqs = andCCan (wl_eqs wl1) (wl_eqs wl2)
304 , wl_other = andCCan (wl_other wl1) (wl_other wl2) }
306 foldWorkListEqCtsM :: Monad m => (a -> WorkItem -> m a) -> a -> WorkList -> m a
307 -- Fold over the equalities of a worklist
308 foldWorkListEqCtsM f r wl = Bag.foldlBagM f r (wl_eqs wl)
310 foldWorkListOtherCtsM :: Monad m => (a -> WorkItem -> m a) -> a -> WorkList -> m a
311 -- Fold over non-equality constraints of a worklist
312 foldWorkListOtherCtsM f r wl = Bag.foldlBagM f r (wl_other wl)
314 isEmptyWorkList :: WorkList -> Bool
315 isEmptyWorkList wl = isEmptyCCan (wl_eqs wl) && isEmptyCCan (wl_other wl)
317 emptyWorkList :: WorkList
318 emptyWorkList = WL { wl_eqs = emptyCCan, wl_other = emptyCCan }
320 workListFromCCans :: CanonicalCts -> WorkList
321 -- Generic, no precondition
322 workListFromCCans cts = WL eqs others
323 where (eqs, others) = Bag.partitionBag isTyEqCCan cts
325 workListFromCCan :: CanonicalCt -> WorkList
326 workListFromCCan ct | isTyEqCCan ct = WL (singleCCan ct) emptyCCan
327 | otherwise = WL emptyCCan (singleCCan ct)
329 -- At the call sites of workListFromCCan(s), sometimes we know whether the new work
330 -- involves equalities or not. It's probably a good idea to add specialized calls for
331 -- those, to avoid asking whether 'isTyEqCCan' all the time.
335 = Stop -- Work item is consumed
336 | ContinueWith WorkItem -- Not consumed
338 instance Outputable StopOrContinue where
339 ppr Stop = ptext (sLit "Stop")
340 ppr (ContinueWith w) = ptext (sLit "ContinueWith") <+> ppr w
342 -- Results after interacting a WorkItem as far as possible with an InertSet
344 = SR { sr_inerts :: InertSet
345 -- The new InertSet to use (REPLACES the old InertSet)
346 , sr_new_work :: WorkList
347 -- Any new work items generated (should be ADDED to the old WorkList)
349 -- sr_stop = Just workitem => workitem is *not* in sr_inerts and
350 -- workitem is inert wrt to sr_inerts
351 , sr_stop :: StopOrContinue
354 instance Outputable StageResult where
355 ppr (SR { sr_inerts = inerts, sr_new_work = work, sr_stop = stop })
356 = ptext (sLit "SR") <+>
357 braces (sep [ ptext (sLit "inerts =") <+> ppr inerts <> comma
358 , ptext (sLit "new work =") <+> ppr work <> comma
359 , ptext (sLit "stop =") <+> ppr stop])
361 instance Outputable WorkList where
362 ppr (WL eqcts othercts) = vcat [ppr eqcts, ppr othercts]
364 type SimplifierStage = WorkItem -> InertSet -> TcS StageResult
366 -- Combine a sequence of simplifier 'stages' to create a pipeline
367 runSolverPipeline :: [(String, SimplifierStage)]
368 -> InertSet -> WorkItem
369 -> TcS (InertSet, WorkList)
370 -- Precondition: non-empty list of stages
371 runSolverPipeline pipeline inerts workItem
372 = do { traceTcS "Start solver pipeline" $
373 vcat [ ptext (sLit "work item =") <+> ppr workItem
374 , ptext (sLit "inerts =") <+> ppr inerts]
376 ; let itr_in = SR { sr_inerts = inerts
377 , sr_new_work = emptyWorkList
378 , sr_stop = ContinueWith workItem }
379 ; itr_out <- run_pipeline pipeline itr_in
381 = case sr_stop itr_out of
382 Stop -> sr_inerts itr_out
383 ContinueWith item -> sr_inerts itr_out `updInertSet` item
384 ; return (new_inert, sr_new_work itr_out) }
386 run_pipeline :: [(String, SimplifierStage)]
387 -> StageResult -> TcS StageResult
388 run_pipeline [] itr = return itr
389 run_pipeline _ itr@(SR { sr_stop = Stop }) = return itr
391 run_pipeline ((name,stage):stages)
392 (SR { sr_new_work = accum_work
394 , sr_stop = ContinueWith work_item })
395 = do { itr <- stage work_item inerts
396 ; traceTcS ("Stage result (" ++ name ++ ")") (ppr itr)
397 ; let itr' = itr { sr_new_work = accum_work `unionWorkLists` sr_new_work itr }
398 ; run_pipeline stages itr' }
402 Inert: {c ~ d, F a ~ t, b ~ Int, a ~ ty} (all given)
403 Reagent: a ~ [b] (given)
405 React with (c~d) ==> IR (ContinueWith (a~[b])) True []
406 React with (F a ~ t) ==> IR (ContinueWith (a~[b])) False [F [b] ~ t]
407 React with (b ~ Int) ==> IR (ContinueWith (a~[Int]) True []
410 Inert: {c ~w d, F a ~g t, b ~w Int, a ~w ty}
413 React with (c ~w d) ==> IR (ContinueWith (a~[b])) True []
414 React with (F a ~g t) ==> IR (ContinueWith (a~[b])) True [] (can't rewrite given with wanted!)
418 Inert: {a ~ Int, F Int ~ b} (given)
419 Reagent: F a ~ b (wanted)
421 React with (a ~ Int) ==> IR (ContinueWith (F Int ~ b)) True []
422 React with (F Int ~ b) ==> IR Stop True [] -- after substituting we re-canonicalize and get nothing
425 -- Main interaction solver: we fully solve the worklist 'in one go',
426 -- returning an extended inert set.
428 -- See Note [Touchables and givens].
429 solveInteract :: InertSet -> CanonicalCts -> TcS InertSet
430 solveInteract inert ws
431 = do { dyn_flags <- getDynFlags
432 ; let worklist = workListFromCCans ws
433 ; solveInteractWithDepth (ctxtStkDepth dyn_flags,0,[]) inert worklist
435 solveOne :: InertSet -> WorkItem -> TcS InertSet
436 solveOne inerts workItem
437 = do { dyn_flags <- getDynFlags
438 ; solveOneWithDepth (ctxtStkDepth dyn_flags,0,[]) inerts workItem
442 solveInteractWithDepth :: (Int, Int, [WorkItem])
443 -> InertSet -> WorkList -> TcS InertSet
444 solveInteractWithDepth ctxt@(max_depth,n,stack) inert ws
449 = solverDepthErrorTcS n stack
452 = do { traceTcS "solveInteractWithDepth" $
453 vcat [ text "Current depth =" <+> ppr n
454 , text "Max depth =" <+> ppr max_depth
456 ; is_from_eqs <- foldWorkListEqCtsM (solveOneWithDepth ctxt) inert ws
457 ; foldWorkListOtherCtsM (solveOneWithDepth ctxt) is_from_eqs ws
461 -- Fully interact the given work item with an inert set, and return a
462 -- new inert set which has assimilated the new information.
463 solveOneWithDepth :: (Int, Int, [WorkItem])
464 -> InertSet -> WorkItem -> TcS InertSet
465 solveOneWithDepth (max_depth, n, stack) inert work
466 = do { traceTcS0 (indent ++ "Solving {") (ppr work)
467 ; (new_inert, new_work) <- runSolverPipeline thePipeline inert work
469 ; traceTcS0 (indent ++ "Subgoals:") (ppr new_work)
471 -- Recursively solve the new work generated
472 -- from workItem, with a greater depth
473 ; res_inert <- solveInteractWithDepth (max_depth, n+1, work:stack)
476 ; traceTcS0 (indent ++ "Done }") (ppr work)
479 indent = replicate (2*n) ' '
481 thePipeline :: [(String,SimplifierStage)]
482 thePipeline = [ ("interact with inert eqs", interactWithInertEqsStage)
483 , ("interact with inerts", interactWithInertsStage)
484 , ("spontaneous solve", spontaneousSolveStage)
485 , ("top-level reactions", topReactionsStage) ]
488 *********************************************************************************
490 The spontaneous-solve Stage
492 *********************************************************************************
495 spontaneousSolveStage :: SimplifierStage
496 spontaneousSolveStage workItem inerts
497 = do { mSolve <- trySpontaneousSolve workItem inerts
499 Nothing -> -- no spontaneous solution for him, keep going
500 return $ SR { sr_new_work = emptyWorkList
502 , sr_stop = ContinueWith workItem }
504 Just workList' -> -- He has been solved; workList' are all givens
505 return $ SR { sr_new_work = workList'
510 -- @trySpontaneousSolve wi@ solves equalities where one side is a
511 -- touchable unification variable. Returns:
512 -- * Nothing if we were not able to solve it
513 -- * Just wi' if we solved it, wi' (now a "given") should be put in the work list.
514 -- See Note [Touchables and givens]
515 -- NB: just passing the inerts through for the skolem equivalence classes
516 trySpontaneousSolve :: WorkItem -> InertSet -> TcS (Maybe SWorkList)
517 trySpontaneousSolve (CTyEqCan { cc_id = cv, cc_flavor = gw, cc_tyvar = tv1, cc_rhs = xi }) inerts
520 | Just tv2 <- tcGetTyVar_maybe xi
521 = do { tch1 <- isTouchableMetaTyVar tv1
522 ; tch2 <- isTouchableMetaTyVar tv2
523 ; case (tch1, tch2) of
524 (True, True) -> trySpontaneousEqTwoWay inerts cv gw tv1 tv2
525 (True, False) -> trySpontaneousEqOneWay inerts cv gw tv1 xi
526 (False, True) -> trySpontaneousEqOneWay inerts cv gw tv2 (mkTyVarTy tv1)
527 _ -> return Nothing }
529 = do { tch1 <- isTouchableMetaTyVar tv1
530 ; if tch1 then trySpontaneousEqOneWay inerts cv gw tv1 xi
531 else return Nothing }
534 -- trySpontaneousSolve (CFunEqCan ...) = ...
535 -- See Note [No touchables as FunEq RHS] in TcSMonad
536 trySpontaneousSolve _ _ = return Nothing
539 trySpontaneousEqOneWay :: InertSet -> CoVar -> CtFlavor -> TcTyVar -> Xi
540 -> TcS (Maybe SWorkList)
541 -- tv is a MetaTyVar, not untouchable
542 trySpontaneousEqOneWay inerts cv gw tv xi
543 | not (isSigTyVar tv) || isTyVarTy xi
544 = if typeKind xi `isSubKind` tyVarKind tv then
545 solveWithIdentity inerts cv gw tv xi
546 else if tyVarKind tv `isSubKind` typeKind xi then
547 return Nothing -- kinds are compatible but we can't solveWithIdentity this way
548 -- This case covers the a_touchable :: * ~ b_untouchable :: ??
549 -- which has to be deferred or floated out for someone else to solve
550 -- it in a scope where 'b' is no longer untouchable.
551 else kindErrorTcS gw (mkTyVarTy tv) xi -- See Note [Kind errors]
553 | otherwise -- Still can't solve, sig tyvar and non-variable rhs
557 trySpontaneousEqTwoWay :: InertSet -> CoVar -> CtFlavor -> TcTyVar -> TcTyVar
558 -> TcS (Maybe SWorkList)
559 -- Both tyvars are *touchable* MetaTyvars so there is only a chance for kind error here
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 -- None is a subkind of the other, but they are both touchable!
566 = kindErrorTcS gw (mkTyVarTy tv1) (mkTyVarTy tv2) -- See Note [Kind errors]
570 nicer_to_update_tv2 = isSigTyVar tv1 || isSystemName (Var.varName tv2)
574 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
575 Consider the wanted problem:
576 alpha ~ (# Int, Int #)
577 where alpha :: ?? and (# Int, Int #) :: (#). We can't spontaneously solve this constraint,
578 but we should rather reject the program that give rise to it. If 'trySpontaneousEqTwoWay'
579 simply returns @Nothing@ then that wanted constraint is going to propagate all the way and
580 get quantified over in inference mode. That's bad because we do know at this point that the
581 constraint is insoluble. Instead, we call 'kindErrorTcS' here, which immediately fails.
583 The same applies in canonicalization code in case of kind errors in the givens.
585 Note [Spontaneous solving and kind compatibility]
586 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
588 Note that our canonical constraints insist that only *given* equalities (tv ~ xi)
589 or (F xis ~ rhs) require the LHS and the RHS to have exactly the same kinds.
591 - We have to require this because:
592 Given equalities can be freely used to rewrite inside
593 other types or constraints.
594 - We do not have to do the same for wanteds because:
595 First, wanted equations (tv ~ xi) where tv is a touchable
596 unification variable may have kinds that do not agree (the
597 kind of xi must be a sub kind of the kind of tv). Second, any
598 potential kind mismatch will result in the constraint not
599 being soluble, which will be reported anyway. This is the
600 reason that @trySpontaneousOneWay@ and @trySpontaneousTwoWay@
601 will perform a kind compatibility check, and only then will
602 they proceed to @solveWithIdentity@.
605 - Givens from higher-rank, such as:
606 type family T b :: * -> * -> *
607 type instance T Bool = (->)
609 f :: forall a. ((T a ~ (->)) => ...) -> a -> ...
611 Whereas we would be able to apply the type instance, we would not be able to
612 use the given (T Bool ~ (->)) in the body of 'flop'
614 Note [Loopy spontaneous solving]
615 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
616 Consider the original wanted:
617 wanted : Maybe (E alpha) ~ alpha
618 where E is a type family, such that E (T x) = x. After canonicalization,
619 as a result of flattening, we will get:
620 given : E alpha ~ fsk
621 wanted : alpha ~ Maybe fsk
622 where (fsk := E alpha, on the side). Now, if we spontaneously *solve*
623 (alpha := Maybe fsk) we are in trouble! Instead, we should refrain from solving
624 it and keep it as wanted. In inference mode we'll end up quantifying over
625 (alpha ~ Maybe (E alpha))
626 Hence, 'solveWithIdentity' performs a small occurs check before
627 actually solving. But this occurs check *must look through* flatten skolems.
629 However, it may be the case that the flatten skolem in hand is equal to some other
630 flatten skolem whith *does not* mention our unification variable. Here's a typical example:
635 After canonicalization:
640 After some reactions:
645 At this point, we will try to spontaneously solve (alpha ~ f2) which remains as yet unsolved.
646 We will look inside f2, which immediately mentions (F alpha), so it's not good to unify! However
647 by looking at the equivalence class of the flatten skolems, we can see that it is fine to
648 unify (alpha ~ f1) which solves our goals!
650 A similar problem happens because of other spontaneous solving. Suppose we have the
651 following wanteds, arriving in this exact order:
652 (first) w: beta ~ alpha
653 (second) w: alpha ~ fsk
654 (third) g: F beta ~ fsk
655 Then, we first spontaneously solve the first constraint, making (beta := alpha), and having
656 (beta ~ alpha) as given. *Then* we encounter the second wanted (alpha ~ fsk). "fsk" does not
657 obviously mention alpha, so naively we can also spontaneously solve (alpha := fsk). But
658 that is wrong since fsk mentions beta, which has already secretly been unified to alpha!
660 To avoid this problem, the same occurs check must unveil rewritings that can happen because
661 of spontaneously having solved other constraints.
664 Note [Avoid double unifications]
665 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
666 The spontaneous solver has to return a given which mentions the unified unification
667 variable *on the left* of the equality. Here is what happens if not:
668 Original wanted: (a ~ alpha), (alpha ~ Int)
669 We spontaneously solve the first wanted, without changing the order!
670 given : a ~ alpha [having unified alpha := a]
671 Now the second wanted comes along, but he cannot rewrite the given, so we simply continue.
672 At the end we spontaneously solve that guy, *reunifying* [alpha := Int]
674 We avoid this problem by orienting the given so that the unification
675 variable is on the left. [Note that alternatively we could attempt to
676 enforce this at canonicalization]
678 See also Note [No touchables as FunEq RHS] in TcSMonad; avoiding
679 double unifications is the main reason we disallow touchable
680 unification variables as RHS of type family equations: F xis ~ alpha.
684 solveWithIdentity :: InertSet
685 -> CoVar -> CtFlavor -> TcTyVar -> Xi
686 -> TcS (Maybe SWorkList)
687 -- Solve with the identity coercion
688 -- Precondition: kind(xi) is a sub-kind of kind(tv)
689 -- Precondition: CtFlavor is Wanted or Derived
690 -- See [New Wanted Superclass Work] to see why solveWithIdentity
691 -- must work for Derived as well as Wanted
692 solveWithIdentity inerts cv gw tv xi
693 = do { tybnds <- getTcSTyBindsMap
694 ; case occurCheck tybnds inerts tv xi of
695 Nothing -> return Nothing
696 Just (xi_unflat,coi) -> solve_with xi_unflat coi }
698 solve_with xi_unflat coi -- coi : xi_unflat ~ xi
699 = do { traceTcS "Sneaky unification:" $
700 vcat [text "Coercion variable: " <+> ppr gw,
701 text "Coercion: " <+> pprEq (mkTyVarTy tv) xi,
702 text "Left Kind is : " <+> ppr (typeKind (mkTyVarTy tv)),
703 text "Right Kind is : " <+> ppr (typeKind xi)
705 ; setWantedTyBind tv xi_unflat -- Set tv := xi_unflat
706 ; cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi_unflat xi_unflat
707 ; let flav = mkGivenFlavor gw UnkSkol
708 ; (cts, co) <- case coi of
709 ACo co -> do { can_eqs <- canEq flav cv_given (mkTyVarTy tv) xi_unflat
710 ; return (can_eqs, co) }
712 (singleCCan (CTyEqCan { cc_id = cv_given
713 , cc_flavor = mkGivenFlavor gw UnkSkol
714 , cc_tyvar = tv, cc_rhs = xi }
715 -- xi, *not* xi_unflat because
716 -- xi_unflat may require flattening!
719 Wanted {} -> setWantedCoBind cv co
720 Derived {} -> setDerivedCoBind cv co
721 _ -> pprPanic "Can't spontaneously solve *given*" empty
722 -- See Note [Avoid double unifications]
723 ; return $ Just (workListFromCCans cts) }
725 occurCheck :: VarEnv (TcTyVar, TcType) -> InertSet
726 -> TcTyVar -> TcType -> Maybe (TcType,CoercionI)
727 -- Traverse @ty@ to make sure that @tv@ does not appear under some flatten skolem.
728 -- If it appears under some flatten skolem look in that flatten skolem equivalence class
729 -- (see Note [InertSet FlattenSkolemEqClass], [Loopy Spontaneous Solving]) to see if you
730 -- can find a different flatten skolem to use, that is, one that does not mention @tv@.
732 -- Postcondition: Just (ty', coi) = occurCheck binds inerts tv ty
734 -- NB: The returned type ty' may not be flat!
736 occurCheck ty_binds inerts the_tv the_ty
737 = ok emptyVarSet the_ty
739 -- If (fsk `elem` bad) then tv occurs in any rendering
740 -- of the type under the expansion of fsk
741 ok bad this_ty@(TyConApp tc tys)
742 | Just tys_cois <- allMaybes (map (ok bad) tys)
743 , (tys',cois') <- unzip tys_cois
744 = Just (TyConApp tc tys', mkTyConAppCoI tc cois')
745 | isSynTyCon tc, Just ty_expanded <- tcView this_ty
746 = ok bad ty_expanded -- See Note [Type synonyms and the occur check] in TcUnify
748 | Just (sty',coi) <- ok_pred bad sty
749 = Just (PredTy sty', coi)
750 ok bad (FunTy arg res)
751 | Just (arg', coiarg) <- ok bad arg, Just (res', coires) <- ok bad res
752 = Just (FunTy arg' res', mkFunTyCoI coiarg coires)
753 ok bad (AppTy fun arg)
754 | Just (fun', coifun) <- ok bad fun, Just (arg', coiarg) <- ok bad arg
755 = Just (AppTy fun' arg', mkAppTyCoI coifun coiarg)
756 ok bad (ForAllTy tv1 ty1)
757 -- WARNING: What if it is a (t1 ~ t2) => t3? It's not handled properly at the moment.
758 | Just (ty1', coi) <- ok bad ty1
759 = Just (ForAllTy tv1 ty1', mkForAllTyCoI tv1 coi)
762 ok bad this_ty@(TyVarTy tv)
763 | tv == the_tv = Nothing -- Occurs check error
764 | not (isTcTyVar tv) = Just (this_ty, IdCo this_ty) -- Bound var
765 | FlatSkol zty <- tcTyVarDetails tv = ok_fsk bad tv zty
766 | Just (_,ty) <- lookupVarEnv ty_binds tv = ok bad ty
767 | otherwise = Just (this_ty, IdCo this_ty)
769 -- Check if there exists a ty bind already, as a result of sneaky unification.
771 ok _bad _ty = Nothing
774 ok_pred bad (ClassP cn tys)
775 | Just tys_cois <- allMaybes $ map (ok bad) tys
776 = let (tys', cois') = unzip tys_cois
777 in Just (ClassP cn tys', mkClassPPredCoI cn cois')
778 ok_pred bad (IParam nm ty)
779 | Just (ty',co') <- ok bad ty
780 = Just (IParam nm ty', mkIParamPredCoI nm co')
781 ok_pred bad (EqPred ty1 ty2)
782 | Just (ty1',coi1) <- ok bad ty1, Just (ty2',coi2) <- ok bad ty2
783 = Just (EqPred ty1' ty2', mkEqPredCoI coi1 coi2)
784 ok_pred _ _ = Nothing
788 | fsk `elemVarSet` bad
789 -- We are already trying to find a rendering of fsk,
790 -- and to do that it seems we need a rendering, so fail
793 = firstJusts (ok new_bad zty : map (go_under_fsk new_bad) fsk_equivs)
795 fsk_equivs = getFskEqClass inerts fsk
796 new_bad = bad `extendVarSetList` (fsk : map fst fsk_equivs)
799 go_under_fsk bad_tvs (fsk,co)
800 | FlatSkol zty <- tcTyVarDetails fsk
801 = case ok bad_tvs zty of
803 Just (ty,coi') -> Just (ty, mkTransCoI coi' (ACo co))
804 | otherwise = pprPanic "go_down_equiv" (ppr fsk)
808 *********************************************************************************
810 The interact-with-inert Stage
812 *********************************************************************************
815 -- Interaction result of WorkItem <~> AtomicInert
817 = IR { ir_stop :: StopOrContinue
819 -- => Reagent (work item) consumed.
820 -- ContinueWith new_reagent
821 -- => Reagent transformed but keep gathering interactions.
822 -- The transformed item remains inert with respect
823 -- to any previously encountered inerts.
825 , ir_inert_action :: InertAction
826 -- Whether the inert item should remain in the InertSet.
828 , ir_new_work :: WorkList
829 -- new work items to add to the WorkList
831 , ir_improvement :: Maybe FDImprovement -- In case improvement kicked in
834 -- What to do with the inert reactant.
835 data InertAction = KeepInert | DropInert
838 mkIRContinue :: Monad m => WorkItem -> InertAction -> WorkList -> m InteractResult
839 mkIRContinue wi keep newWork = return $ IR (ContinueWith wi) keep newWork Nothing
841 mkIRStop :: Monad m => InertAction -> WorkList -> m InteractResult
842 mkIRStop keep newWork = return $ IR Stop keep newWork Nothing
844 mkIRStop_RecordImprovement :: Monad m => InertAction -> WorkList -> FDImprovement -> m InteractResult
845 mkIRStop_RecordImprovement keep newWork fdimpr = return $ IR Stop keep newWork (Just fdimpr)
848 dischargeWorkItem :: Monad m => m InteractResult
849 dischargeWorkItem = mkIRStop KeepInert emptyWorkList
851 noInteraction :: Monad m => WorkItem -> m InteractResult
852 noInteraction workItem = mkIRContinue workItem KeepInert emptyWorkList
854 data WhichComesFromInert = LeftComesFromInert | RightComesFromInert
857 ---------------------------------------------------
858 -- Interact a single WorkItem with the equalities of an inert set as far as possible, i.e. until we
859 -- get a Stop result from an individual reaction (i.e. when the WorkItem is consumed), or until we've
860 -- interact the WorkItem with the entire equalities of the InertSet
862 interactWithInertEqsStage :: SimplifierStage
863 interactWithInertEqsStage workItem inert
864 = foldISEqCtsM interactNext initITR inert
865 where initITR = SR { sr_inerts = IS { inert_eqs = emptyCCan -- We will fold over the equalities
866 , inert_fsks = Map.empty -- which will generate those two again
867 , inert_cts = inert_cts inert
868 , inert_fds = inert_fds inert
870 , sr_new_work = emptyWorkList
871 , sr_stop = ContinueWith workItem }
874 ---------------------------------------------------
875 -- Interact a single WorkItem with *non-equality* constraints in the inert set.
876 -- Precondition: equality interactions must have already happened, hence we have
877 -- to pick up some information from the incoming inert, before folding over the
878 -- "Other" constraints it contains!
879 interactWithInertsStage :: SimplifierStage
880 interactWithInertsStage workItem inert
881 = foldISOtherCtsM interactNext initITR inert
883 initITR = SR { -- Pick up: (1) equations, (2) FD improvements, (3) FlatSkol equiv. classes
884 sr_inerts = IS { inert_eqs = inert_eqs inert
885 , inert_cts = emptyCCan
886 , inert_fds = inert_fds inert
887 , inert_fsks = inert_fsks inert }
888 , sr_new_work = emptyWorkList
889 , sr_stop = ContinueWith workItem }
891 interactNext :: StageResult -> AtomicInert -> TcS StageResult
892 interactNext it inert
893 | ContinueWith workItem <- sr_stop it
894 = do { let inerts = sr_inerts it
895 fdimprs_old = getFDImprovements inerts
897 ; ir <- interactWithInert fdimprs_old inert workItem
899 -- New inerts depend on whether we KeepInert or not and must
900 -- be updated with FD improvement information from the interaction result (ir)
901 ; let inerts_new = updInertSetFDImprs upd_inert (ir_improvement ir)
902 upd_inert = if ir_inert_action ir == KeepInert
903 then inerts `updInertSet` inert else inerts
905 ; return $ SR { sr_inerts = inerts_new
906 , sr_new_work = sr_new_work it `unionWorkLists` ir_new_work ir
907 , sr_stop = ir_stop ir } }
908 | otherwise = return $ itrAddInert inert it
909 where itrAddInert :: AtomicInert -> StageResult -> StageResult
910 itrAddInert inert itr = itr { sr_inerts = (sr_inerts itr) `updInertSet` inert }
912 -- Do a single interaction of two constraints.
913 interactWithInert :: FDImprovements -> AtomicInert -> WorkItem -> TcS InteractResult
914 interactWithInert fdimprs inert workitem
915 = do { ctxt <- getTcSContext
916 ; let is_allowed = allowedInteraction (simplEqsOnly ctxt) inert workitem
917 inert_ev = cc_id inert
918 work_ev = cc_id workitem
920 -- Never interact a wanted and a derived where the derived's evidence
921 -- mentions the wanted evidence in an unguarded way.
922 -- See Note [Superclasses and recursive dictionaries]
923 -- and Note [New Wanted Superclass Work]
924 -- We don't have to do this for givens, as we fully know the evidence for them.
926 case (cc_flavor inert, cc_flavor workitem) of
927 (Wanted loc, Derived {}) -> isGoodRecEv work_ev (WantedEvVar inert_ev loc)
928 (Derived {}, Wanted loc) -> isGoodRecEv inert_ev (WantedEvVar work_ev loc)
931 ; if is_allowed && rec_ev_ok then
932 doInteractWithInert fdimprs inert workitem
934 noInteraction workitem
937 allowedInteraction :: Bool -> AtomicInert -> WorkItem -> Bool
938 -- Allowed interactions
939 allowedInteraction eqs_only (CDictCan {}) (CDictCan {}) = not eqs_only
940 allowedInteraction eqs_only (CIPCan {}) (CIPCan {}) = not eqs_only
941 allowedInteraction _ _ _ = True
943 --------------------------------------------
944 doInteractWithInert :: FDImprovements -> CanonicalCt -> CanonicalCt -> TcS InteractResult
945 -- Identical class constraints.
947 doInteractWithInert fdimprs
948 (CDictCan { cc_id = d1, cc_flavor = fl1, cc_class = cls1, cc_tyargs = tys1 })
949 workItem@(CDictCan { cc_id = d2, cc_flavor = fl2, cc_class = cls2, cc_tyargs = tys2 })
950 | cls1 == cls2 && (and $ zipWith tcEqType tys1 tys2)
951 = solveOneFromTheOther (d1,fl1) workItem
953 | cls1 == cls2 && (not (isGiven fl1 && isGiven fl2))
954 = -- See Note [When improvement happens]
955 do { let pty1 = ClassP cls1 tys1
956 pty2 = ClassP cls2 tys2
957 work_item_pred_loc = (pty2, ppr d2)
958 inert_pred_loc = (pty1, ppr d1)
959 loc = combineCtLoc fl1 fl2
960 eqn_pred_locs = improveFromAnother work_item_pred_loc inert_pred_loc
962 ; wevvars <- mkWantedFunDepEqns loc eqn_pred_locs
963 ; fd_cts <- canWanteds wevvars
964 ; let fd_work = workListFromCCans fd_cts
965 -- See Note [Generating extra equalities]
966 ; traceTcS "Checking if improvements existed." (ppr fdimprs)
967 ; if isEmptyCCan fd_cts || haveBeenImproved fdimprs pty1 pty2 then
969 mkIRContinue workItem KeepInert fd_work
970 else do { traceTcS "Recording improvement and throwing item back in worklist." (ppr (pty1,pty2))
971 ; mkIRStop_RecordImprovement KeepInert
972 (fd_work `unionWorkLists` workListFromCCan workItem) (pty1,pty2)
974 -- See Note [FunDep Reactions]
977 -- Class constraint and given equality: use the equality to rewrite
978 -- the class constraint.
979 doInteractWithInert _fdimprs
980 (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi })
981 (CDictCan { cc_id = dv, cc_flavor = wfl, cc_class = cl, cc_tyargs = xis })
982 | ifl `canRewrite` wfl
983 , tv `elemVarSet` tyVarsOfTypes xis
984 = if isDerivedSC wfl then
985 mkIRStop KeepInert $ emptyWorkList -- See Note [Adding Derived Superclasses]
986 else do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,wfl,cl,xis)
987 -- Continue with rewritten Dictionary because we can only be in the
988 -- interactWithEqsStage, so the dictionary is inert.
989 ; mkIRContinue rewritten_dict KeepInert emptyWorkList }
991 doInteractWithInert _fdimprs
992 (CDictCan { cc_id = dv, cc_flavor = ifl, cc_class = cl, cc_tyargs = xis })
993 workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
994 | wfl `canRewrite` ifl
995 , tv `elemVarSet` tyVarsOfTypes xis
996 = if isDerivedSC ifl then
997 mkIRContinue workItem DropInert emptyWorkList -- No need to do any rewriting,
998 -- see Note [Adding Derived Superclasses]
999 else do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,ifl,cl,xis)
1000 ; mkIRContinue workItem DropInert (workListFromCCan rewritten_dict) }
1002 -- Class constraint and given equality: use the equality to rewrite
1003 -- the class constraint.
1004 doInteractWithInert _fdimprs
1005 (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi })
1006 (CIPCan { cc_id = ipid, cc_flavor = wfl, cc_ip_nm = nm, cc_ip_ty = ty })
1007 | ifl `canRewrite` wfl
1008 , tv `elemVarSet` tyVarsOfType ty
1009 = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,wfl,nm,ty)
1010 ; mkIRContinue rewritten_ip KeepInert emptyWorkList }
1012 doInteractWithInert _fdimprs
1013 (CIPCan { cc_id = ipid, cc_flavor = ifl, cc_ip_nm = nm, cc_ip_ty = ty })
1014 workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
1015 | wfl `canRewrite` ifl
1016 , tv `elemVarSet` tyVarsOfType ty
1017 = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,ifl,nm,ty)
1018 ; mkIRContinue workItem DropInert (workListFromCCan rewritten_ip) }
1020 -- Two implicit parameter constraints. If the names are the same,
1021 -- but their types are not, we generate a wanted type equality
1022 -- that equates the type (this is "improvement").
1023 -- However, we don't actually need the coercion evidence,
1024 -- so we just generate a fresh coercion variable that isn't used anywhere.
1025 doInteractWithInert _fdimprs
1026 (CIPCan { cc_id = id1, cc_flavor = ifl, cc_ip_nm = nm1, cc_ip_ty = ty1 })
1027 workItem@(CIPCan { cc_flavor = wfl, cc_ip_nm = nm2, cc_ip_ty = ty2 })
1028 | nm1 == nm2 && isGiven wfl && isGiven ifl
1029 = -- See Note [Overriding implicit parameters]
1030 -- Dump the inert item, override totally with the new one
1031 -- Do not require type equality
1032 mkIRContinue workItem DropInert emptyWorkList
1034 | nm1 == nm2 && ty1 `tcEqType` ty2
1035 = solveOneFromTheOther (id1,ifl) workItem
1038 = -- See Note [When improvement happens]
1039 do { co_var <- newWantedCoVar ty1 ty2
1040 ; let flav = Wanted (combineCtLoc ifl wfl)
1041 ; cans <- mkCanonical flav co_var
1042 ; mkIRContinue workItem KeepInert (workListFromCCans cans) }
1045 -- Inert: equality, work item: function equality
1047 -- Never rewrite a given with a wanted equality, and a type function
1048 -- equality can never rewrite an equality. Note also that if we have
1049 -- F x1 ~ x2 and a ~ x3, and a occurs in x2, we don't rewrite it. We
1050 -- can wait until F x1 ~ x2 matches another F x1 ~ x4, and only then
1051 -- we will ``expose'' x2 and x4 to rewriting.
1053 -- Otherwise, we can try rewriting the type function equality with the equality.
1054 doInteractWithInert _fdimprs
1055 (CTyEqCan { cc_id = cv1, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi1 })
1056 (CFunEqCan { cc_id = cv2, cc_flavor = wfl, cc_fun = tc
1057 , cc_tyargs = args, cc_rhs = xi2 })
1058 | ifl `canRewrite` wfl
1059 , tv `elemVarSet` tyVarsOfTypes args
1060 = do { rewritten_funeq <- rewriteFunEq (cv1,tv,xi1) (cv2,wfl,tc,args,xi2)
1061 ; mkIRStop KeepInert (workListFromCCan rewritten_funeq) }
1062 -- must Stop here, because we may no longer be inert after the rewritting.
1064 -- Inert: function equality, work item: equality
1065 doInteractWithInert _fdimprs
1066 (CFunEqCan {cc_id = cv1, cc_flavor = ifl, cc_fun = tc
1067 , cc_tyargs = args, cc_rhs = xi1 })
1068 workItem@(CTyEqCan { cc_id = cv2, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi2 })
1069 | wfl `canRewrite` ifl
1070 , tv `elemVarSet` tyVarsOfTypes args
1071 = do { rewritten_funeq <- rewriteFunEq (cv2,tv,xi2) (cv1,ifl,tc,args,xi1)
1072 ; mkIRContinue workItem DropInert (workListFromCCan rewritten_funeq) }
1074 doInteractWithInert _fdimprs
1075 (CFunEqCan { cc_id = cv1, cc_flavor = fl1, cc_fun = tc1
1076 , cc_tyargs = args1, cc_rhs = xi1 })
1077 workItem@(CFunEqCan { cc_id = cv2, cc_flavor = fl2, cc_fun = tc2
1078 , cc_tyargs = args2, cc_rhs = xi2 })
1079 | fl1 `canSolve` fl2 && lhss_match
1080 = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
1081 ; mkIRStop KeepInert (workListFromCCans cans) }
1082 | fl2 `canSolve` fl1 && lhss_match
1083 = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
1084 ; mkIRContinue workItem DropInert (workListFromCCans cans) }
1086 lhss_match = tc1 == tc2 && and (zipWith tcEqType args1 args2)
1088 doInteractWithInert _fdimprs
1089 inert@(CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
1090 workItem@(CTyEqCan { cc_id = cv2, cc_flavor = fl2, cc_tyvar = tv2, cc_rhs = xi2 })
1091 -- Check for matching LHS
1092 | fl1 `canSolve` fl2 && tv1 == tv2
1093 = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
1094 ; mkIRStop KeepInert (workListFromCCans cans) }
1096 | fl2 `canSolve` fl1 && tv1 == tv2
1097 = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
1098 ; mkIRContinue workItem DropInert (workListFromCCans cans) }
1100 -- Check for rewriting RHS
1101 | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfType xi2
1102 = do { rewritten_eq <- rewriteEqRHS (cv1,tv1,xi1) (cv2,fl2,tv2,xi2)
1103 ; mkIRStop KeepInert (workListFromCCans rewritten_eq) }
1104 | fl2 `canRewrite` fl1 && tv2 `elemVarSet` tyVarsOfType xi1
1105 = do { rewritten_eq <- rewriteEqRHS (cv2,tv2,xi2) (cv1,fl1,tv1,xi1)
1106 ; mkIRContinue workItem DropInert (workListFromCCans rewritten_eq) }
1108 -- Finally, if workitem is a Flatten Equivalence Class constraint and the
1109 -- inert is a wanted constraint, even when the workitem cannot rewrite the
1110 -- inert, drop the inert out because you may have to reconsider solving the
1111 -- inert *using* the equivalence class you created. See note [Loopy Spontaneous Solving]
1112 -- and [InertSet FlattenSkolemEqClass]
1114 | not $ isGiven fl1, -- The inert is wanted or derived
1115 isMetaTyVar tv1, -- and has a unification variable lhs
1116 FlatSkol {} <- tcTyVarDetails tv2, -- And workitem is a flatten skolem equality
1117 Just tv2' <- tcGetTyVar_maybe xi2, FlatSkol {} <- tcTyVarDetails tv2'
1118 = mkIRContinue workItem DropInert (workListFromCCan inert)
1121 -- Fall-through case for all other situations
1122 doInteractWithInert _fdimprs _ workItem = noInteraction workItem
1124 -------------------------
1125 -- Equational Rewriting
1126 rewriteDict :: (CoVar, TcTyVar, Xi) -> (DictId, CtFlavor, Class, [Xi]) -> TcS CanonicalCt
1127 rewriteDict (cv,tv,xi) (dv,gw,cl,xis)
1128 = do { let cos = substTysWith [tv] [mkCoVarCoercion cv] xis -- xis[tv] ~ xis[xi]
1129 args = substTysWith [tv] [xi] xis
1131 dict_co = mkTyConCoercion con cos
1132 ; dv' <- newDictVar cl args
1134 Wanted {} -> setDictBind dv (EvCast dv' (mkSymCoercion dict_co))
1135 _given_or_derived -> setDictBind dv' (EvCast dv dict_co)
1136 ; return (CDictCan { cc_id = dv'
1139 , cc_tyargs = args }) }
1141 rewriteIP :: (CoVar,TcTyVar,Xi) -> (EvVar,CtFlavor, IPName Name, TcType) -> TcS CanonicalCt
1142 rewriteIP (cv,tv,xi) (ipid,gw,nm,ty)
1143 = do { let ip_co = substTyWith [tv] [mkCoVarCoercion cv] ty -- ty[tv] ~ t[xi]
1144 ty' = substTyWith [tv] [xi] ty
1145 ; ipid' <- newIPVar nm ty'
1147 Wanted {} -> setIPBind ipid (EvCast ipid' (mkSymCoercion ip_co))
1148 _given_or_derived -> setIPBind ipid' (EvCast ipid ip_co)
1149 ; return (CIPCan { cc_id = ipid'
1152 , cc_ip_ty = ty' }) }
1154 rewriteFunEq :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TyCon, [Xi], Xi) -> TcS CanonicalCt
1155 rewriteFunEq (cv1,tv,xi1) (cv2,gw, tc,args,xi2)
1156 = do { let arg_cos = substTysWith [tv] [mkCoVarCoercion cv1] args
1157 args' = substTysWith [tv] [xi1] args
1158 fun_co = mkTyConCoercion tc arg_cos
1159 ; cv2' <- case gw of
1160 Wanted {} -> do { cv2' <- newWantedCoVar (mkTyConApp tc args') xi2
1161 ; setWantedCoBind cv2 $
1162 mkTransCoercion fun_co (mkCoVarCoercion cv2')
1164 _giv_or_der -> newGivOrDerCoVar (mkTyConApp tc args') xi2 $
1165 mkTransCoercion (mkSymCoercion fun_co) (mkCoVarCoercion cv2)
1166 ; return (CFunEqCan { cc_id = cv2'
1173 rewriteEqRHS :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TcTyVar,Xi) -> TcS CanonicalCts
1174 -- Use the first equality to rewrite the second, flavors already checked.
1175 -- E.g. c1 : tv1 ~ xi1 c2 : tv2 ~ xi2
1176 -- rewrites c2 to give
1177 -- c2' : tv2 ~ xi2[xi1/tv1]
1178 -- We must do an occurs check to sure the new constraint is canonical
1179 -- So we might return an empty bag
1180 rewriteEqRHS (cv1,tv1,xi1) (cv2,gw,tv2,xi2)
1181 | Just tv2' <- tcGetTyVar_maybe xi2'
1182 , tv2 == tv2' -- In this case xi2[xi1/tv1] = tv2, so we have tv2~tv2
1183 = do { when (isWanted gw) (setWantedCoBind cv2 (mkSymCoercion co2'))
1184 ; return emptyCCan }
1189 -> do { cv2' <- newWantedCoVar (mkTyVarTy tv2) xi2'
1190 ; setWantedCoBind cv2 $
1191 mkCoVarCoercion cv2' `mkTransCoercion` mkSymCoercion co2'
1194 -> newGivOrDerCoVar (mkTyVarTy tv2) xi2' $
1195 mkCoVarCoercion cv2 `mkTransCoercion` co2'
1197 ; xi2'' <- canOccursCheck gw tv2 xi2' -- we know xi2' is *not* tv2
1198 ; return (singleCCan $ CTyEqCan { cc_id = cv2'
1204 xi2' = substTyWith [tv1] [xi1] xi2
1205 co2' = substTyWith [tv1] [mkCoVarCoercion cv1] xi2 -- xi2 ~ xi2[xi1/tv1]
1208 rewriteEqLHS :: WhichComesFromInert -> (Coercion,Xi) -> (CoVar,CtFlavor,Xi) -> TcS CanonicalCts
1209 -- Used to ineract two equalities of the following form:
1210 -- First Equality: co1: (XXX ~ xi1)
1211 -- Second Equality: cv2: (XXX ~ xi2)
1212 -- Where the cv1 `canSolve` cv2 equality
1213 -- We have an option of creating new work (xi1 ~ xi2) OR (xi2 ~ xi1). This
1214 -- depends on whether the left or the right equality comes from the inert set.
1216 -- prefer to create (xi2 ~ xi1) if the first comes from the inert
1217 -- prefer to create (xi1 ~ xi2) if the second comes from the inert
1218 rewriteEqLHS which (co1,xi1) (cv2,gw,xi2)
1219 = do { cv2' <- case (isWanted gw, which) of
1220 (True,LeftComesFromInert) ->
1221 do { cv2' <- newWantedCoVar xi2 xi1
1222 ; setWantedCoBind cv2 $
1223 co1 `mkTransCoercion` mkSymCoercion (mkCoVarCoercion cv2')
1225 (True,RightComesFromInert) ->
1226 do { cv2' <- newWantedCoVar xi1 xi2
1227 ; setWantedCoBind cv2 $
1228 co1 `mkTransCoercion` mkCoVarCoercion cv2'
1230 (False,LeftComesFromInert) ->
1231 newGivOrDerCoVar xi2 xi1 $
1232 mkSymCoercion (mkCoVarCoercion cv2) `mkTransCoercion` co1
1233 (False,RightComesFromInert) ->
1234 newGivOrDerCoVar xi1 xi2 $
1235 mkSymCoercion co1 `mkTransCoercion` mkCoVarCoercion cv2
1236 ; mkCanonical gw cv2'
1239 solveOneFromTheOther :: (EvVar, CtFlavor) -> CanonicalCt -> TcS InteractResult
1240 -- First argument inert, second argument workitem. They both represent
1241 -- wanted/given/derived evidence for the *same* predicate so we try here to
1242 -- discharge one directly from the other.
1244 -- Precondition: value evidence only (implicit parameters, classes)
1246 solveOneFromTheOther (iid,ifl) workItem
1247 -- Both derived needs a special case. You might think that we do not need
1248 -- two evidence terms for the same claim. But, since the evidence is partial,
1249 -- either evidence may do in some cases; see TcSMonad.isGoodRecEv.
1250 -- See also Example 3 in Note [Superclasses and recursive dictionaries]
1251 | isDerived ifl && isDerived wfl
1252 = noInteraction workItem
1254 | ifl `canSolve` wfl
1255 = do { unless (isGiven wfl) $ setEvBind wid (EvId iid)
1256 -- Overwrite the binding, if one exists
1257 -- For Givens, which are lambda-bound, nothing to overwrite,
1258 ; dischargeWorkItem }
1260 | otherwise -- wfl `canSolve` ifl
1261 = do { unless (isGiven ifl) $ setEvBind iid (EvId wid)
1262 ; mkIRContinue workItem DropInert emptyWorkList }
1265 wfl = cc_flavor workItem
1266 wid = cc_id workItem
1269 Note [Superclasses and recursive dictionaries]
1270 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1271 Overlaps with Note [SUPERCLASS-LOOP 1]
1272 Note [SUPERCLASS-LOOP 2]
1273 Note [Recursive instances and superclases]
1274 ToDo: check overlap and delete redundant stuff
1276 Right before adding a given into the inert set, we must
1277 produce some more work, that will bring the superclasses
1278 of the given into scope. The superclass constraints go into
1281 When we simplify a wanted constraint, if we first see a matching
1282 instance, we may produce new wanted work. To (1) avoid doing this work
1283 twice in the future and (2) to handle recursive dictionaries we may ``cache''
1284 this item as solved (in effect, given) into our inert set and with that add
1285 its superclass constraints (as given) in our worklist.
1287 But now we have added partially solved constraints to the worklist which may
1288 interact with other wanteds. Consider the example:
1292 class Eq b => Foo a b --- 0-th selector
1293 instance Eq a => Foo [a] a --- fooDFun
1295 and wanted (Foo [t] t). We are first going to see that the instance matches
1296 and create an inert set that includes the solved (Foo [t] t) and its
1298 d1 :_g Foo [t] t d1 := EvDFunApp fooDFun d3
1299 d2 :_g Eq t d2 := EvSuperClass d1 0
1300 Our work list is going to contain a new *wanted* goal
1302 It is wrong to react the wanted (Eq t) with the given (Eq t) because that would
1303 construct loopy evidence. Hence the check isGoodRecEv in doInteractWithInert.
1305 OK, so we have ruled out bad behaviour, but how do we ge recursive dictionaries,
1310 data D r = ZeroD | SuccD (r (D r));
1312 instance (Eq (r (D r))) => Eq (D r) where
1313 ZeroD == ZeroD = True
1314 (SuccD a) == (SuccD b) = a == b
1317 equalDC :: D [] -> D [] -> Bool;
1320 We need to prove (Eq (D [])). Here's how we go:
1324 by instance decl, holds if
1328 *BUT* we have an inert set which gives us (no superclasses):
1330 By the instance declaration of Eq we can show the 'd2' goal if
1332 where d2 = dfEqList d3
1334 Now, however this wanted can interact with our inert d1 to set:
1336 and solve the goal. Why was this interaction OK? Because, if we chase the
1337 evidence of d1 ~~> dfEqD d2 ~~-> dfEqList d3, so by setting d3 := d1 we
1339 d3 := dfEqD2 (dfEqList d3)
1340 which is FINE because the use of d3 is protected by the instance function
1343 So, our strategy is to try to put solved wanted dictionaries into the
1344 inert set along with their superclasses (when this is meaningful,
1345 i.e. when new wanted goals are generated) but solve a wanted dictionary
1346 from a given only in the case where the evidence variable of the
1347 wanted is mentioned in the evidence of the given (recursively through
1348 the evidence binds) in a protected way: more instance function applications
1349 than superclass selectors.
1351 Here are some more examples from GHC's previous type checker
1355 This code arises in the context of "Scrap Your Boilerplate with Class"
1359 instance Sat (ctx Char) => Data ctx Char -- dfunData1
1360 instance (Sat (ctx [a]), Data ctx a) => Data ctx [a] -- dfunData2
1362 class Data Maybe a => Foo a
1364 instance Foo t => Sat (Maybe t) -- dfunSat
1366 instance Data Maybe a => Foo a -- dfunFoo1
1367 instance Foo a => Foo [a] -- dfunFoo2
1368 instance Foo [Char] -- dfunFoo3
1370 Consider generating the superclasses of the instance declaration
1371 instance Foo a => Foo [a]
1373 So our problem is this
1375 d1 :_w Data Maybe [t]
1377 We may add the given in the inert set, along with its superclasses
1378 [assuming we don't fail because there is a matching instance, see
1379 tryTopReact, given case ]
1383 d01 :_g Data Maybe t -- d2 := EvDictSuperClass d0 0
1384 d1 :_w Data Maybe [t]
1385 Then d2 can readily enter the inert, and we also do solving of the wanted
1388 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1390 d2 :_w Sat (Maybe [t])
1392 d01 :_g Data Maybe t
1393 Now, we may simplify d2 more:
1396 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1397 d1 :_g Data Maybe [t]
1398 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1402 d01 :_g Data Maybe t
1404 Now, we can just solve d3.
1407 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1408 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1411 d01 :_g Data Maybe t
1412 And now we can simplify d4 again, but since it has superclasses we *add* them to the worklist:
1415 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1416 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1417 d4 :_g Foo [t] d4 := dfunFoo2 d5
1420 d6 :_g Data Maybe [t] d6 := EvDictSuperClass d4 0
1421 d01 :_g Data Maybe t
1422 Now, d5 can be solved! (and its superclass enter scope)
1425 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1426 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1427 d4 :_g Foo [t] d4 := dfunFoo2 d5
1428 d5 :_g Foo t d5 := dfunFoo1 d7
1431 d6 :_g Data Maybe [t]
1432 d8 :_g Data Maybe t d8 := EvDictSuperClass d5 0
1433 d01 :_g Data Maybe t
1436 [1] Suppose we pick d8 and we react him with d01. Which of the two givens should
1437 we keep? Well, we *MUST NOT* drop d01 because d8 contains recursive evidence
1438 that must not be used (look at case interactInert where both inert and workitem
1439 are givens). So we have several options:
1440 - Drop the workitem always (this will drop d8)
1441 This feels very unsafe -- what if the work item was the "good" one
1442 that should be used later to solve another wanted?
1443 - Don't drop anyone: the inert set may contain multiple givens!
1444 [This is currently implemented]
1446 The "don't drop anyone" seems the most safe thing to do, so now we come to problem 2:
1447 [2] We have added both d6 and d01 in the inert set, and we are interacting our wanted
1448 d7. Now the [isRecDictEv] function in the ineration solver
1449 [case inert-given workitem-wanted] will prevent us from interacting d7 := d8
1450 precisely because chasing the evidence of d8 leads us to an unguarded use of d7.
1452 So, no interaction happens there. Then we meet d01 and there is no recursion
1453 problem there [isRectDictEv] gives us the OK to interact and we do solve d7 := d01!
1455 Note [SUPERCLASS-LOOP 1]
1456 ~~~~~~~~~~~~~~~~~~~~~~~~
1457 We have to be very, very careful when generating superclasses, lest we
1458 accidentally build a loop. Here's an example:
1462 class S a => C a where { opc :: a -> a }
1463 class S b => D b where { opd :: b -> b }
1465 instance C Int where
1468 instance D Int where
1471 From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int}
1472 Simplifying, we may well get:
1473 $dfCInt = :C ds1 (opd dd)
1476 Notice that we spot that we can extract ds1 from dd.
1478 Alas! Alack! We can do the same for (instance D Int):
1480 $dfDInt = :D ds2 (opc dc)
1484 And now we've defined the superclass in terms of itself.
1485 Two more nasty cases are in
1490 - Satisfy the superclass context *all by itself*
1491 (tcSimplifySuperClasses)
1492 - And do so completely; i.e. no left-over constraints
1493 to mix with the constraints arising from method declarations
1496 Note [SUPERCLASS-LOOP 2]
1497 ~~~~~~~~~~~~~~~~~~~~~~~~
1498 We need to be careful when adding "the constaint we are trying to prove".
1499 Suppose we are *given* d1:Ord a, and want to deduce (d2:C [a]) where
1501 class Ord a => C a where
1502 instance Ord [a] => C [a] where ...
1504 Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the
1505 superclasses of C [a] to avails. But we must not overwrite the binding
1506 for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
1509 Here's another variant, immortalised in tcrun020
1510 class Monad m => C1 m
1511 class C1 m => C2 m x
1512 instance C2 Maybe Bool
1513 For the instance decl we need to build (C1 Maybe), and it's no good if
1514 we run around and add (C2 Maybe Bool) and its superclasses to the avails
1515 before we search for C1 Maybe.
1517 Here's another example
1518 class Eq b => Foo a b
1519 instance Eq a => Foo [a] a
1523 we'll first deduce that it holds (via the instance decl). We must not
1524 then overwrite the Eq t constraint with a superclass selection!
1526 At first I had a gross hack, whereby I simply did not add superclass constraints
1527 in addWanted, though I did for addGiven and addIrred. This was sub-optimal,
1528 becuase it lost legitimate superclass sharing, and it still didn't do the job:
1529 I found a very obscure program (now tcrun021) in which improvement meant the
1530 simplifier got two bites a the cherry... so something seemed to be an Stop
1531 first time, but reducible next time.
1533 Now we implement the Right Solution, which is to check for loops directly
1534 when adding superclasses. It's a bit like the occurs check in unification.
1536 Note [Recursive instances and superclases]
1537 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1538 Consider this code, which arises in the context of "Scrap Your
1539 Boilerplate with Class".
1543 instance Sat (ctx Char) => Data ctx Char
1544 instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]
1546 class Data Maybe a => Foo a
1548 instance Foo t => Sat (Maybe t)
1550 instance Data Maybe a => Foo a
1551 instance Foo a => Foo [a]
1554 In the instance for Foo [a], when generating evidence for the superclasses
1555 (ie in tcSimplifySuperClasses) we need a superclass (Data Maybe [a]).
1556 Using the instance for Data, we therefore need
1557 (Sat (Maybe [a], Data Maybe a)
1558 But we are given (Foo a), and hence its superclass (Data Maybe a).
1559 So that leaves (Sat (Maybe [a])). Using the instance for Sat means
1560 we need (Foo [a]). And that is the very dictionary we are bulding
1561 an instance for! So we must put that in the "givens". So in this
1563 Given: Foo a, Foo [a]
1564 Wanted: Data Maybe [a]
1566 BUT we must *not not not* put the *superclasses* of (Foo [a]) in
1567 the givens, which is what 'addGiven' would normally do. Why? Because
1568 (Data Maybe [a]) is the superclass, so we'd "satisfy" the wanted
1569 by selecting a superclass from Foo [a], which simply makes a loop.
1571 On the other hand we *must* put the superclasses of (Foo a) in
1572 the givens, as you can see from the derivation described above.
1574 Conclusion: in the very special case of tcSimplifySuperClasses
1575 we have one 'given' (namely the "this" dictionary) whose superclasses
1576 must not be added to 'givens' by addGiven.
1578 There is a complication though. Suppose there are equalities
1579 instance (Eq a, a~b) => Num (a,b)
1580 Then we normalise the 'givens' wrt the equalities, so the original
1581 given "this" dictionary is cast to one of a different type. So it's a
1582 bit trickier than before to identify the "special" dictionary whose
1583 superclasses must not be added. See test
1584 indexed-types/should_run/EqInInstance
1586 We need a persistent property of the dictionary to record this
1587 special-ness. Current I'm using the InstLocOrigin (a bit of a hack,
1588 but cool), which is maintained by dictionary normalisation.
1589 Specifically, the InstLocOrigin is
1591 then the no-superclass thing kicks in. WATCH OUT if you fiddle
1594 Note [MATCHING-SYNONYMS]
1595 ~~~~~~~~~~~~~~~~~~~~~~~~
1596 When trying to match a dictionary (D tau) to a top-level instance, or a
1597 type family equation (F taus_1 ~ tau_2) to a top-level family instance,
1598 we do *not* need to expand type synonyms because the matcher will do that for us.
1601 Note [RHS-FAMILY-SYNONYMS]
1602 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1603 The RHS of a family instance is represented as yet another constructor which is
1604 like a type synonym for the real RHS the programmer declared. Eg:
1605 type instance F (a,a) = [a]
1607 :R32 a = [a] -- internal type synonym introduced
1608 F (a,a) ~ :R32 a -- instance
1610 When we react a family instance with a type family equation in the work list
1611 we keep the synonym-using RHS without expansion.
1614 *********************************************************************************
1616 The top-reaction Stage
1618 *********************************************************************************
1621 -- If a work item has any form of interaction with top-level we get this
1622 data TopInteractResult
1623 = NoTopInt -- No top-level interaction
1625 { tir_new_work :: WorkList -- Sub-goals or new work (could be given,
1626 -- for superclasses)
1627 , tir_new_inert :: StopOrContinue -- The input work item, ready to become *inert* now:
1628 } -- NB: in ``given'' (solved) form if the
1629 -- original was wanted or given and instance match
1630 -- was found, but may also be in wanted form if we
1631 -- only reacted with functional dependencies
1632 -- arising from top-level instances.
1634 topReactionsStage :: SimplifierStage
1635 topReactionsStage workItem inerts
1636 = do { tir <- tryTopReact workItem
1639 return $ SR { sr_inerts = inerts
1640 , sr_new_work = emptyWorkList
1641 , sr_stop = ContinueWith workItem }
1642 SomeTopInt tir_new_work tir_new_inert ->
1643 return $ SR { sr_inerts = inerts
1644 , sr_new_work = tir_new_work
1645 , sr_stop = tir_new_inert
1649 tryTopReact :: WorkItem -> TcS TopInteractResult
1650 tryTopReact workitem
1651 = do { -- A flag controls the amount of interaction allowed
1652 -- See Note [Simplifying RULE lhs constraints]
1653 ctxt <- getTcSContext
1654 ; if allowedTopReaction (simplEqsOnly ctxt) workitem
1655 then do { traceTcS "tryTopReact / calling doTopReact" (ppr workitem)
1656 ; doTopReact workitem }
1657 else return NoTopInt
1660 allowedTopReaction :: Bool -> WorkItem -> Bool
1661 allowedTopReaction eqs_only (CDictCan {}) = not eqs_only
1662 allowedTopReaction _ _ = True
1665 doTopReact :: WorkItem -> TcS TopInteractResult
1666 -- The work item does not react with the inert set,
1667 -- so try interaction with top-level instances
1668 doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Wanted loc
1669 , cc_class = cls, cc_tyargs = xis })
1670 = do { -- See Note [MATCHING-SYNONYMS]
1671 ; lkp_inst_res <- matchClassInst cls xis loc
1672 ; case lkp_inst_res of
1673 NoInstance -> do { traceTcS "doTopReact/ no class instance for" (ppr dv)
1675 GenInst wtvs ev_term -> -- Solved
1676 -- No need to do fundeps stuff here; the instance
1677 -- matches already so we won't get any more info
1678 -- from functional dependencies
1679 do { traceTcS "doTopReact/ found class instance for" (ppr dv)
1680 ; setDictBind dv ev_term
1681 ; workList <- canWanteds wtvs
1683 -- Solved in one step and no new wanted work produced.
1684 -- i.e we directly matched a top-level instance
1685 -- No point in caching this in 'inert', nor in adding superclasses
1686 then return $ SomeTopInt { tir_new_work = emptyWorkList
1687 , tir_new_inert = Stop }
1689 -- Solved and new wanted work produced, you may cache the
1690 -- (tentatively solved) dictionary as Derived and its superclasses
1691 else do { let solved = makeSolvedByInst workItem
1692 ; sc_work <- newDerivedSCWork dv loc cls xis
1693 -- See Note [Adding Derived Superclasses]
1694 ; let inst_work = workListFromCCans workList
1695 ; return $ SomeTopInt
1696 { tir_new_work = inst_work `unionWorkLists` sc_work
1697 , tir_new_inert = ContinueWith solved } }
1701 -- Try for a fundep reaction beween the wanted item
1702 -- and a top-level instance declaration
1704 = do { instEnvs <- getInstEnvs
1705 ; let eqn_pred_locs = improveFromInstEnv (classInstances instEnvs)
1706 (ClassP cls xis, ppr dv)
1707 ; wevvars <- mkWantedFunDepEqns loc eqn_pred_locs
1708 -- NB: fundeps generate some wanted equalities, but
1709 -- we don't use their evidence for anything
1710 ; fd_cts <- canWanteds wevvars
1711 ; let fd_work = workListFromCCans fd_cts
1713 ; if isEmptyCCan fd_cts then
1714 do { sc_work <- newDerivedSCWork dv loc cls xis
1715 -- See Note [Adding Derived Superclasses]
1716 ; return $ SomeTopInt { tir_new_work = fd_work `unionWorkLists` sc_work
1717 , tir_new_inert = ContinueWith workItem }
1719 else -- More fundep work produced, don't do any superlcass stuff, just
1720 -- thow him back in the worklist prioritizing the solution of fd equalities
1722 SomeTopInt { tir_new_work = fd_work `unionWorkLists` workListFromCCan workItem
1723 , tir_new_inert = Stop }
1725 -- NB: workItem is inert, but it isn't solved
1726 -- keep it as inert, although it's not solved because we
1727 -- have now reacted all its top-level fundep-induced equalities!
1729 -- See Note [FunDep Reactions]
1732 -- Derived, do not add any further derived superclasses; their full transitive
1733 -- closure has already been added.
1734 doTopReact (CDictCan { cc_flavor = fl })
1738 doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Given loc
1739 , cc_class = cls, cc_tyargs = xis })
1740 = do { sc_work <- newGivenSCWork dv loc cls xis
1741 ; return $ SomeTopInt sc_work (ContinueWith workItem) }
1742 -- See Note [Given constraint that matches an instance declaration]
1745 doTopReact (CFunEqCan { cc_id = cv, cc_flavor = fl
1746 , cc_fun = tc, cc_tyargs = args, cc_rhs = xi })
1747 = ASSERT (isSynFamilyTyCon tc) -- No associated data families have reached that far
1748 do { match_res <- matchFam tc args -- See Note [MATCHING-SYNONYMS]
1752 MatchInstSingle (rep_tc, rep_tys)
1753 -> do { let Just coe_tc = tyConFamilyCoercion_maybe rep_tc
1754 Just rhs_ty = tcView (mkTyConApp rep_tc rep_tys)
1755 -- Eagerly expand away the type synonym on the
1756 -- RHS of a type function, so that it never
1757 -- appears in an error message
1758 -- See Note [Type synonym families] in TyCon
1759 coe = mkTyConApp coe_tc rep_tys
1761 Wanted {} -> do { cv' <- newWantedCoVar rhs_ty xi
1762 ; setWantedCoBind cv $
1763 coe `mkTransCoercion`
1766 _ -> newGivOrDerCoVar xi rhs_ty $
1767 mkSymCoercion (mkCoVarCoercion cv) `mkTransCoercion` coe
1769 ; can_cts <- mkCanonical fl cv'
1770 ; let workList = workListFromCCans can_cts
1771 ; return $ SomeTopInt workList Stop }
1773 -> panicTcS $ text "TcSMonad.matchFam returned multiple instances!"
1777 -- Any other work item does not react with any top-level equations
1778 doTopReact _workItem = return NoTopInt
1781 Note [Adding Derived Superclasses]
1782 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1783 Generally speaking, we want to be able to add derived superclasses of
1784 unsolved wanteds, and wanteds that have been partially being solved
1785 via an instance. This is important to be able to simplify the inferred
1786 constraints more (and to allow for recursive dictionaries, less
1787 importantly). Example:
1789 Inferred wanted constraint is (Eq a, Ord a), but we'd only like to
1790 quantify over Ord a, hence we would like to be able to add the
1791 superclass of Ord a as Derived and use it to solve the wanted Eq a.
1793 Hence we will add Derived superclasses in the following two cases:
1794 (1) When we meet an unsolved wanted in top-level reactions
1795 (2) When we partially solve a wanted in top-level reactions using an instance decl.
1797 At that point, we have two options:
1798 (1) Add transitively add *ALL* of the superclasses of the Derived
1799 (2) Add only the immediate ones, but whenever we meet a Derived in
1800 the future, add its own superclasses as Derived.
1802 Option (2) is terrible, because deriveds may be rewritten or kicked
1803 out of the inert set, which will result in slightly rewritten
1804 superclasses being reintroduced in the worklist and the inert set. Eg:
1807 instance Foo a => B [a]
1809 Original constraints:
1811 [Given] co : a ~ Int
1813 We apply the instance to the wanted and put it and its superclasses as
1814 as Deriveds in the inerts:
1817 [Derived] (sel d) : C [a]
1820 [Given] co : a ~ Int
1823 Now, suppose that we interact the Derived with the Given equality, and
1824 kick him out of the inert, the next time around a superclass C [Int]
1825 will be produced -- but we already *have* C [a] in the inerts which
1826 will anyway get rewritten to C [Int].
1828 So we choose (1), and *never* introduce any more superclass work from
1829 Deriveds. This enables yet another optimisation: If we ever meet an
1830 equality that can rewrite a Derived, if that Derived is a superclass
1831 derived (like C [a] above), i.e. not a partially solved one (like B
1832 [a]) above, we may simply completely *discard* that Derived. The
1833 reason is because somewhere in the inert lies the original wanted, or
1834 partially solved constraint that gave rise to that superclass, and
1835 that constraint *will* be kicked out, and *will* result in the
1836 rewritten superclass to be added in the inerts later on, anyway.
1840 Note [FunDep and implicit parameter reactions]
1841 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1842 Currently, our story of interacting two dictionaries (or a dictionary
1843 and top-level instances) for functional dependencies, and implicit
1844 paramters, is that we simply produce new wanted equalities. So for example
1846 class D a b | a -> b where ...
1852 We generate the extra work item
1854 where 'cv' is currently unused. However, this new item reacts with d2,
1855 discharging it in favour of a new constraint d2' thus:
1857 d2 := d2' |> D Int cv
1858 Now d2' can be discharged from d1
1860 We could be more aggressive and try to *immediately* solve the dictionary
1861 using those extra equalities. With the same inert set and work item we
1862 might dischard d2 directly:
1865 d2 := d1 |> D Int cv
1867 But in general it's a bit painful to figure out the necessary coercion,
1868 so we just take the first approach. Here is a better example. Consider:
1869 class C a b c | a -> b
1871 [Given] d1 : C T Int Char
1872 [Wanted] d2 : C T beta Int
1873 In this case, it's *not even possible* to solve the wanted immediately.
1874 So we should simply output the functional dependency and add this guy
1875 [but NOT its superclasses] back in the worklist. Even worse:
1876 [Given] d1 : C T Int beta
1877 [Wanted] d2: C T beta Int
1878 Then it is solvable, but its very hard to detect this on the spot.
1880 It's exactly the same with implicit parameters, except that the
1881 "aggressive" approach would be much easier to implement.
1883 Note [When improvement happens]
1884 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1885 We fire an improvement rule when
1887 * Two constraints match (modulo the fundep)
1888 e.g. C t1 t2, C t1 t3 where C a b | a->b
1889 The two match because the first arg is identical
1891 * At least one is not Given. If they are both given, we don't fire
1892 the reaction because we have no way of constructing evidence for a
1893 new equality nor does it seem right to create a new wanted goal
1894 (because the goal will most likely contain untouchables, which
1895 can't be solved anyway)!
1897 Note that we *do* fire the improvement if one is Given and one is Derived.
1898 The latter can be a superclass of a wanted goal. Example (tcfail138)
1899 class L a b | a -> b
1900 class (G a, L a b) => C a b
1902 instance C a b' => G (Maybe a)
1903 instance C a b => C (Maybe a) a
1904 instance L (Maybe a) a
1906 When solving the superclasses of the (C (Maybe a) a) instance, we get
1907 Given: C a b ... and hance by superclasses, (G a, L a b)
1909 Use the instance decl to get
1911 The (C a b') is inert, so we generate its Derived superclasses (L a b'),
1912 and now we need improvement between that derived superclass an the Given (L a b)
1914 Note [Overriding implicit parameters]
1915 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1917 f :: (?x::a) -> Bool -> a
1919 g v = let ?x::Int = 3
1920 in (f v, let ?x::Bool = True in f v)
1922 This should probably be well typed, with
1923 g :: Bool -> (Int, Bool)
1925 So the inner binding for ?x::Bool *overrides* the outer one.
1926 Hence a work-item Given overrides an inert-item Given.
1928 Note [Given constraint that matches an instance declaration]
1929 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1930 What should we do when we discover that one (or more) top-level
1931 instances match a given (or solved) class constraint? We have
1934 1. Reject the program. The reason is that there may not be a unique
1935 best strategy for the solver. Example, from the OutsideIn(X) paper:
1936 instance P x => Q [x]
1937 instance (x ~ y) => R [x] y
1939 wob :: forall a b. (Q [b], R b a) => a -> Int
1941 g :: forall a. Q [a] => [a] -> Int
1944 will generate the impliation constraint:
1945 Q [a] => (Q [beta], R beta [a])
1946 If we react (Q [beta]) with its top-level axiom, we end up with a
1947 (P beta), which we have no way of discharging. On the other hand,
1948 if we react R beta [a] with the top-level we get (beta ~ a), which
1949 is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
1950 now solvable by the given Q [a].
1952 However, this option is restrictive, for instance [Example 3] from
1953 Note [Recursive dictionaries] will fail to work.
1955 2. Ignore the problem, hoping that the situations where there exist indeed
1956 such multiple strategies are rare: Indeed the cause of the previous
1957 problem is that (R [x] y) yields the new work (x ~ y) which can be
1958 *spontaneously* solved, not using the givens.
1960 We are choosing option 2 below but we might consider having a flag as well.
1963 Note [New Wanted Superclass Work]
1964 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1965 Even in the case of wanted constraints, we add all of its superclasses as
1966 new given work. There are several reasons for this:
1967 a) to minimise error messages;
1968 eg suppose we have wanted (Eq a, Ord a)
1969 then we report only (Ord a) unsoluble
1971 b) to make the smallest number of constraints when *inferring* a type
1972 (same Eq/Ord example)
1974 c) for recursive dictionaries we *must* add the superclasses
1975 so that we can use them when solving a sub-problem
1977 d) To allow FD-like improvement for type families. Assume that
1979 class C a b | a -> b
1980 and we have to solve the implication constraint:
1982 Then, FD improvement can help us to produce a new wanted (beta ~ b)
1984 We want to have the same effect with the type family encoding of
1985 functional dependencies. Namely, consider:
1986 class (F a ~ b) => C a b
1987 Now suppose that we have:
1990 By interacting the given we will get given (F a ~ b) which is not
1991 enough by itself to make us discharge (C a beta). However, we
1992 may create a new derived equality from the super-class of the
1993 wanted constraint (C a beta), namely derived (F a ~ beta).
1994 Now we may interact this with given (F a ~ b) to get:
1996 But 'beta' is a touchable unification variable, and hence OK to
1997 unify it with 'b', replacing the derived evidence with the identity.
1999 This requires trySpontaneousSolve to solve *derived*
2000 equalities that have a touchable in their RHS, *in addition*
2001 to solving wanted equalities.
2003 Here is another example where this is useful.
2007 class (F a ~ b) => C a b
2008 And we are given the wanteds:
2012 We surely do *not* want to quantify over (b ~ c), since if someone provides
2013 dictionaries for (C a b) and (C a c), these dictionaries can provide a proof
2014 of (b ~ c), hence no extra evidence is necessary. Here is what will happen:
2016 Step 1: We will get new *given* superclass work,
2017 provisionally to our solving of w1 and w2
2019 g1: F a ~ b, g2 : F a ~ c,
2020 w1 : C a b, w2 : C a c, w3 : b ~ c
2022 The evidence for g1 and g2 is a superclass evidence term:
2024 g1 := sc w1, g2 := sc w2
2026 Step 2: The givens will solve the wanted w3, so that
2027 w3 := sym (sc w1) ; sc w2
2029 Step 3: Now, one may naively assume that then w2 can be solve from w1
2030 after rewriting with the (now solved equality) (b ~ c).
2032 But this rewriting is ruled out by the isGoodRectDict!
2034 Conclusion, we will (correctly) end up with the unsolved goals
2037 NB: The desugarer needs be more clever to deal with equalities
2038 that participate in recursive dictionary bindings.
2042 newGivenSCWork :: EvVar -> GivenLoc -> Class -> [Xi] -> TcS WorkList
2043 newGivenSCWork ev loc cls xis
2044 | NoScSkol <- ctLocOrigin loc -- Very important!
2045 = return emptyWorkList
2047 = newImmSCWorkFromFlavored ev (Given loc) cls xis >>= return . workListFromCCans
2049 newDerivedSCWork :: EvVar -> WantedLoc -> Class -> [Xi] -> TcS WorkList
2050 newDerivedSCWork ev loc cls xis
2051 = do { ims <- newImmSCWorkFromFlavored ev flavor cls xis
2052 ; final_cts <- rec_sc_work ims
2053 ; return $ workListFromCCans final_cts }
2054 where rec_sc_work :: CanonicalCts -> TcS CanonicalCts
2056 = do { bg <- mapBagM (\c -> do { ims <- imm_sc_work c
2057 ; recs_ims <- rec_sc_work ims
2058 ; return $ consBag c recs_ims }) cts
2059 ; return $ concatBag bg }
2060 imm_sc_work (CDictCan { cc_id = dv, cc_flavor = fl, cc_class = cls, cc_tyargs = xis })
2061 = newImmSCWorkFromFlavored dv fl cls xis
2062 imm_sc_work _ct = return emptyCCan
2064 flavor = Derived loc DerSC
2066 newImmSCWorkFromFlavored :: EvVar -> CtFlavor -> Class -> [Xi] -> TcS CanonicalCts
2067 -- Returns immediate superclasses
2068 newImmSCWorkFromFlavored ev flavor cls xis
2069 = do { let (tyvars, sc_theta, _, _) = classBigSig cls
2070 sc_theta1 = substTheta (zipTopTvSubst tyvars xis) sc_theta
2071 ; sc_vars <- zipWithM inst_one sc_theta1 [0..]
2072 ; mkCanonicals flavor sc_vars }
2074 inst_one pred n = newGivOrDerEvVar pred (EvSuperClass ev n)
2077 data LookupInstResult
2079 | GenInst [WantedEvVar] EvTerm
2081 matchClassInst :: Class -> [Type] -> WantedLoc -> TcS LookupInstResult
2082 matchClassInst clas tys loc
2083 = do { let pred = mkClassPred clas tys
2084 ; mb_result <- matchClass clas tys
2086 MatchInstNo -> return NoInstance
2087 MatchInstMany -> return NoInstance -- defer any reactions of a multitude until
2088 -- we learn more about the reagent
2089 MatchInstSingle (dfun_id, mb_inst_tys) ->
2090 do { checkWellStagedDFun pred dfun_id loc
2092 -- It's possible that not all the tyvars are in
2093 -- the substitution, tenv. For example:
2094 -- instance C X a => D X where ...
2095 -- (presumably there's a functional dependency in class C)
2096 -- Hence mb_inst_tys :: Either TyVar TcType
2098 ; tys <- instDFunTypes mb_inst_tys
2099 ; let (theta, _) = tcSplitPhiTy (applyTys (idType dfun_id) tys)
2100 ; if null theta then
2101 return (GenInst [] (EvDFunApp dfun_id tys []))
2103 { ev_vars <- instDFunConstraints theta
2104 ; let wevs = [WantedEvVar w loc | w <- ev_vars]
2105 ; return $ GenInst wevs (EvDFunApp dfun_id tys ev_vars) }