3 solveInteract, AtomicInert,
4 InertSet, emptyInert, updInertSet, extractUnsolved, solveOne
7 #include "HsVersions.h"
30 import Control.Monad ( when )
39 import qualified Data.Map as Map
42 import Control.Monad( zipWithM, unless )
43 import FastString ( sLit )
47 Note [InertSet invariants]
48 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
50 An InertSet is a bag of canonical constraints, with the following invariants:
52 1 No two constraints react with each other.
54 A tricky case is when there exists a given (solved) dictionary
55 constraint and a wanted identical constraint in the inert set, but do
56 not react because reaction would create loopy dictionary evidence for
57 the wanted. See note [Recursive dictionaries]
59 2 Given equalities form an idempotent substitution [none of the
60 given LHS's occur in any of the given RHS's or reactant parts]
62 3 Wanted equalities also form an idempotent substitution
63 4 The entire set of equalities is acyclic.
65 5 Wanted dictionaries are inert with the top-level axiom set
67 6 Equalities of the form tv1 ~ tv2 always have a touchable variable
68 on the left (if possible).
69 7 No wanted constraints tv1 ~ tv2 with tv1 touchable. Such constraints
70 will be marked as solved right before being pushed into the inert set.
71 See note [Touchables and givens].
73 Note that 6 and 7 are /not/ enforced by canonicalization but rather by
74 insertion in the inert list, ie by TcInteract.
76 During the process of solving, the inert set will contain some
77 previously given constraints, some wanted constraints, and some given
78 constraints which have arisen from solving wanted constraints. For
79 now we do not distinguish between given and solved constraints.
81 Note that we must switch wanted inert items to given when going under an
82 implication constraint (when in top-level inference mode).
84 Note [InertSet FlattenSkolemEqClass]
85 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
86 The inert_fsks field of the inert set contains an "inverse map" of all the
87 flatten skolem equalities in the inert set. For instance, if inert_cts looks
94 Then, the inert_fsks fields holds the following map:
95 fsk2 |-> { fsk1, fsk3 }
97 Along with the necessary coercions to convert fsk1 and fsk3 back to fsk2
98 and fsk4 back to fsk5. Hence, the invariants of the inert_fsks field are:
100 (a) All TcTyVars in the domain and range of inert_fsks are flatten skolems
101 (b) All TcTyVars in the domain of inert_fsk occur naked as rhs in some
102 equalities of inert_cts
103 (c) For every mapping fsk1 |-> { (fsk2,co), ... } it must be:
106 The role of the inert_fsks is to make it easy to maintain the equivalence
107 class of each flatten skolem, which is much needed to correctly do spontaneous
108 solving. See Note [Loopy Spontaneous Solving]
111 data CCanMap a = CCanMap { cts_givder :: Map.Map a CanonicalCts
112 -- Invariant: all Given or Derived
113 , cts_wanted :: Map.Map a CanonicalCts }
114 -- Invariant: all Wanted
115 cCanMapToBag :: Ord a => CCanMap a -> CanonicalCts
116 cCanMapToBag cmap = Map.fold unionBags rest_cts (cts_givder cmap)
117 where rest_cts = Map.fold unionBags emptyCCan (cts_wanted cmap)
119 emptyCCanMap :: CCanMap a
120 emptyCCanMap = CCanMap { cts_givder = Map.empty, cts_wanted = Map.empty }
122 updCCanMap:: Ord a => (a,CanonicalCt) -> CCanMap a -> CCanMap a
123 updCCanMap (a,ct) cmap
124 = case cc_flavor ct of
126 -> cmap { cts_wanted = Map.insertWith unionBags a this_ct (cts_wanted cmap) }
128 -> cmap { cts_givder = Map.insertWith unionBags a this_ct (cts_givder cmap) }
129 where this_ct = singleCCan ct
131 getRelevantCts :: Ord a => a -> CCanMap a -> (CanonicalCts, CCanMap a)
132 -- Gets the relevant constraints and returns the rest of the CCanMap
133 getRelevantCts a cmap
134 = let relevant = unionBags (Map.findWithDefault emptyCCan a (cts_wanted cmap))
135 (Map.findWithDefault emptyCCan a (cts_givder cmap))
136 residual_map = cmap { cts_wanted = Map.delete a (cts_wanted cmap)
137 , cts_givder = Map.delete a (cts_givder cmap) }
138 in (relevant, residual_map)
140 extractUnsolvedCMap :: Ord a => CCanMap a -> (CanonicalCts, CCanMap a)
141 -- Gets the wanted constraints and returns a residual CCanMap
142 extractUnsolvedCMap cmap =
143 let unsolved = Map.fold unionBags emptyCCan (cts_wanted cmap)
144 in (unsolved, cmap { cts_wanted = Map.empty})
146 -- See Note [InertSet invariants]
148 = IS { inert_eqs :: CanonicalCts -- Equalities only (CTyEqCan)
150 , inert_dicts :: CCanMap Class -- Dictionaries only
151 , inert_ips :: CCanMap (IPName Name) -- Implicit parameters
152 , inert_funeqs :: CCanMap TyCon -- Type family equalities only
153 -- This representation allows us to quickly get to the relevant
154 -- inert constraints when interacting a work item with the inert set.
157 , inert_fds :: FDImprovements -- List of pairwise improvements that have kicked in already
158 -- and reside either in the worklist or in the inerts
159 , inert_fsks :: Map.Map TcTyVar [(TcTyVar,Coercion)] }
160 -- See Note [InertSet FlattenSkolemEqClass]
162 type FDImprovement = (PredType,PredType)
163 type FDImprovements = [(PredType,PredType)]
165 instance Outputable InertSet where
166 ppr is = vcat [ vcat (map ppr (Bag.bagToList $ inert_eqs is))
167 , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_dicts is)))
168 , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_ips is)))
169 , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_funeqs is)))
170 , vcat (map (\(v,rest) -> ppr v <+> text "|->" <+> hsep (map (ppr.fst) rest))
171 (Map.toList $ inert_fsks is)
175 emptyInert :: InertSet
176 emptyInert = IS { inert_eqs = Bag.emptyBag
177 , inert_dicts = emptyCCanMap
178 , inert_ips = emptyCCanMap
179 , inert_funeqs = emptyCCanMap
180 , inert_fsks = Map.empty, inert_fds = [] }
182 updInertSet :: InertSet -> AtomicInert -> InertSet
183 -- Introduces an element in the inert set for the first time
184 updInertSet is@(IS { inert_eqs = eqs, inert_fsks = fsks })
185 item@(CTyEqCan { cc_id = cv
188 | Just tv2 <- tcGetTyVar_maybe xi,
189 FlatSkol {} <- tcTyVarDetails tv1,
190 FlatSkol {} <- tcTyVarDetails tv2
191 = let eqs' = eqs `Bag.snocBag` item
192 fsks' = Map.insertWith (++) tv2 [(tv1, mkCoVarCoercion cv)] fsks
193 -- See Note [InertSet FlattenSkolemEqClass]
194 in is { inert_eqs = eqs', inert_fsks = fsks' }
196 | isCTyEqCan item -- Other equality
197 = let eqs' = inert_eqs is `Bag.snocBag` item
198 in is { inert_eqs = eqs' }
199 | Just cls <- isCDictCan_Maybe item -- Dictionary
200 = is { inert_dicts = updCCanMap (cls,item) (inert_dicts is) }
201 | Just x <- isCIPCan_Maybe item -- IP
202 = is { inert_ips = updCCanMap (x,item) (inert_ips is) }
203 | Just tc <- isCFunEqCan_Maybe item -- Function equality
204 = is { inert_funeqs = updCCanMap (tc,item) (inert_funeqs is) }
206 = pprPanic "Unknown form of constraint!" (ppr item)
208 updInertSetFDImprs :: InertSet -> Maybe FDImprovement -> InertSet
209 updInertSetFDImprs is (Just fdi) = is { inert_fds = fdi : inert_fds is }
210 updInertSetFDImprs is Nothing = is
212 foldISEqCtsM :: Monad m => (a -> AtomicInert -> m a) -> a -> InertSet -> m a
213 -- Fold over the equalities of the inerts
214 foldISEqCtsM k z IS { inert_eqs = eqs }
215 = Bag.foldlBagM k z eqs
217 extractUnsolved :: InertSet -> (InertSet, CanonicalCts)
218 extractUnsolved is@(IS {inert_eqs = eqs})
219 = let is_init = is { inert_eqs = emptyCCan
220 , inert_dicts = solved_dicts
221 , inert_ips = solved_ips
222 , inert_funeqs = solved_funeqs }
223 is_final = Bag.foldlBag updInertSet is_init solved_eqs -- Add equalities carefully
224 in (is_final, unsolved)
226 where (unsolved_eqs, solved_eqs) = Bag.partitionBag isWantedCt eqs
227 (unsolved_ips, solved_ips) = extractUnsolvedCMap (inert_ips is)
228 (unsolved_dicts, solved_dicts) = extractUnsolvedCMap (inert_dicts is)
229 (unsolved_funeqs, solved_funeqs) = extractUnsolvedCMap (inert_funeqs is)
231 unsolved = unsolved_eqs `unionBags`
232 unsolved_ips `unionBags` unsolved_dicts `unionBags` unsolved_funeqs
234 getFskEqClass :: InertSet -> TcTyVar -> [(TcTyVar,Coercion)]
235 -- Precondition: tv is a FlatSkol. See Note [InertSet FlattenSkolemEqClass]
236 getFskEqClass (IS { inert_eqs = cts, inert_fsks = fsks }) tv
237 = case lkpTyEqCanByLhs of
238 Nothing -> fromMaybe [] (Map.lookup tv fsks)
240 case tcGetTyVar_maybe (cc_rhs ceq) of
241 Just tv_rhs | FlatSkol {} <- tcTyVarDetails tv_rhs
242 -> let ceq_co = mkSymCoercion $ mkCoVarCoercion (cc_id ceq)
243 mk_co (v,c) = (v, mkTransCoercion c ceq_co)
244 in (tv_rhs, ceq_co): map mk_co (fromMaybe [] $ Map.lookup tv fsks)
246 where lkpTyEqCanByLhs = Bag.foldlBag lkp Nothing cts
247 lkp :: Maybe CanonicalCt -> CanonicalCt -> Maybe CanonicalCt
248 lkp Nothing ct@(CTyEqCan {cc_tyvar = tv'}) | tv' == tv = Just ct
249 lkp other _ct = other
251 haveBeenImproved :: FDImprovements -> PredType -> PredType -> Bool
252 haveBeenImproved [] _ _ = False
253 haveBeenImproved ((pty1,pty2):fdimprs) pty1' pty2'
254 | tcEqPred pty1 pty1' && tcEqPred pty2 pty2'
256 | tcEqPred pty1 pty2' && tcEqPred pty2 pty1'
259 = haveBeenImproved fdimprs pty1' pty2'
261 getFDImprovements :: InertSet -> FDImprovements
262 -- Return a list of the improvements that have kicked in so far
263 getFDImprovements = inert_fds
267 Note [Touchables and givens]
268 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
269 Touchable variables will never show up in givens which are inputs to
270 the solver. However, touchables may show up in givens generated by the flattener.
285 which can be put in the inert set. Suppose we also have a wanted
289 We cannot rewrite the given G alpha ~g b using the wanted alpha ~w
290 Int. Instead, after reacting alpha ~w Int with the whole inert set,
291 we observe that we can solve it by unifying alpha with Int, so we mark
292 it as solved and put it back in the *work list*. [We also immediately unify
293 alpha := Int, without telling anyone, see trySpontaneousSolve function, to
294 avoid doing this in the end.]
296 Later, because it is solved (given, in effect), we can use it to rewrite
297 G alpha ~g b to G Int ~g b, which gets put back in the work list. Eventually,
298 we will dispatch the remaining wanted constraints using the top-level axioms.
300 Finally, note that after reacting a wanted equality with the entire inert set
301 we may end up with something like
305 which we should flip around to generate the solved constraint alpha ~s b.
307 %*********************************************************************
309 * Main Interaction Solver *
311 **********************************************************************
315 1. Canonicalise (unary)
316 2. Pairwise interaction (binary)
317 * Take one from work list
318 * Try all pair-wise interactions with each constraint in inert
320 As an optimisation, we prioritize the equalities both in the
321 worklist and in the inerts.
323 3. Try to solve spontaneously for equalities involving touchables
324 4. Top-level interaction (binary wrt top-level)
325 Superclass decomposition belongs in (4), see note [Superclasses]
328 type AtomicInert = CanonicalCt -- constraint pulled from InertSet
329 type WorkItem = CanonicalCt -- constraint pulled from WorkList
331 -- A mixture of Given, Wanted, and Derived constraints.
332 -- We split between equalities and the rest to process equalities first.
333 type WorkList = CanonicalCts
334 type SWorkList = WorkList -- A worklist of solved
336 unionWorkLists :: WorkList -> WorkList -> WorkList
337 unionWorkLists = andCCan
339 isEmptyWorkList :: WorkList -> Bool
340 isEmptyWorkList = isEmptyCCan
342 emptyWorkList :: WorkList
343 emptyWorkList = emptyCCan
345 workListFromCCan :: CanonicalCt -> WorkList
346 workListFromCCan = singleCCan
348 ------------------------
350 = Stop -- Work item is consumed
351 | ContinueWith WorkItem -- Not consumed
353 instance Outputable StopOrContinue where
354 ppr Stop = ptext (sLit "Stop")
355 ppr (ContinueWith w) = ptext (sLit "ContinueWith") <+> ppr w
357 -- Results after interacting a WorkItem as far as possible with an InertSet
359 = SR { sr_inerts :: InertSet
360 -- The new InertSet to use (REPLACES the old InertSet)
361 , sr_new_work :: WorkList
362 -- Any new work items generated (should be ADDED to the old WorkList)
364 -- sr_stop = Just workitem => workitem is *not* in sr_inerts and
365 -- workitem is inert wrt to sr_inerts
366 , sr_stop :: StopOrContinue
369 instance Outputable StageResult where
370 ppr (SR { sr_inerts = inerts, sr_new_work = work, sr_stop = stop })
371 = ptext (sLit "SR") <+>
372 braces (sep [ ptext (sLit "inerts =") <+> ppr inerts <> comma
373 , ptext (sLit "new work =") <+> ppr work <> comma
374 , ptext (sLit "stop =") <+> ppr stop])
376 type SimplifierStage = WorkItem -> InertSet -> TcS StageResult
378 -- Combine a sequence of simplifier 'stages' to create a pipeline
379 runSolverPipeline :: [(String, SimplifierStage)]
380 -> InertSet -> WorkItem
381 -> TcS (InertSet, WorkList)
382 -- Precondition: non-empty list of stages
383 runSolverPipeline pipeline inerts workItem
384 = do { traceTcS "Start solver pipeline" $
385 vcat [ ptext (sLit "work item =") <+> ppr workItem
386 , ptext (sLit "inerts =") <+> ppr inerts]
388 ; let itr_in = SR { sr_inerts = inerts
389 , sr_new_work = emptyWorkList
390 , sr_stop = ContinueWith workItem }
391 ; itr_out <- run_pipeline pipeline itr_in
393 = case sr_stop itr_out of
394 Stop -> sr_inerts itr_out
395 ContinueWith item -> sr_inerts itr_out `updInertSet` item
396 ; return (new_inert, sr_new_work itr_out) }
398 run_pipeline :: [(String, SimplifierStage)]
399 -> StageResult -> TcS StageResult
400 run_pipeline [] itr = return itr
401 run_pipeline _ itr@(SR { sr_stop = Stop }) = return itr
403 run_pipeline ((name,stage):stages)
404 (SR { sr_new_work = accum_work
406 , sr_stop = ContinueWith work_item })
407 = do { itr <- stage work_item inerts
408 ; traceTcS ("Stage result (" ++ name ++ ")") (ppr itr)
409 ; let itr' = itr { sr_new_work = accum_work `unionWorkLists` sr_new_work itr }
410 ; run_pipeline stages itr' }
414 Inert: {c ~ d, F a ~ t, b ~ Int, a ~ ty} (all given)
415 Reagent: a ~ [b] (given)
417 React with (c~d) ==> IR (ContinueWith (a~[b])) True []
418 React with (F a ~ t) ==> IR (ContinueWith (a~[b])) False [F [b] ~ t]
419 React with (b ~ Int) ==> IR (ContinueWith (a~[Int]) True []
422 Inert: {c ~w d, F a ~g t, b ~w Int, a ~w ty}
425 React with (c ~w d) ==> IR (ContinueWith (a~[b])) True []
426 React with (F a ~g t) ==> IR (ContinueWith (a~[b])) True [] (can't rewrite given with wanted!)
430 Inert: {a ~ Int, F Int ~ b} (given)
431 Reagent: F a ~ b (wanted)
433 React with (a ~ Int) ==> IR (ContinueWith (F Int ~ b)) True []
434 React with (F Int ~ b) ==> IR Stop True [] -- after substituting we re-canonicalize and get nothing
437 -- Main interaction solver: we fully solve the worklist 'in one go',
438 -- returning an extended inert set.
440 -- See Note [Touchables and givens].
441 solveInteract :: InertSet -> CanonicalCts -> TcS InertSet
442 solveInteract inert ws
443 = do { dyn_flags <- getDynFlags
444 ; solveInteractWithDepth (ctxtStkDepth dyn_flags,0,[]) inert ws
446 solveOne :: InertSet -> WorkItem -> TcS InertSet
447 solveOne inerts workItem
448 = do { dyn_flags <- getDynFlags
449 ; solveOneWithDepth (ctxtStkDepth dyn_flags,0,[]) inerts workItem
453 solveInteractWithDepth :: (Int, Int, [WorkItem])
454 -> InertSet -> WorkList -> TcS InertSet
455 solveInteractWithDepth ctxt@(max_depth,n,stack) inert ws
460 = solverDepthErrorTcS n stack
463 = do { traceTcS "solveInteractWithDepth" $
464 vcat [ text "Current depth =" <+> ppr n
465 , text "Max depth =" <+> ppr max_depth ]
467 -- Solve equalities first
468 ; let (eqs, non_eqs) = Bag.partitionBag isCTyEqCan ws
469 ; is_from_eqs <- Bag.foldlBagM (solveOneWithDepth ctxt) inert eqs
470 ; Bag.foldlBagM (solveOneWithDepth ctxt) is_from_eqs non_eqs }
473 -- Fully interact the given work item with an inert set, and return a
474 -- new inert set which has assimilated the new information.
475 solveOneWithDepth :: (Int, Int, [WorkItem])
476 -> InertSet -> WorkItem -> TcS InertSet
477 solveOneWithDepth (max_depth, n, stack) inert work
478 = do { traceTcS0 (indent ++ "Solving {") (ppr work)
479 ; (new_inert, new_work) <- runSolverPipeline thePipeline inert work
481 ; traceTcS0 (indent ++ "Subgoals:") (ppr new_work)
483 -- Recursively solve the new work generated
484 -- from workItem, with a greater depth
485 ; res_inert <- solveInteractWithDepth (max_depth, n+1, work:stack)
488 ; traceTcS0 (indent ++ "Done }") (ppr work)
491 indent = replicate (2*n) ' '
493 thePipeline :: [(String,SimplifierStage)]
494 thePipeline = [ ("interact with inert eqs", interactWithInertEqsStage)
495 , ("interact with inerts", interactWithInertsStage)
496 , ("spontaneous solve", spontaneousSolveStage)
497 , ("top-level reactions", topReactionsStage) ]
500 *********************************************************************************
502 The spontaneous-solve Stage
504 *********************************************************************************
506 Note [Efficient Orientation]
507 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
509 There are two cases where we have to be careful about
510 orienting equalities to get better efficiency.
512 Case 2: In Rewriting Equalities (function rewriteEqLHS)
514 When rewriting two equalities with the same LHS:
517 We have a choice of producing work (xi1 ~ xi2) (up-to the
518 canonicalization invariants) However, to prevent the inert items
519 from getting kicked out of the inerts first, we prefer to
520 canonicalize (xi1 ~ xi2) if (b) comes from the inert set, or (xi2
521 ~ xi1) if (a) comes from the inert set.
523 This choice is implemented using the WhichComesFromInert flag.
525 Case 2: In Spontaneous Solving
527 Inerts: [w1] : D alpha
531 Untouchables = [beta]
532 Then a wanted (beta ~ alpha) comes along.
533 1) While interacting with the inerts it is going to kick w2,w4
535 2) Then, it will spontaneoulsy be solved by (alpha := beta)
536 3) Now (and here is the tricky part), to add him back as
537 solved (alpha ~ beta) is no good because, in the next
538 iteration, it will kick out w1,w3 as well so we will end up
539 with *all* the inert equalities back in the worklist!
541 So it is tempting to just add (beta ~ alpha) instead, that is,
542 maintain the original orietnation of the constraint.
544 But that does not work very well, because it may cause the
545 "double unification problem" (See Note [Avoid double unifications]).
552 At the end of the interaction suppose we spontaneously solve alpha := fsk1
553 but keep [Given] fsk1 ~ alpha. Then, the second time around we see the
554 constraint (fsk2 ~ alpha), and we unify *again* alpha := fsk2, which is wrong.
556 Our conclusion is that, while in some cases (Example 2a), it makes sense to
557 preserve the original orientation, it is hard to do this in a sound way.
558 So we *don't* do this for now, @solveWithIdentity@ outputs a constraint that
559 is oriented with the unified variable on the left.
561 Case 3: Functional Dependencies and IP improvement work
562 TODO. Optimisation not yet implemented there.
565 spontaneousSolveStage :: SimplifierStage
566 spontaneousSolveStage workItem inerts
567 = do { mSolve <- trySpontaneousSolve workItem inerts
569 Nothing -> -- no spontaneous solution for him, keep going
570 return $ SR { sr_new_work = emptyWorkList
572 , sr_stop = ContinueWith workItem }
574 Just (workItem', workList')
575 | not (isGivenCt workItem)
576 -- Original was wanted or derived but we have now made him
577 -- given so we have to interact him with the inerts due to
578 -- its status change. This in turn may produce more work.
579 -- We do this *right now* (rather than just putting workItem'
580 -- back into the work-list) because we've solved
581 -> do { (new_inert, new_work) <- runSolverPipeline
582 [ ("recursive interact with inert eqs", interactWithInertEqsStage)
583 , ("recursive interact with inerts", interactWithInertsStage)
585 ; return $ SR { sr_new_work = new_work `unionWorkLists` workList'
586 , sr_inerts = new_inert -- will include workItem'
590 -> -- Original was given; he must then be inert all right, and
591 -- workList' are all givens from flattening
592 return $ SR { sr_new_work = workList'
593 , sr_inerts = inerts `updInertSet` workItem'
597 -- @trySpontaneousSolve wi@ solves equalities where one side is a
598 -- touchable unification variable. Returns:
599 -- * Nothing if we were not able to solve it
600 -- * Just wi' if we solved it, wi' (now a "given") should be put in the work list.
601 -- See Note [Touchables and givens]
602 -- NB: just passing the inerts through for the skolem equivalence classes
603 trySpontaneousSolve :: WorkItem -> InertSet -> TcS (Maybe (WorkItem, SWorkList))
604 trySpontaneousSolve workItem@(CTyEqCan { cc_id = cv, cc_flavor = gw, cc_tyvar = tv1, cc_rhs = xi }) inerts
607 | Just tv2 <- tcGetTyVar_maybe xi
608 = do { tch1 <- isTouchableMetaTyVar tv1
609 ; tch2 <- isTouchableMetaTyVar tv2
610 ; case (tch1, tch2) of
611 (True, True) -> trySpontaneousEqTwoWay inerts cv gw tv1 tv2
612 (True, False) -> trySpontaneousEqOneWay inerts cv gw tv1 xi
613 (False, True) -> trySpontaneousEqOneWay inerts cv gw tv2 (mkTyVarTy tv1)
614 _ -> return Nothing }
616 = do { tch1 <- isTouchableMetaTyVar tv1
617 ; if tch1 then trySpontaneousEqOneWay inerts cv gw tv1 xi
618 else do { traceTcS "Untouchable LHS, can't spontaneously solve workitem:" (ppr workItem)
623 -- trySpontaneousSolve (CFunEqCan ...) = ...
624 -- See Note [No touchables as FunEq RHS] in TcSMonad
625 trySpontaneousSolve _ _ = return Nothing
628 trySpontaneousEqOneWay :: InertSet -> CoVar -> CtFlavor -> TcTyVar -> Xi
629 -> TcS (Maybe (WorkItem,SWorkList))
630 -- tv is a MetaTyVar, not untouchable
631 trySpontaneousEqOneWay inerts cv gw tv xi
632 | not (isSigTyVar tv) || isTyVarTy xi
633 = do { kxi <- zonkTcTypeTcS xi >>= return . typeKind -- Must look through the TcTyBinds
634 -- hence kxi and not typeKind xi
635 -- See Note [Kind Errors]
636 ; if kxi `isSubKind` tyVarKind tv then
637 solveWithIdentity inerts cv gw tv xi
638 else if tyVarKind tv `isSubKind` kxi then
639 return Nothing -- kinds are compatible but we can't solveWithIdentity this way
640 -- This case covers the a_touchable :: * ~ b_untouchable :: ??
641 -- which has to be deferred or floated out for someone else to solve
642 -- it in a scope where 'b' is no longer untouchable.
643 else kindErrorTcS gw (mkTyVarTy tv) xi -- See Note [Kind errors]
645 | otherwise -- Still can't solve, sig tyvar and non-variable rhs
649 trySpontaneousEqTwoWay :: InertSet -> CoVar -> CtFlavor -> TcTyVar -> TcTyVar
650 -> TcS (Maybe (WorkItem,SWorkList))
651 -- Both tyvars are *touchable* MetaTyvars so there is only a chance for kind error here
652 trySpontaneousEqTwoWay inerts cv gw tv1 tv2
654 , nicer_to_update_tv2 = solveWithIdentity inerts cv gw tv2 (mkTyVarTy tv1)
656 = solveWithIdentity inerts cv gw tv1 (mkTyVarTy tv2)
657 | otherwise -- None is a subkind of the other, but they are both touchable!
658 = kindErrorTcS gw (mkTyVarTy tv1) (mkTyVarTy tv2) -- See Note [Kind errors]
662 nicer_to_update_tv2 = isSigTyVar tv1 || isSystemName (Var.varName tv2)
666 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
667 Consider the wanted problem:
668 alpha ~ (# Int, Int #)
669 where alpha :: ?? and (# Int, Int #) :: (#). We can't spontaneously solve this constraint,
670 but we should rather reject the program that give rise to it. If 'trySpontaneousEqTwoWay'
671 simply returns @Nothing@ then that wanted constraint is going to propagate all the way and
672 get quantified over in inference mode. That's bad because we do know at this point that the
673 constraint is insoluble. Instead, we call 'kindErrorTcS' here, which immediately fails.
675 The same applies in canonicalization code in case of kind errors in the givens.
677 However, when we canonicalize givens we only check for compatibility (@compatKind@).
678 If there were a kind error in the givens, this means some form of inconsistency or dead code.
680 When we spontaneously solve wanteds we may have to look through the bindings, hence we
681 call zonkTcTypeTcS above. The reason is that maybe xi is @alpha@ where alpha :: ? and
682 a previous spontaneous solving has set (alpha := f) with (f :: *). The reason that xi is
683 still alpha and not f is becasue the solved constraint may be oriented as (f ~ alpha) instead
684 of (alpha ~ f). Then we should be using @xi@s "real" kind, which is * and not ?, when we try
685 to detect whether spontaneous solving is possible.
688 Note [Spontaneous solving and kind compatibility]
689 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
691 Note that our canonical constraints insist that only *given* equalities (tv ~ xi)
692 or (F xis ~ rhs) require the LHS and the RHS to have exactly the same kinds.
694 - We have to require this because:
695 Given equalities can be freely used to rewrite inside
696 other types or constraints.
697 - We do not have to do the same for wanteds because:
698 First, wanted equations (tv ~ xi) where tv is a touchable
699 unification variable may have kinds that do not agree (the
700 kind of xi must be a sub kind of the kind of tv). Second, any
701 potential kind mismatch will result in the constraint not
702 being soluble, which will be reported anyway. This is the
703 reason that @trySpontaneousOneWay@ and @trySpontaneousTwoWay@
704 will perform a kind compatibility check, and only then will
705 they proceed to @solveWithIdentity@.
708 - Givens from higher-rank, such as:
709 type family T b :: * -> * -> *
710 type instance T Bool = (->)
712 f :: forall a. ((T a ~ (->)) => ...) -> a -> ...
714 Whereas we would be able to apply the type instance, we would not be able to
715 use the given (T Bool ~ (->)) in the body of 'flop'
717 Note [Loopy Spontaneous Solving]
718 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
720 Example 1: [The problem of loopy spontaneous solving]
722 Consider the original wanted:
723 wanted : Maybe (E alpha) ~ alpha
724 where E is a type family, such that E (T x) = x. After canonicalization,
725 as a result of flattening, we will get:
726 given : E alpha ~ fsk
727 wanted : alpha ~ Maybe fsk
728 where (fsk := E alpha, on the side). Now, if we spontaneously *solve*
729 (alpha := Maybe fsk) we are in trouble! Instead, we should refrain from solving
730 it and keep it as wanted. In inference mode we'll end up quantifying over
731 (alpha ~ Maybe (E alpha))
732 Hence, 'solveWithIdentity' performs a small occurs check before
733 actually solving. But this occurs check *must look through* flatten skolems.
735 However, it may be the case that the flatten skolem in hand is equal to some other
736 flatten skolem whith *does not* mention our unification variable. Here's a typical example:
738 Example 2: [The need of keeping track of flatten skolem equivalence classes]
743 After canonicalization:
748 After some reactions:
753 At this point, we will try to spontaneously solve (alpha ~ f2) which remains as yet unsolved.
754 We will look inside f2, which immediately mentions (F alpha), so it's not good to unify! However
755 by looking at the equivalence class of the flatten skolems, we can see that it is fine to
756 unify (alpha ~ f1) which solves our goals!
758 Example 3: [The need of looking through TyBinds for already spontaneously solved variables]
760 A similar problem happens because of other spontaneous solving. Suppose we have the
761 following wanteds, arriving in this exact order:
762 (first) w: beta ~ alpha
763 (second) w: alpha ~ fsk
764 (third) g: F beta ~ fsk
765 Then, we first spontaneously solve the first constraint, making (beta := alpha), and having
766 (beta ~ alpha) as given. *Then* we encounter the second wanted (alpha ~ fsk). "fsk" does not
767 obviously mention alpha, so naively we can also spontaneously solve (alpha := fsk). But
768 that is wrong since fsk mentions beta, which has already secretly been unified to alpha!
770 To avoid this problem, the same occurs check must unveil rewritings that can happen because
771 of spontaneously having solved other constraints.
773 Example 4: [Orientation of (tv ~ xi) equalities]
775 We orient equalities (tv ~ xi) so that flatten skolems appear on the left, if possible. Here
776 is an example of why this is needed:
778 [Wanted] w1: alpha ~ fsk
779 [Given] g1: F alpha ~ fsk
781 Flatten skolem equivalence class = []
783 Assume that g2 is *not* oriented properly, as shown above. Then we would like to spontaneously
784 solve w1 but we can't set alpha := fsk, since fsk hides the type F alpha. However, by using
785 the equation g2 it would be possible to solve w1 by setting alpha := b. In other words, it is
786 not enough to look at a flatten skolem equivalence class to try to find alternatives to unify
787 with. We may have to go to other variables.
789 By orienting the equalities so that flatten skolems are in the LHS we are eliminating them
790 as much as possible from the RHS of other wanted equalities, and hence it suffices to look
791 in their flatten skolem equivalence classes.
793 NB: This situation appears in the IndTypesPerf test case, inside indexed-types/.
795 Caveat: You may wonder if we should be doing this for unification variables as well.
796 However, Note [Efficient Orientation], Case 2, demonstrates that this is not possible
797 at least for touchable unification variables which we have to keep oriented with the
798 touchable on the LHS to be able to eliminate it. So then, what about untouchables?
802 Untouchable = beta, Touchable = alpha
804 [Wanted] w1: alpha ~ fsk
805 [Given] g1: F alpha ~ fsk
806 [Given] g2: beta ~ fsk
807 Flatten skolem equivalence class = []
809 Should we be able to unify alpha := beta to solve the constraint? Arguably yes, but
810 that implies that an *untouchable* unification variable (beta) is in the same equivalence
811 class as a flatten skolem that mentions @alpha@. I.e. g2 means that:
813 But I do not think that there is any way to produce evidence for such a constraint from
814 the outside other than beta := F alpha, which violates the OutsideIn-ness.
818 Note [Avoid double unifications]
819 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
820 The spontaneous solver has to return a given which mentions the unified unification
821 variable *on the left* of the equality. Here is what happens if not:
822 Original wanted: (a ~ alpha), (alpha ~ Int)
823 We spontaneously solve the first wanted, without changing the order!
824 given : a ~ alpha [having unified alpha := a]
825 Now the second wanted comes along, but he cannot rewrite the given, so we simply continue.
826 At the end we spontaneously solve that guy, *reunifying* [alpha := Int]
828 We avoid this problem by orienting the given so that the unification
829 variable is on the left. [Note that alternatively we could attempt to
830 enforce this at canonicalization]
832 See also Note [No touchables as FunEq RHS] in TcSMonad; avoiding
833 double unifications is the main reason we disallow touchable
834 unification variables as RHS of type family equations: F xis ~ alpha.
838 solveWithIdentity :: InertSet
839 -> CoVar -> CtFlavor -> TcTyVar -> Xi
840 -> TcS (Maybe (WorkItem, SWorkList))
841 -- Solve with the identity coercion
842 -- Precondition: kind(xi) is a sub-kind of kind(tv)
843 -- Precondition: CtFlavor is Wanted or Derived
844 -- See [New Wanted Superclass Work] to see why solveWithIdentity
845 -- must work for Derived as well as Wanted
846 -- Returns: (workItem, workList) where
847 -- workItem = the new Given constraint
848 -- workList = some additional work that may have been produced as a result of flattening
849 -- in case we did some chasing through flatten skolem equivalence classes.
850 solveWithIdentity inerts cv gw tv xi
851 = do { tybnds <- getTcSTyBindsMap
852 ; case occurCheck tybnds inerts tv xi of
853 Nothing -> return Nothing
854 Just (xi_unflat,coi) -> solve_with xi_unflat coi }
856 solve_with xi_unflat coi -- coi : xi_unflat ~ xi
857 = do { traceTcS "Sneaky unification:" $
858 vcat [text "Coercion variable: " <+> ppr gw,
859 text "Coercion: " <+> pprEq (mkTyVarTy tv) xi,
860 text "Left Kind is : " <+> ppr (typeKind (mkTyVarTy tv)),
861 text "Right Kind is : " <+> ppr (typeKind xi)
864 ; setWantedTyBind tv xi_unflat -- Set tv := xi_unflat
865 ; cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi_unflat xi_unflat
866 ; let flav = mkGivenFlavor gw UnkSkol
867 ; (ct,cts, co) <- case coi of
868 ACo co -> do { (cc,ccs) <- canEqLeafTyVarLeft flav cv_given tv xi_unflat
869 ; return (cc, ccs, co) }
870 IdCo co -> return $ (CTyEqCan { cc_id = cv_given
871 , cc_flavor = mkGivenFlavor gw UnkSkol
872 , cc_tyvar = tv, cc_rhs = xi }
873 -- xi, *not* xi_unflat because
874 -- xi_unflat may require flattening!
877 Wanted {} -> setWantedCoBind cv co
878 Derived {} -> setDerivedCoBind cv co
879 _ -> pprPanic "Can't spontaneously solve *given*" empty
880 -- See Note [Avoid double unifications]
881 ; return $ Just (ct,cts)
884 -- ; let flav = mkGivenFlavor gw UnkSkol
885 -- ; (cts, co) <- case coi of
886 -- -- TODO: Optimise this, along the way it used to be
887 -- ACo co -> do { cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi_unflat xi_unflat
888 -- ; setWantedTyBind tv xi_unflat
889 -- ; can_eqs <- canEq flav cv_given (mkTyVarTy tv) xi_unflat
890 -- ; return (can_eqs, co) }
891 -- IdCo co -> do { cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi xi
892 -- ; setWantedTyBind tv xi
893 -- ; can_eqs <- canEq flav cv_given (mkTyVarTy tv) xi
894 -- ; return (can_eqs, co) }
896 -- Wanted {} -> setWantedCoBind cv co
897 -- Derived {} -> setDerivedCoBind cv co
898 -- _ -> pprPanic "Can't spontaneously solve *given*" empty
899 -- -- See Note [Avoid double unifications]
900 -- ; return $ Just cts }
902 occurCheck :: VarEnv (TcTyVar, TcType) -> InertSet
903 -> TcTyVar -> TcType -> Maybe (TcType,CoercionI)
904 -- Traverse @ty@ to make sure that @tv@ does not appear under some flatten skolem.
905 -- If it appears under some flatten skolem look in that flatten skolem equivalence class
906 -- (see Note [InertSet FlattenSkolemEqClass], [Loopy Spontaneous Solving]) to see if you
907 -- can find a different flatten skolem to use, that is, one that does not mention @tv@.
909 -- Postcondition: Just (ty', coi) = occurCheck binds inerts tv ty
911 -- NB: The returned type ty' may not be flat!
913 occurCheck ty_binds inerts the_tv the_ty
914 = ok emptyVarSet the_ty
916 -- If (fsk `elem` bad) then tv occurs in any rendering
917 -- of the type under the expansion of fsk
918 ok bad this_ty@(TyConApp tc tys)
919 | Just tys_cois <- allMaybes (map (ok bad) tys)
920 , (tys',cois') <- unzip tys_cois
921 = Just (TyConApp tc tys', mkTyConAppCoI tc cois')
922 | isSynTyCon tc, Just ty_expanded <- tcView this_ty
923 = ok bad ty_expanded -- See Note [Type synonyms and the occur check] in TcUnify
925 | Just (sty',coi) <- ok_pred bad sty
926 = Just (PredTy sty', coi)
927 ok bad (FunTy arg res)
928 | Just (arg', coiarg) <- ok bad arg, Just (res', coires) <- ok bad res
929 = Just (FunTy arg' res', mkFunTyCoI coiarg coires)
930 ok bad (AppTy fun arg)
931 | Just (fun', coifun) <- ok bad fun, Just (arg', coiarg) <- ok bad arg
932 = Just (AppTy fun' arg', mkAppTyCoI coifun coiarg)
933 ok bad (ForAllTy tv1 ty1)
934 -- WARNING: What if it is a (t1 ~ t2) => t3? It's not handled properly at the moment.
935 | Just (ty1', coi) <- ok bad ty1
936 = Just (ForAllTy tv1 ty1', mkForAllTyCoI tv1 coi)
939 ok bad this_ty@(TyVarTy tv)
940 | tv == the_tv = Nothing -- Occurs check error
941 | not (isTcTyVar tv) = Just (this_ty, IdCo this_ty) -- Bound var
942 | FlatSkol zty <- tcTyVarDetails tv = ok_fsk bad tv zty
943 | Just (_,ty) <- lookupVarEnv ty_binds tv = ok bad ty
944 | otherwise = Just (this_ty, IdCo this_ty)
946 -- Check if there exists a ty bind already, as a result of sneaky unification.
948 ok _bad _ty = Nothing
951 ok_pred bad (ClassP cn tys)
952 | Just tys_cois <- allMaybes $ map (ok bad) tys
953 = let (tys', cois') = unzip tys_cois
954 in Just (ClassP cn tys', mkClassPPredCoI cn cois')
955 ok_pred bad (IParam nm ty)
956 | Just (ty',co') <- ok bad ty
957 = Just (IParam nm ty', mkIParamPredCoI nm co')
958 ok_pred bad (EqPred ty1 ty2)
959 | Just (ty1',coi1) <- ok bad ty1, Just (ty2',coi2) <- ok bad ty2
960 = Just (EqPred ty1' ty2', mkEqPredCoI coi1 coi2)
961 ok_pred _ _ = Nothing
965 | fsk `elemVarSet` bad
966 -- We are already trying to find a rendering of fsk,
967 -- and to do that it seems we need a rendering, so fail
970 = firstJusts (ok new_bad zty : map (go_under_fsk new_bad) fsk_equivs)
972 fsk_equivs = getFskEqClass inerts fsk
973 new_bad = bad `extendVarSetList` (fsk : map fst fsk_equivs)
976 go_under_fsk bad_tvs (fsk,co)
977 | FlatSkol zty <- tcTyVarDetails fsk
978 = case ok bad_tvs zty of
980 Just (ty,coi') -> Just (ty, mkTransCoI coi' (ACo co))
981 | otherwise = pprPanic "go_down_equiv" (ppr fsk)
985 *********************************************************************************
987 The interact-with-inert Stage
989 *********************************************************************************
992 -- Interaction result of WorkItem <~> AtomicInert
994 = IR { ir_stop :: StopOrContinue
996 -- => Reagent (work item) consumed.
997 -- ContinueWith new_reagent
998 -- => Reagent transformed but keep gathering interactions.
999 -- The transformed item remains inert with respect
1000 -- to any previously encountered inerts.
1002 , ir_inert_action :: InertAction
1003 -- Whether the inert item should remain in the InertSet.
1005 , ir_new_work :: WorkList
1006 -- new work items to add to the WorkList
1008 , ir_improvement :: Maybe FDImprovement -- In case improvement kicked in
1011 -- What to do with the inert reactant.
1012 data InertAction = KeepInert | DropInert
1015 mkIRContinue :: Monad m => WorkItem -> InertAction -> WorkList -> m InteractResult
1016 mkIRContinue wi keep newWork = return $ IR (ContinueWith wi) keep newWork Nothing
1018 mkIRStop :: Monad m => InertAction -> WorkList -> m InteractResult
1019 mkIRStop keep newWork = return $ IR Stop keep newWork Nothing
1021 mkIRStop_RecordImprovement :: Monad m => InertAction -> WorkList -> FDImprovement -> m InteractResult
1022 mkIRStop_RecordImprovement keep newWork fdimpr = return $ IR Stop keep newWork (Just fdimpr)
1024 dischargeWorkItem :: Monad m => m InteractResult
1025 dischargeWorkItem = mkIRStop KeepInert emptyWorkList
1027 noInteraction :: Monad m => WorkItem -> m InteractResult
1028 noInteraction workItem = mkIRContinue workItem KeepInert emptyWorkList
1030 data WhichComesFromInert = LeftComesFromInert | RightComesFromInert
1031 -- See Note [Efficient Orientation, Case 2]
1034 ---------------------------------------------------
1035 -- Interact a single WorkItem with the equalities of an inert set as far as possible, i.e. until we
1036 -- get a Stop result from an individual reaction (i.e. when the WorkItem is consumed), or until we've
1037 -- interact the WorkItem with the entire equalities of the InertSet
1039 interactWithInertEqsStage :: SimplifierStage
1040 interactWithInertEqsStage workItem inert
1041 = foldISEqCtsM interactNext initITR inert
1042 where initITR = SR { sr_inerts = IS { inert_eqs = emptyCCan -- We will fold over the equalities
1043 , inert_fsks = Map.empty -- which will generate those two again
1044 , inert_dicts = inert_dicts inert
1045 , inert_ips = inert_ips inert
1046 , inert_funeqs = inert_funeqs inert
1047 , inert_fds = inert_fds inert
1049 , sr_new_work = emptyWorkList
1050 , sr_stop = ContinueWith workItem }
1053 ---------------------------------------------------
1054 -- Interact a single WorkItem with *non-equality* constraints in the inert set.
1055 -- Precondition: equality interactions must have already happened, hence we have
1056 -- to pick up some information from the incoming inert, before folding over the
1057 -- "Other" constraints it contains!
1059 interactWithInertsStage :: SimplifierStage
1060 interactWithInertsStage workItem inert
1061 = let (relevant, inert_residual) = getISRelevant workItem inert
1062 initITR = SR { sr_inerts = inert_residual
1063 , sr_new_work = emptyWorkList
1064 , sr_stop = ContinueWith workItem }
1065 in Bag.foldlBagM interactNext initITR relevant
1067 getISRelevant :: CanonicalCt -> InertSet -> (CanonicalCts, InertSet)
1068 getISRelevant (CDictCan { cc_class = cls } ) is
1069 = let (relevant, residual_map) = getRelevantCts cls (inert_dicts is)
1070 in (relevant, is { inert_dicts = residual_map })
1071 getISRelevant (CFunEqCan { cc_fun = tc } ) is
1072 = let (relevant, residual_map) = getRelevantCts tc (inert_funeqs is)
1073 in (relevant, is { inert_funeqs = residual_map })
1074 getISRelevant (CIPCan { cc_ip_nm = nm }) is
1075 = let (relevant, residual_map) = getRelevantCts nm (inert_ips is)
1076 in (relevant, is { inert_ips = residual_map })
1077 -- An equality, finally, may kick everything except equalities out
1078 -- because we have already interacted the equalities in interactWithInertEqsStage
1079 getISRelevant _eq_ct is -- Equality, everything is relevant for this one
1080 -- TODO: if we were caching variables, we'd know that only
1081 -- some are relevant. Experiment with this for now.
1082 = let cts = cCanMapToBag (inert_ips is) `unionBags`
1083 cCanMapToBag (inert_dicts is) `unionBags` cCanMapToBag (inert_funeqs is)
1084 in (cts, is { inert_dicts = emptyCCanMap
1085 , inert_ips = emptyCCanMap
1086 , inert_funeqs = emptyCCanMap })
1088 interactNext :: StageResult -> AtomicInert -> TcS StageResult
1089 interactNext it inert
1090 | ContinueWith workItem <- sr_stop it
1091 = do { let inerts = sr_inerts it
1092 fdimprs_old = getFDImprovements inerts
1094 ; ir <- interactWithInert fdimprs_old inert workItem
1096 -- New inerts depend on whether we KeepInert or not and must
1097 -- be updated with FD improvement information from the interaction result (ir)
1098 ; let inerts_new = updInertSetFDImprs upd_inert (ir_improvement ir)
1099 upd_inert = if ir_inert_action ir == KeepInert
1100 then inerts `updInertSet` inert else inerts
1102 ; return $ SR { sr_inerts = inerts_new
1103 , sr_new_work = sr_new_work it `unionWorkLists` ir_new_work ir
1104 , sr_stop = ir_stop ir } }
1106 = return $ it { sr_inerts = (sr_inerts it) `updInertSet` inert }
1108 -- Do a single interaction of two constraints.
1109 interactWithInert :: FDImprovements -> AtomicInert -> WorkItem -> TcS InteractResult
1110 interactWithInert fdimprs inert workitem
1111 = do { ctxt <- getTcSContext
1112 ; let is_allowed = allowedInteraction (simplEqsOnly ctxt) inert workitem
1113 inert_ev = cc_id inert
1114 work_ev = cc_id workitem
1116 -- Never interact a wanted and a derived where the derived's evidence
1117 -- mentions the wanted evidence in an unguarded way.
1118 -- See Note [Superclasses and recursive dictionaries]
1119 -- and Note [New Wanted Superclass Work]
1120 -- We don't have to do this for givens, as we fully know the evidence for them.
1122 case (cc_flavor inert, cc_flavor workitem) of
1123 (Wanted loc, Derived {}) -> isGoodRecEv work_ev (WantedEvVar inert_ev loc)
1124 (Derived {}, Wanted loc) -> isGoodRecEv inert_ev (WantedEvVar work_ev loc)
1127 ; if is_allowed && rec_ev_ok then
1128 doInteractWithInert fdimprs inert workitem
1130 noInteraction workitem
1133 allowedInteraction :: Bool -> AtomicInert -> WorkItem -> Bool
1134 -- Allowed interactions
1135 allowedInteraction eqs_only (CDictCan {}) (CDictCan {}) = not eqs_only
1136 allowedInteraction eqs_only (CIPCan {}) (CIPCan {}) = not eqs_only
1137 allowedInteraction _ _ _ = True
1139 --------------------------------------------
1140 doInteractWithInert :: FDImprovements -> CanonicalCt -> CanonicalCt -> TcS InteractResult
1141 -- Identical class constraints.
1143 doInteractWithInert fdimprs
1144 (CDictCan { cc_id = d1, cc_flavor = fl1, cc_class = cls1, cc_tyargs = tys1 })
1145 workItem@(CDictCan { cc_id = d2, cc_flavor = fl2, cc_class = cls2, cc_tyargs = tys2 })
1146 | cls1 == cls2 && (and $ zipWith tcEqType tys1 tys2)
1147 = solveOneFromTheOther (d1,fl1) workItem
1149 | cls1 == cls2 && (not (isGiven fl1 && isGiven fl2))
1150 = -- See Note [When improvement happens]
1151 do { let pty1 = ClassP cls1 tys1
1152 pty2 = ClassP cls2 tys2
1153 work_item_pred_loc = (pty2, ppr d2)
1154 inert_pred_loc = (pty1, ppr d1)
1155 loc = combineCtLoc fl1 fl2
1156 eqn_pred_locs = improveFromAnother work_item_pred_loc inert_pred_loc
1158 ; wevvars <- mkWantedFunDepEqns loc eqn_pred_locs
1159 ; fd_work <- canWanteds wevvars
1160 -- See Note [Generating extra equalities]
1161 ; traceTcS "Checking if improvements existed." (ppr fdimprs)
1162 ; if isEmptyWorkList fd_work || haveBeenImproved fdimprs pty1 pty2 then
1164 mkIRContinue workItem KeepInert fd_work
1165 else do { traceTcS "Recording improvement and throwing item back in worklist." (ppr (pty1,pty2))
1166 ; mkIRStop_RecordImprovement KeepInert
1167 (fd_work `unionWorkLists` workListFromCCan workItem) (pty1,pty2)
1169 -- See Note [FunDep Reactions]
1172 -- Class constraint and given equality: use the equality to rewrite
1173 -- the class constraint.
1174 doInteractWithInert _fdimprs
1175 (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi })
1176 (CDictCan { cc_id = dv, cc_flavor = wfl, cc_class = cl, cc_tyargs = xis })
1177 | ifl `canRewrite` wfl
1178 , tv `elemVarSet` tyVarsOfTypes xis
1179 = if isDerivedSC wfl then
1180 mkIRStop KeepInert $ emptyWorkList -- See Note [Adding Derived Superclasses]
1181 else do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,wfl,cl,xis)
1182 -- Continue with rewritten Dictionary because we can only be in the
1183 -- interactWithEqsStage, so the dictionary is inert.
1184 ; mkIRContinue rewritten_dict KeepInert emptyWorkList }
1186 doInteractWithInert _fdimprs
1187 (CDictCan { cc_id = dv, cc_flavor = ifl, cc_class = cl, cc_tyargs = xis })
1188 workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
1189 | wfl `canRewrite` ifl
1190 , tv `elemVarSet` tyVarsOfTypes xis
1191 = if isDerivedSC ifl then
1192 mkIRContinue workItem DropInert emptyWorkList -- No need to do any rewriting,
1193 -- see Note [Adding Derived Superclasses]
1194 else do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,ifl,cl,xis)
1195 ; mkIRContinue workItem DropInert (workListFromCCan rewritten_dict) }
1197 -- Class constraint and given equality: use the equality to rewrite
1198 -- the class constraint.
1199 doInteractWithInert _fdimprs
1200 (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi })
1201 (CIPCan { cc_id = ipid, cc_flavor = wfl, cc_ip_nm = nm, cc_ip_ty = ty })
1202 | ifl `canRewrite` wfl
1203 , tv `elemVarSet` tyVarsOfType ty
1204 = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,wfl,nm,ty)
1205 ; mkIRContinue rewritten_ip KeepInert emptyWorkList }
1207 doInteractWithInert _fdimprs
1208 (CIPCan { cc_id = ipid, cc_flavor = ifl, cc_ip_nm = nm, cc_ip_ty = ty })
1209 workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
1210 | wfl `canRewrite` ifl
1211 , tv `elemVarSet` tyVarsOfType ty
1212 = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,ifl,nm,ty)
1213 ; mkIRContinue workItem DropInert (workListFromCCan rewritten_ip) }
1215 -- Two implicit parameter constraints. If the names are the same,
1216 -- but their types are not, we generate a wanted type equality
1217 -- that equates the type (this is "improvement").
1218 -- However, we don't actually need the coercion evidence,
1219 -- so we just generate a fresh coercion variable that isn't used anywhere.
1220 doInteractWithInert _fdimprs
1221 (CIPCan { cc_id = id1, cc_flavor = ifl, cc_ip_nm = nm1, cc_ip_ty = ty1 })
1222 workItem@(CIPCan { cc_flavor = wfl, cc_ip_nm = nm2, cc_ip_ty = ty2 })
1223 | nm1 == nm2 && isGiven wfl && isGiven ifl
1224 = -- See Note [Overriding implicit parameters]
1225 -- Dump the inert item, override totally with the new one
1226 -- Do not require type equality
1227 mkIRContinue workItem DropInert emptyWorkList
1229 | nm1 == nm2 && ty1 `tcEqType` ty2
1230 = solveOneFromTheOther (id1,ifl) workItem
1233 = -- See Note [When improvement happens]
1234 do { co_var <- newWantedCoVar ty1 ty2
1235 ; let flav = Wanted (combineCtLoc ifl wfl)
1236 ; cans <- mkCanonical flav co_var
1237 ; mkIRContinue workItem KeepInert cans }
1240 -- Inert: equality, work item: function equality
1242 -- Never rewrite a given with a wanted equality, and a type function
1243 -- equality can never rewrite an equality. Note also that if we have
1244 -- F x1 ~ x2 and a ~ x3, and a occurs in x2, we don't rewrite it. We
1245 -- can wait until F x1 ~ x2 matches another F x1 ~ x4, and only then
1246 -- we will ``expose'' x2 and x4 to rewriting.
1248 -- Otherwise, we can try rewriting the type function equality with the equality.
1249 doInteractWithInert _fdimprs
1250 (CTyEqCan { cc_id = cv1, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi1 })
1251 (CFunEqCan { cc_id = cv2, cc_flavor = wfl, cc_fun = tc
1252 , cc_tyargs = args, cc_rhs = xi2 })
1253 | ifl `canRewrite` wfl
1254 , tv `elemVarSet` tyVarsOfTypes args
1255 = do { rewritten_funeq <- rewriteFunEq (cv1,tv,xi1) (cv2,wfl,tc,args,xi2)
1256 ; mkIRStop KeepInert (workListFromCCan rewritten_funeq) }
1257 -- must Stop here, because we may no longer be inert after the rewritting.
1259 -- Inert: function equality, work item: equality
1260 doInteractWithInert _fdimprs
1261 (CFunEqCan {cc_id = cv1, cc_flavor = ifl, cc_fun = tc
1262 , cc_tyargs = args, cc_rhs = xi1 })
1263 workItem@(CTyEqCan { cc_id = cv2, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi2 })
1264 | wfl `canRewrite` ifl
1265 , tv `elemVarSet` tyVarsOfTypes args
1266 = do { rewritten_funeq <- rewriteFunEq (cv2,tv,xi2) (cv1,ifl,tc,args,xi1)
1267 ; mkIRContinue workItem DropInert (workListFromCCan rewritten_funeq) }
1269 doInteractWithInert _fdimprs
1270 (CFunEqCan { cc_id = cv1, cc_flavor = fl1, cc_fun = tc1
1271 , cc_tyargs = args1, cc_rhs = xi1 })
1272 workItem@(CFunEqCan { cc_id = cv2, cc_flavor = fl2, cc_fun = tc2
1273 , cc_tyargs = args2, cc_rhs = xi2 })
1274 | fl1 `canSolve` fl2 && lhss_match
1275 = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
1276 ; mkIRStop KeepInert cans }
1277 | fl2 `canSolve` fl1 && lhss_match
1278 = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
1279 ; mkIRContinue workItem DropInert cans }
1281 lhss_match = tc1 == tc2 && and (zipWith tcEqType args1 args2)
1283 doInteractWithInert _fdimprs
1284 inert@(CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
1285 workItem@(CTyEqCan { cc_id = cv2, cc_flavor = fl2, cc_tyvar = tv2, cc_rhs = xi2 })
1286 -- Check for matching LHS
1287 | fl1 `canSolve` fl2 && tv1 == tv2
1288 = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
1289 ; mkIRStop KeepInert cans }
1291 | fl2 `canSolve` fl1 && tv1 == tv2
1292 = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
1293 ; mkIRContinue workItem DropInert cans }
1295 -- Check for rewriting RHS
1296 | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfType xi2
1297 = do { rewritten_eq <- rewriteEqRHS (cv1,tv1,xi1) (cv2,fl2,tv2,xi2)
1298 ; mkIRStop KeepInert rewritten_eq }
1299 | fl2 `canRewrite` fl1 && tv2 `elemVarSet` tyVarsOfType xi1
1300 = do { rewritten_eq <- rewriteEqRHS (cv2,tv2,xi2) (cv1,fl1,tv1,xi1)
1301 ; mkIRContinue workItem DropInert rewritten_eq }
1303 -- Finally, if workitem is a Flatten Equivalence Class constraint and the
1304 -- inert is a wanted constraint, even when the workitem cannot rewrite the
1305 -- inert, drop the inert out because you may have to reconsider solving the
1306 -- inert *using* the equivalence class you created. See note [Loopy Spontaneous Solving]
1307 -- and [InertSet FlattenSkolemEqClass]
1309 | not $ isGiven fl1, -- The inert is wanted or derived
1310 isMetaTyVar tv1, -- and has a unification variable lhs
1311 FlatSkol {} <- tcTyVarDetails tv2, -- And workitem is a flatten skolem equality
1312 Just tv2' <- tcGetTyVar_maybe xi2, FlatSkol {} <- tcTyVarDetails tv2'
1313 = mkIRContinue workItem DropInert (workListFromCCan inert)
1316 -- Fall-through case for all other situations
1317 doInteractWithInert _fdimprs _ workItem = noInteraction workItem
1319 -------------------------
1320 -- Equational Rewriting
1321 rewriteDict :: (CoVar, TcTyVar, Xi) -> (DictId, CtFlavor, Class, [Xi]) -> TcS CanonicalCt
1322 rewriteDict (cv,tv,xi) (dv,gw,cl,xis)
1323 = do { let cos = substTysWith [tv] [mkCoVarCoercion cv] xis -- xis[tv] ~ xis[xi]
1324 args = substTysWith [tv] [xi] xis
1326 dict_co = mkTyConCoercion con cos
1327 ; dv' <- newDictVar cl args
1329 Wanted {} -> setDictBind dv (EvCast dv' (mkSymCoercion dict_co))
1330 _given_or_derived -> setDictBind dv' (EvCast dv dict_co)
1331 ; return (CDictCan { cc_id = dv'
1334 , cc_tyargs = args }) }
1336 rewriteIP :: (CoVar,TcTyVar,Xi) -> (EvVar,CtFlavor, IPName Name, TcType) -> TcS CanonicalCt
1337 rewriteIP (cv,tv,xi) (ipid,gw,nm,ty)
1338 = do { let ip_co = substTyWith [tv] [mkCoVarCoercion cv] ty -- ty[tv] ~ t[xi]
1339 ty' = substTyWith [tv] [xi] ty
1340 ; ipid' <- newIPVar nm ty'
1342 Wanted {} -> setIPBind ipid (EvCast ipid' (mkSymCoercion ip_co))
1343 _given_or_derived -> setIPBind ipid' (EvCast ipid ip_co)
1344 ; return (CIPCan { cc_id = ipid'
1347 , cc_ip_ty = ty' }) }
1349 rewriteFunEq :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TyCon, [Xi], Xi) -> TcS CanonicalCt
1350 rewriteFunEq (cv1,tv,xi1) (cv2,gw, tc,args,xi2)
1351 = do { let arg_cos = substTysWith [tv] [mkCoVarCoercion cv1] args
1352 args' = substTysWith [tv] [xi1] args
1353 fun_co = mkTyConCoercion tc arg_cos
1354 ; cv2' <- case gw of
1355 Wanted {} -> do { cv2' <- newWantedCoVar (mkTyConApp tc args') xi2
1356 ; setWantedCoBind cv2 $
1357 mkTransCoercion fun_co (mkCoVarCoercion cv2')
1359 _giv_or_der -> newGivOrDerCoVar (mkTyConApp tc args') xi2 $
1360 mkTransCoercion (mkSymCoercion fun_co) (mkCoVarCoercion cv2)
1361 ; return (CFunEqCan { cc_id = cv2'
1368 rewriteEqRHS :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TcTyVar,Xi) -> TcS WorkList
1369 -- Use the first equality to rewrite the second, flavors already checked.
1370 -- E.g. c1 : tv1 ~ xi1 c2 : tv2 ~ xi2
1371 -- rewrites c2 to give
1372 -- c2' : tv2 ~ xi2[xi1/tv1]
1373 -- We must do an occurs check to sure the new constraint is canonical
1374 -- So we might return an empty bag
1375 rewriteEqRHS (cv1,tv1,xi1) (cv2,gw,tv2,xi2)
1376 | Just tv2' <- tcGetTyVar_maybe xi2'
1377 , tv2 == tv2' -- In this case xi2[xi1/tv1] = tv2, so we have tv2~tv2
1378 = do { when (isWanted gw) (setWantedCoBind cv2 (mkSymCoercion co2'))
1379 ; return emptyCCan }
1384 -> do { cv2' <- newWantedCoVar (mkTyVarTy tv2) xi2'
1385 ; setWantedCoBind cv2 $
1386 mkCoVarCoercion cv2' `mkTransCoercion` mkSymCoercion co2'
1389 -> newGivOrDerCoVar (mkTyVarTy tv2) xi2' $
1390 mkCoVarCoercion cv2 `mkTransCoercion` co2'
1392 ; xi2'' <- canOccursCheck gw tv2 xi2' -- we know xi2' is *not* tv2
1393 ; canEq gw cv2' (mkTyVarTy tv2) xi2''
1396 xi2' = substTyWith [tv1] [xi1] xi2
1397 co2' = substTyWith [tv1] [mkCoVarCoercion cv1] xi2 -- xi2 ~ xi2[xi1/tv1]
1400 rewriteEqLHS :: WhichComesFromInert -> (Coercion,Xi) -> (CoVar,CtFlavor,Xi) -> TcS WorkList
1401 -- Used to ineract two equalities of the following form:
1402 -- First Equality: co1: (XXX ~ xi1)
1403 -- Second Equality: cv2: (XXX ~ xi2)
1404 -- Where the cv1 `canSolve` cv2 equality
1405 -- We have an option of creating new work (xi1 ~ xi2) OR (xi2 ~ xi1),
1406 -- See Note [Efficient Orientation] for that
1407 rewriteEqLHS which (co1,xi1) (cv2,gw,xi2)
1408 = do { cv2' <- case (isWanted gw, which) of
1409 (True,LeftComesFromInert) ->
1410 do { cv2' <- newWantedCoVar xi2 xi1
1411 ; setWantedCoBind cv2 $
1412 co1 `mkTransCoercion` mkSymCoercion (mkCoVarCoercion cv2')
1414 (True,RightComesFromInert) ->
1415 do { cv2' <- newWantedCoVar xi1 xi2
1416 ; setWantedCoBind cv2 $
1417 co1 `mkTransCoercion` mkCoVarCoercion cv2'
1419 (False,LeftComesFromInert) ->
1420 newGivOrDerCoVar xi2 xi1 $
1421 mkSymCoercion (mkCoVarCoercion cv2) `mkTransCoercion` co1
1422 (False,RightComesFromInert) ->
1423 newGivOrDerCoVar xi1 xi2 $
1424 mkSymCoercion co1 `mkTransCoercion` mkCoVarCoercion cv2
1425 ; mkCanonical gw cv2'
1428 solveOneFromTheOther :: (EvVar, CtFlavor) -> CanonicalCt -> TcS InteractResult
1429 -- First argument inert, second argument workitem. They both represent
1430 -- wanted/given/derived evidence for the *same* predicate so we try here to
1431 -- discharge one directly from the other.
1433 -- Precondition: value evidence only (implicit parameters, classes)
1435 solveOneFromTheOther (iid,ifl) workItem
1436 -- Both derived needs a special case. You might think that we do not need
1437 -- two evidence terms for the same claim. But, since the evidence is partial,
1438 -- either evidence may do in some cases; see TcSMonad.isGoodRecEv.
1439 -- See also Example 3 in Note [Superclasses and recursive dictionaries]
1440 | isDerived ifl && isDerived wfl
1441 = noInteraction workItem
1443 | ifl `canSolve` wfl
1444 = do { unless (isGiven wfl) $ setEvBind wid (EvId iid)
1445 -- Overwrite the binding, if one exists
1446 -- For Givens, which are lambda-bound, nothing to overwrite,
1447 ; dischargeWorkItem }
1449 | otherwise -- wfl `canSolve` ifl
1450 = do { unless (isGiven ifl) $ setEvBind iid (EvId wid)
1451 ; mkIRContinue workItem DropInert emptyWorkList }
1454 wfl = cc_flavor workItem
1455 wid = cc_id workItem
1458 Note [Superclasses and recursive dictionaries]
1459 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1460 Overlaps with Note [SUPERCLASS-LOOP 1]
1461 Note [SUPERCLASS-LOOP 2]
1462 Note [Recursive instances and superclases]
1463 ToDo: check overlap and delete redundant stuff
1465 Right before adding a given into the inert set, we must
1466 produce some more work, that will bring the superclasses
1467 of the given into scope. The superclass constraints go into
1470 When we simplify a wanted constraint, if we first see a matching
1471 instance, we may produce new wanted work. To (1) avoid doing this work
1472 twice in the future and (2) to handle recursive dictionaries we may ``cache''
1473 this item as solved (in effect, given) into our inert set and with that add
1474 its superclass constraints (as given) in our worklist.
1476 But now we have added partially solved constraints to the worklist which may
1477 interact with other wanteds. Consider the example:
1481 class Eq b => Foo a b --- 0-th selector
1482 instance Eq a => Foo [a] a --- fooDFun
1484 and wanted (Foo [t] t). We are first going to see that the instance matches
1485 and create an inert set that includes the solved (Foo [t] t) and its
1487 d1 :_g Foo [t] t d1 := EvDFunApp fooDFun d3
1488 d2 :_g Eq t d2 := EvSuperClass d1 0
1489 Our work list is going to contain a new *wanted* goal
1491 It is wrong to react the wanted (Eq t) with the given (Eq t) because that would
1492 construct loopy evidence. Hence the check isGoodRecEv in doInteractWithInert.
1494 OK, so we have ruled out bad behaviour, but how do we ge recursive dictionaries,
1499 data D r = ZeroD | SuccD (r (D r));
1501 instance (Eq (r (D r))) => Eq (D r) where
1502 ZeroD == ZeroD = True
1503 (SuccD a) == (SuccD b) = a == b
1506 equalDC :: D [] -> D [] -> Bool;
1509 We need to prove (Eq (D [])). Here's how we go:
1513 by instance decl, holds if
1517 *BUT* we have an inert set which gives us (no superclasses):
1519 By the instance declaration of Eq we can show the 'd2' goal if
1521 where d2 = dfEqList d3
1523 Now, however this wanted can interact with our inert d1 to set:
1525 and solve the goal. Why was this interaction OK? Because, if we chase the
1526 evidence of d1 ~~> dfEqD d2 ~~-> dfEqList d3, so by setting d3 := d1 we
1528 d3 := dfEqD2 (dfEqList d3)
1529 which is FINE because the use of d3 is protected by the instance function
1532 So, our strategy is to try to put solved wanted dictionaries into the
1533 inert set along with their superclasses (when this is meaningful,
1534 i.e. when new wanted goals are generated) but solve a wanted dictionary
1535 from a given only in the case where the evidence variable of the
1536 wanted is mentioned in the evidence of the given (recursively through
1537 the evidence binds) in a protected way: more instance function applications
1538 than superclass selectors.
1540 Here are some more examples from GHC's previous type checker
1544 This code arises in the context of "Scrap Your Boilerplate with Class"
1548 instance Sat (ctx Char) => Data ctx Char -- dfunData1
1549 instance (Sat (ctx [a]), Data ctx a) => Data ctx [a] -- dfunData2
1551 class Data Maybe a => Foo a
1553 instance Foo t => Sat (Maybe t) -- dfunSat
1555 instance Data Maybe a => Foo a -- dfunFoo1
1556 instance Foo a => Foo [a] -- dfunFoo2
1557 instance Foo [Char] -- dfunFoo3
1559 Consider generating the superclasses of the instance declaration
1560 instance Foo a => Foo [a]
1562 So our problem is this
1564 d1 :_w Data Maybe [t]
1566 We may add the given in the inert set, along with its superclasses
1567 [assuming we don't fail because there is a matching instance, see
1568 tryTopReact, given case ]
1572 d01 :_g Data Maybe t -- d2 := EvDictSuperClass d0 0
1573 d1 :_w Data Maybe [t]
1574 Then d2 can readily enter the inert, and we also do solving of the wanted
1577 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1579 d2 :_w Sat (Maybe [t])
1581 d01 :_g Data Maybe t
1582 Now, we may simplify d2 more:
1585 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1586 d1 :_g Data Maybe [t]
1587 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1591 d01 :_g Data Maybe t
1593 Now, we can just solve d3.
1596 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1597 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1600 d01 :_g Data Maybe t
1601 And now we can simplify d4 again, but since it has superclasses we *add* them to the worklist:
1604 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1605 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1606 d4 :_g Foo [t] d4 := dfunFoo2 d5
1609 d6 :_g Data Maybe [t] d6 := EvDictSuperClass d4 0
1610 d01 :_g Data Maybe t
1611 Now, d5 can be solved! (and its superclass enter scope)
1614 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1615 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1616 d4 :_g Foo [t] d4 := dfunFoo2 d5
1617 d5 :_g Foo t d5 := dfunFoo1 d7
1620 d6 :_g Data Maybe [t]
1621 d8 :_g Data Maybe t d8 := EvDictSuperClass d5 0
1622 d01 :_g Data Maybe t
1625 [1] Suppose we pick d8 and we react him with d01. Which of the two givens should
1626 we keep? Well, we *MUST NOT* drop d01 because d8 contains recursive evidence
1627 that must not be used (look at case interactInert where both inert and workitem
1628 are givens). So we have several options:
1629 - Drop the workitem always (this will drop d8)
1630 This feels very unsafe -- what if the work item was the "good" one
1631 that should be used later to solve another wanted?
1632 - Don't drop anyone: the inert set may contain multiple givens!
1633 [This is currently implemented]
1635 The "don't drop anyone" seems the most safe thing to do, so now we come to problem 2:
1636 [2] We have added both d6 and d01 in the inert set, and we are interacting our wanted
1637 d7. Now the [isRecDictEv] function in the ineration solver
1638 [case inert-given workitem-wanted] will prevent us from interacting d7 := d8
1639 precisely because chasing the evidence of d8 leads us to an unguarded use of d7.
1641 So, no interaction happens there. Then we meet d01 and there is no recursion
1642 problem there [isRectDictEv] gives us the OK to interact and we do solve d7 := d01!
1644 Note [SUPERCLASS-LOOP 1]
1645 ~~~~~~~~~~~~~~~~~~~~~~~~
1646 We have to be very, very careful when generating superclasses, lest we
1647 accidentally build a loop. Here's an example:
1651 class S a => C a where { opc :: a -> a }
1652 class S b => D b where { opd :: b -> b }
1654 instance C Int where
1657 instance D Int where
1660 From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int}
1661 Simplifying, we may well get:
1662 $dfCInt = :C ds1 (opd dd)
1665 Notice that we spot that we can extract ds1 from dd.
1667 Alas! Alack! We can do the same for (instance D Int):
1669 $dfDInt = :D ds2 (opc dc)
1673 And now we've defined the superclass in terms of itself.
1674 Two more nasty cases are in
1679 - Satisfy the superclass context *all by itself*
1680 (tcSimplifySuperClasses)
1681 - And do so completely; i.e. no left-over constraints
1682 to mix with the constraints arising from method declarations
1685 Note [SUPERCLASS-LOOP 2]
1686 ~~~~~~~~~~~~~~~~~~~~~~~~
1687 We need to be careful when adding "the constaint we are trying to prove".
1688 Suppose we are *given* d1:Ord a, and want to deduce (d2:C [a]) where
1690 class Ord a => C a where
1691 instance Ord [a] => C [a] where ...
1693 Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the
1694 superclasses of C [a] to avails. But we must not overwrite the binding
1695 for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
1698 Here's another variant, immortalised in tcrun020
1699 class Monad m => C1 m
1700 class C1 m => C2 m x
1701 instance C2 Maybe Bool
1702 For the instance decl we need to build (C1 Maybe), and it's no good if
1703 we run around and add (C2 Maybe Bool) and its superclasses to the avails
1704 before we search for C1 Maybe.
1706 Here's another example
1707 class Eq b => Foo a b
1708 instance Eq a => Foo [a] a
1712 we'll first deduce that it holds (via the instance decl). We must not
1713 then overwrite the Eq t constraint with a superclass selection!
1715 At first I had a gross hack, whereby I simply did not add superclass constraints
1716 in addWanted, though I did for addGiven and addIrred. This was sub-optimal,
1717 becuase it lost legitimate superclass sharing, and it still didn't do the job:
1718 I found a very obscure program (now tcrun021) in which improvement meant the
1719 simplifier got two bites a the cherry... so something seemed to be an Stop
1720 first time, but reducible next time.
1722 Now we implement the Right Solution, which is to check for loops directly
1723 when adding superclasses. It's a bit like the occurs check in unification.
1725 Note [Recursive instances and superclases]
1726 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1727 Consider this code, which arises in the context of "Scrap Your
1728 Boilerplate with Class".
1732 instance Sat (ctx Char) => Data ctx Char
1733 instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]
1735 class Data Maybe a => Foo a
1737 instance Foo t => Sat (Maybe t)
1739 instance Data Maybe a => Foo a
1740 instance Foo a => Foo [a]
1743 In the instance for Foo [a], when generating evidence for the superclasses
1744 (ie in tcSimplifySuperClasses) we need a superclass (Data Maybe [a]).
1745 Using the instance for Data, we therefore need
1746 (Sat (Maybe [a], Data Maybe a)
1747 But we are given (Foo a), and hence its superclass (Data Maybe a).
1748 So that leaves (Sat (Maybe [a])). Using the instance for Sat means
1749 we need (Foo [a]). And that is the very dictionary we are bulding
1750 an instance for! So we must put that in the "givens". So in this
1752 Given: Foo a, Foo [a]
1753 Wanted: Data Maybe [a]
1755 BUT we must *not not not* put the *superclasses* of (Foo [a]) in
1756 the givens, which is what 'addGiven' would normally do. Why? Because
1757 (Data Maybe [a]) is the superclass, so we'd "satisfy" the wanted
1758 by selecting a superclass from Foo [a], which simply makes a loop.
1760 On the other hand we *must* put the superclasses of (Foo a) in
1761 the givens, as you can see from the derivation described above.
1763 Conclusion: in the very special case of tcSimplifySuperClasses
1764 we have one 'given' (namely the "this" dictionary) whose superclasses
1765 must not be added to 'givens' by addGiven.
1767 There is a complication though. Suppose there are equalities
1768 instance (Eq a, a~b) => Num (a,b)
1769 Then we normalise the 'givens' wrt the equalities, so the original
1770 given "this" dictionary is cast to one of a different type. So it's a
1771 bit trickier than before to identify the "special" dictionary whose
1772 superclasses must not be added. See test
1773 indexed-types/should_run/EqInInstance
1775 We need a persistent property of the dictionary to record this
1776 special-ness. Current I'm using the InstLocOrigin (a bit of a hack,
1777 but cool), which is maintained by dictionary normalisation.
1778 Specifically, the InstLocOrigin is
1780 then the no-superclass thing kicks in. WATCH OUT if you fiddle
1783 Note [MATCHING-SYNONYMS]
1784 ~~~~~~~~~~~~~~~~~~~~~~~~
1785 When trying to match a dictionary (D tau) to a top-level instance, or a
1786 type family equation (F taus_1 ~ tau_2) to a top-level family instance,
1787 we do *not* need to expand type synonyms because the matcher will do that for us.
1790 Note [RHS-FAMILY-SYNONYMS]
1791 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1792 The RHS of a family instance is represented as yet another constructor which is
1793 like a type synonym for the real RHS the programmer declared. Eg:
1794 type instance F (a,a) = [a]
1796 :R32 a = [a] -- internal type synonym introduced
1797 F (a,a) ~ :R32 a -- instance
1799 When we react a family instance with a type family equation in the work list
1800 we keep the synonym-using RHS without expansion.
1803 *********************************************************************************
1805 The top-reaction Stage
1807 *********************************************************************************
1810 -- If a work item has any form of interaction with top-level we get this
1811 data TopInteractResult
1812 = NoTopInt -- No top-level interaction
1814 { tir_new_work :: WorkList -- Sub-goals or new work (could be given,
1815 -- for superclasses)
1816 , tir_new_inert :: StopOrContinue -- The input work item, ready to become *inert* now:
1817 } -- NB: in ``given'' (solved) form if the
1818 -- original was wanted or given and instance match
1819 -- was found, but may also be in wanted form if we
1820 -- only reacted with functional dependencies
1821 -- arising from top-level instances.
1823 topReactionsStage :: SimplifierStage
1824 topReactionsStage workItem inerts
1825 = do { tir <- tryTopReact workItem
1828 return $ SR { sr_inerts = inerts
1829 , sr_new_work = emptyWorkList
1830 , sr_stop = ContinueWith workItem }
1831 SomeTopInt tir_new_work tir_new_inert ->
1832 return $ SR { sr_inerts = inerts
1833 , sr_new_work = tir_new_work
1834 , sr_stop = tir_new_inert
1838 tryTopReact :: WorkItem -> TcS TopInteractResult
1839 tryTopReact workitem
1840 = do { -- A flag controls the amount of interaction allowed
1841 -- See Note [Simplifying RULE lhs constraints]
1842 ctxt <- getTcSContext
1843 ; if allowedTopReaction (simplEqsOnly ctxt) workitem
1844 then do { traceTcS "tryTopReact / calling doTopReact" (ppr workitem)
1845 ; doTopReact workitem }
1846 else return NoTopInt
1849 allowedTopReaction :: Bool -> WorkItem -> Bool
1850 allowedTopReaction eqs_only (CDictCan {}) = not eqs_only
1851 allowedTopReaction _ _ = True
1854 doTopReact :: WorkItem -> TcS TopInteractResult
1855 -- The work item does not react with the inert set,
1856 -- so try interaction with top-level instances
1858 -- Given dictionary; just add superclasses
1859 -- See Note [Given constraint that matches an instance declaration]
1860 doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Given loc
1861 , cc_class = cls, cc_tyargs = xis })
1862 = do { sc_work <- newGivenSCWork dv loc cls xis
1863 ; return $ SomeTopInt sc_work (ContinueWith workItem) }
1865 -- Derived dictionary
1866 -- Do not add any further derived superclasses; their
1867 -- full transitive closure has already been added.
1868 -- But do look for functional dependencies
1869 doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Derived loc _
1870 , cc_class = cls, cc_tyargs = xis })
1871 = do { fd_work <- findClassFunDeps dv cls xis loc
1872 ; if isEmptyWorkList fd_work then
1874 else return $ SomeTopInt { tir_new_work = fd_work
1875 , tir_new_inert = ContinueWith workItem } }
1877 doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Wanted loc
1878 , cc_class = cls, cc_tyargs = xis })
1879 = do { -- See Note [MATCHING-SYNONYMS]
1880 ; lkp_inst_res <- matchClassInst cls xis loc
1881 ; case lkp_inst_res of
1883 do { traceTcS "doTopReact/ no class instance for" (ppr dv)
1884 ; fd_work <- findClassFunDeps dv cls xis loc
1885 ; if isEmptyWorkList fd_work then
1886 do { sc_work <- newDerivedSCWork dv loc cls xis
1887 -- See Note [Adding Derived Superclasses]
1888 -- NB: workItem is inert, but it isn't solved
1889 -- keep it as inert, although it's not solved
1890 -- because we have now reacted all its
1891 -- top-level fundep-induced equalities!
1892 ; return $ SomeTopInt
1893 { tir_new_work = fd_work `unionWorkLists` sc_work
1894 , tir_new_inert = ContinueWith workItem } }
1896 else -- More fundep work produced, don't do any superclass stuff,
1897 -- just thow him back in the worklist, which will prioritize
1898 -- the solution of fd equalities
1900 { tir_new_work = fd_work `unionWorkLists`
1901 workListFromCCan workItem
1902 , tir_new_inert = Stop } }
1904 GenInst wtvs ev_term -> -- Solved
1905 -- No need to do fundeps stuff here; the instance
1906 -- matches already so we won't get any more info
1907 -- from functional dependencies
1908 do { traceTcS "doTopReact/ found class instance for" (ppr dv)
1909 ; setDictBind dv ev_term
1910 ; inst_work <- canWanteds wtvs
1912 -- Solved in one step and no new wanted work produced.
1913 -- i.e we directly matched a top-level instance
1914 -- No point in caching this in 'inert', nor in adding superclasses
1915 then return $ SomeTopInt { tir_new_work = emptyWorkList
1916 , tir_new_inert = Stop }
1918 -- Solved and new wanted work produced, you may cache the
1919 -- (tentatively solved) dictionary as Derived and its superclasses
1920 else do { let solved = makeSolvedByInst workItem
1921 ; sc_work <- newDerivedSCWork dv loc cls xis
1922 -- See Note [Adding Derived Superclasses]
1923 ; return $ SomeTopInt
1924 { tir_new_work = inst_work `unionWorkLists` sc_work
1925 , tir_new_inert = ContinueWith solved } }
1929 doTopReact (CFunEqCan { cc_id = cv, cc_flavor = fl
1930 , cc_fun = tc, cc_tyargs = args, cc_rhs = xi })
1931 = ASSERT (isSynFamilyTyCon tc) -- No associated data families have reached that far
1932 do { match_res <- matchFam tc args -- See Note [MATCHING-SYNONYMS]
1936 MatchInstSingle (rep_tc, rep_tys)
1937 -> do { let Just coe_tc = tyConFamilyCoercion_maybe rep_tc
1938 Just rhs_ty = tcView (mkTyConApp rep_tc rep_tys)
1939 -- Eagerly expand away the type synonym on the
1940 -- RHS of a type function, so that it never
1941 -- appears in an error message
1942 -- See Note [Type synonym families] in TyCon
1943 coe = mkTyConApp coe_tc rep_tys
1945 Wanted {} -> do { cv' <- newWantedCoVar rhs_ty xi
1946 ; setWantedCoBind cv $
1947 coe `mkTransCoercion`
1950 _ -> newGivOrDerCoVar xi rhs_ty $
1951 mkSymCoercion (mkCoVarCoercion cv) `mkTransCoercion` coe
1953 ; can_cts <- mkCanonical fl cv'
1954 ; return $ SomeTopInt can_cts Stop }
1956 -> panicTcS $ text "TcSMonad.matchFam returned multiple instances!"
1960 -- Any other work item does not react with any top-level equations
1961 doTopReact _workItem = return NoTopInt
1963 ----------------------
1964 findClassFunDeps :: EvVar -> Class -> [Xi] -> WantedLoc -> TcS WorkList
1965 -- Look for a fundep reaction beween the wanted item
1966 -- and a top-level instance declaration
1967 findClassFunDeps dv cls xis loc
1968 = do { instEnvs <- getInstEnvs
1969 ; let eqn_pred_locs = improveFromInstEnv (classInstances instEnvs)
1970 (ClassP cls xis, ppr dv)
1971 ; wevvars <- mkWantedFunDepEqns loc eqn_pred_locs
1972 -- NB: fundeps generate some wanted equalities, but
1973 -- we don't use their evidence for anything
1974 ; canWanteds wevvars }
1977 Note [Adding Derived Superclasses]
1978 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1979 Generally speaking, we want to be able to add derived superclasses of
1980 unsolved wanteds, and wanteds that have been partially being solved
1981 via an instance. This is important to be able to simplify the inferred
1982 constraints more (and to allow for recursive dictionaries, less
1983 importantly). Example:
1985 Inferred wanted constraint is (Eq a, Ord a), but we'd only like to
1986 quantify over Ord a, hence we would like to be able to add the
1987 superclass of Ord a as Derived and use it to solve the wanted Eq a.
1989 Hence we will add Derived superclasses in the following two cases:
1990 (1) When we meet an unsolved wanted in top-level reactions
1991 (2) When we partially solve a wanted in top-level reactions using an instance decl.
1993 At that point, we have two options:
1994 (1) Add transitively add *ALL* of the superclasses of the Derived
1995 (2) Add only the immediate ones, but whenever we meet a Derived in
1996 the future, add its own superclasses as Derived.
1998 Option (2) is terrible, because deriveds may be rewritten or kicked
1999 out of the inert set, which will result in slightly rewritten
2000 superclasses being reintroduced in the worklist and the inert set. Eg:
2003 instance Foo a => B [a]
2005 Original constraints:
2007 [Given] co : a ~ Int
2009 We apply the instance to the wanted and put it and its superclasses as
2010 as Deriveds in the inerts:
2013 [Derived] (sel d) : C [a]
2016 [Given] co : a ~ Int
2019 Now, suppose that we interact the Derived with the Given equality, and
2020 kick him out of the inert, the next time around a superclass C [Int]
2021 will be produced -- but we already *have* C [a] in the inerts which
2022 will anyway get rewritten to C [Int].
2024 So we choose (1), and *never* introduce any more superclass work from
2025 Deriveds. This enables yet another optimisation: If we ever meet an
2026 equality that can rewrite a Derived, if that Derived is a superclass
2027 derived (like C [a] above), i.e. not a partially solved one (like B
2028 [a]) above, we may simply completely *discard* that Derived. The
2029 reason is because somewhere in the inert lies the original wanted, or
2030 partially solved constraint that gave rise to that superclass, and
2031 that constraint *will* be kicked out, and *will* result in the
2032 rewritten superclass to be added in the inerts later on, anyway.
2036 Note [FunDep and implicit parameter reactions]
2037 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2038 Currently, our story of interacting two dictionaries (or a dictionary
2039 and top-level instances) for functional dependencies, and implicit
2040 paramters, is that we simply produce new wanted equalities. So for example
2042 class D a b | a -> b where ...
2048 We generate the extra work item
2050 where 'cv' is currently unused. However, this new item reacts with d2,
2051 discharging it in favour of a new constraint d2' thus:
2053 d2 := d2' |> D Int cv
2054 Now d2' can be discharged from d1
2056 We could be more aggressive and try to *immediately* solve the dictionary
2057 using those extra equalities. With the same inert set and work item we
2058 might dischard d2 directly:
2061 d2 := d1 |> D Int cv
2063 But in general it's a bit painful to figure out the necessary coercion,
2064 so we just take the first approach. Here is a better example. Consider:
2065 class C a b c | a -> b
2067 [Given] d1 : C T Int Char
2068 [Wanted] d2 : C T beta Int
2069 In this case, it's *not even possible* to solve the wanted immediately.
2070 So we should simply output the functional dependency and add this guy
2071 [but NOT its superclasses] back in the worklist. Even worse:
2072 [Given] d1 : C T Int beta
2073 [Wanted] d2: C T beta Int
2074 Then it is solvable, but its very hard to detect this on the spot.
2076 It's exactly the same with implicit parameters, except that the
2077 "aggressive" approach would be much easier to implement.
2079 Note [When improvement happens]
2080 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2081 We fire an improvement rule when
2083 * Two constraints match (modulo the fundep)
2084 e.g. C t1 t2, C t1 t3 where C a b | a->b
2085 The two match because the first arg is identical
2087 * At least one is not Given. If they are both given, we don't fire
2088 the reaction because we have no way of constructing evidence for a
2089 new equality nor does it seem right to create a new wanted goal
2090 (because the goal will most likely contain untouchables, which
2091 can't be solved anyway)!
2093 Note that we *do* fire the improvement if one is Given and one is Derived.
2094 The latter can be a superclass of a wanted goal. Example (tcfail138)
2095 class L a b | a -> b
2096 class (G a, L a b) => C a b
2098 instance C a b' => G (Maybe a)
2099 instance C a b => C (Maybe a) a
2100 instance L (Maybe a) a
2102 When solving the superclasses of the (C (Maybe a) a) instance, we get
2103 Given: C a b ... and hance by superclasses, (G a, L a b)
2105 Use the instance decl to get
2107 The (C a b') is inert, so we generate its Derived superclasses (L a b'),
2108 and now we need improvement between that derived superclass an the Given (L a b)
2110 Note [Overriding implicit parameters]
2111 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2113 f :: (?x::a) -> Bool -> a
2115 g v = let ?x::Int = 3
2116 in (f v, let ?x::Bool = True in f v)
2118 This should probably be well typed, with
2119 g :: Bool -> (Int, Bool)
2121 So the inner binding for ?x::Bool *overrides* the outer one.
2122 Hence a work-item Given overrides an inert-item Given.
2124 Note [Given constraint that matches an instance declaration]
2125 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2126 What should we do when we discover that one (or more) top-level
2127 instances match a given (or solved) class constraint? We have
2130 1. Reject the program. The reason is that there may not be a unique
2131 best strategy for the solver. Example, from the OutsideIn(X) paper:
2132 instance P x => Q [x]
2133 instance (x ~ y) => R [x] y
2135 wob :: forall a b. (Q [b], R b a) => a -> Int
2137 g :: forall a. Q [a] => [a] -> Int
2140 will generate the impliation constraint:
2141 Q [a] => (Q [beta], R beta [a])
2142 If we react (Q [beta]) with its top-level axiom, we end up with a
2143 (P beta), which we have no way of discharging. On the other hand,
2144 if we react R beta [a] with the top-level we get (beta ~ a), which
2145 is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
2146 now solvable by the given Q [a].
2148 However, this option is restrictive, for instance [Example 3] from
2149 Note [Recursive dictionaries] will fail to work.
2151 2. Ignore the problem, hoping that the situations where there exist indeed
2152 such multiple strategies are rare: Indeed the cause of the previous
2153 problem is that (R [x] y) yields the new work (x ~ y) which can be
2154 *spontaneously* solved, not using the givens.
2156 We are choosing option 2 below but we might consider having a flag as well.
2159 Note [New Wanted Superclass Work]
2160 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2161 Even in the case of wanted constraints, we add all of its superclasses as
2162 new given work. There are several reasons for this:
2163 a) to minimise error messages;
2164 eg suppose we have wanted (Eq a, Ord a)
2165 then we report only (Ord a) unsoluble
2167 b) to make the smallest number of constraints when *inferring* a type
2168 (same Eq/Ord example)
2170 c) for recursive dictionaries we *must* add the superclasses
2171 so that we can use them when solving a sub-problem
2173 d) To allow FD-like improvement for type families. Assume that
2175 class C a b | a -> b
2176 and we have to solve the implication constraint:
2178 Then, FD improvement can help us to produce a new wanted (beta ~ b)
2180 We want to have the same effect with the type family encoding of
2181 functional dependencies. Namely, consider:
2182 class (F a ~ b) => C a b
2183 Now suppose that we have:
2186 By interacting the given we will get given (F a ~ b) which is not
2187 enough by itself to make us discharge (C a beta). However, we
2188 may create a new derived equality from the super-class of the
2189 wanted constraint (C a beta), namely derived (F a ~ beta).
2190 Now we may interact this with given (F a ~ b) to get:
2192 But 'beta' is a touchable unification variable, and hence OK to
2193 unify it with 'b', replacing the derived evidence with the identity.
2195 This requires trySpontaneousSolve to solve *derived*
2196 equalities that have a touchable in their RHS, *in addition*
2197 to solving wanted equalities.
2199 Here is another example where this is useful.
2203 class (F a ~ b) => C a b
2204 And we are given the wanteds:
2208 We surely do *not* want to quantify over (b ~ c), since if someone provides
2209 dictionaries for (C a b) and (C a c), these dictionaries can provide a proof
2210 of (b ~ c), hence no extra evidence is necessary. Here is what will happen:
2212 Step 1: We will get new *given* superclass work,
2213 provisionally to our solving of w1 and w2
2215 g1: F a ~ b, g2 : F a ~ c,
2216 w1 : C a b, w2 : C a c, w3 : b ~ c
2218 The evidence for g1 and g2 is a superclass evidence term:
2220 g1 := sc w1, g2 := sc w2
2222 Step 2: The givens will solve the wanted w3, so that
2223 w3 := sym (sc w1) ; sc w2
2225 Step 3: Now, one may naively assume that then w2 can be solve from w1
2226 after rewriting with the (now solved equality) (b ~ c).
2228 But this rewriting is ruled out by the isGoodRectDict!
2230 Conclusion, we will (correctly) end up with the unsolved goals
2233 NB: The desugarer needs be more clever to deal with equalities
2234 that participate in recursive dictionary bindings.
2238 newGivenSCWork :: EvVar -> GivenLoc -> Class -> [Xi] -> TcS WorkList
2239 newGivenSCWork ev loc cls xis
2240 | NoScSkol <- ctLocOrigin loc -- Very important!
2241 = return emptyWorkList
2243 = newImmSCWorkFromFlavored ev (Given loc) cls xis >>= return
2245 newDerivedSCWork :: EvVar -> WantedLoc -> Class -> [Xi] -> TcS WorkList
2246 newDerivedSCWork ev loc cls xis
2247 = do { ims <- newImmSCWorkFromFlavored ev flavor cls xis
2250 rec_sc_work :: CanonicalCts -> TcS CanonicalCts
2252 = do { bg <- mapBagM (\c -> do { ims <- imm_sc_work c
2253 ; recs_ims <- rec_sc_work ims
2254 ; return $ consBag c recs_ims }) cts
2255 ; return $ concatBag bg }
2256 imm_sc_work (CDictCan { cc_id = dv, cc_flavor = fl, cc_class = cls, cc_tyargs = xis })
2257 = newImmSCWorkFromFlavored dv fl cls xis
2258 imm_sc_work _ct = return emptyCCan
2260 flavor = Derived loc DerSC
2262 newImmSCWorkFromFlavored :: EvVar -> CtFlavor -> Class -> [Xi] -> TcS WorkList
2263 -- Returns immediate superclasses
2264 newImmSCWorkFromFlavored ev flavor cls xis
2265 = do { let (tyvars, sc_theta, _, _) = classBigSig cls
2266 sc_theta1 = substTheta (zipTopTvSubst tyvars xis) sc_theta
2267 ; sc_vars <- zipWithM inst_one sc_theta1 [0..]
2268 ; mkCanonicals flavor sc_vars }
2270 inst_one pred n = newGivOrDerEvVar pred (EvSuperClass ev n)
2273 data LookupInstResult
2275 | GenInst [WantedEvVar] EvTerm
2277 matchClassInst :: Class -> [Type] -> WantedLoc -> TcS LookupInstResult
2278 matchClassInst clas tys loc
2279 = do { let pred = mkClassPred clas tys
2280 ; mb_result <- matchClass clas tys
2282 MatchInstNo -> return NoInstance
2283 MatchInstMany -> return NoInstance -- defer any reactions of a multitude until
2284 -- we learn more about the reagent
2285 MatchInstSingle (dfun_id, mb_inst_tys) ->
2286 do { checkWellStagedDFun pred dfun_id loc
2288 -- It's possible that not all the tyvars are in
2289 -- the substitution, tenv. For example:
2290 -- instance C X a => D X where ...
2291 -- (presumably there's a functional dependency in class C)
2292 -- Hence mb_inst_tys :: Either TyVar TcType
2294 ; tys <- instDFunTypes mb_inst_tys
2295 ; let (theta, _) = tcSplitPhiTy (applyTys (idType dfun_id) tys)
2296 ; if null theta then
2297 return (GenInst [] (EvDFunApp dfun_id tys []))
2299 { ev_vars <- instDFunConstraints theta
2300 ; let wevs = [WantedEvVar w loc | w <- ev_vars]
2301 ; return $ GenInst wevs (EvDFunApp dfun_id tys ev_vars) }