3 solveInteract, AtomicInert,
4 InertSet, emptyInert, extendInertSet, extractUnsolved, solveOne,
8 #include "HsVersions.h"
30 import Control.Monad ( when )
38 import qualified Bag as Bag
39 import qualified Data.Map as Map
42 import Control.Monad( zipWithM, unless )
43 import FastString ( sLit )
47 Note [InsertSet 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).
86 -- See Note [InertSet invariants]
88 = IS { inert_cts :: Bag.Bag CanonicalCt
89 , inert_fsks :: Map.Map TcTyVar [(TcTyVar,Coercion)] }
90 -- inert_fsks contains the *FlattenSkolem* equivalence classes.
91 -- inert_fsks extra invariants:
92 -- (a) all TcTyVars in the domain and range of inert_fsks are flatten skolems
93 -- (b) for every mapping tv1 |-> (tv2,co), co : tv2 ~ tv1
95 -- newtype InertSet = IS (Bag.Bag CanonicalCt)
96 instance Outputable InertSet where
97 ppr is = vcat [ vcat (map ppr (Bag.bagToList $ inert_cts is))
98 , vcat (map (\(v,rest) -> ppr v <+> text "|->" <+> hsep (map (ppr.fst) rest))
99 (Map.toList $ inert_fsks is)
105 emptyInert :: InertSet
106 emptyInert = IS { inert_cts = Bag.emptyBag, inert_fsks = Map.empty }
109 extendInertSet :: InertSet -> AtomicInert -> InertSet
110 -- Simply extend the bag of constraints rebuilding an inert set
111 extendInertSet (IS { inert_cts = cts
112 , inert_fsks = fsks }) item
113 = IS { inert_cts = cts `Bag.snocBag` item
114 , inert_fsks = fsks }
117 updInertSet :: InertSet -> AtomicInert -> InertSet
118 -- Introduces an element in the inert set for the first time
119 updInertSet (IS { inert_cts = cts, inert_fsks = fsks })
120 item@(CTyEqCan { cc_id = cv
123 | Just tv2 <- tcGetTyVar_maybe xi,
124 FlatSkol {} <- tcTyVarDetails tv1,
125 FlatSkol {} <- tcTyVarDetails tv2
126 = let cts' = cts `Bag.snocBag` item
127 fsks' = Map.insertWith (++) tv2 [(tv1, mkCoVarCoercion cv)] fsks
128 in IS { inert_cts = cts', inert_fsks = fsks' }
129 updInertSet (IS { inert_cts = cts
130 , inert_fsks = fsks }) item
131 = let cts' = cts `Bag.snocBag` item
132 in IS { inert_cts = cts', inert_fsks = fsks }
135 foldlInertSetM :: (Monad m) => (a -> AtomicInert -> m a) -> a -> InertSet -> m a
136 foldlInertSetM k z (IS { inert_cts = cts })
137 = Bag.foldlBagM k z cts
139 extractUnsolved :: InertSet -> (InertSet, CanonicalCts)
140 extractUnsolved is@(IS {inert_cts = cts})
141 = (is { inert_cts = cts'}, unsolved)
142 where (unsolved, cts') = Bag.partitionBag isWantedCt cts
145 getFskEqClass :: InertSet -> TcTyVar -> [(TcTyVar,Coercion)]
146 -- Precondition: tv is a FlatSkol
147 getFskEqClass (IS { inert_cts = cts, inert_fsks = fsks }) tv
148 = case lkpTyEqCanByLhs of
149 Nothing -> fromMaybe [] (Map.lookup tv fsks)
151 case tcGetTyVar_maybe (cc_rhs ceq) of
152 Just tv_rhs | FlatSkol {} <- tcTyVarDetails tv_rhs
153 -> let ceq_co = mkSymCoercion $ mkCoVarCoercion (cc_id ceq)
154 mk_co (v,c) = (v, mkTransCoercion c ceq_co)
155 in (tv_rhs, ceq_co): map mk_co (fromMaybe [] $ Map.lookup tv fsks)
157 where lkpTyEqCanByLhs = Bag.foldlBag lkp Nothing cts
158 lkp :: Maybe CanonicalCt -> CanonicalCt -> Maybe CanonicalCt
159 lkp Nothing ct@(CTyEqCan {cc_tyvar = tv'}) | tv' == tv = Just ct
160 lkp other _ct = other
163 isWantedCt :: CanonicalCt -> Bool
164 isWantedCt ct = isWanted (cc_flavor ct)
167 data Inert = IS { class_inerts :: FiniteMap Class Atomics
168 ip_inerts :: FiniteMap Class Atomics
169 tyfun_inerts :: FiniteMap TyCon Atomics
170 tyvar_inerts :: FiniteMap TyVar Atomics
173 Later should we also separate out givens and wanteds?
178 Note [Touchables and givens]
179 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
180 Touchable variables will never show up in givens which are inputs to
181 the solver. However, touchables may show up in givens generated by the flattener.
196 which can be put in the inert set. Suppose we also have a wanted
200 We cannot rewrite the given G alpha ~g b using the wanted alpha ~w
201 Int. Instead, after reacting alpha ~w Int with the whole inert set,
202 we observe that we can solve it by unifying alpha with Int, so we mark
203 it as solved and put it back in the *work list*. [We also immediately unify
204 alpha := Int, without telling anyone, see trySpontaneousSolve function, to
205 avoid doing this in the end.]
207 Later, because it is solved (given, in effect), we can use it to rewrite
208 G alpha ~g b to G Int ~g b, which gets put back in the work list. Eventually,
209 we will dispatch the remaining wanted constraints using the top-level axioms.
211 Finally, note that after reacting a wanted equality with the entire inert set
212 we may end up with something like
216 which we should flip around to generate the solved constraint alpha ~s b.
218 %*********************************************************************
220 * Main Interaction Solver *
222 **********************************************************************
226 1. Canonicalise (unary)
227 2. Pairwise interaction (binary)
228 * Take one from work list
229 * Try all pair-wise interactions with each constraint in inert
230 3. Try to solve spontaneously for equalities involving touchables
231 4. Top-level interaction (binary wrt top-level)
232 Superclass decomposition belongs in (4), see note [Superclasses]
236 type AtomicInert = CanonicalCt -- constraint pulled from InertSet
237 type WorkItem = CanonicalCt -- constraint pulled from WorkList
239 type WorkList = CanonicalCts -- A mixture of Given, Wanted, and Solved
240 type SWorkList = WorkList -- A worklist of solved
243 listToWorkList :: [WorkItem] -> WorkList
244 listToWorkList = Bag.listToBag
246 unionWorkLists :: WorkList -> WorkList -> WorkList
247 unionWorkLists = Bag.unionBags
249 foldlWorkListM :: (Monad m) => (a -> WorkItem -> m a) -> a -> WorkList -> m a
250 foldlWorkListM = Bag.foldlBagM
252 isEmptyWorkList :: WorkList -> Bool
253 isEmptyWorkList = Bag.isEmptyBag
255 emptyWorkList :: WorkList
256 emptyWorkList = Bag.emptyBag
258 singletonWorkList :: CanonicalCt -> WorkList
259 singletonWorkList ct = singleCCan ct
262 = Stop -- Work item is consumed
263 | ContinueWith WorkItem -- Not consumed
265 instance Outputable StopOrContinue where
266 ppr Stop = ptext (sLit "Stop")
267 ppr (ContinueWith w) = ptext (sLit "ContinueWith") <+> ppr w
269 -- Results after interacting a WorkItem as far as possible with an InertSet
271 = SR { sr_inerts :: InertSet
272 -- The new InertSet to use (REPLACES the old InertSet)
273 , sr_new_work :: WorkList
274 -- Any new work items generated (should be ADDED to the old WorkList)
276 -- sr_stop = Just workitem => workitem is *not* in sr_inerts and
277 -- workitem is inert wrt to sr_inerts
278 , sr_stop :: StopOrContinue
281 instance Outputable StageResult where
282 ppr (SR { sr_inerts = inerts, sr_new_work = work, sr_stop = stop })
283 = ptext (sLit "SR") <+>
284 braces (sep [ ptext (sLit "inerts =") <+> ppr inerts <> comma
285 , ptext (sLit "new work =") <+> ppr work <> comma
286 , ptext (sLit "stop =") <+> ppr stop])
288 type SimplifierStage = WorkItem -> InertSet -> TcS StageResult
290 -- Combine a sequence of simplifier 'stages' to create a pipeline
291 runSolverPipeline :: [(String, SimplifierStage)]
292 -> InertSet -> WorkItem
293 -> TcS (InertSet, WorkList)
294 -- Precondition: non-empty list of stages
295 runSolverPipeline pipeline inerts workItem
296 = do { traceTcS "Start solver pipeline" $
297 vcat [ ptext (sLit "work item =") <+> ppr workItem
298 , ptext (sLit "inerts =") <+> ppr inerts]
300 ; let itr_in = SR { sr_inerts = inerts
301 , sr_new_work = emptyWorkList
302 , sr_stop = ContinueWith workItem }
303 ; itr_out <- run_pipeline pipeline itr_in
305 = case sr_stop itr_out of
306 Stop -> sr_inerts itr_out
307 ContinueWith item -> sr_inerts itr_out `updInertSet` item
308 ; return (new_inert, sr_new_work itr_out) }
310 run_pipeline :: [(String, SimplifierStage)]
311 -> StageResult -> TcS StageResult
312 run_pipeline [] itr = return itr
313 run_pipeline _ itr@(SR { sr_stop = Stop }) = return itr
315 run_pipeline ((name,stage):stages)
316 (SR { sr_new_work = accum_work
318 , sr_stop = ContinueWith work_item })
319 = do { itr <- stage work_item inerts
320 ; traceTcS ("Stage result (" ++ name ++ ")") (ppr itr)
321 ; let itr' = itr { sr_new_work = sr_new_work itr
322 `unionWorkLists` accum_work }
323 ; run_pipeline stages itr' }
327 Inert: {c ~ d, F a ~ t, b ~ Int, a ~ ty} (all given)
328 Reagent: a ~ [b] (given)
330 React with (c~d) ==> IR (ContinueWith (a~[b])) True []
331 React with (F a ~ t) ==> IR (ContinueWith (a~[b])) False [F [b] ~ t]
332 React with (b ~ Int) ==> IR (ContinueWith (a~[Int]) True []
335 Inert: {c ~w d, F a ~g t, b ~w Int, a ~w ty}
338 React with (c ~w d) ==> IR (ContinueWith (a~[b])) True []
339 React with (F a ~g t) ==> IR (ContinueWith (a~[b])) True [] (can't rewrite given with wanted!)
343 Inert: {a ~ Int, F Int ~ b} (given)
344 Reagent: F a ~ b (wanted)
346 React with (a ~ Int) ==> IR (ContinueWith (F Int ~ b)) True []
347 React with (F Int ~ b) ==> IR Stop True [] -- after substituting we re-canonicalize and get nothing
350 -- Main interaction solver: we fully solve the worklist 'in one go',
351 -- returning an extended inert set.
353 -- See Note [Touchables and givens].
354 solveInteract :: InertSet -> WorkList -> TcS InertSet
355 solveInteract inert ws
356 = do { dyn_flags <- getDynFlags
357 ; solveInteractWithDepth (ctxtStkDepth dyn_flags,0,[]) inert ws
359 solveOne :: InertSet -> WorkItem -> TcS InertSet
360 solveOne inerts workItem
361 = do { dyn_flags <- getDynFlags
362 ; solveOneWithDepth (ctxtStkDepth dyn_flags,0,[]) inerts workItem
366 solveInteractWithDepth :: (Int, Int, [WorkItem])
367 -> InertSet -> WorkList -> TcS InertSet
368 solveInteractWithDepth ctxt@(max_depth,n,stack) inert ws
373 = solverDepthErrorTcS n stack
376 = do { traceTcS "solveInteractWithDepth" $
377 vcat [ text "Current depth =" <+> ppr n
378 , text "Max depth =" <+> ppr max_depth
380 ; foldlWorkListM (solveOneWithDepth ctxt) inert ws }
383 -- Fully interact the given work item with an inert set, and return a
384 -- new inert set which has assimilated the new information.
385 solveOneWithDepth :: (Int, Int, [WorkItem])
386 -> InertSet -> WorkItem -> TcS InertSet
387 solveOneWithDepth (max_depth, n, stack) inert work
388 = do { traceTcS0 (indent ++ "Solving {") (ppr work)
389 ; (new_inert, new_work) <- runSolverPipeline thePipeline inert work
391 ; traceTcS0 (indent ++ "Subgoals:") (ppr new_work)
393 -- Recursively solve the new work generated
394 -- from workItem, with a greater depth
395 ; res_inert <- solveInteractWithDepth (max_depth, n+1, work:stack)
398 ; traceTcS0 (indent ++ "Done }") (ppr work)
401 indent = replicate (2*n) ' '
403 thePipeline :: [(String,SimplifierStage)]
404 thePipeline = [ ("interact with inerts", interactWithInertsStage)
405 , ("spontaneous solve", spontaneousSolveStage)
406 , ("top-level reactions", topReactionsStage) ]
409 *********************************************************************************
411 The spontaneous-solve Stage
413 *********************************************************************************
416 spontaneousSolveStage :: SimplifierStage
417 spontaneousSolveStage workItem inerts
418 = do { mSolve <- trySpontaneousSolve workItem inerts
420 Nothing -> -- no spontaneous solution for him, keep going
421 return $ SR { sr_new_work = emptyWorkList
423 , sr_stop = ContinueWith workItem }
425 Just workList' -> -- He has been solved; workList' are all givens
426 return $ SR { sr_new_work = workList'
431 | isWantedCt workItem
432 -- Original was wanted we have now made him given so
433 -- we have to ineract him with the inerts again because
434 -- of the change in his status. This may produce some work.
435 -> do { traceTcS "recursive interact with inerts {" $ vcat
436 [ text "work = " <+> ppr workItem'
437 , text "inerts = " <+> ppr inerts ]
438 ; itr_again <- interactWithInertsStage workItem' inerts
439 ; case sr_stop itr_again of
440 Stop -> pprPanic "BUG: Impossible to happen" $
441 vcat [ text "Original workitem:" <+> ppr workItem
442 , text "Spontaneously solved:" <+> ppr workItem'
443 , text "Solved was consumed, when reacting with inerts:"
444 , nest 2 (ppr inerts) ]
445 ContinueWith workItem'' -- Now *this* guy is inert wrt to inerts
446 -> do { traceTcS "end recursive interact }" $ ppr workItem''
447 ; return $ SR { sr_new_work = sr_new_work itr_again
448 , sr_inerts = sr_inerts itr_again
449 `extendInertSet` workItem''
453 -> return $ SR { sr_new_work = emptyWorkList
454 , sr_inerts = inerts `extendInertSet` workItem'
458 -- @trySpontaneousSolve wi@ solves equalities where one side is a
459 -- touchable unification variable. Returns:
460 -- * Nothing if we were not able to solve it
461 -- * Just wi' if we solved it, wi' (now a "given") should be put in the work list.
462 -- See Note [Touchables and givens]
463 -- Note, just passing the inerts through for the skolem equivalence classes
464 trySpontaneousSolve :: WorkItem -> InertSet -> TcS (Maybe SWorkList)
465 trySpontaneousSolve (CTyEqCan { cc_id = cv, cc_flavor = gw, cc_tyvar = tv1, cc_rhs = xi }) inerts
466 | Just tv2 <- tcGetTyVar_maybe xi
467 = do { tch1 <- isTouchableMetaTyVar tv1
468 ; tch2 <- isTouchableMetaTyVar tv2
469 ; case (tch1, tch2) of
470 (True, True) -> trySpontaneousEqTwoWay inerts cv gw tv1 tv2
471 (True, False) -> trySpontaneousEqOneWay inerts cv gw tv1 xi
472 (False, True) | tyVarKind tv1 `isSubKind` tyVarKind tv2
473 -> trySpontaneousEqOneWay inerts cv gw tv2 (mkTyVarTy tv1)
474 _ -> return Nothing }
476 = do { tch1 <- isTouchableMetaTyVar tv1
477 ; if tch1 then trySpontaneousEqOneWay inerts cv gw tv1 xi
478 else return Nothing }
481 -- trySpontaneousSolve (CFunEqCan ...) = ...
482 -- See Note [No touchables as FunEq RHS] in TcSMonad
483 trySpontaneousSolve _ _ = return Nothing
486 trySpontaneousEqOneWay :: InertSet -> CoVar -> CtFlavor -> TcTyVar -> Xi
487 -> TcS (Maybe SWorkList)
488 -- tv is a MetaTyVar, not untouchable
489 -- Precondition: kind(xi) is a sub-kind of kind(tv)
490 trySpontaneousEqOneWay inerts cv gw tv xi
491 | not (isSigTyVar tv) || isTyVarTy xi
492 = solveWithIdentity inerts cv gw tv xi
497 trySpontaneousEqTwoWay :: InertSet -> CoVar -> CtFlavor -> TcTyVar -> TcTyVar
498 -> TcS (Maybe SWorkList)
499 -- Both tyvars are *touchable* MetaTyvars
500 -- By the CTyEqCan invariant, k2 `isSubKind` k1
501 trySpontaneousEqTwoWay inerts cv gw tv1 tv2
503 , nicer_to_update_tv2 = solveWithIdentity inerts cv gw tv2 (mkTyVarTy tv1)
504 | otherwise = ASSERT( k2 `isSubKind` k1 )
505 solveWithIdentity inerts cv gw tv1 (mkTyVarTy tv2)
509 nicer_to_update_tv2 = isSigTyVar tv1 || isSystemName (Var.varName tv2)
512 Note [Loopy spontaneous solving]
513 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
514 Consider the original wanted:
515 wanted : Maybe (E alpha) ~ alpha
516 where E is a type family, such that E (T x) = x. After canonicalization,
517 as a result of flattening, we will get:
518 given : E alpha ~ fsk
519 wanted : alpha ~ Maybe fsk
520 where (fsk := E alpha, on the side). Now, if we spontaneously *solve*
521 (alpha := Maybe fsk) we are in trouble! Instead, we should refrain from solving
522 it and keep it as wanted. In inference mode we'll end up quantifying over
523 (alpha ~ Maybe (E alpha))
524 Hence, 'solveWithIdentity' performs a small occurs check before
525 actually solving. But this occurs check *must look through* flatten
528 Note [Avoid double unifications]
529 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
530 The spontaneous solver has to return a given which mentions the unified unification
531 variable *on the left* of the equality. Here is what happens if not:
532 Original wanted: (a ~ alpha), (alpha ~ Int)
533 We spontaneously solve the first wanted, without changing the order!
534 given : a ~ alpha [having unifice alpha := a]
535 Now the second wanted comes along, but he cannot rewrite the given, so we simply continue.
536 At the end we spontaneously solve that guy, *reunifying* [alpha := Int]
538 We avoid this problem by orienting the given so that the unification variable is on the left.
539 [Note that alternatively we could attempt to enforce this at canonicalization]
541 Avoiding double unifications is yet another reason to disallow touchable unification variables
542 as RHS of type family equations: F xis ~ alpha. Consider having already spontaneously solved
543 a wanted (alpha ~ [b]) by setting alpha := [b]. So the inert set looks like:
545 And now a new wanted (F tau ~ alpha) comes along. Since it does not react with anything
546 we will be left with a constraint (F tau ~ alpha) that must cause a unification of
547 (alpha := F tau) at some point (either in spontaneous solving, or at the end). But alpha
548 is *already* unified so we must not do anything to it. By disallowing naked touchables in
549 the RHS of constraints (in favor of introduced flatten skolems) we do not have to worry at
550 all about unifying or spontaneously solving (F xis ~ alpha) by unification.
554 solveWithIdentity :: InertSet
555 -> CoVar -> CtFlavor -> TcTyVar -> Xi
556 -> TcS (Maybe SWorkList)
557 -- Solve with the identity coercion
558 -- Precondition: kind(xi) is a sub-kind of kind(tv)
559 -- See [New Wanted Superclass Work] to see why we do this for *given* as well
560 solveWithIdentity inerts cv gw tv xi
562 = do { m <- passOccursCheck inerts tv xi
564 Nothing -> return Nothing
565 Just (xi_unflat,coi) -- coi : xi_unflat ~ xi
566 -> do { traceTcS "Sneaky unification:" $
567 vcat [text "Coercion variable: " <+> ppr gw,
568 text "Coercion: " <+> pprEq (mkTyVarTy tv) xi,
569 text "Left Kind is : " <+> ppr (typeKind (mkTyVarTy tv)),
570 text "Right Kind is : " <+> ppr (typeKind xi)
572 ; setWantedTyBind tv xi_unflat -- Set tv := xi_unflat
573 ; cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi_unflat xi_unflat
574 ; let flav = mkGivenFlavor gw UnkSkol
575 ; (cts, co) <- case coi of
576 ACo co -> do { can_eqs <- canEq flav cv_given (mkTyVarTy tv) xi_unflat
577 ; return (can_eqs, co) }
579 (singleCCan (CTyEqCan { cc_id = cv_given
580 , cc_flavor = mkGivenFlavor gw UnkSkol
581 , cc_tyvar = tv, cc_rhs = xi }
582 -- xi, *not* xi_unflat!
585 Wanted {} -> setWantedCoBind cv co
586 Derived {} -> setDerivedCoBind cv co
587 _ -> pprPanic "Can't spontaneously solve *given*" empty
589 -- See Note [Avoid double unifications]
591 -- The reason that we create a new given variable (cv_given) instead of reusing cv
592 -- is because we do not want to end up with coercion unification variables in the givens.
593 ; return (Just cts) }
599 passOccursCheck :: InertSet -> TcTyVar -> TcType -> TcS (Maybe (TcType,CoercionI))
600 -- passOccursCheck inerts tv ty
601 -- Traverse the type and make sure that 'tv' does not appear under
602 -- some flatten skolem. If it appears under some flatten skolem
603 -- look in that flatten skolem equivalence class to see if you can
604 -- find a different flatten skolem to use, which does not mention the
606 -- Postcondition: Just (ty',coi) <- passOccursCheck tv ty
608 -- NB: I believe there is no need to do the tcView thing here
609 passOccursCheck is tv (TyConApp tc tys)
610 = do { tys_mbs <- mapM (passOccursCheck is tv) tys
611 ; case allMaybes tys_mbs of
612 Nothing -> return Nothing
614 let (tys',cois') = unzip tys_cois
616 Just (TyConApp tc tys', mkTyConAppCoI tc cois')
618 passOccursCheck is tv (PredTy sty)
619 = do { sty_mb <- passOccursCheckPred tv sty
621 Nothing -> return Nothing
622 Just (sty',coi) -> return (Just (PredTy sty', coi))
624 where passOccursCheckPred tv (ClassP cn tys)
625 = do { tys_mbs <- mapM (passOccursCheck is tv) tys
626 ; case allMaybes tys_mbs of
627 Nothing -> return Nothing
629 let (tys', cois') = unzip tys_cois
631 Just (ClassP cn tys', mkClassPPredCoI cn cois')
633 passOccursCheckPred tv (IParam nm ty)
634 = do { mty <- passOccursCheck is tv ty
636 Nothing -> return Nothing
638 -> return (Just (IParam nm ty',
639 mkIParamPredCoI nm co'))
641 passOccursCheckPred tv (EqPred ty1 ty2)
642 = do { mty1 <- passOccursCheck is tv ty1
643 ; mty2 <- passOccursCheck is tv ty2
644 ; case (mty1,mty2) of
645 (Just (ty1',coi1), Just (ty2',coi2))
647 Just (EqPred ty1' ty2', mkEqPredCoI coi1 coi2)
651 passOccursCheck is tv (FunTy arg res)
652 = do { arg_mb <- passOccursCheck is tv arg
653 ; res_mb <- passOccursCheck is tv res
654 ; case (arg_mb,res_mb) of
655 (Just (arg',coiarg), Just (res',coires))
657 Just (FunTy arg' res', mkFunTyCoI coiarg coires)
661 passOccursCheck is tv (AppTy fun arg)
662 = do { fun_mb <- passOccursCheck is tv fun
663 ; arg_mb <- passOccursCheck is tv arg
664 ; case (fun_mb,arg_mb) of
665 (Just (fun',coifun), Just (arg',coiarg))
667 Just (AppTy fun' arg', mkAppTyCoI coifun coiarg)
671 passOccursCheck is tv (ForAllTy tv1 ty1)
672 = do { ty1_mb <- passOccursCheck is tv ty1
674 Nothing -> return Nothing
677 Just (ForAllTy tv1 ty1', mkForAllTyCoI tv1 coi)
680 passOccursCheck _is tv (TyVarTy tv')
684 passOccursCheck is tv (TyVarTy fsk)
685 | FlatSkol ty <- tcTyVarDetails fsk
686 = do { zty <- zonkFlattenedType ty -- Must zonk as it contains unif. vars
687 ; occ <- passOccursCheck is tv zty
689 Nothing -> go_down_eq_class $ getFskEqClass is fsk
690 Just (zty',ico) -> return $ Just (zty',ico)
692 where go_down_eq_class [] = return Nothing
693 go_down_eq_class ((fsk1,co1):rest)
694 = do { occ1 <- passOccursCheck is tv (TyVarTy fsk1)
696 Nothing -> go_down_eq_class rest
698 -> return $ Just (ty1, mkTransCoI co1i' (ACo co1)) }
699 passOccursCheck _is _tv ty
700 = return (Just (ty,IdCo ty))
703 Problematic situation:
704 ~~~~~~~~~~~~~~~~~~~~~~
705 Suppose we have a flatten skolem f1 := F f6
706 Suppose we are chasing for 'alpha', and:
707 f6 := G alpha with eq.class f7,f8
709 Then we will return F f7 potentially.
717 *********************************************************************************
719 The interact-with-inert Stage
721 *********************************************************************************
724 -- Interaction result of WorkItem <~> AtomicInert
726 = IR { ir_stop :: StopOrContinue
728 -- => Reagent (work item) consumed.
729 -- ContinueWith new_reagent
730 -- => Reagent transformed but keep gathering interactions.
731 -- The transformed item remains inert with respect
732 -- to any previously encountered inerts.
734 , ir_inert_action :: InertAction
735 -- Whether the inert item should remain in the InertSet.
737 , ir_new_work :: WorkList
738 -- new work items to add to the WorkList
741 -- What to do with the inert reactant.
742 data InertAction = KeepInert | DropInert
745 mkIRContinue :: Monad m => WorkItem -> InertAction -> WorkList -> m InteractResult
746 mkIRContinue wi keep newWork = return $ IR (ContinueWith wi) keep newWork
748 mkIRStop :: Monad m => InertAction -> WorkList -> m InteractResult
749 mkIRStop keep newWork = return $ IR Stop keep newWork
751 dischargeWorkItem :: Monad m => m InteractResult
752 dischargeWorkItem = mkIRStop KeepInert emptyCCan
754 noInteraction :: Monad m => WorkItem -> m InteractResult
755 noInteraction workItem = mkIRContinue workItem KeepInert emptyCCan
757 data WhichComesFromInert = LeftComesFromInert | RightComesFromInert
759 ---------------------------------------------------
760 -- Interact a single WorkItem with an InertSet as far as possible, i.e. until we get a Stop
761 -- result from an individual interaction (i.e. when the WorkItem is consumed), or until we've
762 -- interacted the WorkItem with the entire InertSet.
764 -- Postcondition: the new InertSet in the resulting StageResult is subset
765 -- of the input InertSet.
767 interactWithInertsStage :: SimplifierStage
768 interactWithInertsStage workItem inert
769 = foldlInertSetM interactNext initITR inert
771 initITR = SR { sr_inerts = emptyInert
772 , sr_new_work = emptyCCan
773 , sr_stop = ContinueWith workItem }
776 interactNext :: StageResult -> AtomicInert -> TcS StageResult
777 interactNext it inert
778 | ContinueWith workItem <- sr_stop it
779 = do { ir <- interactWithInert inert workItem
780 ; let inerts = sr_inerts it
781 ; return $ SR { sr_inerts = if ir_inert_action ir == KeepInert
782 then inerts `updInertSet` inert
784 , sr_new_work = sr_new_work it `unionWorkLists` ir_new_work ir
785 , sr_stop = ir_stop ir } }
786 | otherwise = return $ itrAddInert inert it
789 itrAddInert :: AtomicInert -> StageResult -> StageResult
790 itrAddInert inert itr = itr { sr_inerts = (sr_inerts itr) `updInertSet` inert }
792 -- Do a single interaction of two constraints.
793 interactWithInert :: AtomicInert -> WorkItem -> TcS InteractResult
794 interactWithInert inert workitem
795 = do { ctxt <- getTcSContext
796 ; let is_allowed = allowedInteraction (simplEqsOnly ctxt) inert workitem
797 inert_ev = cc_id inert
798 work_ev = cc_id workitem
800 -- Never interact a wanted and a derived where the derived's evidence
801 -- mentions the wanted evidence in an unguarded way.
802 -- See Note [Superclasses and recursive dictionaries]
803 -- and Note [New Wanted Superclass Work]
804 -- We don't have to do this for givens, as we fully know the evidence for them.
806 case (cc_flavor inert, cc_flavor workitem) of
807 (Wanted loc, Derived _) -> isGoodRecEv work_ev (WantedEvVar inert_ev loc)
808 (Derived _, Wanted loc) -> isGoodRecEv inert_ev (WantedEvVar work_ev loc)
811 ; if is_allowed && rec_ev_ok then
812 doInteractWithInert inert workitem
814 noInteraction workitem
817 allowedInteraction :: Bool -> AtomicInert -> WorkItem -> Bool
818 -- Allowed interactions
819 allowedInteraction eqs_only (CDictCan {}) (CDictCan {}) = not eqs_only
820 allowedInteraction eqs_only (CIPCan {}) (CIPCan {}) = not eqs_only
821 allowedInteraction _ _ _ = True
823 --------------------------------------------
824 doInteractWithInert :: CanonicalCt -> CanonicalCt -> TcS InteractResult
825 -- Identical class constraints.
828 (CDictCan { cc_id = d1, cc_flavor = fl1, cc_class = cls1, cc_tyargs = tys1 })
829 workItem@(CDictCan { cc_id = d2, cc_flavor = fl2, cc_class = cls2, cc_tyargs = tys2 })
830 | cls1 == cls2 && (and $ zipWith tcEqType tys1 tys2)
831 = solveOneFromTheOther (d1,fl1) workItem
833 | cls1 == cls2 && (not (isGiven fl1 && isGiven fl2))
834 = -- See Note [When improvement happens]
835 do { let work_item_pred_loc = (ClassP cls2 tys2, ppr d2)
836 inert_pred_loc = (ClassP cls1 tys1, ppr d1)
837 loc = combineCtLoc fl1 fl2
838 eqn_pred_locs = improveFromAnother work_item_pred_loc inert_pred_loc
839 ; wevvars <- mkWantedFunDepEqns loc eqn_pred_locs
840 -- See Note [Generating extra equalities]
841 ; workList <- canWanteds wevvars
842 ; mkIRContinue workItem KeepInert workList -- Keep the inert there so we avoid
843 -- re-introducing the fundep equalities
844 -- See Note [FunDep Reactions]
847 -- Class constraint and given equality: use the equality to rewrite
848 -- the class constraint.
849 doInteractWithInert (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi })
850 (CDictCan { cc_id = dv, cc_flavor = wfl, cc_class = cl, cc_tyargs = xis })
851 | ifl `canRewrite` wfl
852 , tv `elemVarSet` tyVarsOfTypes xis
853 -- substitute for tv in xis. Note that the resulting class
854 -- constraint is still canonical, since substituting xi-types in
855 -- xi-types generates xi-types. However, it may no longer be
856 -- inert with respect to the inert set items we've already seen.
857 -- For example, consider the inert set
862 -- and the work item D a (w). D a does not interact with D Int.
863 -- Next, it does interact with a ~g Int, getting rewritten to D
864 -- Int (w). But now we must go back through the rest of the inert
865 -- set again, to find that it can now be discharged by the given D
867 = do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,wfl,cl,xis)
868 ; mkIRStop KeepInert (singleCCan rewritten_dict) }
870 doInteractWithInert (CDictCan { cc_id = dv, cc_flavor = ifl, cc_class = cl, cc_tyargs = xis })
871 workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
872 | wfl `canRewrite` ifl
873 , tv `elemVarSet` tyVarsOfTypes xis
874 = do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,ifl,cl,xis)
875 ; mkIRContinue workItem DropInert (singleCCan rewritten_dict) }
877 -- Class constraint and given equality: use the equality to rewrite
878 -- the class constraint.
879 doInteractWithInert (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi })
880 (CIPCan { cc_id = ipid, cc_flavor = wfl, cc_ip_nm = nm, cc_ip_ty = ty })
881 | ifl `canRewrite` wfl
882 , tv `elemVarSet` tyVarsOfType ty
883 = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,wfl,nm,ty)
884 ; mkIRStop KeepInert (singleCCan rewritten_ip) }
886 doInteractWithInert (CIPCan { cc_id = ipid, cc_flavor = ifl, cc_ip_nm = nm, cc_ip_ty = ty })
887 workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
888 | wfl `canRewrite` ifl
889 , tv `elemVarSet` tyVarsOfType ty
890 = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,ifl,nm,ty)
891 ; mkIRContinue workItem DropInert (singleCCan rewritten_ip) }
893 -- Two implicit parameter constraints. If the names are the same,
894 -- but their types are not, we generate a wanted type equality
895 -- that equates the type (this is "improvement").
896 -- However, we don't actually need the coercion evidence,
897 -- so we just generate a fresh coercion variable that isn't used anywhere.
898 doInteractWithInert (CIPCan { cc_id = id1, cc_flavor = ifl, cc_ip_nm = nm1, cc_ip_ty = ty1 })
899 workItem@(CIPCan { cc_flavor = wfl, cc_ip_nm = nm2, cc_ip_ty = ty2 })
900 | nm1 == nm2 && isGiven wfl && isGiven ifl
901 = -- See Note [Overriding implicit parameters]
902 -- Dump the inert item, override totally with the new one
903 -- Do not require type equality
904 mkIRContinue workItem DropInert emptyCCan
906 | nm1 == nm2 && ty1 `tcEqType` ty2
907 = solveOneFromTheOther (id1,ifl) workItem
910 = -- See Note [When improvement happens]
911 do { co_var <- newWantedCoVar ty1 ty2
912 ; let flav = Wanted (combineCtLoc ifl wfl)
913 ; mkCanonical flav co_var >>= mkIRContinue workItem KeepInert }
916 -- Inert: equality, work item: function equality
918 -- Never rewrite a given with a wanted equality, and a type function
919 -- equality can never rewrite an equality. Note also that if we have
920 -- F x1 ~ x2 and a ~ x3, and a occurs in x2, we don't rewrite it. We
921 -- can wait until F x1 ~ x2 matches another F x1 ~ x4, and only then
922 -- we will ``expose'' x2 and x4 to rewriting.
924 -- Otherwise, we can try rewriting the type function equality with the equality.
925 doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi1 })
926 (CFunEqCan { cc_id = cv2, cc_flavor = wfl, cc_fun = tc
927 , cc_tyargs = args, cc_rhs = xi2 })
928 | ifl `canRewrite` wfl
929 , tv `elemVarSet` tyVarsOfTypes args
930 = do { rewritten_funeq <- rewriteFunEq (cv1,tv,xi1) (cv2,wfl,tc,args,xi2)
931 ; mkIRStop KeepInert (singleCCan rewritten_funeq) }
933 -- Inert: function equality, work item: equality
935 doInteractWithInert (CFunEqCan {cc_id = cv1, cc_flavor = ifl, cc_fun = tc
936 , cc_tyargs = args, cc_rhs = xi1 })
937 workItem@(CTyEqCan { cc_id = cv2, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi2 })
938 | wfl `canRewrite` ifl
939 , tv `elemVarSet` tyVarsOfTypes args
940 = do { rewritten_funeq <- rewriteFunEq (cv2,tv,xi2) (cv1,ifl,tc,args,xi1)
941 ; mkIRContinue workItem DropInert (singleCCan rewritten_funeq) }
943 doInteractWithInert (CFunEqCan { cc_id = cv1, cc_flavor = fl1, cc_fun = tc1
944 , cc_tyargs = args1, cc_rhs = xi1 })
945 workItem@(CFunEqCan { cc_id = cv2, cc_flavor = fl2, cc_fun = tc2
946 , cc_tyargs = args2, cc_rhs = xi2 })
947 | fl1 `canRewrite` fl2 && lhss_match
948 = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
949 ; mkIRStop KeepInert cans }
950 | fl2 `canRewrite` fl1 && lhss_match
951 = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
952 ; mkIRContinue workItem DropInert cans }
954 lhss_match = tc1 == tc2 && and (zipWith tcEqType args1 args2)
957 inert@(CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
958 workItem@(CTyEqCan { cc_id = cv2, cc_flavor = fl2, cc_tyvar = tv2, cc_rhs = xi2 })
959 -- Check for matching LHS
960 | fl1 `canRewrite` fl2 && tv1 == tv2
961 = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
962 ; mkIRStop KeepInert cans }
964 | fl2 `canRewrite` fl1 && tv1 == tv2
965 = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
966 ; mkIRContinue workItem DropInert cans }
968 -- Check for rewriting RHS
969 | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfType xi2
970 = do { rewritten_eq <- rewriteEqRHS (cv1,tv1,xi1) (cv2,fl2,tv2,xi2)
971 ; mkIRStop KeepInert rewritten_eq }
972 | fl2 `canRewrite` fl1 && tv2 `elemVarSet` tyVarsOfType xi1
973 = do { rewritten_eq <- rewriteEqRHS (cv2,tv2,xi2) (cv1,fl1,tv1,xi1)
974 ; mkIRContinue workItem DropInert rewritten_eq }
975 -- Finally, if workitem is a flatten equivalence class constraint and the
976 -- inert is a wanted constraints, even when the workitem cannot rewrite the
977 -- inert, drop the inert out because you may have to reconsider solving him
978 -- using the equivalence class you created.
980 | not $ isGiven fl1, -- The inert is wanted or derived
981 isMetaTyVar tv1, -- and has a unification variable lhs
982 FlatSkol {} <- tcTyVarDetails tv2, -- And workitem is a flatten skolem equality
983 Just tv2' <- tcGetTyVar_maybe xi2, FlatSkol {} <- tcTyVarDetails tv2'
984 = mkIRContinue workItem DropInert (singletonWorkList inert)
987 -- Fall-through case for all other cases
988 doInteractWithInert _ workItem = noInteraction workItem
990 --------------------------------------------
991 combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
992 -- Precondition: At least one of them should be wanted
993 combineCtLoc (Wanted loc) _ = loc
994 combineCtLoc _ (Wanted loc) = loc
995 combineCtLoc _ _ = panic "Expected one of wanted constraints (BUG)"
998 -- Equational Rewriting
999 rewriteDict :: (CoVar, TcTyVar, Xi) -> (DictId, CtFlavor, Class, [Xi]) -> TcS CanonicalCt
1000 rewriteDict (cv,tv,xi) (dv,gw,cl,xis)
1001 = do { let cos = substTysWith [tv] [mkCoVarCoercion cv] xis -- xis[tv] ~ xis[xi]
1002 args = substTysWith [tv] [xi] xis
1004 dict_co = mkTyConCoercion con cos
1005 ; dv' <- newDictVar cl args
1007 Wanted {} -> setDictBind dv (EvCast dv' (mkSymCoercion dict_co))
1008 _given_or_derived -> setDictBind dv' (EvCast dv dict_co)
1009 ; return (CDictCan { cc_id = dv'
1012 , cc_tyargs = args }) }
1014 rewriteIP :: (CoVar,TcTyVar,Xi) -> (EvVar,CtFlavor, IPName Name, TcType) -> TcS CanonicalCt
1015 rewriteIP (cv,tv,xi) (ipid,gw,nm,ty)
1016 = do { let ip_co = substTyWith [tv] [mkCoVarCoercion cv] ty -- ty[tv] ~ t[xi]
1017 ty' = substTyWith [tv] [xi] ty
1018 ; ipid' <- newIPVar nm ty'
1020 Wanted {} -> setIPBind ipid (EvCast ipid' (mkSymCoercion ip_co))
1021 _given_or_derived -> setIPBind ipid' (EvCast ipid ip_co)
1022 ; return (CIPCan { cc_id = ipid'
1025 , cc_ip_ty = ty' }) }
1027 rewriteFunEq :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TyCon, [Xi], Xi) -> TcS CanonicalCt
1028 rewriteFunEq (cv1,tv,xi1) (cv2,gw, tc,args,xi2)
1029 = do { let arg_cos = substTysWith [tv] [mkCoVarCoercion cv1] args
1030 args' = substTysWith [tv] [xi1] args
1031 fun_co = mkTyConCoercion tc arg_cos
1032 ; cv2' <- case gw of
1033 Wanted {} -> do { cv2' <- newWantedCoVar (mkTyConApp tc args') xi2
1034 ; setWantedCoBind cv2 $
1035 mkTransCoercion fun_co (mkCoVarCoercion cv2')
1037 _giv_or_der -> newGivOrDerCoVar (mkTyConApp tc args') xi2 $
1038 mkTransCoercion (mkSymCoercion fun_co) (mkCoVarCoercion cv2)
1039 ; return (CFunEqCan { cc_id = cv2'
1046 rewriteEqRHS :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TcTyVar,Xi) -> TcS CanonicalCts
1047 -- Use the first equality to rewrite the second, flavors already checked.
1048 -- E.g. c1 : tv1 ~ xi1 c2 : tv2 ~ xi2
1049 -- rewrites c2 to give
1050 -- c2' : tv2 ~ xi2[xi1/tv1]
1051 -- We must do an occurs check to sure the new constraint is canonical
1052 -- So we might return an empty bag
1053 rewriteEqRHS (cv1,tv1,xi1) (cv2,gw,tv2,xi2)
1054 | Just tv2' <- tcGetTyVar_maybe xi2'
1055 , tv2 == tv2' -- In this case xi2[xi1/tv1] = tv2, so we have tv2~tv2
1056 = do { when (isWanted gw) (setWantedCoBind cv2 (mkSymCoercion co2'))
1057 ; return emptyCCan }
1062 -> do { cv2' <- newWantedCoVar (mkTyVarTy tv2) xi2'
1063 ; setWantedCoBind cv2 $
1064 mkCoVarCoercion cv2' `mkTransCoercion` mkSymCoercion co2'
1067 -> newGivOrDerCoVar (mkTyVarTy tv2) xi2' $
1068 mkCoVarCoercion cv2 `mkTransCoercion` co2'
1070 ; xi2'' <- canOccursCheck gw tv2 xi2' -- we know xi2' is *not* tv2
1071 ; return (singleCCan $ CTyEqCan { cc_id = cv2'
1077 xi2' = substTyWith [tv1] [xi1] xi2
1078 co2' = substTyWith [tv1] [mkCoVarCoercion cv1] xi2 -- xi2 ~ xi2[xi1/tv1]
1081 rewriteEqLHS :: WhichComesFromInert -> (Coercion,Xi) -> (CoVar,CtFlavor,Xi) -> TcS CanonicalCts
1082 -- Used to ineratct two equalities of the following form:
1083 -- First Equality: co1: (XXX ~ xi1)
1084 -- Second Equality: cv2: (XXX ~ xi2)
1085 -- Where the cv1 `canRewrite` cv2 equality
1086 -- We have an option of creating new work (xi1 ~ xi2) OR (xi2 ~ xi1). This
1087 -- depends on whether the left or the right equality comes from the inert set.
1089 -- prefer to create (xi2 ~ xi1) if the first comes from the inert
1090 -- prefer to create (xi1 ~ xi2) if the second comes from the inert
1091 rewriteEqLHS which (co1,xi1) (cv2,gw,xi2)
1092 = do { cv2' <- case (isWanted gw, which) of
1093 (True,LeftComesFromInert) ->
1094 do { cv2' <- newWantedCoVar xi2 xi1
1095 ; setWantedCoBind cv2 $
1096 co1 `mkTransCoercion` mkSymCoercion (mkCoVarCoercion cv2')
1098 (True,RightComesFromInert) ->
1099 do { cv2' <- newWantedCoVar xi1 xi2
1100 ; setWantedCoBind cv2 $
1101 co1 `mkTransCoercion` mkCoVarCoercion cv2'
1103 (False,LeftComesFromInert) ->
1104 newGivOrDerCoVar xi2 xi1 $
1105 mkSymCoercion (mkCoVarCoercion cv2) `mkTransCoercion` co1
1106 (False,RightComesFromInert) ->
1107 newGivOrDerCoVar xi1 xi2 $
1108 mkSymCoercion co1 `mkTransCoercion` mkCoVarCoercion cv2
1109 ; mkCanonical gw cv2' }
1112 -- if isWanted gw then
1113 -- do { cv2' <- newWantedCoVar xi1 xi2
1114 -- ; setWantedCoBind cv2 $
1115 -- co1 `mkTransCoercion` mkCoVarCoercion cv2'
1117 -- else newGivOrDerCoVar xi1 xi2 $
1118 -- mkSymCoercion co1 `mkTransCoercion` mkCoVarCoercion cv2
1119 -- ; mkCanonical gw cv2' }
1122 solveOneFromTheOther :: (EvVar, CtFlavor) -> CanonicalCt -> TcS InteractResult
1123 -- First argument inert, second argument workitem. They both represent
1124 -- wanted/given/derived evidence for the *same* predicate so we try here to
1125 -- discharge one directly from the other.
1127 -- Precondition: value evidence only (implicit parameters, classes)
1129 solveOneFromTheOther (iid,ifl) workItem
1130 -- Both derived needs a special case. You might think that we do not need
1131 -- two evidence terms for the same claim. But, since the evidence is partial,
1132 -- either evidence may do in some cases; see TcSMonad.isGoodRecEv.
1133 -- See also Example 3 in Note [Superclasses and recursive dictionaries]
1134 | isDerived ifl && isDerived wfl
1135 = noInteraction workItem
1137 | ifl `canRewrite` wfl
1138 = do { unless (isGiven wfl) $ setEvBind wid (EvId iid)
1139 -- Overwrite the binding, if one exists
1140 -- For Givens, which are lambda-bound, nothing to overwrite,
1141 ; dischargeWorkItem }
1143 | otherwise -- wfl `canRewrite` ifl
1144 = do { unless (isGiven ifl) $ setEvBind iid (EvId wid)
1145 ; mkIRContinue workItem DropInert emptyCCan }
1148 wfl = cc_flavor workItem
1149 wid = cc_id workItem
1152 Note [Superclasses and recursive dictionaries]
1153 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1154 Overlaps with Note [SUPERCLASS-LOOP 1]
1155 Note [SUPERCLASS-LOOP 2]
1156 Note [Recursive instances and superclases]
1157 ToDo: check overlap and delete redundant stuff
1159 Right before adding a given into the inert set, we must
1160 produce some more work, that will bring the superclasses
1161 of the given into scope. The superclass constraints go into
1164 When we simplify a wanted constraint, if we first see a matching
1165 instance, we may produce new wanted work. To (1) avoid doing this work
1166 twice in the future and (2) to handle recursive dictionaries we may ``cache''
1167 this item as solved (in effect, given) into our inert set and with that add
1168 its superclass constraints (as given) in our worklist.
1170 But now we have added partially solved constraints to the worklist which may
1171 interact with other wanteds. Consider the example:
1175 class Eq b => Foo a b --- 0-th selector
1176 instance Eq a => Foo [a] a --- fooDFun
1178 and wanted (Foo [t] t). We are first going to see that the instance matches
1179 and create an inert set that includes the solved (Foo [t] t) and its
1181 d1 :_g Foo [t] t d1 := EvDFunApp fooDFun d3
1182 d2 :_g Eq t d2 := EvSuperClass d1 0
1183 Our work list is going to contain a new *wanted* goal
1185 It is wrong to react the wanted (Eq t) with the given (Eq t) because that would
1186 construct loopy evidence. Hence the check isGoodRecEv in doInteractWithInert.
1188 OK, so we have ruled out bad behaviour, but how do we ge recursive dictionaries,
1193 data D r = ZeroD | SuccD (r (D r));
1195 instance (Eq (r (D r))) => Eq (D r) where
1196 ZeroD == ZeroD = True
1197 (SuccD a) == (SuccD b) = a == b
1200 equalDC :: D [] -> D [] -> Bool;
1203 We need to prove (Eq (D [])). Here's how we go:
1207 by instance decl, holds if
1211 *BUT* we have an inert set which gives us (no superclasses):
1213 By the instance declaration of Eq we can show the 'd2' goal if
1215 where d2 = dfEqList d3
1217 Now, however this wanted can interact with our inert d1 to set:
1219 and solve the goal. Why was this interaction OK? Because, if we chase the
1220 evidence of d1 ~~> dfEqD d2 ~~-> dfEqList d3, so by setting d3 := d1 we
1222 d3 := dfEqD2 (dfEqList d3)
1223 which is FINE because the use of d3 is protected by the instance function
1226 So, our strategy is to try to put solved wanted dictionaries into the
1227 inert set along with their superclasses (when this is meaningful,
1228 i.e. when new wanted goals are generated) but solve a wanted dictionary
1229 from a given only in the case where the evidence variable of the
1230 wanted is mentioned in the evidence of the given (recursively through
1231 the evidence binds) in a protected way: more instance function applications
1232 than superclass selectors.
1234 Here are some more examples from GHC's previous type checker
1238 This code arises in the context of "Scrap Your Boilerplate with Class"
1242 instance Sat (ctx Char) => Data ctx Char -- dfunData1
1243 instance (Sat (ctx [a]), Data ctx a) => Data ctx [a] -- dfunData2
1245 class Data Maybe a => Foo a
1247 instance Foo t => Sat (Maybe t) -- dfunSat
1249 instance Data Maybe a => Foo a -- dfunFoo1
1250 instance Foo a => Foo [a] -- dfunFoo2
1251 instance Foo [Char] -- dfunFoo3
1253 Consider generating the superclasses of the instance declaration
1254 instance Foo a => Foo [a]
1256 So our problem is this
1258 d1 :_w Data Maybe [t]
1260 We may add the given in the inert set, along with its superclasses
1261 [assuming we don't fail because there is a matching instance, see
1262 tryTopReact, given case ]
1266 d01 :_g Data Maybe t -- d2 := EvDictSuperClass d0 0
1267 d1 :_w Data Maybe [t]
1268 Then d2 can readily enter the inert, and we also do solving of the wanted
1271 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1273 d2 :_w Sat (Maybe [t])
1275 d01 :_g Data Maybe t
1276 Now, we may simplify d2 more:
1279 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1280 d1 :_g Data Maybe [t]
1281 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1285 d01 :_g Data Maybe t
1287 Now, we can just solve d3.
1290 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1291 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1294 d01 :_g Data Maybe t
1295 And now we can simplify d4 again, but since it has superclasses we *add* them to the worklist:
1298 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1299 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1300 d4 :_g Foo [t] d4 := dfunFoo2 d5
1303 d6 :_g Data Maybe [t] d6 := EvDictSuperClass d4 0
1304 d01 :_g Data Maybe t
1305 Now, d5 can be solved! (and its superclass enter scope)
1308 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1309 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1310 d4 :_g Foo [t] d4 := dfunFoo2 d5
1311 d5 :_g Foo t d5 := dfunFoo1 d7
1314 d6 :_g Data Maybe [t]
1315 d8 :_g Data Maybe t d8 := EvDictSuperClass d5 0
1316 d01 :_g Data Maybe t
1319 [1] Suppose we pick d8 and we react him with d01. Which of the two givens should
1320 we keep? Well, we *MUST NOT* drop d01 because d8 contains recursive evidence
1321 that must not be used (look at case interactInert where both inert and workitem
1322 are givens). So we have several options:
1323 - Drop the workitem always (this will drop d8)
1324 This feels very unsafe -- what if the work item was the "good" one
1325 that should be used later to solve another wanted?
1326 - Don't drop anyone: the inert set may contain multiple givens!
1327 [This is currently implemented]
1329 The "don't drop anyone" seems the most safe thing to do, so now we come to problem 2:
1330 [2] We have added both d6 and d01 in the inert set, and we are interacting our wanted
1331 d7. Now the [isRecDictEv] function in the ineration solver
1332 [case inert-given workitem-wanted] will prevent us from interacting d7 := d8
1333 precisely because chasing the evidence of d8 leads us to an unguarded use of d7.
1335 So, no interaction happens there. Then we meet d01 and there is no recursion
1336 problem there [isRectDictEv] gives us the OK to interact and we do solve d7 := d01!
1338 Note [SUPERCLASS-LOOP 1]
1339 ~~~~~~~~~~~~~~~~~~~~~~~~
1340 We have to be very, very careful when generating superclasses, lest we
1341 accidentally build a loop. Here's an example:
1345 class S a => C a where { opc :: a -> a }
1346 class S b => D b where { opd :: b -> b }
1348 instance C Int where
1351 instance D Int where
1354 From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int}
1355 Simplifying, we may well get:
1356 $dfCInt = :C ds1 (opd dd)
1359 Notice that we spot that we can extract ds1 from dd.
1361 Alas! Alack! We can do the same for (instance D Int):
1363 $dfDInt = :D ds2 (opc dc)
1367 And now we've defined the superclass in terms of itself.
1368 Two more nasty cases are in
1373 - Satisfy the superclass context *all by itself*
1374 (tcSimplifySuperClasses)
1375 - And do so completely; i.e. no left-over constraints
1376 to mix with the constraints arising from method declarations
1379 Note [SUPERCLASS-LOOP 2]
1380 ~~~~~~~~~~~~~~~~~~~~~~~~
1381 We need to be careful when adding "the constaint we are trying to prove".
1382 Suppose we are *given* d1:Ord a, and want to deduce (d2:C [a]) where
1384 class Ord a => C a where
1385 instance Ord [a] => C [a] where ...
1387 Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the
1388 superclasses of C [a] to avails. But we must not overwrite the binding
1389 for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
1392 Here's another variant, immortalised in tcrun020
1393 class Monad m => C1 m
1394 class C1 m => C2 m x
1395 instance C2 Maybe Bool
1396 For the instance decl we need to build (C1 Maybe), and it's no good if
1397 we run around and add (C2 Maybe Bool) and its superclasses to the avails
1398 before we search for C1 Maybe.
1400 Here's another example
1401 class Eq b => Foo a b
1402 instance Eq a => Foo [a] a
1406 we'll first deduce that it holds (via the instance decl). We must not
1407 then overwrite the Eq t constraint with a superclass selection!
1409 At first I had a gross hack, whereby I simply did not add superclass constraints
1410 in addWanted, though I did for addGiven and addIrred. This was sub-optimal,
1411 becuase it lost legitimate superclass sharing, and it still didn't do the job:
1412 I found a very obscure program (now tcrun021) in which improvement meant the
1413 simplifier got two bites a the cherry... so something seemed to be an Stop
1414 first time, but reducible next time.
1416 Now we implement the Right Solution, which is to check for loops directly
1417 when adding superclasses. It's a bit like the occurs check in unification.
1419 Note [Recursive instances and superclases]
1420 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1421 Consider this code, which arises in the context of "Scrap Your
1422 Boilerplate with Class".
1426 instance Sat (ctx Char) => Data ctx Char
1427 instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]
1429 class Data Maybe a => Foo a
1431 instance Foo t => Sat (Maybe t)
1433 instance Data Maybe a => Foo a
1434 instance Foo a => Foo [a]
1437 In the instance for Foo [a], when generating evidence for the superclasses
1438 (ie in tcSimplifySuperClasses) we need a superclass (Data Maybe [a]).
1439 Using the instance for Data, we therefore need
1440 (Sat (Maybe [a], Data Maybe a)
1441 But we are given (Foo a), and hence its superclass (Data Maybe a).
1442 So that leaves (Sat (Maybe [a])). Using the instance for Sat means
1443 we need (Foo [a]). And that is the very dictionary we are bulding
1444 an instance for! So we must put that in the "givens". So in this
1446 Given: Foo a, Foo [a]
1447 Wanted: Data Maybe [a]
1449 BUT we must *not not not* put the *superclasses* of (Foo [a]) in
1450 the givens, which is what 'addGiven' would normally do. Why? Because
1451 (Data Maybe [a]) is the superclass, so we'd "satisfy" the wanted
1452 by selecting a superclass from Foo [a], which simply makes a loop.
1454 On the other hand we *must* put the superclasses of (Foo a) in
1455 the givens, as you can see from the derivation described above.
1457 Conclusion: in the very special case of tcSimplifySuperClasses
1458 we have one 'given' (namely the "this" dictionary) whose superclasses
1459 must not be added to 'givens' by addGiven.
1461 There is a complication though. Suppose there are equalities
1462 instance (Eq a, a~b) => Num (a,b)
1463 Then we normalise the 'givens' wrt the equalities, so the original
1464 given "this" dictionary is cast to one of a different type. So it's a
1465 bit trickier than before to identify the "special" dictionary whose
1466 superclasses must not be added. See test
1467 indexed-types/should_run/EqInInstance
1469 We need a persistent property of the dictionary to record this
1470 special-ness. Current I'm using the InstLocOrigin (a bit of a hack,
1471 but cool), which is maintained by dictionary normalisation.
1472 Specifically, the InstLocOrigin is
1474 then the no-superclass thing kicks in. WATCH OUT if you fiddle
1477 Note [MATCHING-SYNONYMS]
1478 ~~~~~~~~~~~~~~~~~~~~~~~~
1479 When trying to match a dictionary (D tau) to a top-level instance, or a
1480 type family equation (F taus_1 ~ tau_2) to a top-level family instance,
1481 we do *not* need to expand type synonyms because the matcher will do that for us.
1484 Note [RHS-FAMILY-SYNONYMS]
1485 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1486 The RHS of a family instance is represented as yet another constructor which is
1487 like a type synonym for the real RHS the programmer declared. Eg:
1488 type instance F (a,a) = [a]
1490 :R32 a = [a] -- internal type synonym introduced
1491 F (a,a) ~ :R32 a -- instance
1493 When we react a family instance with a type family equation in the work list
1494 we keep the synonym-using RHS without expansion.
1497 *********************************************************************************
1499 The top-reaction Stage
1501 *********************************************************************************
1504 -- If a work item has any form of interaction with top-level we get this
1505 data TopInteractResult
1506 = NoTopInt -- No top-level interaction
1508 { tir_new_work :: WorkList -- Sub-goals or new work (could be given,
1509 -- for superclasses)
1510 , tir_new_inert :: StopOrContinue -- The input work item, ready to become *inert* now:
1511 } -- NB: in ``given'' (solved) form if the
1512 -- original was wanted or given and instance match
1513 -- was found, but may also be in wanted form if we
1514 -- only reacted with functional dependencies
1515 -- arising from top-level instances.
1517 topReactionsStage :: SimplifierStage
1518 topReactionsStage workItem inerts
1519 = do { tir <- tryTopReact workItem
1522 return $ SR { sr_inerts = inerts
1523 , sr_new_work = emptyWorkList
1524 , sr_stop = ContinueWith workItem }
1525 SomeTopInt tir_new_work tir_new_inert ->
1526 return $ SR { sr_inerts = inerts
1527 , sr_new_work = tir_new_work
1528 , sr_stop = tir_new_inert
1532 tryTopReact :: WorkItem -> TcS TopInteractResult
1533 tryTopReact workitem
1534 = do { -- A flag controls the amount of interaction allowed
1535 -- See Note [Simplifying RULE lhs constraints]
1536 ctxt <- getTcSContext
1537 ; if allowedTopReaction (simplEqsOnly ctxt) workitem
1538 then do { traceTcS "tryTopReact / calling doTopReact" (ppr workitem)
1539 ; doTopReact workitem }
1540 else return NoTopInt
1543 allowedTopReaction :: Bool -> WorkItem -> Bool
1544 allowedTopReaction eqs_only (CDictCan {}) = not eqs_only
1545 allowedTopReaction _ _ = True
1548 doTopReact :: WorkItem -> TcS TopInteractResult
1549 -- The work item does not react with the inert set,
1550 -- so try interaction with top-level instances
1551 doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Wanted loc
1552 , cc_class = cls, cc_tyargs = xis })
1553 = do { -- See Note [MATCHING-SYNONYMS]
1554 ; lkp_inst_res <- matchClassInst cls xis loc
1555 ; case lkp_inst_res of
1556 NoInstance -> do { traceTcS "doTopReact/ no class instance for" (ppr dv)
1558 GenInst wtvs ev_term -> -- Solved
1559 -- No need to do fundeps stuff here; the instance
1560 -- matches already so we won't get any more info
1561 -- from functional dependencies
1562 do { traceTcS "doTopReact/ found class instance for" (ppr dv)
1563 ; setDictBind dv ev_term
1564 ; workList <- canWanteds wtvs
1566 -- Solved in one step and no new wanted work produced.
1567 -- i.e we directly matched a top-level instance
1568 -- No point in caching this in 'inert', nor in adding superclasses
1569 then return $ SomeTopInt { tir_new_work = emptyCCan
1570 , tir_new_inert = Stop }
1572 -- Solved and new wanted work produced, you may cache the
1573 -- (tentatively solved) dictionary as Derived and its superclasses
1574 else do { let solved = makeSolved workItem
1575 ; sc_work <- newSCWorkFromFlavored dv (Derived loc) cls xis
1576 ; return $ SomeTopInt
1577 { tir_new_work = workList `unionWorkLists` sc_work
1578 , tir_new_inert = ContinueWith solved } }
1582 -- Try for a fundep reaction beween the wanted item
1583 -- and a top-level instance declaration
1585 = do { instEnvs <- getInstEnvs
1586 ; let eqn_pred_locs = improveFromInstEnv (classInstances instEnvs)
1587 (ClassP cls xis, ppr dv)
1588 ; wevvars <- mkWantedFunDepEqns loc eqn_pred_locs
1589 -- NB: fundeps generate some wanted equalities, but
1590 -- we don't use their evidence for anything
1591 ; fd_work <- canWanteds wevvars
1592 ; sc_work <- newSCWorkFromFlavored dv (Derived loc) cls xis
1593 ; return $ SomeTopInt { tir_new_work = fd_work `unionWorkLists` sc_work
1594 , tir_new_inert = ContinueWith workItem }
1595 -- NB: workItem is inert, but it isn't solved
1596 -- keep it as inert, although it's not solved because we
1597 -- have now reacted all its top-level fundep-induced equalities!
1599 -- See Note [FunDep Reactions]
1602 -- Otherwise, we have a given or derived
1603 doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = fl
1604 , cc_class = cls, cc_tyargs = xis })
1605 = do { sc_work <- newSCWorkFromFlavored dv fl cls xis
1606 ; return $ SomeTopInt sc_work (ContinueWith workItem) }
1607 -- See Note [Given constraint that matches an instance declaration]
1610 doTopReact (CFunEqCan { cc_id = cv, cc_flavor = fl
1611 , cc_fun = tc, cc_tyargs = args, cc_rhs = xi })
1612 = ASSERT (isSynFamilyTyCon tc) -- No associated data families have reached that far
1613 do { match_res <- matchFam tc args -- See Note [MATCHING-SYNONYMS]
1617 MatchInstSingle (rep_tc, rep_tys)
1618 -> do { let Just coe_tc = tyConFamilyCoercion_maybe rep_tc
1619 Just rhs_ty = tcView (mkTyConApp rep_tc rep_tys)
1620 -- Eagerly expand away the type synonym on the
1621 -- RHS of a type function, so that it never
1622 -- appears in an error message
1623 -- See Note [Type synonym families] in TyCon
1624 coe = mkTyConApp coe_tc rep_tys
1626 Wanted {} -> do { cv' <- newWantedCoVar rhs_ty xi
1627 ; setWantedCoBind cv $
1628 coe `mkTransCoercion`
1631 _ -> newGivOrDerCoVar xi rhs_ty $
1632 mkSymCoercion (mkCoVarCoercion cv) `mkTransCoercion` coe
1634 ; workList <- mkCanonical fl cv'
1635 ; return $ SomeTopInt workList Stop }
1637 -> panicTcS $ text "TcSMonad.matchFam returned multiple instances!"
1641 -- Any other work item does not react with any top-level equations
1642 doTopReact _workItem = return NoTopInt
1645 Note [FunDep and implicit parameter reactions]
1646 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1647 Currently, our story of interacting two dictionaries (or a dictionary
1648 and top-level instances) for functional dependencies, and implicit
1649 paramters, is that we simply produce new wanted equalities. So for example
1651 class D a b | a -> b where ...
1657 We generate the extra work item
1659 where 'cv' is currently unused. However, this new item reacts with d2,
1660 discharging it in favour of a new constraint d2' thus:
1662 d2 := d2' |> D Int cv
1663 Now d2' can be discharged from d1
1665 We could be more aggressive and try to *immediately* solve the dictionary
1666 using those extra equalities. With the same inert set and work item we
1667 might dischard d2 directly:
1670 d2 := d1 |> D Int cv
1672 But in general it's a bit painful to figure out the necessary coercion,
1673 so we just take the first approach.
1675 It's exactly the same with implicit parameters, except that the
1676 "aggressive" approach would be much easier to implement.
1678 Note [When improvement happens]
1679 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1680 We fire an improvement rule when
1682 * Two constraints match (modulo the fundep)
1683 e.g. C t1 t2, C t1 t3 where C a b | a->b
1684 The two match because the first arg is identical
1686 * At least one is not Given. If they are both given, we don't fire
1687 the reaction because we have no way of constructing evidence for a
1688 new equality nor does it seem right to create a new wanted goal
1689 (because the goal will most likely contain untouchables, which
1690 can't be solved anyway)!
1692 Note that we *do* fire the improvement if one is Given and one is Derived.
1693 The latter can be a superclass of a wanted goal. Example (tcfail138)
1694 class L a b | a -> b
1695 class (G a, L a b) => C a b
1697 instance C a b' => G (Maybe a)
1698 instance C a b => C (Maybe a) a
1699 instance L (Maybe a) a
1701 When solving the superclasses of the (C (Maybe a) a) instance, we get
1702 Given: C a b ... and hance by superclasses, (G a, L a b)
1704 Use the instance decl to get
1706 The (C a b') is inert, so we generate its Derived superclasses (L a b'),
1707 and now we need improvement between that derived superclass an the Given (L a b)
1709 Note [Overriding implicit parameters]
1710 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1712 f :: (?x::a) -> Bool -> a
1714 g v = let ?x::Int = 3
1715 in (f v, let ?x::Bool = True in f v)
1717 This should probably be well typed, with
1718 g :: Bool -> (Int, Bool)
1720 So the inner binding for ?x::Bool *overrides* the outer one.
1721 Hence a work-item Given overrides an inert-item Given.
1723 Note [Given constraint that matches an instance declaration]
1724 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1725 What should we do when we discover that one (or more) top-level
1726 instances match a given (or solved) class constraint? We have
1729 1. Reject the program. The reason is that there may not be a unique
1730 best strategy for the solver. Example, from the OutsideIn(X) paper:
1731 instance P x => Q [x]
1732 instance (x ~ y) => R [x] y
1734 wob :: forall a b. (Q [b], R b a) => a -> Int
1736 g :: forall a. Q [a] => [a] -> Int
1739 will generate the impliation constraint:
1740 Q [a] => (Q [beta], R beta [a])
1741 If we react (Q [beta]) with its top-level axiom, we end up with a
1742 (P beta), which we have no way of discharging. On the other hand,
1743 if we react R beta [a] with the top-level we get (beta ~ a), which
1744 is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
1745 now solvable by the given Q [a].
1747 However, this option is restrictive, for instance [Example 3] from
1748 Note [Recursive dictionaries] will fail to work.
1750 2. Ignore the problem, hoping that the situations where there exist indeed
1751 such multiple strategies are rare: Indeed the cause of the previous
1752 problem is that (R [x] y) yields the new work (x ~ y) which can be
1753 *spontaneously* solved, not using the givens.
1755 We are choosing option 2 below but we might consider having a flag as well.
1758 Note [New Wanted Superclass Work]
1759 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1760 Even in the case of wanted constraints, we add all of its superclasses as
1761 new given work. There are several reasons for this:
1762 a) to minimise error messages;
1763 eg suppose we have wanted (Eq a, Ord a)
1764 then we report only (Ord a) unsoluble
1766 b) to make the smallest number of constraints when *inferring* a type
1767 (same Eq/Ord example)
1769 c) for recursive dictionaries we *must* add the superclasses
1770 so that we can use them when solving a sub-problem
1772 d) To allow FD-like improvement for type families. Assume that
1774 class C a b | a -> b
1775 and we have to solve the implication constraint:
1777 Then, FD improvement can help us to produce a new wanted (beta ~ b)
1779 We want to have the same effect with the type family encoding of
1780 functional dependencies. Namely, consider:
1781 class (F a ~ b) => C a b
1782 Now suppose that we have:
1785 By interacting the given we will get that (F a ~ b) which is not
1786 enough by itself to make us discharge (C a beta). However, we
1787 may create a new given equality from the super-class that we promise
1788 to solve: (F a ~ beta). Now we may interact this with the rest of
1789 constraint to finally get:
1792 But 'beta' is a touchable unification variable, and hence OK to
1793 unify it with 'b', replacing the given evidence with the identity.
1795 This requires trySpontaneousSolve to solve given equalities that
1796 have a touchable in their RHS, *in addition* to solving wanted
1799 Here is another example where this is useful.
1803 class (F a ~ b) => C a b
1804 And we are given the wanteds:
1808 We surely do *not* want to quantify over (b ~ c), since if someone provides
1809 dictionaries for (C a b) and (C a c), these dictionaries can provide a proof
1810 of (b ~ c), hence no extra evidence is necessary. Here is what will happen:
1812 Step 1: We will get new *given* superclass work,
1813 provisionally to our solving of w1 and w2
1815 g1: F a ~ b, g2 : F a ~ c,
1816 w1 : C a b, w2 : C a c, w3 : b ~ c
1818 The evidence for g1 and g2 is a superclass evidence term:
1820 g1 := sc w1, g2 := sc w2
1822 Step 2: The givens will solve the wanted w3, so that
1823 w3 := sym (sc w1) ; sc w2
1825 Step 3: Now, one may naively assume that then w2 can be solve from w1
1826 after rewriting with the (now solved equality) (b ~ c).
1828 But this rewriting is ruled out by the isGoodRectDict!
1830 Conclusion, we will (correctly) end up with the unsolved goals
1833 NB: The desugarer needs be more clever to deal with equalities
1834 that participate in recursive dictionary bindings.
1837 newSCWorkFromFlavored :: EvVar -> CtFlavor -> Class -> [Xi]
1839 newSCWorkFromFlavored ev flavor cls xis
1840 | Given loc <- flavor -- The NoScSkol says "don't add superclasses"
1841 , NoScSkol <- ctLocOrigin loc -- Very important!
1842 = return emptyWorkList
1845 = do { let (tyvars, sc_theta, _, _) = classBigSig cls
1846 sc_theta1 = substTheta (zipTopTvSubst tyvars xis) sc_theta
1847 -- Add *all* its superclasses (equalities or not) as new given work
1848 -- See Note [New Wanted Superclass Work]
1849 ; sc_vars <- zipWithM inst_one sc_theta1 [0..]
1850 ; mkCanonicals flavor sc_vars }
1852 inst_one pred n = newGivOrDerEvVar pred (EvSuperClass ev n)
1854 data LookupInstResult
1856 | GenInst [WantedEvVar] EvTerm
1858 matchClassInst :: Class -> [Type] -> WantedLoc -> TcS LookupInstResult
1859 matchClassInst clas tys loc
1860 = do { let pred = mkClassPred clas tys
1861 ; mb_result <- matchClass clas tys
1863 MatchInstNo -> return NoInstance
1864 MatchInstMany -> return NoInstance -- defer any reactions of a multitude until
1865 -- we learn more about the reagent
1866 MatchInstSingle (dfun_id, mb_inst_tys) ->
1867 do { checkWellStagedDFun pred dfun_id loc
1869 -- It's possible that not all the tyvars are in
1870 -- the substitution, tenv. For example:
1871 -- instance C X a => D X where ...
1872 -- (presumably there's a functional dependency in class C)
1873 -- Hence mb_inst_tys :: Either TyVar TcType
1875 ; tys <- instDFunTypes mb_inst_tys
1876 ; let (theta, _) = tcSplitPhiTy (applyTys (idType dfun_id) tys)
1877 ; if null theta then
1878 return (GenInst [] (EvDFunApp dfun_id tys []))
1880 { ev_vars <- instDFunConstraints theta
1881 ; let wevs = [WantedEvVar w loc | w <- ev_vars]
1882 ; return $ GenInst wevs (EvDFunApp dfun_id tys ev_vars) }