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
215 data Inert = IS { class_inerts :: FiniteMap Class Atomics
216 ip_inerts :: FiniteMap Class Atomics
217 tyfun_inerts :: FiniteMap TyCon Atomics
218 tyvar_inerts :: FiniteMap TyVar Atomics
221 Later should we also separate out givens and wanteds?
226 Note [Touchables and givens]
227 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
228 Touchable variables will never show up in givens which are inputs to
229 the solver. However, touchables may show up in givens generated by the flattener.
244 which can be put in the inert set. Suppose we also have a wanted
248 We cannot rewrite the given G alpha ~g b using the wanted alpha ~w
249 Int. Instead, after reacting alpha ~w Int with the whole inert set,
250 we observe that we can solve it by unifying alpha with Int, so we mark
251 it as solved and put it back in the *work list*. [We also immediately unify
252 alpha := Int, without telling anyone, see trySpontaneousSolve function, to
253 avoid doing this in the end.]
255 Later, because it is solved (given, in effect), we can use it to rewrite
256 G alpha ~g b to G Int ~g b, which gets put back in the work list. Eventually,
257 we will dispatch the remaining wanted constraints using the top-level axioms.
259 Finally, note that after reacting a wanted equality with the entire inert set
260 we may end up with something like
264 which we should flip around to generate the solved constraint alpha ~s b.
266 %*********************************************************************
268 * Main Interaction Solver *
270 **********************************************************************
274 1. Canonicalise (unary)
275 2. Pairwise interaction (binary)
276 * Take one from work list
277 * Try all pair-wise interactions with each constraint in inert
279 As an optimisation, we prioritize the equalities both in the
280 worklist and in the inerts.
282 3. Try to solve spontaneously for equalities involving touchables
283 4. Top-level interaction (binary wrt top-level)
284 Superclass decomposition belongs in (4), see note [Superclasses]
287 type AtomicInert = CanonicalCt -- constraint pulled from InertSet
288 type WorkItem = CanonicalCt -- constraint pulled from WorkList
290 -- A mixture of Given, Wanted, and Derived constraints.
291 -- We split between equalities and the rest to process equalities first.
292 type WorkList = CanonicalCts
293 type SWorkList = WorkList -- A worklist of solved
295 unionWorkLists :: WorkList -> WorkList -> WorkList
296 unionWorkLists = andCCan
298 isEmptyWorkList :: WorkList -> Bool
299 isEmptyWorkList = isEmptyCCan
301 emptyWorkList :: WorkList
302 emptyWorkList = emptyCCan
304 workListFromCCan :: CanonicalCt -> WorkList
305 workListFromCCan = singleCCan
307 ------------------------
309 = Stop -- Work item is consumed
310 | ContinueWith WorkItem -- Not consumed
312 instance Outputable StopOrContinue where
313 ppr Stop = ptext (sLit "Stop")
314 ppr (ContinueWith w) = ptext (sLit "ContinueWith") <+> ppr w
316 -- Results after interacting a WorkItem as far as possible with an InertSet
318 = SR { sr_inerts :: InertSet
319 -- The new InertSet to use (REPLACES the old InertSet)
320 , sr_new_work :: WorkList
321 -- Any new work items generated (should be ADDED to the old WorkList)
323 -- sr_stop = Just workitem => workitem is *not* in sr_inerts and
324 -- workitem is inert wrt to sr_inerts
325 , sr_stop :: StopOrContinue
328 instance Outputable StageResult where
329 ppr (SR { sr_inerts = inerts, sr_new_work = work, sr_stop = stop })
330 = ptext (sLit "SR") <+>
331 braces (sep [ ptext (sLit "inerts =") <+> ppr inerts <> comma
332 , ptext (sLit "new work =") <+> ppr work <> comma
333 , ptext (sLit "stop =") <+> ppr stop])
335 type SimplifierStage = WorkItem -> InertSet -> TcS StageResult
337 -- Combine a sequence of simplifier 'stages' to create a pipeline
338 runSolverPipeline :: [(String, SimplifierStage)]
339 -> InertSet -> WorkItem
340 -> TcS (InertSet, WorkList)
341 -- Precondition: non-empty list of stages
342 runSolverPipeline pipeline inerts workItem
343 = do { traceTcS "Start solver pipeline" $
344 vcat [ ptext (sLit "work item =") <+> ppr workItem
345 , ptext (sLit "inerts =") <+> ppr inerts]
347 ; let itr_in = SR { sr_inerts = inerts
348 , sr_new_work = emptyWorkList
349 , sr_stop = ContinueWith workItem }
350 ; itr_out <- run_pipeline pipeline itr_in
352 = case sr_stop itr_out of
353 Stop -> sr_inerts itr_out
354 ContinueWith item -> sr_inerts itr_out `updInertSet` item
355 ; return (new_inert, sr_new_work itr_out) }
357 run_pipeline :: [(String, SimplifierStage)]
358 -> StageResult -> TcS StageResult
359 run_pipeline [] itr = return itr
360 run_pipeline _ itr@(SR { sr_stop = Stop }) = return itr
362 run_pipeline ((name,stage):stages)
363 (SR { sr_new_work = accum_work
365 , sr_stop = ContinueWith work_item })
366 = do { itr <- stage work_item inerts
367 ; traceTcS ("Stage result (" ++ name ++ ")") (ppr itr)
368 ; let itr' = itr { sr_new_work = accum_work `unionWorkLists` sr_new_work itr }
369 ; run_pipeline stages itr' }
373 Inert: {c ~ d, F a ~ t, b ~ Int, a ~ ty} (all given)
374 Reagent: a ~ [b] (given)
376 React with (c~d) ==> IR (ContinueWith (a~[b])) True []
377 React with (F a ~ t) ==> IR (ContinueWith (a~[b])) False [F [b] ~ t]
378 React with (b ~ Int) ==> IR (ContinueWith (a~[Int]) True []
381 Inert: {c ~w d, F a ~g t, b ~w Int, a ~w ty}
384 React with (c ~w d) ==> IR (ContinueWith (a~[b])) True []
385 React with (F a ~g t) ==> IR (ContinueWith (a~[b])) True [] (can't rewrite given with wanted!)
389 Inert: {a ~ Int, F Int ~ b} (given)
390 Reagent: F a ~ b (wanted)
392 React with (a ~ Int) ==> IR (ContinueWith (F Int ~ b)) True []
393 React with (F Int ~ b) ==> IR Stop True [] -- after substituting we re-canonicalize and get nothing
396 -- Main interaction solver: we fully solve the worklist 'in one go',
397 -- returning an extended inert set.
399 -- See Note [Touchables and givens].
400 solveInteract :: InertSet -> CanonicalCts -> TcS InertSet
401 solveInteract inert ws
402 = do { dyn_flags <- getDynFlags
403 ; solveInteractWithDepth (ctxtStkDepth dyn_flags,0,[]) inert ws
405 solveOne :: InertSet -> WorkItem -> TcS InertSet
406 solveOne inerts workItem
407 = do { dyn_flags <- getDynFlags
408 ; solveOneWithDepth (ctxtStkDepth dyn_flags,0,[]) inerts workItem
412 solveInteractWithDepth :: (Int, Int, [WorkItem])
413 -> InertSet -> WorkList -> TcS InertSet
414 solveInteractWithDepth ctxt@(max_depth,n,stack) inert ws
419 = solverDepthErrorTcS n stack
422 = do { traceTcS "solveInteractWithDepth" $
423 vcat [ text "Current depth =" <+> ppr n
424 , text "Max depth =" <+> ppr max_depth ]
426 -- Solve equalities first
427 ; let (eqs, non_eqs) = Bag.partitionBag isTyEqCCan ws
428 ; is_from_eqs <- Bag.foldlBagM (solveOneWithDepth ctxt) inert eqs
429 ; Bag.foldlBagM (solveOneWithDepth ctxt) is_from_eqs non_eqs }
432 -- Fully interact the given work item with an inert set, and return a
433 -- new inert set which has assimilated the new information.
434 solveOneWithDepth :: (Int, Int, [WorkItem])
435 -> InertSet -> WorkItem -> TcS InertSet
436 solveOneWithDepth (max_depth, n, stack) inert work
437 = do { traceTcS0 (indent ++ "Solving {") (ppr work)
438 ; (new_inert, new_work) <- runSolverPipeline thePipeline inert work
440 ; traceTcS0 (indent ++ "Subgoals:") (ppr new_work)
442 -- Recursively solve the new work generated
443 -- from workItem, with a greater depth
444 ; res_inert <- solveInteractWithDepth (max_depth, n+1, work:stack)
447 ; traceTcS0 (indent ++ "Done }") (ppr work)
450 indent = replicate (2*n) ' '
452 thePipeline :: [(String,SimplifierStage)]
453 thePipeline = [ ("interact with inert eqs", interactWithInertEqsStage)
454 , ("interact with inerts", interactWithInertsStage)
455 , ("spontaneous solve", spontaneousSolveStage)
456 , ("top-level reactions", topReactionsStage) ]
459 *********************************************************************************
461 The spontaneous-solve Stage
463 *********************************************************************************
465 Note [Efficient Orientation]
466 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
468 There are two cases where we have to be careful about
469 orienting equalities to get better efficiency.
471 Case 2: In Rewriting Equalities (function rewriteEqLHS)
473 When rewriting two equalities with the same LHS:
476 We have a choice of producing work (xi1 ~ xi2) (up-to the
477 canonicalization invariants) However, to prevent the inert items
478 from getting kicked out of the inerts first, we prefer to
479 canonicalize (xi1 ~ xi2) if (b) comes from the inert set, or (xi2
480 ~ xi1) if (a) comes from the inert set.
482 This choice is implemented using the WhichComesFromInert flag.
484 Case 2: In Spontaneous Solving
486 Inerts: [w1] : D alpha
490 Untouchables = [beta]
491 Then a wanted (beta ~ alpha) comes along.
492 1) While interacting with the inerts it is going to kick w2,w4
494 2) Then, it will spontaneoulsy be solved by (alpha := beta)
495 3) Now (and here is the tricky part), to add him back as
496 solved (alpha ~ beta) is no good because, in the next
497 iteration, it will kick out w1,w3 as well so we will end up
498 with *all* the inert equalities back in the worklist!
500 So it is tempting to just add (beta ~ alpha) instead, that is,
501 maintain the original orietnation of the constraint.
503 But that does not work very well, because it may cause the
504 "double unification problem" (See Note [Avoid double unifications]).
511 At the end of the interaction suppose we spontaneously solve alpha := fsk1
512 but keep [Given] fsk1 ~ alpha. Then, the second time around we see the
513 constraint (fsk2 ~ alpha), and we unify *again* alpha := fsk2, which is wrong.
515 Our conclusion is that, while in some cases (Example 2a), it makes sense to
516 preserve the original orientation, it is hard to do this in a sound way.
517 So we *don't* do this for now, @solveWithIdentity@ outputs a constraint that
518 is oriented with the unified variable on the left.
520 Case 3: Functional Dependencies and IP improvement work
521 TODO. Optimisation not yet implemented there.
524 spontaneousSolveStage :: SimplifierStage
525 spontaneousSolveStage workItem inerts
526 = do { mSolve <- trySpontaneousSolve workItem inerts
528 Nothing -> -- no spontaneous solution for him, keep going
529 return $ SR { sr_new_work = emptyWorkList
531 , sr_stop = ContinueWith workItem }
533 Just (workItem', workList')
534 | not (isGivenCt workItem) -- Original was wanted or derived but we have now made him
535 -- given so we have to interact him with the inerts due to
536 -- its status change. This in turn may produce more work.
537 -> do { (new_inert, new_work) <- runSolverPipeline [ ("recursive interact with inert eqs", interactWithInertEqsStage)
538 , ("recursive interact with inerts", interactWithInertsStage)
540 ; return $ SR { sr_new_work = new_work `unionWorkLists` workList'
541 , sr_inerts = new_inert -- will include workItem'
545 -> -- Original was given; he must then be inert all right, and
546 -- workList' are all givens from flattening
547 return $ SR { sr_new_work = workList'
548 , sr_inerts = inerts `updInertSet` workItem'
552 -- @trySpontaneousSolve wi@ solves equalities where one side is a
553 -- touchable unification variable. Returns:
554 -- * Nothing if we were not able to solve it
555 -- * Just wi' if we solved it, wi' (now a "given") should be put in the work list.
556 -- See Note [Touchables and givens]
557 -- NB: just passing the inerts through for the skolem equivalence classes
558 trySpontaneousSolve :: WorkItem -> InertSet -> TcS (Maybe (WorkItem, SWorkList))
559 trySpontaneousSolve workItem@(CTyEqCan { cc_id = cv, cc_flavor = gw, cc_tyvar = tv1, cc_rhs = xi }) inerts
562 | Just tv2 <- tcGetTyVar_maybe xi
563 = do { tch1 <- isTouchableMetaTyVar tv1
564 ; tch2 <- isTouchableMetaTyVar tv2
565 ; case (tch1, tch2) of
566 (True, True) -> trySpontaneousEqTwoWay inerts cv gw tv1 tv2
567 (True, False) -> trySpontaneousEqOneWay inerts cv gw tv1 xi
568 (False, True) -> trySpontaneousEqOneWay inerts cv gw tv2 (mkTyVarTy tv1)
569 _ -> return Nothing }
571 = do { tch1 <- isTouchableMetaTyVar tv1
572 ; if tch1 then trySpontaneousEqOneWay inerts cv gw tv1 xi
573 else do { traceTcS "Untouchable LHS, can't spontaneously solve workitem:" (ppr workItem)
578 -- trySpontaneousSolve (CFunEqCan ...) = ...
579 -- See Note [No touchables as FunEq RHS] in TcSMonad
580 trySpontaneousSolve _ _ = return Nothing
583 trySpontaneousEqOneWay :: InertSet -> CoVar -> CtFlavor -> TcTyVar -> Xi
584 -> TcS (Maybe (WorkItem,SWorkList))
585 -- tv is a MetaTyVar, not untouchable
586 trySpontaneousEqOneWay inerts cv gw tv xi
587 | not (isSigTyVar tv) || isTyVarTy xi
588 = do { kxi <- zonkTcTypeTcS xi >>= return . typeKind -- Must look through the TcTyBinds
589 -- hence kxi and not typeKind xi
590 -- See Note [Kind Errors]
591 ; if kxi `isSubKind` tyVarKind tv then
592 solveWithIdentity inerts cv gw tv xi
593 else if tyVarKind tv `isSubKind` kxi then
594 return Nothing -- kinds are compatible but we can't solveWithIdentity this way
595 -- This case covers the a_touchable :: * ~ b_untouchable :: ??
596 -- which has to be deferred or floated out for someone else to solve
597 -- it in a scope where 'b' is no longer untouchable.
598 else kindErrorTcS gw (mkTyVarTy tv) xi -- See Note [Kind errors]
600 | otherwise -- Still can't solve, sig tyvar and non-variable rhs
604 trySpontaneousEqTwoWay :: InertSet -> CoVar -> CtFlavor -> TcTyVar -> TcTyVar
605 -> TcS (Maybe (WorkItem,SWorkList))
606 -- Both tyvars are *touchable* MetaTyvars so there is only a chance for kind error here
607 trySpontaneousEqTwoWay inerts cv gw tv1 tv2
609 , nicer_to_update_tv2 = solveWithIdentity inerts cv gw tv2 (mkTyVarTy tv1)
611 = solveWithIdentity inerts cv gw tv1 (mkTyVarTy tv2)
612 | otherwise -- None is a subkind of the other, but they are both touchable!
613 = kindErrorTcS gw (mkTyVarTy tv1) (mkTyVarTy tv2) -- See Note [Kind errors]
617 nicer_to_update_tv2 = isSigTyVar tv1 || isSystemName (Var.varName tv2)
621 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
622 Consider the wanted problem:
623 alpha ~ (# Int, Int #)
624 where alpha :: ?? and (# Int, Int #) :: (#). We can't spontaneously solve this constraint,
625 but we should rather reject the program that give rise to it. If 'trySpontaneousEqTwoWay'
626 simply returns @Nothing@ then that wanted constraint is going to propagate all the way and
627 get quantified over in inference mode. That's bad because we do know at this point that the
628 constraint is insoluble. Instead, we call 'kindErrorTcS' here, which immediately fails.
630 The same applies in canonicalization code in case of kind errors in the givens.
632 However, when we canonicalize givens we only check for compatibility (@compatKind@).
633 If there were a kind error in the givens, this means some form of inconsistency or dead code.
635 When we spontaneously solve wanteds we may have to look through the bindings, hence we
636 call zonkTcTypeTcS above. The reason is that maybe xi is @alpha@ where alpha :: ? and
637 a previous spontaneous solving has set (alpha := f) with (f :: *). The reason that xi is
638 still alpha and not f is becasue the solved constraint may be oriented as (f ~ alpha) instead
639 of (alpha ~ f). Then we should be using @xi@s "real" kind, which is * and not ?, when we try
640 to detect whether spontaneous solving is possible.
643 Note [Spontaneous solving and kind compatibility]
644 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
646 Note that our canonical constraints insist that only *given* equalities (tv ~ xi)
647 or (F xis ~ rhs) require the LHS and the RHS to have exactly the same kinds.
649 - We have to require this because:
650 Given equalities can be freely used to rewrite inside
651 other types or constraints.
652 - We do not have to do the same for wanteds because:
653 First, wanted equations (tv ~ xi) where tv is a touchable
654 unification variable may have kinds that do not agree (the
655 kind of xi must be a sub kind of the kind of tv). Second, any
656 potential kind mismatch will result in the constraint not
657 being soluble, which will be reported anyway. This is the
658 reason that @trySpontaneousOneWay@ and @trySpontaneousTwoWay@
659 will perform a kind compatibility check, and only then will
660 they proceed to @solveWithIdentity@.
663 - Givens from higher-rank, such as:
664 type family T b :: * -> * -> *
665 type instance T Bool = (->)
667 f :: forall a. ((T a ~ (->)) => ...) -> a -> ...
669 Whereas we would be able to apply the type instance, we would not be able to
670 use the given (T Bool ~ (->)) in the body of 'flop'
672 Note [Loopy Spontaneous Solving]
673 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
675 Example 1: [The problem of loopy spontaneous solving]
677 Consider the original wanted:
678 wanted : Maybe (E alpha) ~ alpha
679 where E is a type family, such that E (T x) = x. After canonicalization,
680 as a result of flattening, we will get:
681 given : E alpha ~ fsk
682 wanted : alpha ~ Maybe fsk
683 where (fsk := E alpha, on the side). Now, if we spontaneously *solve*
684 (alpha := Maybe fsk) we are in trouble! Instead, we should refrain from solving
685 it and keep it as wanted. In inference mode we'll end up quantifying over
686 (alpha ~ Maybe (E alpha))
687 Hence, 'solveWithIdentity' performs a small occurs check before
688 actually solving. But this occurs check *must look through* flatten skolems.
690 However, it may be the case that the flatten skolem in hand is equal to some other
691 flatten skolem whith *does not* mention our unification variable. Here's a typical example:
693 Example 2: [The need of keeping track of flatten skolem equivalence classes]
698 After canonicalization:
703 After some reactions:
708 At this point, we will try to spontaneously solve (alpha ~ f2) which remains as yet unsolved.
709 We will look inside f2, which immediately mentions (F alpha), so it's not good to unify! However
710 by looking at the equivalence class of the flatten skolems, we can see that it is fine to
711 unify (alpha ~ f1) which solves our goals!
713 Example 3: [The need of looking through TyBinds for already spontaneously solved variables]
715 A similar problem happens because of other spontaneous solving. Suppose we have the
716 following wanteds, arriving in this exact order:
717 (first) w: beta ~ alpha
718 (second) w: alpha ~ fsk
719 (third) g: F beta ~ fsk
720 Then, we first spontaneously solve the first constraint, making (beta := alpha), and having
721 (beta ~ alpha) as given. *Then* we encounter the second wanted (alpha ~ fsk). "fsk" does not
722 obviously mention alpha, so naively we can also spontaneously solve (alpha := fsk). But
723 that is wrong since fsk mentions beta, which has already secretly been unified to alpha!
725 To avoid this problem, the same occurs check must unveil rewritings that can happen because
726 of spontaneously having solved other constraints.
728 Example 4: [Orientation of (tv ~ xi) equalities]
730 We orient equalities (tv ~ xi) so that flatten skolems appear on the left, if possible. Here
731 is an example of why this is needed:
733 [Wanted] w1: alpha ~ fsk
734 [Given] g1: F alpha ~ fsk
736 Flatten skolem equivalence class = []
738 Assume that g2 is *not* oriented properly, as shown above. Then we would like to spontaneously
739 solve w1 but we can't set alpha := fsk, since fsk hides the type F alpha. However, by using
740 the equation g2 it would be possible to solve w1 by setting alpha := b. In other words, it is
741 not enough to look at a flatten skolem equivalence class to try to find alternatives to unify
742 with. We may have to go to other variables.
744 By orienting the equalities so that flatten skolems are in the LHS we are eliminating them
745 as much as possible from the RHS of other wanted equalities, and hence it suffices to look
746 in their flatten skolem equivalence classes.
748 NB: This situation appears in the IndTypesPerf test case, inside indexed-types/.
750 Caveat: You may wonder if we should be doing this for unification variables as well.
751 However, Note [Efficient Orientation], Case 2, demonstrates that this is not possible
752 at least for touchable unification variables which we have to keep oriented with the
753 touchable on the LHS to be able to eliminate it. So then, what about untouchables?
757 Untouchable = beta, Touchable = alpha
759 [Wanted] w1: alpha ~ fsk
760 [Given] g1: F alpha ~ fsk
761 [Given] g2: beta ~ fsk
762 Flatten skolem equivalence class = []
764 Should we be able to unify alpha := beta to solve the constraint? Arguably yes, but
765 that implies that an *untouchable* unification variable (beta) is in the same equivalence
766 class as a flatten skolem that mentions @alpha@. I.e. g2 means that:
768 But I do not think that there is any way to produce evidence for such a constraint from
769 the outside other than beta := F alpha, which violates the OutsideIn-ness.
773 Note [Avoid double unifications]
774 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
775 The spontaneous solver has to return a given which mentions the unified unification
776 variable *on the left* of the equality. Here is what happens if not:
777 Original wanted: (a ~ alpha), (alpha ~ Int)
778 We spontaneously solve the first wanted, without changing the order!
779 given : a ~ alpha [having unified alpha := a]
780 Now the second wanted comes along, but he cannot rewrite the given, so we simply continue.
781 At the end we spontaneously solve that guy, *reunifying* [alpha := Int]
783 We avoid this problem by orienting the given so that the unification
784 variable is on the left. [Note that alternatively we could attempt to
785 enforce this at canonicalization]
787 See also Note [No touchables as FunEq RHS] in TcSMonad; avoiding
788 double unifications is the main reason we disallow touchable
789 unification variables as RHS of type family equations: F xis ~ alpha.
793 solveWithIdentity :: InertSet
794 -> CoVar -> CtFlavor -> TcTyVar -> Xi
795 -> TcS (Maybe (WorkItem, SWorkList))
796 -- Solve with the identity coercion
797 -- Precondition: kind(xi) is a sub-kind of kind(tv)
798 -- Precondition: CtFlavor is Wanted or Derived
799 -- See [New Wanted Superclass Work] to see why solveWithIdentity
800 -- must work for Derived as well as Wanted
801 -- Returns: (workItem, workList) where
802 -- workItem = the new Given constraint
803 -- workList = some additional work that may have been produced as a result of flattening
804 -- in case we did some chasing through flatten skolem equivalence classes.
805 solveWithIdentity inerts cv gw tv xi
806 = do { tybnds <- getTcSTyBindsMap
807 ; case occurCheck tybnds inerts tv xi of
808 Nothing -> return Nothing
809 Just (xi_unflat,coi) -> solve_with xi_unflat coi }
811 solve_with xi_unflat coi -- coi : xi_unflat ~ xi
812 = do { traceTcS "Sneaky unification:" $
813 vcat [text "Coercion variable: " <+> ppr gw,
814 text "Coercion: " <+> pprEq (mkTyVarTy tv) xi,
815 text "Left Kind is : " <+> ppr (typeKind (mkTyVarTy tv)),
816 text "Right Kind is : " <+> ppr (typeKind xi)
819 ; setWantedTyBind tv xi_unflat -- Set tv := xi_unflat
820 ; cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi_unflat xi_unflat
821 ; let flav = mkGivenFlavor gw UnkSkol
822 ; (ct,cts, co) <- case coi of
823 ACo co -> do { (cc,ccs) <- canEqLeafTyVarLeft flav cv_given tv xi_unflat
824 ; return (cc, ccs, co) }
825 IdCo co -> return $ (CTyEqCan { cc_id = cv_given
826 , cc_flavor = mkGivenFlavor gw UnkSkol
827 , cc_tyvar = tv, cc_rhs = xi }
828 -- xi, *not* xi_unflat because
829 -- xi_unflat may require flattening!
832 Wanted {} -> setWantedCoBind cv co
833 Derived {} -> setDerivedCoBind cv co
834 _ -> pprPanic "Can't spontaneously solve *given*" empty
835 -- See Note [Avoid double unifications]
836 ; return $ Just (ct,cts)
839 -- ; let flav = mkGivenFlavor gw UnkSkol
840 -- ; (cts, co) <- case coi of
841 -- -- TODO: Optimise this, along the way it used to be
842 -- ACo co -> do { cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi_unflat xi_unflat
843 -- ; setWantedTyBind tv xi_unflat
844 -- ; can_eqs <- canEq flav cv_given (mkTyVarTy tv) xi_unflat
845 -- ; return (can_eqs, co) }
846 -- IdCo co -> do { cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi xi
847 -- ; setWantedTyBind tv xi
848 -- ; can_eqs <- canEq flav cv_given (mkTyVarTy tv) xi
849 -- ; return (can_eqs, co) }
851 -- Wanted {} -> setWantedCoBind cv co
852 -- Derived {} -> setDerivedCoBind cv co
853 -- _ -> pprPanic "Can't spontaneously solve *given*" empty
854 -- -- See Note [Avoid double unifications]
855 -- ; return $ Just cts }
857 occurCheck :: VarEnv (TcTyVar, TcType) -> InertSet
858 -> TcTyVar -> TcType -> Maybe (TcType,CoercionI)
859 -- Traverse @ty@ to make sure that @tv@ does not appear under some flatten skolem.
860 -- If it appears under some flatten skolem look in that flatten skolem equivalence class
861 -- (see Note [InertSet FlattenSkolemEqClass], [Loopy Spontaneous Solving]) to see if you
862 -- can find a different flatten skolem to use, that is, one that does not mention @tv@.
864 -- Postcondition: Just (ty', coi) = occurCheck binds inerts tv ty
866 -- NB: The returned type ty' may not be flat!
868 occurCheck ty_binds inerts the_tv the_ty
869 = ok emptyVarSet the_ty
871 -- If (fsk `elem` bad) then tv occurs in any rendering
872 -- of the type under the expansion of fsk
873 ok bad this_ty@(TyConApp tc tys)
874 | Just tys_cois <- allMaybes (map (ok bad) tys)
875 , (tys',cois') <- unzip tys_cois
876 = Just (TyConApp tc tys', mkTyConAppCoI tc cois')
877 | isSynTyCon tc, Just ty_expanded <- tcView this_ty
878 = ok bad ty_expanded -- See Note [Type synonyms and the occur check] in TcUnify
880 | Just (sty',coi) <- ok_pred bad sty
881 = Just (PredTy sty', coi)
882 ok bad (FunTy arg res)
883 | Just (arg', coiarg) <- ok bad arg, Just (res', coires) <- ok bad res
884 = Just (FunTy arg' res', mkFunTyCoI coiarg coires)
885 ok bad (AppTy fun arg)
886 | Just (fun', coifun) <- ok bad fun, Just (arg', coiarg) <- ok bad arg
887 = Just (AppTy fun' arg', mkAppTyCoI coifun coiarg)
888 ok bad (ForAllTy tv1 ty1)
889 -- WARNING: What if it is a (t1 ~ t2) => t3? It's not handled properly at the moment.
890 | Just (ty1', coi) <- ok bad ty1
891 = Just (ForAllTy tv1 ty1', mkForAllTyCoI tv1 coi)
894 ok bad this_ty@(TyVarTy tv)
895 | tv == the_tv = Nothing -- Occurs check error
896 | not (isTcTyVar tv) = Just (this_ty, IdCo this_ty) -- Bound var
897 | FlatSkol zty <- tcTyVarDetails tv = ok_fsk bad tv zty
898 | Just (_,ty) <- lookupVarEnv ty_binds tv = ok bad ty
899 | otherwise = Just (this_ty, IdCo this_ty)
901 -- Check if there exists a ty bind already, as a result of sneaky unification.
903 ok _bad _ty = Nothing
906 ok_pred bad (ClassP cn tys)
907 | Just tys_cois <- allMaybes $ map (ok bad) tys
908 = let (tys', cois') = unzip tys_cois
909 in Just (ClassP cn tys', mkClassPPredCoI cn cois')
910 ok_pred bad (IParam nm ty)
911 | Just (ty',co') <- ok bad ty
912 = Just (IParam nm ty', mkIParamPredCoI nm co')
913 ok_pred bad (EqPred ty1 ty2)
914 | Just (ty1',coi1) <- ok bad ty1, Just (ty2',coi2) <- ok bad ty2
915 = Just (EqPred ty1' ty2', mkEqPredCoI coi1 coi2)
916 ok_pred _ _ = Nothing
920 | fsk `elemVarSet` bad
921 -- We are already trying to find a rendering of fsk,
922 -- and to do that it seems we need a rendering, so fail
925 = firstJusts (ok new_bad zty : map (go_under_fsk new_bad) fsk_equivs)
927 fsk_equivs = getFskEqClass inerts fsk
928 new_bad = bad `extendVarSetList` (fsk : map fst fsk_equivs)
931 go_under_fsk bad_tvs (fsk,co)
932 | FlatSkol zty <- tcTyVarDetails fsk
933 = case ok bad_tvs zty of
935 Just (ty,coi') -> Just (ty, mkTransCoI coi' (ACo co))
936 | otherwise = pprPanic "go_down_equiv" (ppr fsk)
940 *********************************************************************************
942 The interact-with-inert Stage
944 *********************************************************************************
947 -- Interaction result of WorkItem <~> AtomicInert
949 = IR { ir_stop :: StopOrContinue
951 -- => Reagent (work item) consumed.
952 -- ContinueWith new_reagent
953 -- => Reagent transformed but keep gathering interactions.
954 -- The transformed item remains inert with respect
955 -- to any previously encountered inerts.
957 , ir_inert_action :: InertAction
958 -- Whether the inert item should remain in the InertSet.
960 , ir_new_work :: WorkList
961 -- new work items to add to the WorkList
963 , ir_improvement :: Maybe FDImprovement -- In case improvement kicked in
966 -- What to do with the inert reactant.
967 data InertAction = KeepInert | DropInert
970 mkIRContinue :: Monad m => WorkItem -> InertAction -> WorkList -> m InteractResult
971 mkIRContinue wi keep newWork = return $ IR (ContinueWith wi) keep newWork Nothing
973 mkIRStop :: Monad m => InertAction -> WorkList -> m InteractResult
974 mkIRStop keep newWork = return $ IR Stop keep newWork Nothing
976 mkIRStop_RecordImprovement :: Monad m => InertAction -> WorkList -> FDImprovement -> m InteractResult
977 mkIRStop_RecordImprovement keep newWork fdimpr = return $ IR Stop keep newWork (Just fdimpr)
980 dischargeWorkItem :: Monad m => m InteractResult
981 dischargeWorkItem = mkIRStop KeepInert emptyWorkList
983 noInteraction :: Monad m => WorkItem -> m InteractResult
984 noInteraction workItem = mkIRContinue workItem KeepInert emptyWorkList
986 data WhichComesFromInert = LeftComesFromInert | RightComesFromInert
987 -- See Note [Efficient Orientation, Case 2]
990 ---------------------------------------------------
991 -- Interact a single WorkItem with the equalities of an inert set as far as possible, i.e. until we
992 -- get a Stop result from an individual reaction (i.e. when the WorkItem is consumed), or until we've
993 -- interact the WorkItem with the entire equalities of the InertSet
995 interactWithInertEqsStage :: SimplifierStage
996 interactWithInertEqsStage workItem inert
997 = foldISEqCtsM interactNext initITR inert
998 where initITR = SR { sr_inerts = IS { inert_eqs = emptyCCan -- We will fold over the equalities
999 , inert_fsks = Map.empty -- which will generate those two again
1000 , inert_cts = inert_cts inert
1001 , inert_fds = inert_fds inert
1003 , sr_new_work = emptyWorkList
1004 , sr_stop = ContinueWith workItem }
1007 ---------------------------------------------------
1008 -- Interact a single WorkItem with *non-equality* constraints in the inert set.
1009 -- Precondition: equality interactions must have already happened, hence we have
1010 -- to pick up some information from the incoming inert, before folding over the
1011 -- "Other" constraints it contains!
1012 interactWithInertsStage :: SimplifierStage
1013 interactWithInertsStage workItem inert
1014 = foldISOtherCtsM interactNext initITR inert
1016 initITR = SR { -- Pick up: (1) equations, (2) FD improvements, (3) FlatSkol equiv. classes
1017 sr_inerts = IS { inert_eqs = inert_eqs inert
1018 , inert_cts = emptyCCan
1019 , inert_fds = inert_fds inert
1020 , inert_fsks = inert_fsks inert }
1021 , sr_new_work = emptyWorkList
1022 , sr_stop = ContinueWith workItem }
1024 interactNext :: StageResult -> AtomicInert -> TcS StageResult
1025 interactNext it inert
1026 | ContinueWith workItem <- sr_stop it
1027 = do { let inerts = sr_inerts it
1028 fdimprs_old = getFDImprovements inerts
1030 ; ir <- interactWithInert fdimprs_old inert workItem
1032 -- New inerts depend on whether we KeepInert or not and must
1033 -- be updated with FD improvement information from the interaction result (ir)
1034 ; let inerts_new = updInertSetFDImprs upd_inert (ir_improvement ir)
1035 upd_inert = if ir_inert_action ir == KeepInert
1036 then inerts `updInertSet` inert else inerts
1038 ; return $ SR { sr_inerts = inerts_new
1039 , sr_new_work = sr_new_work it `unionWorkLists` ir_new_work ir
1040 , sr_stop = ir_stop ir } }
1042 = return $ it { sr_inerts = (sr_inerts it) `updInertSet` inert }
1044 -- Do a single interaction of two constraints.
1045 interactWithInert :: FDImprovements -> AtomicInert -> WorkItem -> TcS InteractResult
1046 interactWithInert fdimprs inert workitem
1047 = do { ctxt <- getTcSContext
1048 ; let is_allowed = allowedInteraction (simplEqsOnly ctxt) inert workitem
1049 inert_ev = cc_id inert
1050 work_ev = cc_id workitem
1052 -- Never interact a wanted and a derived where the derived's evidence
1053 -- mentions the wanted evidence in an unguarded way.
1054 -- See Note [Superclasses and recursive dictionaries]
1055 -- and Note [New Wanted Superclass Work]
1056 -- We don't have to do this for givens, as we fully know the evidence for them.
1058 case (cc_flavor inert, cc_flavor workitem) of
1059 (Wanted loc, Derived {}) -> isGoodRecEv work_ev (WantedEvVar inert_ev loc)
1060 (Derived {}, Wanted loc) -> isGoodRecEv inert_ev (WantedEvVar work_ev loc)
1063 ; if is_allowed && rec_ev_ok then
1064 doInteractWithInert fdimprs inert workitem
1066 noInteraction workitem
1069 allowedInteraction :: Bool -> AtomicInert -> WorkItem -> Bool
1070 -- Allowed interactions
1071 allowedInteraction eqs_only (CDictCan {}) (CDictCan {}) = not eqs_only
1072 allowedInteraction eqs_only (CIPCan {}) (CIPCan {}) = not eqs_only
1073 allowedInteraction _ _ _ = True
1075 --------------------------------------------
1076 doInteractWithInert :: FDImprovements -> CanonicalCt -> CanonicalCt -> TcS InteractResult
1077 -- Identical class constraints.
1079 doInteractWithInert fdimprs
1080 (CDictCan { cc_id = d1, cc_flavor = fl1, cc_class = cls1, cc_tyargs = tys1 })
1081 workItem@(CDictCan { cc_id = d2, cc_flavor = fl2, cc_class = cls2, cc_tyargs = tys2 })
1082 | cls1 == cls2 && (and $ zipWith tcEqType tys1 tys2)
1083 = solveOneFromTheOther (d1,fl1) workItem
1085 | cls1 == cls2 && (not (isGiven fl1 && isGiven fl2))
1086 = -- See Note [When improvement happens]
1087 do { let pty1 = ClassP cls1 tys1
1088 pty2 = ClassP cls2 tys2
1089 work_item_pred_loc = (pty2, ppr d2)
1090 inert_pred_loc = (pty1, ppr d1)
1091 loc = combineCtLoc fl1 fl2
1092 eqn_pred_locs = improveFromAnother work_item_pred_loc inert_pred_loc
1094 ; wevvars <- mkWantedFunDepEqns loc eqn_pred_locs
1095 ; fd_work <- canWanteds wevvars
1096 -- See Note [Generating extra equalities]
1097 ; traceTcS "Checking if improvements existed." (ppr fdimprs)
1098 ; if isEmptyWorkList fd_work || haveBeenImproved fdimprs pty1 pty2 then
1100 mkIRContinue workItem KeepInert fd_work
1101 else do { traceTcS "Recording improvement and throwing item back in worklist." (ppr (pty1,pty2))
1102 ; mkIRStop_RecordImprovement KeepInert
1103 (fd_work `unionWorkLists` workListFromCCan workItem) (pty1,pty2)
1105 -- See Note [FunDep Reactions]
1108 -- Class constraint and given equality: use the equality to rewrite
1109 -- the class constraint.
1110 doInteractWithInert _fdimprs
1111 (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi })
1112 (CDictCan { cc_id = dv, cc_flavor = wfl, cc_class = cl, cc_tyargs = xis })
1113 | ifl `canRewrite` wfl
1114 , tv `elemVarSet` tyVarsOfTypes xis
1115 = if isDerivedSC wfl then
1116 mkIRStop KeepInert $ emptyWorkList -- See Note [Adding Derived Superclasses]
1117 else do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,wfl,cl,xis)
1118 -- Continue with rewritten Dictionary because we can only be in the
1119 -- interactWithEqsStage, so the dictionary is inert.
1120 ; mkIRContinue rewritten_dict KeepInert emptyWorkList }
1122 doInteractWithInert _fdimprs
1123 (CDictCan { cc_id = dv, cc_flavor = ifl, cc_class = cl, cc_tyargs = xis })
1124 workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
1125 | wfl `canRewrite` ifl
1126 , tv `elemVarSet` tyVarsOfTypes xis
1127 = if isDerivedSC ifl then
1128 mkIRContinue workItem DropInert emptyWorkList -- No need to do any rewriting,
1129 -- see Note [Adding Derived Superclasses]
1130 else do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,ifl,cl,xis)
1131 ; mkIRContinue workItem DropInert (workListFromCCan rewritten_dict) }
1133 -- Class constraint and given equality: use the equality to rewrite
1134 -- the class constraint.
1135 doInteractWithInert _fdimprs
1136 (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi })
1137 (CIPCan { cc_id = ipid, cc_flavor = wfl, cc_ip_nm = nm, cc_ip_ty = ty })
1138 | ifl `canRewrite` wfl
1139 , tv `elemVarSet` tyVarsOfType ty
1140 = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,wfl,nm,ty)
1141 ; mkIRContinue rewritten_ip KeepInert emptyWorkList }
1143 doInteractWithInert _fdimprs
1144 (CIPCan { cc_id = ipid, cc_flavor = ifl, cc_ip_nm = nm, cc_ip_ty = ty })
1145 workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
1146 | wfl `canRewrite` ifl
1147 , tv `elemVarSet` tyVarsOfType ty
1148 = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,ifl,nm,ty)
1149 ; mkIRContinue workItem DropInert (workListFromCCan rewritten_ip) }
1151 -- Two implicit parameter constraints. If the names are the same,
1152 -- but their types are not, we generate a wanted type equality
1153 -- that equates the type (this is "improvement").
1154 -- However, we don't actually need the coercion evidence,
1155 -- so we just generate a fresh coercion variable that isn't used anywhere.
1156 doInteractWithInert _fdimprs
1157 (CIPCan { cc_id = id1, cc_flavor = ifl, cc_ip_nm = nm1, cc_ip_ty = ty1 })
1158 workItem@(CIPCan { cc_flavor = wfl, cc_ip_nm = nm2, cc_ip_ty = ty2 })
1159 | nm1 == nm2 && isGiven wfl && isGiven ifl
1160 = -- See Note [Overriding implicit parameters]
1161 -- Dump the inert item, override totally with the new one
1162 -- Do not require type equality
1163 mkIRContinue workItem DropInert emptyWorkList
1165 | nm1 == nm2 && ty1 `tcEqType` ty2
1166 = solveOneFromTheOther (id1,ifl) workItem
1169 = -- See Note [When improvement happens]
1170 do { co_var <- newWantedCoVar ty1 ty2
1171 ; let flav = Wanted (combineCtLoc ifl wfl)
1172 ; cans <- mkCanonical flav co_var
1173 ; mkIRContinue workItem KeepInert cans }
1176 -- Inert: equality, work item: function equality
1178 -- Never rewrite a given with a wanted equality, and a type function
1179 -- equality can never rewrite an equality. Note also that if we have
1180 -- F x1 ~ x2 and a ~ x3, and a occurs in x2, we don't rewrite it. We
1181 -- can wait until F x1 ~ x2 matches another F x1 ~ x4, and only then
1182 -- we will ``expose'' x2 and x4 to rewriting.
1184 -- Otherwise, we can try rewriting the type function equality with the equality.
1185 doInteractWithInert _fdimprs
1186 (CTyEqCan { cc_id = cv1, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi1 })
1187 (CFunEqCan { cc_id = cv2, cc_flavor = wfl, cc_fun = tc
1188 , cc_tyargs = args, cc_rhs = xi2 })
1189 | ifl `canRewrite` wfl
1190 , tv `elemVarSet` tyVarsOfTypes args
1191 = do { rewritten_funeq <- rewriteFunEq (cv1,tv,xi1) (cv2,wfl,tc,args,xi2)
1192 ; mkIRStop KeepInert (workListFromCCan rewritten_funeq) }
1193 -- must Stop here, because we may no longer be inert after the rewritting.
1195 -- Inert: function equality, work item: equality
1196 doInteractWithInert _fdimprs
1197 (CFunEqCan {cc_id = cv1, cc_flavor = ifl, cc_fun = tc
1198 , cc_tyargs = args, cc_rhs = xi1 })
1199 workItem@(CTyEqCan { cc_id = cv2, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi2 })
1200 | wfl `canRewrite` ifl
1201 , tv `elemVarSet` tyVarsOfTypes args
1202 = do { rewritten_funeq <- rewriteFunEq (cv2,tv,xi2) (cv1,ifl,tc,args,xi1)
1203 ; mkIRContinue workItem DropInert (workListFromCCan rewritten_funeq) }
1205 doInteractWithInert _fdimprs
1206 (CFunEqCan { cc_id = cv1, cc_flavor = fl1, cc_fun = tc1
1207 , cc_tyargs = args1, cc_rhs = xi1 })
1208 workItem@(CFunEqCan { cc_id = cv2, cc_flavor = fl2, cc_fun = tc2
1209 , cc_tyargs = args2, cc_rhs = xi2 })
1210 | fl1 `canSolve` fl2 && lhss_match
1211 = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
1212 ; mkIRStop KeepInert cans }
1213 | fl2 `canSolve` fl1 && lhss_match
1214 = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
1215 ; mkIRContinue workItem DropInert cans }
1217 lhss_match = tc1 == tc2 && and (zipWith tcEqType args1 args2)
1219 doInteractWithInert _fdimprs
1220 inert@(CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
1221 workItem@(CTyEqCan { cc_id = cv2, cc_flavor = fl2, cc_tyvar = tv2, cc_rhs = xi2 })
1222 -- Check for matching LHS
1223 | fl1 `canSolve` fl2 && tv1 == tv2
1224 = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
1225 ; mkIRStop KeepInert cans }
1227 | fl2 `canSolve` fl1 && tv1 == tv2
1228 = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
1229 ; mkIRContinue workItem DropInert cans }
1231 -- Check for rewriting RHS
1232 | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfType xi2
1233 = do { rewritten_eq <- rewriteEqRHS (cv1,tv1,xi1) (cv2,fl2,tv2,xi2)
1234 ; mkIRStop KeepInert rewritten_eq }
1235 | fl2 `canRewrite` fl1 && tv2 `elemVarSet` tyVarsOfType xi1
1236 = do { rewritten_eq <- rewriteEqRHS (cv2,tv2,xi2) (cv1,fl1,tv1,xi1)
1237 ; mkIRContinue workItem DropInert rewritten_eq }
1239 -- Finally, if workitem is a Flatten Equivalence Class constraint and the
1240 -- inert is a wanted constraint, even when the workitem cannot rewrite the
1241 -- inert, drop the inert out because you may have to reconsider solving the
1242 -- inert *using* the equivalence class you created. See note [Loopy Spontaneous Solving]
1243 -- and [InertSet FlattenSkolemEqClass]
1245 | not $ isGiven fl1, -- The inert is wanted or derived
1246 isMetaTyVar tv1, -- and has a unification variable lhs
1247 FlatSkol {} <- tcTyVarDetails tv2, -- And workitem is a flatten skolem equality
1248 Just tv2' <- tcGetTyVar_maybe xi2, FlatSkol {} <- tcTyVarDetails tv2'
1249 = mkIRContinue workItem DropInert (workListFromCCan inert)
1252 -- Fall-through case for all other situations
1253 doInteractWithInert _fdimprs _ workItem = noInteraction workItem
1255 -------------------------
1256 -- Equational Rewriting
1257 rewriteDict :: (CoVar, TcTyVar, Xi) -> (DictId, CtFlavor, Class, [Xi]) -> TcS CanonicalCt
1258 rewriteDict (cv,tv,xi) (dv,gw,cl,xis)
1259 = do { let cos = substTysWith [tv] [mkCoVarCoercion cv] xis -- xis[tv] ~ xis[xi]
1260 args = substTysWith [tv] [xi] xis
1262 dict_co = mkTyConCoercion con cos
1263 ; dv' <- newDictVar cl args
1265 Wanted {} -> setDictBind dv (EvCast dv' (mkSymCoercion dict_co))
1266 _given_or_derived -> setDictBind dv' (EvCast dv dict_co)
1267 ; return (CDictCan { cc_id = dv'
1270 , cc_tyargs = args }) }
1272 rewriteIP :: (CoVar,TcTyVar,Xi) -> (EvVar,CtFlavor, IPName Name, TcType) -> TcS CanonicalCt
1273 rewriteIP (cv,tv,xi) (ipid,gw,nm,ty)
1274 = do { let ip_co = substTyWith [tv] [mkCoVarCoercion cv] ty -- ty[tv] ~ t[xi]
1275 ty' = substTyWith [tv] [xi] ty
1276 ; ipid' <- newIPVar nm ty'
1278 Wanted {} -> setIPBind ipid (EvCast ipid' (mkSymCoercion ip_co))
1279 _given_or_derived -> setIPBind ipid' (EvCast ipid ip_co)
1280 ; return (CIPCan { cc_id = ipid'
1283 , cc_ip_ty = ty' }) }
1285 rewriteFunEq :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TyCon, [Xi], Xi) -> TcS CanonicalCt
1286 rewriteFunEq (cv1,tv,xi1) (cv2,gw, tc,args,xi2)
1287 = do { let arg_cos = substTysWith [tv] [mkCoVarCoercion cv1] args
1288 args' = substTysWith [tv] [xi1] args
1289 fun_co = mkTyConCoercion tc arg_cos
1290 ; cv2' <- case gw of
1291 Wanted {} -> do { cv2' <- newWantedCoVar (mkTyConApp tc args') xi2
1292 ; setWantedCoBind cv2 $
1293 mkTransCoercion fun_co (mkCoVarCoercion cv2')
1295 _giv_or_der -> newGivOrDerCoVar (mkTyConApp tc args') xi2 $
1296 mkTransCoercion (mkSymCoercion fun_co) (mkCoVarCoercion cv2)
1297 ; return (CFunEqCan { cc_id = cv2'
1304 rewriteEqRHS :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TcTyVar,Xi) -> TcS WorkList
1305 -- Use the first equality to rewrite the second, flavors already checked.
1306 -- E.g. c1 : tv1 ~ xi1 c2 : tv2 ~ xi2
1307 -- rewrites c2 to give
1308 -- c2' : tv2 ~ xi2[xi1/tv1]
1309 -- We must do an occurs check to sure the new constraint is canonical
1310 -- So we might return an empty bag
1311 rewriteEqRHS (cv1,tv1,xi1) (cv2,gw,tv2,xi2)
1312 | Just tv2' <- tcGetTyVar_maybe xi2'
1313 , tv2 == tv2' -- In this case xi2[xi1/tv1] = tv2, so we have tv2~tv2
1314 = do { when (isWanted gw) (setWantedCoBind cv2 (mkSymCoercion co2'))
1315 ; return emptyCCan }
1320 -> do { cv2' <- newWantedCoVar (mkTyVarTy tv2) xi2'
1321 ; setWantedCoBind cv2 $
1322 mkCoVarCoercion cv2' `mkTransCoercion` mkSymCoercion co2'
1325 -> newGivOrDerCoVar (mkTyVarTy tv2) xi2' $
1326 mkCoVarCoercion cv2 `mkTransCoercion` co2'
1328 ; xi2'' <- canOccursCheck gw tv2 xi2' -- we know xi2' is *not* tv2
1329 ; canEq gw cv2' (mkTyVarTy tv2) xi2''
1332 xi2' = substTyWith [tv1] [xi1] xi2
1333 co2' = substTyWith [tv1] [mkCoVarCoercion cv1] xi2 -- xi2 ~ xi2[xi1/tv1]
1336 rewriteEqLHS :: WhichComesFromInert -> (Coercion,Xi) -> (CoVar,CtFlavor,Xi) -> TcS WorkList
1337 -- Used to ineract two equalities of the following form:
1338 -- First Equality: co1: (XXX ~ xi1)
1339 -- Second Equality: cv2: (XXX ~ xi2)
1340 -- Where the cv1 `canSolve` cv2 equality
1341 -- We have an option of creating new work (xi1 ~ xi2) OR (xi2 ~ xi1),
1342 -- See Note [Efficient Orientation] for that
1343 rewriteEqLHS which (co1,xi1) (cv2,gw,xi2)
1344 = do { cv2' <- case (isWanted gw, which) of
1345 (True,LeftComesFromInert) ->
1346 do { cv2' <- newWantedCoVar xi2 xi1
1347 ; setWantedCoBind cv2 $
1348 co1 `mkTransCoercion` mkSymCoercion (mkCoVarCoercion cv2')
1350 (True,RightComesFromInert) ->
1351 do { cv2' <- newWantedCoVar xi1 xi2
1352 ; setWantedCoBind cv2 $
1353 co1 `mkTransCoercion` mkCoVarCoercion cv2'
1355 (False,LeftComesFromInert) ->
1356 newGivOrDerCoVar xi2 xi1 $
1357 mkSymCoercion (mkCoVarCoercion cv2) `mkTransCoercion` co1
1358 (False,RightComesFromInert) ->
1359 newGivOrDerCoVar xi1 xi2 $
1360 mkSymCoercion co1 `mkTransCoercion` mkCoVarCoercion cv2
1361 ; mkCanonical gw cv2'
1364 solveOneFromTheOther :: (EvVar, CtFlavor) -> CanonicalCt -> TcS InteractResult
1365 -- First argument inert, second argument workitem. They both represent
1366 -- wanted/given/derived evidence for the *same* predicate so we try here to
1367 -- discharge one directly from the other.
1369 -- Precondition: value evidence only (implicit parameters, classes)
1371 solveOneFromTheOther (iid,ifl) workItem
1372 -- Both derived needs a special case. You might think that we do not need
1373 -- two evidence terms for the same claim. But, since the evidence is partial,
1374 -- either evidence may do in some cases; see TcSMonad.isGoodRecEv.
1375 -- See also Example 3 in Note [Superclasses and recursive dictionaries]
1376 | isDerived ifl && isDerived wfl
1377 = noInteraction workItem
1379 | ifl `canSolve` wfl
1380 = do { unless (isGiven wfl) $ setEvBind wid (EvId iid)
1381 -- Overwrite the binding, if one exists
1382 -- For Givens, which are lambda-bound, nothing to overwrite,
1383 ; dischargeWorkItem }
1385 | otherwise -- wfl `canSolve` ifl
1386 = do { unless (isGiven ifl) $ setEvBind iid (EvId wid)
1387 ; mkIRContinue workItem DropInert emptyWorkList }
1390 wfl = cc_flavor workItem
1391 wid = cc_id workItem
1394 Note [Superclasses and recursive dictionaries]
1395 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1396 Overlaps with Note [SUPERCLASS-LOOP 1]
1397 Note [SUPERCLASS-LOOP 2]
1398 Note [Recursive instances and superclases]
1399 ToDo: check overlap and delete redundant stuff
1401 Right before adding a given into the inert set, we must
1402 produce some more work, that will bring the superclasses
1403 of the given into scope. The superclass constraints go into
1406 When we simplify a wanted constraint, if we first see a matching
1407 instance, we may produce new wanted work. To (1) avoid doing this work
1408 twice in the future and (2) to handle recursive dictionaries we may ``cache''
1409 this item as solved (in effect, given) into our inert set and with that add
1410 its superclass constraints (as given) in our worklist.
1412 But now we have added partially solved constraints to the worklist which may
1413 interact with other wanteds. Consider the example:
1417 class Eq b => Foo a b --- 0-th selector
1418 instance Eq a => Foo [a] a --- fooDFun
1420 and wanted (Foo [t] t). We are first going to see that the instance matches
1421 and create an inert set that includes the solved (Foo [t] t) and its
1423 d1 :_g Foo [t] t d1 := EvDFunApp fooDFun d3
1424 d2 :_g Eq t d2 := EvSuperClass d1 0
1425 Our work list is going to contain a new *wanted* goal
1427 It is wrong to react the wanted (Eq t) with the given (Eq t) because that would
1428 construct loopy evidence. Hence the check isGoodRecEv in doInteractWithInert.
1430 OK, so we have ruled out bad behaviour, but how do we ge recursive dictionaries,
1435 data D r = ZeroD | SuccD (r (D r));
1437 instance (Eq (r (D r))) => Eq (D r) where
1438 ZeroD == ZeroD = True
1439 (SuccD a) == (SuccD b) = a == b
1442 equalDC :: D [] -> D [] -> Bool;
1445 We need to prove (Eq (D [])). Here's how we go:
1449 by instance decl, holds if
1453 *BUT* we have an inert set which gives us (no superclasses):
1455 By the instance declaration of Eq we can show the 'd2' goal if
1457 where d2 = dfEqList d3
1459 Now, however this wanted can interact with our inert d1 to set:
1461 and solve the goal. Why was this interaction OK? Because, if we chase the
1462 evidence of d1 ~~> dfEqD d2 ~~-> dfEqList d3, so by setting d3 := d1 we
1464 d3 := dfEqD2 (dfEqList d3)
1465 which is FINE because the use of d3 is protected by the instance function
1468 So, our strategy is to try to put solved wanted dictionaries into the
1469 inert set along with their superclasses (when this is meaningful,
1470 i.e. when new wanted goals are generated) but solve a wanted dictionary
1471 from a given only in the case where the evidence variable of the
1472 wanted is mentioned in the evidence of the given (recursively through
1473 the evidence binds) in a protected way: more instance function applications
1474 than superclass selectors.
1476 Here are some more examples from GHC's previous type checker
1480 This code arises in the context of "Scrap Your Boilerplate with Class"
1484 instance Sat (ctx Char) => Data ctx Char -- dfunData1
1485 instance (Sat (ctx [a]), Data ctx a) => Data ctx [a] -- dfunData2
1487 class Data Maybe a => Foo a
1489 instance Foo t => Sat (Maybe t) -- dfunSat
1491 instance Data Maybe a => Foo a -- dfunFoo1
1492 instance Foo a => Foo [a] -- dfunFoo2
1493 instance Foo [Char] -- dfunFoo3
1495 Consider generating the superclasses of the instance declaration
1496 instance Foo a => Foo [a]
1498 So our problem is this
1500 d1 :_w Data Maybe [t]
1502 We may add the given in the inert set, along with its superclasses
1503 [assuming we don't fail because there is a matching instance, see
1504 tryTopReact, given case ]
1508 d01 :_g Data Maybe t -- d2 := EvDictSuperClass d0 0
1509 d1 :_w Data Maybe [t]
1510 Then d2 can readily enter the inert, and we also do solving of the wanted
1513 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1515 d2 :_w Sat (Maybe [t])
1517 d01 :_g Data Maybe t
1518 Now, we may simplify d2 more:
1521 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1522 d1 :_g Data Maybe [t]
1523 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1527 d01 :_g Data Maybe t
1529 Now, we can just solve d3.
1532 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1533 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1536 d01 :_g Data Maybe t
1537 And now we can simplify d4 again, but since it has superclasses we *add* them to the worklist:
1540 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1541 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1542 d4 :_g Foo [t] d4 := dfunFoo2 d5
1545 d6 :_g Data Maybe [t] d6 := EvDictSuperClass d4 0
1546 d01 :_g Data Maybe t
1547 Now, d5 can be solved! (and its superclass enter scope)
1550 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1551 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1552 d4 :_g Foo [t] d4 := dfunFoo2 d5
1553 d5 :_g Foo t d5 := dfunFoo1 d7
1556 d6 :_g Data Maybe [t]
1557 d8 :_g Data Maybe t d8 := EvDictSuperClass d5 0
1558 d01 :_g Data Maybe t
1561 [1] Suppose we pick d8 and we react him with d01. Which of the two givens should
1562 we keep? Well, we *MUST NOT* drop d01 because d8 contains recursive evidence
1563 that must not be used (look at case interactInert where both inert and workitem
1564 are givens). So we have several options:
1565 - Drop the workitem always (this will drop d8)
1566 This feels very unsafe -- what if the work item was the "good" one
1567 that should be used later to solve another wanted?
1568 - Don't drop anyone: the inert set may contain multiple givens!
1569 [This is currently implemented]
1571 The "don't drop anyone" seems the most safe thing to do, so now we come to problem 2:
1572 [2] We have added both d6 and d01 in the inert set, and we are interacting our wanted
1573 d7. Now the [isRecDictEv] function in the ineration solver
1574 [case inert-given workitem-wanted] will prevent us from interacting d7 := d8
1575 precisely because chasing the evidence of d8 leads us to an unguarded use of d7.
1577 So, no interaction happens there. Then we meet d01 and there is no recursion
1578 problem there [isRectDictEv] gives us the OK to interact and we do solve d7 := d01!
1580 Note [SUPERCLASS-LOOP 1]
1581 ~~~~~~~~~~~~~~~~~~~~~~~~
1582 We have to be very, very careful when generating superclasses, lest we
1583 accidentally build a loop. Here's an example:
1587 class S a => C a where { opc :: a -> a }
1588 class S b => D b where { opd :: b -> b }
1590 instance C Int where
1593 instance D Int where
1596 From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int}
1597 Simplifying, we may well get:
1598 $dfCInt = :C ds1 (opd dd)
1601 Notice that we spot that we can extract ds1 from dd.
1603 Alas! Alack! We can do the same for (instance D Int):
1605 $dfDInt = :D ds2 (opc dc)
1609 And now we've defined the superclass in terms of itself.
1610 Two more nasty cases are in
1615 - Satisfy the superclass context *all by itself*
1616 (tcSimplifySuperClasses)
1617 - And do so completely; i.e. no left-over constraints
1618 to mix with the constraints arising from method declarations
1621 Note [SUPERCLASS-LOOP 2]
1622 ~~~~~~~~~~~~~~~~~~~~~~~~
1623 We need to be careful when adding "the constaint we are trying to prove".
1624 Suppose we are *given* d1:Ord a, and want to deduce (d2:C [a]) where
1626 class Ord a => C a where
1627 instance Ord [a] => C [a] where ...
1629 Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the
1630 superclasses of C [a] to avails. But we must not overwrite the binding
1631 for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
1634 Here's another variant, immortalised in tcrun020
1635 class Monad m => C1 m
1636 class C1 m => C2 m x
1637 instance C2 Maybe Bool
1638 For the instance decl we need to build (C1 Maybe), and it's no good if
1639 we run around and add (C2 Maybe Bool) and its superclasses to the avails
1640 before we search for C1 Maybe.
1642 Here's another example
1643 class Eq b => Foo a b
1644 instance Eq a => Foo [a] a
1648 we'll first deduce that it holds (via the instance decl). We must not
1649 then overwrite the Eq t constraint with a superclass selection!
1651 At first I had a gross hack, whereby I simply did not add superclass constraints
1652 in addWanted, though I did for addGiven and addIrred. This was sub-optimal,
1653 becuase it lost legitimate superclass sharing, and it still didn't do the job:
1654 I found a very obscure program (now tcrun021) in which improvement meant the
1655 simplifier got two bites a the cherry... so something seemed to be an Stop
1656 first time, but reducible next time.
1658 Now we implement the Right Solution, which is to check for loops directly
1659 when adding superclasses. It's a bit like the occurs check in unification.
1661 Note [Recursive instances and superclases]
1662 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1663 Consider this code, which arises in the context of "Scrap Your
1664 Boilerplate with Class".
1668 instance Sat (ctx Char) => Data ctx Char
1669 instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]
1671 class Data Maybe a => Foo a
1673 instance Foo t => Sat (Maybe t)
1675 instance Data Maybe a => Foo a
1676 instance Foo a => Foo [a]
1679 In the instance for Foo [a], when generating evidence for the superclasses
1680 (ie in tcSimplifySuperClasses) we need a superclass (Data Maybe [a]).
1681 Using the instance for Data, we therefore need
1682 (Sat (Maybe [a], Data Maybe a)
1683 But we are given (Foo a), and hence its superclass (Data Maybe a).
1684 So that leaves (Sat (Maybe [a])). Using the instance for Sat means
1685 we need (Foo [a]). And that is the very dictionary we are bulding
1686 an instance for! So we must put that in the "givens". So in this
1688 Given: Foo a, Foo [a]
1689 Wanted: Data Maybe [a]
1691 BUT we must *not not not* put the *superclasses* of (Foo [a]) in
1692 the givens, which is what 'addGiven' would normally do. Why? Because
1693 (Data Maybe [a]) is the superclass, so we'd "satisfy" the wanted
1694 by selecting a superclass from Foo [a], which simply makes a loop.
1696 On the other hand we *must* put the superclasses of (Foo a) in
1697 the givens, as you can see from the derivation described above.
1699 Conclusion: in the very special case of tcSimplifySuperClasses
1700 we have one 'given' (namely the "this" dictionary) whose superclasses
1701 must not be added to 'givens' by addGiven.
1703 There is a complication though. Suppose there are equalities
1704 instance (Eq a, a~b) => Num (a,b)
1705 Then we normalise the 'givens' wrt the equalities, so the original
1706 given "this" dictionary is cast to one of a different type. So it's a
1707 bit trickier than before to identify the "special" dictionary whose
1708 superclasses must not be added. See test
1709 indexed-types/should_run/EqInInstance
1711 We need a persistent property of the dictionary to record this
1712 special-ness. Current I'm using the InstLocOrigin (a bit of a hack,
1713 but cool), which is maintained by dictionary normalisation.
1714 Specifically, the InstLocOrigin is
1716 then the no-superclass thing kicks in. WATCH OUT if you fiddle
1719 Note [MATCHING-SYNONYMS]
1720 ~~~~~~~~~~~~~~~~~~~~~~~~
1721 When trying to match a dictionary (D tau) to a top-level instance, or a
1722 type family equation (F taus_1 ~ tau_2) to a top-level family instance,
1723 we do *not* need to expand type synonyms because the matcher will do that for us.
1726 Note [RHS-FAMILY-SYNONYMS]
1727 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1728 The RHS of a family instance is represented as yet another constructor which is
1729 like a type synonym for the real RHS the programmer declared. Eg:
1730 type instance F (a,a) = [a]
1732 :R32 a = [a] -- internal type synonym introduced
1733 F (a,a) ~ :R32 a -- instance
1735 When we react a family instance with a type family equation in the work list
1736 we keep the synonym-using RHS without expansion.
1739 *********************************************************************************
1741 The top-reaction Stage
1743 *********************************************************************************
1746 -- If a work item has any form of interaction with top-level we get this
1747 data TopInteractResult
1748 = NoTopInt -- No top-level interaction
1750 { tir_new_work :: WorkList -- Sub-goals or new work (could be given,
1751 -- for superclasses)
1752 , tir_new_inert :: StopOrContinue -- The input work item, ready to become *inert* now:
1753 } -- NB: in ``given'' (solved) form if the
1754 -- original was wanted or given and instance match
1755 -- was found, but may also be in wanted form if we
1756 -- only reacted with functional dependencies
1757 -- arising from top-level instances.
1759 topReactionsStage :: SimplifierStage
1760 topReactionsStage workItem inerts
1761 = do { tir <- tryTopReact workItem
1764 return $ SR { sr_inerts = inerts
1765 , sr_new_work = emptyWorkList
1766 , sr_stop = ContinueWith workItem }
1767 SomeTopInt tir_new_work tir_new_inert ->
1768 return $ SR { sr_inerts = inerts
1769 , sr_new_work = tir_new_work
1770 , sr_stop = tir_new_inert
1774 tryTopReact :: WorkItem -> TcS TopInteractResult
1775 tryTopReact workitem
1776 = do { -- A flag controls the amount of interaction allowed
1777 -- See Note [Simplifying RULE lhs constraints]
1778 ctxt <- getTcSContext
1779 ; if allowedTopReaction (simplEqsOnly ctxt) workitem
1780 then do { traceTcS "tryTopReact / calling doTopReact" (ppr workitem)
1781 ; doTopReact workitem }
1782 else return NoTopInt
1785 allowedTopReaction :: Bool -> WorkItem -> Bool
1786 allowedTopReaction eqs_only (CDictCan {}) = not eqs_only
1787 allowedTopReaction _ _ = True
1790 doTopReact :: WorkItem -> TcS TopInteractResult
1791 -- The work item does not react with the inert set,
1792 -- so try interaction with top-level instances
1794 -- Given dictionary; just add superclasses
1795 -- See Note [Given constraint that matches an instance declaration]
1796 doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Given loc
1797 , cc_class = cls, cc_tyargs = xis })
1798 = do { sc_work <- newGivenSCWork dv loc cls xis
1799 ; return $ SomeTopInt sc_work (ContinueWith workItem) }
1801 -- Derived dictionary
1802 -- Do not add any further derived superclasses; their
1803 -- full transitive closure has already been added.
1804 -- But do look for functional dependencies
1805 doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Derived loc _
1806 , cc_class = cls, cc_tyargs = xis })
1807 = do { fd_work <- findClassFunDeps dv cls xis loc
1808 ; if isEmptyWorkList fd_work then
1810 else return $ SomeTopInt { tir_new_work = fd_work
1811 , tir_new_inert = ContinueWith workItem } }
1813 doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Wanted loc
1814 , cc_class = cls, cc_tyargs = xis })
1815 = do { -- See Note [MATCHING-SYNONYMS]
1816 ; lkp_inst_res <- matchClassInst cls xis loc
1817 ; case lkp_inst_res of
1819 do { traceTcS "doTopReact/ no class instance for" (ppr dv)
1820 ; fd_work <- findClassFunDeps dv cls xis loc
1821 ; if isEmptyWorkList fd_work then
1822 do { sc_work <- newDerivedSCWork dv loc cls xis
1823 -- See Note [Adding Derived Superclasses]
1824 -- NB: workItem is inert, but it isn't solved
1825 -- keep it as inert, although it's not solved
1826 -- because we have now reacted all its
1827 -- top-level fundep-induced equalities!
1828 ; return $ SomeTopInt
1829 { tir_new_work = fd_work `unionWorkLists` sc_work
1830 , tir_new_inert = ContinueWith workItem } }
1832 else -- More fundep work produced, don't do any superclass stuff,
1833 -- just thow him back in the worklist, which will prioritize
1834 -- the solution of fd equalities
1836 { tir_new_work = fd_work `unionWorkLists`
1837 workListFromCCan workItem
1838 , tir_new_inert = Stop } }
1840 GenInst wtvs ev_term -> -- Solved
1841 -- No need to do fundeps stuff here; the instance
1842 -- matches already so we won't get any more info
1843 -- from functional dependencies
1844 do { traceTcS "doTopReact/ found class instance for" (ppr dv)
1845 ; setDictBind dv ev_term
1846 ; inst_work <- canWanteds wtvs
1848 -- Solved in one step and no new wanted work produced.
1849 -- i.e we directly matched a top-level instance
1850 -- No point in caching this in 'inert', nor in adding superclasses
1851 then return $ SomeTopInt { tir_new_work = emptyWorkList
1852 , tir_new_inert = Stop }
1854 -- Solved and new wanted work produced, you may cache the
1855 -- (tentatively solved) dictionary as Derived and its superclasses
1856 else do { let solved = makeSolvedByInst workItem
1857 ; sc_work <- newDerivedSCWork dv loc cls xis
1858 -- See Note [Adding Derived Superclasses]
1859 ; return $ SomeTopInt
1860 { tir_new_work = inst_work `unionWorkLists` sc_work
1861 , tir_new_inert = ContinueWith solved } }
1865 doTopReact (CFunEqCan { cc_id = cv, cc_flavor = fl
1866 , cc_fun = tc, cc_tyargs = args, cc_rhs = xi })
1867 = ASSERT (isSynFamilyTyCon tc) -- No associated data families have reached that far
1868 do { match_res <- matchFam tc args -- See Note [MATCHING-SYNONYMS]
1872 MatchInstSingle (rep_tc, rep_tys)
1873 -> do { let Just coe_tc = tyConFamilyCoercion_maybe rep_tc
1874 Just rhs_ty = tcView (mkTyConApp rep_tc rep_tys)
1875 -- Eagerly expand away the type synonym on the
1876 -- RHS of a type function, so that it never
1877 -- appears in an error message
1878 -- See Note [Type synonym families] in TyCon
1879 coe = mkTyConApp coe_tc rep_tys
1881 Wanted {} -> do { cv' <- newWantedCoVar rhs_ty xi
1882 ; setWantedCoBind cv $
1883 coe `mkTransCoercion`
1886 _ -> newGivOrDerCoVar xi rhs_ty $
1887 mkSymCoercion (mkCoVarCoercion cv) `mkTransCoercion` coe
1889 ; can_cts <- mkCanonical fl cv'
1890 ; return $ SomeTopInt can_cts Stop }
1892 -> panicTcS $ text "TcSMonad.matchFam returned multiple instances!"
1896 -- Any other work item does not react with any top-level equations
1897 doTopReact _workItem = return NoTopInt
1899 ----------------------
1900 findClassFunDeps :: EvVar -> Class -> [Xi] -> WantedLoc -> TcS WorkList
1901 -- Look for a fundep reaction beween the wanted item
1902 -- and a top-level instance declaration
1903 findClassFunDeps dv cls xis loc
1904 = do { instEnvs <- getInstEnvs
1905 ; let eqn_pred_locs = improveFromInstEnv (classInstances instEnvs)
1906 (ClassP cls xis, ppr dv)
1907 ; wevvars <- mkWantedFunDepEqns loc eqn_pred_locs
1908 -- NB: fundeps generate some wanted equalities, but
1909 -- we don't use their evidence for anything
1910 ; canWanteds wevvars }
1913 Note [Adding Derived Superclasses]
1914 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1915 Generally speaking, we want to be able to add derived superclasses of
1916 unsolved wanteds, and wanteds that have been partially being solved
1917 via an instance. This is important to be able to simplify the inferred
1918 constraints more (and to allow for recursive dictionaries, less
1919 importantly). Example:
1921 Inferred wanted constraint is (Eq a, Ord a), but we'd only like to
1922 quantify over Ord a, hence we would like to be able to add the
1923 superclass of Ord a as Derived and use it to solve the wanted Eq a.
1925 Hence we will add Derived superclasses in the following two cases:
1926 (1) When we meet an unsolved wanted in top-level reactions
1927 (2) When we partially solve a wanted in top-level reactions using an instance decl.
1929 At that point, we have two options:
1930 (1) Add transitively add *ALL* of the superclasses of the Derived
1931 (2) Add only the immediate ones, but whenever we meet a Derived in
1932 the future, add its own superclasses as Derived.
1934 Option (2) is terrible, because deriveds may be rewritten or kicked
1935 out of the inert set, which will result in slightly rewritten
1936 superclasses being reintroduced in the worklist and the inert set. Eg:
1939 instance Foo a => B [a]
1941 Original constraints:
1943 [Given] co : a ~ Int
1945 We apply the instance to the wanted and put it and its superclasses as
1946 as Deriveds in the inerts:
1949 [Derived] (sel d) : C [a]
1952 [Given] co : a ~ Int
1955 Now, suppose that we interact the Derived with the Given equality, and
1956 kick him out of the inert, the next time around a superclass C [Int]
1957 will be produced -- but we already *have* C [a] in the inerts which
1958 will anyway get rewritten to C [Int].
1960 So we choose (1), and *never* introduce any more superclass work from
1961 Deriveds. This enables yet another optimisation: If we ever meet an
1962 equality that can rewrite a Derived, if that Derived is a superclass
1963 derived (like C [a] above), i.e. not a partially solved one (like B
1964 [a]) above, we may simply completely *discard* that Derived. The
1965 reason is because somewhere in the inert lies the original wanted, or
1966 partially solved constraint that gave rise to that superclass, and
1967 that constraint *will* be kicked out, and *will* result in the
1968 rewritten superclass to be added in the inerts later on, anyway.
1972 Note [FunDep and implicit parameter reactions]
1973 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1974 Currently, our story of interacting two dictionaries (or a dictionary
1975 and top-level instances) for functional dependencies, and implicit
1976 paramters, is that we simply produce new wanted equalities. So for example
1978 class D a b | a -> b where ...
1984 We generate the extra work item
1986 where 'cv' is currently unused. However, this new item reacts with d2,
1987 discharging it in favour of a new constraint d2' thus:
1989 d2 := d2' |> D Int cv
1990 Now d2' can be discharged from d1
1992 We could be more aggressive and try to *immediately* solve the dictionary
1993 using those extra equalities. With the same inert set and work item we
1994 might dischard d2 directly:
1997 d2 := d1 |> D Int cv
1999 But in general it's a bit painful to figure out the necessary coercion,
2000 so we just take the first approach. Here is a better example. Consider:
2001 class C a b c | a -> b
2003 [Given] d1 : C T Int Char
2004 [Wanted] d2 : C T beta Int
2005 In this case, it's *not even possible* to solve the wanted immediately.
2006 So we should simply output the functional dependency and add this guy
2007 [but NOT its superclasses] back in the worklist. Even worse:
2008 [Given] d1 : C T Int beta
2009 [Wanted] d2: C T beta Int
2010 Then it is solvable, but its very hard to detect this on the spot.
2012 It's exactly the same with implicit parameters, except that the
2013 "aggressive" approach would be much easier to implement.
2015 Note [When improvement happens]
2016 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2017 We fire an improvement rule when
2019 * Two constraints match (modulo the fundep)
2020 e.g. C t1 t2, C t1 t3 where C a b | a->b
2021 The two match because the first arg is identical
2023 * At least one is not Given. If they are both given, we don't fire
2024 the reaction because we have no way of constructing evidence for a
2025 new equality nor does it seem right to create a new wanted goal
2026 (because the goal will most likely contain untouchables, which
2027 can't be solved anyway)!
2029 Note that we *do* fire the improvement if one is Given and one is Derived.
2030 The latter can be a superclass of a wanted goal. Example (tcfail138)
2031 class L a b | a -> b
2032 class (G a, L a b) => C a b
2034 instance C a b' => G (Maybe a)
2035 instance C a b => C (Maybe a) a
2036 instance L (Maybe a) a
2038 When solving the superclasses of the (C (Maybe a) a) instance, we get
2039 Given: C a b ... and hance by superclasses, (G a, L a b)
2041 Use the instance decl to get
2043 The (C a b') is inert, so we generate its Derived superclasses (L a b'),
2044 and now we need improvement between that derived superclass an the Given (L a b)
2046 Note [Overriding implicit parameters]
2047 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2049 f :: (?x::a) -> Bool -> a
2051 g v = let ?x::Int = 3
2052 in (f v, let ?x::Bool = True in f v)
2054 This should probably be well typed, with
2055 g :: Bool -> (Int, Bool)
2057 So the inner binding for ?x::Bool *overrides* the outer one.
2058 Hence a work-item Given overrides an inert-item Given.
2060 Note [Given constraint that matches an instance declaration]
2061 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2062 What should we do when we discover that one (or more) top-level
2063 instances match a given (or solved) class constraint? We have
2066 1. Reject the program. The reason is that there may not be a unique
2067 best strategy for the solver. Example, from the OutsideIn(X) paper:
2068 instance P x => Q [x]
2069 instance (x ~ y) => R [x] y
2071 wob :: forall a b. (Q [b], R b a) => a -> Int
2073 g :: forall a. Q [a] => [a] -> Int
2076 will generate the impliation constraint:
2077 Q [a] => (Q [beta], R beta [a])
2078 If we react (Q [beta]) with its top-level axiom, we end up with a
2079 (P beta), which we have no way of discharging. On the other hand,
2080 if we react R beta [a] with the top-level we get (beta ~ a), which
2081 is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
2082 now solvable by the given Q [a].
2084 However, this option is restrictive, for instance [Example 3] from
2085 Note [Recursive dictionaries] will fail to work.
2087 2. Ignore the problem, hoping that the situations where there exist indeed
2088 such multiple strategies are rare: Indeed the cause of the previous
2089 problem is that (R [x] y) yields the new work (x ~ y) which can be
2090 *spontaneously* solved, not using the givens.
2092 We are choosing option 2 below but we might consider having a flag as well.
2095 Note [New Wanted Superclass Work]
2096 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2097 Even in the case of wanted constraints, we add all of its superclasses as
2098 new given work. There are several reasons for this:
2099 a) to minimise error messages;
2100 eg suppose we have wanted (Eq a, Ord a)
2101 then we report only (Ord a) unsoluble
2103 b) to make the smallest number of constraints when *inferring* a type
2104 (same Eq/Ord example)
2106 c) for recursive dictionaries we *must* add the superclasses
2107 so that we can use them when solving a sub-problem
2109 d) To allow FD-like improvement for type families. Assume that
2111 class C a b | a -> b
2112 and we have to solve the implication constraint:
2114 Then, FD improvement can help us to produce a new wanted (beta ~ b)
2116 We want to have the same effect with the type family encoding of
2117 functional dependencies. Namely, consider:
2118 class (F a ~ b) => C a b
2119 Now suppose that we have:
2122 By interacting the given we will get given (F a ~ b) which is not
2123 enough by itself to make us discharge (C a beta). However, we
2124 may create a new derived equality from the super-class of the
2125 wanted constraint (C a beta), namely derived (F a ~ beta).
2126 Now we may interact this with given (F a ~ b) to get:
2128 But 'beta' is a touchable unification variable, and hence OK to
2129 unify it with 'b', replacing the derived evidence with the identity.
2131 This requires trySpontaneousSolve to solve *derived*
2132 equalities that have a touchable in their RHS, *in addition*
2133 to solving wanted equalities.
2135 Here is another example where this is useful.
2139 class (F a ~ b) => C a b
2140 And we are given the wanteds:
2144 We surely do *not* want to quantify over (b ~ c), since if someone provides
2145 dictionaries for (C a b) and (C a c), these dictionaries can provide a proof
2146 of (b ~ c), hence no extra evidence is necessary. Here is what will happen:
2148 Step 1: We will get new *given* superclass work,
2149 provisionally to our solving of w1 and w2
2151 g1: F a ~ b, g2 : F a ~ c,
2152 w1 : C a b, w2 : C a c, w3 : b ~ c
2154 The evidence for g1 and g2 is a superclass evidence term:
2156 g1 := sc w1, g2 := sc w2
2158 Step 2: The givens will solve the wanted w3, so that
2159 w3 := sym (sc w1) ; sc w2
2161 Step 3: Now, one may naively assume that then w2 can be solve from w1
2162 after rewriting with the (now solved equality) (b ~ c).
2164 But this rewriting is ruled out by the isGoodRectDict!
2166 Conclusion, we will (correctly) end up with the unsolved goals
2169 NB: The desugarer needs be more clever to deal with equalities
2170 that participate in recursive dictionary bindings.
2174 newGivenSCWork :: EvVar -> GivenLoc -> Class -> [Xi] -> TcS WorkList
2175 newGivenSCWork ev loc cls xis
2176 | NoScSkol <- ctLocOrigin loc -- Very important!
2177 = return emptyWorkList
2179 = newImmSCWorkFromFlavored ev (Given loc) cls xis >>= return
2181 newDerivedSCWork :: EvVar -> WantedLoc -> Class -> [Xi] -> TcS WorkList
2182 newDerivedSCWork ev loc cls xis
2183 = do { ims <- newImmSCWorkFromFlavored ev flavor cls xis
2186 rec_sc_work :: CanonicalCts -> TcS CanonicalCts
2188 = do { bg <- mapBagM (\c -> do { ims <- imm_sc_work c
2189 ; recs_ims <- rec_sc_work ims
2190 ; return $ consBag c recs_ims }) cts
2191 ; return $ concatBag bg }
2192 imm_sc_work (CDictCan { cc_id = dv, cc_flavor = fl, cc_class = cls, cc_tyargs = xis })
2193 = newImmSCWorkFromFlavored dv fl cls xis
2194 imm_sc_work _ct = return emptyCCan
2196 flavor = Derived loc DerSC
2198 newImmSCWorkFromFlavored :: EvVar -> CtFlavor -> Class -> [Xi] -> TcS WorkList
2199 -- Returns immediate superclasses
2200 newImmSCWorkFromFlavored ev flavor cls xis
2201 = do { let (tyvars, sc_theta, _, _) = classBigSig cls
2202 sc_theta1 = substTheta (zipTopTvSubst tyvars xis) sc_theta
2203 ; sc_vars <- zipWithM inst_one sc_theta1 [0..]
2204 ; mkCanonicals flavor sc_vars }
2206 inst_one pred n = newGivOrDerEvVar pred (EvSuperClass ev n)
2209 data LookupInstResult
2211 | GenInst [WantedEvVar] EvTerm
2213 matchClassInst :: Class -> [Type] -> WantedLoc -> TcS LookupInstResult
2214 matchClassInst clas tys loc
2215 = do { let pred = mkClassPred clas tys
2216 ; mb_result <- matchClass clas tys
2218 MatchInstNo -> return NoInstance
2219 MatchInstMany -> return NoInstance -- defer any reactions of a multitude until
2220 -- we learn more about the reagent
2221 MatchInstSingle (dfun_id, mb_inst_tys) ->
2222 do { checkWellStagedDFun pred dfun_id loc
2224 -- It's possible that not all the tyvars are in
2225 -- the substitution, tenv. For example:
2226 -- instance C X a => D X where ...
2227 -- (presumably there's a functional dependency in class C)
2228 -- Hence mb_inst_tys :: Either TyVar TcType
2230 ; tys <- instDFunTypes mb_inst_tys
2231 ; let (theta, _) = tcSplitPhiTy (applyTys (idType dfun_id) tys)
2232 ; if null theta then
2233 return (GenInst [] (EvDFunApp dfun_id tys []))
2235 { ev_vars <- instDFunConstraints theta
2236 ; let wevs = [WantedEvVar w loc | w <- ev_vars]
2237 ; return $ GenInst wevs (EvDFunApp dfun_id tys ev_vars) }