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 Wanted or Derived
608 -- See [New Wanted Superclass Work] to see why solveWithIdentity
609 -- must work for Derived as well as Wanted
610 solveWithIdentity inerts cv gw tv xi
611 = do { tybnds <- getTcSTyBindsBag
612 ; case occurCheck tybnds inerts tv xi of
613 Nothing -> return Nothing
614 Just (xi_unflat,coi) -> solve_with xi_unflat coi }
616 solve_with xi_unflat coi -- coi : xi_unflat ~ xi
617 = do { traceTcS "Sneaky unification:" $
618 vcat [text "Coercion variable: " <+> ppr gw,
619 text "Coercion: " <+> pprEq (mkTyVarTy tv) xi,
620 text "Left Kind is : " <+> ppr (typeKind (mkTyVarTy tv)),
621 text "Right Kind is : " <+> ppr (typeKind xi)
623 ; setWantedTyBind tv xi_unflat -- Set tv := xi_unflat
624 ; cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi_unflat xi_unflat
625 ; let flav = mkGivenFlavor gw UnkSkol
626 ; (cts, co) <- case coi of
627 ACo co -> do { can_eqs <- canEq flav cv_given (mkTyVarTy tv) xi_unflat
628 ; return (can_eqs, co) }
630 (singleCCan (CTyEqCan { cc_id = cv_given
631 , cc_flavor = mkGivenFlavor gw UnkSkol
632 , cc_tyvar = tv, cc_rhs = xi }
633 -- xi, *not* xi_unflat because
634 -- xi_unflat may require flattening!
637 Wanted {} -> setWantedCoBind cv co
638 Derived {} -> setDerivedCoBind cv co
639 _ -> pprPanic "Can't spontaneously solve *given*" empty
640 -- See Note [Avoid double unifications]
641 ; return (Just cts) }
643 occurCheck :: Bag (TcTyVar, TcType) -> InertSet
644 -> TcTyVar -> TcType -> Maybe (TcType,CoercionI)
645 -- Traverse @ty@ to make sure that @tv@ does not appear under some flatten skolem.
646 -- If it appears under some flatten skolem look in that flatten skolem equivalence class
647 -- (see Note [InertSet FlattenSkolemEqClass], [Loopy Spontaneous Solving]) to see if you
648 -- can find a different flatten skolem to use, that is, one that does not mention @tv@.
650 -- Postcondition: Just (ty', coi) = occurCheck binds inerts tv ty
652 -- NB: The returned type ty' may not be flat!
654 occurCheck ty_binds_bag inerts tv ty
657 -- If (fsk `elem` bad) then tv occurs in any rendering
658 -- of the type under the expansion of fsk
659 ok bad this_ty@(TyConApp tc tys)
660 | Just tys_cois <- allMaybes (map (ok bad) tys)
661 , (tys',cois') <- unzip tys_cois
662 = Just (TyConApp tc tys', mkTyConAppCoI tc cois')
663 | isSynTyCon tc, Just ty_expanded <- tcView this_ty
664 = ok bad ty_expanded -- See Note [Type synonyms and the occur check] in TcUnify
666 | Just (sty',coi) <- ok_pred bad sty
667 = Just (PredTy sty', coi)
668 ok bad (FunTy arg res)
669 | Just (arg', coiarg) <- ok bad arg, Just (res', coires) <- ok bad res
670 = Just (FunTy arg' res', mkFunTyCoI coiarg coires)
671 ok bad (AppTy fun arg)
672 | Just (fun', coifun) <- ok bad fun, Just (arg', coiarg) <- ok bad arg
673 = Just (AppTy fun' arg', mkAppTyCoI coifun coiarg)
674 ok bad (ForAllTy tv1 ty1)
675 -- WARNING: What if it is a (t1 ~ t2) => t3? It's not handled properly at the moment.
676 | Just (ty1', coi) <- ok bad ty1
677 = Just (ForAllTy tv1 ty1', mkForAllTyCoI tv1 coi)
680 ok _bad this_ty@(TyVarTy tv')
681 | not $ isTcTyVar tv' = Just (this_ty, IdCo this_ty) -- Bound variable
682 | tv == tv' = Nothing -- Occurs check error
685 | FlatSkol zty <- tcTyVarDetails fsk
686 = if fsk `elemVarSet` bad then
687 -- its type has been checked
688 go_down_eq_class bad $ getFskEqClass inerts fsk
690 -- its type is not yet checked
692 Nothing -> go_down_eq_class (bad `extendVarSet` fsk) $
693 getFskEqClass inerts fsk
694 Just (zty',ico) -> Just (zty',ico)
696 -- Check if there exists a ty bind already, as a result of sneaky unification.
697 ok bad this_ty@(TyVarTy tv0)
698 = case Bag.foldlBag find_bind Nothing ty_binds_bag of
699 Nothing -> Just (this_ty, IdCo this_ty)
700 Just ty0 -> ok bad ty0
701 where find_bind Nothing (tvx,tyx) | tv0 == tvx = Just tyx
704 ok _bad _ty = Nothing
706 ok_pred bad (ClassP cn tys)
707 | Just tys_cois <- allMaybes $ map (ok bad) tys
708 = let (tys', cois') = unzip tys_cois
709 in Just (ClassP cn tys', mkClassPPredCoI cn cois')
710 ok_pred bad (IParam nm ty)
711 | Just (ty',co') <- ok bad ty
712 = Just (IParam nm ty', mkIParamPredCoI nm co')
713 ok_pred bad (EqPred ty1 ty2)
714 | Just (ty1',coi1) <- ok bad ty1, Just (ty2',coi2) <- ok bad ty2
715 = Just (EqPred ty1' ty2', mkEqPredCoI coi1 coi2)
716 ok_pred _ _ = Nothing
718 go_down_eq_class _bad_tvs [] = Nothing
719 go_down_eq_class bad_tvs ((fsk1,co1):rest)
720 | fsk1 `elemVarSet` bad_tvs = go_down_eq_class bad_tvs rest
722 = case ok bad_tvs (TyVarTy fsk1) of
723 Nothing -> go_down_eq_class (bad_tvs `extendVarSet` fsk1) rest
724 Just (ty1,co1i') -> Just (ty1, mkTransCoI co1i' (ACo co1))
728 *********************************************************************************
730 The interact-with-inert Stage
732 *********************************************************************************
735 -- Interaction result of WorkItem <~> AtomicInert
737 = IR { ir_stop :: StopOrContinue
739 -- => Reagent (work item) consumed.
740 -- ContinueWith new_reagent
741 -- => Reagent transformed but keep gathering interactions.
742 -- The transformed item remains inert with respect
743 -- to any previously encountered inerts.
745 , ir_inert_action :: InertAction
746 -- Whether the inert item should remain in the InertSet.
748 , ir_new_work :: WorkList
749 -- new work items to add to the WorkList
752 -- What to do with the inert reactant.
753 data InertAction = KeepInert | DropInert
756 mkIRContinue :: Monad m => WorkItem -> InertAction -> WorkList -> m InteractResult
757 mkIRContinue wi keep newWork = return $ IR (ContinueWith wi) keep newWork
759 mkIRStop :: Monad m => InertAction -> WorkList -> m InteractResult
760 mkIRStop keep newWork = return $ IR Stop keep newWork
762 dischargeWorkItem :: Monad m => m InteractResult
763 dischargeWorkItem = mkIRStop KeepInert emptyCCan
765 noInteraction :: Monad m => WorkItem -> m InteractResult
766 noInteraction workItem = mkIRContinue workItem KeepInert emptyCCan
768 data WhichComesFromInert = LeftComesFromInert | RightComesFromInert
770 ---------------------------------------------------
771 -- Interact a single WorkItem with an InertSet as far as possible, i.e. until we get a Stop
772 -- result from an individual interaction (i.e. when the WorkItem is consumed), or until we've
773 -- interacted the WorkItem with the entire InertSet.
775 -- Postcondition: the new InertSet in the resulting StageResult is subset
776 -- of the input InertSet.
778 interactWithInertsStage :: SimplifierStage
779 interactWithInertsStage workItem inert
780 = foldlInertSetM interactNext initITR inert
782 initITR = SR { sr_inerts = emptyInert
783 , sr_new_work = emptyCCan
784 , sr_stop = ContinueWith workItem }
787 interactNext :: StageResult -> AtomicInert -> TcS StageResult
788 interactNext it inert
789 | ContinueWith workItem <- sr_stop it
790 = do { ir <- interactWithInert inert workItem
791 ; let inerts = sr_inerts it
792 ; return $ SR { sr_inerts = if ir_inert_action ir == KeepInert
793 then inerts `updInertSet` inert
795 , sr_new_work = sr_new_work it `unionWorkLists` ir_new_work ir
796 , sr_stop = ir_stop ir } }
797 | otherwise = return $ itrAddInert inert it
800 itrAddInert :: AtomicInert -> StageResult -> StageResult
801 itrAddInert inert itr = itr { sr_inerts = (sr_inerts itr) `updInertSet` inert }
803 -- Do a single interaction of two constraints.
804 interactWithInert :: AtomicInert -> WorkItem -> TcS InteractResult
805 interactWithInert inert workitem
806 = do { ctxt <- getTcSContext
807 ; let is_allowed = allowedInteraction (simplEqsOnly ctxt) inert workitem
808 inert_ev = cc_id inert
809 work_ev = cc_id workitem
811 -- Never interact a wanted and a derived where the derived's evidence
812 -- mentions the wanted evidence in an unguarded way.
813 -- See Note [Superclasses and recursive dictionaries]
814 -- and Note [New Wanted Superclass Work]
815 -- We don't have to do this for givens, as we fully know the evidence for them.
817 case (cc_flavor inert, cc_flavor workitem) of
818 (Wanted loc, Derived _) -> isGoodRecEv work_ev (WantedEvVar inert_ev loc)
819 (Derived _, Wanted loc) -> isGoodRecEv inert_ev (WantedEvVar work_ev loc)
822 ; if is_allowed && rec_ev_ok then
823 doInteractWithInert inert workitem
825 noInteraction workitem
828 allowedInteraction :: Bool -> AtomicInert -> WorkItem -> Bool
829 -- Allowed interactions
830 allowedInteraction eqs_only (CDictCan {}) (CDictCan {}) = not eqs_only
831 allowedInteraction eqs_only (CIPCan {}) (CIPCan {}) = not eqs_only
832 allowedInteraction _ _ _ = True
834 --------------------------------------------
835 doInteractWithInert :: CanonicalCt -> CanonicalCt -> TcS InteractResult
836 -- Identical class constraints.
839 (CDictCan { cc_id = d1, cc_flavor = fl1, cc_class = cls1, cc_tyargs = tys1 })
840 workItem@(CDictCan { cc_id = d2, cc_flavor = fl2, cc_class = cls2, cc_tyargs = tys2 })
841 | cls1 == cls2 && (and $ zipWith tcEqType tys1 tys2)
842 = solveOneFromTheOther (d1,fl1) workItem
844 | cls1 == cls2 && (not (isGiven fl1 && isGiven fl2))
845 = -- See Note [When improvement happens]
846 do { let work_item_pred_loc = (ClassP cls2 tys2, ppr d2)
847 inert_pred_loc = (ClassP cls1 tys1, ppr d1)
848 loc = combineCtLoc fl1 fl2
849 eqn_pred_locs = improveFromAnother work_item_pred_loc inert_pred_loc
850 ; wevvars <- mkWantedFunDepEqns loc eqn_pred_locs
851 -- See Note [Generating extra equalities]
852 ; workList <- canWanteds wevvars
853 ; mkIRContinue workItem KeepInert workList -- Keep the inert there so we avoid
854 -- re-introducing the fundep equalities
855 -- See Note [FunDep Reactions]
858 -- Class constraint and given equality: use the equality to rewrite
859 -- the class constraint.
860 doInteractWithInert (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi })
861 (CDictCan { cc_id = dv, cc_flavor = wfl, cc_class = cl, cc_tyargs = xis })
862 | ifl `canRewrite` wfl
863 , tv `elemVarSet` tyVarsOfTypes xis
864 -- substitute for tv in xis. Note that the resulting class
865 -- constraint is still canonical, since substituting xi-types in
866 -- xi-types generates xi-types. However, it may no longer be
867 -- inert with respect to the inert set items we've already seen.
868 -- For example, consider the inert set
873 -- and the work item D a (w). D a does not interact with D Int.
874 -- Next, it does interact with a ~g Int, getting rewritten to D
875 -- Int (w). But now we must go back through the rest of the inert
876 -- set again, to find that it can now be discharged by the given D
878 = do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,wfl,cl,xis)
879 ; mkIRStop KeepInert (singleCCan rewritten_dict) }
881 doInteractWithInert (CDictCan { cc_id = dv, cc_flavor = ifl, cc_class = cl, cc_tyargs = xis })
882 workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
883 | wfl `canRewrite` ifl
884 , tv `elemVarSet` tyVarsOfTypes xis
885 = do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,ifl,cl,xis)
886 ; mkIRContinue workItem DropInert (singleCCan rewritten_dict) }
888 -- Class constraint and given equality: use the equality to rewrite
889 -- the class constraint.
890 doInteractWithInert (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi })
891 (CIPCan { cc_id = ipid, cc_flavor = wfl, cc_ip_nm = nm, cc_ip_ty = ty })
892 | ifl `canRewrite` wfl
893 , tv `elemVarSet` tyVarsOfType ty
894 = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,wfl,nm,ty)
895 ; mkIRStop KeepInert (singleCCan rewritten_ip) }
897 doInteractWithInert (CIPCan { cc_id = ipid, cc_flavor = ifl, cc_ip_nm = nm, cc_ip_ty = ty })
898 workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
899 | wfl `canRewrite` ifl
900 , tv `elemVarSet` tyVarsOfType ty
901 = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,ifl,nm,ty)
902 ; mkIRContinue workItem DropInert (singleCCan rewritten_ip) }
904 -- Two implicit parameter constraints. If the names are the same,
905 -- but their types are not, we generate a wanted type equality
906 -- that equates the type (this is "improvement").
907 -- However, we don't actually need the coercion evidence,
908 -- so we just generate a fresh coercion variable that isn't used anywhere.
909 doInteractWithInert (CIPCan { cc_id = id1, cc_flavor = ifl, cc_ip_nm = nm1, cc_ip_ty = ty1 })
910 workItem@(CIPCan { cc_flavor = wfl, cc_ip_nm = nm2, cc_ip_ty = ty2 })
911 | nm1 == nm2 && isGiven wfl && isGiven ifl
912 = -- See Note [Overriding implicit parameters]
913 -- Dump the inert item, override totally with the new one
914 -- Do not require type equality
915 mkIRContinue workItem DropInert emptyCCan
917 | nm1 == nm2 && ty1 `tcEqType` ty2
918 = solveOneFromTheOther (id1,ifl) workItem
921 = -- See Note [When improvement happens]
922 do { co_var <- newWantedCoVar ty1 ty2
923 ; let flav = Wanted (combineCtLoc ifl wfl)
924 ; mkCanonical flav co_var >>= mkIRContinue workItem KeepInert }
927 -- Inert: equality, work item: function equality
929 -- Never rewrite a given with a wanted equality, and a type function
930 -- equality can never rewrite an equality. Note also that if we have
931 -- F x1 ~ x2 and a ~ x3, and a occurs in x2, we don't rewrite it. We
932 -- can wait until F x1 ~ x2 matches another F x1 ~ x4, and only then
933 -- we will ``expose'' x2 and x4 to rewriting.
935 -- Otherwise, we can try rewriting the type function equality with the equality.
936 doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi1 })
937 (CFunEqCan { cc_id = cv2, cc_flavor = wfl, cc_fun = tc
938 , cc_tyargs = args, cc_rhs = xi2 })
939 | ifl `canRewrite` wfl
940 , tv `elemVarSet` tyVarsOfTypes args
941 = do { rewritten_funeq <- rewriteFunEq (cv1,tv,xi1) (cv2,wfl,tc,args,xi2)
942 ; mkIRStop KeepInert (singleCCan rewritten_funeq) }
944 -- Inert: function equality, work item: equality
946 doInteractWithInert (CFunEqCan {cc_id = cv1, cc_flavor = ifl, cc_fun = tc
947 , cc_tyargs = args, cc_rhs = xi1 })
948 workItem@(CTyEqCan { cc_id = cv2, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi2 })
949 | wfl `canRewrite` ifl
950 , tv `elemVarSet` tyVarsOfTypes args
951 = do { rewritten_funeq <- rewriteFunEq (cv2,tv,xi2) (cv1,ifl,tc,args,xi1)
952 ; mkIRContinue workItem DropInert (singleCCan rewritten_funeq) }
954 doInteractWithInert (CFunEqCan { cc_id = cv1, cc_flavor = fl1, cc_fun = tc1
955 , cc_tyargs = args1, cc_rhs = xi1 })
956 workItem@(CFunEqCan { cc_id = cv2, cc_flavor = fl2, cc_fun = tc2
957 , cc_tyargs = args2, cc_rhs = xi2 })
958 | fl1 `canRewrite` fl2 && lhss_match
959 = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
960 ; mkIRStop KeepInert cans }
961 | fl2 `canRewrite` fl1 && lhss_match
962 = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
963 ; mkIRContinue workItem DropInert cans }
965 lhss_match = tc1 == tc2 && and (zipWith tcEqType args1 args2)
968 inert@(CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
969 workItem@(CTyEqCan { cc_id = cv2, cc_flavor = fl2, cc_tyvar = tv2, cc_rhs = xi2 })
970 -- Check for matching LHS
971 | fl1 `canRewrite` fl2 && tv1 == tv2
972 = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
973 ; mkIRStop KeepInert cans }
975 | fl2 `canRewrite` fl1 && tv1 == tv2
976 = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
977 ; mkIRContinue workItem DropInert cans }
979 -- Check for rewriting RHS
980 | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfType xi2
981 = do { rewritten_eq <- rewriteEqRHS (cv1,tv1,xi1) (cv2,fl2,tv2,xi2)
982 ; mkIRStop KeepInert rewritten_eq }
983 | fl2 `canRewrite` fl1 && tv2 `elemVarSet` tyVarsOfType xi1
984 = do { rewritten_eq <- rewriteEqRHS (cv2,tv2,xi2) (cv1,fl1,tv1,xi1)
985 ; mkIRContinue workItem DropInert rewritten_eq }
987 -- Finally, if workitem is a Flatten Equivalence Class constraint and the
988 -- inert is a wanted constraint, even when the workitem cannot rewrite the
989 -- inert, drop the inert out because you may have to reconsider solving the
990 -- inert *using* the equivalence class you created. See note [Loopy Spontaneous Solving]
991 -- and [InertSet FlattenSkolemEqClass]
993 | not $ isGiven fl1, -- The inert is wanted or derived
994 isMetaTyVar tv1, -- and has a unification variable lhs
995 FlatSkol {} <- tcTyVarDetails tv2, -- And workitem is a flatten skolem equality
996 Just tv2' <- tcGetTyVar_maybe xi2, FlatSkol {} <- tcTyVarDetails tv2'
997 = mkIRContinue workItem DropInert (singletonWorkList inert)
1000 -- Fall-through case for all other situations
1001 doInteractWithInert _ workItem = noInteraction workItem
1003 --------------------------------------------
1004 combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
1005 -- Precondition: At least one of them should be wanted
1006 combineCtLoc (Wanted loc) _ = loc
1007 combineCtLoc _ (Wanted loc) = loc
1008 combineCtLoc _ _ = panic "Expected one of wanted constraints (BUG)"
1011 -- Equational Rewriting
1012 rewriteDict :: (CoVar, TcTyVar, Xi) -> (DictId, CtFlavor, Class, [Xi]) -> TcS CanonicalCt
1013 rewriteDict (cv,tv,xi) (dv,gw,cl,xis)
1014 = do { let cos = substTysWith [tv] [mkCoVarCoercion cv] xis -- xis[tv] ~ xis[xi]
1015 args = substTysWith [tv] [xi] xis
1017 dict_co = mkTyConCoercion con cos
1018 ; dv' <- newDictVar cl args
1020 Wanted {} -> setDictBind dv (EvCast dv' (mkSymCoercion dict_co))
1021 _given_or_derived -> setDictBind dv' (EvCast dv dict_co)
1022 ; return (CDictCan { cc_id = dv'
1025 , cc_tyargs = args }) }
1027 rewriteIP :: (CoVar,TcTyVar,Xi) -> (EvVar,CtFlavor, IPName Name, TcType) -> TcS CanonicalCt
1028 rewriteIP (cv,tv,xi) (ipid,gw,nm,ty)
1029 = do { let ip_co = substTyWith [tv] [mkCoVarCoercion cv] ty -- ty[tv] ~ t[xi]
1030 ty' = substTyWith [tv] [xi] ty
1031 ; ipid' <- newIPVar nm ty'
1033 Wanted {} -> setIPBind ipid (EvCast ipid' (mkSymCoercion ip_co))
1034 _given_or_derived -> setIPBind ipid' (EvCast ipid ip_co)
1035 ; return (CIPCan { cc_id = ipid'
1038 , cc_ip_ty = ty' }) }
1040 rewriteFunEq :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TyCon, [Xi], Xi) -> TcS CanonicalCt
1041 rewriteFunEq (cv1,tv,xi1) (cv2,gw, tc,args,xi2)
1042 = do { let arg_cos = substTysWith [tv] [mkCoVarCoercion cv1] args
1043 args' = substTysWith [tv] [xi1] args
1044 fun_co = mkTyConCoercion tc arg_cos
1045 ; cv2' <- case gw of
1046 Wanted {} -> do { cv2' <- newWantedCoVar (mkTyConApp tc args') xi2
1047 ; setWantedCoBind cv2 $
1048 mkTransCoercion fun_co (mkCoVarCoercion cv2')
1050 _giv_or_der -> newGivOrDerCoVar (mkTyConApp tc args') xi2 $
1051 mkTransCoercion (mkSymCoercion fun_co) (mkCoVarCoercion cv2)
1052 ; return (CFunEqCan { cc_id = cv2'
1059 rewriteEqRHS :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TcTyVar,Xi) -> TcS CanonicalCts
1060 -- Use the first equality to rewrite the second, flavors already checked.
1061 -- E.g. c1 : tv1 ~ xi1 c2 : tv2 ~ xi2
1062 -- rewrites c2 to give
1063 -- c2' : tv2 ~ xi2[xi1/tv1]
1064 -- We must do an occurs check to sure the new constraint is canonical
1065 -- So we might return an empty bag
1066 rewriteEqRHS (cv1,tv1,xi1) (cv2,gw,tv2,xi2)
1067 | Just tv2' <- tcGetTyVar_maybe xi2'
1068 , tv2 == tv2' -- In this case xi2[xi1/tv1] = tv2, so we have tv2~tv2
1069 = do { when (isWanted gw) (setWantedCoBind cv2 (mkSymCoercion co2'))
1070 ; return emptyCCan }
1075 -> do { cv2' <- newWantedCoVar (mkTyVarTy tv2) xi2'
1076 ; setWantedCoBind cv2 $
1077 mkCoVarCoercion cv2' `mkTransCoercion` mkSymCoercion co2'
1080 -> newGivOrDerCoVar (mkTyVarTy tv2) xi2' $
1081 mkCoVarCoercion cv2 `mkTransCoercion` co2'
1083 ; xi2'' <- canOccursCheck gw tv2 xi2' -- we know xi2' is *not* tv2
1084 ; return (singleCCan $ CTyEqCan { cc_id = cv2'
1090 xi2' = substTyWith [tv1] [xi1] xi2
1091 co2' = substTyWith [tv1] [mkCoVarCoercion cv1] xi2 -- xi2 ~ xi2[xi1/tv1]
1094 rewriteEqLHS :: WhichComesFromInert -> (Coercion,Xi) -> (CoVar,CtFlavor,Xi) -> TcS CanonicalCts
1095 -- Used to ineratct two equalities of the following form:
1096 -- First Equality: co1: (XXX ~ xi1)
1097 -- Second Equality: cv2: (XXX ~ xi2)
1098 -- Where the cv1 `canRewrite` cv2 equality
1099 -- We have an option of creating new work (xi1 ~ xi2) OR (xi2 ~ xi1). This
1100 -- depends on whether the left or the right equality comes from the inert set.
1102 -- prefer to create (xi2 ~ xi1) if the first comes from the inert
1103 -- prefer to create (xi1 ~ xi2) if the second comes from the inert
1104 rewriteEqLHS which (co1,xi1) (cv2,gw,xi2)
1105 = do { cv2' <- case (isWanted gw, which) of
1106 (True,LeftComesFromInert) ->
1107 do { cv2' <- newWantedCoVar xi2 xi1
1108 ; setWantedCoBind cv2 $
1109 co1 `mkTransCoercion` mkSymCoercion (mkCoVarCoercion cv2')
1111 (True,RightComesFromInert) ->
1112 do { cv2' <- newWantedCoVar xi1 xi2
1113 ; setWantedCoBind cv2 $
1114 co1 `mkTransCoercion` mkCoVarCoercion cv2'
1116 (False,LeftComesFromInert) ->
1117 newGivOrDerCoVar xi2 xi1 $
1118 mkSymCoercion (mkCoVarCoercion cv2) `mkTransCoercion` co1
1119 (False,RightComesFromInert) ->
1120 newGivOrDerCoVar xi1 xi2 $
1121 mkSymCoercion co1 `mkTransCoercion` mkCoVarCoercion cv2
1122 ; mkCanonical gw cv2' }
1126 solveOneFromTheOther :: (EvVar, CtFlavor) -> CanonicalCt -> TcS InteractResult
1127 -- First argument inert, second argument workitem. They both represent
1128 -- wanted/given/derived evidence for the *same* predicate so we try here to
1129 -- discharge one directly from the other.
1131 -- Precondition: value evidence only (implicit parameters, classes)
1133 solveOneFromTheOther (iid,ifl) workItem
1134 -- Both derived needs a special case. You might think that we do not need
1135 -- two evidence terms for the same claim. But, since the evidence is partial,
1136 -- either evidence may do in some cases; see TcSMonad.isGoodRecEv.
1137 -- See also Example 3 in Note [Superclasses and recursive dictionaries]
1138 | isDerived ifl && isDerived wfl
1139 = noInteraction workItem
1141 | ifl `canRewrite` wfl
1142 = do { unless (isGiven wfl) $ setEvBind wid (EvId iid)
1143 -- Overwrite the binding, if one exists
1144 -- For Givens, which are lambda-bound, nothing to overwrite,
1145 ; dischargeWorkItem }
1147 | otherwise -- wfl `canRewrite` ifl
1148 = do { unless (isGiven ifl) $ setEvBind iid (EvId wid)
1149 ; mkIRContinue workItem DropInert emptyCCan }
1152 wfl = cc_flavor workItem
1153 wid = cc_id workItem
1156 Note [Superclasses and recursive dictionaries]
1157 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1158 Overlaps with Note [SUPERCLASS-LOOP 1]
1159 Note [SUPERCLASS-LOOP 2]
1160 Note [Recursive instances and superclases]
1161 ToDo: check overlap and delete redundant stuff
1163 Right before adding a given into the inert set, we must
1164 produce some more work, that will bring the superclasses
1165 of the given into scope. The superclass constraints go into
1168 When we simplify a wanted constraint, if we first see a matching
1169 instance, we may produce new wanted work. To (1) avoid doing this work
1170 twice in the future and (2) to handle recursive dictionaries we may ``cache''
1171 this item as solved (in effect, given) into our inert set and with that add
1172 its superclass constraints (as given) in our worklist.
1174 But now we have added partially solved constraints to the worklist which may
1175 interact with other wanteds. Consider the example:
1179 class Eq b => Foo a b --- 0-th selector
1180 instance Eq a => Foo [a] a --- fooDFun
1182 and wanted (Foo [t] t). We are first going to see that the instance matches
1183 and create an inert set that includes the solved (Foo [t] t) and its
1185 d1 :_g Foo [t] t d1 := EvDFunApp fooDFun d3
1186 d2 :_g Eq t d2 := EvSuperClass d1 0
1187 Our work list is going to contain a new *wanted* goal
1189 It is wrong to react the wanted (Eq t) with the given (Eq t) because that would
1190 construct loopy evidence. Hence the check isGoodRecEv in doInteractWithInert.
1192 OK, so we have ruled out bad behaviour, but how do we ge recursive dictionaries,
1197 data D r = ZeroD | SuccD (r (D r));
1199 instance (Eq (r (D r))) => Eq (D r) where
1200 ZeroD == ZeroD = True
1201 (SuccD a) == (SuccD b) = a == b
1204 equalDC :: D [] -> D [] -> Bool;
1207 We need to prove (Eq (D [])). Here's how we go:
1211 by instance decl, holds if
1215 *BUT* we have an inert set which gives us (no superclasses):
1217 By the instance declaration of Eq we can show the 'd2' goal if
1219 where d2 = dfEqList d3
1221 Now, however this wanted can interact with our inert d1 to set:
1223 and solve the goal. Why was this interaction OK? Because, if we chase the
1224 evidence of d1 ~~> dfEqD d2 ~~-> dfEqList d3, so by setting d3 := d1 we
1226 d3 := dfEqD2 (dfEqList d3)
1227 which is FINE because the use of d3 is protected by the instance function
1230 So, our strategy is to try to put solved wanted dictionaries into the
1231 inert set along with their superclasses (when this is meaningful,
1232 i.e. when new wanted goals are generated) but solve a wanted dictionary
1233 from a given only in the case where the evidence variable of the
1234 wanted is mentioned in the evidence of the given (recursively through
1235 the evidence binds) in a protected way: more instance function applications
1236 than superclass selectors.
1238 Here are some more examples from GHC's previous type checker
1242 This code arises in the context of "Scrap Your Boilerplate with Class"
1246 instance Sat (ctx Char) => Data ctx Char -- dfunData1
1247 instance (Sat (ctx [a]), Data ctx a) => Data ctx [a] -- dfunData2
1249 class Data Maybe a => Foo a
1251 instance Foo t => Sat (Maybe t) -- dfunSat
1253 instance Data Maybe a => Foo a -- dfunFoo1
1254 instance Foo a => Foo [a] -- dfunFoo2
1255 instance Foo [Char] -- dfunFoo3
1257 Consider generating the superclasses of the instance declaration
1258 instance Foo a => Foo [a]
1260 So our problem is this
1262 d1 :_w Data Maybe [t]
1264 We may add the given in the inert set, along with its superclasses
1265 [assuming we don't fail because there is a matching instance, see
1266 tryTopReact, given case ]
1270 d01 :_g Data Maybe t -- d2 := EvDictSuperClass d0 0
1271 d1 :_w Data Maybe [t]
1272 Then d2 can readily enter the inert, and we also do solving of the wanted
1275 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1277 d2 :_w Sat (Maybe [t])
1279 d01 :_g Data Maybe t
1280 Now, we may simplify d2 more:
1283 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1284 d1 :_g Data Maybe [t]
1285 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1289 d01 :_g Data Maybe t
1291 Now, we can just solve d3.
1294 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1295 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1298 d01 :_g Data Maybe t
1299 And now we can simplify d4 again, but since it has superclasses we *add* them to the worklist:
1302 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1303 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1304 d4 :_g Foo [t] d4 := dfunFoo2 d5
1307 d6 :_g Data Maybe [t] d6 := EvDictSuperClass d4 0
1308 d01 :_g Data Maybe t
1309 Now, d5 can be solved! (and its superclass enter scope)
1312 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1313 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1314 d4 :_g Foo [t] d4 := dfunFoo2 d5
1315 d5 :_g Foo t d5 := dfunFoo1 d7
1318 d6 :_g Data Maybe [t]
1319 d8 :_g Data Maybe t d8 := EvDictSuperClass d5 0
1320 d01 :_g Data Maybe t
1323 [1] Suppose we pick d8 and we react him with d01. Which of the two givens should
1324 we keep? Well, we *MUST NOT* drop d01 because d8 contains recursive evidence
1325 that must not be used (look at case interactInert where both inert and workitem
1326 are givens). So we have several options:
1327 - Drop the workitem always (this will drop d8)
1328 This feels very unsafe -- what if the work item was the "good" one
1329 that should be used later to solve another wanted?
1330 - Don't drop anyone: the inert set may contain multiple givens!
1331 [This is currently implemented]
1333 The "don't drop anyone" seems the most safe thing to do, so now we come to problem 2:
1334 [2] We have added both d6 and d01 in the inert set, and we are interacting our wanted
1335 d7. Now the [isRecDictEv] function in the ineration solver
1336 [case inert-given workitem-wanted] will prevent us from interacting d7 := d8
1337 precisely because chasing the evidence of d8 leads us to an unguarded use of d7.
1339 So, no interaction happens there. Then we meet d01 and there is no recursion
1340 problem there [isRectDictEv] gives us the OK to interact and we do solve d7 := d01!
1342 Note [SUPERCLASS-LOOP 1]
1343 ~~~~~~~~~~~~~~~~~~~~~~~~
1344 We have to be very, very careful when generating superclasses, lest we
1345 accidentally build a loop. Here's an example:
1349 class S a => C a where { opc :: a -> a }
1350 class S b => D b where { opd :: b -> b }
1352 instance C Int where
1355 instance D Int where
1358 From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int}
1359 Simplifying, we may well get:
1360 $dfCInt = :C ds1 (opd dd)
1363 Notice that we spot that we can extract ds1 from dd.
1365 Alas! Alack! We can do the same for (instance D Int):
1367 $dfDInt = :D ds2 (opc dc)
1371 And now we've defined the superclass in terms of itself.
1372 Two more nasty cases are in
1377 - Satisfy the superclass context *all by itself*
1378 (tcSimplifySuperClasses)
1379 - And do so completely; i.e. no left-over constraints
1380 to mix with the constraints arising from method declarations
1383 Note [SUPERCLASS-LOOP 2]
1384 ~~~~~~~~~~~~~~~~~~~~~~~~
1385 We need to be careful when adding "the constaint we are trying to prove".
1386 Suppose we are *given* d1:Ord a, and want to deduce (d2:C [a]) where
1388 class Ord a => C a where
1389 instance Ord [a] => C [a] where ...
1391 Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the
1392 superclasses of C [a] to avails. But we must not overwrite the binding
1393 for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
1396 Here's another variant, immortalised in tcrun020
1397 class Monad m => C1 m
1398 class C1 m => C2 m x
1399 instance C2 Maybe Bool
1400 For the instance decl we need to build (C1 Maybe), and it's no good if
1401 we run around and add (C2 Maybe Bool) and its superclasses to the avails
1402 before we search for C1 Maybe.
1404 Here's another example
1405 class Eq b => Foo a b
1406 instance Eq a => Foo [a] a
1410 we'll first deduce that it holds (via the instance decl). We must not
1411 then overwrite the Eq t constraint with a superclass selection!
1413 At first I had a gross hack, whereby I simply did not add superclass constraints
1414 in addWanted, though I did for addGiven and addIrred. This was sub-optimal,
1415 becuase it lost legitimate superclass sharing, and it still didn't do the job:
1416 I found a very obscure program (now tcrun021) in which improvement meant the
1417 simplifier got two bites a the cherry... so something seemed to be an Stop
1418 first time, but reducible next time.
1420 Now we implement the Right Solution, which is to check for loops directly
1421 when adding superclasses. It's a bit like the occurs check in unification.
1423 Note [Recursive instances and superclases]
1424 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1425 Consider this code, which arises in the context of "Scrap Your
1426 Boilerplate with Class".
1430 instance Sat (ctx Char) => Data ctx Char
1431 instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]
1433 class Data Maybe a => Foo a
1435 instance Foo t => Sat (Maybe t)
1437 instance Data Maybe a => Foo a
1438 instance Foo a => Foo [a]
1441 In the instance for Foo [a], when generating evidence for the superclasses
1442 (ie in tcSimplifySuperClasses) we need a superclass (Data Maybe [a]).
1443 Using the instance for Data, we therefore need
1444 (Sat (Maybe [a], Data Maybe a)
1445 But we are given (Foo a), and hence its superclass (Data Maybe a).
1446 So that leaves (Sat (Maybe [a])). Using the instance for Sat means
1447 we need (Foo [a]). And that is the very dictionary we are bulding
1448 an instance for! So we must put that in the "givens". So in this
1450 Given: Foo a, Foo [a]
1451 Wanted: Data Maybe [a]
1453 BUT we must *not not not* put the *superclasses* of (Foo [a]) in
1454 the givens, which is what 'addGiven' would normally do. Why? Because
1455 (Data Maybe [a]) is the superclass, so we'd "satisfy" the wanted
1456 by selecting a superclass from Foo [a], which simply makes a loop.
1458 On the other hand we *must* put the superclasses of (Foo a) in
1459 the givens, as you can see from the derivation described above.
1461 Conclusion: in the very special case of tcSimplifySuperClasses
1462 we have one 'given' (namely the "this" dictionary) whose superclasses
1463 must not be added to 'givens' by addGiven.
1465 There is a complication though. Suppose there are equalities
1466 instance (Eq a, a~b) => Num (a,b)
1467 Then we normalise the 'givens' wrt the equalities, so the original
1468 given "this" dictionary is cast to one of a different type. So it's a
1469 bit trickier than before to identify the "special" dictionary whose
1470 superclasses must not be added. See test
1471 indexed-types/should_run/EqInInstance
1473 We need a persistent property of the dictionary to record this
1474 special-ness. Current I'm using the InstLocOrigin (a bit of a hack,
1475 but cool), which is maintained by dictionary normalisation.
1476 Specifically, the InstLocOrigin is
1478 then the no-superclass thing kicks in. WATCH OUT if you fiddle
1481 Note [MATCHING-SYNONYMS]
1482 ~~~~~~~~~~~~~~~~~~~~~~~~
1483 When trying to match a dictionary (D tau) to a top-level instance, or a
1484 type family equation (F taus_1 ~ tau_2) to a top-level family instance,
1485 we do *not* need to expand type synonyms because the matcher will do that for us.
1488 Note [RHS-FAMILY-SYNONYMS]
1489 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1490 The RHS of a family instance is represented as yet another constructor which is
1491 like a type synonym for the real RHS the programmer declared. Eg:
1492 type instance F (a,a) = [a]
1494 :R32 a = [a] -- internal type synonym introduced
1495 F (a,a) ~ :R32 a -- instance
1497 When we react a family instance with a type family equation in the work list
1498 we keep the synonym-using RHS without expansion.
1501 *********************************************************************************
1503 The top-reaction Stage
1505 *********************************************************************************
1508 -- If a work item has any form of interaction with top-level we get this
1509 data TopInteractResult
1510 = NoTopInt -- No top-level interaction
1512 { tir_new_work :: WorkList -- Sub-goals or new work (could be given,
1513 -- for superclasses)
1514 , tir_new_inert :: StopOrContinue -- The input work item, ready to become *inert* now:
1515 } -- NB: in ``given'' (solved) form if the
1516 -- original was wanted or given and instance match
1517 -- was found, but may also be in wanted form if we
1518 -- only reacted with functional dependencies
1519 -- arising from top-level instances.
1521 topReactionsStage :: SimplifierStage
1522 topReactionsStage workItem inerts
1523 = do { tir <- tryTopReact workItem
1526 return $ SR { sr_inerts = inerts
1527 , sr_new_work = emptyWorkList
1528 , sr_stop = ContinueWith workItem }
1529 SomeTopInt tir_new_work tir_new_inert ->
1530 return $ SR { sr_inerts = inerts
1531 , sr_new_work = tir_new_work
1532 , sr_stop = tir_new_inert
1536 tryTopReact :: WorkItem -> TcS TopInteractResult
1537 tryTopReact workitem
1538 = do { -- A flag controls the amount of interaction allowed
1539 -- See Note [Simplifying RULE lhs constraints]
1540 ctxt <- getTcSContext
1541 ; if allowedTopReaction (simplEqsOnly ctxt) workitem
1542 then do { traceTcS "tryTopReact / calling doTopReact" (ppr workitem)
1543 ; doTopReact workitem }
1544 else return NoTopInt
1547 allowedTopReaction :: Bool -> WorkItem -> Bool
1548 allowedTopReaction eqs_only (CDictCan {}) = not eqs_only
1549 allowedTopReaction _ _ = True
1552 doTopReact :: WorkItem -> TcS TopInteractResult
1553 -- The work item does not react with the inert set,
1554 -- so try interaction with top-level instances
1555 doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Wanted loc
1556 , cc_class = cls, cc_tyargs = xis })
1557 = do { -- See Note [MATCHING-SYNONYMS]
1558 ; lkp_inst_res <- matchClassInst cls xis loc
1559 ; case lkp_inst_res of
1560 NoInstance -> do { traceTcS "doTopReact/ no class instance for" (ppr dv)
1562 GenInst wtvs ev_term -> -- Solved
1563 -- No need to do fundeps stuff here; the instance
1564 -- matches already so we won't get any more info
1565 -- from functional dependencies
1566 do { traceTcS "doTopReact/ found class instance for" (ppr dv)
1567 ; setDictBind dv ev_term
1568 ; workList <- canWanteds wtvs
1570 -- Solved in one step and no new wanted work produced.
1571 -- i.e we directly matched a top-level instance
1572 -- No point in caching this in 'inert', nor in adding superclasses
1573 then return $ SomeTopInt { tir_new_work = emptyCCan
1574 , tir_new_inert = Stop }
1576 -- Solved and new wanted work produced, you may cache the
1577 -- (tentatively solved) dictionary as Derived and its superclasses
1578 else do { let solved = makeSolved workItem
1579 ; sc_work <- newSCWorkFromFlavored dv (Derived loc) cls xis
1580 ; return $ SomeTopInt
1581 { tir_new_work = workList `unionWorkLists` sc_work
1582 , tir_new_inert = ContinueWith solved } }
1586 -- Try for a fundep reaction beween the wanted item
1587 -- and a top-level instance declaration
1589 = do { instEnvs <- getInstEnvs
1590 ; let eqn_pred_locs = improveFromInstEnv (classInstances instEnvs)
1591 (ClassP cls xis, ppr dv)
1592 ; wevvars <- mkWantedFunDepEqns loc eqn_pred_locs
1593 -- NB: fundeps generate some wanted equalities, but
1594 -- we don't use their evidence for anything
1595 ; fd_work <- canWanteds wevvars
1596 ; sc_work <- newSCWorkFromFlavored dv (Derived loc) cls xis
1597 ; return $ SomeTopInt { tir_new_work = fd_work `unionWorkLists` sc_work
1598 , tir_new_inert = ContinueWith workItem }
1599 -- NB: workItem is inert, but it isn't solved
1600 -- keep it as inert, although it's not solved because we
1601 -- have now reacted all its top-level fundep-induced equalities!
1603 -- See Note [FunDep Reactions]
1606 -- Otherwise, we have a given or derived
1607 doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = fl
1608 , cc_class = cls, cc_tyargs = xis })
1609 = do { sc_work <- newSCWorkFromFlavored dv fl cls xis
1610 ; return $ SomeTopInt sc_work (ContinueWith workItem) }
1611 -- See Note [Given constraint that matches an instance declaration]
1614 doTopReact (CFunEqCan { cc_id = cv, cc_flavor = fl
1615 , cc_fun = tc, cc_tyargs = args, cc_rhs = xi })
1616 = ASSERT (isSynFamilyTyCon tc) -- No associated data families have reached that far
1617 do { match_res <- matchFam tc args -- See Note [MATCHING-SYNONYMS]
1621 MatchInstSingle (rep_tc, rep_tys)
1622 -> do { let Just coe_tc = tyConFamilyCoercion_maybe rep_tc
1623 Just rhs_ty = tcView (mkTyConApp rep_tc rep_tys)
1624 -- Eagerly expand away the type synonym on the
1625 -- RHS of a type function, so that it never
1626 -- appears in an error message
1627 -- See Note [Type synonym families] in TyCon
1628 coe = mkTyConApp coe_tc rep_tys
1630 Wanted {} -> do { cv' <- newWantedCoVar rhs_ty xi
1631 ; setWantedCoBind cv $
1632 coe `mkTransCoercion`
1635 _ -> newGivOrDerCoVar xi rhs_ty $
1636 mkSymCoercion (mkCoVarCoercion cv) `mkTransCoercion` coe
1638 ; workList <- mkCanonical fl cv'
1639 ; return $ SomeTopInt workList Stop }
1641 -> panicTcS $ text "TcSMonad.matchFam returned multiple instances!"
1645 -- Any other work item does not react with any top-level equations
1646 doTopReact _workItem = return NoTopInt
1649 Note [FunDep and implicit parameter reactions]
1650 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1651 Currently, our story of interacting two dictionaries (or a dictionary
1652 and top-level instances) for functional dependencies, and implicit
1653 paramters, is that we simply produce new wanted equalities. So for example
1655 class D a b | a -> b where ...
1661 We generate the extra work item
1663 where 'cv' is currently unused. However, this new item reacts with d2,
1664 discharging it in favour of a new constraint d2' thus:
1666 d2 := d2' |> D Int cv
1667 Now d2' can be discharged from d1
1669 We could be more aggressive and try to *immediately* solve the dictionary
1670 using those extra equalities. With the same inert set and work item we
1671 might dischard d2 directly:
1674 d2 := d1 |> D Int cv
1676 But in general it's a bit painful to figure out the necessary coercion,
1677 so we just take the first approach.
1679 It's exactly the same with implicit parameters, except that the
1680 "aggressive" approach would be much easier to implement.
1682 Note [When improvement happens]
1683 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1684 We fire an improvement rule when
1686 * Two constraints match (modulo the fundep)
1687 e.g. C t1 t2, C t1 t3 where C a b | a->b
1688 The two match because the first arg is identical
1690 * At least one is not Given. If they are both given, we don't fire
1691 the reaction because we have no way of constructing evidence for a
1692 new equality nor does it seem right to create a new wanted goal
1693 (because the goal will most likely contain untouchables, which
1694 can't be solved anyway)!
1696 Note that we *do* fire the improvement if one is Given and one is Derived.
1697 The latter can be a superclass of a wanted goal. Example (tcfail138)
1698 class L a b | a -> b
1699 class (G a, L a b) => C a b
1701 instance C a b' => G (Maybe a)
1702 instance C a b => C (Maybe a) a
1703 instance L (Maybe a) a
1705 When solving the superclasses of the (C (Maybe a) a) instance, we get
1706 Given: C a b ... and hance by superclasses, (G a, L a b)
1708 Use the instance decl to get
1710 The (C a b') is inert, so we generate its Derived superclasses (L a b'),
1711 and now we need improvement between that derived superclass an the Given (L a b)
1713 Note [Overriding implicit parameters]
1714 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1716 f :: (?x::a) -> Bool -> a
1718 g v = let ?x::Int = 3
1719 in (f v, let ?x::Bool = True in f v)
1721 This should probably be well typed, with
1722 g :: Bool -> (Int, Bool)
1724 So the inner binding for ?x::Bool *overrides* the outer one.
1725 Hence a work-item Given overrides an inert-item Given.
1727 Note [Given constraint that matches an instance declaration]
1728 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1729 What should we do when we discover that one (or more) top-level
1730 instances match a given (or solved) class constraint? We have
1733 1. Reject the program. The reason is that there may not be a unique
1734 best strategy for the solver. Example, from the OutsideIn(X) paper:
1735 instance P x => Q [x]
1736 instance (x ~ y) => R [x] y
1738 wob :: forall a b. (Q [b], R b a) => a -> Int
1740 g :: forall a. Q [a] => [a] -> Int
1743 will generate the impliation constraint:
1744 Q [a] => (Q [beta], R beta [a])
1745 If we react (Q [beta]) with its top-level axiom, we end up with a
1746 (P beta), which we have no way of discharging. On the other hand,
1747 if we react R beta [a] with the top-level we get (beta ~ a), which
1748 is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
1749 now solvable by the given Q [a].
1751 However, this option is restrictive, for instance [Example 3] from
1752 Note [Recursive dictionaries] will fail to work.
1754 2. Ignore the problem, hoping that the situations where there exist indeed
1755 such multiple strategies are rare: Indeed the cause of the previous
1756 problem is that (R [x] y) yields the new work (x ~ y) which can be
1757 *spontaneously* solved, not using the givens.
1759 We are choosing option 2 below but we might consider having a flag as well.
1762 Note [New Wanted Superclass Work]
1763 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1764 Even in the case of wanted constraints, we add all of its superclasses as
1765 new given work. There are several reasons for this:
1766 a) to minimise error messages;
1767 eg suppose we have wanted (Eq a, Ord a)
1768 then we report only (Ord a) unsoluble
1770 b) to make the smallest number of constraints when *inferring* a type
1771 (same Eq/Ord example)
1773 c) for recursive dictionaries we *must* add the superclasses
1774 so that we can use them when solving a sub-problem
1776 d) To allow FD-like improvement for type families. Assume that
1778 class C a b | a -> b
1779 and we have to solve the implication constraint:
1781 Then, FD improvement can help us to produce a new wanted (beta ~ b)
1783 We want to have the same effect with the type family encoding of
1784 functional dependencies. Namely, consider:
1785 class (F a ~ b) => C a b
1786 Now suppose that we have:
1789 By interacting the given we will get given (F a ~ b) which is not
1790 enough by itself to make us discharge (C a beta). However, we
1791 may create a new derived equality from the super-class of the
1792 wanted constraint (C a beta), namely derived (F a ~ beta).
1793 Now we may interact this with given (F a ~ b) to get:
1795 But 'beta' is a touchable unification variable, and hence OK to
1796 unify it with 'b', replacing the derived evidence with the identity.
1798 This requires trySpontaneousSolve to solve *derived*
1799 equalities that have a touchable in their RHS, *in addition*
1800 to solving wanted equalities.
1802 Here is another example where this is useful.
1806 class (F a ~ b) => C a b
1807 And we are given the wanteds:
1811 We surely do *not* want to quantify over (b ~ c), since if someone provides
1812 dictionaries for (C a b) and (C a c), these dictionaries can provide a proof
1813 of (b ~ c), hence no extra evidence is necessary. Here is what will happen:
1815 Step 1: We will get new *given* superclass work,
1816 provisionally to our solving of w1 and w2
1818 g1: F a ~ b, g2 : F a ~ c,
1819 w1 : C a b, w2 : C a c, w3 : b ~ c
1821 The evidence for g1 and g2 is a superclass evidence term:
1823 g1 := sc w1, g2 := sc w2
1825 Step 2: The givens will solve the wanted w3, so that
1826 w3 := sym (sc w1) ; sc w2
1828 Step 3: Now, one may naively assume that then w2 can be solve from w1
1829 after rewriting with the (now solved equality) (b ~ c).
1831 But this rewriting is ruled out by the isGoodRectDict!
1833 Conclusion, we will (correctly) end up with the unsolved goals
1836 NB: The desugarer needs be more clever to deal with equalities
1837 that participate in recursive dictionary bindings.
1840 newSCWorkFromFlavored :: EvVar -> CtFlavor -> Class -> [Xi]
1842 newSCWorkFromFlavored ev flavor cls xis
1843 | Given loc <- flavor -- The NoScSkol says "don't add superclasses"
1844 , NoScSkol <- ctLocOrigin loc -- Very important!
1845 = return emptyWorkList
1848 = do { let (tyvars, sc_theta, _, _) = classBigSig cls
1849 sc_theta1 = substTheta (zipTopTvSubst tyvars xis) sc_theta
1850 -- Add *all* its superclasses (equalities or not) as new given work
1851 -- See Note [New Wanted Superclass Work]
1852 ; sc_vars <- zipWithM inst_one sc_theta1 [0..]
1853 ; mkCanonicals flavor sc_vars }
1855 inst_one pred n = newGivOrDerEvVar pred (EvSuperClass ev n)
1857 data LookupInstResult
1859 | GenInst [WantedEvVar] EvTerm
1861 matchClassInst :: Class -> [Type] -> WantedLoc -> TcS LookupInstResult
1862 matchClassInst clas tys loc
1863 = do { let pred = mkClassPred clas tys
1864 ; mb_result <- matchClass clas tys
1866 MatchInstNo -> return NoInstance
1867 MatchInstMany -> return NoInstance -- defer any reactions of a multitude until
1868 -- we learn more about the reagent
1869 MatchInstSingle (dfun_id, mb_inst_tys) ->
1870 do { checkWellStagedDFun pred dfun_id loc
1872 -- It's possible that not all the tyvars are in
1873 -- the substitution, tenv. For example:
1874 -- instance C X a => D X where ...
1875 -- (presumably there's a functional dependency in class C)
1876 -- Hence mb_inst_tys :: Either TyVar TcType
1878 ; tys <- instDFunTypes mb_inst_tys
1879 ; let (theta, _) = tcSplitPhiTy (applyTys (idType dfun_id) tys)
1880 ; if null theta then
1881 return (GenInst [] (EvDFunApp dfun_id tys []))
1883 { ev_vars <- instDFunConstraints theta
1884 ; let wevs = [WantedEvVar w loc | w <- ev_vars]
1885 ; return $ GenInst wevs (EvDFunApp dfun_id tys ev_vars) }