3 solveInteract, AtomicInert, tyVarsOfInert,
4 InertSet, emptyInert, updInertSet, extractUnsolved, solveOne, foldISEqCts
7 #include "HsVersions.h"
28 import Control.Monad ( when )
37 import qualified Data.Map as Map
39 import Control.Monad( unless )
40 import FastString ( sLit )
44 Note [InertSet invariants]
45 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
46 An InertSet is a bag of canonical constraints, with the following invariants:
48 1 No two constraints react with each other.
50 A tricky case is when there exists a given (solved) dictionary
51 constraint and a wanted identical constraint in the inert set, but do
52 not react because reaction would create loopy dictionary evidence for
53 the wanted. See note [Recursive dictionaries]
55 2 Given equalities form an idempotent substitution [none of the
56 given LHS's occur in any of the given RHS's or reactant parts]
58 3 Wanted equalities also form an idempotent substitution
60 4 The entire set of equalities is acyclic.
62 5 Wanted dictionaries are inert with the top-level axiom set
64 6 Equalities of the form tv1 ~ tv2 always have a touchable variable
65 on the left (if possible).
67 7 No wanted constraints tv1 ~ tv2 with tv1 touchable. Such constraints
68 will be marked as solved right before being pushed into the inert set.
69 See note [Touchables and givens].
71 8 No Given constraint mentions a touchable unification variable,
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).
87 data CCanMap a = CCanMap { cts_givder :: Map.Map a CanonicalCts
88 -- Invariant: all Given or Derived
89 , cts_wanted :: Map.Map a CanonicalCts }
90 -- Invariant: all Wanted
91 cCanMapToBag :: Ord a => CCanMap a -> CanonicalCts
92 cCanMapToBag cmap = Map.fold unionBags rest_cts (cts_givder cmap)
93 where rest_cts = Map.fold unionBags emptyCCan (cts_wanted cmap)
95 emptyCCanMap :: CCanMap a
96 emptyCCanMap = CCanMap { cts_givder = Map.empty, cts_wanted = Map.empty }
98 updCCanMap:: Ord a => (a,CanonicalCt) -> CCanMap a -> CCanMap a
99 updCCanMap (a,ct) cmap
100 = case cc_flavor ct of
102 -> cmap { cts_wanted = Map.insertWith unionBags a this_ct (cts_wanted cmap) }
104 -> cmap { cts_givder = Map.insertWith unionBags a this_ct (cts_givder cmap) }
105 where this_ct = singleCCan ct
107 getRelevantCts :: Ord a => a -> CCanMap a -> (CanonicalCts, CCanMap a)
108 -- Gets the relevant constraints and returns the rest of the CCanMap
109 getRelevantCts a cmap
110 = let relevant = unionBags (Map.findWithDefault emptyCCan a (cts_wanted cmap))
111 (Map.findWithDefault emptyCCan a (cts_givder cmap))
112 residual_map = cmap { cts_wanted = Map.delete a (cts_wanted cmap)
113 , cts_givder = Map.delete a (cts_givder cmap) }
114 in (relevant, residual_map)
116 extractUnsolvedCMap :: Ord a => CCanMap a -> (CanonicalCts, CCanMap a)
117 -- Gets the wanted constraints and returns a residual CCanMap
118 extractUnsolvedCMap cmap =
119 let unsolved = Map.fold unionBags emptyCCan (cts_wanted cmap)
120 in (unsolved, cmap { cts_wanted = Map.empty})
122 -- See Note [InertSet invariants]
124 = IS { inert_eqs :: CanonicalCts -- Equalities only (CTyEqCan)
126 , inert_dicts :: CCanMap Class -- Dictionaries only
127 , inert_ips :: CCanMap (IPName Name) -- Implicit parameters
128 , inert_funeqs :: CCanMap TyCon -- Type family equalities only
129 -- This representation allows us to quickly get to the relevant
130 -- inert constraints when interacting a work item with the inert set.
133 , inert_fds :: FDImprovements -- List of pairwise improvements that have kicked in already
134 -- and reside either in the worklist or in the inerts
137 tyVarsOfInert :: InertSet -> TcTyVarSet
138 tyVarsOfInert (IS { inert_eqs = eqs
139 , inert_dicts = dictmap
141 , inert_funeqs = funeqmap }) = tyVarsOfCanonicals cts
142 where cts = eqs `andCCan` cCanMapToBag dictmap
143 `andCCan` cCanMapToBag ipmap `andCCan` cCanMapToBag funeqmap
145 type FDImprovement = (PredType,PredType)
146 type FDImprovements = [(PredType,PredType)]
148 instance Outputable InertSet where
149 ppr is = vcat [ vcat (map ppr (Bag.bagToList $ inert_eqs is))
150 , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_dicts is)))
151 , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_ips is)))
152 , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_funeqs is)))
155 emptyInert :: InertSet
156 emptyInert = IS { inert_eqs = Bag.emptyBag
157 , inert_dicts = emptyCCanMap
158 , inert_ips = emptyCCanMap
159 , inert_funeqs = emptyCCanMap
162 updInertSet :: InertSet -> AtomicInert -> InertSet
164 | isCTyEqCan item -- Other equality
165 = let eqs' = inert_eqs is `Bag.snocBag` item
166 in is { inert_eqs = eqs' }
167 | Just cls <- isCDictCan_Maybe item -- Dictionary
168 = is { inert_dicts = updCCanMap (cls,item) (inert_dicts is) }
169 | Just x <- isCIPCan_Maybe item -- IP
170 = is { inert_ips = updCCanMap (x,item) (inert_ips is) }
171 | Just tc <- isCFunEqCan_Maybe item -- Function equality
172 = is { inert_funeqs = updCCanMap (tc,item) (inert_funeqs is) }
174 = pprPanic "Unknown form of constraint!" (ppr item)
176 updInertSetFDImprs :: InertSet -> Maybe FDImprovement -> InertSet
177 updInertSetFDImprs is (Just fdi) = is { inert_fds = fdi : inert_fds is }
178 updInertSetFDImprs is Nothing = is
180 foldISEqCtsM :: Monad m => (a -> AtomicInert -> m a) -> a -> InertSet -> m a
181 -- Fold over the equalities of the inerts
182 foldISEqCtsM k z IS { inert_eqs = eqs }
183 = Bag.foldlBagM k z eqs
185 foldISEqCts :: (a -> AtomicInert -> a) -> a -> InertSet -> a
186 foldISEqCts k z IS { inert_eqs = eqs }
187 = Bag.foldlBag k z eqs
189 extractUnsolved :: InertSet -> (InertSet, CanonicalCts)
190 -- Postcondition: the canonical cts returnd are the very same as the
191 -- WantedEvVars in their canonical form.
192 extractUnsolved is@(IS {inert_eqs = eqs})
193 = let is_solved = is { inert_eqs = solved_eqs
194 , inert_dicts = solved_dicts
195 , inert_ips = solved_ips
196 , inert_funeqs = solved_funeqs }
197 in (is_solved, unsolved)
199 where (unsolved_eqs, solved_eqs) = Bag.partitionBag isWantedCt eqs
200 (unsolved_ips, solved_ips) = extractUnsolvedCMap (inert_ips is)
201 (unsolved_dicts, solved_dicts) = extractUnsolvedCMap (inert_dicts is)
202 (unsolved_funeqs, solved_funeqs) = extractUnsolvedCMap (inert_funeqs is)
204 unsolved = unsolved_eqs `unionBags`
205 unsolved_ips `unionBags` unsolved_dicts `unionBags` unsolved_funeqs
207 haveBeenImproved :: FDImprovements -> PredType -> PredType -> Bool
208 haveBeenImproved [] _ _ = False
209 haveBeenImproved ((pty1,pty2):fdimprs) pty1' pty2'
210 | tcEqPred pty1 pty1' && tcEqPred pty2 pty2'
212 | tcEqPred pty1 pty2' && tcEqPred pty2 pty1'
215 = haveBeenImproved fdimprs pty1' pty2'
217 getFDImprovements :: InertSet -> FDImprovements
218 -- Return a list of the improvements that have kicked in so far
219 getFDImprovements = inert_fds
223 {-- DV: This note will go away!
225 Note [Touchables and givens]
226 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
227 Touchable variables will never show up in givens which are inputs to
228 the solver. However, touchables may show up in givens generated by the flattener.
243 which can be put in the inert set. Suppose we also have a wanted
247 We cannot rewrite the given G alpha ~g b using the wanted alpha ~w
248 Int. Instead, after reacting alpha ~w Int with the whole inert set,
249 we observe that we can solve it by unifying alpha with Int, so we mark
250 it as solved and put it back in the *work list*. [We also immediately unify
251 alpha := Int, without telling anyone, see trySpontaneousSolve function, to
252 avoid doing this in the end.]
254 Later, because it is solved (given, in effect), we can use it to rewrite
255 G alpha ~g b to G Int ~g b, which gets put back in the work list. Eventually,
256 we will dispatch the remaining wanted constraints using the top-level axioms.
258 Finally, note that after reacting a wanted equality with the entire inert set
259 we may end up with something like
263 which we should flip around to generate the solved constraint alpha ~s b.
269 %*********************************************************************
271 * Main Interaction Solver *
273 **********************************************************************
277 1. Canonicalise (unary)
278 2. Pairwise interaction (binary)
279 * Take one from work list
280 * Try all pair-wise interactions with each constraint in inert
282 As an optimisation, we prioritize the equalities both in the
283 worklist and in the inerts.
285 3. Try to solve spontaneously for equalities involving touchables
286 4. Top-level interaction (binary wrt top-level)
287 Superclass decomposition belongs in (4), see note [Superclasses]
290 type AtomicInert = CanonicalCt -- constraint pulled from InertSet
291 type WorkItem = CanonicalCt -- constraint pulled from WorkList
293 -- A mixture of Given, Wanted, and Derived constraints.
294 -- We split between equalities and the rest to process equalities first.
295 type WorkList = CanonicalCts
297 unionWorkLists :: WorkList -> WorkList -> WorkList
298 unionWorkLists = andCCan
300 isEmptyWorkList :: WorkList -> Bool
301 isEmptyWorkList = isEmptyCCan
303 emptyWorkList :: WorkList
304 emptyWorkList = emptyCCan
306 workListFromCCan :: CanonicalCt -> WorkList
307 workListFromCCan = singleCCan
309 ------------------------
311 = Stop -- Work item is consumed
312 | ContinueWith WorkItem -- Not consumed
314 instance Outputable StopOrContinue where
315 ppr Stop = ptext (sLit "Stop")
316 ppr (ContinueWith w) = ptext (sLit "ContinueWith") <+> ppr w
318 -- Results after interacting a WorkItem as far as possible with an InertSet
320 = SR { sr_inerts :: InertSet
321 -- The new InertSet to use (REPLACES the old InertSet)
322 , sr_new_work :: WorkList
323 -- Any new work items generated (should be ADDED to the old WorkList)
325 -- sr_stop = Just workitem => workitem is *not* in sr_inerts and
326 -- workitem is inert wrt to sr_inerts
327 , sr_stop :: StopOrContinue
330 instance Outputable StageResult where
331 ppr (SR { sr_inerts = inerts, sr_new_work = work, sr_stop = stop })
332 = ptext (sLit "SR") <+>
333 braces (sep [ ptext (sLit "inerts =") <+> ppr inerts <> comma
334 , ptext (sLit "new work =") <+> ppr work <> comma
335 , ptext (sLit "stop =") <+> ppr stop])
337 type SimplifierStage = WorkItem -> InertSet -> TcS StageResult
339 -- Combine a sequence of simplifier 'stages' to create a pipeline
340 runSolverPipeline :: [(String, SimplifierStage)]
341 -> InertSet -> WorkItem
342 -> TcS (InertSet, WorkList)
343 -- Precondition: non-empty list of stages
344 runSolverPipeline pipeline inerts workItem
345 = do { traceTcS "Start solver pipeline" $
346 vcat [ ptext (sLit "work item =") <+> ppr workItem
347 , ptext (sLit "inerts =") <+> ppr inerts]
349 ; let itr_in = SR { sr_inerts = inerts
350 , sr_new_work = emptyWorkList
351 , sr_stop = ContinueWith workItem }
352 ; itr_out <- run_pipeline pipeline itr_in
354 = case sr_stop itr_out of
355 Stop -> sr_inerts itr_out
356 ContinueWith item -> sr_inerts itr_out `updInertSet` item
357 ; return (new_inert, sr_new_work itr_out) }
359 run_pipeline :: [(String, SimplifierStage)]
360 -> StageResult -> TcS StageResult
361 run_pipeline [] itr = return itr
362 run_pipeline _ itr@(SR { sr_stop = Stop }) = return itr
364 run_pipeline ((name,stage):stages)
365 (SR { sr_new_work = accum_work
367 , sr_stop = ContinueWith work_item })
368 = do { itr <- stage work_item inerts
369 ; traceTcS ("Stage result (" ++ name ++ ")") (ppr itr)
370 ; let itr' = itr { sr_new_work = accum_work `unionWorkLists` sr_new_work itr }
371 ; run_pipeline stages itr' }
375 Inert: {c ~ d, F a ~ t, b ~ Int, a ~ ty} (all given)
376 Reagent: a ~ [b] (given)
378 React with (c~d) ==> IR (ContinueWith (a~[b])) True []
379 React with (F a ~ t) ==> IR (ContinueWith (a~[b])) False [F [b] ~ t]
380 React with (b ~ Int) ==> IR (ContinueWith (a~[Int]) True []
383 Inert: {c ~w d, F a ~g t, b ~w Int, a ~w ty}
386 React with (c ~w d) ==> IR (ContinueWith (a~[b])) True []
387 React with (F a ~g t) ==> IR (ContinueWith (a~[b])) True [] (can't rewrite given with wanted!)
391 Inert: {a ~ Int, F Int ~ b} (given)
392 Reagent: F a ~ b (wanted)
394 React with (a ~ Int) ==> IR (ContinueWith (F Int ~ b)) True []
395 React with (F Int ~ b) ==> IR Stop True [] -- after substituting we re-canonicalize and get nothing
398 -- Main interaction solver: we fully solve the worklist 'in one go',
399 -- returning an extended inert set.
401 -- See Note [Touchables and givens].
402 solveInteract :: InertSet -> Bag (CtFlavor,EvVar) -> TcS InertSet
403 solveInteract inert ws
404 = do { dyn_flags <- getDynFlags
405 ; sctx <- getTcSContext
407 ; traceTcS "solveInteract, before clever canonicalization:" $
408 ppr (mapBag (\(ct,ev) -> (ct,evVarPred ev)) ws)
410 ; can_ws <- foldlBagM (tryPreSolveAndCanon sctx inert) emptyCCan ws
412 ; traceTcS "solveInteract, after clever canonicalization:" $
415 ; solveInteractWithDepth (ctxtStkDepth dyn_flags,0,[]) inert can_ws }
417 tryPreSolveAndCanon :: SimplContext -> InertSet -> CanonicalCts -> (CtFlavor, EvVar) -> TcS CanonicalCts
418 -- Checks if this constraint can be immediately solved from a constraint in the
419 -- inert set or in the previously encountered CanonicalCts and only then
420 -- canonicalise it. See Note [Avoiding the superclass explosion]
421 tryPreSolveAndCanon sctx is cts_acc (fl,ev_var)
422 | ClassP clas tys <- evVarPred ev_var
423 , not $ simplEqsOnly sctx -- And we *can* discharge constraints from other constraints
424 = do { let (relevant_inert_dicts,_) = getRelevantCts clas (inert_dicts is)
425 ; b <- dischargeFromCans (cts_acc `unionBags` relevant_inert_dicts)
427 ; extra_cts <- if b then return emptyCCan else mkCanonical fl ev_var
428 ; return (cts_acc `unionBags` extra_cts) }
430 = do { extra_cts <- mkCanonical fl ev_var
431 ; return (cts_acc `unionBags` extra_cts) }
433 dischargeFromCans :: CanonicalCts -> (CtFlavor,EvVar,Class,[Type]) -> TcS Bool
434 dischargeFromCans cans (fl,ev,clas,tys)
435 = Bag.foldlBagM discharge_ct False cans
436 where discharge_ct :: Bool -> CanonicalCt -> TcS Bool
437 discharge_ct True _ct = return True
438 discharge_ct False (CDictCan { cc_id = ev1, cc_flavor = fl1
439 , cc_class = clas1, cc_tyargs = tys1 })
441 , (and $ zipWith tcEqType tys tys1)
443 = setEvBind ev (EvId ev1) >> return True
444 discharge_ct False _ct = return False
447 Note [Avoiding the superclass explosion]
448 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
450 Consider the example:
452 We have 5 wanted (Num alpha) constraints. If we simply try to canonicalize and add them
453 in our worklist, we will also get all of their superclasses as Derived, hence we will
454 have an inert set that contains 5*n constraints, where n is the number of superclasses
455 of of Num. That is bad for the additional reason that we keep *all* the Derived, even
456 for identical class constraints (for reasons related to recursive dictionaries).
458 Instead, what we do with tryPreSolveAndCanon, is when we encounter a new constraint,
459 such as the second (Num alpha) above we very quickly see if it can be immediately
460 discharged by a class constraint in our inert set or the previous canonicals. If so,
461 we add nothing to the returned canonical constraints.
463 For our particular example this will reduce the size of the inert set that we use from
464 5*n to just n. And hence the number of all possible interactions that we have to look
465 through is significantly smaller!
468 solveOne :: InertSet -> WorkItem -> TcS InertSet
469 solveOne inerts workItem
470 = do { dyn_flags <- getDynFlags
471 ; solveOneWithDepth (ctxtStkDepth dyn_flags,0,[]) inerts workItem
475 solveInteractWithDepth :: (Int, Int, [WorkItem])
476 -> InertSet -> WorkList -> TcS InertSet
477 solveInteractWithDepth ctxt@(max_depth,n,stack) inert ws
482 = solverDepthErrorTcS n stack
485 = do { traceTcS "solveInteractWithDepth" $
486 vcat [ text "Current depth =" <+> ppr n
487 , text "Max depth =" <+> ppr max_depth ]
489 -- Solve equalities first
490 ; let (eqs, non_eqs) = Bag.partitionBag isCTyEqCan ws
491 ; is_from_eqs <- Bag.foldlBagM (solveOneWithDepth ctxt) inert eqs
492 ; Bag.foldlBagM (solveOneWithDepth ctxt) is_from_eqs non_eqs }
495 -- Fully interact the given work item with an inert set, and return a
496 -- new inert set which has assimilated the new information.
497 solveOneWithDepth :: (Int, Int, [WorkItem])
498 -> InertSet -> WorkItem -> TcS InertSet
499 solveOneWithDepth (max_depth, n, stack) inert work
500 = do { traceTcS0 (indent ++ "Solving {") (ppr work)
501 ; (new_inert, new_work) <- runSolverPipeline thePipeline inert work
503 ; traceTcS0 (indent ++ "Subgoals:") (ppr new_work)
505 -- Recursively solve the new work generated
506 -- from workItem, with a greater depth
507 ; res_inert <- solveInteractWithDepth (max_depth, n+1, work:stack)
510 ; traceTcS0 (indent ++ "Done }") (ppr work)
513 indent = replicate (2*n) ' '
515 thePipeline :: [(String,SimplifierStage)]
516 thePipeline = [ ("interact with inert eqs", interactWithInertEqsStage)
517 , ("interact with inerts", interactWithInertsStage)
518 , ("spontaneous solve", spontaneousSolveStage)
519 , ("top-level reactions", topReactionsStage) ]
522 *********************************************************************************
524 The spontaneous-solve Stage
526 *********************************************************************************
528 Note [Efficient Orientation]
529 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
531 There are two cases where we have to be careful about
532 orienting equalities to get better efficiency.
534 Case 1: In Rewriting Equalities (function rewriteEqLHS)
536 When rewriting two equalities with the same LHS:
539 We have a choice of producing work (xi1 ~ xi2) (up-to the
540 canonicalization invariants) However, to prevent the inert items
541 from getting kicked out of the inerts first, we prefer to
542 canonicalize (xi1 ~ xi2) if (b) comes from the inert set, or (xi2
543 ~ xi1) if (a) comes from the inert set.
545 This choice is implemented using the WhichComesFromInert flag.
547 Case 2: Functional Dependencies
548 Again, we should prefer, if possible, the inert variables on the RHS
550 Case 3: IP improvement work
551 We must always rewrite so that the inert type is on the right.
554 spontaneousSolveStage :: SimplifierStage
555 spontaneousSolveStage workItem inerts
556 = do { mSolve <- trySpontaneousSolve workItem
559 SPCantSolve -> -- No spontaneous solution for him, keep going
560 return $ SR { sr_new_work = emptyWorkList
562 , sr_stop = ContinueWith workItem }
565 | not (isGivenCt workItem)
566 -- Original was wanted or derived but we have now made him
567 -- given so we have to interact him with the inerts due to
568 -- its status change. This in turn may produce more work.
569 -- We do this *right now* (rather than just putting workItem'
570 -- back into the work-list) because we've solved
571 -> do { (new_inert, new_work) <- runSolverPipeline
572 [ ("recursive interact with inert eqs", interactWithInertEqsStage)
573 , ("recursive interact with inerts", interactWithInertsStage)
575 ; return $ SR { sr_new_work = new_work
576 , sr_inerts = new_inert -- will include workItem'
580 -> -- Original was given; he must then be inert all right, and
581 -- workList' are all givens from flattening
582 return $ SR { sr_new_work = emptyWorkList
583 , sr_inerts = inerts `updInertSet` workItem'
585 SPError -> -- Return with no new work
586 return $ SR { sr_new_work = emptyWorkList
591 data SPSolveResult = SPCantSolve | SPSolved WorkItem | SPError
592 -- SPCantSolve means that we can't do the unification because e.g. the variable is untouchable
593 -- SPSolved workItem' gives us a new *given* to go on
594 -- SPError means that it's completely impossible to solve this equality, eg due to a kind error
597 -- @trySpontaneousSolve wi@ solves equalities where one side is a
598 -- touchable unification variable.
599 -- See Note [Touchables and givens]
600 trySpontaneousSolve :: WorkItem -> TcS SPSolveResult
601 trySpontaneousSolve workItem@(CTyEqCan { cc_id = cv, cc_flavor = gw, cc_tyvar = tv1, cc_rhs = xi })
604 | Just tv2 <- tcGetTyVar_maybe xi
605 = do { tch1 <- isTouchableMetaTyVar tv1
606 ; tch2 <- isTouchableMetaTyVar tv2
607 ; case (tch1, tch2) of
608 (True, True) -> trySpontaneousEqTwoWay cv gw tv1 tv2
609 (True, False) -> trySpontaneousEqOneWay cv gw tv1 xi
610 (False, True) -> trySpontaneousEqOneWay cv gw tv2 (mkTyVarTy tv1)
611 _ -> return SPCantSolve }
613 = do { tch1 <- isTouchableMetaTyVar tv1
614 ; if tch1 then trySpontaneousEqOneWay cv gw tv1 xi
615 else do { traceTcS "Untouchable LHS, can't spontaneously solve workitem:" (ppr workItem)
616 ; return SPCantSolve }
620 -- trySpontaneousSolve (CFunEqCan ...) = ...
621 -- See Note [No touchables as FunEq RHS] in TcSMonad
622 trySpontaneousSolve _ = return SPCantSolve
625 trySpontaneousEqOneWay :: CoVar -> CtFlavor -> TcTyVar -> Xi -> TcS SPSolveResult
626 -- tv is a MetaTyVar, not untouchable
627 trySpontaneousEqOneWay cv gw tv xi
628 | not (isSigTyVar tv) || isTyVarTy xi
629 = do { let kxi = typeKind xi -- NB: 'xi' is fully rewritten according to the inerts
630 -- so we have its more specific kind in our hands
631 ; if kxi `isSubKind` tyVarKind tv then
632 solveWithIdentity cv gw tv xi
633 else if tyVarKind tv `isSubKind` kxi then
634 return SPCantSolve -- kinds are compatible but we can't solveWithIdentity this way
635 -- This case covers the a_touchable :: * ~ b_untouchable :: ??
636 -- which has to be deferred or floated out for someone else to solve
637 -- it in a scope where 'b' is no longer untouchable.
638 else do { addErrorTcS KindError gw (mkTyVarTy tv) xi -- See Note [Kind errors]
641 | otherwise -- Still can't solve, sig tyvar and non-variable rhs
645 trySpontaneousEqTwoWay :: CoVar -> CtFlavor -> TcTyVar -> TcTyVar -> TcS SPSolveResult
646 -- Both tyvars are *touchable* MetaTyvars so there is only a chance for kind error here
647 trySpontaneousEqTwoWay cv gw tv1 tv2
649 , nicer_to_update_tv2 = solveWithIdentity cv gw tv2 (mkTyVarTy tv1)
651 = solveWithIdentity cv gw tv1 (mkTyVarTy tv2)
652 | otherwise -- None is a subkind of the other, but they are both touchable!
653 = do { addErrorTcS KindError gw (mkTyVarTy tv1) (mkTyVarTy tv2)
658 nicer_to_update_tv2 = isSigTyVar tv1 || isSystemName (Var.varName tv2)
662 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
663 Consider the wanted problem:
664 alpha ~ (# Int, Int #)
665 where alpha :: ?? and (# Int, Int #) :: (#). We can't spontaneously solve this constraint,
666 but we should rather reject the program that give rise to it. If 'trySpontaneousEqTwoWay'
667 simply returns @CantSolve@ then that wanted constraint is going to propagate all the way and
668 get quantified over in inference mode. That's bad because we do know at this point that the
669 constraint is insoluble. Instead, we call 'recKindErrorTcS' here, which will fail later on.
671 The same applies in canonicalization code in case of kind errors in the givens.
673 However, when we canonicalize givens we only check for compatibility (@compatKind@).
674 If there were a kind error in the givens, this means some form of inconsistency or dead code.
676 You may think that when we spontaneously solve wanteds we may have to look through the
677 bindings to determine the right kind of the RHS type. E.g one may be worried that xi is
678 @alpha@ where alpha :: ? and a previous spontaneous solving has set (alpha := f) with (f :: *).
679 But we orient our constraints so that spontaneously solved ones can rewrite all other constraint
680 so this situation can't happen.
682 Note [Spontaneous solving and kind compatibility]
683 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
685 Note that our canonical constraints insist that only *given* equalities (tv ~ xi)
686 or (F xis ~ rhs) require the LHS and the RHS to have exactly the same kinds.
688 - We have to require this because:
689 Given equalities can be freely used to rewrite inside
690 other types or constraints.
691 - We do not have to do the same for wanteds because:
692 First, wanted equations (tv ~ xi) where tv is a touchable
693 unification variable may have kinds that do not agree (the
694 kind of xi must be a sub kind of the kind of tv). Second, any
695 potential kind mismatch will result in the constraint not
696 being soluble, which will be reported anyway. This is the
697 reason that @trySpontaneousOneWay@ and @trySpontaneousTwoWay@
698 will perform a kind compatibility check, and only then will
699 they proceed to @solveWithIdentity@.
702 - Givens from higher-rank, such as:
703 type family T b :: * -> * -> *
704 type instance T Bool = (->)
706 f :: forall a. ((T a ~ (->)) => ...) -> a -> ...
708 Whereas we would be able to apply the type instance, we would not be able to
709 use the given (T Bool ~ (->)) in the body of 'flop'
712 Note [Avoid double unifications]
713 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
714 The spontaneous solver has to return a given which mentions the unified unification
715 variable *on the left* of the equality. Here is what happens if not:
716 Original wanted: (a ~ alpha), (alpha ~ Int)
717 We spontaneously solve the first wanted, without changing the order!
718 given : a ~ alpha [having unified alpha := a]
719 Now the second wanted comes along, but he cannot rewrite the given, so we simply continue.
720 At the end we spontaneously solve that guy, *reunifying* [alpha := Int]
722 We avoid this problem by orienting the resulting given so that the unification
723 variable is on the left. [Note that alternatively we could attempt to
724 enforce this at canonicalization]
726 See also Note [No touchables as FunEq RHS] in TcSMonad; avoiding
727 double unifications is the main reason we disallow touchable
728 unification variables as RHS of type family equations: F xis ~ alpha.
733 solveWithIdentity :: CoVar -> CtFlavor -> TcTyVar -> Xi -> TcS SPSolveResult
734 -- Solve with the identity coercion
735 -- Precondition: kind(xi) is a sub-kind of kind(tv)
736 -- Precondition: CtFlavor is Wanted or Derived
737 -- See [New Wanted Superclass Work] to see why solveWithIdentity
738 -- must work for Derived as well as Wanted
739 -- Returns: workItem where
740 -- workItem = the new Given constraint
741 solveWithIdentity cv wd tv xi
742 = do { traceTcS "Sneaky unification:" $
743 vcat [text "Coercion variable: " <+> ppr wd,
744 text "Coercion: " <+> pprEq (mkTyVarTy tv) xi,
745 text "Left Kind is : " <+> ppr (typeKind (mkTyVarTy tv)),
746 text "Right Kind is : " <+> ppr (typeKind xi)
749 ; setWantedTyBind tv xi -- Set tv := xi_unflat
750 ; cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi xi
752 ; case wd of Wanted {} -> setWantedCoBind cv xi
753 Derived {} -> setDerivedCoBind cv xi
754 _ -> pprPanic "Can't spontaneously solve given!" empty
756 ; return $ SPSolved (CTyEqCan { cc_id = cv_given
757 , cc_flavor = mkGivenFlavor wd UnkSkol
758 , cc_tyvar = tv, cc_rhs = xi })
766 *********************************************************************************
768 The interact-with-inert Stage
770 *********************************************************************************
773 -- Interaction result of WorkItem <~> AtomicInert
775 = IR { ir_stop :: StopOrContinue
777 -- => Reagent (work item) consumed.
778 -- ContinueWith new_reagent
779 -- => Reagent transformed but keep gathering interactions.
780 -- The transformed item remains inert with respect
781 -- to any previously encountered inerts.
783 , ir_inert_action :: InertAction
784 -- Whether the inert item should remain in the InertSet.
786 , ir_new_work :: WorkList
787 -- new work items to add to the WorkList
789 , ir_improvement :: Maybe FDImprovement -- In case improvement kicked in
792 -- What to do with the inert reactant.
793 data InertAction = KeepInert
795 | KeepTransformedInert CanonicalCt -- Keep a slightly transformed inert
797 mkIRContinue :: Monad m => WorkItem -> InertAction -> WorkList -> m InteractResult
798 mkIRContinue wi keep newWork = return $ IR (ContinueWith wi) keep newWork Nothing
800 mkIRStop :: Monad m => InertAction -> WorkList -> m InteractResult
801 mkIRStop keep newWork = return $ IR Stop keep newWork Nothing
803 mkIRStop_RecordImprovement :: Monad m => InertAction -> WorkList -> FDImprovement -> m InteractResult
804 mkIRStop_RecordImprovement keep newWork fdimpr = return $ IR Stop keep newWork (Just fdimpr)
806 dischargeWorkItem :: Monad m => m InteractResult
807 dischargeWorkItem = mkIRStop KeepInert emptyWorkList
809 noInteraction :: Monad m => WorkItem -> m InteractResult
810 noInteraction workItem = mkIRContinue workItem KeepInert emptyWorkList
812 data WhichComesFromInert = LeftComesFromInert | RightComesFromInert
813 -- See Note [Efficient Orientation]
816 ---------------------------------------------------
817 -- Interact a single WorkItem with the equalities of an inert set as far as possible, i.e. until we
818 -- get a Stop result from an individual reaction (i.e. when the WorkItem is consumed), or until we've
819 -- interact the WorkItem with the entire equalities of the InertSet
821 interactWithInertEqsStage :: SimplifierStage
822 interactWithInertEqsStage workItem inert
823 = foldISEqCtsM interactNext initITR inert
824 where initITR = SR { sr_inerts = IS { inert_eqs = emptyCCan -- Will fold over equalities
825 , inert_dicts = inert_dicts inert
826 , inert_ips = inert_ips inert
827 , inert_funeqs = inert_funeqs inert
828 , inert_fds = inert_fds inert
830 , sr_new_work = emptyWorkList
831 , sr_stop = ContinueWith workItem }
834 ---------------------------------------------------
835 -- Interact a single WorkItem with *non-equality* constraints in the inert set.
836 -- Precondition: equality interactions must have already happened, hence we have
837 -- to pick up some information from the incoming inert, before folding over the
838 -- "Other" constraints it contains!
840 interactWithInertsStage :: SimplifierStage
841 interactWithInertsStage workItem inert
842 = let (relevant, inert_residual) = getISRelevant workItem inert
843 initITR = SR { sr_inerts = inert_residual
844 , sr_new_work = emptyWorkList
845 , sr_stop = ContinueWith workItem }
846 in Bag.foldlBagM interactNext initITR relevant
848 getISRelevant :: CanonicalCt -> InertSet -> (CanonicalCts, InertSet)
849 getISRelevant (CDictCan { cc_class = cls } ) is
850 = let (relevant, residual_map) = getRelevantCts cls (inert_dicts is)
851 in (relevant, is { inert_dicts = residual_map })
852 getISRelevant (CFunEqCan { cc_fun = tc } ) is
853 = let (relevant, residual_map) = getRelevantCts tc (inert_funeqs is)
854 in (relevant, is { inert_funeqs = residual_map })
855 getISRelevant (CIPCan { cc_ip_nm = nm }) is
856 = let (relevant, residual_map) = getRelevantCts nm (inert_ips is)
857 in (relevant, is { inert_ips = residual_map })
858 -- An equality, finally, may kick everything except equalities out
859 -- because we have already interacted the equalities in interactWithInertEqsStage
860 getISRelevant _eq_ct is -- Equality, everything is relevant for this one
861 -- TODO: if we were caching variables, we'd know that only
862 -- some are relevant. Experiment with this for now.
863 = let cts = cCanMapToBag (inert_ips is) `unionBags`
864 cCanMapToBag (inert_dicts is) `unionBags` cCanMapToBag (inert_funeqs is)
865 in (cts, is { inert_dicts = emptyCCanMap
866 , inert_ips = emptyCCanMap
867 , inert_funeqs = emptyCCanMap })
869 interactNext :: StageResult -> AtomicInert -> TcS StageResult
870 interactNext it inert
871 | ContinueWith workItem <- sr_stop it
872 = do { let inerts = sr_inerts it
873 fdimprs_old = getFDImprovements inerts
875 ; ir <- interactWithInert fdimprs_old inert workItem
877 -- New inerts depend on whether we KeepInert or not and must
878 -- be updated with FD improvement information from the interaction result (ir)
879 ; let inerts_new = updInertSetFDImprs upd_inert (ir_improvement ir)
880 upd_inert = case ir_inert_action ir of
881 KeepInert -> inerts `updInertSet` inert
883 KeepTransformedInert inert' -> inerts `updInertSet` inert'
885 ; return $ SR { sr_inerts = inerts_new
886 , sr_new_work = sr_new_work it `unionWorkLists` ir_new_work ir
887 , sr_stop = ir_stop ir } }
889 = return $ it { sr_inerts = (sr_inerts it) `updInertSet` inert }
891 -- Do a single interaction of two constraints.
892 interactWithInert :: FDImprovements -> AtomicInert -> WorkItem -> TcS InteractResult
893 interactWithInert fdimprs inert workitem
894 = do { ctxt <- getTcSContext
895 ; let is_allowed = allowedInteraction (simplEqsOnly ctxt) inert workitem
896 inert_ev = cc_id inert
897 work_ev = cc_id workitem
899 -- Never interact a wanted and a derived where the derived's evidence
900 -- mentions the wanted evidence in an unguarded way.
901 -- See Note [Superclasses and recursive dictionaries]
902 -- and Note [New Wanted Superclass Work]
903 -- We don't have to do this for givens, as we fully know the evidence for them.
905 case (cc_flavor inert, cc_flavor workitem) of
906 (Wanted {}, Derived {}) -> isGoodRecEv work_ev inert_ev
907 (Derived {}, Wanted {}) -> isGoodRecEv inert_ev work_ev
910 ; if is_allowed && rec_ev_ok then
911 doInteractWithInert fdimprs inert workitem
913 noInteraction workitem
916 allowedInteraction :: Bool -> AtomicInert -> WorkItem -> Bool
917 -- Allowed interactions
918 allowedInteraction eqs_only (CDictCan {}) (CDictCan {}) = not eqs_only
919 allowedInteraction eqs_only (CIPCan {}) (CIPCan {}) = not eqs_only
920 allowedInteraction _ _ _ = True
922 --------------------------------------------
923 doInteractWithInert :: FDImprovements -> CanonicalCt -> CanonicalCt -> TcS InteractResult
924 -- Identical class constraints.
926 doInteractWithInert fdimprs
927 (CDictCan { cc_id = d1, cc_flavor = fl1, cc_class = cls1, cc_tyargs = tys1 })
928 workItem@(CDictCan { cc_flavor = fl2, cc_class = cls2, cc_tyargs = tys2 })
929 | cls1 == cls2 && (and $ zipWith tcEqType tys1 tys2)
930 = solveOneFromTheOther (d1,fl1) workItem
932 | cls1 == cls2 && (not (isGiven fl1 && isGiven fl2))
933 = -- See Note [When improvement happens]
934 do { let pty1 = ClassP cls1 tys1
935 pty2 = ClassP cls2 tys2
936 work_item_pred_loc = (pty2, pprFlavorArising fl2)
937 inert_pred_loc = (pty1, pprFlavorArising fl1)
938 loc = combineCtLoc fl1 fl2
939 eqn_pred_locs = improveFromAnother work_item_pred_loc inert_pred_loc
940 -- See Note [Efficient Orientation]
942 ; wevvars <- mkWantedFunDepEqns loc eqn_pred_locs
943 ; fd_work <- canWanteds wevvars
944 -- See Note [Generating extra equalities]
945 ; traceTcS "Checking if improvements existed." (ppr fdimprs)
946 ; if isEmptyWorkList fd_work || haveBeenImproved fdimprs pty1 pty2 then
948 mkIRContinue workItem KeepInert fd_work
949 else do { traceTcS "Recording improvement and throwing item back in worklist." (ppr (pty1,pty2))
950 ; mkIRStop_RecordImprovement KeepInert
951 (fd_work `unionWorkLists` workListFromCCan workItem) (pty1,pty2)
953 -- See Note [FunDep Reactions]
956 -- Class constraint and given equality: use the equality to rewrite
957 -- the class constraint.
958 doInteractWithInert _fdimprs
959 (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi })
960 (CDictCan { cc_id = dv, cc_flavor = wfl, cc_class = cl, cc_tyargs = xis })
961 | ifl `canRewrite` wfl
962 , tv `elemVarSet` tyVarsOfTypes xis
963 = do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,wfl,cl,xis)
964 -- Continue with rewritten Dictionary because we can only be in the
965 -- interactWithEqsStage, so the dictionary is inert.
966 ; mkIRContinue rewritten_dict KeepInert emptyWorkList }
968 doInteractWithInert _fdimprs
969 (CDictCan { cc_id = dv, cc_flavor = ifl, cc_class = cl, cc_tyargs = xis })
970 workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
971 | wfl `canRewrite` ifl
972 , tv `elemVarSet` tyVarsOfTypes xis
973 = do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,ifl,cl,xis)
974 ; mkIRContinue workItem DropInert (workListFromCCan rewritten_dict) }
976 -- Class constraint and given equality: use the equality to rewrite
977 -- the class constraint.
978 doInteractWithInert _fdimprs
979 (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi })
980 (CIPCan { cc_id = ipid, cc_flavor = wfl, cc_ip_nm = nm, cc_ip_ty = ty })
981 | ifl `canRewrite` wfl
982 , tv `elemVarSet` tyVarsOfType ty
983 = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,wfl,nm,ty)
984 ; mkIRContinue rewritten_ip KeepInert emptyWorkList }
986 doInteractWithInert _fdimprs
987 (CIPCan { cc_id = ipid, cc_flavor = ifl, cc_ip_nm = nm, cc_ip_ty = ty })
988 workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
989 | wfl `canRewrite` ifl
990 , tv `elemVarSet` tyVarsOfType ty
991 = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,ifl,nm,ty)
992 ; mkIRContinue workItem DropInert (workListFromCCan rewritten_ip) }
994 -- Two implicit parameter constraints. If the names are the same,
995 -- but their types are not, we generate a wanted type equality
996 -- that equates the type (this is "improvement").
997 -- However, we don't actually need the coercion evidence,
998 -- so we just generate a fresh coercion variable that isn't used anywhere.
999 doInteractWithInert _fdimprs
1000 (CIPCan { cc_id = id1, cc_flavor = ifl, cc_ip_nm = nm1, cc_ip_ty = ty1 })
1001 workItem@(CIPCan { cc_flavor = wfl, cc_ip_nm = nm2, cc_ip_ty = ty2 })
1002 | nm1 == nm2 && isGiven wfl && isGiven ifl
1003 = -- See Note [Overriding implicit parameters]
1004 -- Dump the inert item, override totally with the new one
1005 -- Do not require type equality
1006 mkIRContinue workItem DropInert emptyWorkList
1008 | nm1 == nm2 && ty1 `tcEqType` ty2
1009 = solveOneFromTheOther (id1,ifl) workItem
1012 = -- See Note [When improvement happens]
1013 do { co_var <- newWantedCoVar ty2 ty1 -- See Note [Efficient Orientation]
1014 ; let flav = Wanted (combineCtLoc ifl wfl)
1015 ; cans <- mkCanonical flav co_var
1016 ; mkIRContinue workItem KeepInert cans }
1020 -- Never rewrite a given with a wanted equality, and a type function
1021 -- equality can never rewrite an equality. We rewrite LHS *and* RHS
1022 -- of function equalities so that our inert set exposes everything that
1023 -- we know about equalities.
1025 -- Inert: equality, work item: function equality
1026 doInteractWithInert _fdimprs
1027 (CTyEqCan { cc_id = cv1, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi1 })
1028 (CFunEqCan { cc_id = cv2, cc_flavor = wfl, cc_fun = tc
1029 , cc_tyargs = args, cc_rhs = xi2 })
1030 | ifl `canRewrite` wfl
1031 , tv `elemVarSet` tyVarsOfTypes (xi2:args) -- Rewrite RHS as well
1032 = do { rewritten_funeq <- rewriteFunEq (cv1,tv,xi1) (cv2,wfl,tc,args,xi2)
1033 ; mkIRStop KeepInert (workListFromCCan rewritten_funeq) }
1034 -- Must Stop here, because we may no longer be inert after the rewritting.
1036 -- Inert: function equality, work item: equality
1037 doInteractWithInert _fdimprs
1038 (CFunEqCan {cc_id = cv1, cc_flavor = ifl, cc_fun = tc
1039 , cc_tyargs = args, cc_rhs = xi1 })
1040 workItem@(CTyEqCan { cc_id = cv2, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi2 })
1041 | wfl `canRewrite` ifl
1042 , tv `elemVarSet` tyVarsOfTypes (xi1:args) -- Rewrite RHS as well
1043 = do { rewritten_funeq <- rewriteFunEq (cv2,tv,xi2) (cv1,ifl,tc,args,xi1)
1044 ; mkIRContinue workItem DropInert (workListFromCCan rewritten_funeq) }
1045 -- One may think that we could (KeepTransformedInert rewritten_funeq)
1046 -- but that is wrong, because it may end up not being inert with respect
1047 -- to future inerts. Example:
1048 -- Original inert = { F xis ~ [a], b ~ Maybe Int }
1049 -- Work item comes along = a ~ [b]
1050 -- If we keep { F xis ~ [b] } in the inert set we will end up with:
1051 -- { F xis ~ [b], b ~ Maybe Int, a ~ [Maybe Int] }
1052 -- At the end, which is *not* inert. So we should unfortunately DropInert here.
1054 doInteractWithInert _fdimprs
1055 (CFunEqCan { cc_id = cv1, cc_flavor = fl1, cc_fun = tc1
1056 , cc_tyargs = args1, cc_rhs = xi1 })
1057 workItem@(CFunEqCan { cc_id = cv2, cc_flavor = fl2, cc_fun = tc2
1058 , cc_tyargs = args2, cc_rhs = xi2 })
1059 | fl1 `canSolve` fl2 && lhss_match
1060 = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
1061 ; mkIRStop KeepInert cans }
1062 | fl2 `canSolve` fl1 && lhss_match
1063 = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
1064 ; mkIRContinue workItem DropInert cans }
1066 lhss_match = tc1 == tc2 && and (zipWith tcEqType args1 args2)
1068 doInteractWithInert _fdimprs
1069 (CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
1070 workItem@(CTyEqCan { cc_id = cv2, cc_flavor = fl2, cc_tyvar = tv2, cc_rhs = xi2 })
1071 -- Check for matching LHS
1072 | fl1 `canSolve` fl2 && tv1 == tv2
1073 = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
1074 ; mkIRStop KeepInert cans }
1076 | fl2 `canSolve` fl1 && tv1 == tv2
1077 = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
1078 ; mkIRContinue workItem DropInert cans }
1079 -- Check for rewriting RHS
1080 | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfType xi2
1081 = do { rewritten_eq <- rewriteEqRHS (cv1,tv1,xi1) (cv2,fl2,tv2,xi2)
1082 ; mkIRStop KeepInert rewritten_eq }
1083 | fl2 `canRewrite` fl1 && tv2 `elemVarSet` tyVarsOfType xi1
1084 = do { rewritten_eq <- rewriteEqRHS (cv2,tv2,xi2) (cv1,fl1,tv1,xi1)
1085 ; mkIRContinue workItem DropInert rewritten_eq }
1087 -- Fall-through case for all other situations
1088 doInteractWithInert _fdimprs _ workItem = noInteraction workItem
1090 -------------------------
1091 -- Equational Rewriting
1092 rewriteDict :: (CoVar, TcTyVar, Xi) -> (DictId, CtFlavor, Class, [Xi]) -> TcS CanonicalCt
1093 rewriteDict (cv,tv,xi) (dv,gw,cl,xis)
1094 = do { let cos = substTysWith [tv] [mkCoVarCoercion cv] xis -- xis[tv] ~ xis[xi]
1095 args = substTysWith [tv] [xi] xis
1097 dict_co = mkTyConCoercion con cos
1098 ; dv' <- newDictVar cl args
1100 Wanted {} -> setDictBind dv (EvCast dv' (mkSymCoercion dict_co))
1101 _given_or_derived -> setDictBind dv' (EvCast dv dict_co)
1102 ; return (CDictCan { cc_id = dv'
1105 , cc_tyargs = args }) }
1107 rewriteIP :: (CoVar,TcTyVar,Xi) -> (EvVar,CtFlavor, IPName Name, TcType) -> TcS CanonicalCt
1108 rewriteIP (cv,tv,xi) (ipid,gw,nm,ty)
1109 = do { let ip_co = substTyWith [tv] [mkCoVarCoercion cv] ty -- ty[tv] ~ t[xi]
1110 ty' = substTyWith [tv] [xi] ty
1111 ; ipid' <- newIPVar nm ty'
1113 Wanted {} -> setIPBind ipid (EvCast ipid' (mkSymCoercion ip_co))
1114 _given_or_derived -> setIPBind ipid' (EvCast ipid ip_co)
1115 ; return (CIPCan { cc_id = ipid'
1118 , cc_ip_ty = ty' }) }
1120 rewriteFunEq :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TyCon, [Xi], Xi) -> TcS CanonicalCt
1121 rewriteFunEq (cv1,tv,xi1) (cv2,gw, tc,args,xi2) -- cv2 :: F args ~ xi2
1122 = do { let arg_cos = substTysWith [tv] [mkCoVarCoercion cv1] args
1123 args' = substTysWith [tv] [xi1] args
1124 fun_co = mkTyConCoercion tc arg_cos -- fun_co :: F args ~ F args'
1126 xi2' = substTyWith [tv] [xi1] xi2
1127 xi2_co = substTyWith [tv] [mkCoVarCoercion cv1] xi2 -- xi2_co :: xi2 ~ xi2'
1128 ; cv2' <- case gw of
1129 Wanted {} -> do { cv2' <- newWantedCoVar (mkTyConApp tc args') xi2'
1130 ; setWantedCoBind cv2 $
1131 fun_co `mkTransCoercion`
1132 mkCoVarCoercion cv2' `mkTransCoercion` mkSymCoercion xi2_co
1134 _giv_or_der -> newGivOrDerCoVar (mkTyConApp tc args') xi2' $
1135 mkSymCoercion fun_co `mkTransCoercion`
1136 mkCoVarCoercion cv2 `mkTransCoercion` xi2_co
1137 ; return (CFunEqCan { cc_id = cv2'
1141 , cc_rhs = xi2' }) }
1144 rewriteEqRHS :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TcTyVar,Xi) -> TcS WorkList
1145 -- Use the first equality to rewrite the second, flavors already checked.
1146 -- E.g. c1 : tv1 ~ xi1 c2 : tv2 ~ xi2
1147 -- rewrites c2 to give
1148 -- c2' : tv2 ~ xi2[xi1/tv1]
1149 -- We must do an occurs check to sure the new constraint is canonical
1150 -- So we might return an empty bag
1151 rewriteEqRHS (cv1,tv1,xi1) (cv2,gw,tv2,xi2)
1152 | Just tv2' <- tcGetTyVar_maybe xi2'
1153 , tv2 == tv2' -- In this case xi2[xi1/tv1] = tv2, so we have tv2~tv2
1154 = do { when (isWanted gw) (setWantedCoBind cv2 (mkSymCoercion co2'))
1155 ; return emptyCCan }
1160 -> do { cv2' <- newWantedCoVar (mkTyVarTy tv2) xi2'
1161 ; setWantedCoBind cv2 $
1162 mkCoVarCoercion cv2' `mkTransCoercion` mkSymCoercion co2'
1165 -> newGivOrDerCoVar (mkTyVarTy tv2) xi2' $
1166 mkCoVarCoercion cv2 `mkTransCoercion` co2'
1168 ; canEq gw cv2' (mkTyVarTy tv2) xi2'
1171 xi2' = substTyWith [tv1] [xi1] xi2
1172 co2' = substTyWith [tv1] [mkCoVarCoercion cv1] xi2 -- xi2 ~ xi2[xi1/tv1]
1175 rewriteEqLHS :: WhichComesFromInert -> (Coercion,Xi) -> (CoVar,CtFlavor,Xi) -> TcS WorkList
1176 -- Used to ineract two equalities of the following form:
1177 -- First Equality: co1: (XXX ~ xi1)
1178 -- Second Equality: cv2: (XXX ~ xi2)
1179 -- Where the cv1 `canSolve` cv2 equality
1180 -- We have an option of creating new work (xi1 ~ xi2) OR (xi2 ~ xi1),
1181 -- See Note [Efficient Orientation] for that
1182 rewriteEqLHS which (co1,xi1) (cv2,gw,xi2)
1183 = do { cv2' <- case (isWanted gw, which) of
1184 (True,LeftComesFromInert) ->
1185 do { cv2' <- newWantedCoVar xi2 xi1
1186 ; setWantedCoBind cv2 $
1187 co1 `mkTransCoercion` mkSymCoercion (mkCoVarCoercion cv2')
1189 (True,RightComesFromInert) ->
1190 do { cv2' <- newWantedCoVar xi1 xi2
1191 ; setWantedCoBind cv2 $
1192 co1 `mkTransCoercion` mkCoVarCoercion cv2'
1194 (False,LeftComesFromInert) ->
1195 newGivOrDerCoVar xi2 xi1 $
1196 mkSymCoercion (mkCoVarCoercion cv2) `mkTransCoercion` co1
1197 (False,RightComesFromInert) ->
1198 newGivOrDerCoVar xi1 xi2 $
1199 mkSymCoercion co1 `mkTransCoercion` mkCoVarCoercion cv2
1200 ; mkCanonical gw cv2'
1203 solveOneFromTheOther :: (EvVar, CtFlavor) -> CanonicalCt -> TcS InteractResult
1204 -- First argument inert, second argument workitem. They both represent
1205 -- wanted/given/derived evidence for the *same* predicate so we try here to
1206 -- discharge one directly from the other.
1208 -- Precondition: value evidence only (implicit parameters, classes)
1210 solveOneFromTheOther (iid,ifl) workItem
1211 -- Both derived needs a special case. You might think that we do not need
1212 -- two evidence terms for the same claim. But, since the evidence is partial,
1213 -- either evidence may do in some cases; see TcSMonad.isGoodRecEv.
1214 -- See also Example 3 in Note [Superclasses and recursive dictionaries]
1215 | isDerived ifl && isDerived wfl
1216 = noInteraction workItem
1218 | ifl `canSolve` wfl
1219 = do { unless (isGiven wfl) $ setEvBind wid (EvId iid)
1220 -- Overwrite the binding, if one exists
1221 -- For Givens, which are lambda-bound, nothing to overwrite,
1222 ; dischargeWorkItem }
1224 | otherwise -- wfl `canSolve` ifl
1225 = do { unless (isGiven ifl) $ setEvBind iid (EvId wid)
1226 ; mkIRContinue workItem DropInert emptyWorkList }
1229 wfl = cc_flavor workItem
1230 wid = cc_id workItem
1233 Note [Superclasses and recursive dictionaries]
1234 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1235 Overlaps with Note [SUPERCLASS-LOOP 1]
1236 Note [SUPERCLASS-LOOP 2]
1237 Note [Recursive instances and superclases]
1238 ToDo: check overlap and delete redundant stuff
1240 Right before adding a given into the inert set, we must
1241 produce some more work, that will bring the superclasses
1242 of the given into scope. The superclass constraints go into
1245 When we simplify a wanted constraint, if we first see a matching
1246 instance, we may produce new wanted work. To (1) avoid doing this work
1247 twice in the future and (2) to handle recursive dictionaries we may ``cache''
1248 this item as solved (in effect, given) into our inert set and with that add
1249 its superclass constraints (as given) in our worklist.
1251 But now we have added partially solved constraints to the worklist which may
1252 interact with other wanteds. Consider the example:
1256 class Eq b => Foo a b --- 0-th selector
1257 instance Eq a => Foo [a] a --- fooDFun
1259 and wanted (Foo [t] t). We are first going to see that the instance matches
1260 and create an inert set that includes the solved (Foo [t] t) and its
1262 d1 :_g Foo [t] t d1 := EvDFunApp fooDFun d3
1263 d2 :_g Eq t d2 := EvSuperClass d1 0
1264 Our work list is going to contain a new *wanted* goal
1266 It is wrong to react the wanted (Eq t) with the given (Eq t) because that would
1267 construct loopy evidence. Hence the check isGoodRecEv in doInteractWithInert.
1269 OK, so we have ruled out bad behaviour, but how do we ge recursive dictionaries,
1274 data D r = ZeroD | SuccD (r (D r));
1276 instance (Eq (r (D r))) => Eq (D r) where
1277 ZeroD == ZeroD = True
1278 (SuccD a) == (SuccD b) = a == b
1281 equalDC :: D [] -> D [] -> Bool;
1284 We need to prove (Eq (D [])). Here's how we go:
1288 by instance decl, holds if
1292 *BUT* we have an inert set which gives us (no superclasses):
1294 By the instance declaration of Eq we can show the 'd2' goal if
1296 where d2 = dfEqList d3
1298 Now, however this wanted can interact with our inert d1 to set:
1300 and solve the goal. Why was this interaction OK? Because, if we chase the
1301 evidence of d1 ~~> dfEqD d2 ~~-> dfEqList d3, so by setting d3 := d1 we
1303 d3 := dfEqD2 (dfEqList d3)
1304 which is FINE because the use of d3 is protected by the instance function
1307 So, our strategy is to try to put solved wanted dictionaries into the
1308 inert set along with their superclasses (when this is meaningful,
1309 i.e. when new wanted goals are generated) but solve a wanted dictionary
1310 from a given only in the case where the evidence variable of the
1311 wanted is mentioned in the evidence of the given (recursively through
1312 the evidence binds) in a protected way: more instance function applications
1313 than superclass selectors.
1315 Here are some more examples from GHC's previous type checker
1319 This code arises in the context of "Scrap Your Boilerplate with Class"
1323 instance Sat (ctx Char) => Data ctx Char -- dfunData1
1324 instance (Sat (ctx [a]), Data ctx a) => Data ctx [a] -- dfunData2
1326 class Data Maybe a => Foo a
1328 instance Foo t => Sat (Maybe t) -- dfunSat
1330 instance Data Maybe a => Foo a -- dfunFoo1
1331 instance Foo a => Foo [a] -- dfunFoo2
1332 instance Foo [Char] -- dfunFoo3
1334 Consider generating the superclasses of the instance declaration
1335 instance Foo a => Foo [a]
1337 So our problem is this
1339 d1 :_w Data Maybe [t]
1341 We may add the given in the inert set, along with its superclasses
1342 [assuming we don't fail because there is a matching instance, see
1343 tryTopReact, given case ]
1347 d01 :_g Data Maybe t -- d2 := EvDictSuperClass d0 0
1348 d1 :_w Data Maybe [t]
1349 Then d2 can readily enter the inert, and we also do solving of the wanted
1352 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1354 d2 :_w Sat (Maybe [t])
1356 d01 :_g Data Maybe t
1357 Now, we may simplify d2 more:
1360 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1361 d1 :_g Data Maybe [t]
1362 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1366 d01 :_g Data Maybe t
1368 Now, we can just solve d3.
1371 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1372 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1375 d01 :_g Data Maybe t
1376 And now we can simplify d4 again, but since it has superclasses we *add* them to the worklist:
1379 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1380 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1381 d4 :_g Foo [t] d4 := dfunFoo2 d5
1384 d6 :_g Data Maybe [t] d6 := EvDictSuperClass d4 0
1385 d01 :_g Data Maybe t
1386 Now, d5 can be solved! (and its superclass enter scope)
1389 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1390 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1391 d4 :_g Foo [t] d4 := dfunFoo2 d5
1392 d5 :_g Foo t d5 := dfunFoo1 d7
1395 d6 :_g Data Maybe [t]
1396 d8 :_g Data Maybe t d8 := EvDictSuperClass d5 0
1397 d01 :_g Data Maybe t
1400 [1] Suppose we pick d8 and we react him with d01. Which of the two givens should
1401 we keep? Well, we *MUST NOT* drop d01 because d8 contains recursive evidence
1402 that must not be used (look at case interactInert where both inert and workitem
1403 are givens). So we have several options:
1404 - Drop the workitem always (this will drop d8)
1405 This feels very unsafe -- what if the work item was the "good" one
1406 that should be used later to solve another wanted?
1407 - Don't drop anyone: the inert set may contain multiple givens!
1408 [This is currently implemented]
1410 The "don't drop anyone" seems the most safe thing to do, so now we come to problem 2:
1411 [2] We have added both d6 and d01 in the inert set, and we are interacting our wanted
1412 d7. Now the [isRecDictEv] function in the ineration solver
1413 [case inert-given workitem-wanted] will prevent us from interacting d7 := d8
1414 precisely because chasing the evidence of d8 leads us to an unguarded use of d7.
1416 So, no interaction happens there. Then we meet d01 and there is no recursion
1417 problem there [isRectDictEv] gives us the OK to interact and we do solve d7 := d01!
1419 Note [SUPERCLASS-LOOP 1]
1420 ~~~~~~~~~~~~~~~~~~~~~~~~
1421 We have to be very, very careful when generating superclasses, lest we
1422 accidentally build a loop. Here's an example:
1426 class S a => C a where { opc :: a -> a }
1427 class S b => D b where { opd :: b -> b }
1429 instance C Int where
1432 instance D Int where
1435 From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int}
1436 Simplifying, we may well get:
1437 $dfCInt = :C ds1 (opd dd)
1440 Notice that we spot that we can extract ds1 from dd.
1442 Alas! Alack! We can do the same for (instance D Int):
1444 $dfDInt = :D ds2 (opc dc)
1448 And now we've defined the superclass in terms of itself.
1449 Two more nasty cases are in
1454 - Satisfy the superclass context *all by itself*
1455 (tcSimplifySuperClasses)
1456 - And do so completely; i.e. no left-over constraints
1457 to mix with the constraints arising from method declarations
1460 Note [SUPERCLASS-LOOP 2]
1461 ~~~~~~~~~~~~~~~~~~~~~~~~
1462 We need to be careful when adding "the constaint we are trying to prove".
1463 Suppose we are *given* d1:Ord a, and want to deduce (d2:C [a]) where
1465 class Ord a => C a where
1466 instance Ord [a] => C [a] where ...
1468 Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the
1469 superclasses of C [a] to avails. But we must not overwrite the binding
1470 for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
1473 Here's another variant, immortalised in tcrun020
1474 class Monad m => C1 m
1475 class C1 m => C2 m x
1476 instance C2 Maybe Bool
1477 For the instance decl we need to build (C1 Maybe), and it's no good if
1478 we run around and add (C2 Maybe Bool) and its superclasses to the avails
1479 before we search for C1 Maybe.
1481 Here's another example
1482 class Eq b => Foo a b
1483 instance Eq a => Foo [a] a
1487 we'll first deduce that it holds (via the instance decl). We must not
1488 then overwrite the Eq t constraint with a superclass selection!
1490 At first I had a gross hack, whereby I simply did not add superclass constraints
1491 in addWanted, though I did for addGiven and addIrred. This was sub-optimal,
1492 becuase it lost legitimate superclass sharing, and it still didn't do the job:
1493 I found a very obscure program (now tcrun021) in which improvement meant the
1494 simplifier got two bites a the cherry... so something seemed to be an Stop
1495 first time, but reducible next time.
1497 Now we implement the Right Solution, which is to check for loops directly
1498 when adding superclasses. It's a bit like the occurs check in unification.
1500 Note [Recursive instances and superclases]
1501 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1502 Consider this code, which arises in the context of "Scrap Your
1503 Boilerplate with Class".
1507 instance Sat (ctx Char) => Data ctx Char
1508 instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]
1510 class Data Maybe a => Foo a
1512 instance Foo t => Sat (Maybe t)
1514 instance Data Maybe a => Foo a
1515 instance Foo a => Foo [a]
1518 In the instance for Foo [a], when generating evidence for the superclasses
1519 (ie in tcSimplifySuperClasses) we need a superclass (Data Maybe [a]).
1520 Using the instance for Data, we therefore need
1521 (Sat (Maybe [a], Data Maybe a)
1522 But we are given (Foo a), and hence its superclass (Data Maybe a).
1523 So that leaves (Sat (Maybe [a])). Using the instance for Sat means
1524 we need (Foo [a]). And that is the very dictionary we are bulding
1525 an instance for! So we must put that in the "givens". So in this
1527 Given: Foo a, Foo [a]
1528 Wanted: Data Maybe [a]
1530 BUT we must *not not not* put the *superclasses* of (Foo [a]) in
1531 the givens, which is what 'addGiven' would normally do. Why? Because
1532 (Data Maybe [a]) is the superclass, so we'd "satisfy" the wanted
1533 by selecting a superclass from Foo [a], which simply makes a loop.
1535 On the other hand we *must* put the superclasses of (Foo a) in
1536 the givens, as you can see from the derivation described above.
1538 Conclusion: in the very special case of tcSimplifySuperClasses
1539 we have one 'given' (namely the "this" dictionary) whose superclasses
1540 must not be added to 'givens' by addGiven.
1542 There is a complication though. Suppose there are equalities
1543 instance (Eq a, a~b) => Num (a,b)
1544 Then we normalise the 'givens' wrt the equalities, so the original
1545 given "this" dictionary is cast to one of a different type. So it's a
1546 bit trickier than before to identify the "special" dictionary whose
1547 superclasses must not be added. See test
1548 indexed-types/should_run/EqInInstance
1550 We need a persistent property of the dictionary to record this
1551 special-ness. Current I'm using the InstLocOrigin (a bit of a hack,
1552 but cool), which is maintained by dictionary normalisation.
1553 Specifically, the InstLocOrigin is
1555 then the no-superclass thing kicks in. WATCH OUT if you fiddle
1558 Note [MATCHING-SYNONYMS]
1559 ~~~~~~~~~~~~~~~~~~~~~~~~
1560 When trying to match a dictionary (D tau) to a top-level instance, or a
1561 type family equation (F taus_1 ~ tau_2) to a top-level family instance,
1562 we do *not* need to expand type synonyms because the matcher will do that for us.
1565 Note [RHS-FAMILY-SYNONYMS]
1566 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1567 The RHS of a family instance is represented as yet another constructor which is
1568 like a type synonym for the real RHS the programmer declared. Eg:
1569 type instance F (a,a) = [a]
1571 :R32 a = [a] -- internal type synonym introduced
1572 F (a,a) ~ :R32 a -- instance
1574 When we react a family instance with a type family equation in the work list
1575 we keep the synonym-using RHS without expansion.
1578 *********************************************************************************
1580 The top-reaction Stage
1582 *********************************************************************************
1585 -- If a work item has any form of interaction with top-level we get this
1586 data TopInteractResult
1587 = NoTopInt -- No top-level interaction
1589 { tir_new_work :: WorkList -- Sub-goals or new work (could be given,
1590 -- for superclasses)
1591 , tir_new_inert :: StopOrContinue -- The input work item, ready to become *inert* now:
1592 } -- NB: in ``given'' (solved) form if the
1593 -- original was wanted or given and instance match
1594 -- was found, but may also be in wanted form if we
1595 -- only reacted with functional dependencies
1596 -- arising from top-level instances.
1598 topReactionsStage :: SimplifierStage
1599 topReactionsStage workItem inerts
1600 = do { tir <- tryTopReact workItem
1603 return $ SR { sr_inerts = inerts
1604 , sr_new_work = emptyWorkList
1605 , sr_stop = ContinueWith workItem }
1606 SomeTopInt tir_new_work tir_new_inert ->
1607 return $ SR { sr_inerts = inerts
1608 , sr_new_work = tir_new_work
1609 , sr_stop = tir_new_inert
1613 tryTopReact :: WorkItem -> TcS TopInteractResult
1614 tryTopReact workitem
1615 = do { -- A flag controls the amount of interaction allowed
1616 -- See Note [Simplifying RULE lhs constraints]
1617 ctxt <- getTcSContext
1618 ; if allowedTopReaction (simplEqsOnly ctxt) workitem
1619 then do { traceTcS "tryTopReact / calling doTopReact" (ppr workitem)
1620 ; doTopReact workitem }
1621 else return NoTopInt
1624 allowedTopReaction :: Bool -> WorkItem -> Bool
1625 allowedTopReaction eqs_only (CDictCan {}) = not eqs_only
1626 allowedTopReaction _ _ = True
1629 doTopReact :: WorkItem -> TcS TopInteractResult
1630 -- The work item does not react with the inert set, so try interaction with top-level instances
1631 -- NB: The place to add superclasses in *not* in doTopReact stage. Instead superclasses are
1632 -- added in the worklist as part of the canonicalisation process.
1633 -- See Note [Adding superclasses] in TcCanonical.
1636 -- See Note [Given constraint that matches an instance declaration]
1637 doTopReact (CDictCan { cc_flavor = Given {} })
1638 = return NoTopInt -- NB: Superclasses already added since it's canonical
1640 -- Derived dictionary: just look for functional dependencies
1641 doTopReact workItem@(CDictCan { cc_flavor = Derived loc _
1642 , cc_class = cls, cc_tyargs = xis })
1643 = do { fd_work <- findClassFunDeps cls xis loc
1644 ; if isEmptyWorkList fd_work then
1646 else return $ SomeTopInt { tir_new_work = fd_work
1647 , tir_new_inert = ContinueWith workItem } }
1648 -- Wanted dictionary
1649 doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Wanted loc
1650 , cc_class = cls, cc_tyargs = xis })
1651 = do { -- See Note [MATCHING-SYNONYMS]
1652 ; lkp_inst_res <- matchClassInst cls xis loc
1653 ; case lkp_inst_res of
1655 do { traceTcS "doTopReact/ no class instance for" (ppr dv)
1656 ; fd_work <- findClassFunDeps cls xis loc
1657 ; if isEmptyWorkList fd_work then
1659 { tir_new_work = emptyWorkList
1660 , tir_new_inert = ContinueWith workItem }
1661 else -- More fundep work produced, just thow him back in the
1662 -- worklist to prioritize the solution of fd equalities
1664 { tir_new_work = fd_work `unionWorkLists` workListFromCCan workItem
1665 , tir_new_inert = Stop } }
1667 GenInst wtvs ev_term -> -- Solved
1668 -- No need to do fundeps stuff here; the instance
1669 -- matches already so we won't get any more info
1670 -- from functional dependencies
1671 do { traceTcS "doTopReact/ found class instance for" (ppr dv)
1672 ; setDictBind dv ev_term
1673 ; inst_work <- canWanteds wtvs
1675 -- Solved in one step and no new wanted work produced.
1676 -- i.e we directly matched a top-level instance
1677 -- No point in caching this in 'inert'
1678 then return $ SomeTopInt { tir_new_work = emptyWorkList
1679 , tir_new_inert = Stop }
1681 -- Solved and new wanted work produced, you may cache the
1682 -- (tentatively solved) dictionary as Derived
1683 else do { let solved = makeSolvedByInst workItem
1684 ; return $ SomeTopInt
1685 { tir_new_work = inst_work
1686 , tir_new_inert = ContinueWith solved } }
1690 doTopReact (CFunEqCan { cc_id = cv, cc_flavor = fl
1691 , cc_fun = tc, cc_tyargs = args, cc_rhs = xi })
1692 = ASSERT (isSynFamilyTyCon tc) -- No associated data families have reached that far
1693 do { match_res <- matchFam tc args -- See Note [MATCHING-SYNONYMS]
1697 MatchInstSingle (rep_tc, rep_tys)
1698 -> do { let Just coe_tc = tyConFamilyCoercion_maybe rep_tc
1699 Just rhs_ty = tcView (mkTyConApp rep_tc rep_tys)
1700 -- Eagerly expand away the type synonym on the
1701 -- RHS of a type function, so that it never
1702 -- appears in an error message
1703 -- See Note [Type synonym families] in TyCon
1704 coe = mkTyConApp coe_tc rep_tys
1706 Wanted {} -> do { cv' <- newWantedCoVar rhs_ty xi
1707 ; setWantedCoBind cv $
1708 coe `mkTransCoercion`
1711 _ -> newGivOrDerCoVar xi rhs_ty $
1712 mkSymCoercion (mkCoVarCoercion cv) `mkTransCoercion` coe
1714 ; can_cts <- mkCanonical fl cv'
1715 ; return $ SomeTopInt can_cts Stop }
1717 -> panicTcS $ text "TcSMonad.matchFam returned multiple instances!"
1721 -- Any other work item does not react with any top-level equations
1722 doTopReact _workItem = return NoTopInt
1724 ----------------------
1725 findClassFunDeps :: Class -> [Xi] -> WantedLoc -> TcS WorkList
1726 -- Look for a fundep reaction beween the wanted item
1727 -- and a top-level instance declaration
1728 findClassFunDeps cls xis loc
1729 = do { instEnvs <- getInstEnvs
1730 ; let eqn_pred_locs = improveFromInstEnv (classInstances instEnvs)
1731 (ClassP cls xis, pprArisingAt loc)
1732 ; wevvars <- mkWantedFunDepEqns loc eqn_pred_locs
1733 -- NB: fundeps generate some wanted equalities, but
1734 -- we don't use their evidence for anything
1735 ; canWanteds wevvars }
1739 Note [FunDep and implicit parameter reactions]
1740 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1741 Currently, our story of interacting two dictionaries (or a dictionary
1742 and top-level instances) for functional dependencies, and implicit
1743 paramters, is that we simply produce new wanted equalities. So for example
1745 class D a b | a -> b where ...
1751 We generate the extra work item
1753 where 'cv' is currently unused. However, this new item reacts with d2,
1754 discharging it in favour of a new constraint d2' thus:
1756 d2 := d2' |> D Int cv
1757 Now d2' can be discharged from d1
1759 We could be more aggressive and try to *immediately* solve the dictionary
1760 using those extra equalities. With the same inert set and work item we
1761 might dischard d2 directly:
1764 d2 := d1 |> D Int cv
1766 But in general it's a bit painful to figure out the necessary coercion,
1767 so we just take the first approach. Here is a better example. Consider:
1768 class C a b c | a -> b
1770 [Given] d1 : C T Int Char
1771 [Wanted] d2 : C T beta Int
1772 In this case, it's *not even possible* to solve the wanted immediately.
1773 So we should simply output the functional dependency and add this guy
1774 [but NOT its superclasses] back in the worklist. Even worse:
1775 [Given] d1 : C T Int beta
1776 [Wanted] d2: C T beta Int
1777 Then it is solvable, but its very hard to detect this on the spot.
1779 It's exactly the same with implicit parameters, except that the
1780 "aggressive" approach would be much easier to implement.
1782 Note [When improvement happens]
1783 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1784 We fire an improvement rule when
1786 * Two constraints match (modulo the fundep)
1787 e.g. C t1 t2, C t1 t3 where C a b | a->b
1788 The two match because the first arg is identical
1790 * At least one is not Given. If they are both given, we don't fire
1791 the reaction because we have no way of constructing evidence for a
1792 new equality nor does it seem right to create a new wanted goal
1793 (because the goal will most likely contain untouchables, which
1794 can't be solved anyway)!
1796 Note that we *do* fire the improvement if one is Given and one is Derived.
1797 The latter can be a superclass of a wanted goal. Example (tcfail138)
1798 class L a b | a -> b
1799 class (G a, L a b) => C a b
1801 instance C a b' => G (Maybe a)
1802 instance C a b => C (Maybe a) a
1803 instance L (Maybe a) a
1805 When solving the superclasses of the (C (Maybe a) a) instance, we get
1806 Given: C a b ... and hance by superclasses, (G a, L a b)
1808 Use the instance decl to get
1810 The (C a b') is inert, so we generate its Derived superclasses (L a b'),
1811 and now we need improvement between that derived superclass an the Given (L a b)
1813 Note [Overriding implicit parameters]
1814 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1816 f :: (?x::a) -> Bool -> a
1818 g v = let ?x::Int = 3
1819 in (f v, let ?x::Bool = True in f v)
1821 This should probably be well typed, with
1822 g :: Bool -> (Int, Bool)
1824 So the inner binding for ?x::Bool *overrides* the outer one.
1825 Hence a work-item Given overrides an inert-item Given.
1827 Note [Given constraint that matches an instance declaration]
1828 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1829 What should we do when we discover that one (or more) top-level
1830 instances match a given (or solved) class constraint? We have
1833 1. Reject the program. The reason is that there may not be a unique
1834 best strategy for the solver. Example, from the OutsideIn(X) paper:
1835 instance P x => Q [x]
1836 instance (x ~ y) => R [x] y
1838 wob :: forall a b. (Q [b], R b a) => a -> Int
1840 g :: forall a. Q [a] => [a] -> Int
1843 will generate the impliation constraint:
1844 Q [a] => (Q [beta], R beta [a])
1845 If we react (Q [beta]) with its top-level axiom, we end up with a
1846 (P beta), which we have no way of discharging. On the other hand,
1847 if we react R beta [a] with the top-level we get (beta ~ a), which
1848 is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
1849 now solvable by the given Q [a].
1851 However, this option is restrictive, for instance [Example 3] from
1852 Note [Recursive dictionaries] will fail to work.
1854 2. Ignore the problem, hoping that the situations where there exist indeed
1855 such multiple strategies are rare: Indeed the cause of the previous
1856 problem is that (R [x] y) yields the new work (x ~ y) which can be
1857 *spontaneously* solved, not using the givens.
1859 We are choosing option 2 below but we might consider having a flag as well.
1862 Note [New Wanted Superclass Work]
1863 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1864 Even in the case of wanted constraints, we add all of its superclasses as
1865 new given work. There are several reasons for this:
1866 a) to minimise error messages;
1867 eg suppose we have wanted (Eq a, Ord a)
1868 then we report only (Ord a) unsoluble
1870 b) to make the smallest number of constraints when *inferring* a type
1871 (same Eq/Ord example)
1873 c) for recursive dictionaries we *must* add the superclasses
1874 so that we can use them when solving a sub-problem
1876 d) To allow FD-like improvement for type families. Assume that
1878 class C a b | a -> b
1879 and we have to solve the implication constraint:
1881 Then, FD improvement can help us to produce a new wanted (beta ~ b)
1883 We want to have the same effect with the type family encoding of
1884 functional dependencies. Namely, consider:
1885 class (F a ~ b) => C a b
1886 Now suppose that we have:
1889 By interacting the given we will get given (F a ~ b) which is not
1890 enough by itself to make us discharge (C a beta). However, we
1891 may create a new derived equality from the super-class of the
1892 wanted constraint (C a beta), namely derived (F a ~ beta).
1893 Now we may interact this with given (F a ~ b) to get:
1895 But 'beta' is a touchable unification variable, and hence OK to
1896 unify it with 'b', replacing the derived evidence with the identity.
1898 This requires trySpontaneousSolve to solve *derived*
1899 equalities that have a touchable in their RHS, *in addition*
1900 to solving wanted equalities.
1902 Here is another example where this is useful.
1906 class (F a ~ b) => C a b
1907 And we are given the wanteds:
1911 We surely do *not* want to quantify over (b ~ c), since if someone provides
1912 dictionaries for (C a b) and (C a c), these dictionaries can provide a proof
1913 of (b ~ c), hence no extra evidence is necessary. Here is what will happen:
1915 Step 1: We will get new *given* superclass work,
1916 provisionally to our solving of w1 and w2
1918 g1: F a ~ b, g2 : F a ~ c,
1919 w1 : C a b, w2 : C a c, w3 : b ~ c
1921 The evidence for g1 and g2 is a superclass evidence term:
1923 g1 := sc w1, g2 := sc w2
1925 Step 2: The givens will solve the wanted w3, so that
1926 w3 := sym (sc w1) ; sc w2
1928 Step 3: Now, one may naively assume that then w2 can be solve from w1
1929 after rewriting with the (now solved equality) (b ~ c).
1931 But this rewriting is ruled out by the isGoodRectDict!
1933 Conclusion, we will (correctly) end up with the unsolved goals
1936 NB: The desugarer needs be more clever to deal with equalities
1937 that participate in recursive dictionary bindings.
1942 data LookupInstResult
1944 | GenInst [WantedEvVar] EvTerm
1946 matchClassInst :: Class -> [Type] -> WantedLoc -> TcS LookupInstResult
1947 matchClassInst clas tys loc
1948 = do { let pred = mkClassPred clas tys
1949 ; mb_result <- matchClass clas tys
1951 MatchInstNo -> return NoInstance
1952 MatchInstMany -> return NoInstance -- defer any reactions of a multitude until
1953 -- we learn more about the reagent
1954 MatchInstSingle (dfun_id, mb_inst_tys) ->
1955 do { checkWellStagedDFun pred dfun_id loc
1957 -- It's possible that not all the tyvars are in
1958 -- the substitution, tenv. For example:
1959 -- instance C X a => D X where ...
1960 -- (presumably there's a functional dependency in class C)
1961 -- Hence mb_inst_tys :: Either TyVar TcType
1963 ; tys <- instDFunTypes mb_inst_tys
1964 ; let (theta, _) = tcSplitPhiTy (applyTys (idType dfun_id) tys)
1965 ; if null theta then
1966 return (GenInst [] (EvDFunApp dfun_id tys []))
1968 { ev_vars <- instDFunConstraints theta
1969 ; let wevs = [WantedEvVar w loc | w <- ev_vars]
1970 ; return $ GenInst wevs (EvDFunApp dfun_id tys ev_vars) }