3 solveInteract, AtomicInert,
4 InertSet, emptyInert, updInertSet, extractUnsolved, solveOne,
8 #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_cts :: Bag.Bag CanonicalCt
114 , inert_fsks :: Map.Map TcTyVar [(TcTyVar,Coercion)] }
115 -- See Note [InertSet FlattenSkolemEqClass]
117 instance Outputable InertSet where
118 ppr is = vcat [ vcat (map ppr (Bag.bagToList $ inert_cts is))
119 , vcat (map (\(v,rest) -> ppr v <+> text "|->" <+> hsep (map (ppr.fst) rest))
120 (Map.toList $ inert_fsks is)
124 emptyInert :: InertSet
125 emptyInert = IS { inert_cts = Bag.emptyBag, inert_fsks = Map.empty }
127 updInertSet :: InertSet -> AtomicInert -> InertSet
128 -- Introduces an element in the inert set for the first time
129 updInertSet (IS { inert_cts = cts, inert_fsks = fsks })
130 item@(CTyEqCan { cc_id = cv
133 | Just tv2 <- tcGetTyVar_maybe xi,
134 FlatSkol {} <- tcTyVarDetails tv1,
135 FlatSkol {} <- tcTyVarDetails tv2
136 = let cts' = cts `Bag.snocBag` item
137 fsks' = Map.insertWith (++) tv2 [(tv1, mkCoVarCoercion cv)] fsks
138 -- See Note [InertSet FlattenSkolemEqClass]
139 in IS { inert_cts = cts', inert_fsks = fsks' }
140 updInertSet (IS { inert_cts = cts
141 , inert_fsks = fsks }) item
142 = let cts' = cts `Bag.snocBag` item
143 in IS { inert_cts = cts', inert_fsks = fsks }
145 foldlInertSetM :: (Monad m) => (a -> AtomicInert -> m a) -> a -> InertSet -> m a
146 foldlInertSetM k z (IS { inert_cts = cts })
147 = Bag.foldlBagM k z cts
149 extractUnsolved :: InertSet -> (InertSet, CanonicalCts)
150 extractUnsolved is@(IS {inert_cts = cts})
151 = (is { inert_cts = cts'}, unsolved)
152 where (unsolved, cts') = Bag.partitionBag isWantedCt cts
155 getFskEqClass :: InertSet -> TcTyVar -> [(TcTyVar,Coercion)]
156 -- Precondition: tv is a FlatSkol. See Note [InertSet FlattenSkolemEqClass]
157 getFskEqClass (IS { inert_cts = cts, inert_fsks = fsks }) tv
158 = case lkpTyEqCanByLhs of
159 Nothing -> fromMaybe [] (Map.lookup tv fsks)
161 case tcGetTyVar_maybe (cc_rhs ceq) of
162 Just tv_rhs | FlatSkol {} <- tcTyVarDetails tv_rhs
163 -> let ceq_co = mkSymCoercion $ mkCoVarCoercion (cc_id ceq)
164 mk_co (v,c) = (v, mkTransCoercion c ceq_co)
165 in (tv_rhs, ceq_co): map mk_co (fromMaybe [] $ Map.lookup tv fsks)
167 where lkpTyEqCanByLhs = Bag.foldlBag lkp Nothing cts
168 lkp :: Maybe CanonicalCt -> CanonicalCt -> Maybe CanonicalCt
169 lkp Nothing ct@(CTyEqCan {cc_tyvar = tv'}) | tv' == tv = Just ct
170 lkp other _ct = other
173 isWantedCt :: CanonicalCt -> Bool
174 isWantedCt ct = isWanted (cc_flavor ct)
177 data Inert = IS { class_inerts :: FiniteMap Class Atomics
178 ip_inerts :: FiniteMap Class Atomics
179 tyfun_inerts :: FiniteMap TyCon Atomics
180 tyvar_inerts :: FiniteMap TyVar Atomics
183 Later should we also separate out givens and wanteds?
188 Note [Touchables and givens]
189 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
190 Touchable variables will never show up in givens which are inputs to
191 the solver. However, touchables may show up in givens generated by the flattener.
206 which can be put in the inert set. Suppose we also have a wanted
210 We cannot rewrite the given G alpha ~g b using the wanted alpha ~w
211 Int. Instead, after reacting alpha ~w Int with the whole inert set,
212 we observe that we can solve it by unifying alpha with Int, so we mark
213 it as solved and put it back in the *work list*. [We also immediately unify
214 alpha := Int, without telling anyone, see trySpontaneousSolve function, to
215 avoid doing this in the end.]
217 Later, because it is solved (given, in effect), we can use it to rewrite
218 G alpha ~g b to G Int ~g b, which gets put back in the work list. Eventually,
219 we will dispatch the remaining wanted constraints using the top-level axioms.
221 Finally, note that after reacting a wanted equality with the entire inert set
222 we may end up with something like
226 which we should flip around to generate the solved constraint alpha ~s b.
228 %*********************************************************************
230 * Main Interaction Solver *
232 **********************************************************************
236 1. Canonicalise (unary)
237 2. Pairwise interaction (binary)
238 * Take one from work list
239 * Try all pair-wise interactions with each constraint in inert
240 3. Try to solve spontaneously for equalities involving touchables
241 4. Top-level interaction (binary wrt top-level)
242 Superclass decomposition belongs in (4), see note [Superclasses]
246 type AtomicInert = CanonicalCt -- constraint pulled from InertSet
247 type WorkItem = CanonicalCt -- constraint pulled from WorkList
249 type WorkList = CanonicalCts -- A mixture of Given, Wanted, and Solved
250 type SWorkList = WorkList -- A worklist of solved
253 listToWorkList :: [WorkItem] -> WorkList
254 listToWorkList = Bag.listToBag
256 unionWorkLists :: WorkList -> WorkList -> WorkList
257 unionWorkLists = Bag.unionBags
259 foldlWorkListM :: (Monad m) => (a -> WorkItem -> m a) -> a -> WorkList -> m a
260 foldlWorkListM = Bag.foldlBagM
262 isEmptyWorkList :: WorkList -> Bool
263 isEmptyWorkList = Bag.isEmptyBag
265 emptyWorkList :: WorkList
266 emptyWorkList = Bag.emptyBag
268 singletonWorkList :: CanonicalCt -> WorkList
269 singletonWorkList ct = singleCCan ct
272 = Stop -- Work item is consumed
273 | ContinueWith WorkItem -- Not consumed
275 instance Outputable StopOrContinue where
276 ppr Stop = ptext (sLit "Stop")
277 ppr (ContinueWith w) = ptext (sLit "ContinueWith") <+> ppr w
279 -- Results after interacting a WorkItem as far as possible with an InertSet
281 = SR { sr_inerts :: InertSet
282 -- The new InertSet to use (REPLACES the old InertSet)
283 , sr_new_work :: WorkList
284 -- Any new work items generated (should be ADDED to the old WorkList)
286 -- sr_stop = Just workitem => workitem is *not* in sr_inerts and
287 -- workitem is inert wrt to sr_inerts
288 , sr_stop :: StopOrContinue
291 instance Outputable StageResult where
292 ppr (SR { sr_inerts = inerts, sr_new_work = work, sr_stop = stop })
293 = ptext (sLit "SR") <+>
294 braces (sep [ ptext (sLit "inerts =") <+> ppr inerts <> comma
295 , ptext (sLit "new work =") <+> ppr work <> comma
296 , ptext (sLit "stop =") <+> ppr stop])
298 type SimplifierStage = WorkItem -> InertSet -> TcS StageResult
300 -- Combine a sequence of simplifier 'stages' to create a pipeline
301 runSolverPipeline :: [(String, SimplifierStage)]
302 -> InertSet -> WorkItem
303 -> TcS (InertSet, WorkList)
304 -- Precondition: non-empty list of stages
305 runSolverPipeline pipeline inerts workItem
306 = do { traceTcS "Start solver pipeline" $
307 vcat [ ptext (sLit "work item =") <+> ppr workItem
308 , ptext (sLit "inerts =") <+> ppr inerts]
310 ; let itr_in = SR { sr_inerts = inerts
311 , sr_new_work = emptyWorkList
312 , sr_stop = ContinueWith workItem }
313 ; itr_out <- run_pipeline pipeline itr_in
315 = case sr_stop itr_out of
316 Stop -> sr_inerts itr_out
317 ContinueWith item -> sr_inerts itr_out `updInertSet` item
318 ; return (new_inert, sr_new_work itr_out) }
320 run_pipeline :: [(String, SimplifierStage)]
321 -> StageResult -> TcS StageResult
322 run_pipeline [] itr = return itr
323 run_pipeline _ itr@(SR { sr_stop = Stop }) = return itr
325 run_pipeline ((name,stage):stages)
326 (SR { sr_new_work = accum_work
328 , sr_stop = ContinueWith work_item })
329 = do { itr <- stage work_item inerts
330 ; traceTcS ("Stage result (" ++ name ++ ")") (ppr itr)
331 ; let itr' = itr { sr_new_work = sr_new_work itr
332 `unionWorkLists` accum_work }
333 ; run_pipeline stages itr' }
337 Inert: {c ~ d, F a ~ t, b ~ Int, a ~ ty} (all given)
338 Reagent: a ~ [b] (given)
340 React with (c~d) ==> IR (ContinueWith (a~[b])) True []
341 React with (F a ~ t) ==> IR (ContinueWith (a~[b])) False [F [b] ~ t]
342 React with (b ~ Int) ==> IR (ContinueWith (a~[Int]) True []
345 Inert: {c ~w d, F a ~g t, b ~w Int, a ~w ty}
348 React with (c ~w d) ==> IR (ContinueWith (a~[b])) True []
349 React with (F a ~g t) ==> IR (ContinueWith (a~[b])) True [] (can't rewrite given with wanted!)
353 Inert: {a ~ Int, F Int ~ b} (given)
354 Reagent: F a ~ b (wanted)
356 React with (a ~ Int) ==> IR (ContinueWith (F Int ~ b)) True []
357 React with (F Int ~ b) ==> IR Stop True [] -- after substituting we re-canonicalize and get nothing
360 -- Main interaction solver: we fully solve the worklist 'in one go',
361 -- returning an extended inert set.
363 -- See Note [Touchables and givens].
364 solveInteract :: InertSet -> WorkList -> TcS InertSet
365 solveInteract inert ws
366 = do { dyn_flags <- getDynFlags
367 ; solveInteractWithDepth (ctxtStkDepth dyn_flags,0,[]) inert ws
369 solveOne :: InertSet -> WorkItem -> TcS InertSet
370 solveOne inerts workItem
371 = do { dyn_flags <- getDynFlags
372 ; solveOneWithDepth (ctxtStkDepth dyn_flags,0,[]) inerts workItem
376 solveInteractWithDepth :: (Int, Int, [WorkItem])
377 -> InertSet -> WorkList -> TcS InertSet
378 solveInteractWithDepth ctxt@(max_depth,n,stack) inert ws
383 = solverDepthErrorTcS n stack
386 = do { traceTcS "solveInteractWithDepth" $
387 vcat [ text "Current depth =" <+> ppr n
388 , text "Max depth =" <+> ppr max_depth
390 ; foldlWorkListM (solveOneWithDepth ctxt) inert ws }
393 -- Fully interact the given work item with an inert set, and return a
394 -- new inert set which has assimilated the new information.
395 solveOneWithDepth :: (Int, Int, [WorkItem])
396 -> InertSet -> WorkItem -> TcS InertSet
397 solveOneWithDepth (max_depth, n, stack) inert work
398 = do { traceTcS0 (indent ++ "Solving {") (ppr work)
399 ; (new_inert, new_work) <- runSolverPipeline thePipeline inert work
401 ; traceTcS0 (indent ++ "Subgoals:") (ppr new_work)
403 -- Recursively solve the new work generated
404 -- from workItem, with a greater depth
405 ; res_inert <- solveInteractWithDepth (max_depth, n+1, work:stack)
408 ; traceTcS0 (indent ++ "Done }") (ppr work)
411 indent = replicate (2*n) ' '
413 thePipeline :: [(String,SimplifierStage)]
414 thePipeline = [ ("interact with inerts", interactWithInertsStage)
415 , ("spontaneous solve", spontaneousSolveStage)
416 , ("top-level reactions", topReactionsStage) ]
419 *********************************************************************************
421 The spontaneous-solve Stage
423 *********************************************************************************
426 spontaneousSolveStage :: SimplifierStage
427 spontaneousSolveStage workItem inerts
428 = do { mSolve <- trySpontaneousSolve workItem inerts
430 Nothing -> -- no spontaneous solution for him, keep going
431 return $ SR { sr_new_work = emptyWorkList
433 , sr_stop = ContinueWith workItem }
435 Just workList' -> -- He has been solved; workList' are all givens
436 return $ SR { sr_new_work = workList'
441 {-- This is all old code, but does not quite work now. The problem is that due to
442 Note [Loopy Spontaneous Solving] we may have unflattened a type, to be able to
443 perform a sneaky unification. This unflattening means that we may have to recanonicalize
444 a given (solved) equality, this is why the result of trySpontaneousSolve is now a list
445 of constraints (instead of an atomic solved constraint). We would have to react all of
446 them once again with the worklist but that is very tiresome. Instead we throw them back
449 | isWantedCt workItem
450 -- Original was wanted we have now made him given so
451 -- we have to ineract him with the inerts again because
452 -- of the change in his status. This may produce some work.
453 -> do { traceTcS "recursive interact with inerts {" $ vcat
454 [ text "work = " <+> ppr workItem'
455 , text "inerts = " <+> ppr inerts ]
456 ; itr_again <- interactWithInertsStage workItem' inerts
457 ; case sr_stop itr_again of
458 Stop -> pprPanic "BUG: Impossible to happen" $
459 vcat [ text "Original workitem:" <+> ppr workItem
460 , text "Spontaneously solved:" <+> ppr workItem'
461 , text "Solved was consumed, when reacting with inerts:"
462 , nest 2 (ppr inerts) ]
463 ContinueWith workItem'' -- Now *this* guy is inert wrt to inerts
464 -> do { traceTcS "end recursive interact }" $ ppr workItem''
465 ; return $ SR { sr_new_work = sr_new_work itr_again
466 , sr_inerts = sr_inerts itr_again
467 `extendInertSet` workItem''
471 -> return $ SR { sr_new_work = emptyWorkList
472 , sr_inerts = inerts `extendInertSet` workItem'
476 -- @trySpontaneousSolve wi@ solves equalities where one side is a
477 -- touchable unification variable. Returns:
478 -- * Nothing if we were not able to solve it
479 -- * Just wi' if we solved it, wi' (now a "given") should be put in the work list.
480 -- See Note [Touchables and givens]
481 -- Note, just passing the inerts through for the skolem equivalence classes
482 trySpontaneousSolve :: WorkItem -> InertSet -> TcS (Maybe SWorkList)
483 trySpontaneousSolve (CTyEqCan { cc_id = cv, cc_flavor = gw, cc_tyvar = tv1, cc_rhs = xi }) inerts
486 | Just tv2 <- tcGetTyVar_maybe xi
487 = do { tch1 <- isTouchableMetaTyVar tv1
488 ; tch2 <- isTouchableMetaTyVar tv2
489 ; case (tch1, tch2) of
490 (True, True) -> trySpontaneousEqTwoWay inerts cv gw tv1 tv2
491 (True, False) -> trySpontaneousEqOneWay inerts cv gw tv1 xi
492 (False, True) | tyVarKind tv1 `isSubKind` tyVarKind tv2
493 -> trySpontaneousEqOneWay inerts cv gw tv2 (mkTyVarTy tv1)
494 _ -> return Nothing }
496 = do { tch1 <- isTouchableMetaTyVar tv1
497 ; if tch1 then trySpontaneousEqOneWay inerts cv gw tv1 xi
498 else return Nothing }
501 -- trySpontaneousSolve (CFunEqCan ...) = ...
502 -- See Note [No touchables as FunEq RHS] in TcSMonad
503 trySpontaneousSolve _ _ = return Nothing
506 trySpontaneousEqOneWay :: InertSet -> CoVar -> CtFlavor -> TcTyVar -> Xi
507 -> TcS (Maybe SWorkList)
508 -- tv is a MetaTyVar, not untouchable
509 -- Precondition: kind(xi) is a sub-kind of kind(tv)
510 trySpontaneousEqOneWay inerts cv gw tv xi
511 | not (isSigTyVar tv) || isTyVarTy xi
512 = solveWithIdentity inerts cv gw tv xi
517 trySpontaneousEqTwoWay :: InertSet -> CoVar -> CtFlavor -> TcTyVar -> TcTyVar
518 -> TcS (Maybe SWorkList)
519 -- Both tyvars are *touchable* MetaTyvars
520 -- By the CTyEqCan invariant, k2 `isSubKind` k1
521 trySpontaneousEqTwoWay inerts cv gw tv1 tv2
523 , nicer_to_update_tv2 = solveWithIdentity inerts cv gw tv2 (mkTyVarTy tv1)
524 | otherwise = ASSERT( k2 `isSubKind` k1 )
525 solveWithIdentity inerts cv gw tv1 (mkTyVarTy tv2)
529 nicer_to_update_tv2 = isSigTyVar tv1 || isSystemName (Var.varName tv2)
532 Note [Loopy spontaneous solving]
533 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
534 Consider the original wanted:
535 wanted : Maybe (E alpha) ~ alpha
536 where E is a type family, such that E (T x) = x. After canonicalization,
537 as a result of flattening, we will get:
538 given : E alpha ~ fsk
539 wanted : alpha ~ Maybe fsk
540 where (fsk := E alpha, on the side). Now, if we spontaneously *solve*
541 (alpha := Maybe fsk) we are in trouble! Instead, we should refrain from solving
542 it and keep it as wanted. In inference mode we'll end up quantifying over
543 (alpha ~ Maybe (E alpha))
544 Hence, 'solveWithIdentity' performs a small occurs check before
545 actually solving. But this occurs check *must look through* flatten skolems.
547 However, it may be the case that the flatten skolem in hand is equal to some other
548 flatten skolem whith *does not* mention our unification variable. Here's a typical example:
553 After canonicalization:
558 After some reactions:
563 At this point, we will try to spontaneously solve (alpha ~ f2) which remains as yet unsolved.
564 We will look inside f2, which immediately mentions (F alpha), so it's not good to unify! However
565 by looking at the equivalence class of the flatten skolems, we can see that it is fine to
566 unify (alpha ~ f1) which solves our goals!
568 A similar problem happens because of other spontaneous solving. Suppose we have the
569 following wanteds, arriving in this exact order:
570 (first) w: beta ~ alpha
571 (second) w: alpha ~ fsk
572 (third) g: F beta ~ fsk
573 Then, we first spontaneously solve the first constraint, making (beta := alpha), and having
574 (beta ~ alpha) as given. *Then* we encounter the second wanted (alpha ~ fsk). "fsk" does not
575 obviously mention alpha, so naively we can also spontaneously solve (alpha := fsk). But
576 that is wrong since fsk mentions beta, which has already secretly been unified to alpha!
578 To avoid this problem, the same occurs check must unveil rewritings that can happen because
579 of spontaneously having solved other constraints.
582 Note [Avoid double unifications]
583 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
584 The spontaneous solver has to return a given which mentions the unified unification
585 variable *on the left* of the equality. Here is what happens if not:
586 Original wanted: (a ~ alpha), (alpha ~ Int)
587 We spontaneously solve the first wanted, without changing the order!
588 given : a ~ alpha [having unified alpha := a]
589 Now the second wanted comes along, but he cannot rewrite the given, so we simply continue.
590 At the end we spontaneously solve that guy, *reunifying* [alpha := Int]
592 We avoid this problem by orienting the given so that the unification
593 variable is on the left. [Note that alternatively we could attempt to
594 enforce this at canonicalization]
596 See also Note [No touchables as FunEq RHS] in TcSMonad; avoiding
597 double unifications is the main reason we disallow touchable
598 unification variables as RHS of type family equations: F xis ~ alpha.
602 solveWithIdentity :: InertSet
603 -> CoVar -> CtFlavor -> TcTyVar -> Xi
604 -> TcS (Maybe SWorkList)
605 -- Solve with the identity coercion
606 -- Precondition: kind(xi) is a sub-kind of kind(tv)
607 -- Precondition: CtFlavor is not Given
608 -- See [New Wanted Superclass Work] to see why we do this for *given* as well
609 solveWithIdentity inerts cv gw tv xi
610 = do { tybnds <- getTcSTyBindsBag
611 ; case occurCheck tybnds inerts tv xi of
612 Nothing -> return Nothing
613 Just (xi_unflat,coi) -> solve_with xi_unflat coi }
615 solve_with xi_unflat coi -- coi : xi_unflat ~ xi
616 = do { traceTcS "Sneaky unification:" $
617 vcat [text "Coercion variable: " <+> ppr gw,
618 text "Coercion: " <+> pprEq (mkTyVarTy tv) xi,
619 text "Left Kind is : " <+> ppr (typeKind (mkTyVarTy tv)),
620 text "Right Kind is : " <+> ppr (typeKind xi)
622 ; setWantedTyBind tv xi_unflat -- Set tv := xi_unflat
623 ; cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi_unflat xi_unflat
624 ; let flav = mkGivenFlavor gw UnkSkol
625 ; (cts, co) <- case coi of
626 ACo co -> do { can_eqs <- canEq flav cv_given (mkTyVarTy tv) xi_unflat
627 ; return (can_eqs, co) }
629 (singleCCan (CTyEqCan { cc_id = cv_given
630 , cc_flavor = mkGivenFlavor gw UnkSkol
631 , cc_tyvar = tv, cc_rhs = xi }
632 -- xi, *not* xi_unflat because
633 -- xi_unflat may require flattening!
636 Wanted {} -> setWantedCoBind cv co
637 Derived {} -> setDerivedCoBind cv co
638 _ -> pprPanic "Can't spontaneously solve *given*" empty
639 -- See Note [Avoid double unifications]
640 ; return (Just cts) }
642 occurCheck :: Bag (TcTyVar, TcType) -> InertSet
643 -> TcTyVar -> TcType -> Maybe (TcType,CoercionI)
644 -- Traverse @ty@ to make sure that @tv@ does not appear under some flatten skolem.
645 -- If it appears under some flatten skolem look in that flatten skolem equivalence class
646 -- (see Note [InertSet FlattenSkolemEqClass], [Loopy Spontaneous Solving]) to see if you
647 -- can find a different flatten skolem to use, that is, one that does not mention @tv@.
649 -- Postcondition: Just (ty', coi) = occurCheck binds inerts tv ty
651 -- NB: The returned type ty' may not be flat!
653 occurCheck ty_binds_bag inerts tv ty
656 ok bad this_ty@(TyConApp tc tys)
657 | Just tys_cois <- allMaybes (map (ok bad) tys)
658 , (tys',cois') <- unzip tys_cois
659 = Just (TyConApp tc tys', mkTyConAppCoI tc cois')
660 | isSynTyCon tc, Just ty_expanded <- tcView this_ty
661 = ok bad ty_expanded -- See Note [Type synonyms and the occur check] in TcUnify
663 | Just (sty',coi) <- ok_pred bad sty
664 = Just (PredTy sty', coi)
665 ok bad (FunTy arg res)
666 | Just (arg', coiarg) <- ok bad arg, Just (res', coires) <- ok bad res
667 = Just (FunTy arg' res', mkFunTyCoI coiarg coires)
668 ok bad (AppTy fun arg)
669 | Just (fun', coifun) <- ok bad fun, Just (arg', coiarg) <- ok bad arg
670 = Just (AppTy fun' arg', mkAppTyCoI coifun coiarg)
671 ok bad (ForAllTy tv1 ty1)
672 -- WARNING: What if it is a (t1 ~ t2) => t3? It's not handled properly at the moment.
673 | Just (ty1', coi) <- ok bad ty1
674 = Just (ForAllTy tv1 ty1', mkForAllTyCoI tv1 coi)
677 ok _bad this_ty@(TyVarTy tv')
678 | not $ isTcTyVar tv' = Just (this_ty, IdCo this_ty) -- Bound variable
679 | tv == tv' = Nothing -- Occurs check error
682 | FlatSkol zty <- tcTyVarDetails fsk
683 = if fsk `elemVarSet` bad then
684 -- its type has been checked
685 go_down_eq_class bad $ getFskEqClass inerts fsk
687 -- its type is not yet checked
689 Nothing -> go_down_eq_class (bad `extendVarSet` fsk) $
690 getFskEqClass inerts fsk
691 Just (zty',ico) -> Just (zty',ico)
693 -- Check if there exists a ty bind already, as a result of sneaky unification.
694 ok bad this_ty@(TyVarTy tv0)
695 = case Bag.foldlBag find_bind Nothing ty_binds_bag of
696 Nothing -> Just (this_ty, IdCo this_ty)
697 Just ty0 -> ok bad ty0
698 where find_bind Nothing (tvx,tyx) | tv0 == tvx = Just tyx
701 ok _bad _ty = Nothing
703 ok_pred bad (ClassP cn tys)
704 | Just tys_cois <- allMaybes $ map (ok bad) tys
705 = let (tys', cois') = unzip tys_cois
706 in Just (ClassP cn tys', mkClassPPredCoI cn cois')
707 ok_pred bad (IParam nm ty)
708 | Just (ty',co') <- ok bad ty
709 = Just (IParam nm ty', mkIParamPredCoI nm co')
710 ok_pred bad (EqPred ty1 ty2)
711 | Just (ty1',coi1) <- ok bad ty1, Just (ty2',coi2) <- ok bad ty2
712 = Just (EqPred ty1' ty2', mkEqPredCoI coi1 coi2)
713 ok_pred _ _ = Nothing
715 go_down_eq_class _bad_tvs [] = Nothing
716 go_down_eq_class bad_tvs ((fsk1,co1):rest)
717 | fsk1 `elemVarSet` bad_tvs = go_down_eq_class bad_tvs rest
719 = case ok bad_tvs (TyVarTy fsk1) of
720 Nothing -> go_down_eq_class (bad_tvs `extendVarSet` fsk1) rest
721 Just (ty1,co1i') -> Just (ty1, mkTransCoI co1i' (ACo co1))
725 *********************************************************************************
727 The interact-with-inert Stage
729 *********************************************************************************
732 -- Interaction result of WorkItem <~> AtomicInert
734 = IR { ir_stop :: StopOrContinue
736 -- => Reagent (work item) consumed.
737 -- ContinueWith new_reagent
738 -- => Reagent transformed but keep gathering interactions.
739 -- The transformed item remains inert with respect
740 -- to any previously encountered inerts.
742 , ir_inert_action :: InertAction
743 -- Whether the inert item should remain in the InertSet.
745 , ir_new_work :: WorkList
746 -- new work items to add to the WorkList
749 -- What to do with the inert reactant.
750 data InertAction = KeepInert | DropInert
753 mkIRContinue :: Monad m => WorkItem -> InertAction -> WorkList -> m InteractResult
754 mkIRContinue wi keep newWork = return $ IR (ContinueWith wi) keep newWork
756 mkIRStop :: Monad m => InertAction -> WorkList -> m InteractResult
757 mkIRStop keep newWork = return $ IR Stop keep newWork
759 dischargeWorkItem :: Monad m => m InteractResult
760 dischargeWorkItem = mkIRStop KeepInert emptyCCan
762 noInteraction :: Monad m => WorkItem -> m InteractResult
763 noInteraction workItem = mkIRContinue workItem KeepInert emptyCCan
765 data WhichComesFromInert = LeftComesFromInert | RightComesFromInert
767 ---------------------------------------------------
768 -- Interact a single WorkItem with an InertSet as far as possible, i.e. until we get a Stop
769 -- result from an individual interaction (i.e. when the WorkItem is consumed), or until we've
770 -- interacted the WorkItem with the entire InertSet.
772 -- Postcondition: the new InertSet in the resulting StageResult is subset
773 -- of the input InertSet.
775 interactWithInertsStage :: SimplifierStage
776 interactWithInertsStage workItem inert
777 = foldlInertSetM interactNext initITR inert
779 initITR = SR { sr_inerts = emptyInert
780 , sr_new_work = emptyCCan
781 , sr_stop = ContinueWith workItem }
784 interactNext :: StageResult -> AtomicInert -> TcS StageResult
785 interactNext it inert
786 | ContinueWith workItem <- sr_stop it
787 = do { ir <- interactWithInert inert workItem
788 ; let inerts = sr_inerts it
789 ; return $ SR { sr_inerts = if ir_inert_action ir == KeepInert
790 then inerts `updInertSet` inert
792 , sr_new_work = sr_new_work it `unionWorkLists` ir_new_work ir
793 , sr_stop = ir_stop ir } }
794 | otherwise = return $ itrAddInert inert it
797 itrAddInert :: AtomicInert -> StageResult -> StageResult
798 itrAddInert inert itr = itr { sr_inerts = (sr_inerts itr) `updInertSet` inert }
800 -- Do a single interaction of two constraints.
801 interactWithInert :: AtomicInert -> WorkItem -> TcS InteractResult
802 interactWithInert inert workitem
803 = do { ctxt <- getTcSContext
804 ; let is_allowed = allowedInteraction (simplEqsOnly ctxt) inert workitem
805 inert_ev = cc_id inert
806 work_ev = cc_id workitem
808 -- Never interact a wanted and a derived where the derived's evidence
809 -- mentions the wanted evidence in an unguarded way.
810 -- See Note [Superclasses and recursive dictionaries]
811 -- and Note [New Wanted Superclass Work]
812 -- We don't have to do this for givens, as we fully know the evidence for them.
814 case (cc_flavor inert, cc_flavor workitem) of
815 (Wanted loc, Derived _) -> isGoodRecEv work_ev (WantedEvVar inert_ev loc)
816 (Derived _, Wanted loc) -> isGoodRecEv inert_ev (WantedEvVar work_ev loc)
819 ; if is_allowed && rec_ev_ok then
820 doInteractWithInert inert workitem
822 noInteraction workitem
825 allowedInteraction :: Bool -> AtomicInert -> WorkItem -> Bool
826 -- Allowed interactions
827 allowedInteraction eqs_only (CDictCan {}) (CDictCan {}) = not eqs_only
828 allowedInteraction eqs_only (CIPCan {}) (CIPCan {}) = not eqs_only
829 allowedInteraction _ _ _ = True
831 --------------------------------------------
832 doInteractWithInert :: CanonicalCt -> CanonicalCt -> TcS InteractResult
833 -- Identical class constraints.
836 (CDictCan { cc_id = d1, cc_flavor = fl1, cc_class = cls1, cc_tyargs = tys1 })
837 workItem@(CDictCan { cc_id = d2, cc_flavor = fl2, cc_class = cls2, cc_tyargs = tys2 })
838 | cls1 == cls2 && (and $ zipWith tcEqType tys1 tys2)
839 = solveOneFromTheOther (d1,fl1) workItem
841 | cls1 == cls2 && (not (isGiven fl1 && isGiven fl2))
842 = -- See Note [When improvement happens]
843 do { let work_item_pred_loc = (ClassP cls2 tys2, ppr d2)
844 inert_pred_loc = (ClassP cls1 tys1, ppr d1)
845 loc = combineCtLoc fl1 fl2
846 eqn_pred_locs = improveFromAnother work_item_pred_loc inert_pred_loc
847 ; wevvars <- mkWantedFunDepEqns loc eqn_pred_locs
848 -- See Note [Generating extra equalities]
849 ; workList <- canWanteds wevvars
850 ; mkIRContinue workItem KeepInert workList -- Keep the inert there so we avoid
851 -- re-introducing the fundep equalities
852 -- See Note [FunDep Reactions]
855 -- Class constraint and given equality: use the equality to rewrite
856 -- the class constraint.
857 doInteractWithInert (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi })
858 (CDictCan { cc_id = dv, cc_flavor = wfl, cc_class = cl, cc_tyargs = xis })
859 | ifl `canRewrite` wfl
860 , tv `elemVarSet` tyVarsOfTypes xis
861 -- substitute for tv in xis. Note that the resulting class
862 -- constraint is still canonical, since substituting xi-types in
863 -- xi-types generates xi-types. However, it may no longer be
864 -- inert with respect to the inert set items we've already seen.
865 -- For example, consider the inert set
870 -- and the work item D a (w). D a does not interact with D Int.
871 -- Next, it does interact with a ~g Int, getting rewritten to D
872 -- Int (w). But now we must go back through the rest of the inert
873 -- set again, to find that it can now be discharged by the given D
875 = do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,wfl,cl,xis)
876 ; mkIRStop KeepInert (singleCCan rewritten_dict) }
878 doInteractWithInert (CDictCan { cc_id = dv, cc_flavor = ifl, cc_class = cl, cc_tyargs = xis })
879 workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
880 | wfl `canRewrite` ifl
881 , tv `elemVarSet` tyVarsOfTypes xis
882 = do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,ifl,cl,xis)
883 ; mkIRContinue workItem DropInert (singleCCan rewritten_dict) }
885 -- Class constraint and given equality: use the equality to rewrite
886 -- the class constraint.
887 doInteractWithInert (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi })
888 (CIPCan { cc_id = ipid, cc_flavor = wfl, cc_ip_nm = nm, cc_ip_ty = ty })
889 | ifl `canRewrite` wfl
890 , tv `elemVarSet` tyVarsOfType ty
891 = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,wfl,nm,ty)
892 ; mkIRStop KeepInert (singleCCan rewritten_ip) }
894 doInteractWithInert (CIPCan { cc_id = ipid, cc_flavor = ifl, cc_ip_nm = nm, cc_ip_ty = ty })
895 workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
896 | wfl `canRewrite` ifl
897 , tv `elemVarSet` tyVarsOfType ty
898 = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,ifl,nm,ty)
899 ; mkIRContinue workItem DropInert (singleCCan rewritten_ip) }
901 -- Two implicit parameter constraints. If the names are the same,
902 -- but their types are not, we generate a wanted type equality
903 -- that equates the type (this is "improvement").
904 -- However, we don't actually need the coercion evidence,
905 -- so we just generate a fresh coercion variable that isn't used anywhere.
906 doInteractWithInert (CIPCan { cc_id = id1, cc_flavor = ifl, cc_ip_nm = nm1, cc_ip_ty = ty1 })
907 workItem@(CIPCan { cc_flavor = wfl, cc_ip_nm = nm2, cc_ip_ty = ty2 })
908 | nm1 == nm2 && isGiven wfl && isGiven ifl
909 = -- See Note [Overriding implicit parameters]
910 -- Dump the inert item, override totally with the new one
911 -- Do not require type equality
912 mkIRContinue workItem DropInert emptyCCan
914 | nm1 == nm2 && ty1 `tcEqType` ty2
915 = solveOneFromTheOther (id1,ifl) workItem
918 = -- See Note [When improvement happens]
919 do { co_var <- newWantedCoVar ty1 ty2
920 ; let flav = Wanted (combineCtLoc ifl wfl)
921 ; mkCanonical flav co_var >>= mkIRContinue workItem KeepInert }
924 -- Inert: equality, work item: function equality
926 -- Never rewrite a given with a wanted equality, and a type function
927 -- equality can never rewrite an equality. Note also that if we have
928 -- F x1 ~ x2 and a ~ x3, and a occurs in x2, we don't rewrite it. We
929 -- can wait until F x1 ~ x2 matches another F x1 ~ x4, and only then
930 -- we will ``expose'' x2 and x4 to rewriting.
932 -- Otherwise, we can try rewriting the type function equality with the equality.
933 doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi1 })
934 (CFunEqCan { cc_id = cv2, cc_flavor = wfl, cc_fun = tc
935 , cc_tyargs = args, cc_rhs = xi2 })
936 | ifl `canRewrite` wfl
937 , tv `elemVarSet` tyVarsOfTypes args
938 = do { rewritten_funeq <- rewriteFunEq (cv1,tv,xi1) (cv2,wfl,tc,args,xi2)
939 ; mkIRStop KeepInert (singleCCan rewritten_funeq) }
941 -- Inert: function equality, work item: equality
943 doInteractWithInert (CFunEqCan {cc_id = cv1, cc_flavor = ifl, cc_fun = tc
944 , cc_tyargs = args, cc_rhs = xi1 })
945 workItem@(CTyEqCan { cc_id = cv2, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi2 })
946 | wfl `canRewrite` ifl
947 , tv `elemVarSet` tyVarsOfTypes args
948 = do { rewritten_funeq <- rewriteFunEq (cv2,tv,xi2) (cv1,ifl,tc,args,xi1)
949 ; mkIRContinue workItem DropInert (singleCCan rewritten_funeq) }
951 doInteractWithInert (CFunEqCan { cc_id = cv1, cc_flavor = fl1, cc_fun = tc1
952 , cc_tyargs = args1, cc_rhs = xi1 })
953 workItem@(CFunEqCan { cc_id = cv2, cc_flavor = fl2, cc_fun = tc2
954 , cc_tyargs = args2, cc_rhs = xi2 })
955 | fl1 `canRewrite` fl2 && lhss_match
956 = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
957 ; mkIRStop KeepInert cans }
958 | fl2 `canRewrite` fl1 && lhss_match
959 = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
960 ; mkIRContinue workItem DropInert cans }
962 lhss_match = tc1 == tc2 && and (zipWith tcEqType args1 args2)
965 inert@(CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
966 workItem@(CTyEqCan { cc_id = cv2, cc_flavor = fl2, cc_tyvar = tv2, cc_rhs = xi2 })
967 -- Check for matching LHS
968 | fl1 `canRewrite` fl2 && tv1 == tv2
969 = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
970 ; mkIRStop KeepInert cans }
972 | fl2 `canRewrite` fl1 && tv1 == tv2
973 = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
974 ; mkIRContinue workItem DropInert cans }
976 -- Check for rewriting RHS
977 | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfType xi2
978 = do { rewritten_eq <- rewriteEqRHS (cv1,tv1,xi1) (cv2,fl2,tv2,xi2)
979 ; mkIRStop KeepInert rewritten_eq }
980 | fl2 `canRewrite` fl1 && tv2 `elemVarSet` tyVarsOfType xi1
981 = do { rewritten_eq <- rewriteEqRHS (cv2,tv2,xi2) (cv1,fl1,tv1,xi1)
982 ; mkIRContinue workItem DropInert rewritten_eq }
984 -- Finally, if workitem is a Flatten Equivalence Class constraint and the
985 -- inert is a wanted constraint, even when the workitem cannot rewrite the
986 -- inert, drop the inert out because you may have to reconsider solving the
987 -- inert *using* the equivalence class you created. See note [Loopy Spontaneous Solving]
988 -- and [InertSet FlattenSkolemEqClass]
990 | not $ isGiven fl1, -- The inert is wanted or derived
991 isMetaTyVar tv1, -- and has a unification variable lhs
992 FlatSkol {} <- tcTyVarDetails tv2, -- And workitem is a flatten skolem equality
993 Just tv2' <- tcGetTyVar_maybe xi2, FlatSkol {} <- tcTyVarDetails tv2'
994 = mkIRContinue workItem DropInert (singletonWorkList inert)
997 -- Fall-through case for all other situations
998 doInteractWithInert _ workItem = noInteraction workItem
1000 --------------------------------------------
1001 combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
1002 -- Precondition: At least one of them should be wanted
1003 combineCtLoc (Wanted loc) _ = loc
1004 combineCtLoc _ (Wanted loc) = loc
1005 combineCtLoc _ _ = panic "Expected one of wanted constraints (BUG)"
1008 -- Equational Rewriting
1009 rewriteDict :: (CoVar, TcTyVar, Xi) -> (DictId, CtFlavor, Class, [Xi]) -> TcS CanonicalCt
1010 rewriteDict (cv,tv,xi) (dv,gw,cl,xis)
1011 = do { let cos = substTysWith [tv] [mkCoVarCoercion cv] xis -- xis[tv] ~ xis[xi]
1012 args = substTysWith [tv] [xi] xis
1014 dict_co = mkTyConCoercion con cos
1015 ; dv' <- newDictVar cl args
1017 Wanted {} -> setDictBind dv (EvCast dv' (mkSymCoercion dict_co))
1018 _given_or_derived -> setDictBind dv' (EvCast dv dict_co)
1019 ; return (CDictCan { cc_id = dv'
1022 , cc_tyargs = args }) }
1024 rewriteIP :: (CoVar,TcTyVar,Xi) -> (EvVar,CtFlavor, IPName Name, TcType) -> TcS CanonicalCt
1025 rewriteIP (cv,tv,xi) (ipid,gw,nm,ty)
1026 = do { let ip_co = substTyWith [tv] [mkCoVarCoercion cv] ty -- ty[tv] ~ t[xi]
1027 ty' = substTyWith [tv] [xi] ty
1028 ; ipid' <- newIPVar nm ty'
1030 Wanted {} -> setIPBind ipid (EvCast ipid' (mkSymCoercion ip_co))
1031 _given_or_derived -> setIPBind ipid' (EvCast ipid ip_co)
1032 ; return (CIPCan { cc_id = ipid'
1035 , cc_ip_ty = ty' }) }
1037 rewriteFunEq :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TyCon, [Xi], Xi) -> TcS CanonicalCt
1038 rewriteFunEq (cv1,tv,xi1) (cv2,gw, tc,args,xi2)
1039 = do { let arg_cos = substTysWith [tv] [mkCoVarCoercion cv1] args
1040 args' = substTysWith [tv] [xi1] args
1041 fun_co = mkTyConCoercion tc arg_cos
1042 ; cv2' <- case gw of
1043 Wanted {} -> do { cv2' <- newWantedCoVar (mkTyConApp tc args') xi2
1044 ; setWantedCoBind cv2 $
1045 mkTransCoercion fun_co (mkCoVarCoercion cv2')
1047 _giv_or_der -> newGivOrDerCoVar (mkTyConApp tc args') xi2 $
1048 mkTransCoercion (mkSymCoercion fun_co) (mkCoVarCoercion cv2)
1049 ; return (CFunEqCan { cc_id = cv2'
1056 rewriteEqRHS :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TcTyVar,Xi) -> TcS CanonicalCts
1057 -- Use the first equality to rewrite the second, flavors already checked.
1058 -- E.g. c1 : tv1 ~ xi1 c2 : tv2 ~ xi2
1059 -- rewrites c2 to give
1060 -- c2' : tv2 ~ xi2[xi1/tv1]
1061 -- We must do an occurs check to sure the new constraint is canonical
1062 -- So we might return an empty bag
1063 rewriteEqRHS (cv1,tv1,xi1) (cv2,gw,tv2,xi2)
1064 | Just tv2' <- tcGetTyVar_maybe xi2'
1065 , tv2 == tv2' -- In this case xi2[xi1/tv1] = tv2, so we have tv2~tv2
1066 = do { when (isWanted gw) (setWantedCoBind cv2 (mkSymCoercion co2'))
1067 ; return emptyCCan }
1072 -> do { cv2' <- newWantedCoVar (mkTyVarTy tv2) xi2'
1073 ; setWantedCoBind cv2 $
1074 mkCoVarCoercion cv2' `mkTransCoercion` mkSymCoercion co2'
1077 -> newGivOrDerCoVar (mkTyVarTy tv2) xi2' $
1078 mkCoVarCoercion cv2 `mkTransCoercion` co2'
1080 ; xi2'' <- canOccursCheck gw tv2 xi2' -- we know xi2' is *not* tv2
1081 ; return (singleCCan $ CTyEqCan { cc_id = cv2'
1087 xi2' = substTyWith [tv1] [xi1] xi2
1088 co2' = substTyWith [tv1] [mkCoVarCoercion cv1] xi2 -- xi2 ~ xi2[xi1/tv1]
1091 rewriteEqLHS :: WhichComesFromInert -> (Coercion,Xi) -> (CoVar,CtFlavor,Xi) -> TcS CanonicalCts
1092 -- Used to ineratct two equalities of the following form:
1093 -- First Equality: co1: (XXX ~ xi1)
1094 -- Second Equality: cv2: (XXX ~ xi2)
1095 -- Where the cv1 `canRewrite` cv2 equality
1096 -- We have an option of creating new work (xi1 ~ xi2) OR (xi2 ~ xi1). This
1097 -- depends on whether the left or the right equality comes from the inert set.
1099 -- prefer to create (xi2 ~ xi1) if the first comes from the inert
1100 -- prefer to create (xi1 ~ xi2) if the second comes from the inert
1101 rewriteEqLHS which (co1,xi1) (cv2,gw,xi2)
1102 = do { cv2' <- case (isWanted gw, which) of
1103 (True,LeftComesFromInert) ->
1104 do { cv2' <- newWantedCoVar xi2 xi1
1105 ; setWantedCoBind cv2 $
1106 co1 `mkTransCoercion` mkSymCoercion (mkCoVarCoercion cv2')
1108 (True,RightComesFromInert) ->
1109 do { cv2' <- newWantedCoVar xi1 xi2
1110 ; setWantedCoBind cv2 $
1111 co1 `mkTransCoercion` mkCoVarCoercion cv2'
1113 (False,LeftComesFromInert) ->
1114 newGivOrDerCoVar xi2 xi1 $
1115 mkSymCoercion (mkCoVarCoercion cv2) `mkTransCoercion` co1
1116 (False,RightComesFromInert) ->
1117 newGivOrDerCoVar xi1 xi2 $
1118 mkSymCoercion co1 `mkTransCoercion` mkCoVarCoercion cv2
1119 ; mkCanonical gw cv2' }
1123 solveOneFromTheOther :: (EvVar, CtFlavor) -> CanonicalCt -> TcS InteractResult
1124 -- First argument inert, second argument workitem. They both represent
1125 -- wanted/given/derived evidence for the *same* predicate so we try here to
1126 -- discharge one directly from the other.
1128 -- Precondition: value evidence only (implicit parameters, classes)
1130 solveOneFromTheOther (iid,ifl) workItem
1131 -- Both derived needs a special case. You might think that we do not need
1132 -- two evidence terms for the same claim. But, since the evidence is partial,
1133 -- either evidence may do in some cases; see TcSMonad.isGoodRecEv.
1134 -- See also Example 3 in Note [Superclasses and recursive dictionaries]
1135 | isDerived ifl && isDerived wfl
1136 = noInteraction workItem
1138 | ifl `canRewrite` wfl
1139 = do { unless (isGiven wfl) $ setEvBind wid (EvId iid)
1140 -- Overwrite the binding, if one exists
1141 -- For Givens, which are lambda-bound, nothing to overwrite,
1142 ; dischargeWorkItem }
1144 | otherwise -- wfl `canRewrite` ifl
1145 = do { unless (isGiven ifl) $ setEvBind iid (EvId wid)
1146 ; mkIRContinue workItem DropInert emptyCCan }
1149 wfl = cc_flavor workItem
1150 wid = cc_id workItem
1153 Note [Superclasses and recursive dictionaries]
1154 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1155 Overlaps with Note [SUPERCLASS-LOOP 1]
1156 Note [SUPERCLASS-LOOP 2]
1157 Note [Recursive instances and superclases]
1158 ToDo: check overlap and delete redundant stuff
1160 Right before adding a given into the inert set, we must
1161 produce some more work, that will bring the superclasses
1162 of the given into scope. The superclass constraints go into
1165 When we simplify a wanted constraint, if we first see a matching
1166 instance, we may produce new wanted work. To (1) avoid doing this work
1167 twice in the future and (2) to handle recursive dictionaries we may ``cache''
1168 this item as solved (in effect, given) into our inert set and with that add
1169 its superclass constraints (as given) in our worklist.
1171 But now we have added partially solved constraints to the worklist which may
1172 interact with other wanteds. Consider the example:
1176 class Eq b => Foo a b --- 0-th selector
1177 instance Eq a => Foo [a] a --- fooDFun
1179 and wanted (Foo [t] t). We are first going to see that the instance matches
1180 and create an inert set that includes the solved (Foo [t] t) and its
1182 d1 :_g Foo [t] t d1 := EvDFunApp fooDFun d3
1183 d2 :_g Eq t d2 := EvSuperClass d1 0
1184 Our work list is going to contain a new *wanted* goal
1186 It is wrong to react the wanted (Eq t) with the given (Eq t) because that would
1187 construct loopy evidence. Hence the check isGoodRecEv in doInteractWithInert.
1189 OK, so we have ruled out bad behaviour, but how do we ge recursive dictionaries,
1194 data D r = ZeroD | SuccD (r (D r));
1196 instance (Eq (r (D r))) => Eq (D r) where
1197 ZeroD == ZeroD = True
1198 (SuccD a) == (SuccD b) = a == b
1201 equalDC :: D [] -> D [] -> Bool;
1204 We need to prove (Eq (D [])). Here's how we go:
1208 by instance decl, holds if
1212 *BUT* we have an inert set which gives us (no superclasses):
1214 By the instance declaration of Eq we can show the 'd2' goal if
1216 where d2 = dfEqList d3
1218 Now, however this wanted can interact with our inert d1 to set:
1220 and solve the goal. Why was this interaction OK? Because, if we chase the
1221 evidence of d1 ~~> dfEqD d2 ~~-> dfEqList d3, so by setting d3 := d1 we
1223 d3 := dfEqD2 (dfEqList d3)
1224 which is FINE because the use of d3 is protected by the instance function
1227 So, our strategy is to try to put solved wanted dictionaries into the
1228 inert set along with their superclasses (when this is meaningful,
1229 i.e. when new wanted goals are generated) but solve a wanted dictionary
1230 from a given only in the case where the evidence variable of the
1231 wanted is mentioned in the evidence of the given (recursively through
1232 the evidence binds) in a protected way: more instance function applications
1233 than superclass selectors.
1235 Here are some more examples from GHC's previous type checker
1239 This code arises in the context of "Scrap Your Boilerplate with Class"
1243 instance Sat (ctx Char) => Data ctx Char -- dfunData1
1244 instance (Sat (ctx [a]), Data ctx a) => Data ctx [a] -- dfunData2
1246 class Data Maybe a => Foo a
1248 instance Foo t => Sat (Maybe t) -- dfunSat
1250 instance Data Maybe a => Foo a -- dfunFoo1
1251 instance Foo a => Foo [a] -- dfunFoo2
1252 instance Foo [Char] -- dfunFoo3
1254 Consider generating the superclasses of the instance declaration
1255 instance Foo a => Foo [a]
1257 So our problem is this
1259 d1 :_w Data Maybe [t]
1261 We may add the given in the inert set, along with its superclasses
1262 [assuming we don't fail because there is a matching instance, see
1263 tryTopReact, given case ]
1267 d01 :_g Data Maybe t -- d2 := EvDictSuperClass d0 0
1268 d1 :_w Data Maybe [t]
1269 Then d2 can readily enter the inert, and we also do solving of the wanted
1272 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1274 d2 :_w Sat (Maybe [t])
1276 d01 :_g Data Maybe t
1277 Now, we may simplify d2 more:
1280 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1281 d1 :_g Data Maybe [t]
1282 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1286 d01 :_g Data Maybe t
1288 Now, we can just solve d3.
1291 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1292 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1295 d01 :_g Data Maybe t
1296 And now we can simplify d4 again, but since it has superclasses we *add* them to the worklist:
1299 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1300 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1301 d4 :_g Foo [t] d4 := dfunFoo2 d5
1304 d6 :_g Data Maybe [t] d6 := EvDictSuperClass d4 0
1305 d01 :_g Data Maybe t
1306 Now, d5 can be solved! (and its superclass enter scope)
1309 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1310 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1311 d4 :_g Foo [t] d4 := dfunFoo2 d5
1312 d5 :_g Foo t d5 := dfunFoo1 d7
1315 d6 :_g Data Maybe [t]
1316 d8 :_g Data Maybe t d8 := EvDictSuperClass d5 0
1317 d01 :_g Data Maybe t
1320 [1] Suppose we pick d8 and we react him with d01. Which of the two givens should
1321 we keep? Well, we *MUST NOT* drop d01 because d8 contains recursive evidence
1322 that must not be used (look at case interactInert where both inert and workitem
1323 are givens). So we have several options:
1324 - Drop the workitem always (this will drop d8)
1325 This feels very unsafe -- what if the work item was the "good" one
1326 that should be used later to solve another wanted?
1327 - Don't drop anyone: the inert set may contain multiple givens!
1328 [This is currently implemented]
1330 The "don't drop anyone" seems the most safe thing to do, so now we come to problem 2:
1331 [2] We have added both d6 and d01 in the inert set, and we are interacting our wanted
1332 d7. Now the [isRecDictEv] function in the ineration solver
1333 [case inert-given workitem-wanted] will prevent us from interacting d7 := d8
1334 precisely because chasing the evidence of d8 leads us to an unguarded use of d7.
1336 So, no interaction happens there. Then we meet d01 and there is no recursion
1337 problem there [isRectDictEv] gives us the OK to interact and we do solve d7 := d01!
1339 Note [SUPERCLASS-LOOP 1]
1340 ~~~~~~~~~~~~~~~~~~~~~~~~
1341 We have to be very, very careful when generating superclasses, lest we
1342 accidentally build a loop. Here's an example:
1346 class S a => C a where { opc :: a -> a }
1347 class S b => D b where { opd :: b -> b }
1349 instance C Int where
1352 instance D Int where
1355 From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int}
1356 Simplifying, we may well get:
1357 $dfCInt = :C ds1 (opd dd)
1360 Notice that we spot that we can extract ds1 from dd.
1362 Alas! Alack! We can do the same for (instance D Int):
1364 $dfDInt = :D ds2 (opc dc)
1368 And now we've defined the superclass in terms of itself.
1369 Two more nasty cases are in
1374 - Satisfy the superclass context *all by itself*
1375 (tcSimplifySuperClasses)
1376 - And do so completely; i.e. no left-over constraints
1377 to mix with the constraints arising from method declarations
1380 Note [SUPERCLASS-LOOP 2]
1381 ~~~~~~~~~~~~~~~~~~~~~~~~
1382 We need to be careful when adding "the constaint we are trying to prove".
1383 Suppose we are *given* d1:Ord a, and want to deduce (d2:C [a]) where
1385 class Ord a => C a where
1386 instance Ord [a] => C [a] where ...
1388 Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the
1389 superclasses of C [a] to avails. But we must not overwrite the binding
1390 for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
1393 Here's another variant, immortalised in tcrun020
1394 class Monad m => C1 m
1395 class C1 m => C2 m x
1396 instance C2 Maybe Bool
1397 For the instance decl we need to build (C1 Maybe), and it's no good if
1398 we run around and add (C2 Maybe Bool) and its superclasses to the avails
1399 before we search for C1 Maybe.
1401 Here's another example
1402 class Eq b => Foo a b
1403 instance Eq a => Foo [a] a
1407 we'll first deduce that it holds (via the instance decl). We must not
1408 then overwrite the Eq t constraint with a superclass selection!
1410 At first I had a gross hack, whereby I simply did not add superclass constraints
1411 in addWanted, though I did for addGiven and addIrred. This was sub-optimal,
1412 becuase it lost legitimate superclass sharing, and it still didn't do the job:
1413 I found a very obscure program (now tcrun021) in which improvement meant the
1414 simplifier got two bites a the cherry... so something seemed to be an Stop
1415 first time, but reducible next time.
1417 Now we implement the Right Solution, which is to check for loops directly
1418 when adding superclasses. It's a bit like the occurs check in unification.
1420 Note [Recursive instances and superclases]
1421 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1422 Consider this code, which arises in the context of "Scrap Your
1423 Boilerplate with Class".
1427 instance Sat (ctx Char) => Data ctx Char
1428 instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]
1430 class Data Maybe a => Foo a
1432 instance Foo t => Sat (Maybe t)
1434 instance Data Maybe a => Foo a
1435 instance Foo a => Foo [a]
1438 In the instance for Foo [a], when generating evidence for the superclasses
1439 (ie in tcSimplifySuperClasses) we need a superclass (Data Maybe [a]).
1440 Using the instance for Data, we therefore need
1441 (Sat (Maybe [a], Data Maybe a)
1442 But we are given (Foo a), and hence its superclass (Data Maybe a).
1443 So that leaves (Sat (Maybe [a])). Using the instance for Sat means
1444 we need (Foo [a]). And that is the very dictionary we are bulding
1445 an instance for! So we must put that in the "givens". So in this
1447 Given: Foo a, Foo [a]
1448 Wanted: Data Maybe [a]
1450 BUT we must *not not not* put the *superclasses* of (Foo [a]) in
1451 the givens, which is what 'addGiven' would normally do. Why? Because
1452 (Data Maybe [a]) is the superclass, so we'd "satisfy" the wanted
1453 by selecting a superclass from Foo [a], which simply makes a loop.
1455 On the other hand we *must* put the superclasses of (Foo a) in
1456 the givens, as you can see from the derivation described above.
1458 Conclusion: in the very special case of tcSimplifySuperClasses
1459 we have one 'given' (namely the "this" dictionary) whose superclasses
1460 must not be added to 'givens' by addGiven.
1462 There is a complication though. Suppose there are equalities
1463 instance (Eq a, a~b) => Num (a,b)
1464 Then we normalise the 'givens' wrt the equalities, so the original
1465 given "this" dictionary is cast to one of a different type. So it's a
1466 bit trickier than before to identify the "special" dictionary whose
1467 superclasses must not be added. See test
1468 indexed-types/should_run/EqInInstance
1470 We need a persistent property of the dictionary to record this
1471 special-ness. Current I'm using the InstLocOrigin (a bit of a hack,
1472 but cool), which is maintained by dictionary normalisation.
1473 Specifically, the InstLocOrigin is
1475 then the no-superclass thing kicks in. WATCH OUT if you fiddle
1478 Note [MATCHING-SYNONYMS]
1479 ~~~~~~~~~~~~~~~~~~~~~~~~
1480 When trying to match a dictionary (D tau) to a top-level instance, or a
1481 type family equation (F taus_1 ~ tau_2) to a top-level family instance,
1482 we do *not* need to expand type synonyms because the matcher will do that for us.
1485 Note [RHS-FAMILY-SYNONYMS]
1486 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1487 The RHS of a family instance is represented as yet another constructor which is
1488 like a type synonym for the real RHS the programmer declared. Eg:
1489 type instance F (a,a) = [a]
1491 :R32 a = [a] -- internal type synonym introduced
1492 F (a,a) ~ :R32 a -- instance
1494 When we react a family instance with a type family equation in the work list
1495 we keep the synonym-using RHS without expansion.
1498 *********************************************************************************
1500 The top-reaction Stage
1502 *********************************************************************************
1505 -- If a work item has any form of interaction with top-level we get this
1506 data TopInteractResult
1507 = NoTopInt -- No top-level interaction
1509 { tir_new_work :: WorkList -- Sub-goals or new work (could be given,
1510 -- for superclasses)
1511 , tir_new_inert :: StopOrContinue -- The input work item, ready to become *inert* now:
1512 } -- NB: in ``given'' (solved) form if the
1513 -- original was wanted or given and instance match
1514 -- was found, but may also be in wanted form if we
1515 -- only reacted with functional dependencies
1516 -- arising from top-level instances.
1518 topReactionsStage :: SimplifierStage
1519 topReactionsStage workItem inerts
1520 = do { tir <- tryTopReact workItem
1523 return $ SR { sr_inerts = inerts
1524 , sr_new_work = emptyWorkList
1525 , sr_stop = ContinueWith workItem }
1526 SomeTopInt tir_new_work tir_new_inert ->
1527 return $ SR { sr_inerts = inerts
1528 , sr_new_work = tir_new_work
1529 , sr_stop = tir_new_inert
1533 tryTopReact :: WorkItem -> TcS TopInteractResult
1534 tryTopReact workitem
1535 = do { -- A flag controls the amount of interaction allowed
1536 -- See Note [Simplifying RULE lhs constraints]
1537 ctxt <- getTcSContext
1538 ; if allowedTopReaction (simplEqsOnly ctxt) workitem
1539 then do { traceTcS "tryTopReact / calling doTopReact" (ppr workitem)
1540 ; doTopReact workitem }
1541 else return NoTopInt
1544 allowedTopReaction :: Bool -> WorkItem -> Bool
1545 allowedTopReaction eqs_only (CDictCan {}) = not eqs_only
1546 allowedTopReaction _ _ = True
1549 doTopReact :: WorkItem -> TcS TopInteractResult
1550 -- The work item does not react with the inert set,
1551 -- so try interaction with top-level instances
1552 doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Wanted loc
1553 , cc_class = cls, cc_tyargs = xis })
1554 = do { -- See Note [MATCHING-SYNONYMS]
1555 ; lkp_inst_res <- matchClassInst cls xis loc
1556 ; case lkp_inst_res of
1557 NoInstance -> do { traceTcS "doTopReact/ no class instance for" (ppr dv)
1559 GenInst wtvs ev_term -> -- Solved
1560 -- No need to do fundeps stuff here; the instance
1561 -- matches already so we won't get any more info
1562 -- from functional dependencies
1563 do { traceTcS "doTopReact/ found class instance for" (ppr dv)
1564 ; setDictBind dv ev_term
1565 ; workList <- canWanteds wtvs
1567 -- Solved in one step and no new wanted work produced.
1568 -- i.e we directly matched a top-level instance
1569 -- No point in caching this in 'inert', nor in adding superclasses
1570 then return $ SomeTopInt { tir_new_work = emptyCCan
1571 , tir_new_inert = Stop }
1573 -- Solved and new wanted work produced, you may cache the
1574 -- (tentatively solved) dictionary as Derived and its superclasses
1575 else do { let solved = makeSolved workItem
1576 ; sc_work <- newSCWorkFromFlavored dv (Derived loc) cls xis
1577 ; return $ SomeTopInt
1578 { tir_new_work = workList `unionWorkLists` sc_work
1579 , tir_new_inert = ContinueWith solved } }
1583 -- Try for a fundep reaction beween the wanted item
1584 -- and a top-level instance declaration
1586 = do { instEnvs <- getInstEnvs
1587 ; let eqn_pred_locs = improveFromInstEnv (classInstances instEnvs)
1588 (ClassP cls xis, ppr dv)
1589 ; wevvars <- mkWantedFunDepEqns loc eqn_pred_locs
1590 -- NB: fundeps generate some wanted equalities, but
1591 -- we don't use their evidence for anything
1592 ; fd_work <- canWanteds wevvars
1593 ; sc_work <- newSCWorkFromFlavored dv (Derived loc) cls xis
1594 ; return $ SomeTopInt { tir_new_work = fd_work `unionWorkLists` sc_work
1595 , tir_new_inert = ContinueWith workItem }
1596 -- NB: workItem is inert, but it isn't solved
1597 -- keep it as inert, although it's not solved because we
1598 -- have now reacted all its top-level fundep-induced equalities!
1600 -- See Note [FunDep Reactions]
1603 -- Otherwise, we have a given or derived
1604 doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = fl
1605 , cc_class = cls, cc_tyargs = xis })
1606 = do { sc_work <- newSCWorkFromFlavored dv fl cls xis
1607 ; return $ SomeTopInt sc_work (ContinueWith workItem) }
1608 -- See Note [Given constraint that matches an instance declaration]
1611 doTopReact (CFunEqCan { cc_id = cv, cc_flavor = fl
1612 , cc_fun = tc, cc_tyargs = args, cc_rhs = xi })
1613 = ASSERT (isSynFamilyTyCon tc) -- No associated data families have reached that far
1614 do { match_res <- matchFam tc args -- See Note [MATCHING-SYNONYMS]
1618 MatchInstSingle (rep_tc, rep_tys)
1619 -> do { let Just coe_tc = tyConFamilyCoercion_maybe rep_tc
1620 Just rhs_ty = tcView (mkTyConApp rep_tc rep_tys)
1621 -- Eagerly expand away the type synonym on the
1622 -- RHS of a type function, so that it never
1623 -- appears in an error message
1624 -- See Note [Type synonym families] in TyCon
1625 coe = mkTyConApp coe_tc rep_tys
1627 Wanted {} -> do { cv' <- newWantedCoVar rhs_ty xi
1628 ; setWantedCoBind cv $
1629 coe `mkTransCoercion`
1632 _ -> newGivOrDerCoVar xi rhs_ty $
1633 mkSymCoercion (mkCoVarCoercion cv) `mkTransCoercion` coe
1635 ; workList <- mkCanonical fl cv'
1636 ; return $ SomeTopInt workList Stop }
1638 -> panicTcS $ text "TcSMonad.matchFam returned multiple instances!"
1642 -- Any other work item does not react with any top-level equations
1643 doTopReact _workItem = return NoTopInt
1646 Note [FunDep and implicit parameter reactions]
1647 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1648 Currently, our story of interacting two dictionaries (or a dictionary
1649 and top-level instances) for functional dependencies, and implicit
1650 paramters, is that we simply produce new wanted equalities. So for example
1652 class D a b | a -> b where ...
1658 We generate the extra work item
1660 where 'cv' is currently unused. However, this new item reacts with d2,
1661 discharging it in favour of a new constraint d2' thus:
1663 d2 := d2' |> D Int cv
1664 Now d2' can be discharged from d1
1666 We could be more aggressive and try to *immediately* solve the dictionary
1667 using those extra equalities. With the same inert set and work item we
1668 might dischard d2 directly:
1671 d2 := d1 |> D Int cv
1673 But in general it's a bit painful to figure out the necessary coercion,
1674 so we just take the first approach.
1676 It's exactly the same with implicit parameters, except that the
1677 "aggressive" approach would be much easier to implement.
1679 Note [When improvement happens]
1680 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1681 We fire an improvement rule when
1683 * Two constraints match (modulo the fundep)
1684 e.g. C t1 t2, C t1 t3 where C a b | a->b
1685 The two match because the first arg is identical
1687 * At least one is not Given. If they are both given, we don't fire
1688 the reaction because we have no way of constructing evidence for a
1689 new equality nor does it seem right to create a new wanted goal
1690 (because the goal will most likely contain untouchables, which
1691 can't be solved anyway)!
1693 Note that we *do* fire the improvement if one is Given and one is Derived.
1694 The latter can be a superclass of a wanted goal. Example (tcfail138)
1695 class L a b | a -> b
1696 class (G a, L a b) => C a b
1698 instance C a b' => G (Maybe a)
1699 instance C a b => C (Maybe a) a
1700 instance L (Maybe a) a
1702 When solving the superclasses of the (C (Maybe a) a) instance, we get
1703 Given: C a b ... and hance by superclasses, (G a, L a b)
1705 Use the instance decl to get
1707 The (C a b') is inert, so we generate its Derived superclasses (L a b'),
1708 and now we need improvement between that derived superclass an the Given (L a b)
1710 Note [Overriding implicit parameters]
1711 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1713 f :: (?x::a) -> Bool -> a
1715 g v = let ?x::Int = 3
1716 in (f v, let ?x::Bool = True in f v)
1718 This should probably be well typed, with
1719 g :: Bool -> (Int, Bool)
1721 So the inner binding for ?x::Bool *overrides* the outer one.
1722 Hence a work-item Given overrides an inert-item Given.
1724 Note [Given constraint that matches an instance declaration]
1725 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1726 What should we do when we discover that one (or more) top-level
1727 instances match a given (or solved) class constraint? We have
1730 1. Reject the program. The reason is that there may not be a unique
1731 best strategy for the solver. Example, from the OutsideIn(X) paper:
1732 instance P x => Q [x]
1733 instance (x ~ y) => R [x] y
1735 wob :: forall a b. (Q [b], R b a) => a -> Int
1737 g :: forall a. Q [a] => [a] -> Int
1740 will generate the impliation constraint:
1741 Q [a] => (Q [beta], R beta [a])
1742 If we react (Q [beta]) with its top-level axiom, we end up with a
1743 (P beta), which we have no way of discharging. On the other hand,
1744 if we react R beta [a] with the top-level we get (beta ~ a), which
1745 is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
1746 now solvable by the given Q [a].
1748 However, this option is restrictive, for instance [Example 3] from
1749 Note [Recursive dictionaries] will fail to work.
1751 2. Ignore the problem, hoping that the situations where there exist indeed
1752 such multiple strategies are rare: Indeed the cause of the previous
1753 problem is that (R [x] y) yields the new work (x ~ y) which can be
1754 *spontaneously* solved, not using the givens.
1756 We are choosing option 2 below but we might consider having a flag as well.
1759 Note [New Wanted Superclass Work]
1760 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1761 Even in the case of wanted constraints, we add all of its superclasses as
1762 new given work. There are several reasons for this:
1763 a) to minimise error messages;
1764 eg suppose we have wanted (Eq a, Ord a)
1765 then we report only (Ord a) unsoluble
1767 b) to make the smallest number of constraints when *inferring* a type
1768 (same Eq/Ord example)
1770 c) for recursive dictionaries we *must* add the superclasses
1771 so that we can use them when solving a sub-problem
1773 d) To allow FD-like improvement for type families. Assume that
1775 class C a b | a -> b
1776 and we have to solve the implication constraint:
1778 Then, FD improvement can help us to produce a new wanted (beta ~ b)
1780 We want to have the same effect with the type family encoding of
1781 functional dependencies. Namely, consider:
1782 class (F a ~ b) => C a b
1783 Now suppose that we have:
1786 By interacting the given we will get that (F a ~ b) which is not
1787 enough by itself to make us discharge (C a beta). However, we
1788 may create a new given equality from the super-class that we promise
1789 to solve: (F a ~ beta). Now we may interact this with the rest of
1790 constraint to finally get:
1793 But 'beta' is a touchable unification variable, and hence OK to
1794 unify it with 'b', replacing the given evidence with the identity.
1796 This requires trySpontaneousSolve to solve given equalities that
1797 have a touchable in their RHS, *in addition* to solving wanted
1800 Here is another example where this is useful.
1804 class (F a ~ b) => C a b
1805 And we are given the wanteds:
1809 We surely do *not* want to quantify over (b ~ c), since if someone provides
1810 dictionaries for (C a b) and (C a c), these dictionaries can provide a proof
1811 of (b ~ c), hence no extra evidence is necessary. Here is what will happen:
1813 Step 1: We will get new *given* superclass work,
1814 provisionally to our solving of w1 and w2
1816 g1: F a ~ b, g2 : F a ~ c,
1817 w1 : C a b, w2 : C a c, w3 : b ~ c
1819 The evidence for g1 and g2 is a superclass evidence term:
1821 g1 := sc w1, g2 := sc w2
1823 Step 2: The givens will solve the wanted w3, so that
1824 w3 := sym (sc w1) ; sc w2
1826 Step 3: Now, one may naively assume that then w2 can be solve from w1
1827 after rewriting with the (now solved equality) (b ~ c).
1829 But this rewriting is ruled out by the isGoodRectDict!
1831 Conclusion, we will (correctly) end up with the unsolved goals
1834 NB: The desugarer needs be more clever to deal with equalities
1835 that participate in recursive dictionary bindings.
1838 newSCWorkFromFlavored :: EvVar -> CtFlavor -> Class -> [Xi]
1840 newSCWorkFromFlavored ev flavor cls xis
1841 | Given loc <- flavor -- The NoScSkol says "don't add superclasses"
1842 , NoScSkol <- ctLocOrigin loc -- Very important!
1843 = return emptyWorkList
1846 = do { let (tyvars, sc_theta, _, _) = classBigSig cls
1847 sc_theta1 = substTheta (zipTopTvSubst tyvars xis) sc_theta
1848 -- Add *all* its superclasses (equalities or not) as new given work
1849 -- See Note [New Wanted Superclass Work]
1850 ; sc_vars <- zipWithM inst_one sc_theta1 [0..]
1851 ; mkCanonicals flavor sc_vars }
1853 inst_one pred n = newGivOrDerEvVar pred (EvSuperClass ev n)
1855 data LookupInstResult
1857 | GenInst [WantedEvVar] EvTerm
1859 matchClassInst :: Class -> [Type] -> WantedLoc -> TcS LookupInstResult
1860 matchClassInst clas tys loc
1861 = do { let pred = mkClassPred clas tys
1862 ; mb_result <- matchClass clas tys
1864 MatchInstNo -> return NoInstance
1865 MatchInstMany -> return NoInstance -- defer any reactions of a multitude until
1866 -- we learn more about the reagent
1867 MatchInstSingle (dfun_id, mb_inst_tys) ->
1868 do { checkWellStagedDFun pred dfun_id loc
1870 -- It's possible that not all the tyvars are in
1871 -- the substitution, tenv. For example:
1872 -- instance C X a => D X where ...
1873 -- (presumably there's a functional dependency in class C)
1874 -- Hence mb_inst_tys :: Either TyVar TcType
1876 ; tys <- instDFunTypes mb_inst_tys
1877 ; let (theta, _) = tcSplitPhiTy (applyTys (idType dfun_id) tys)
1878 ; if null theta then
1879 return (GenInst [] (EvDFunApp dfun_id tys []))
1881 { ev_vars <- instDFunConstraints theta
1882 ; let wevs = [WantedEvVar w loc | w <- ev_vars]
1883 ; return $ GenInst wevs (EvDFunApp dfun_id tys ev_vars) }