3 solveInteract, AtomicInert,
4 InertSet, emptyInert, updInertSet, extractUnsolved, solveOne,
8 #include "HsVersions.h"
31 import Control.Monad ( when )
40 import qualified Data.Map as Map
43 import Control.Monad( zipWithM, unless )
44 import FastString ( sLit )
48 Note [InertSet invariants]
49 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
51 An InertSet is a bag of canonical constraints, with the following invariants:
53 1 No two constraints react with each other.
55 A tricky case is when there exists a given (solved) dictionary
56 constraint and a wanted identical constraint in the inert set, but do
57 not react because reaction would create loopy dictionary evidence for
58 the wanted. See note [Recursive dictionaries]
60 2 Given equalities form an idempotent substitution [none of the
61 given LHS's occur in any of the given RHS's or reactant parts]
63 3 Wanted equalities also form an idempotent substitution
64 4 The entire set of equalities is acyclic.
66 5 Wanted dictionaries are inert with the top-level axiom set
68 6 Equalities of the form tv1 ~ tv2 always have a touchable variable
69 on the left (if possible).
70 7 No wanted constraints tv1 ~ tv2 with tv1 touchable. Such constraints
71 will be marked as solved right before being pushed into the inert set.
72 See note [Touchables and givens].
74 Note that 6 and 7 are /not/ enforced by canonicalization but rather by
75 insertion in the inert list, ie by TcInteract.
77 During the process of solving, the inert set will contain some
78 previously given constraints, some wanted constraints, and some given
79 constraints which have arisen from solving wanted constraints. For
80 now we do not distinguish between given and solved constraints.
82 Note that we must switch wanted inert items to given when going under an
83 implication constraint (when in top-level inference mode).
85 Note [InertSet FlattenSkolemEqClass]
86 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
87 The inert_fsks field of the inert set contains an "inverse map" of all the
88 flatten skolem equalities in the inert set. For instance, if inert_cts looks
95 Then, the inert_fsks fields holds the following map:
96 fsk2 |-> { fsk1, fsk3 }
98 Along with the necessary coercions to convert fsk1 and fsk3 back to fsk2
99 and fsk4 back to fsk5. Hence, the invariants of the inert_fsks field are:
101 (a) All TcTyVars in the domain and range of inert_fsks are flatten skolems
102 (b) All TcTyVars in the domain of inert_fsk occur naked as rhs in some
103 equalities of inert_cts
104 (c) For every mapping fsk1 |-> { (fsk2,co), ... } it must be:
107 The role of the inert_fsks is to make it easy to maintain the equivalence
108 class of each flatten skolem, which is much needed to correctly do spontaneous
109 solving. See Note [Loopy Spontaneous Solving]
112 -- See Note [InertSet invariants]
114 = IS { inert_cts :: Bag.Bag CanonicalCt
115 , inert_fsks :: Map.Map TcTyVar [(TcTyVar,Coercion)] }
116 -- See Note [InertSet FlattenSkolemEqClass]
118 instance Outputable InertSet where
119 ppr is = vcat [ vcat (map ppr (Bag.bagToList $ inert_cts is))
120 , vcat (map (\(v,rest) -> ppr v <+> text "|->" <+> hsep (map (ppr.fst) rest))
121 (Map.toList $ inert_fsks is)
125 emptyInert :: InertSet
126 emptyInert = IS { inert_cts = Bag.emptyBag, inert_fsks = Map.empty }
128 updInertSet :: InertSet -> AtomicInert -> InertSet
129 -- Introduces an element in the inert set for the first time
130 updInertSet (IS { inert_cts = cts, inert_fsks = fsks })
131 item@(CTyEqCan { cc_id = cv
134 | Just tv2 <- tcGetTyVar_maybe xi,
135 FlatSkol {} <- tcTyVarDetails tv1,
136 FlatSkol {} <- tcTyVarDetails tv2
137 = let cts' = cts `Bag.snocBag` item
138 fsks' = Map.insertWith (++) tv2 [(tv1, mkCoVarCoercion cv)] fsks
139 -- See Note [InertSet FlattenSkolemEqClass]
140 in IS { inert_cts = cts', inert_fsks = fsks' }
141 updInertSet (IS { inert_cts = cts
142 , inert_fsks = fsks }) item
143 = let cts' = cts `Bag.snocBag` item
144 in IS { inert_cts = cts', inert_fsks = fsks }
146 foldlInertSetM :: (Monad m) => (a -> AtomicInert -> m a) -> a -> InertSet -> m a
147 foldlInertSetM k z (IS { inert_cts = cts })
148 = Bag.foldlBagM k z cts
150 extractUnsolved :: InertSet -> (InertSet, CanonicalCts)
151 extractUnsolved is@(IS {inert_cts = cts})
152 = (is { inert_cts = cts'}, unsolved)
153 where (unsolved, cts') = Bag.partitionBag isWantedCt cts
156 getFskEqClass :: InertSet -> TcTyVar -> [(TcTyVar,Coercion)]
157 -- Precondition: tv is a FlatSkol. See Note [InertSet FlattenSkolemEqClass]
158 getFskEqClass (IS { inert_cts = cts, inert_fsks = fsks }) tv
159 = case lkpTyEqCanByLhs of
160 Nothing -> fromMaybe [] (Map.lookup tv fsks)
162 case tcGetTyVar_maybe (cc_rhs ceq) of
163 Just tv_rhs | FlatSkol {} <- tcTyVarDetails tv_rhs
164 -> let ceq_co = mkSymCoercion $ mkCoVarCoercion (cc_id ceq)
165 mk_co (v,c) = (v, mkTransCoercion c ceq_co)
166 in (tv_rhs, ceq_co): map mk_co (fromMaybe [] $ Map.lookup tv fsks)
168 where lkpTyEqCanByLhs = Bag.foldlBag lkp Nothing cts
169 lkp :: Maybe CanonicalCt -> CanonicalCt -> Maybe CanonicalCt
170 lkp Nothing ct@(CTyEqCan {cc_tyvar = tv'}) | tv' == tv = Just ct
171 lkp other _ct = other
174 isWantedCt :: CanonicalCt -> Bool
175 isWantedCt ct = isWanted (cc_flavor ct)
178 data Inert = IS { class_inerts :: FiniteMap Class Atomics
179 ip_inerts :: FiniteMap Class Atomics
180 tyfun_inerts :: FiniteMap TyCon Atomics
181 tyvar_inerts :: FiniteMap TyVar Atomics
184 Later should we also separate out givens and wanteds?
189 Note [Touchables and givens]
190 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
191 Touchable variables will never show up in givens which are inputs to
192 the solver. However, touchables may show up in givens generated by the flattener.
207 which can be put in the inert set. Suppose we also have a wanted
211 We cannot rewrite the given G alpha ~g b using the wanted alpha ~w
212 Int. Instead, after reacting alpha ~w Int with the whole inert set,
213 we observe that we can solve it by unifying alpha with Int, so we mark
214 it as solved and put it back in the *work list*. [We also immediately unify
215 alpha := Int, without telling anyone, see trySpontaneousSolve function, to
216 avoid doing this in the end.]
218 Later, because it is solved (given, in effect), we can use it to rewrite
219 G alpha ~g b to G Int ~g b, which gets put back in the work list. Eventually,
220 we will dispatch the remaining wanted constraints using the top-level axioms.
222 Finally, note that after reacting a wanted equality with the entire inert set
223 we may end up with something like
227 which we should flip around to generate the solved constraint alpha ~s b.
229 %*********************************************************************
231 * Main Interaction Solver *
233 **********************************************************************
237 1. Canonicalise (unary)
238 2. Pairwise interaction (binary)
239 * Take one from work list
240 * Try all pair-wise interactions with each constraint in inert
241 3. Try to solve spontaneously for equalities involving touchables
242 4. Top-level interaction (binary wrt top-level)
243 Superclass decomposition belongs in (4), see note [Superclasses]
247 type AtomicInert = CanonicalCt -- constraint pulled from InertSet
248 type WorkItem = CanonicalCt -- constraint pulled from WorkList
250 type WorkList = CanonicalCts -- A mixture of Given, Wanted, and Solved
251 type SWorkList = WorkList -- A worklist of solved
254 listToWorkList :: [WorkItem] -> WorkList
255 listToWorkList = Bag.listToBag
257 unionWorkLists :: WorkList -> WorkList -> WorkList
258 unionWorkLists = Bag.unionBags
260 foldlWorkListM :: (Monad m) => (a -> WorkItem -> m a) -> a -> WorkList -> m a
261 foldlWorkListM = Bag.foldlBagM
263 isEmptyWorkList :: WorkList -> Bool
264 isEmptyWorkList = Bag.isEmptyBag
266 emptyWorkList :: WorkList
267 emptyWorkList = Bag.emptyBag
269 singletonWorkList :: CanonicalCt -> WorkList
270 singletonWorkList ct = singleCCan ct
273 = Stop -- Work item is consumed
274 | ContinueWith WorkItem -- Not consumed
276 instance Outputable StopOrContinue where
277 ppr Stop = ptext (sLit "Stop")
278 ppr (ContinueWith w) = ptext (sLit "ContinueWith") <+> ppr w
280 -- Results after interacting a WorkItem as far as possible with an InertSet
282 = SR { sr_inerts :: InertSet
283 -- The new InertSet to use (REPLACES the old InertSet)
284 , sr_new_work :: WorkList
285 -- Any new work items generated (should be ADDED to the old WorkList)
287 -- sr_stop = Just workitem => workitem is *not* in sr_inerts and
288 -- workitem is inert wrt to sr_inerts
289 , sr_stop :: StopOrContinue
292 instance Outputable StageResult where
293 ppr (SR { sr_inerts = inerts, sr_new_work = work, sr_stop = stop })
294 = ptext (sLit "SR") <+>
295 braces (sep [ ptext (sLit "inerts =") <+> ppr inerts <> comma
296 , ptext (sLit "new work =") <+> ppr work <> comma
297 , ptext (sLit "stop =") <+> ppr stop])
299 type SimplifierStage = WorkItem -> InertSet -> TcS StageResult
301 -- Combine a sequence of simplifier 'stages' to create a pipeline
302 runSolverPipeline :: [(String, SimplifierStage)]
303 -> InertSet -> WorkItem
304 -> TcS (InertSet, WorkList)
305 -- Precondition: non-empty list of stages
306 runSolverPipeline pipeline inerts workItem
307 = do { traceTcS "Start solver pipeline" $
308 vcat [ ptext (sLit "work item =") <+> ppr workItem
309 , ptext (sLit "inerts =") <+> ppr inerts]
311 ; let itr_in = SR { sr_inerts = inerts
312 , sr_new_work = emptyWorkList
313 , sr_stop = ContinueWith workItem }
314 ; itr_out <- run_pipeline pipeline itr_in
316 = case sr_stop itr_out of
317 Stop -> sr_inerts itr_out
318 ContinueWith item -> sr_inerts itr_out `updInertSet` item
319 ; return (new_inert, sr_new_work itr_out) }
321 run_pipeline :: [(String, SimplifierStage)]
322 -> StageResult -> TcS StageResult
323 run_pipeline [] itr = return itr
324 run_pipeline _ itr@(SR { sr_stop = Stop }) = return itr
326 run_pipeline ((name,stage):stages)
327 (SR { sr_new_work = accum_work
329 , sr_stop = ContinueWith work_item })
330 = do { itr <- stage work_item inerts
331 ; traceTcS ("Stage result (" ++ name ++ ")") (ppr itr)
332 ; let itr' = itr { sr_new_work = sr_new_work itr
333 `unionWorkLists` accum_work }
334 ; run_pipeline stages itr' }
338 Inert: {c ~ d, F a ~ t, b ~ Int, a ~ ty} (all given)
339 Reagent: a ~ [b] (given)
341 React with (c~d) ==> IR (ContinueWith (a~[b])) True []
342 React with (F a ~ t) ==> IR (ContinueWith (a~[b])) False [F [b] ~ t]
343 React with (b ~ Int) ==> IR (ContinueWith (a~[Int]) True []
346 Inert: {c ~w d, F a ~g t, b ~w Int, a ~w ty}
349 React with (c ~w d) ==> IR (ContinueWith (a~[b])) True []
350 React with (F a ~g t) ==> IR (ContinueWith (a~[b])) True [] (can't rewrite given with wanted!)
354 Inert: {a ~ Int, F Int ~ b} (given)
355 Reagent: F a ~ b (wanted)
357 React with (a ~ Int) ==> IR (ContinueWith (F Int ~ b)) True []
358 React with (F Int ~ b) ==> IR Stop True [] -- after substituting we re-canonicalize and get nothing
361 -- Main interaction solver: we fully solve the worklist 'in one go',
362 -- returning an extended inert set.
364 -- See Note [Touchables and givens].
365 solveInteract :: InertSet -> WorkList -> TcS InertSet
366 solveInteract inert ws
367 = do { dyn_flags <- getDynFlags
368 ; solveInteractWithDepth (ctxtStkDepth dyn_flags,0,[]) inert ws
370 solveOne :: InertSet -> WorkItem -> TcS InertSet
371 solveOne inerts workItem
372 = do { dyn_flags <- getDynFlags
373 ; solveOneWithDepth (ctxtStkDepth dyn_flags,0,[]) inerts workItem
377 solveInteractWithDepth :: (Int, Int, [WorkItem])
378 -> InertSet -> WorkList -> TcS InertSet
379 solveInteractWithDepth ctxt@(max_depth,n,stack) inert ws
384 = solverDepthErrorTcS n stack
387 = do { traceTcS "solveInteractWithDepth" $
388 vcat [ text "Current depth =" <+> ppr n
389 , text "Max depth =" <+> ppr max_depth
391 ; foldlWorkListM (solveOneWithDepth ctxt) inert ws }
394 -- Fully interact the given work item with an inert set, and return a
395 -- new inert set which has assimilated the new information.
396 solveOneWithDepth :: (Int, Int, [WorkItem])
397 -> InertSet -> WorkItem -> TcS InertSet
398 solveOneWithDepth (max_depth, n, stack) inert work
399 = do { traceTcS0 (indent ++ "Solving {") (ppr work)
400 ; (new_inert, new_work) <- runSolverPipeline thePipeline inert work
402 ; traceTcS0 (indent ++ "Subgoals:") (ppr new_work)
404 -- Recursively solve the new work generated
405 -- from workItem, with a greater depth
406 ; res_inert <- solveInteractWithDepth (max_depth, n+1, work:stack)
409 ; traceTcS0 (indent ++ "Done }") (ppr work)
412 indent = replicate (2*n) ' '
414 thePipeline :: [(String,SimplifierStage)]
415 thePipeline = [ ("interact with inerts", interactWithInertsStage)
416 , ("spontaneous solve", spontaneousSolveStage)
417 , ("top-level reactions", topReactionsStage) ]
420 *********************************************************************************
422 The spontaneous-solve Stage
424 *********************************************************************************
427 spontaneousSolveStage :: SimplifierStage
428 spontaneousSolveStage workItem inerts
429 = do { mSolve <- trySpontaneousSolve workItem inerts
431 Nothing -> -- no spontaneous solution for him, keep going
432 return $ SR { sr_new_work = emptyWorkList
434 , sr_stop = ContinueWith workItem }
436 Just workList' -> -- He has been solved; workList' are all givens
437 return $ SR { sr_new_work = workList'
442 {-- This is all old code, but does not quite work now. The problem is that due to
443 Note [Loopy Spontaneous Solving] we may have unflattened a type, to be able to
444 perform a sneaky unification. This unflattening means that we may have to recanonicalize
445 a given (solved) equality, this is why the result of trySpontaneousSolve is now a list
446 of constraints (instead of an atomic solved constraint). We would have to react all of
447 them once again with the worklist but that is very tiresome. Instead we throw them back
450 | isWantedCt workItem
451 -- Original was wanted we have now made him given so
452 -- we have to ineract him with the inerts again because
453 -- of the change in his status. This may produce some work.
454 -> do { traceTcS "recursive interact with inerts {" $ vcat
455 [ text "work = " <+> ppr workItem'
456 , text "inerts = " <+> ppr inerts ]
457 ; itr_again <- interactWithInertsStage workItem' inerts
458 ; case sr_stop itr_again of
459 Stop -> pprPanic "BUG: Impossible to happen" $
460 vcat [ text "Original workitem:" <+> ppr workItem
461 , text "Spontaneously solved:" <+> ppr workItem'
462 , text "Solved was consumed, when reacting with inerts:"
463 , nest 2 (ppr inerts) ]
464 ContinueWith workItem'' -- Now *this* guy is inert wrt to inerts
465 -> do { traceTcS "end recursive interact }" $ ppr workItem''
466 ; return $ SR { sr_new_work = sr_new_work itr_again
467 , sr_inerts = sr_inerts itr_again
468 `extendInertSet` workItem''
472 -> return $ SR { sr_new_work = emptyWorkList
473 , sr_inerts = inerts `extendInertSet` workItem'
477 -- @trySpontaneousSolve wi@ solves equalities where one side is a
478 -- touchable unification variable. Returns:
479 -- * Nothing if we were not able to solve it
480 -- * Just wi' if we solved it, wi' (now a "given") should be put in the work list.
481 -- See Note [Touchables and givens]
482 -- Note, just passing the inerts through for the skolem equivalence classes
483 trySpontaneousSolve :: WorkItem -> InertSet -> TcS (Maybe SWorkList)
484 trySpontaneousSolve (CTyEqCan { cc_id = cv, cc_flavor = gw, cc_tyvar = tv1, cc_rhs = xi }) inerts
487 | Just tv2 <- tcGetTyVar_maybe xi
488 = do { tch1 <- isTouchableMetaTyVar tv1
489 ; tch2 <- isTouchableMetaTyVar tv2
490 ; case (tch1, tch2) of
491 (True, True) -> trySpontaneousEqTwoWay inerts cv gw tv1 tv2
492 (True, False) -> trySpontaneousEqOneWay inerts cv gw tv1 xi
493 (False, True) | tyVarKind tv1 `isSubKind` tyVarKind tv2
494 -> trySpontaneousEqOneWay inerts cv gw tv2 (mkTyVarTy tv1)
495 _ -> return Nothing }
497 = do { tch1 <- isTouchableMetaTyVar tv1
498 ; if tch1 then trySpontaneousEqOneWay inerts cv gw tv1 xi
499 else return Nothing }
502 -- trySpontaneousSolve (CFunEqCan ...) = ...
503 -- See Note [No touchables as FunEq RHS] in TcSMonad
504 trySpontaneousSolve _ _ = return Nothing
507 trySpontaneousEqOneWay :: InertSet -> CoVar -> CtFlavor -> TcTyVar -> Xi
508 -> TcS (Maybe SWorkList)
509 -- tv is a MetaTyVar, not untouchable
510 -- Precondition: kind(xi) is a sub-kind of kind(tv)
511 trySpontaneousEqOneWay inerts cv gw tv xi
512 | not (isSigTyVar tv) || isTyVarTy xi
513 = solveWithIdentity inerts cv gw tv xi
518 trySpontaneousEqTwoWay :: InertSet -> CoVar -> CtFlavor -> TcTyVar -> TcTyVar
519 -> TcS (Maybe SWorkList)
520 -- Both tyvars are *touchable* MetaTyvars
521 -- By the CTyEqCan invariant, k2 `isSubKind` k1
522 trySpontaneousEqTwoWay inerts cv gw tv1 tv2
524 , nicer_to_update_tv2 = solveWithIdentity inerts cv gw tv2 (mkTyVarTy tv1)
525 | otherwise = ASSERT( k2 `isSubKind` k1 )
526 solveWithIdentity inerts cv gw tv1 (mkTyVarTy tv2)
530 nicer_to_update_tv2 = isSigTyVar tv1 || isSystemName (Var.varName tv2)
533 Note [Loopy spontaneous solving]
534 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
535 Consider the original wanted:
536 wanted : Maybe (E alpha) ~ alpha
537 where E is a type family, such that E (T x) = x. After canonicalization,
538 as a result of flattening, we will get:
539 given : E alpha ~ fsk
540 wanted : alpha ~ Maybe fsk
541 where (fsk := E alpha, on the side). Now, if we spontaneously *solve*
542 (alpha := Maybe fsk) we are in trouble! Instead, we should refrain from solving
543 it and keep it as wanted. In inference mode we'll end up quantifying over
544 (alpha ~ Maybe (E alpha))
545 Hence, 'solveWithIdentity' performs a small occurs check before
546 actually solving. But this occurs check *must look through* flatten skolems.
548 However, it may be the case that the flatten skolem in hand is equal to some other
549 flatten skolem whith *does not* mention our unification variable. Here's a typical example:
554 After canonicalization:
559 After some reactions:
564 At this point, we will try to spontaneously solve (alpha ~ f2) which remains as yet unsolved.
565 We will look inside f2, which immediately mentions (F alpha), so it's not good to unify! However
566 by looking at the equivalence class of the flatten skolems, we can see that it is fine to
567 unify (alpha ~ f1) which solves our goals!
569 A similar problem happens because of other spontaneous solving. Suppose we have the
570 following wanteds, arriving in this exact order:
571 (first) w: beta ~ alpha
572 (second) w: alpha ~ fsk
573 (third) g: F beta ~ fsk
574 Then, we first spontaneously solve the first constraint, making (beta := alpha), and having
575 (beta ~ alpha) as given. *Then* we encounter the second wanted (alpha ~ fsk). "fsk" does not
576 obviously mention alpha, so naively we can also spontaneously solve (alpha := fsk). But
577 that is wrong since fsk mentions beta, which has already secretly been unified to alpha!
579 To avoid this problem, the same occurs check must unveil rewritings that can happen because
580 of spontaneously having solved other constraints.
583 Note [Avoid double unifications]
584 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
585 The spontaneous solver has to return a given which mentions the unified unification
586 variable *on the left* of the equality. Here is what happens if not:
587 Original wanted: (a ~ alpha), (alpha ~ Int)
588 We spontaneously solve the first wanted, without changing the order!
589 given : a ~ alpha [having unified alpha := a]
590 Now the second wanted comes along, but he cannot rewrite the given, so we simply continue.
591 At the end we spontaneously solve that guy, *reunifying* [alpha := Int]
593 We avoid this problem by orienting the given so that the unification
594 variable is on the left. [Note that alternatively we could attempt to
595 enforce this at canonicalization]
597 See also Note [No touchables as FunEq RHS] in TcSMonad; avoiding
598 double unifications is the main reason we disallow touchable
599 unification variables as RHS of type family equations: F xis ~ alpha.
603 solveWithIdentity :: InertSet
604 -> CoVar -> CtFlavor -> TcTyVar -> Xi
605 -> TcS (Maybe SWorkList)
606 -- Solve with the identity coercion
607 -- Precondition: kind(xi) is a sub-kind of kind(tv)
608 -- Precondition: CtFlavor is Wanted or Derived
609 -- See [New Wanted Superclass Work] to see why solveWithIdentity
610 -- must work for Derived as well as Wanted
611 solveWithIdentity inerts cv gw tv xi
612 = do { tybnds <- getTcSTyBindsMap
613 ; case occurCheck tybnds inerts tv xi of
614 Nothing -> return Nothing
615 Just (xi_unflat,coi) -> solve_with xi_unflat coi }
617 solve_with xi_unflat coi -- coi : xi_unflat ~ xi
618 = do { traceTcS "Sneaky unification:" $
619 vcat [text "Coercion variable: " <+> ppr gw,
620 text "Coercion: " <+> pprEq (mkTyVarTy tv) xi,
621 text "Left Kind is : " <+> ppr (typeKind (mkTyVarTy tv)),
622 text "Right Kind is : " <+> ppr (typeKind xi)
624 ; setWantedTyBind tv xi_unflat -- Set tv := xi_unflat
625 ; cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi_unflat xi_unflat
626 ; let flav = mkGivenFlavor gw UnkSkol
627 ; (cts, co) <- case coi of
628 ACo co -> do { can_eqs <- canEq flav cv_given (mkTyVarTy tv) xi_unflat
629 ; return (can_eqs, co) }
631 (singleCCan (CTyEqCan { cc_id = cv_given
632 , cc_flavor = mkGivenFlavor gw UnkSkol
633 , cc_tyvar = tv, cc_rhs = xi }
634 -- xi, *not* xi_unflat because
635 -- xi_unflat may require flattening!
638 Wanted {} -> setWantedCoBind cv co
639 Derived {} -> setDerivedCoBind cv co
640 _ -> pprPanic "Can't spontaneously solve *given*" empty
641 -- See Note [Avoid double unifications]
642 ; return (Just cts) }
644 occurCheck :: VarEnv (TcTyVar, TcType) -> InertSet
645 -> TcTyVar -> TcType -> Maybe (TcType,CoercionI)
646 -- Traverse @ty@ to make sure that @tv@ does not appear under some flatten skolem.
647 -- If it appears under some flatten skolem look in that flatten skolem equivalence class
648 -- (see Note [InertSet FlattenSkolemEqClass], [Loopy Spontaneous Solving]) to see if you
649 -- can find a different flatten skolem to use, that is, one that does not mention @tv@.
651 -- Postcondition: Just (ty', coi) = occurCheck binds inerts tv ty
653 -- NB: The returned type ty' may not be flat!
655 occurCheck ty_binds inerts the_tv the_ty
656 = ok emptyVarSet the_ty
658 -- If (fsk `elem` bad) then tv occurs in any rendering
659 -- of the type under the expansion of fsk
660 ok bad this_ty@(TyConApp tc tys)
661 | Just tys_cois <- allMaybes (map (ok bad) tys)
662 , (tys',cois') <- unzip tys_cois
663 = Just (TyConApp tc tys', mkTyConAppCoI tc cois')
664 | isSynTyCon tc, Just ty_expanded <- tcView this_ty
665 = ok bad ty_expanded -- See Note [Type synonyms and the occur check] in TcUnify
667 | Just (sty',coi) <- ok_pred bad sty
668 = Just (PredTy sty', coi)
669 ok bad (FunTy arg res)
670 | Just (arg', coiarg) <- ok bad arg, Just (res', coires) <- ok bad res
671 = Just (FunTy arg' res', mkFunTyCoI coiarg coires)
672 ok bad (AppTy fun arg)
673 | Just (fun', coifun) <- ok bad fun, Just (arg', coiarg) <- ok bad arg
674 = Just (AppTy fun' arg', mkAppTyCoI coifun coiarg)
675 ok bad (ForAllTy tv1 ty1)
676 -- WARNING: What if it is a (t1 ~ t2) => t3? It's not handled properly at the moment.
677 | Just (ty1', coi) <- ok bad ty1
678 = Just (ForAllTy tv1 ty1', mkForAllTyCoI tv1 coi)
681 ok bad this_ty@(TyVarTy tv)
682 | tv == the_tv = Nothing -- Occurs check error
683 | not (isTcTyVar tv) = Just (this_ty, IdCo this_ty) -- Bound var
684 | FlatSkol zty <- tcTyVarDetails tv = ok_fsk bad tv zty
685 | Just (_,ty) <- lookupVarEnv ty_binds tv = ok bad ty
686 | otherwise = Just (this_ty, IdCo this_ty)
688 -- Check if there exists a ty bind already, as a result of sneaky unification.
690 ok _bad _ty = Nothing
693 ok_pred bad (ClassP cn tys)
694 | Just tys_cois <- allMaybes $ map (ok bad) tys
695 = let (tys', cois') = unzip tys_cois
696 in Just (ClassP cn tys', mkClassPPredCoI cn cois')
697 ok_pred bad (IParam nm ty)
698 | Just (ty',co') <- ok bad ty
699 = Just (IParam nm ty', mkIParamPredCoI nm co')
700 ok_pred bad (EqPred ty1 ty2)
701 | Just (ty1',coi1) <- ok bad ty1, Just (ty2',coi2) <- ok bad ty2
702 = Just (EqPred ty1' ty2', mkEqPredCoI coi1 coi2)
703 ok_pred _ _ = Nothing
707 | fsk `elemVarSet` bad
708 -- We are already trying to find a rendering of fsk,
709 -- and to do that it seems we need a rendering, so fail
712 = firstJusts (ok new_bad zty : map (go_under_fsk new_bad) fsk_equivs)
714 fsk_equivs = getFskEqClass inerts fsk
715 new_bad = bad `extendVarSetList` (fsk : map fst fsk_equivs)
718 go_under_fsk bad_tvs (fsk,co)
719 | FlatSkol zty <- tcTyVarDetails fsk
720 = case ok bad_tvs zty of
722 Just (ty,coi') -> Just (ty, mkTransCoI coi' (ACo co))
723 | otherwise = pprPanic "go_down_equiv" (ppr fsk)
727 *********************************************************************************
729 The interact-with-inert Stage
731 *********************************************************************************
734 -- Interaction result of WorkItem <~> AtomicInert
736 = IR { ir_stop :: StopOrContinue
738 -- => Reagent (work item) consumed.
739 -- ContinueWith new_reagent
740 -- => Reagent transformed but keep gathering interactions.
741 -- The transformed item remains inert with respect
742 -- to any previously encountered inerts.
744 , ir_inert_action :: InertAction
745 -- Whether the inert item should remain in the InertSet.
747 , ir_new_work :: WorkList
748 -- new work items to add to the WorkList
751 -- What to do with the inert reactant.
752 data InertAction = KeepInert | DropInert
755 mkIRContinue :: Monad m => WorkItem -> InertAction -> WorkList -> m InteractResult
756 mkIRContinue wi keep newWork = return $ IR (ContinueWith wi) keep newWork
758 mkIRStop :: Monad m => InertAction -> WorkList -> m InteractResult
759 mkIRStop keep newWork = return $ IR Stop keep newWork
761 dischargeWorkItem :: Monad m => m InteractResult
762 dischargeWorkItem = mkIRStop KeepInert emptyCCan
764 noInteraction :: Monad m => WorkItem -> m InteractResult
765 noInteraction workItem = mkIRContinue workItem KeepInert emptyCCan
767 data WhichComesFromInert = LeftComesFromInert | RightComesFromInert
769 ---------------------------------------------------
770 -- Interact a single WorkItem with an InertSet as far as possible, i.e. until we get a Stop
771 -- result from an individual interaction (i.e. when the WorkItem is consumed), or until we've
772 -- interacted the WorkItem with the entire InertSet.
774 -- Postcondition: the new InertSet in the resulting StageResult is subset
775 -- of the input InertSet.
777 interactWithInertsStage :: SimplifierStage
778 interactWithInertsStage workItem inert
779 = foldlInertSetM interactNext initITR inert
781 initITR = SR { sr_inerts = emptyInert
782 , sr_new_work = emptyCCan
783 , sr_stop = ContinueWith workItem }
786 interactNext :: StageResult -> AtomicInert -> TcS StageResult
787 interactNext it inert
788 | ContinueWith workItem <- sr_stop it
789 = do { ir <- interactWithInert inert workItem
790 ; let inerts = sr_inerts it
791 ; return $ SR { sr_inerts = if ir_inert_action ir == KeepInert
792 then inerts `updInertSet` inert
794 , sr_new_work = sr_new_work it `unionWorkLists` ir_new_work ir
795 , sr_stop = ir_stop ir } }
796 | otherwise = return $ itrAddInert inert it
799 itrAddInert :: AtomicInert -> StageResult -> StageResult
800 itrAddInert inert itr = itr { sr_inerts = (sr_inerts itr) `updInertSet` inert }
802 -- Do a single interaction of two constraints.
803 interactWithInert :: AtomicInert -> WorkItem -> TcS InteractResult
804 interactWithInert inert workitem
805 = do { ctxt <- getTcSContext
806 ; let is_allowed = allowedInteraction (simplEqsOnly ctxt) inert workitem
807 inert_ev = cc_id inert
808 work_ev = cc_id workitem
810 -- Never interact a wanted and a derived where the derived's evidence
811 -- mentions the wanted evidence in an unguarded way.
812 -- See Note [Superclasses and recursive dictionaries]
813 -- and Note [New Wanted Superclass Work]
814 -- We don't have to do this for givens, as we fully know the evidence for them.
816 case (cc_flavor inert, cc_flavor workitem) of
817 (Wanted loc, Derived _) -> isGoodRecEv work_ev (WantedEvVar inert_ev loc)
818 (Derived _, Wanted loc) -> isGoodRecEv inert_ev (WantedEvVar work_ev loc)
821 ; if is_allowed && rec_ev_ok then
822 doInteractWithInert inert workitem
824 noInteraction workitem
827 allowedInteraction :: Bool -> AtomicInert -> WorkItem -> Bool
828 -- Allowed interactions
829 allowedInteraction eqs_only (CDictCan {}) (CDictCan {}) = not eqs_only
830 allowedInteraction eqs_only (CIPCan {}) (CIPCan {}) = not eqs_only
831 allowedInteraction _ _ _ = True
833 --------------------------------------------
834 doInteractWithInert :: CanonicalCt -> CanonicalCt -> TcS InteractResult
835 -- Identical class constraints.
838 (CDictCan { cc_id = d1, cc_flavor = fl1, cc_class = cls1, cc_tyargs = tys1 })
839 workItem@(CDictCan { cc_id = d2, cc_flavor = fl2, cc_class = cls2, cc_tyargs = tys2 })
840 | cls1 == cls2 && (and $ zipWith tcEqType tys1 tys2)
841 = solveOneFromTheOther (d1,fl1) workItem
843 | cls1 == cls2 && (not (isGiven fl1 && isGiven fl2))
844 = -- See Note [When improvement happens]
845 do { let work_item_pred_loc = (ClassP cls2 tys2, ppr d2)
846 inert_pred_loc = (ClassP cls1 tys1, ppr d1)
847 loc = combineCtLoc fl1 fl2
848 eqn_pred_locs = improveFromAnother work_item_pred_loc inert_pred_loc
849 ; wevvars <- mkWantedFunDepEqns loc eqn_pred_locs
850 -- See Note [Generating extra equalities]
851 ; workList <- canWanteds wevvars
852 ; mkIRContinue workItem KeepInert workList -- Keep the inert there so we avoid
853 -- re-introducing the fundep equalities
854 -- See Note [FunDep Reactions]
857 -- Class constraint and given equality: use the equality to rewrite
858 -- the class constraint.
859 doInteractWithInert (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi })
860 (CDictCan { cc_id = dv, cc_flavor = wfl, cc_class = cl, cc_tyargs = xis })
861 | ifl `canRewrite` wfl
862 , tv `elemVarSet` tyVarsOfTypes xis
863 -- substitute for tv in xis. Note that the resulting class
864 -- constraint is still canonical, since substituting xi-types in
865 -- xi-types generates xi-types. However, it may no longer be
866 -- inert with respect to the inert set items we've already seen.
867 -- For example, consider the inert set
872 -- and the work item D a (w). D a does not interact with D Int.
873 -- Next, it does interact with a ~g Int, getting rewritten to D
874 -- Int (w). But now we must go back through the rest of the inert
875 -- set again, to find that it can now be discharged by the given D
877 = do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,wfl,cl,xis)
878 ; mkIRStop KeepInert (singleCCan rewritten_dict) }
880 doInteractWithInert (CDictCan { cc_id = dv, cc_flavor = ifl, cc_class = cl, cc_tyargs = xis })
881 workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
882 | wfl `canRewrite` ifl
883 , tv `elemVarSet` tyVarsOfTypes xis
884 = do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,ifl,cl,xis)
885 ; mkIRContinue workItem DropInert (singleCCan rewritten_dict) }
887 -- Class constraint and given equality: use the equality to rewrite
888 -- the class constraint.
889 doInteractWithInert (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi })
890 (CIPCan { cc_id = ipid, cc_flavor = wfl, cc_ip_nm = nm, cc_ip_ty = ty })
891 | ifl `canRewrite` wfl
892 , tv `elemVarSet` tyVarsOfType ty
893 = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,wfl,nm,ty)
894 ; mkIRStop KeepInert (singleCCan rewritten_ip) }
896 doInteractWithInert (CIPCan { cc_id = ipid, cc_flavor = ifl, cc_ip_nm = nm, cc_ip_ty = ty })
897 workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
898 | wfl `canRewrite` ifl
899 , tv `elemVarSet` tyVarsOfType ty
900 = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,ifl,nm,ty)
901 ; mkIRContinue workItem DropInert (singleCCan rewritten_ip) }
903 -- Two implicit parameter constraints. If the names are the same,
904 -- but their types are not, we generate a wanted type equality
905 -- that equates the type (this is "improvement").
906 -- However, we don't actually need the coercion evidence,
907 -- so we just generate a fresh coercion variable that isn't used anywhere.
908 doInteractWithInert (CIPCan { cc_id = id1, cc_flavor = ifl, cc_ip_nm = nm1, cc_ip_ty = ty1 })
909 workItem@(CIPCan { cc_flavor = wfl, cc_ip_nm = nm2, cc_ip_ty = ty2 })
910 | nm1 == nm2 && isGiven wfl && isGiven ifl
911 = -- See Note [Overriding implicit parameters]
912 -- Dump the inert item, override totally with the new one
913 -- Do not require type equality
914 mkIRContinue workItem DropInert emptyCCan
916 | nm1 == nm2 && ty1 `tcEqType` ty2
917 = solveOneFromTheOther (id1,ifl) workItem
920 = -- See Note [When improvement happens]
921 do { co_var <- newWantedCoVar ty1 ty2
922 ; let flav = Wanted (combineCtLoc ifl wfl)
923 ; mkCanonical flav co_var >>= mkIRContinue workItem KeepInert }
926 -- Inert: equality, work item: function equality
928 -- Never rewrite a given with a wanted equality, and a type function
929 -- equality can never rewrite an equality. Note also that if we have
930 -- F x1 ~ x2 and a ~ x3, and a occurs in x2, we don't rewrite it. We
931 -- can wait until F x1 ~ x2 matches another F x1 ~ x4, and only then
932 -- we will ``expose'' x2 and x4 to rewriting.
934 -- Otherwise, we can try rewriting the type function equality with the equality.
935 doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi1 })
936 (CFunEqCan { cc_id = cv2, cc_flavor = wfl, cc_fun = tc
937 , cc_tyargs = args, cc_rhs = xi2 })
938 | ifl `canRewrite` wfl
939 , tv `elemVarSet` tyVarsOfTypes args
940 = do { rewritten_funeq <- rewriteFunEq (cv1,tv,xi1) (cv2,wfl,tc,args,xi2)
941 ; mkIRStop KeepInert (singleCCan rewritten_funeq) }
943 -- Inert: function equality, work item: equality
945 doInteractWithInert (CFunEqCan {cc_id = cv1, cc_flavor = ifl, cc_fun = tc
946 , cc_tyargs = args, cc_rhs = xi1 })
947 workItem@(CTyEqCan { cc_id = cv2, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi2 })
948 | wfl `canRewrite` ifl
949 , tv `elemVarSet` tyVarsOfTypes args
950 = do { rewritten_funeq <- rewriteFunEq (cv2,tv,xi2) (cv1,ifl,tc,args,xi1)
951 ; mkIRContinue workItem DropInert (singleCCan rewritten_funeq) }
953 doInteractWithInert (CFunEqCan { cc_id = cv1, cc_flavor = fl1, cc_fun = tc1
954 , cc_tyargs = args1, cc_rhs = xi1 })
955 workItem@(CFunEqCan { cc_id = cv2, cc_flavor = fl2, cc_fun = tc2
956 , cc_tyargs = args2, cc_rhs = xi2 })
957 | fl1 `canRewrite` fl2 && lhss_match
958 = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
959 ; mkIRStop KeepInert cans }
960 | fl2 `canRewrite` fl1 && lhss_match
961 = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
962 ; mkIRContinue workItem DropInert cans }
964 lhss_match = tc1 == tc2 && and (zipWith tcEqType args1 args2)
967 inert@(CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
968 workItem@(CTyEqCan { cc_id = cv2, cc_flavor = fl2, cc_tyvar = tv2, cc_rhs = xi2 })
969 -- Check for matching LHS
970 | fl1 `canRewrite` fl2 && tv1 == tv2
971 = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
972 ; mkIRStop KeepInert cans }
974 | fl2 `canRewrite` fl1 && tv1 == tv2
975 = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
976 ; mkIRContinue workItem DropInert cans }
978 -- Check for rewriting RHS
979 | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfType xi2
980 = do { rewritten_eq <- rewriteEqRHS (cv1,tv1,xi1) (cv2,fl2,tv2,xi2)
981 ; mkIRStop KeepInert rewritten_eq }
982 | fl2 `canRewrite` fl1 && tv2 `elemVarSet` tyVarsOfType xi1
983 = do { rewritten_eq <- rewriteEqRHS (cv2,tv2,xi2) (cv1,fl1,tv1,xi1)
984 ; mkIRContinue workItem DropInert rewritten_eq }
986 -- Finally, if workitem is a Flatten Equivalence Class constraint and the
987 -- inert is a wanted constraint, even when the workitem cannot rewrite the
988 -- inert, drop the inert out because you may have to reconsider solving the
989 -- inert *using* the equivalence class you created. See note [Loopy Spontaneous Solving]
990 -- and [InertSet FlattenSkolemEqClass]
992 | not $ isGiven fl1, -- The inert is wanted or derived
993 isMetaTyVar tv1, -- and has a unification variable lhs
994 FlatSkol {} <- tcTyVarDetails tv2, -- And workitem is a flatten skolem equality
995 Just tv2' <- tcGetTyVar_maybe xi2, FlatSkol {} <- tcTyVarDetails tv2'
996 = mkIRContinue workItem DropInert (singletonWorkList inert)
999 -- Fall-through case for all other situations
1000 doInteractWithInert _ workItem = noInteraction workItem
1002 --------------------------------------------
1003 combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
1004 -- Precondition: At least one of them should be wanted
1005 combineCtLoc (Wanted loc) _ = loc
1006 combineCtLoc _ (Wanted loc) = loc
1007 combineCtLoc _ _ = panic "Expected one of wanted constraints (BUG)"
1010 -- Equational Rewriting
1011 rewriteDict :: (CoVar, TcTyVar, Xi) -> (DictId, CtFlavor, Class, [Xi]) -> TcS CanonicalCt
1012 rewriteDict (cv,tv,xi) (dv,gw,cl,xis)
1013 = do { let cos = substTysWith [tv] [mkCoVarCoercion cv] xis -- xis[tv] ~ xis[xi]
1014 args = substTysWith [tv] [xi] xis
1016 dict_co = mkTyConCoercion con cos
1017 ; dv' <- newDictVar cl args
1019 Wanted {} -> setDictBind dv (EvCast dv' (mkSymCoercion dict_co))
1020 _given_or_derived -> setDictBind dv' (EvCast dv dict_co)
1021 ; return (CDictCan { cc_id = dv'
1024 , cc_tyargs = args }) }
1026 rewriteIP :: (CoVar,TcTyVar,Xi) -> (EvVar,CtFlavor, IPName Name, TcType) -> TcS CanonicalCt
1027 rewriteIP (cv,tv,xi) (ipid,gw,nm,ty)
1028 = do { let ip_co = substTyWith [tv] [mkCoVarCoercion cv] ty -- ty[tv] ~ t[xi]
1029 ty' = substTyWith [tv] [xi] ty
1030 ; ipid' <- newIPVar nm ty'
1032 Wanted {} -> setIPBind ipid (EvCast ipid' (mkSymCoercion ip_co))
1033 _given_or_derived -> setIPBind ipid' (EvCast ipid ip_co)
1034 ; return (CIPCan { cc_id = ipid'
1037 , cc_ip_ty = ty' }) }
1039 rewriteFunEq :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TyCon, [Xi], Xi) -> TcS CanonicalCt
1040 rewriteFunEq (cv1,tv,xi1) (cv2,gw, tc,args,xi2)
1041 = do { let arg_cos = substTysWith [tv] [mkCoVarCoercion cv1] args
1042 args' = substTysWith [tv] [xi1] args
1043 fun_co = mkTyConCoercion tc arg_cos
1044 ; cv2' <- case gw of
1045 Wanted {} -> do { cv2' <- newWantedCoVar (mkTyConApp tc args') xi2
1046 ; setWantedCoBind cv2 $
1047 mkTransCoercion fun_co (mkCoVarCoercion cv2')
1049 _giv_or_der -> newGivOrDerCoVar (mkTyConApp tc args') xi2 $
1050 mkTransCoercion (mkSymCoercion fun_co) (mkCoVarCoercion cv2)
1051 ; return (CFunEqCan { cc_id = cv2'
1058 rewriteEqRHS :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TcTyVar,Xi) -> TcS CanonicalCts
1059 -- Use the first equality to rewrite the second, flavors already checked.
1060 -- E.g. c1 : tv1 ~ xi1 c2 : tv2 ~ xi2
1061 -- rewrites c2 to give
1062 -- c2' : tv2 ~ xi2[xi1/tv1]
1063 -- We must do an occurs check to sure the new constraint is canonical
1064 -- So we might return an empty bag
1065 rewriteEqRHS (cv1,tv1,xi1) (cv2,gw,tv2,xi2)
1066 | Just tv2' <- tcGetTyVar_maybe xi2'
1067 , tv2 == tv2' -- In this case xi2[xi1/tv1] = tv2, so we have tv2~tv2
1068 = do { when (isWanted gw) (setWantedCoBind cv2 (mkSymCoercion co2'))
1069 ; return emptyCCan }
1074 -> do { cv2' <- newWantedCoVar (mkTyVarTy tv2) xi2'
1075 ; setWantedCoBind cv2 $
1076 mkCoVarCoercion cv2' `mkTransCoercion` mkSymCoercion co2'
1079 -> newGivOrDerCoVar (mkTyVarTy tv2) xi2' $
1080 mkCoVarCoercion cv2 `mkTransCoercion` co2'
1082 ; xi2'' <- canOccursCheck gw tv2 xi2' -- we know xi2' is *not* tv2
1083 ; return (singleCCan $ CTyEqCan { cc_id = cv2'
1089 xi2' = substTyWith [tv1] [xi1] xi2
1090 co2' = substTyWith [tv1] [mkCoVarCoercion cv1] xi2 -- xi2 ~ xi2[xi1/tv1]
1093 rewriteEqLHS :: WhichComesFromInert -> (Coercion,Xi) -> (CoVar,CtFlavor,Xi) -> TcS CanonicalCts
1094 -- Used to ineratct two equalities of the following form:
1095 -- First Equality: co1: (XXX ~ xi1)
1096 -- Second Equality: cv2: (XXX ~ xi2)
1097 -- Where the cv1 `canRewrite` cv2 equality
1098 -- We have an option of creating new work (xi1 ~ xi2) OR (xi2 ~ xi1). This
1099 -- depends on whether the left or the right equality comes from the inert set.
1101 -- prefer to create (xi2 ~ xi1) if the first comes from the inert
1102 -- prefer to create (xi1 ~ xi2) if the second comes from the inert
1103 rewriteEqLHS which (co1,xi1) (cv2,gw,xi2)
1104 = do { cv2' <- case (isWanted gw, which) of
1105 (True,LeftComesFromInert) ->
1106 do { cv2' <- newWantedCoVar xi2 xi1
1107 ; setWantedCoBind cv2 $
1108 co1 `mkTransCoercion` mkSymCoercion (mkCoVarCoercion cv2')
1110 (True,RightComesFromInert) ->
1111 do { cv2' <- newWantedCoVar xi1 xi2
1112 ; setWantedCoBind cv2 $
1113 co1 `mkTransCoercion` mkCoVarCoercion cv2'
1115 (False,LeftComesFromInert) ->
1116 newGivOrDerCoVar xi2 xi1 $
1117 mkSymCoercion (mkCoVarCoercion cv2) `mkTransCoercion` co1
1118 (False,RightComesFromInert) ->
1119 newGivOrDerCoVar xi1 xi2 $
1120 mkSymCoercion co1 `mkTransCoercion` mkCoVarCoercion cv2
1121 ; mkCanonical gw cv2' }
1125 solveOneFromTheOther :: (EvVar, CtFlavor) -> CanonicalCt -> TcS InteractResult
1126 -- First argument inert, second argument workitem. They both represent
1127 -- wanted/given/derived evidence for the *same* predicate so we try here to
1128 -- discharge one directly from the other.
1130 -- Precondition: value evidence only (implicit parameters, classes)
1132 solveOneFromTheOther (iid,ifl) workItem
1133 -- Both derived needs a special case. You might think that we do not need
1134 -- two evidence terms for the same claim. But, since the evidence is partial,
1135 -- either evidence may do in some cases; see TcSMonad.isGoodRecEv.
1136 -- See also Example 3 in Note [Superclasses and recursive dictionaries]
1137 | isDerived ifl && isDerived wfl
1138 = noInteraction workItem
1140 | ifl `canRewrite` wfl
1141 = do { unless (isGiven wfl) $ setEvBind wid (EvId iid)
1142 -- Overwrite the binding, if one exists
1143 -- For Givens, which are lambda-bound, nothing to overwrite,
1144 ; dischargeWorkItem }
1146 | otherwise -- wfl `canRewrite` ifl
1147 = do { unless (isGiven ifl) $ setEvBind iid (EvId wid)
1148 ; mkIRContinue workItem DropInert emptyCCan }
1151 wfl = cc_flavor workItem
1152 wid = cc_id workItem
1155 Note [Superclasses and recursive dictionaries]
1156 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1157 Overlaps with Note [SUPERCLASS-LOOP 1]
1158 Note [SUPERCLASS-LOOP 2]
1159 Note [Recursive instances and superclases]
1160 ToDo: check overlap and delete redundant stuff
1162 Right before adding a given into the inert set, we must
1163 produce some more work, that will bring the superclasses
1164 of the given into scope. The superclass constraints go into
1167 When we simplify a wanted constraint, if we first see a matching
1168 instance, we may produce new wanted work. To (1) avoid doing this work
1169 twice in the future and (2) to handle recursive dictionaries we may ``cache''
1170 this item as solved (in effect, given) into our inert set and with that add
1171 its superclass constraints (as given) in our worklist.
1173 But now we have added partially solved constraints to the worklist which may
1174 interact with other wanteds. Consider the example:
1178 class Eq b => Foo a b --- 0-th selector
1179 instance Eq a => Foo [a] a --- fooDFun
1181 and wanted (Foo [t] t). We are first going to see that the instance matches
1182 and create an inert set that includes the solved (Foo [t] t) and its
1184 d1 :_g Foo [t] t d1 := EvDFunApp fooDFun d3
1185 d2 :_g Eq t d2 := EvSuperClass d1 0
1186 Our work list is going to contain a new *wanted* goal
1188 It is wrong to react the wanted (Eq t) with the given (Eq t) because that would
1189 construct loopy evidence. Hence the check isGoodRecEv in doInteractWithInert.
1191 OK, so we have ruled out bad behaviour, but how do we ge recursive dictionaries,
1196 data D r = ZeroD | SuccD (r (D r));
1198 instance (Eq (r (D r))) => Eq (D r) where
1199 ZeroD == ZeroD = True
1200 (SuccD a) == (SuccD b) = a == b
1203 equalDC :: D [] -> D [] -> Bool;
1206 We need to prove (Eq (D [])). Here's how we go:
1210 by instance decl, holds if
1214 *BUT* we have an inert set which gives us (no superclasses):
1216 By the instance declaration of Eq we can show the 'd2' goal if
1218 where d2 = dfEqList d3
1220 Now, however this wanted can interact with our inert d1 to set:
1222 and solve the goal. Why was this interaction OK? Because, if we chase the
1223 evidence of d1 ~~> dfEqD d2 ~~-> dfEqList d3, so by setting d3 := d1 we
1225 d3 := dfEqD2 (dfEqList d3)
1226 which is FINE because the use of d3 is protected by the instance function
1229 So, our strategy is to try to put solved wanted dictionaries into the
1230 inert set along with their superclasses (when this is meaningful,
1231 i.e. when new wanted goals are generated) but solve a wanted dictionary
1232 from a given only in the case where the evidence variable of the
1233 wanted is mentioned in the evidence of the given (recursively through
1234 the evidence binds) in a protected way: more instance function applications
1235 than superclass selectors.
1237 Here are some more examples from GHC's previous type checker
1241 This code arises in the context of "Scrap Your Boilerplate with Class"
1245 instance Sat (ctx Char) => Data ctx Char -- dfunData1
1246 instance (Sat (ctx [a]), Data ctx a) => Data ctx [a] -- dfunData2
1248 class Data Maybe a => Foo a
1250 instance Foo t => Sat (Maybe t) -- dfunSat
1252 instance Data Maybe a => Foo a -- dfunFoo1
1253 instance Foo a => Foo [a] -- dfunFoo2
1254 instance Foo [Char] -- dfunFoo3
1256 Consider generating the superclasses of the instance declaration
1257 instance Foo a => Foo [a]
1259 So our problem is this
1261 d1 :_w Data Maybe [t]
1263 We may add the given in the inert set, along with its superclasses
1264 [assuming we don't fail because there is a matching instance, see
1265 tryTopReact, given case ]
1269 d01 :_g Data Maybe t -- d2 := EvDictSuperClass d0 0
1270 d1 :_w Data Maybe [t]
1271 Then d2 can readily enter the inert, and we also do solving of the wanted
1274 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1276 d2 :_w Sat (Maybe [t])
1278 d01 :_g Data Maybe t
1279 Now, we may simplify d2 more:
1282 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1283 d1 :_g Data Maybe [t]
1284 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1288 d01 :_g Data Maybe t
1290 Now, we can just solve d3.
1293 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1294 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1297 d01 :_g Data Maybe t
1298 And now we can simplify d4 again, but since it has superclasses we *add* them to the worklist:
1301 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1302 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1303 d4 :_g Foo [t] d4 := dfunFoo2 d5
1306 d6 :_g Data Maybe [t] d6 := EvDictSuperClass d4 0
1307 d01 :_g Data Maybe t
1308 Now, d5 can be solved! (and its superclass enter scope)
1311 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1312 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1313 d4 :_g Foo [t] d4 := dfunFoo2 d5
1314 d5 :_g Foo t d5 := dfunFoo1 d7
1317 d6 :_g Data Maybe [t]
1318 d8 :_g Data Maybe t d8 := EvDictSuperClass d5 0
1319 d01 :_g Data Maybe t
1322 [1] Suppose we pick d8 and we react him with d01. Which of the two givens should
1323 we keep? Well, we *MUST NOT* drop d01 because d8 contains recursive evidence
1324 that must not be used (look at case interactInert where both inert and workitem
1325 are givens). So we have several options:
1326 - Drop the workitem always (this will drop d8)
1327 This feels very unsafe -- what if the work item was the "good" one
1328 that should be used later to solve another wanted?
1329 - Don't drop anyone: the inert set may contain multiple givens!
1330 [This is currently implemented]
1332 The "don't drop anyone" seems the most safe thing to do, so now we come to problem 2:
1333 [2] We have added both d6 and d01 in the inert set, and we are interacting our wanted
1334 d7. Now the [isRecDictEv] function in the ineration solver
1335 [case inert-given workitem-wanted] will prevent us from interacting d7 := d8
1336 precisely because chasing the evidence of d8 leads us to an unguarded use of d7.
1338 So, no interaction happens there. Then we meet d01 and there is no recursion
1339 problem there [isRectDictEv] gives us the OK to interact and we do solve d7 := d01!
1341 Note [SUPERCLASS-LOOP 1]
1342 ~~~~~~~~~~~~~~~~~~~~~~~~
1343 We have to be very, very careful when generating superclasses, lest we
1344 accidentally build a loop. Here's an example:
1348 class S a => C a where { opc :: a -> a }
1349 class S b => D b where { opd :: b -> b }
1351 instance C Int where
1354 instance D Int where
1357 From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int}
1358 Simplifying, we may well get:
1359 $dfCInt = :C ds1 (opd dd)
1362 Notice that we spot that we can extract ds1 from dd.
1364 Alas! Alack! We can do the same for (instance D Int):
1366 $dfDInt = :D ds2 (opc dc)
1370 And now we've defined the superclass in terms of itself.
1371 Two more nasty cases are in
1376 - Satisfy the superclass context *all by itself*
1377 (tcSimplifySuperClasses)
1378 - And do so completely; i.e. no left-over constraints
1379 to mix with the constraints arising from method declarations
1382 Note [SUPERCLASS-LOOP 2]
1383 ~~~~~~~~~~~~~~~~~~~~~~~~
1384 We need to be careful when adding "the constaint we are trying to prove".
1385 Suppose we are *given* d1:Ord a, and want to deduce (d2:C [a]) where
1387 class Ord a => C a where
1388 instance Ord [a] => C [a] where ...
1390 Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the
1391 superclasses of C [a] to avails. But we must not overwrite the binding
1392 for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
1395 Here's another variant, immortalised in tcrun020
1396 class Monad m => C1 m
1397 class C1 m => C2 m x
1398 instance C2 Maybe Bool
1399 For the instance decl we need to build (C1 Maybe), and it's no good if
1400 we run around and add (C2 Maybe Bool) and its superclasses to the avails
1401 before we search for C1 Maybe.
1403 Here's another example
1404 class Eq b => Foo a b
1405 instance Eq a => Foo [a] a
1409 we'll first deduce that it holds (via the instance decl). We must not
1410 then overwrite the Eq t constraint with a superclass selection!
1412 At first I had a gross hack, whereby I simply did not add superclass constraints
1413 in addWanted, though I did for addGiven and addIrred. This was sub-optimal,
1414 becuase it lost legitimate superclass sharing, and it still didn't do the job:
1415 I found a very obscure program (now tcrun021) in which improvement meant the
1416 simplifier got two bites a the cherry... so something seemed to be an Stop
1417 first time, but reducible next time.
1419 Now we implement the Right Solution, which is to check for loops directly
1420 when adding superclasses. It's a bit like the occurs check in unification.
1422 Note [Recursive instances and superclases]
1423 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1424 Consider this code, which arises in the context of "Scrap Your
1425 Boilerplate with Class".
1429 instance Sat (ctx Char) => Data ctx Char
1430 instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]
1432 class Data Maybe a => Foo a
1434 instance Foo t => Sat (Maybe t)
1436 instance Data Maybe a => Foo a
1437 instance Foo a => Foo [a]
1440 In the instance for Foo [a], when generating evidence for the superclasses
1441 (ie in tcSimplifySuperClasses) we need a superclass (Data Maybe [a]).
1442 Using the instance for Data, we therefore need
1443 (Sat (Maybe [a], Data Maybe a)
1444 But we are given (Foo a), and hence its superclass (Data Maybe a).
1445 So that leaves (Sat (Maybe [a])). Using the instance for Sat means
1446 we need (Foo [a]). And that is the very dictionary we are bulding
1447 an instance for! So we must put that in the "givens". So in this
1449 Given: Foo a, Foo [a]
1450 Wanted: Data Maybe [a]
1452 BUT we must *not not not* put the *superclasses* of (Foo [a]) in
1453 the givens, which is what 'addGiven' would normally do. Why? Because
1454 (Data Maybe [a]) is the superclass, so we'd "satisfy" the wanted
1455 by selecting a superclass from Foo [a], which simply makes a loop.
1457 On the other hand we *must* put the superclasses of (Foo a) in
1458 the givens, as you can see from the derivation described above.
1460 Conclusion: in the very special case of tcSimplifySuperClasses
1461 we have one 'given' (namely the "this" dictionary) whose superclasses
1462 must not be added to 'givens' by addGiven.
1464 There is a complication though. Suppose there are equalities
1465 instance (Eq a, a~b) => Num (a,b)
1466 Then we normalise the 'givens' wrt the equalities, so the original
1467 given "this" dictionary is cast to one of a different type. So it's a
1468 bit trickier than before to identify the "special" dictionary whose
1469 superclasses must not be added. See test
1470 indexed-types/should_run/EqInInstance
1472 We need a persistent property of the dictionary to record this
1473 special-ness. Current I'm using the InstLocOrigin (a bit of a hack,
1474 but cool), which is maintained by dictionary normalisation.
1475 Specifically, the InstLocOrigin is
1477 then the no-superclass thing kicks in. WATCH OUT if you fiddle
1480 Note [MATCHING-SYNONYMS]
1481 ~~~~~~~~~~~~~~~~~~~~~~~~
1482 When trying to match a dictionary (D tau) to a top-level instance, or a
1483 type family equation (F taus_1 ~ tau_2) to a top-level family instance,
1484 we do *not* need to expand type synonyms because the matcher will do that for us.
1487 Note [RHS-FAMILY-SYNONYMS]
1488 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1489 The RHS of a family instance is represented as yet another constructor which is
1490 like a type synonym for the real RHS the programmer declared. Eg:
1491 type instance F (a,a) = [a]
1493 :R32 a = [a] -- internal type synonym introduced
1494 F (a,a) ~ :R32 a -- instance
1496 When we react a family instance with a type family equation in the work list
1497 we keep the synonym-using RHS without expansion.
1500 *********************************************************************************
1502 The top-reaction Stage
1504 *********************************************************************************
1507 -- If a work item has any form of interaction with top-level we get this
1508 data TopInteractResult
1509 = NoTopInt -- No top-level interaction
1511 { tir_new_work :: WorkList -- Sub-goals or new work (could be given,
1512 -- for superclasses)
1513 , tir_new_inert :: StopOrContinue -- The input work item, ready to become *inert* now:
1514 } -- NB: in ``given'' (solved) form if the
1515 -- original was wanted or given and instance match
1516 -- was found, but may also be in wanted form if we
1517 -- only reacted with functional dependencies
1518 -- arising from top-level instances.
1520 topReactionsStage :: SimplifierStage
1521 topReactionsStage workItem inerts
1522 = do { tir <- tryTopReact workItem
1525 return $ SR { sr_inerts = inerts
1526 , sr_new_work = emptyWorkList
1527 , sr_stop = ContinueWith workItem }
1528 SomeTopInt tir_new_work tir_new_inert ->
1529 return $ SR { sr_inerts = inerts
1530 , sr_new_work = tir_new_work
1531 , sr_stop = tir_new_inert
1535 tryTopReact :: WorkItem -> TcS TopInteractResult
1536 tryTopReact workitem
1537 = do { -- A flag controls the amount of interaction allowed
1538 -- See Note [Simplifying RULE lhs constraints]
1539 ctxt <- getTcSContext
1540 ; if allowedTopReaction (simplEqsOnly ctxt) workitem
1541 then do { traceTcS "tryTopReact / calling doTopReact" (ppr workitem)
1542 ; doTopReact workitem }
1543 else return NoTopInt
1546 allowedTopReaction :: Bool -> WorkItem -> Bool
1547 allowedTopReaction eqs_only (CDictCan {}) = not eqs_only
1548 allowedTopReaction _ _ = True
1551 doTopReact :: WorkItem -> TcS TopInteractResult
1552 -- The work item does not react with the inert set,
1553 -- so try interaction with top-level instances
1554 doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Wanted loc
1555 , cc_class = cls, cc_tyargs = xis })
1556 = do { -- See Note [MATCHING-SYNONYMS]
1557 ; lkp_inst_res <- matchClassInst cls xis loc
1558 ; case lkp_inst_res of
1559 NoInstance -> do { traceTcS "doTopReact/ no class instance for" (ppr dv)
1561 GenInst wtvs ev_term -> -- Solved
1562 -- No need to do fundeps stuff here; the instance
1563 -- matches already so we won't get any more info
1564 -- from functional dependencies
1565 do { traceTcS "doTopReact/ found class instance for" (ppr dv)
1566 ; setDictBind dv ev_term
1567 ; workList <- canWanteds wtvs
1569 -- Solved in one step and no new wanted work produced.
1570 -- i.e we directly matched a top-level instance
1571 -- No point in caching this in 'inert', nor in adding superclasses
1572 then return $ SomeTopInt { tir_new_work = emptyCCan
1573 , tir_new_inert = Stop }
1575 -- Solved and new wanted work produced, you may cache the
1576 -- (tentatively solved) dictionary as Derived and its superclasses
1577 else do { let solved = makeSolved workItem
1578 ; sc_work <- newSCWorkFromFlavored dv (Derived loc) cls xis
1579 ; return $ SomeTopInt
1580 { tir_new_work = workList `unionWorkLists` sc_work
1581 , tir_new_inert = ContinueWith solved } }
1585 -- Try for a fundep reaction beween the wanted item
1586 -- and a top-level instance declaration
1588 = do { instEnvs <- getInstEnvs
1589 ; let eqn_pred_locs = improveFromInstEnv (classInstances instEnvs)
1590 (ClassP cls xis, ppr dv)
1591 ; wevvars <- mkWantedFunDepEqns loc eqn_pred_locs
1592 -- NB: fundeps generate some wanted equalities, but
1593 -- we don't use their evidence for anything
1594 ; fd_work <- canWanteds wevvars
1595 ; sc_work <- newSCWorkFromFlavored dv (Derived loc) cls xis
1596 ; return $ SomeTopInt { tir_new_work = fd_work `unionWorkLists` sc_work
1597 , tir_new_inert = ContinueWith workItem }
1598 -- NB: workItem is inert, but it isn't solved
1599 -- keep it as inert, although it's not solved because we
1600 -- have now reacted all its top-level fundep-induced equalities!
1602 -- See Note [FunDep Reactions]
1605 -- Otherwise, we have a given or derived
1606 doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = fl
1607 , cc_class = cls, cc_tyargs = xis })
1608 = do { sc_work <- newSCWorkFromFlavored dv fl cls xis
1609 ; return $ SomeTopInt sc_work (ContinueWith workItem) }
1610 -- See Note [Given constraint that matches an instance declaration]
1613 doTopReact (CFunEqCan { cc_id = cv, cc_flavor = fl
1614 , cc_fun = tc, cc_tyargs = args, cc_rhs = xi })
1615 = ASSERT (isSynFamilyTyCon tc) -- No associated data families have reached that far
1616 do { match_res <- matchFam tc args -- See Note [MATCHING-SYNONYMS]
1620 MatchInstSingle (rep_tc, rep_tys)
1621 -> do { let Just coe_tc = tyConFamilyCoercion_maybe rep_tc
1622 Just rhs_ty = tcView (mkTyConApp rep_tc rep_tys)
1623 -- Eagerly expand away the type synonym on the
1624 -- RHS of a type function, so that it never
1625 -- appears in an error message
1626 -- See Note [Type synonym families] in TyCon
1627 coe = mkTyConApp coe_tc rep_tys
1629 Wanted {} -> do { cv' <- newWantedCoVar rhs_ty xi
1630 ; setWantedCoBind cv $
1631 coe `mkTransCoercion`
1634 _ -> newGivOrDerCoVar xi rhs_ty $
1635 mkSymCoercion (mkCoVarCoercion cv) `mkTransCoercion` coe
1637 ; workList <- mkCanonical fl cv'
1638 ; return $ SomeTopInt workList Stop }
1640 -> panicTcS $ text "TcSMonad.matchFam returned multiple instances!"
1644 -- Any other work item does not react with any top-level equations
1645 doTopReact _workItem = return NoTopInt
1648 Note [FunDep and implicit parameter reactions]
1649 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1650 Currently, our story of interacting two dictionaries (or a dictionary
1651 and top-level instances) for functional dependencies, and implicit
1652 paramters, is that we simply produce new wanted equalities. So for example
1654 class D a b | a -> b where ...
1660 We generate the extra work item
1662 where 'cv' is currently unused. However, this new item reacts with d2,
1663 discharging it in favour of a new constraint d2' thus:
1665 d2 := d2' |> D Int cv
1666 Now d2' can be discharged from d1
1668 We could be more aggressive and try to *immediately* solve the dictionary
1669 using those extra equalities. With the same inert set and work item we
1670 might dischard d2 directly:
1673 d2 := d1 |> D Int cv
1675 But in general it's a bit painful to figure out the necessary coercion,
1676 so we just take the first approach.
1678 It's exactly the same with implicit parameters, except that the
1679 "aggressive" approach would be much easier to implement.
1681 Note [When improvement happens]
1682 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1683 We fire an improvement rule when
1685 * Two constraints match (modulo the fundep)
1686 e.g. C t1 t2, C t1 t3 where C a b | a->b
1687 The two match because the first arg is identical
1689 * At least one is not Given. If they are both given, we don't fire
1690 the reaction because we have no way of constructing evidence for a
1691 new equality nor does it seem right to create a new wanted goal
1692 (because the goal will most likely contain untouchables, which
1693 can't be solved anyway)!
1695 Note that we *do* fire the improvement if one is Given and one is Derived.
1696 The latter can be a superclass of a wanted goal. Example (tcfail138)
1697 class L a b | a -> b
1698 class (G a, L a b) => C a b
1700 instance C a b' => G (Maybe a)
1701 instance C a b => C (Maybe a) a
1702 instance L (Maybe a) a
1704 When solving the superclasses of the (C (Maybe a) a) instance, we get
1705 Given: C a b ... and hance by superclasses, (G a, L a b)
1707 Use the instance decl to get
1709 The (C a b') is inert, so we generate its Derived superclasses (L a b'),
1710 and now we need improvement between that derived superclass an the Given (L a b)
1712 Note [Overriding implicit parameters]
1713 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1715 f :: (?x::a) -> Bool -> a
1717 g v = let ?x::Int = 3
1718 in (f v, let ?x::Bool = True in f v)
1720 This should probably be well typed, with
1721 g :: Bool -> (Int, Bool)
1723 So the inner binding for ?x::Bool *overrides* the outer one.
1724 Hence a work-item Given overrides an inert-item Given.
1726 Note [Given constraint that matches an instance declaration]
1727 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1728 What should we do when we discover that one (or more) top-level
1729 instances match a given (or solved) class constraint? We have
1732 1. Reject the program. The reason is that there may not be a unique
1733 best strategy for the solver. Example, from the OutsideIn(X) paper:
1734 instance P x => Q [x]
1735 instance (x ~ y) => R [x] y
1737 wob :: forall a b. (Q [b], R b a) => a -> Int
1739 g :: forall a. Q [a] => [a] -> Int
1742 will generate the impliation constraint:
1743 Q [a] => (Q [beta], R beta [a])
1744 If we react (Q [beta]) with its top-level axiom, we end up with a
1745 (P beta), which we have no way of discharging. On the other hand,
1746 if we react R beta [a] with the top-level we get (beta ~ a), which
1747 is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
1748 now solvable by the given Q [a].
1750 However, this option is restrictive, for instance [Example 3] from
1751 Note [Recursive dictionaries] will fail to work.
1753 2. Ignore the problem, hoping that the situations where there exist indeed
1754 such multiple strategies are rare: Indeed the cause of the previous
1755 problem is that (R [x] y) yields the new work (x ~ y) which can be
1756 *spontaneously* solved, not using the givens.
1758 We are choosing option 2 below but we might consider having a flag as well.
1761 Note [New Wanted Superclass Work]
1762 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1763 Even in the case of wanted constraints, we add all of its superclasses as
1764 new given work. There are several reasons for this:
1765 a) to minimise error messages;
1766 eg suppose we have wanted (Eq a, Ord a)
1767 then we report only (Ord a) unsoluble
1769 b) to make the smallest number of constraints when *inferring* a type
1770 (same Eq/Ord example)
1772 c) for recursive dictionaries we *must* add the superclasses
1773 so that we can use them when solving a sub-problem
1775 d) To allow FD-like improvement for type families. Assume that
1777 class C a b | a -> b
1778 and we have to solve the implication constraint:
1780 Then, FD improvement can help us to produce a new wanted (beta ~ b)
1782 We want to have the same effect with the type family encoding of
1783 functional dependencies. Namely, consider:
1784 class (F a ~ b) => C a b
1785 Now suppose that we have:
1788 By interacting the given we will get given (F a ~ b) which is not
1789 enough by itself to make us discharge (C a beta). However, we
1790 may create a new derived equality from the super-class of the
1791 wanted constraint (C a beta), namely derived (F a ~ beta).
1792 Now we may interact this with given (F a ~ b) to get:
1794 But 'beta' is a touchable unification variable, and hence OK to
1795 unify it with 'b', replacing the derived evidence with the identity.
1797 This requires trySpontaneousSolve to solve *derived*
1798 equalities that have a touchable in their RHS, *in addition*
1799 to solving wanted equalities.
1801 Here is another example where this is useful.
1805 class (F a ~ b) => C a b
1806 And we are given the wanteds:
1810 We surely do *not* want to quantify over (b ~ c), since if someone provides
1811 dictionaries for (C a b) and (C a c), these dictionaries can provide a proof
1812 of (b ~ c), hence no extra evidence is necessary. Here is what will happen:
1814 Step 1: We will get new *given* superclass work,
1815 provisionally to our solving of w1 and w2
1817 g1: F a ~ b, g2 : F a ~ c,
1818 w1 : C a b, w2 : C a c, w3 : b ~ c
1820 The evidence for g1 and g2 is a superclass evidence term:
1822 g1 := sc w1, g2 := sc w2
1824 Step 2: The givens will solve the wanted w3, so that
1825 w3 := sym (sc w1) ; sc w2
1827 Step 3: Now, one may naively assume that then w2 can be solve from w1
1828 after rewriting with the (now solved equality) (b ~ c).
1830 But this rewriting is ruled out by the isGoodRectDict!
1832 Conclusion, we will (correctly) end up with the unsolved goals
1835 NB: The desugarer needs be more clever to deal with equalities
1836 that participate in recursive dictionary bindings.
1839 newSCWorkFromFlavored :: EvVar -> CtFlavor -> Class -> [Xi]
1841 newSCWorkFromFlavored ev flavor cls xis
1842 | Given loc <- flavor -- The NoScSkol says "don't add superclasses"
1843 , NoScSkol <- ctLocOrigin loc -- Very important!
1844 = return emptyWorkList
1847 = do { let (tyvars, sc_theta, _, _) = classBigSig cls
1848 sc_theta1 = substTheta (zipTopTvSubst tyvars xis) sc_theta
1849 -- Add *all* its superclasses (equalities or not) as new given work
1850 -- See Note [New Wanted Superclass Work]
1851 ; sc_vars <- zipWithM inst_one sc_theta1 [0..]
1852 ; mkCanonicals flavor sc_vars }
1854 inst_one pred n = newGivOrDerEvVar pred (EvSuperClass ev n)
1856 data LookupInstResult
1858 | GenInst [WantedEvVar] EvTerm
1860 matchClassInst :: Class -> [Type] -> WantedLoc -> TcS LookupInstResult
1861 matchClassInst clas tys loc
1862 = do { let pred = mkClassPred clas tys
1863 ; mb_result <- matchClass clas tys
1865 MatchInstNo -> return NoInstance
1866 MatchInstMany -> return NoInstance -- defer any reactions of a multitude until
1867 -- we learn more about the reagent
1868 MatchInstSingle (dfun_id, mb_inst_tys) ->
1869 do { checkWellStagedDFun pred dfun_id loc
1871 -- It's possible that not all the tyvars are in
1872 -- the substitution, tenv. For example:
1873 -- instance C X a => D X where ...
1874 -- (presumably there's a functional dependency in class C)
1875 -- Hence mb_inst_tys :: Either TyVar TcType
1877 ; tys <- instDFunTypes mb_inst_tys
1878 ; let (theta, _) = tcSplitPhiTy (applyTys (idType dfun_id) tys)
1879 ; if null theta then
1880 return (GenInst [] (EvDFunApp dfun_id tys []))
1882 { ev_vars <- instDFunConstraints theta
1883 ; let wevs = [WantedEvVar w loc | w <- ev_vars]
1884 ; return $ GenInst wevs (EvDFunApp dfun_id tys ev_vars) }