3 solveInteract, AtomicInert,
4 InertSet, emptyInert, updInertSet, extractUnsolved, solveOne
7 #include "HsVersions.h"
30 import Control.Monad ( when )
39 import qualified Data.Map as Map
42 import Control.Monad( zipWithM, unless )
43 import FastString ( sLit )
47 Note [InertSet invariants]
48 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
50 An InertSet is a bag of canonical constraints, with the following invariants:
52 1 No two constraints react with each other.
54 A tricky case is when there exists a given (solved) dictionary
55 constraint and a wanted identical constraint in the inert set, but do
56 not react because reaction would create loopy dictionary evidence for
57 the wanted. See note [Recursive dictionaries]
59 2 Given equalities form an idempotent substitution [none of the
60 given LHS's occur in any of the given RHS's or reactant parts]
62 3 Wanted equalities also form an idempotent substitution
63 4 The entire set of equalities is acyclic.
65 5 Wanted dictionaries are inert with the top-level axiom set
67 6 Equalities of the form tv1 ~ tv2 always have a touchable variable
68 on the left (if possible).
69 7 No wanted constraints tv1 ~ tv2 with tv1 touchable. Such constraints
70 will be marked as solved right before being pushed into the inert set.
71 See note [Touchables and givens].
73 Note that 6 and 7 are /not/ enforced by canonicalization but rather by
74 insertion in the inert list, ie by TcInteract.
76 During the process of solving, the inert set will contain some
77 previously given constraints, some wanted constraints, and some given
78 constraints which have arisen from solving wanted constraints. For
79 now we do not distinguish between given and solved constraints.
81 Note that we must switch wanted inert items to given when going under an
82 implication constraint (when in top-level inference mode).
84 Note [InertSet FlattenSkolemEqClass]
85 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
86 The inert_fsks field of the inert set contains an "inverse map" of all the
87 flatten skolem equalities in the inert set. For instance, if inert_cts looks
94 Then, the inert_fsks fields holds the following map:
95 fsk2 |-> { fsk1, fsk3 }
97 Along with the necessary coercions to convert fsk1 and fsk3 back to fsk2
98 and fsk4 back to fsk5. Hence, the invariants of the inert_fsks field are:
100 (a) All TcTyVars in the domain and range of inert_fsks are flatten skolems
101 (b) All TcTyVars in the domain of inert_fsk occur naked as rhs in some
102 equalities of inert_cts
103 (c) For every mapping fsk1 |-> { (fsk2,co), ... } it must be:
106 The role of the inert_fsks is to make it easy to maintain the equivalence
107 class of each flatten skolem, which is much needed to correctly do spontaneous
108 solving. See Note [Loopy Spontaneous Solving]
111 -- See Note [InertSet invariants]
113 = IS { inert_eqs :: Bag.Bag CanonicalCt -- Equalities only **CTyEqCan**
114 , inert_cts :: Bag.Bag CanonicalCt -- Other constraints
115 , inert_fds :: FDImprovements -- List of pairwise improvements that have kicked in already
116 -- and reside either in the worklist or in the inerts
117 , inert_fsks :: Map.Map TcTyVar [(TcTyVar,Coercion)] }
118 -- See Note [InertSet FlattenSkolemEqClass]
120 type FDImprovement = (PredType,PredType)
121 type FDImprovements = [(PredType,PredType)]
123 instance Outputable InertSet where
124 ppr is = vcat [ vcat (map ppr (Bag.bagToList $ inert_eqs is))
125 , vcat (map ppr (Bag.bagToList $ inert_cts is))
126 , vcat (map (\(v,rest) -> ppr v <+> text "|->" <+> hsep (map (ppr.fst) rest))
127 (Map.toList $ inert_fsks is)
131 emptyInert :: InertSet
132 emptyInert = IS { inert_eqs = Bag.emptyBag
133 , inert_cts = Bag.emptyBag, inert_fsks = Map.empty, inert_fds = [] }
135 updInertSet :: InertSet -> AtomicInert -> InertSet
136 -- Introduces an element in the inert set for the first time
137 updInertSet (IS { inert_eqs = eqs, inert_cts = cts, inert_fsks = fsks, inert_fds = fdis })
138 item@(CTyEqCan { cc_id = cv
141 | Just tv2 <- tcGetTyVar_maybe xi,
142 FlatSkol {} <- tcTyVarDetails tv1,
143 FlatSkol {} <- tcTyVarDetails tv2
144 = let eqs' = eqs `Bag.snocBag` item
145 fsks' = Map.insertWith (++) tv2 [(tv1, mkCoVarCoercion cv)] fsks
146 -- See Note [InertSet FlattenSkolemEqClass]
147 in IS { inert_eqs = eqs', inert_cts = cts, inert_fsks = fsks', inert_fds = fdis }
148 updInertSet (IS { inert_eqs = eqs, inert_cts = cts
149 , inert_fsks = fsks, inert_fds = fdis }) item
151 = let eqs' = eqs `Bag.snocBag` item
152 in IS { inert_eqs = eqs', inert_cts = cts, inert_fsks = fsks, inert_fds = fdis }
154 = let cts' = cts `Bag.snocBag` item
155 in IS { inert_eqs = eqs, inert_cts = cts', inert_fsks = fsks, inert_fds = fdis }
157 updInertSetFDImprs :: InertSet -> Maybe FDImprovement -> InertSet
158 updInertSetFDImprs is (Just fdi) = is { inert_fds = fdi : inert_fds is }
159 updInertSetFDImprs is Nothing = is
161 foldISEqCtsM :: Monad m => (a -> AtomicInert -> m a) -> a -> InertSet -> m a
162 -- Fold over the equalities of the inerts
163 foldISEqCtsM k z IS { inert_eqs = eqs }
164 = Bag.foldlBagM k z eqs
166 foldISOtherCtsM :: Monad m => (a -> AtomicInert -> m a) -> a -> InertSet -> m a
167 -- Fold over other constraints in the inerts
168 foldISOtherCtsM k z IS { inert_cts = cts }
169 = Bag.foldlBagM k z cts
171 extractUnsolved :: InertSet -> (InertSet, CanonicalCts)
172 extractUnsolved is@(IS {inert_eqs = eqs, inert_cts = cts, inert_fds = fdis })
173 = let is_init = is { inert_eqs = emptyCCan
174 , inert_cts = solved_cts, inert_fsks = Map.empty, inert_fds = fdis }
175 is_final = Bag.foldlBag updInertSet is_init solved_eqs -- Add equalities carefully
176 in (is_final, unsolved)
177 where (unsolved_cts, solved_cts) = Bag.partitionBag isWantedCt cts
178 (unsolved_eqs, solved_eqs) = Bag.partitionBag isWantedCt eqs
179 unsolved = unsolved_cts `unionBags` unsolved_eqs
182 getFskEqClass :: InertSet -> TcTyVar -> [(TcTyVar,Coercion)]
183 -- Precondition: tv is a FlatSkol. See Note [InertSet FlattenSkolemEqClass]
184 getFskEqClass (IS { inert_cts = cts, inert_fsks = fsks }) tv
185 = case lkpTyEqCanByLhs of
186 Nothing -> fromMaybe [] (Map.lookup tv fsks)
188 case tcGetTyVar_maybe (cc_rhs ceq) of
189 Just tv_rhs | FlatSkol {} <- tcTyVarDetails tv_rhs
190 -> let ceq_co = mkSymCoercion $ mkCoVarCoercion (cc_id ceq)
191 mk_co (v,c) = (v, mkTransCoercion c ceq_co)
192 in (tv_rhs, ceq_co): map mk_co (fromMaybe [] $ Map.lookup tv fsks)
194 where lkpTyEqCanByLhs = Bag.foldlBag lkp Nothing cts
195 lkp :: Maybe CanonicalCt -> CanonicalCt -> Maybe CanonicalCt
196 lkp Nothing ct@(CTyEqCan {cc_tyvar = tv'}) | tv' == tv = Just ct
197 lkp other _ct = other
199 haveBeenImproved :: FDImprovements -> PredType -> PredType -> Bool
200 haveBeenImproved [] _ _ = False
201 haveBeenImproved ((pty1,pty2):fdimprs) pty1' pty2'
202 | tcEqPred pty1 pty1' && tcEqPred pty2 pty2'
204 | tcEqPred pty1 pty2' && tcEqPred pty2 pty1'
207 = haveBeenImproved fdimprs pty1' pty2'
209 getFDImprovements :: InertSet -> FDImprovements
210 -- Return a list of the improvements that have kicked in so far
211 getFDImprovements = inert_fds
214 isWantedCt :: CanonicalCt -> Bool
215 isWantedCt ct = isWanted (cc_flavor ct)
218 data Inert = IS { class_inerts :: FiniteMap Class Atomics
219 ip_inerts :: FiniteMap Class Atomics
220 tyfun_inerts :: FiniteMap TyCon Atomics
221 tyvar_inerts :: FiniteMap TyVar Atomics
224 Later should we also separate out givens and wanteds?
229 Note [Touchables and givens]
230 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
231 Touchable variables will never show up in givens which are inputs to
232 the solver. However, touchables may show up in givens generated by the flattener.
247 which can be put in the inert set. Suppose we also have a wanted
251 We cannot rewrite the given G alpha ~g b using the wanted alpha ~w
252 Int. Instead, after reacting alpha ~w Int with the whole inert set,
253 we observe that we can solve it by unifying alpha with Int, so we mark
254 it as solved and put it back in the *work list*. [We also immediately unify
255 alpha := Int, without telling anyone, see trySpontaneousSolve function, to
256 avoid doing this in the end.]
258 Later, because it is solved (given, in effect), we can use it to rewrite
259 G alpha ~g b to G Int ~g b, which gets put back in the work list. Eventually,
260 we will dispatch the remaining wanted constraints using the top-level axioms.
262 Finally, note that after reacting a wanted equality with the entire inert set
263 we may end up with something like
267 which we should flip around to generate the solved constraint alpha ~s b.
269 %*********************************************************************
271 * Main Interaction Solver *
273 **********************************************************************
277 1. Canonicalise (unary)
278 2. Pairwise interaction (binary)
279 * Take one from work list
280 * Try all pair-wise interactions with each constraint in inert
282 As an optimisation, we prioritize the equalities both in the
283 worklist and in the inerts.
285 3. Try to solve spontaneously for equalities involving touchables
286 4. Top-level interaction (binary wrt top-level)
287 Superclass decomposition belongs in (4), see note [Superclasses]
290 type AtomicInert = CanonicalCt -- constraint pulled from InertSet
291 type WorkItem = CanonicalCt -- constraint pulled from WorkList
293 -- A mixture of Given, Wanted, and Derived constraints.
294 -- We split between equalities and the rest to process equalities first.
295 type WorkList = CanonicalCts
296 type SWorkList = WorkList -- A worklist of solved
298 unionWorkLists :: WorkList -> WorkList -> WorkList
299 unionWorkLists = andCCan
301 isEmptyWorkList :: WorkList -> Bool
302 isEmptyWorkList = isEmptyCCan
304 emptyWorkList :: WorkList
305 emptyWorkList = emptyCCan
307 workListFromCCan :: CanonicalCt -> WorkList
308 workListFromCCan = singleCCan
310 ------------------------
312 = Stop -- Work item is consumed
313 | ContinueWith WorkItem -- Not consumed
315 instance Outputable StopOrContinue where
316 ppr Stop = ptext (sLit "Stop")
317 ppr (ContinueWith w) = ptext (sLit "ContinueWith") <+> ppr w
319 -- Results after interacting a WorkItem as far as possible with an InertSet
321 = SR { sr_inerts :: InertSet
322 -- The new InertSet to use (REPLACES the old InertSet)
323 , sr_new_work :: WorkList
324 -- Any new work items generated (should be ADDED to the old WorkList)
326 -- sr_stop = Just workitem => workitem is *not* in sr_inerts and
327 -- workitem is inert wrt to sr_inerts
328 , sr_stop :: StopOrContinue
331 instance Outputable StageResult where
332 ppr (SR { sr_inerts = inerts, sr_new_work = work, sr_stop = stop })
333 = ptext (sLit "SR") <+>
334 braces (sep [ ptext (sLit "inerts =") <+> ppr inerts <> comma
335 , ptext (sLit "new work =") <+> ppr work <> comma
336 , ptext (sLit "stop =") <+> ppr stop])
338 type SimplifierStage = WorkItem -> InertSet -> TcS StageResult
340 -- Combine a sequence of simplifier 'stages' to create a pipeline
341 runSolverPipeline :: [(String, SimplifierStage)]
342 -> InertSet -> WorkItem
343 -> TcS (InertSet, WorkList)
344 -- Precondition: non-empty list of stages
345 runSolverPipeline pipeline inerts workItem
346 = do { traceTcS "Start solver pipeline" $
347 vcat [ ptext (sLit "work item =") <+> ppr workItem
348 , ptext (sLit "inerts =") <+> ppr inerts]
350 ; let itr_in = SR { sr_inerts = inerts
351 , sr_new_work = emptyWorkList
352 , sr_stop = ContinueWith workItem }
353 ; itr_out <- run_pipeline pipeline itr_in
355 = case sr_stop itr_out of
356 Stop -> sr_inerts itr_out
357 ContinueWith item -> sr_inerts itr_out `updInertSet` item
358 ; return (new_inert, sr_new_work itr_out) }
360 run_pipeline :: [(String, SimplifierStage)]
361 -> StageResult -> TcS StageResult
362 run_pipeline [] itr = return itr
363 run_pipeline _ itr@(SR { sr_stop = Stop }) = return itr
365 run_pipeline ((name,stage):stages)
366 (SR { sr_new_work = accum_work
368 , sr_stop = ContinueWith work_item })
369 = do { itr <- stage work_item inerts
370 ; traceTcS ("Stage result (" ++ name ++ ")") (ppr itr)
371 ; let itr' = itr { sr_new_work = accum_work `unionWorkLists` sr_new_work itr }
372 ; run_pipeline stages itr' }
376 Inert: {c ~ d, F a ~ t, b ~ Int, a ~ ty} (all given)
377 Reagent: a ~ [b] (given)
379 React with (c~d) ==> IR (ContinueWith (a~[b])) True []
380 React with (F a ~ t) ==> IR (ContinueWith (a~[b])) False [F [b] ~ t]
381 React with (b ~ Int) ==> IR (ContinueWith (a~[Int]) True []
384 Inert: {c ~w d, F a ~g t, b ~w Int, a ~w ty}
387 React with (c ~w d) ==> IR (ContinueWith (a~[b])) True []
388 React with (F a ~g t) ==> IR (ContinueWith (a~[b])) True [] (can't rewrite given with wanted!)
392 Inert: {a ~ Int, F Int ~ b} (given)
393 Reagent: F a ~ b (wanted)
395 React with (a ~ Int) ==> IR (ContinueWith (F Int ~ b)) True []
396 React with (F Int ~ b) ==> IR Stop True [] -- after substituting we re-canonicalize and get nothing
399 -- Main interaction solver: we fully solve the worklist 'in one go',
400 -- returning an extended inert set.
402 -- See Note [Touchables and givens].
403 solveInteract :: InertSet -> CanonicalCts -> TcS InertSet
404 solveInteract inert ws
405 = do { dyn_flags <- getDynFlags
406 ; solveInteractWithDepth (ctxtStkDepth dyn_flags,0,[]) inert ws
408 solveOne :: InertSet -> WorkItem -> TcS InertSet
409 solveOne inerts workItem
410 = do { dyn_flags <- getDynFlags
411 ; solveOneWithDepth (ctxtStkDepth dyn_flags,0,[]) inerts workItem
415 solveInteractWithDepth :: (Int, Int, [WorkItem])
416 -> InertSet -> WorkList -> TcS InertSet
417 solveInteractWithDepth ctxt@(max_depth,n,stack) inert ws
422 = solverDepthErrorTcS n stack
425 = do { traceTcS "solveInteractWithDepth" $
426 vcat [ text "Current depth =" <+> ppr n
427 , text "Max depth =" <+> ppr max_depth ]
429 -- Solve equalities first
430 ; let (eqs, non_eqs) = Bag.partitionBag isTyEqCCan ws
431 ; is_from_eqs <- Bag.foldlBagM (solveOneWithDepth ctxt) inert eqs
432 ; Bag.foldlBagM (solveOneWithDepth ctxt) is_from_eqs non_eqs }
435 -- Fully interact the given work item with an inert set, and return a
436 -- new inert set which has assimilated the new information.
437 solveOneWithDepth :: (Int, Int, [WorkItem])
438 -> InertSet -> WorkItem -> TcS InertSet
439 solveOneWithDepth (max_depth, n, stack) inert work
440 = do { traceTcS0 (indent ++ "Solving {") (ppr work)
441 ; (new_inert, new_work) <- runSolverPipeline thePipeline inert work
443 ; traceTcS0 (indent ++ "Subgoals:") (ppr new_work)
445 -- Recursively solve the new work generated
446 -- from workItem, with a greater depth
447 ; res_inert <- solveInteractWithDepth (max_depth, n+1, work:stack)
450 ; traceTcS0 (indent ++ "Done }") (ppr work)
453 indent = replicate (2*n) ' '
455 thePipeline :: [(String,SimplifierStage)]
456 thePipeline = [ ("interact with inert eqs", interactWithInertEqsStage)
457 , ("interact with inerts", interactWithInertsStage)
458 , ("spontaneous solve", spontaneousSolveStage)
459 , ("top-level reactions", topReactionsStage) ]
462 *********************************************************************************
464 The spontaneous-solve Stage
466 *********************************************************************************
468 Note [Efficient Orientation]
469 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
471 There are two cases where we have to be careful about
472 orienting equalities to get better efficiency.
474 Case 1: In Spontaneous Solving
476 The OrientFlag is used to preserve the original orientation of a
477 spontaneously solved equality (insofar the canonical constraints
478 invariants allow it). This way we hope to be more efficient since
479 when reaching the spontaneous solve stage, a particular
480 constraint has already been inert-ified wrt to the preexisting
484 Inerts: [w1] : D alpha
488 Untouchables = [beta]
489 Then a wanted (beta ~ alpha) comes along.
491 1) While interacting with the inerts it is going to kick w2,w4
493 2) Then, it will spontaneoulsy be solved by (alpha := beta)
494 3) Now (and here is the tricky part), to add him back as
495 solved (alpha ~ beta) is no good because, in the next
496 iteration, it will kick out w1,w3 as well so we will end up
497 with *all* the inert equalities back in the worklist!
499 So, we instead solve (alpha := beta), but we preserve the
500 original orientation, so that we get a given (beta ~ alpha),
501 which will result in no more inerts getting kicked out of the
502 inert set in the next iteration.
504 Case 2: In Rewriting Equalities (function rewriteEqLHS)
506 When rewriting two equalities with the same LHS:
509 We have a choice of producing work (xi1 ~ xi2) (up-to the
510 canonicalization invariants) However, to prevent the inert items
511 from getting kicked out of the inerts first, we prefer to
512 canonicalize (xi1 ~ xi2) if (b) comes from the inert set, or (xi2
513 ~ xi1) if (a) comes from the inert set.
515 This choice is implemented using the WhichComesFromInert flag.
517 Case 3: Functional Dependencies and IP improvement work
518 TODO. Optimisation not yet implemented there.
521 spontaneousSolveStage :: SimplifierStage
522 spontaneousSolveStage workItem inerts
523 = do { mSolve <- trySpontaneousSolve workItem inerts
525 Nothing -> -- no spontaneous solution for him, keep going
526 return $ SR { sr_new_work = emptyWorkList
528 , sr_stop = ContinueWith workItem }
530 Just workList' -> -- He has been solved; workList' are all givens
531 return $ SR { sr_new_work = workList'
537 data OrientFlag = OrientThisWay
538 | OrientOtherWay -- See Note [Efficient Orientation]
540 -- @trySpontaneousSolve wi@ solves equalities where one side is a
541 -- touchable unification variable. Returns:
542 -- * Nothing if we were not able to solve it
543 -- * Just wi' if we solved it, wi' (now a "given") should be put in the work list.
544 -- See Note [Touchables and givens]
545 -- NB: just passing the inerts through for the skolem equivalence classes
546 trySpontaneousSolve :: WorkItem -> InertSet -> TcS (Maybe SWorkList)
547 trySpontaneousSolve workItem@(CTyEqCan { cc_id = cv, cc_flavor = gw, cc_tyvar = tv1, cc_rhs = xi }) inerts
550 | Just tv2 <- tcGetTyVar_maybe xi
551 = do { tch1 <- isTouchableMetaTyVar tv1
552 ; tch2 <- isTouchableMetaTyVar tv2
553 ; case (tch1, tch2) of
554 (True, True) -> trySpontaneousEqTwoWay inerts cv gw tv1 tv2
555 (True, False) -> trySpontaneousEqOneWay OrientThisWay inerts cv gw tv1 xi
556 (False, True) -> trySpontaneousEqOneWay OrientOtherWay inerts cv gw tv2 (mkTyVarTy tv1)
557 _ -> return Nothing }
559 = do { tch1 <- isTouchableMetaTyVar tv1
560 ; if tch1 then trySpontaneousEqOneWay OrientThisWay inerts cv gw tv1 xi
561 else do { traceTcS "Untouchable LHS, can't spontaneously solve workitem:" (ppr workItem)
566 -- trySpontaneousSolve (CFunEqCan ...) = ...
567 -- See Note [No touchables as FunEq RHS] in TcSMonad
568 trySpontaneousSolve _ _ = return Nothing
571 trySpontaneousEqOneWay :: OrientFlag
572 -> InertSet -> CoVar -> CtFlavor -> TcTyVar -> Xi
573 -> TcS (Maybe SWorkList)
574 -- NB: The OrientFlag is there to help us recover the orientation of the original
575 -- constraint which is important for enforcing the canonical constraints invariants.
576 -- Also, tv is a MetaTyVar, not untouchable
577 trySpontaneousEqOneWay or_flag inerts cv gw tv xi
578 | not (isSigTyVar tv) || isTyVarTy xi
579 = do { kxi <- zonkTcTypeTcS xi >>= return . typeKind -- Must look through the TcTyBinds
580 -- hence kxi and not typeKind xi
581 -- See Note [Kind Errors]
582 ; if kxi `isSubKind` tyVarKind tv then
583 solveWithIdentity or_flag inerts cv gw tv xi
584 else if tyVarKind tv `isSubKind` kxi then
585 return Nothing -- kinds are compatible but we can't solveWithIdentity this way
586 -- This case covers the a_touchable :: * ~ b_untouchable :: ??
587 -- which has to be deferred or floated out for someone else to solve
588 -- it in a scope where 'b' is no longer untouchable.
589 else kindErrorTcS gw (mkTyVarTy tv) xi -- See Note [Kind errors]
591 | otherwise -- Still can't solve, sig tyvar and non-variable rhs
595 trySpontaneousEqTwoWay :: InertSet -> CoVar -> CtFlavor -> TcTyVar -> TcTyVar
596 -> TcS (Maybe SWorkList)
597 -- Both tyvars are *touchable* MetaTyvars so there is only a chance for kind error here
598 trySpontaneousEqTwoWay inerts cv gw tv1 tv2
600 , nicer_to_update_tv2 = solveWithIdentity OrientOtherWay inerts cv gw tv2 (mkTyVarTy tv1)
602 = solveWithIdentity OrientThisWay inerts cv gw tv1 (mkTyVarTy tv2)
603 | otherwise -- None is a subkind of the other, but they are both touchable!
604 = kindErrorTcS gw (mkTyVarTy tv1) (mkTyVarTy tv2) -- See Note [Kind errors]
608 nicer_to_update_tv2 = isSigTyVar tv1 || isSystemName (Var.varName tv2)
612 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
613 Consider the wanted problem:
614 alpha ~ (# Int, Int #)
615 where alpha :: ?? and (# Int, Int #) :: (#). We can't spontaneously solve this constraint,
616 but we should rather reject the program that give rise to it. If 'trySpontaneousEqTwoWay'
617 simply returns @Nothing@ then that wanted constraint is going to propagate all the way and
618 get quantified over in inference mode. That's bad because we do know at this point that the
619 constraint is insoluble. Instead, we call 'kindErrorTcS' here, which immediately fails.
621 The same applies in canonicalization code in case of kind errors in the givens.
623 However, when we canonicalize givens we only check for compatibility (@compatKind@).
624 If there were a kind error in the givens, this means some form of inconsistency or dead code.
626 When we spontaneously solve wanteds we may have to look through the bindings, hence we
627 call zonkTcTypeTcS above. The reason is that maybe xi is @alpha@ where alpha :: ? and
628 a previous spontaneous solving has set (alpha := f) with (f :: *). The reason that xi is
629 still alpha and not f is becasue the solved constraint may be oriented as (f ~ alpha) instead
630 of (alpha ~ f). Then we should be using @xi@s "real" kind, which is * and not ?, when we try
631 to detect whether spontaneous solving is possible.
634 Note [Spontaneous solving and kind compatibility]
635 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
637 Note that our canonical constraints insist that only *given* equalities (tv ~ xi)
638 or (F xis ~ rhs) require the LHS and the RHS to have exactly the same kinds.
640 - We have to require this because:
641 Given equalities can be freely used to rewrite inside
642 other types or constraints.
643 - We do not have to do the same for wanteds because:
644 First, wanted equations (tv ~ xi) where tv is a touchable
645 unification variable may have kinds that do not agree (the
646 kind of xi must be a sub kind of the kind of tv). Second, any
647 potential kind mismatch will result in the constraint not
648 being soluble, which will be reported anyway. This is the
649 reason that @trySpontaneousOneWay@ and @trySpontaneousTwoWay@
650 will perform a kind compatibility check, and only then will
651 they proceed to @solveWithIdentity@.
654 - Givens from higher-rank, such as:
655 type family T b :: * -> * -> *
656 type instance T Bool = (->)
658 f :: forall a. ((T a ~ (->)) => ...) -> a -> ...
660 Whereas we would be able to apply the type instance, we would not be able to
661 use the given (T Bool ~ (->)) in the body of 'flop'
663 Note [Loopy Spontaneous Solving]
664 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
666 Example 1: (The problem of loopy spontaneous solving)
667 ****************************************************************************
668 Consider the original wanted:
669 wanted : Maybe (E alpha) ~ alpha
670 where E is a type family, such that E (T x) = x. After canonicalization,
671 as a result of flattening, we will get:
672 given : E alpha ~ fsk
673 wanted : alpha ~ Maybe fsk
674 where (fsk := E alpha, on the side). Now, if we spontaneously *solve*
675 (alpha := Maybe fsk) we are in trouble! Instead, we should refrain from solving
676 it and keep it as wanted. In inference mode we'll end up quantifying over
677 (alpha ~ Maybe (E alpha))
678 Hence, 'solveWithIdentity' performs a small occurs check before
679 actually solving. But this occurs check *must look through* flatten skolems.
681 However, it may be the case that the flatten skolem in hand is equal to some other
682 flatten skolem whith *does not* mention our unification variable. Here's a typical example:
684 Example 2: (The need of keeping track of flatten skolem equivalence classes)
685 ****************************************************************************
689 After canonicalization:
694 After some reactions:
699 At this point, we will try to spontaneously solve (alpha ~ f2) which remains as yet unsolved.
700 We will look inside f2, which immediately mentions (F alpha), so it's not good to unify! However
701 by looking at the equivalence class of the flatten skolems, we can see that it is fine to
702 unify (alpha ~ f1) which solves our goals!
704 Example 3: (The need of looking through TyBinds for already spontaneously solved variables)
705 *******************************************************************************************
706 A similar problem happens because of other spontaneous solving. Suppose we have the
707 following wanteds, arriving in this exact order:
708 (first) w: beta ~ alpha
709 (second) w: alpha ~ fsk
710 (third) g: F beta ~ fsk
711 Then, we first spontaneously solve the first constraint, making (beta := alpha), and having
712 (beta ~ alpha) as given. *Then* we encounter the second wanted (alpha ~ fsk). "fsk" does not
713 obviously mention alpha, so naively we can also spontaneously solve (alpha := fsk). But
714 that is wrong since fsk mentions beta, which has already secretly been unified to alpha!
716 To avoid this problem, the same occurs check must unveil rewritings that can happen because
717 of spontaneously having solved other constraints.
719 Example 4: (Orientation of (tv ~ xi) equalities)
720 ************************************************
721 We orient equalities (tv ~ xi) so that flatten skolems appear on the left, if possible. Here
722 is an example of why this is needed:
724 [Wanted] w1: alpha ~ fsk
725 [Given] g1: F alpha ~ fsk
727 Flatten skolem equivalence class = []
729 Assume that g2 is *not* oriented properly, as shown above. Then we would like to spontaneously
730 solve w1 but we can't set alpha := fsk, since fsk hides the type F alpha. However, by using
731 the equation g2 it would be possible to solve w1 by setting alpha := b. In other words, it is
732 not enough to look at a flatten skolem equivalence class to try to find alternatives to unify
733 with. We may have to go to other variables.
735 By orienting the equalities so that flatten skolems are in the LHS we are eliminating them
736 as much as possible from the RHS of other wanted equalities, and hence it suffices to look
737 in their flatten skolem equivalence classes.
739 This situation appears in the IndTypesPerf test case, inside indexed-types/.
741 Note [Avoid double unifications]
742 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
743 The spontaneous solver has to return a given which mentions the unified unification
744 variable *on the left* of the equality. Here is what happens if not:
745 Original wanted: (a ~ alpha), (alpha ~ Int)
746 We spontaneously solve the first wanted, without changing the order!
747 given : a ~ alpha [having unified alpha := a]
748 Now the second wanted comes along, but he cannot rewrite the given, so we simply continue.
749 At the end we spontaneously solve that guy, *reunifying* [alpha := Int]
751 We avoid this problem by orienting the given so that the unification
752 variable is on the left. [Note that alternatively we could attempt to
753 enforce this at canonicalization]
755 See also Note [No touchables as FunEq RHS] in TcSMonad; avoiding
756 double unifications is the main reason we disallow touchable
757 unification variables as RHS of type family equations: F xis ~ alpha.
761 solveWithIdentity :: OrientFlag
763 -> CoVar -> CtFlavor -> TcTyVar -> Xi
764 -> TcS (Maybe SWorkList)
765 -- Solve with the identity coercion
766 -- Precondition: kind(xi) is a sub-kind of kind(tv)
767 -- Precondition: CtFlavor is Wanted or Derived
768 -- See [New Wanted Superclass Work] to see why solveWithIdentity
769 -- must work for Derived as well as Wanted
770 solveWithIdentity or_flag inerts cv gw tv xi
771 = do { tybnds <- getTcSTyBindsMap
772 ; case occurCheck tybnds inerts tv xi of
773 Nothing -> return Nothing
774 Just (xi_unflat,coi) -> solve_with xi_unflat coi }
776 solve_with xi_unflat coi -- coi : xi_unflat ~ xi
777 = do { traceTcS "Sneaky unification:" $
778 vcat [text "Coercion variable: " <+> ppr gw,
779 text "Coercion: " <+> pprEq (mkTyVarTy tv) xi,
780 text "Left Kind is : " <+> ppr (typeKind (mkTyVarTy tv)),
781 text "Right Kind is : " <+> ppr (typeKind xi)
783 -- ; setWantedTyBind tv xi_unflat -- Set tv := xi_unflat
784 -- ; cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi_unflat xi_unflat
785 ; let flav = mkGivenFlavor gw UnkSkol
786 ; (cts, co) <- case coi of
787 ACo co -> do { cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi_unflat xi_unflat
788 ; setWantedTyBind tv xi_unflat
789 ; can_eqs <- case or_flag of
790 OrientThisWay -> canEq flav cv_given (mkTyVarTy tv) xi_unflat
791 OrientOtherWay -> canEq flav cv_given xi_unflat (mkTyVarTy tv)
792 ; return (can_eqs, co) }
793 IdCo co -> do { cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi xi
794 ; setWantedTyBind tv xi
795 ; can_eqs <- case or_flag of
796 OrientThisWay -> canEq flav cv_given (mkTyVarTy tv) xi
797 OrientOtherWay -> canEq flav cv_given xi (mkTyVarTy tv)
798 ; return (can_eqs, co) }
800 Wanted {} -> setWantedCoBind cv co
801 Derived {} -> setDerivedCoBind cv co
802 _ -> pprPanic "Can't spontaneously solve *given*" empty
803 -- See Note [Avoid double unifications]
804 ; return $ Just cts }
806 occurCheck :: VarEnv (TcTyVar, TcType) -> InertSet
807 -> TcTyVar -> TcType -> Maybe (TcType,CoercionI)
808 -- Traverse @ty@ to make sure that @tv@ does not appear under some flatten skolem.
809 -- If it appears under some flatten skolem look in that flatten skolem equivalence class
810 -- (see Note [InertSet FlattenSkolemEqClass], [Loopy Spontaneous Solving]) to see if you
811 -- can find a different flatten skolem to use, that is, one that does not mention @tv@.
813 -- Postcondition: Just (ty', coi) = occurCheck binds inerts tv ty
815 -- NB: The returned type ty' may not be flat!
817 occurCheck ty_binds inerts the_tv the_ty
818 = ok emptyVarSet the_ty
820 -- If (fsk `elem` bad) then tv occurs in any rendering
821 -- of the type under the expansion of fsk
822 ok bad this_ty@(TyConApp tc tys)
823 | Just tys_cois <- allMaybes (map (ok bad) tys)
824 , (tys',cois') <- unzip tys_cois
825 = Just (TyConApp tc tys', mkTyConAppCoI tc cois')
826 | isSynTyCon tc, Just ty_expanded <- tcView this_ty
827 = ok bad ty_expanded -- See Note [Type synonyms and the occur check] in TcUnify
829 | Just (sty',coi) <- ok_pred bad sty
830 = Just (PredTy sty', coi)
831 ok bad (FunTy arg res)
832 | Just (arg', coiarg) <- ok bad arg, Just (res', coires) <- ok bad res
833 = Just (FunTy arg' res', mkFunTyCoI coiarg coires)
834 ok bad (AppTy fun arg)
835 | Just (fun', coifun) <- ok bad fun, Just (arg', coiarg) <- ok bad arg
836 = Just (AppTy fun' arg', mkAppTyCoI coifun coiarg)
837 ok bad (ForAllTy tv1 ty1)
838 -- WARNING: What if it is a (t1 ~ t2) => t3? It's not handled properly at the moment.
839 | Just (ty1', coi) <- ok bad ty1
840 = Just (ForAllTy tv1 ty1', mkForAllTyCoI tv1 coi)
843 ok bad this_ty@(TyVarTy tv)
844 | tv == the_tv = Nothing -- Occurs check error
845 | not (isTcTyVar tv) = Just (this_ty, IdCo this_ty) -- Bound var
846 | FlatSkol zty <- tcTyVarDetails tv = ok_fsk bad tv zty
847 | Just (_,ty) <- lookupVarEnv ty_binds tv = ok bad ty
848 | otherwise = Just (this_ty, IdCo this_ty)
850 -- Check if there exists a ty bind already, as a result of sneaky unification.
852 ok _bad _ty = Nothing
855 ok_pred bad (ClassP cn tys)
856 | Just tys_cois <- allMaybes $ map (ok bad) tys
857 = let (tys', cois') = unzip tys_cois
858 in Just (ClassP cn tys', mkClassPPredCoI cn cois')
859 ok_pred bad (IParam nm ty)
860 | Just (ty',co') <- ok bad ty
861 = Just (IParam nm ty', mkIParamPredCoI nm co')
862 ok_pred bad (EqPred ty1 ty2)
863 | Just (ty1',coi1) <- ok bad ty1, Just (ty2',coi2) <- ok bad ty2
864 = Just (EqPred ty1' ty2', mkEqPredCoI coi1 coi2)
865 ok_pred _ _ = Nothing
869 | fsk `elemVarSet` bad
870 -- We are already trying to find a rendering of fsk,
871 -- and to do that it seems we need a rendering, so fail
874 = firstJusts (ok new_bad zty : map (go_under_fsk new_bad) fsk_equivs)
876 fsk_equivs = getFskEqClass inerts fsk
877 new_bad = bad `extendVarSetList` (fsk : map fst fsk_equivs)
880 go_under_fsk bad_tvs (fsk,co)
881 | FlatSkol zty <- tcTyVarDetails fsk
882 = case ok bad_tvs zty of
884 Just (ty,coi') -> Just (ty, mkTransCoI coi' (ACo co))
885 | otherwise = pprPanic "go_down_equiv" (ppr fsk)
889 *********************************************************************************
891 The interact-with-inert Stage
893 *********************************************************************************
896 -- Interaction result of WorkItem <~> AtomicInert
898 = IR { ir_stop :: StopOrContinue
900 -- => Reagent (work item) consumed.
901 -- ContinueWith new_reagent
902 -- => Reagent transformed but keep gathering interactions.
903 -- The transformed item remains inert with respect
904 -- to any previously encountered inerts.
906 , ir_inert_action :: InertAction
907 -- Whether the inert item should remain in the InertSet.
909 , ir_new_work :: WorkList
910 -- new work items to add to the WorkList
912 , ir_improvement :: Maybe FDImprovement -- In case improvement kicked in
915 -- What to do with the inert reactant.
916 data InertAction = KeepInert | DropInert
919 mkIRContinue :: Monad m => WorkItem -> InertAction -> WorkList -> m InteractResult
920 mkIRContinue wi keep newWork = return $ IR (ContinueWith wi) keep newWork Nothing
922 mkIRStop :: Monad m => InertAction -> WorkList -> m InteractResult
923 mkIRStop keep newWork = return $ IR Stop keep newWork Nothing
925 mkIRStop_RecordImprovement :: Monad m => InertAction -> WorkList -> FDImprovement -> m InteractResult
926 mkIRStop_RecordImprovement keep newWork fdimpr = return $ IR Stop keep newWork (Just fdimpr)
929 dischargeWorkItem :: Monad m => m InteractResult
930 dischargeWorkItem = mkIRStop KeepInert emptyWorkList
932 noInteraction :: Monad m => WorkItem -> m InteractResult
933 noInteraction workItem = mkIRContinue workItem KeepInert emptyWorkList
935 data WhichComesFromInert = LeftComesFromInert | RightComesFromInert
936 -- See Note [Efficient Orientation, Case 2]
939 ---------------------------------------------------
940 -- Interact a single WorkItem with the equalities of an inert set as far as possible, i.e. until we
941 -- get a Stop result from an individual reaction (i.e. when the WorkItem is consumed), or until we've
942 -- interact the WorkItem with the entire equalities of the InertSet
944 interactWithInertEqsStage :: SimplifierStage
945 interactWithInertEqsStage workItem inert
946 = foldISEqCtsM interactNext initITR inert
947 where initITR = SR { sr_inerts = IS { inert_eqs = emptyCCan -- We will fold over the equalities
948 , inert_fsks = Map.empty -- which will generate those two again
949 , inert_cts = inert_cts inert
950 , inert_fds = inert_fds inert
952 , sr_new_work = emptyWorkList
953 , sr_stop = ContinueWith workItem }
956 ---------------------------------------------------
957 -- Interact a single WorkItem with *non-equality* constraints in the inert set.
958 -- Precondition: equality interactions must have already happened, hence we have
959 -- to pick up some information from the incoming inert, before folding over the
960 -- "Other" constraints it contains!
961 interactWithInertsStage :: SimplifierStage
962 interactWithInertsStage workItem inert
963 = foldISOtherCtsM interactNext initITR inert
965 initITR = SR { -- Pick up: (1) equations, (2) FD improvements, (3) FlatSkol equiv. classes
966 sr_inerts = IS { inert_eqs = inert_eqs inert
967 , inert_cts = emptyCCan
968 , inert_fds = inert_fds inert
969 , inert_fsks = inert_fsks inert }
970 , sr_new_work = emptyWorkList
971 , sr_stop = ContinueWith workItem }
973 interactNext :: StageResult -> AtomicInert -> TcS StageResult
974 interactNext it inert
975 | ContinueWith workItem <- sr_stop it
976 = do { let inerts = sr_inerts it
977 fdimprs_old = getFDImprovements inerts
979 ; ir <- interactWithInert fdimprs_old inert workItem
981 -- New inerts depend on whether we KeepInert or not and must
982 -- be updated with FD improvement information from the interaction result (ir)
983 ; let inerts_new = updInertSetFDImprs upd_inert (ir_improvement ir)
984 upd_inert = if ir_inert_action ir == KeepInert
985 then inerts `updInertSet` inert else inerts
987 ; return $ SR { sr_inerts = inerts_new
988 , sr_new_work = sr_new_work it `unionWorkLists` ir_new_work ir
989 , sr_stop = ir_stop ir } }
991 = return $ it { sr_inerts = (sr_inerts it) `updInertSet` inert }
993 -- Do a single interaction of two constraints.
994 interactWithInert :: FDImprovements -> AtomicInert -> WorkItem -> TcS InteractResult
995 interactWithInert fdimprs inert workitem
996 = do { ctxt <- getTcSContext
997 ; let is_allowed = allowedInteraction (simplEqsOnly ctxt) inert workitem
998 inert_ev = cc_id inert
999 work_ev = cc_id workitem
1001 -- Never interact a wanted and a derived where the derived's evidence
1002 -- mentions the wanted evidence in an unguarded way.
1003 -- See Note [Superclasses and recursive dictionaries]
1004 -- and Note [New Wanted Superclass Work]
1005 -- We don't have to do this for givens, as we fully know the evidence for them.
1007 case (cc_flavor inert, cc_flavor workitem) of
1008 (Wanted loc, Derived {}) -> isGoodRecEv work_ev (WantedEvVar inert_ev loc)
1009 (Derived {}, Wanted loc) -> isGoodRecEv inert_ev (WantedEvVar work_ev loc)
1012 ; if is_allowed && rec_ev_ok then
1013 doInteractWithInert fdimprs inert workitem
1015 noInteraction workitem
1018 allowedInteraction :: Bool -> AtomicInert -> WorkItem -> Bool
1019 -- Allowed interactions
1020 allowedInteraction eqs_only (CDictCan {}) (CDictCan {}) = not eqs_only
1021 allowedInteraction eqs_only (CIPCan {}) (CIPCan {}) = not eqs_only
1022 allowedInteraction _ _ _ = True
1024 --------------------------------------------
1025 doInteractWithInert :: FDImprovements -> CanonicalCt -> CanonicalCt -> TcS InteractResult
1026 -- Identical class constraints.
1028 doInteractWithInert fdimprs
1029 (CDictCan { cc_id = d1, cc_flavor = fl1, cc_class = cls1, cc_tyargs = tys1 })
1030 workItem@(CDictCan { cc_id = d2, cc_flavor = fl2, cc_class = cls2, cc_tyargs = tys2 })
1031 | cls1 == cls2 && (and $ zipWith tcEqType tys1 tys2)
1032 = solveOneFromTheOther (d1,fl1) workItem
1034 | cls1 == cls2 && (not (isGiven fl1 && isGiven fl2))
1035 = -- See Note [When improvement happens]
1036 do { let pty1 = ClassP cls1 tys1
1037 pty2 = ClassP cls2 tys2
1038 work_item_pred_loc = (pty2, ppr d2)
1039 inert_pred_loc = (pty1, ppr d1)
1040 loc = combineCtLoc fl1 fl2
1041 eqn_pred_locs = improveFromAnother work_item_pred_loc inert_pred_loc
1043 ; wevvars <- mkWantedFunDepEqns loc eqn_pred_locs
1044 ; fd_work <- canWanteds wevvars
1045 -- See Note [Generating extra equalities]
1046 ; traceTcS "Checking if improvements existed." (ppr fdimprs)
1047 ; if isEmptyWorkList fd_work || haveBeenImproved fdimprs pty1 pty2 then
1049 mkIRContinue workItem KeepInert fd_work
1050 else do { traceTcS "Recording improvement and throwing item back in worklist." (ppr (pty1,pty2))
1051 ; mkIRStop_RecordImprovement KeepInert
1052 (fd_work `unionWorkLists` workListFromCCan workItem) (pty1,pty2)
1054 -- See Note [FunDep Reactions]
1057 -- Class constraint and given equality: use the equality to rewrite
1058 -- the class constraint.
1059 doInteractWithInert _fdimprs
1060 (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi })
1061 (CDictCan { cc_id = dv, cc_flavor = wfl, cc_class = cl, cc_tyargs = xis })
1062 | ifl `canRewrite` wfl
1063 , tv `elemVarSet` tyVarsOfTypes xis
1064 = if isDerivedSC wfl then
1065 mkIRStop KeepInert $ emptyWorkList -- See Note [Adding Derived Superclasses]
1066 else do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,wfl,cl,xis)
1067 -- Continue with rewritten Dictionary because we can only be in the
1068 -- interactWithEqsStage, so the dictionary is inert.
1069 ; mkIRContinue rewritten_dict KeepInert emptyWorkList }
1071 doInteractWithInert _fdimprs
1072 (CDictCan { cc_id = dv, cc_flavor = ifl, cc_class = cl, cc_tyargs = xis })
1073 workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
1074 | wfl `canRewrite` ifl
1075 , tv `elemVarSet` tyVarsOfTypes xis
1076 = if isDerivedSC ifl then
1077 mkIRContinue workItem DropInert emptyWorkList -- No need to do any rewriting,
1078 -- see Note [Adding Derived Superclasses]
1079 else do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,ifl,cl,xis)
1080 ; mkIRContinue workItem DropInert (workListFromCCan rewritten_dict) }
1082 -- Class constraint and given equality: use the equality to rewrite
1083 -- the class constraint.
1084 doInteractWithInert _fdimprs
1085 (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi })
1086 (CIPCan { cc_id = ipid, cc_flavor = wfl, cc_ip_nm = nm, cc_ip_ty = ty })
1087 | ifl `canRewrite` wfl
1088 , tv `elemVarSet` tyVarsOfType ty
1089 = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,wfl,nm,ty)
1090 ; mkIRContinue rewritten_ip KeepInert emptyWorkList }
1092 doInteractWithInert _fdimprs
1093 (CIPCan { cc_id = ipid, cc_flavor = ifl, cc_ip_nm = nm, cc_ip_ty = ty })
1094 workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
1095 | wfl `canRewrite` ifl
1096 , tv `elemVarSet` tyVarsOfType ty
1097 = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,ifl,nm,ty)
1098 ; mkIRContinue workItem DropInert (workListFromCCan rewritten_ip) }
1100 -- Two implicit parameter constraints. If the names are the same,
1101 -- but their types are not, we generate a wanted type equality
1102 -- that equates the type (this is "improvement").
1103 -- However, we don't actually need the coercion evidence,
1104 -- so we just generate a fresh coercion variable that isn't used anywhere.
1105 doInteractWithInert _fdimprs
1106 (CIPCan { cc_id = id1, cc_flavor = ifl, cc_ip_nm = nm1, cc_ip_ty = ty1 })
1107 workItem@(CIPCan { cc_flavor = wfl, cc_ip_nm = nm2, cc_ip_ty = ty2 })
1108 | nm1 == nm2 && isGiven wfl && isGiven ifl
1109 = -- See Note [Overriding implicit parameters]
1110 -- Dump the inert item, override totally with the new one
1111 -- Do not require type equality
1112 mkIRContinue workItem DropInert emptyWorkList
1114 | nm1 == nm2 && ty1 `tcEqType` ty2
1115 = solveOneFromTheOther (id1,ifl) workItem
1118 = -- See Note [When improvement happens]
1119 do { co_var <- newWantedCoVar ty1 ty2
1120 ; let flav = Wanted (combineCtLoc ifl wfl)
1121 ; cans <- mkCanonical flav co_var
1122 ; mkIRContinue workItem KeepInert cans }
1125 -- Inert: equality, work item: function equality
1127 -- Never rewrite a given with a wanted equality, and a type function
1128 -- equality can never rewrite an equality. Note also that if we have
1129 -- F x1 ~ x2 and a ~ x3, and a occurs in x2, we don't rewrite it. We
1130 -- can wait until F x1 ~ x2 matches another F x1 ~ x4, and only then
1131 -- we will ``expose'' x2 and x4 to rewriting.
1133 -- Otherwise, we can try rewriting the type function equality with the equality.
1134 doInteractWithInert _fdimprs
1135 (CTyEqCan { cc_id = cv1, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi1 })
1136 (CFunEqCan { cc_id = cv2, cc_flavor = wfl, cc_fun = tc
1137 , cc_tyargs = args, cc_rhs = xi2 })
1138 | ifl `canRewrite` wfl
1139 , tv `elemVarSet` tyVarsOfTypes args
1140 = do { rewritten_funeq <- rewriteFunEq (cv1,tv,xi1) (cv2,wfl,tc,args,xi2)
1141 ; mkIRStop KeepInert (workListFromCCan rewritten_funeq) }
1142 -- must Stop here, because we may no longer be inert after the rewritting.
1144 -- Inert: function equality, work item: equality
1145 doInteractWithInert _fdimprs
1146 (CFunEqCan {cc_id = cv1, cc_flavor = ifl, cc_fun = tc
1147 , cc_tyargs = args, cc_rhs = xi1 })
1148 workItem@(CTyEqCan { cc_id = cv2, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi2 })
1149 | wfl `canRewrite` ifl
1150 , tv `elemVarSet` tyVarsOfTypes args
1151 = do { rewritten_funeq <- rewriteFunEq (cv2,tv,xi2) (cv1,ifl,tc,args,xi1)
1152 ; mkIRContinue workItem DropInert (workListFromCCan rewritten_funeq) }
1154 doInteractWithInert _fdimprs
1155 (CFunEqCan { cc_id = cv1, cc_flavor = fl1, cc_fun = tc1
1156 , cc_tyargs = args1, cc_rhs = xi1 })
1157 workItem@(CFunEqCan { cc_id = cv2, cc_flavor = fl2, cc_fun = tc2
1158 , cc_tyargs = args2, cc_rhs = xi2 })
1159 | fl1 `canSolve` fl2 && lhss_match
1160 = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
1161 ; mkIRStop KeepInert cans }
1162 | fl2 `canSolve` fl1 && lhss_match
1163 = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
1164 ; mkIRContinue workItem DropInert cans }
1166 lhss_match = tc1 == tc2 && and (zipWith tcEqType args1 args2)
1168 doInteractWithInert _fdimprs
1169 inert@(CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
1170 workItem@(CTyEqCan { cc_id = cv2, cc_flavor = fl2, cc_tyvar = tv2, cc_rhs = xi2 })
1171 -- Check for matching LHS
1172 | fl1 `canSolve` fl2 && tv1 == tv2
1173 = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
1174 ; mkIRStop KeepInert cans }
1176 | fl2 `canSolve` fl1 && tv1 == tv2
1177 = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
1178 ; mkIRContinue workItem DropInert cans }
1180 -- Check for rewriting RHS
1181 | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfType xi2
1182 = do { rewritten_eq <- rewriteEqRHS (cv1,tv1,xi1) (cv2,fl2,tv2,xi2)
1183 ; mkIRStop KeepInert rewritten_eq }
1184 | fl2 `canRewrite` fl1 && tv2 `elemVarSet` tyVarsOfType xi1
1185 = do { rewritten_eq <- rewriteEqRHS (cv2,tv2,xi2) (cv1,fl1,tv1,xi1)
1186 ; mkIRContinue workItem DropInert rewritten_eq }
1188 -- Finally, if workitem is a Flatten Equivalence Class constraint and the
1189 -- inert is a wanted constraint, even when the workitem cannot rewrite the
1190 -- inert, drop the inert out because you may have to reconsider solving the
1191 -- inert *using* the equivalence class you created. See note [Loopy Spontaneous Solving]
1192 -- and [InertSet FlattenSkolemEqClass]
1194 | not $ isGiven fl1, -- The inert is wanted or derived
1195 isMetaTyVar tv1, -- and has a unification variable lhs
1196 FlatSkol {} <- tcTyVarDetails tv2, -- And workitem is a flatten skolem equality
1197 Just tv2' <- tcGetTyVar_maybe xi2, FlatSkol {} <- tcTyVarDetails tv2'
1198 = mkIRContinue workItem DropInert (workListFromCCan inert)
1201 -- Fall-through case for all other situations
1202 doInteractWithInert _fdimprs _ workItem = noInteraction workItem
1204 -------------------------
1205 -- Equational Rewriting
1206 rewriteDict :: (CoVar, TcTyVar, Xi) -> (DictId, CtFlavor, Class, [Xi]) -> TcS CanonicalCt
1207 rewriteDict (cv,tv,xi) (dv,gw,cl,xis)
1208 = do { let cos = substTysWith [tv] [mkCoVarCoercion cv] xis -- xis[tv] ~ xis[xi]
1209 args = substTysWith [tv] [xi] xis
1211 dict_co = mkTyConCoercion con cos
1212 ; dv' <- newDictVar cl args
1214 Wanted {} -> setDictBind dv (EvCast dv' (mkSymCoercion dict_co))
1215 _given_or_derived -> setDictBind dv' (EvCast dv dict_co)
1216 ; return (CDictCan { cc_id = dv'
1219 , cc_tyargs = args }) }
1221 rewriteIP :: (CoVar,TcTyVar,Xi) -> (EvVar,CtFlavor, IPName Name, TcType) -> TcS CanonicalCt
1222 rewriteIP (cv,tv,xi) (ipid,gw,nm,ty)
1223 = do { let ip_co = substTyWith [tv] [mkCoVarCoercion cv] ty -- ty[tv] ~ t[xi]
1224 ty' = substTyWith [tv] [xi] ty
1225 ; ipid' <- newIPVar nm ty'
1227 Wanted {} -> setIPBind ipid (EvCast ipid' (mkSymCoercion ip_co))
1228 _given_or_derived -> setIPBind ipid' (EvCast ipid ip_co)
1229 ; return (CIPCan { cc_id = ipid'
1232 , cc_ip_ty = ty' }) }
1234 rewriteFunEq :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TyCon, [Xi], Xi) -> TcS CanonicalCt
1235 rewriteFunEq (cv1,tv,xi1) (cv2,gw, tc,args,xi2)
1236 = do { let arg_cos = substTysWith [tv] [mkCoVarCoercion cv1] args
1237 args' = substTysWith [tv] [xi1] args
1238 fun_co = mkTyConCoercion tc arg_cos
1239 ; cv2' <- case gw of
1240 Wanted {} -> do { cv2' <- newWantedCoVar (mkTyConApp tc args') xi2
1241 ; setWantedCoBind cv2 $
1242 mkTransCoercion fun_co (mkCoVarCoercion cv2')
1244 _giv_or_der -> newGivOrDerCoVar (mkTyConApp tc args') xi2 $
1245 mkTransCoercion (mkSymCoercion fun_co) (mkCoVarCoercion cv2)
1246 ; return (CFunEqCan { cc_id = cv2'
1253 rewriteEqRHS :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TcTyVar,Xi) -> TcS WorkList
1254 -- Use the first equality to rewrite the second, flavors already checked.
1255 -- E.g. c1 : tv1 ~ xi1 c2 : tv2 ~ xi2
1256 -- rewrites c2 to give
1257 -- c2' : tv2 ~ xi2[xi1/tv1]
1258 -- We must do an occurs check to sure the new constraint is canonical
1259 -- So we might return an empty bag
1260 rewriteEqRHS (cv1,tv1,xi1) (cv2,gw,tv2,xi2)
1261 | Just tv2' <- tcGetTyVar_maybe xi2'
1262 , tv2 == tv2' -- In this case xi2[xi1/tv1] = tv2, so we have tv2~tv2
1263 = do { when (isWanted gw) (setWantedCoBind cv2 (mkSymCoercion co2'))
1264 ; return emptyCCan }
1269 -> do { cv2' <- newWantedCoVar (mkTyVarTy tv2) xi2'
1270 ; setWantedCoBind cv2 $
1271 mkCoVarCoercion cv2' `mkTransCoercion` mkSymCoercion co2'
1274 -> newGivOrDerCoVar (mkTyVarTy tv2) xi2' $
1275 mkCoVarCoercion cv2 `mkTransCoercion` co2'
1277 ; xi2'' <- canOccursCheck gw tv2 xi2' -- we know xi2' is *not* tv2
1278 ; canEq gw cv2' (mkTyVarTy tv2) xi2''
1281 xi2' = substTyWith [tv1] [xi1] xi2
1282 co2' = substTyWith [tv1] [mkCoVarCoercion cv1] xi2 -- xi2 ~ xi2[xi1/tv1]
1285 rewriteEqLHS :: WhichComesFromInert -> (Coercion,Xi) -> (CoVar,CtFlavor,Xi) -> TcS WorkList
1286 -- Used to ineract two equalities of the following form:
1287 -- First Equality: co1: (XXX ~ xi1)
1288 -- Second Equality: cv2: (XXX ~ xi2)
1289 -- Where the cv1 `canSolve` cv2 equality
1290 -- We have an option of creating new work (xi1 ~ xi2) OR (xi2 ~ xi1),
1291 -- See Note [Efficient Orientation] for that
1292 rewriteEqLHS which (co1,xi1) (cv2,gw,xi2)
1293 = do { cv2' <- case (isWanted gw, which) of
1294 (True,LeftComesFromInert) ->
1295 do { cv2' <- newWantedCoVar xi2 xi1
1296 ; setWantedCoBind cv2 $
1297 co1 `mkTransCoercion` mkSymCoercion (mkCoVarCoercion cv2')
1299 (True,RightComesFromInert) ->
1300 do { cv2' <- newWantedCoVar xi1 xi2
1301 ; setWantedCoBind cv2 $
1302 co1 `mkTransCoercion` mkCoVarCoercion cv2'
1304 (False,LeftComesFromInert) ->
1305 newGivOrDerCoVar xi2 xi1 $
1306 mkSymCoercion (mkCoVarCoercion cv2) `mkTransCoercion` co1
1307 (False,RightComesFromInert) ->
1308 newGivOrDerCoVar xi1 xi2 $
1309 mkSymCoercion co1 `mkTransCoercion` mkCoVarCoercion cv2
1310 ; mkCanonical gw cv2'
1313 solveOneFromTheOther :: (EvVar, CtFlavor) -> CanonicalCt -> TcS InteractResult
1314 -- First argument inert, second argument workitem. They both represent
1315 -- wanted/given/derived evidence for the *same* predicate so we try here to
1316 -- discharge one directly from the other.
1318 -- Precondition: value evidence only (implicit parameters, classes)
1320 solveOneFromTheOther (iid,ifl) workItem
1321 -- Both derived needs a special case. You might think that we do not need
1322 -- two evidence terms for the same claim. But, since the evidence is partial,
1323 -- either evidence may do in some cases; see TcSMonad.isGoodRecEv.
1324 -- See also Example 3 in Note [Superclasses and recursive dictionaries]
1325 | isDerived ifl && isDerived wfl
1326 = noInteraction workItem
1328 | ifl `canSolve` wfl
1329 = do { unless (isGiven wfl) $ setEvBind wid (EvId iid)
1330 -- Overwrite the binding, if one exists
1331 -- For Givens, which are lambda-bound, nothing to overwrite,
1332 ; dischargeWorkItem }
1334 | otherwise -- wfl `canSolve` ifl
1335 = do { unless (isGiven ifl) $ setEvBind iid (EvId wid)
1336 ; mkIRContinue workItem DropInert emptyWorkList }
1339 wfl = cc_flavor workItem
1340 wid = cc_id workItem
1343 Note [Superclasses and recursive dictionaries]
1344 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1345 Overlaps with Note [SUPERCLASS-LOOP 1]
1346 Note [SUPERCLASS-LOOP 2]
1347 Note [Recursive instances and superclases]
1348 ToDo: check overlap and delete redundant stuff
1350 Right before adding a given into the inert set, we must
1351 produce some more work, that will bring the superclasses
1352 of the given into scope. The superclass constraints go into
1355 When we simplify a wanted constraint, if we first see a matching
1356 instance, we may produce new wanted work. To (1) avoid doing this work
1357 twice in the future and (2) to handle recursive dictionaries we may ``cache''
1358 this item as solved (in effect, given) into our inert set and with that add
1359 its superclass constraints (as given) in our worklist.
1361 But now we have added partially solved constraints to the worklist which may
1362 interact with other wanteds. Consider the example:
1366 class Eq b => Foo a b --- 0-th selector
1367 instance Eq a => Foo [a] a --- fooDFun
1369 and wanted (Foo [t] t). We are first going to see that the instance matches
1370 and create an inert set that includes the solved (Foo [t] t) and its
1372 d1 :_g Foo [t] t d1 := EvDFunApp fooDFun d3
1373 d2 :_g Eq t d2 := EvSuperClass d1 0
1374 Our work list is going to contain a new *wanted* goal
1376 It is wrong to react the wanted (Eq t) with the given (Eq t) because that would
1377 construct loopy evidence. Hence the check isGoodRecEv in doInteractWithInert.
1379 OK, so we have ruled out bad behaviour, but how do we ge recursive dictionaries,
1384 data D r = ZeroD | SuccD (r (D r));
1386 instance (Eq (r (D r))) => Eq (D r) where
1387 ZeroD == ZeroD = True
1388 (SuccD a) == (SuccD b) = a == b
1391 equalDC :: D [] -> D [] -> Bool;
1394 We need to prove (Eq (D [])). Here's how we go:
1398 by instance decl, holds if
1402 *BUT* we have an inert set which gives us (no superclasses):
1404 By the instance declaration of Eq we can show the 'd2' goal if
1406 where d2 = dfEqList d3
1408 Now, however this wanted can interact with our inert d1 to set:
1410 and solve the goal. Why was this interaction OK? Because, if we chase the
1411 evidence of d1 ~~> dfEqD d2 ~~-> dfEqList d3, so by setting d3 := d1 we
1413 d3 := dfEqD2 (dfEqList d3)
1414 which is FINE because the use of d3 is protected by the instance function
1417 So, our strategy is to try to put solved wanted dictionaries into the
1418 inert set along with their superclasses (when this is meaningful,
1419 i.e. when new wanted goals are generated) but solve a wanted dictionary
1420 from a given only in the case where the evidence variable of the
1421 wanted is mentioned in the evidence of the given (recursively through
1422 the evidence binds) in a protected way: more instance function applications
1423 than superclass selectors.
1425 Here are some more examples from GHC's previous type checker
1429 This code arises in the context of "Scrap Your Boilerplate with Class"
1433 instance Sat (ctx Char) => Data ctx Char -- dfunData1
1434 instance (Sat (ctx [a]), Data ctx a) => Data ctx [a] -- dfunData2
1436 class Data Maybe a => Foo a
1438 instance Foo t => Sat (Maybe t) -- dfunSat
1440 instance Data Maybe a => Foo a -- dfunFoo1
1441 instance Foo a => Foo [a] -- dfunFoo2
1442 instance Foo [Char] -- dfunFoo3
1444 Consider generating the superclasses of the instance declaration
1445 instance Foo a => Foo [a]
1447 So our problem is this
1449 d1 :_w Data Maybe [t]
1451 We may add the given in the inert set, along with its superclasses
1452 [assuming we don't fail because there is a matching instance, see
1453 tryTopReact, given case ]
1457 d01 :_g Data Maybe t -- d2 := EvDictSuperClass d0 0
1458 d1 :_w Data Maybe [t]
1459 Then d2 can readily enter the inert, and we also do solving of the wanted
1462 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1464 d2 :_w Sat (Maybe [t])
1466 d01 :_g Data Maybe t
1467 Now, we may simplify d2 more:
1470 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1471 d1 :_g Data Maybe [t]
1472 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1476 d01 :_g Data Maybe t
1478 Now, we can just solve d3.
1481 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1482 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1485 d01 :_g Data Maybe t
1486 And now we can simplify d4 again, but since it has superclasses we *add* them to the worklist:
1489 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1490 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1491 d4 :_g Foo [t] d4 := dfunFoo2 d5
1494 d6 :_g Data Maybe [t] d6 := EvDictSuperClass d4 0
1495 d01 :_g Data Maybe t
1496 Now, d5 can be solved! (and its superclass enter scope)
1499 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1500 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1501 d4 :_g Foo [t] d4 := dfunFoo2 d5
1502 d5 :_g Foo t d5 := dfunFoo1 d7
1505 d6 :_g Data Maybe [t]
1506 d8 :_g Data Maybe t d8 := EvDictSuperClass d5 0
1507 d01 :_g Data Maybe t
1510 [1] Suppose we pick d8 and we react him with d01. Which of the two givens should
1511 we keep? Well, we *MUST NOT* drop d01 because d8 contains recursive evidence
1512 that must not be used (look at case interactInert where both inert and workitem
1513 are givens). So we have several options:
1514 - Drop the workitem always (this will drop d8)
1515 This feels very unsafe -- what if the work item was the "good" one
1516 that should be used later to solve another wanted?
1517 - Don't drop anyone: the inert set may contain multiple givens!
1518 [This is currently implemented]
1520 The "don't drop anyone" seems the most safe thing to do, so now we come to problem 2:
1521 [2] We have added both d6 and d01 in the inert set, and we are interacting our wanted
1522 d7. Now the [isRecDictEv] function in the ineration solver
1523 [case inert-given workitem-wanted] will prevent us from interacting d7 := d8
1524 precisely because chasing the evidence of d8 leads us to an unguarded use of d7.
1526 So, no interaction happens there. Then we meet d01 and there is no recursion
1527 problem there [isRectDictEv] gives us the OK to interact and we do solve d7 := d01!
1529 Note [SUPERCLASS-LOOP 1]
1530 ~~~~~~~~~~~~~~~~~~~~~~~~
1531 We have to be very, very careful when generating superclasses, lest we
1532 accidentally build a loop. Here's an example:
1536 class S a => C a where { opc :: a -> a }
1537 class S b => D b where { opd :: b -> b }
1539 instance C Int where
1542 instance D Int where
1545 From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int}
1546 Simplifying, we may well get:
1547 $dfCInt = :C ds1 (opd dd)
1550 Notice that we spot that we can extract ds1 from dd.
1552 Alas! Alack! We can do the same for (instance D Int):
1554 $dfDInt = :D ds2 (opc dc)
1558 And now we've defined the superclass in terms of itself.
1559 Two more nasty cases are in
1564 - Satisfy the superclass context *all by itself*
1565 (tcSimplifySuperClasses)
1566 - And do so completely; i.e. no left-over constraints
1567 to mix with the constraints arising from method declarations
1570 Note [SUPERCLASS-LOOP 2]
1571 ~~~~~~~~~~~~~~~~~~~~~~~~
1572 We need to be careful when adding "the constaint we are trying to prove".
1573 Suppose we are *given* d1:Ord a, and want to deduce (d2:C [a]) where
1575 class Ord a => C a where
1576 instance Ord [a] => C [a] where ...
1578 Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the
1579 superclasses of C [a] to avails. But we must not overwrite the binding
1580 for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
1583 Here's another variant, immortalised in tcrun020
1584 class Monad m => C1 m
1585 class C1 m => C2 m x
1586 instance C2 Maybe Bool
1587 For the instance decl we need to build (C1 Maybe), and it's no good if
1588 we run around and add (C2 Maybe Bool) and its superclasses to the avails
1589 before we search for C1 Maybe.
1591 Here's another example
1592 class Eq b => Foo a b
1593 instance Eq a => Foo [a] a
1597 we'll first deduce that it holds (via the instance decl). We must not
1598 then overwrite the Eq t constraint with a superclass selection!
1600 At first I had a gross hack, whereby I simply did not add superclass constraints
1601 in addWanted, though I did for addGiven and addIrred. This was sub-optimal,
1602 becuase it lost legitimate superclass sharing, and it still didn't do the job:
1603 I found a very obscure program (now tcrun021) in which improvement meant the
1604 simplifier got two bites a the cherry... so something seemed to be an Stop
1605 first time, but reducible next time.
1607 Now we implement the Right Solution, which is to check for loops directly
1608 when adding superclasses. It's a bit like the occurs check in unification.
1610 Note [Recursive instances and superclases]
1611 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1612 Consider this code, which arises in the context of "Scrap Your
1613 Boilerplate with Class".
1617 instance Sat (ctx Char) => Data ctx Char
1618 instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]
1620 class Data Maybe a => Foo a
1622 instance Foo t => Sat (Maybe t)
1624 instance Data Maybe a => Foo a
1625 instance Foo a => Foo [a]
1628 In the instance for Foo [a], when generating evidence for the superclasses
1629 (ie in tcSimplifySuperClasses) we need a superclass (Data Maybe [a]).
1630 Using the instance for Data, we therefore need
1631 (Sat (Maybe [a], Data Maybe a)
1632 But we are given (Foo a), and hence its superclass (Data Maybe a).
1633 So that leaves (Sat (Maybe [a])). Using the instance for Sat means
1634 we need (Foo [a]). And that is the very dictionary we are bulding
1635 an instance for! So we must put that in the "givens". So in this
1637 Given: Foo a, Foo [a]
1638 Wanted: Data Maybe [a]
1640 BUT we must *not not not* put the *superclasses* of (Foo [a]) in
1641 the givens, which is what 'addGiven' would normally do. Why? Because
1642 (Data Maybe [a]) is the superclass, so we'd "satisfy" the wanted
1643 by selecting a superclass from Foo [a], which simply makes a loop.
1645 On the other hand we *must* put the superclasses of (Foo a) in
1646 the givens, as you can see from the derivation described above.
1648 Conclusion: in the very special case of tcSimplifySuperClasses
1649 we have one 'given' (namely the "this" dictionary) whose superclasses
1650 must not be added to 'givens' by addGiven.
1652 There is a complication though. Suppose there are equalities
1653 instance (Eq a, a~b) => Num (a,b)
1654 Then we normalise the 'givens' wrt the equalities, so the original
1655 given "this" dictionary is cast to one of a different type. So it's a
1656 bit trickier than before to identify the "special" dictionary whose
1657 superclasses must not be added. See test
1658 indexed-types/should_run/EqInInstance
1660 We need a persistent property of the dictionary to record this
1661 special-ness. Current I'm using the InstLocOrigin (a bit of a hack,
1662 but cool), which is maintained by dictionary normalisation.
1663 Specifically, the InstLocOrigin is
1665 then the no-superclass thing kicks in. WATCH OUT if you fiddle
1668 Note [MATCHING-SYNONYMS]
1669 ~~~~~~~~~~~~~~~~~~~~~~~~
1670 When trying to match a dictionary (D tau) to a top-level instance, or a
1671 type family equation (F taus_1 ~ tau_2) to a top-level family instance,
1672 we do *not* need to expand type synonyms because the matcher will do that for us.
1675 Note [RHS-FAMILY-SYNONYMS]
1676 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1677 The RHS of a family instance is represented as yet another constructor which is
1678 like a type synonym for the real RHS the programmer declared. Eg:
1679 type instance F (a,a) = [a]
1681 :R32 a = [a] -- internal type synonym introduced
1682 F (a,a) ~ :R32 a -- instance
1684 When we react a family instance with a type family equation in the work list
1685 we keep the synonym-using RHS without expansion.
1688 *********************************************************************************
1690 The top-reaction Stage
1692 *********************************************************************************
1695 -- If a work item has any form of interaction with top-level we get this
1696 data TopInteractResult
1697 = NoTopInt -- No top-level interaction
1699 { tir_new_work :: WorkList -- Sub-goals or new work (could be given,
1700 -- for superclasses)
1701 , tir_new_inert :: StopOrContinue -- The input work item, ready to become *inert* now:
1702 } -- NB: in ``given'' (solved) form if the
1703 -- original was wanted or given and instance match
1704 -- was found, but may also be in wanted form if we
1705 -- only reacted with functional dependencies
1706 -- arising from top-level instances.
1708 topReactionsStage :: SimplifierStage
1709 topReactionsStage workItem inerts
1710 = do { tir <- tryTopReact workItem
1713 return $ SR { sr_inerts = inerts
1714 , sr_new_work = emptyWorkList
1715 , sr_stop = ContinueWith workItem }
1716 SomeTopInt tir_new_work tir_new_inert ->
1717 return $ SR { sr_inerts = inerts
1718 , sr_new_work = tir_new_work
1719 , sr_stop = tir_new_inert
1723 tryTopReact :: WorkItem -> TcS TopInteractResult
1724 tryTopReact workitem
1725 = do { -- A flag controls the amount of interaction allowed
1726 -- See Note [Simplifying RULE lhs constraints]
1727 ctxt <- getTcSContext
1728 ; if allowedTopReaction (simplEqsOnly ctxt) workitem
1729 then do { traceTcS "tryTopReact / calling doTopReact" (ppr workitem)
1730 ; doTopReact workitem }
1731 else return NoTopInt
1734 allowedTopReaction :: Bool -> WorkItem -> Bool
1735 allowedTopReaction eqs_only (CDictCan {}) = not eqs_only
1736 allowedTopReaction _ _ = True
1739 doTopReact :: WorkItem -> TcS TopInteractResult
1740 -- The work item does not react with the inert set,
1741 -- so try interaction with top-level instances
1743 -- Given dictionary; just add superclasses
1744 -- See Note [Given constraint that matches an instance declaration]
1745 doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Given loc
1746 , cc_class = cls, cc_tyargs = xis })
1747 = do { sc_work <- newGivenSCWork dv loc cls xis
1748 ; return $ SomeTopInt sc_work (ContinueWith workItem) }
1750 -- Derived dictionary
1751 -- Do not add any further derived superclasses; their
1752 -- full transitive closure has already been added.
1753 -- But do look for functional dependencies
1754 doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Derived loc _
1755 , cc_class = cls, cc_tyargs = xis })
1756 = do { fd_work <- findClassFunDeps dv cls xis loc
1757 ; if isEmptyWorkList fd_work then
1759 else return $ SomeTopInt { tir_new_work = fd_work
1760 , tir_new_inert = ContinueWith workItem } }
1762 doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Wanted loc
1763 , cc_class = cls, cc_tyargs = xis })
1764 = do { -- See Note [MATCHING-SYNONYMS]
1765 ; lkp_inst_res <- matchClassInst cls xis loc
1766 ; case lkp_inst_res of
1768 do { traceTcS "doTopReact/ no class instance for" (ppr dv)
1769 ; fd_work <- findClassFunDeps dv cls xis loc
1770 ; if isEmptyWorkList fd_work then
1771 do { sc_work <- newDerivedSCWork dv loc cls xis
1772 -- See Note [Adding Derived Superclasses]
1773 -- NB: workItem is inert, but it isn't solved
1774 -- keep it as inert, although it's not solved
1775 -- because we have now reacted all its
1776 -- top-level fundep-induced equalities!
1777 ; return $ SomeTopInt
1778 { tir_new_work = fd_work `unionWorkLists` sc_work
1779 , tir_new_inert = ContinueWith workItem } }
1781 else -- More fundep work produced, don't do any superclass stuff,
1782 -- just thow him back in the worklist, which will prioritize
1783 -- the solution of fd equalities
1785 { tir_new_work = fd_work `unionWorkLists`
1786 workListFromCCan workItem
1787 , tir_new_inert = Stop } }
1789 GenInst wtvs ev_term -> -- Solved
1790 -- No need to do fundeps stuff here; the instance
1791 -- matches already so we won't get any more info
1792 -- from functional dependencies
1793 do { traceTcS "doTopReact/ found class instance for" (ppr dv)
1794 ; setDictBind dv ev_term
1795 ; inst_work <- canWanteds wtvs
1797 -- Solved in one step and no new wanted work produced.
1798 -- i.e we directly matched a top-level instance
1799 -- No point in caching this in 'inert', nor in adding superclasses
1800 then return $ SomeTopInt { tir_new_work = emptyWorkList
1801 , tir_new_inert = Stop }
1803 -- Solved and new wanted work produced, you may cache the
1804 -- (tentatively solved) dictionary as Derived and its superclasses
1805 else do { let solved = makeSolvedByInst workItem
1806 ; sc_work <- newDerivedSCWork dv loc cls xis
1807 -- See Note [Adding Derived Superclasses]
1808 ; return $ SomeTopInt
1809 { tir_new_work = inst_work `unionWorkLists` sc_work
1810 , tir_new_inert = ContinueWith solved } }
1814 doTopReact (CFunEqCan { cc_id = cv, cc_flavor = fl
1815 , cc_fun = tc, cc_tyargs = args, cc_rhs = xi })
1816 = ASSERT (isSynFamilyTyCon tc) -- No associated data families have reached that far
1817 do { match_res <- matchFam tc args -- See Note [MATCHING-SYNONYMS]
1821 MatchInstSingle (rep_tc, rep_tys)
1822 -> do { let Just coe_tc = tyConFamilyCoercion_maybe rep_tc
1823 Just rhs_ty = tcView (mkTyConApp rep_tc rep_tys)
1824 -- Eagerly expand away the type synonym on the
1825 -- RHS of a type function, so that it never
1826 -- appears in an error message
1827 -- See Note [Type synonym families] in TyCon
1828 coe = mkTyConApp coe_tc rep_tys
1830 Wanted {} -> do { cv' <- newWantedCoVar rhs_ty xi
1831 ; setWantedCoBind cv $
1832 coe `mkTransCoercion`
1835 _ -> newGivOrDerCoVar xi rhs_ty $
1836 mkSymCoercion (mkCoVarCoercion cv) `mkTransCoercion` coe
1838 ; can_cts <- mkCanonical fl cv'
1839 ; return $ SomeTopInt can_cts Stop }
1841 -> panicTcS $ text "TcSMonad.matchFam returned multiple instances!"
1845 -- Any other work item does not react with any top-level equations
1846 doTopReact _workItem = return NoTopInt
1848 ----------------------
1849 findClassFunDeps :: EvVar -> Class -> [Xi] -> WantedLoc -> TcS WorkList
1850 -- Look for a fundep reaction beween the wanted item
1851 -- and a top-level instance declaration
1852 findClassFunDeps dv cls xis loc
1853 = do { instEnvs <- getInstEnvs
1854 ; let eqn_pred_locs = improveFromInstEnv (classInstances instEnvs)
1855 (ClassP cls xis, ppr dv)
1856 ; wevvars <- mkWantedFunDepEqns loc eqn_pred_locs
1857 -- NB: fundeps generate some wanted equalities, but
1858 -- we don't use their evidence for anything
1859 ; canWanteds wevvars }
1862 Note [Adding Derived Superclasses]
1863 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1864 Generally speaking, we want to be able to add derived superclasses of
1865 unsolved wanteds, and wanteds that have been partially being solved
1866 via an instance. This is important to be able to simplify the inferred
1867 constraints more (and to allow for recursive dictionaries, less
1868 importantly). Example:
1870 Inferred wanted constraint is (Eq a, Ord a), but we'd only like to
1871 quantify over Ord a, hence we would like to be able to add the
1872 superclass of Ord a as Derived and use it to solve the wanted Eq a.
1874 Hence we will add Derived superclasses in the following two cases:
1875 (1) When we meet an unsolved wanted in top-level reactions
1876 (2) When we partially solve a wanted in top-level reactions using an instance decl.
1878 At that point, we have two options:
1879 (1) Add transitively add *ALL* of the superclasses of the Derived
1880 (2) Add only the immediate ones, but whenever we meet a Derived in
1881 the future, add its own superclasses as Derived.
1883 Option (2) is terrible, because deriveds may be rewritten or kicked
1884 out of the inert set, which will result in slightly rewritten
1885 superclasses being reintroduced in the worklist and the inert set. Eg:
1888 instance Foo a => B [a]
1890 Original constraints:
1892 [Given] co : a ~ Int
1894 We apply the instance to the wanted and put it and its superclasses as
1895 as Deriveds in the inerts:
1898 [Derived] (sel d) : C [a]
1901 [Given] co : a ~ Int
1904 Now, suppose that we interact the Derived with the Given equality, and
1905 kick him out of the inert, the next time around a superclass C [Int]
1906 will be produced -- but we already *have* C [a] in the inerts which
1907 will anyway get rewritten to C [Int].
1909 So we choose (1), and *never* introduce any more superclass work from
1910 Deriveds. This enables yet another optimisation: If we ever meet an
1911 equality that can rewrite a Derived, if that Derived is a superclass
1912 derived (like C [a] above), i.e. not a partially solved one (like B
1913 [a]) above, we may simply completely *discard* that Derived. The
1914 reason is because somewhere in the inert lies the original wanted, or
1915 partially solved constraint that gave rise to that superclass, and
1916 that constraint *will* be kicked out, and *will* result in the
1917 rewritten superclass to be added in the inerts later on, anyway.
1921 Note [FunDep and implicit parameter reactions]
1922 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1923 Currently, our story of interacting two dictionaries (or a dictionary
1924 and top-level instances) for functional dependencies, and implicit
1925 paramters, is that we simply produce new wanted equalities. So for example
1927 class D a b | a -> b where ...
1933 We generate the extra work item
1935 where 'cv' is currently unused. However, this new item reacts with d2,
1936 discharging it in favour of a new constraint d2' thus:
1938 d2 := d2' |> D Int cv
1939 Now d2' can be discharged from d1
1941 We could be more aggressive and try to *immediately* solve the dictionary
1942 using those extra equalities. With the same inert set and work item we
1943 might dischard d2 directly:
1946 d2 := d1 |> D Int cv
1948 But in general it's a bit painful to figure out the necessary coercion,
1949 so we just take the first approach. Here is a better example. Consider:
1950 class C a b c | a -> b
1952 [Given] d1 : C T Int Char
1953 [Wanted] d2 : C T beta Int
1954 In this case, it's *not even possible* to solve the wanted immediately.
1955 So we should simply output the functional dependency and add this guy
1956 [but NOT its superclasses] back in the worklist. Even worse:
1957 [Given] d1 : C T Int beta
1958 [Wanted] d2: C T beta Int
1959 Then it is solvable, but its very hard to detect this on the spot.
1961 It's exactly the same with implicit parameters, except that the
1962 "aggressive" approach would be much easier to implement.
1964 Note [When improvement happens]
1965 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1966 We fire an improvement rule when
1968 * Two constraints match (modulo the fundep)
1969 e.g. C t1 t2, C t1 t3 where C a b | a->b
1970 The two match because the first arg is identical
1972 * At least one is not Given. If they are both given, we don't fire
1973 the reaction because we have no way of constructing evidence for a
1974 new equality nor does it seem right to create a new wanted goal
1975 (because the goal will most likely contain untouchables, which
1976 can't be solved anyway)!
1978 Note that we *do* fire the improvement if one is Given and one is Derived.
1979 The latter can be a superclass of a wanted goal. Example (tcfail138)
1980 class L a b | a -> b
1981 class (G a, L a b) => C a b
1983 instance C a b' => G (Maybe a)
1984 instance C a b => C (Maybe a) a
1985 instance L (Maybe a) a
1987 When solving the superclasses of the (C (Maybe a) a) instance, we get
1988 Given: C a b ... and hance by superclasses, (G a, L a b)
1990 Use the instance decl to get
1992 The (C a b') is inert, so we generate its Derived superclasses (L a b'),
1993 and now we need improvement between that derived superclass an the Given (L a b)
1995 Note [Overriding implicit parameters]
1996 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1998 f :: (?x::a) -> Bool -> a
2000 g v = let ?x::Int = 3
2001 in (f v, let ?x::Bool = True in f v)
2003 This should probably be well typed, with
2004 g :: Bool -> (Int, Bool)
2006 So the inner binding for ?x::Bool *overrides* the outer one.
2007 Hence a work-item Given overrides an inert-item Given.
2009 Note [Given constraint that matches an instance declaration]
2010 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2011 What should we do when we discover that one (or more) top-level
2012 instances match a given (or solved) class constraint? We have
2015 1. Reject the program. The reason is that there may not be a unique
2016 best strategy for the solver. Example, from the OutsideIn(X) paper:
2017 instance P x => Q [x]
2018 instance (x ~ y) => R [x] y
2020 wob :: forall a b. (Q [b], R b a) => a -> Int
2022 g :: forall a. Q [a] => [a] -> Int
2025 will generate the impliation constraint:
2026 Q [a] => (Q [beta], R beta [a])
2027 If we react (Q [beta]) with its top-level axiom, we end up with a
2028 (P beta), which we have no way of discharging. On the other hand,
2029 if we react R beta [a] with the top-level we get (beta ~ a), which
2030 is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
2031 now solvable by the given Q [a].
2033 However, this option is restrictive, for instance [Example 3] from
2034 Note [Recursive dictionaries] will fail to work.
2036 2. Ignore the problem, hoping that the situations where there exist indeed
2037 such multiple strategies are rare: Indeed the cause of the previous
2038 problem is that (R [x] y) yields the new work (x ~ y) which can be
2039 *spontaneously* solved, not using the givens.
2041 We are choosing option 2 below but we might consider having a flag as well.
2044 Note [New Wanted Superclass Work]
2045 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2046 Even in the case of wanted constraints, we add all of its superclasses as
2047 new given work. There are several reasons for this:
2048 a) to minimise error messages;
2049 eg suppose we have wanted (Eq a, Ord a)
2050 then we report only (Ord a) unsoluble
2052 b) to make the smallest number of constraints when *inferring* a type
2053 (same Eq/Ord example)
2055 c) for recursive dictionaries we *must* add the superclasses
2056 so that we can use them when solving a sub-problem
2058 d) To allow FD-like improvement for type families. Assume that
2060 class C a b | a -> b
2061 and we have to solve the implication constraint:
2063 Then, FD improvement can help us to produce a new wanted (beta ~ b)
2065 We want to have the same effect with the type family encoding of
2066 functional dependencies. Namely, consider:
2067 class (F a ~ b) => C a b
2068 Now suppose that we have:
2071 By interacting the given we will get given (F a ~ b) which is not
2072 enough by itself to make us discharge (C a beta). However, we
2073 may create a new derived equality from the super-class of the
2074 wanted constraint (C a beta), namely derived (F a ~ beta).
2075 Now we may interact this with given (F a ~ b) to get:
2077 But 'beta' is a touchable unification variable, and hence OK to
2078 unify it with 'b', replacing the derived evidence with the identity.
2080 This requires trySpontaneousSolve to solve *derived*
2081 equalities that have a touchable in their RHS, *in addition*
2082 to solving wanted equalities.
2084 Here is another example where this is useful.
2088 class (F a ~ b) => C a b
2089 And we are given the wanteds:
2093 We surely do *not* want to quantify over (b ~ c), since if someone provides
2094 dictionaries for (C a b) and (C a c), these dictionaries can provide a proof
2095 of (b ~ c), hence no extra evidence is necessary. Here is what will happen:
2097 Step 1: We will get new *given* superclass work,
2098 provisionally to our solving of w1 and w2
2100 g1: F a ~ b, g2 : F a ~ c,
2101 w1 : C a b, w2 : C a c, w3 : b ~ c
2103 The evidence for g1 and g2 is a superclass evidence term:
2105 g1 := sc w1, g2 := sc w2
2107 Step 2: The givens will solve the wanted w3, so that
2108 w3 := sym (sc w1) ; sc w2
2110 Step 3: Now, one may naively assume that then w2 can be solve from w1
2111 after rewriting with the (now solved equality) (b ~ c).
2113 But this rewriting is ruled out by the isGoodRectDict!
2115 Conclusion, we will (correctly) end up with the unsolved goals
2118 NB: The desugarer needs be more clever to deal with equalities
2119 that participate in recursive dictionary bindings.
2123 newGivenSCWork :: EvVar -> GivenLoc -> Class -> [Xi] -> TcS WorkList
2124 newGivenSCWork ev loc cls xis
2125 | NoScSkol <- ctLocOrigin loc -- Very important!
2126 = return emptyWorkList
2128 = newImmSCWorkFromFlavored ev (Given loc) cls xis >>= return
2130 newDerivedSCWork :: EvVar -> WantedLoc -> Class -> [Xi] -> TcS WorkList
2131 newDerivedSCWork ev loc cls xis
2132 = do { ims <- newImmSCWorkFromFlavored ev flavor cls xis
2135 rec_sc_work :: CanonicalCts -> TcS CanonicalCts
2137 = do { bg <- mapBagM (\c -> do { ims <- imm_sc_work c
2138 ; recs_ims <- rec_sc_work ims
2139 ; return $ consBag c recs_ims }) cts
2140 ; return $ concatBag bg }
2141 imm_sc_work (CDictCan { cc_id = dv, cc_flavor = fl, cc_class = cls, cc_tyargs = xis })
2142 = newImmSCWorkFromFlavored dv fl cls xis
2143 imm_sc_work _ct = return emptyCCan
2145 flavor = Derived loc DerSC
2147 newImmSCWorkFromFlavored :: EvVar -> CtFlavor -> Class -> [Xi] -> TcS WorkList
2148 -- Returns immediate superclasses
2149 newImmSCWorkFromFlavored ev flavor cls xis
2150 = do { let (tyvars, sc_theta, _, _) = classBigSig cls
2151 sc_theta1 = substTheta (zipTopTvSubst tyvars xis) sc_theta
2152 ; sc_vars <- zipWithM inst_one sc_theta1 [0..]
2153 ; mkCanonicals flavor sc_vars }
2155 inst_one pred n = newGivOrDerEvVar pred (EvSuperClass ev n)
2158 data LookupInstResult
2160 | GenInst [WantedEvVar] EvTerm
2162 matchClassInst :: Class -> [Type] -> WantedLoc -> TcS LookupInstResult
2163 matchClassInst clas tys loc
2164 = do { let pred = mkClassPred clas tys
2165 ; mb_result <- matchClass clas tys
2167 MatchInstNo -> return NoInstance
2168 MatchInstMany -> return NoInstance -- defer any reactions of a multitude until
2169 -- we learn more about the reagent
2170 MatchInstSingle (dfun_id, mb_inst_tys) ->
2171 do { checkWellStagedDFun pred dfun_id loc
2173 -- It's possible that not all the tyvars are in
2174 -- the substitution, tenv. For example:
2175 -- instance C X a => D X where ...
2176 -- (presumably there's a functional dependency in class C)
2177 -- Hence mb_inst_tys :: Either TyVar TcType
2179 ; tys <- instDFunTypes mb_inst_tys
2180 ; let (theta, _) = tcSplitPhiTy (applyTys (idType dfun_id) tys)
2181 ; if null theta then
2182 return (GenInst [] (EvDFunApp dfun_id tys []))
2184 { ev_vars <- instDFunConstraints theta
2185 ; let wevs = [WantedEvVar w loc | w <- ev_vars]
2186 ; return $ GenInst wevs (EvDFunApp dfun_id tys ev_vars) }