3 solveInteract, solveInteractGiven, solveInteractWanted,
4 AtomicInert, tyVarsOfInert,
5 InertSet, emptyInert, updInertSet, extractUnsolved, solveOne,
8 #include "HsVersions.h"
23 import Inst( tyVarsOfEvVar )
34 import TcMType ( isSilentEvVar )
38 import qualified Data.Map as Map
40 import Control.Monad( when )
42 import FastString ( sLit )
46 Note [InertSet invariants]
47 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
48 An InertSet is a bag of canonical constraints, with the following invariants:
50 1 No two constraints react with each other.
52 A tricky case is when there exists a given (solved) dictionary
53 constraint and a wanted identical constraint in the inert set, but do
54 not react because reaction would create loopy dictionary evidence for
55 the wanted. See note [Recursive dictionaries]
57 2 Given equalities form an idempotent substitution [none of the
58 given LHS's occur in any of the given RHS's or reactant parts]
60 3 Wanted equalities also form an idempotent substitution
62 4 The entire set of equalities is acyclic.
64 5 Wanted dictionaries are inert with the top-level axiom set
66 6 Equalities of the form tv1 ~ tv2 always have a touchable variable
67 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 8 No Given constraint mentions a touchable unification variable, but
74 Given/Solved may do so.
76 9 Given constraints will also have their superclasses in the inert set,
77 but Given/Solved will not.
79 Note that 6 and 7 are /not/ enforced by canonicalization but rather by
80 insertion in the inert list, ie by TcInteract.
82 During the process of solving, the inert set will contain some
83 previously given constraints, some wanted constraints, and some given
84 constraints which have arisen from solving wanted constraints. For
85 now we do not distinguish between given and solved constraints.
87 Note that we must switch wanted inert items to given when going under an
88 implication constraint (when in top-level inference mode).
92 data CCanMap a = CCanMap { cts_given :: Map.Map a CanonicalCts
93 -- Invariant: all Given
94 , cts_derived :: Map.Map a CanonicalCts
95 -- Invariant: all Derived
96 , cts_wanted :: Map.Map a CanonicalCts }
97 -- Invariant: all Wanted
99 cCanMapToBag :: Ord a => CCanMap a -> CanonicalCts
100 cCanMapToBag cmap = Map.fold unionBags rest_wder (cts_given cmap)
101 where rest_wder = Map.fold unionBags rest_der (cts_wanted cmap)
102 rest_der = Map.fold unionBags emptyCCan (cts_derived cmap)
104 emptyCCanMap :: CCanMap a
105 emptyCCanMap = CCanMap { cts_given = Map.empty
106 , cts_derived = Map.empty, cts_wanted = Map.empty }
108 updCCanMap:: Ord a => (a,CanonicalCt) -> CCanMap a -> CCanMap a
109 updCCanMap (a,ct) cmap
110 = case cc_flavor ct of
112 -> cmap { cts_wanted = Map.insertWith unionBags a this_ct (cts_wanted cmap) }
114 -> cmap { cts_given = Map.insertWith unionBags a this_ct (cts_given cmap) }
116 -> cmap { cts_derived = Map.insertWith unionBags a this_ct (cts_derived cmap) }
117 where this_ct = singleCCan ct
119 getRelevantCts :: Ord a => a -> CCanMap a -> (CanonicalCts, CCanMap a)
120 -- Gets the relevant constraints and returns the rest of the CCanMap
121 getRelevantCts a cmap
122 = let relevant = unionManyBags [ Map.findWithDefault emptyCCan a (cts_wanted cmap)
123 , Map.findWithDefault emptyCCan a (cts_given cmap)
124 , Map.findWithDefault emptyCCan a (cts_derived cmap) ]
125 residual_map = cmap { cts_wanted = Map.delete a (cts_wanted cmap)
126 , cts_given = Map.delete a (cts_given cmap)
127 , cts_derived = Map.delete a (cts_derived cmap) }
128 in (relevant, residual_map)
130 extractUnsolvedCMap :: Ord a => CCanMap a -> (CanonicalCts, CCanMap a)
131 -- Gets the wanted or derived constraints and returns a residual
132 -- CCanMap with only givens.
133 extractUnsolvedCMap cmap =
134 let wntd = Map.fold unionBags emptyCCan (cts_wanted cmap)
135 derd = Map.fold unionBags emptyCCan (cts_derived cmap)
136 in (wntd `unionBags` derd,
137 cmap { cts_wanted = Map.empty, cts_derived = Map.empty })
140 -- See Note [InertSet invariants]
142 = IS { inert_eqs :: CanonicalCts -- Equalities only (CTyEqCan)
143 , inert_dicts :: CCanMap Class -- Dictionaries only
144 , inert_ips :: CCanMap (IPName Name) -- Implicit parameters
145 , inert_frozen :: CanonicalCts
146 , inert_funeqs :: CCanMap TyCon -- Type family equalities only
147 -- This representation allows us to quickly get to the relevant
148 -- inert constraints when interacting a work item with the inert set.
151 tyVarsOfInert :: InertSet -> TcTyVarSet
152 tyVarsOfInert (IS { inert_eqs = eqs
153 , inert_dicts = dictmap
155 , inert_frozen = frozen
156 , inert_funeqs = funeqmap }) = tyVarsOfCanonicals cts
158 cts = eqs `andCCan` frozen `andCCan` cCanMapToBag dictmap
159 `andCCan` cCanMapToBag ipmap `andCCan` cCanMapToBag funeqmap
161 instance Outputable InertSet where
162 ppr is = vcat [ vcat (map ppr (Bag.bagToList $ inert_eqs is))
163 , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_dicts is)))
164 , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_ips is)))
165 , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_funeqs is)))
166 , vcat (map ppr (Bag.bagToList $ inert_frozen is))
169 emptyInert :: InertSet
170 emptyInert = IS { inert_eqs = Bag.emptyBag
171 , inert_frozen = Bag.emptyBag
172 , inert_dicts = emptyCCanMap
173 , inert_ips = emptyCCanMap
174 , inert_funeqs = emptyCCanMap }
176 updInertSet :: InertSet -> AtomicInert -> InertSet
178 | isCTyEqCan item -- Other equality
179 = let eqs' = inert_eqs is `Bag.snocBag` item
180 in is { inert_eqs = eqs' }
181 | Just cls <- isCDictCan_Maybe item -- Dictionary
182 = is { inert_dicts = updCCanMap (cls,item) (inert_dicts is) }
183 | Just x <- isCIPCan_Maybe item -- IP
184 = is { inert_ips = updCCanMap (x,item) (inert_ips is) }
185 | Just tc <- isCFunEqCan_Maybe item -- Function equality
186 = is { inert_funeqs = updCCanMap (tc,item) (inert_funeqs is) }
188 = is { inert_frozen = inert_frozen is `Bag.snocBag` item }
190 extractUnsolved :: InertSet -> (InertSet, CanonicalCts)
191 -- Postcondition: the returned canonical cts are either Derived, or Wanted.
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_frozen = emptyCCan
197 , inert_funeqs = solved_funeqs }
198 in (is_solved, unsolved)
200 where (unsolved_eqs, solved_eqs) = Bag.partitionBag (not.isGivenOrSolvedCt) eqs
201 (unsolved_ips, solved_ips) = extractUnsolvedCMap (inert_ips is)
202 (unsolved_dicts, solved_dicts) = extractUnsolvedCMap (inert_dicts is)
203 (unsolved_funeqs, solved_funeqs) = extractUnsolvedCMap (inert_funeqs is)
205 unsolved = unsolved_eqs `unionBags` inert_frozen is `unionBags`
206 unsolved_ips `unionBags` unsolved_dicts `unionBags` unsolved_funeqs
209 %*********************************************************************
211 * Main Interaction Solver *
213 **********************************************************************
217 1. Canonicalise (unary)
218 2. Pairwise interaction (binary)
219 * Take one from work list
220 * Try all pair-wise interactions with each constraint in inert
222 As an optimisation, we prioritize the equalities both in the
223 worklist and in the inerts.
225 3. Try to solve spontaneously for equalities involving touchables
226 4. Top-level interaction (binary wrt top-level)
227 Superclass decomposition belongs in (4), see note [Superclasses]
230 type AtomicInert = CanonicalCt -- constraint pulled from InertSet
231 type WorkItem = CanonicalCt -- constraint pulled from WorkList
233 ------------------------
235 = Stop -- Work item is consumed
236 | ContinueWith WorkItem -- Not consumed
238 instance Outputable StopOrContinue where
239 ppr Stop = ptext (sLit "Stop")
240 ppr (ContinueWith w) = ptext (sLit "ContinueWith") <+> ppr w
242 -- Results after interacting a WorkItem as far as possible with an InertSet
244 = SR { sr_inerts :: InertSet
245 -- The new InertSet to use (REPLACES the old InertSet)
246 , sr_new_work :: WorkList
247 -- Any new work items generated (should be ADDED to the old WorkList)
249 -- sr_stop = Just workitem => workitem is *not* in sr_inerts and
250 -- workitem is inert wrt to sr_inerts
251 , sr_stop :: StopOrContinue
254 instance Outputable StageResult where
255 ppr (SR { sr_inerts = inerts, sr_new_work = work, sr_stop = stop })
256 = ptext (sLit "SR") <+>
257 braces (sep [ ptext (sLit "inerts =") <+> ppr inerts <> comma
258 , ptext (sLit "new work =") <+> ppr work <> comma
259 , ptext (sLit "stop =") <+> ppr stop])
261 type SubGoalDepth = Int -- Starts at zero; used to limit infinite
262 -- recursion of sub-goals
263 type SimplifierStage = SubGoalDepth -> WorkItem -> InertSet -> TcS StageResult
265 -- Combine a sequence of simplifier 'stages' to create a pipeline
266 runSolverPipeline :: SubGoalDepth
267 -> [(String, SimplifierStage)]
268 -> InertSet -> WorkItem
269 -> TcS (InertSet, WorkList)
270 -- Precondition: non-empty list of stages
271 runSolverPipeline depth pipeline inerts workItem
272 = do { traceTcS "Start solver pipeline" $
273 vcat [ ptext (sLit "work item =") <+> ppr workItem
274 , ptext (sLit "inerts =") <+> ppr inerts]
276 ; let itr_in = SR { sr_inerts = inerts
277 , sr_new_work = emptyWorkList
278 , sr_stop = ContinueWith workItem }
279 ; itr_out <- run_pipeline pipeline itr_in
281 = case sr_stop itr_out of
282 Stop -> sr_inerts itr_out
283 ContinueWith item -> sr_inerts itr_out `updInertSet` item
284 ; return (new_inert, sr_new_work itr_out) }
286 run_pipeline :: [(String, SimplifierStage)]
287 -> StageResult -> TcS StageResult
288 run_pipeline [] itr = return itr
289 run_pipeline _ itr@(SR { sr_stop = Stop }) = return itr
291 run_pipeline ((name,stage):stages)
292 (SR { sr_new_work = accum_work
294 , sr_stop = ContinueWith work_item })
295 = do { itr <- stage depth work_item inerts
296 ; traceTcS ("Stage result (" ++ name ++ ")") (ppr itr)
297 ; let itr' = itr { sr_new_work = accum_work `unionWorkList` sr_new_work itr }
298 ; run_pipeline stages itr' }
302 Inert: {c ~ d, F a ~ t, b ~ Int, a ~ ty} (all given)
303 Reagent: a ~ [b] (given)
305 React with (c~d) ==> IR (ContinueWith (a~[b])) True []
306 React with (F a ~ t) ==> IR (ContinueWith (a~[b])) False [F [b] ~ t]
307 React with (b ~ Int) ==> IR (ContinueWith (a~[Int]) True []
310 Inert: {c ~w d, F a ~g t, b ~w Int, a ~w ty}
313 React with (c ~w d) ==> IR (ContinueWith (a~[b])) True []
314 React with (F a ~g t) ==> IR (ContinueWith (a~[b])) True [] (can't rewrite given with wanted!)
318 Inert: {a ~ Int, F Int ~ b} (given)
319 Reagent: F a ~ b (wanted)
321 React with (a ~ Int) ==> IR (ContinueWith (F Int ~ b)) True []
322 React with (F Int ~ b) ==> IR Stop True [] -- after substituting we re-canonicalize and get nothing
325 -- Main interaction solver: we fully solve the worklist 'in one go',
326 -- returning an extended inert set.
328 -- See Note [Touchables and givens].
329 solveInteractGiven :: InertSet -> GivenLoc -> [EvVar] -> TcS InertSet
330 solveInteractGiven inert gloc evs
331 = do { (_, inert_ret) <- solveInteract inert $ listToBag $
335 flav = Given gloc GivenOrig
336 mk_given ev = mkEvVarX ev flav
338 solveInteractWanted :: InertSet -> [WantedEvVar] -> TcS InertSet
339 solveInteractWanted inert wvs
340 = do { (_,inert_ret) <- solveInteract inert $ listToBag $
341 map wantedToFlavored wvs
344 solveInteract :: InertSet -> Bag FlavoredEvVar -> TcS (Bool, InertSet)
345 -- Post: (True, inert_set) means we managed to discharge all constraints
346 -- without actually doing any interactions!
347 -- (False, inert_set) means some interactions occurred
348 solveInteract inert ws
349 = do { dyn_flags <- getDynFlags
350 ; sctx <- getTcSContext
352 ; traceTcS "solveInteract, before clever canonicalization:" $
353 vcat [ text "ws = " <+> ppr (mapBag (\(EvVarX ev ct)
354 -> (ct,evVarPred ev)) ws)
355 , text "inert = " <+> ppr inert ]
357 ; can_ws <- mkCanonicalFEVs ws
360 <- foldrWorkListM (tryPreSolveAndInteract sctx dyn_flags) (True,inert) can_ws
362 ; traceTcS "solveInteract, after clever canonicalization (and interaction):" $
363 vcat [ text "No interaction happened = " <+> ppr flag
364 , text "inert_ret = " <+> ppr inert_ret ]
366 ; return (flag, inert_ret) }
368 tryPreSolveAndInteract :: SimplContext
372 -> TcS (Bool, InertSet)
373 -- Returns: True if it was able to discharge this constraint AND all previous ones
374 tryPreSolveAndInteract sctx dyn_flags ct (all_previous_discharged, inert)
375 = do { let inert_cts = get_inert_cts (evVarPred ev_var)
377 ; this_one_discharged <-
378 if isCFrozenErr ct then
381 dischargeFromCCans inert_cts ev_var fl
383 ; if this_one_discharged
384 then return (all_previous_discharged, inert)
387 { inert_ret <- solveOneWithDepth (ctxtStkDepth dyn_flags,0,[]) ct inert
388 ; return (False, inert_ret) } }
394 get_inert_cts (ClassP clas _)
395 | simplEqsOnly sctx = emptyCCan
396 | otherwise = fst (getRelevantCts clas (inert_dicts inert))
397 get_inert_cts (IParam {})
398 = emptyCCan -- We must not do the same thing for IParams, because (contrary
399 -- to dictionaries), work items /must/ override inert items.
400 -- See Note [Overriding implicit parameters] in TcInteract.
401 get_inert_cts (EqPred {})
402 = inert_eqs inert `unionBags` cCanMapToBag (inert_funeqs inert)
404 dischargeFromCCans :: CanonicalCts -> EvVar -> CtFlavor -> TcS Bool
405 -- See if this (pre-canonicalised) work-item is identical to a
406 -- one already in the inert set. Reasons:
407 -- a) Avoid creating superclass constraints for millions of incoming (Num a) constraints
408 -- b) Termination for improve_eqs in TcSimplify.simpl_loop
409 dischargeFromCCans cans ev fl
410 = Bag.foldrBag discharge_ct (return False) cans
412 the_pred = evVarPred ev
414 discharge_ct :: CanonicalCt -> TcS Bool -> TcS Bool
415 discharge_ct ct _rest
416 | evVarPred (cc_id ct) `eqPred` the_pred
417 , cc_flavor ct `canSolve` fl
418 = do { when (isWanted fl) $ setEvBind ev (evVarTerm (cc_id ct))
419 -- Deriveds need no evidence
420 -- For Givens, we already have evidence, and we don't need it twice
423 discharge_ct _ct rest = rest
426 Note [Avoiding the superclass explosion]
427 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
428 This note now is not as significant as it used to be because we no
429 longer add the superclasses of Wanted as Derived, except only if they
430 have equality superclasses or superclasses with functional
431 dependencies. The fear was that hundreds of identical wanteds would
432 give rise each to the same superclass or equality Derived's which
433 would lead to a blo-up in the number of interactions.
435 Instead, what we do with tryPreSolveAndCanon, is when we encounter a
436 new constraint, we very quickly see if it can be immediately
437 discharged by a class constraint in our inert set or the previous
438 canonicals. If so, we add nothing to the returned canonical
442 solveOne :: WorkItem -> InertSet -> TcS InertSet
443 solveOne workItem inerts
444 = do { dyn_flags <- getDynFlags
445 ; solveOneWithDepth (ctxtStkDepth dyn_flags,0,[]) workItem inerts
449 solveInteractWithDepth :: (Int, Int, [WorkItem])
450 -> WorkList -> InertSet -> TcS InertSet
451 solveInteractWithDepth ctxt@(max_depth,n,stack) ws inert
456 = solverDepthErrorTcS n stack
459 = do { traceTcS "solveInteractWithDepth" $
460 vcat [ text "Current depth =" <+> ppr n
461 , text "Max depth =" <+> ppr max_depth
462 , text "ws =" <+> ppr ws ]
465 ; foldrWorkListM (solveOneWithDepth ctxt) inert ws }
466 -- use foldr to preserve the order
469 -- Fully interact the given work item with an inert set, and return a
470 -- new inert set which has assimilated the new information.
471 solveOneWithDepth :: (Int, Int, [WorkItem])
472 -> WorkItem -> InertSet -> TcS InertSet
473 solveOneWithDepth (max_depth, depth, stack) work inert
474 = do { traceFireTcS depth (text "Solving {" <+> ppr work)
475 ; (new_inert, new_work) <- runSolverPipeline depth thePipeline inert work
477 -- Recursively solve the new work generated
478 -- from workItem, with a greater depth
479 ; res_inert <- solveInteractWithDepth (max_depth, depth+1, work:stack) new_work new_inert
481 ; traceFireTcS depth (text "Done }" <+> ppr work)
485 thePipeline :: [(String,SimplifierStage)]
486 thePipeline = [ ("interact with inert eqs", interactWithInertEqsStage)
487 , ("interact with inerts", interactWithInertsStage)
488 , ("spontaneous solve", spontaneousSolveStage)
489 , ("top-level reactions", topReactionsStage) ]
492 *********************************************************************************
494 The spontaneous-solve Stage
496 *********************************************************************************
498 Note [Efficient Orientation]
499 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
501 There are two cases where we have to be careful about
502 orienting equalities to get better efficiency.
504 Case 1: In Rewriting Equalities (function rewriteEqLHS)
506 When rewriting two equalities with the same LHS:
509 We have a choice of producing work (xi1 ~ xi2) (up-to the
510 canonicalization invariants) However, to prevent the inert items
511 from getting kicked out of the inerts first, we prefer to
512 canonicalize (xi1 ~ xi2) if (b) comes from the inert set, or (xi2
513 ~ xi1) if (a) comes from the inert set.
515 This choice is implemented using the WhichComesFromInert flag.
517 Case 2: Functional Dependencies
518 Again, we should prefer, if possible, the inert variables on the RHS
520 Case 3: IP improvement work
521 We must always rewrite so that the inert type is on the right.
524 spontaneousSolveStage :: SimplifierStage
525 spontaneousSolveStage depth workItem inerts
526 = do { mSolve <- trySpontaneousSolve workItem
529 SPCantSolve -> -- No spontaneous solution for him, keep going
530 return $ SR { sr_new_work = emptyWorkList
532 , sr_stop = ContinueWith workItem }
535 | not (isGivenOrSolvedCt workItem)
536 -- Original was wanted or derived but we have now made him
537 -- given so we have to interact him with the inerts due to
538 -- its status change. This in turn may produce more work.
539 -- We do this *right now* (rather than just putting workItem'
540 -- back into the work-list) because we've solved
541 -> do { bumpStepCountTcS
542 ; traceFireTcS depth (ptext (sLit "Spontaneous (w/d)") <+> ppr workItem)
543 ; (new_inert, new_work) <- runSolverPipeline depth
544 [ ("recursive interact with inert eqs", interactWithInertEqsStage)
545 , ("recursive interact with inerts", interactWithInertsStage)
547 ; return $ SR { sr_new_work = new_work
548 , sr_inerts = new_inert -- will include workItem'
552 -> -- Original was given; he must then be inert all right, and
553 -- workList' are all givens from flattening
554 do { bumpStepCountTcS
555 ; traceFireTcS depth (ptext (sLit "Spontaneous (g)") <+> ppr workItem)
556 ; return $ SR { sr_new_work = emptyWorkList
557 , sr_inerts = inerts `updInertSet` workItem'
559 SPError -> -- Return with no new work
560 return $ SR { sr_new_work = emptyWorkList
565 data SPSolveResult = SPCantSolve | SPSolved WorkItem | SPError
566 -- SPCantSolve means that we can't do the unification because e.g. the variable is untouchable
567 -- SPSolved workItem' gives us a new *given* to go on
568 -- SPError means that it's completely impossible to solve this equality, eg due to a kind error
571 -- @trySpontaneousSolve wi@ solves equalities where one side is a
572 -- touchable unification variable.
573 -- See Note [Touchables and givens]
574 trySpontaneousSolve :: WorkItem -> TcS SPSolveResult
575 trySpontaneousSolve workItem@(CTyEqCan { cc_id = cv, cc_flavor = gw, cc_tyvar = tv1, cc_rhs = xi })
578 | Just tv2 <- tcGetTyVar_maybe xi
579 = do { tch1 <- isTouchableMetaTyVar tv1
580 ; tch2 <- isTouchableMetaTyVar tv2
581 ; case (tch1, tch2) of
582 (True, True) -> trySpontaneousEqTwoWay cv gw tv1 tv2
583 (True, False) -> trySpontaneousEqOneWay cv gw tv1 xi
584 (False, True) -> trySpontaneousEqOneWay cv gw tv2 (mkTyVarTy tv1)
585 _ -> return SPCantSolve }
587 = do { tch1 <- isTouchableMetaTyVar tv1
588 ; if tch1 then trySpontaneousEqOneWay cv gw tv1 xi
589 else do { traceTcS "Untouchable LHS, can't spontaneously solve workitem:"
591 ; return SPCantSolve }
595 -- trySpontaneousSolve (CFunEqCan ...) = ...
596 -- See Note [No touchables as FunEq RHS] in TcSMonad
597 trySpontaneousSolve _ = return SPCantSolve
600 trySpontaneousEqOneWay :: CoVar -> CtFlavor -> TcTyVar -> Xi -> TcS SPSolveResult
601 -- tv is a MetaTyVar, not untouchable
602 trySpontaneousEqOneWay cv gw tv xi
603 | not (isSigTyVar tv) || isTyVarTy xi
604 = do { let kxi = typeKind xi -- NB: 'xi' is fully rewritten according to the inerts
605 -- so we have its more specific kind in our hands
606 ; if kxi `isSubKind` tyVarKind tv then
607 solveWithIdentity cv gw tv xi
608 else return SPCantSolve
610 else if tyVarKind tv `isSubKind` kxi then
611 return SPCantSolve -- kinds are compatible but we can't solveWithIdentity this way
612 -- This case covers the a_touchable :: * ~ b_untouchable :: ??
613 -- which has to be deferred or floated out for someone else to solve
614 -- it in a scope where 'b' is no longer untouchable.
615 else do { addErrorTcS KindError gw (mkTyVarTy tv) xi -- See Note [Kind errors]
619 | otherwise -- Still can't solve, sig tyvar and non-variable rhs
623 trySpontaneousEqTwoWay :: CoVar -> CtFlavor -> TcTyVar -> TcTyVar -> TcS SPSolveResult
624 -- Both tyvars are *touchable* MetaTyvars so there is only a chance for kind error here
625 trySpontaneousEqTwoWay cv gw tv1 tv2
627 , nicer_to_update_tv2 = solveWithIdentity cv gw tv2 (mkTyVarTy tv1)
629 = solveWithIdentity cv gw tv1 (mkTyVarTy tv2)
630 | otherwise -- None is a subkind of the other, but they are both touchable!
632 -- do { addErrorTcS KindError gw (mkTyVarTy tv1) (mkTyVarTy tv2)
633 -- ; return SPError }
637 nicer_to_update_tv2 = isSigTyVar tv1 || isSystemName (Var.varName tv2)
641 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
642 Consider the wanted problem:
643 alpha ~ (# Int, Int #)
644 where alpha :: ?? and (# Int, Int #) :: (#). We can't spontaneously solve this constraint,
645 but we should rather reject the program that give rise to it. If 'trySpontaneousEqTwoWay'
646 simply returns @CantSolve@ then that wanted constraint is going to propagate all the way and
647 get quantified over in inference mode. That's bad because we do know at this point that the
648 constraint is insoluble. Instead, we call 'recKindErrorTcS' here, which will fail later on.
650 The same applies in canonicalization code in case of kind errors in the givens.
652 However, when we canonicalize givens we only check for compatibility (@compatKind@).
653 If there were a kind error in the givens, this means some form of inconsistency or dead code.
655 You may think that when we spontaneously solve wanteds we may have to look through the
656 bindings to determine the right kind of the RHS type. E.g one may be worried that xi is
657 @alpha@ where alpha :: ? and a previous spontaneous solving has set (alpha := f) with (f :: *).
658 But we orient our constraints so that spontaneously solved ones can rewrite all other constraint
659 so this situation can't happen.
661 Note [Spontaneous solving and kind compatibility]
662 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
663 Note that our canonical constraints insist that *all* equalities (tv ~
664 xi) or (F xis ~ rhs) require the LHS and the RHS to have *compatible*
665 the same kinds. ("compatible" means one is a subKind of the other.)
667 - It can't be *equal* kinds, because
668 b) wanted constraints don't necessarily have identical kinds
670 b) a solved wanted constraint becomes a given
672 - SPJ thinks that *given* constraints (tv ~ tau) always have that
673 tau has a sub-kind of tv; and when solving wanted constraints
674 in trySpontaneousEqTwoWay we re-orient to achieve this.
676 - Note that the kind invariant is maintained by rewriting.
677 Eg wanted1 rewrites wanted2; if both were compatible kinds before,
678 wanted2 will be afterwards. Similarly givens.
681 - Givens from higher-rank, such as:
682 type family T b :: * -> * -> *
683 type instance T Bool = (->)
685 f :: forall a. ((T a ~ (->)) => ...) -> a -> ...
687 Whereas we would be able to apply the type instance, we would not be able to
688 use the given (T Bool ~ (->)) in the body of 'flop'
691 Note [Avoid double unifications]
692 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
693 The spontaneous solver has to return a given which mentions the unified unification
694 variable *on the left* of the equality. Here is what happens if not:
695 Original wanted: (a ~ alpha), (alpha ~ Int)
696 We spontaneously solve the first wanted, without changing the order!
697 given : a ~ alpha [having unified alpha := a]
698 Now the second wanted comes along, but he cannot rewrite the given, so we simply continue.
699 At the end we spontaneously solve that guy, *reunifying* [alpha := Int]
701 We avoid this problem by orienting the resulting given so that the unification
702 variable is on the left. [Note that alternatively we could attempt to
703 enforce this at canonicalization]
705 See also Note [No touchables as FunEq RHS] in TcSMonad; avoiding
706 double unifications is the main reason we disallow touchable
707 unification variables as RHS of type family equations: F xis ~ alpha.
712 solveWithIdentity :: CoVar -> CtFlavor -> TcTyVar -> Xi -> TcS SPSolveResult
713 -- Solve with the identity coercion
714 -- Precondition: kind(xi) is a sub-kind of kind(tv)
715 -- Precondition: CtFlavor is Wanted or Derived
716 -- See [New Wanted Superclass Work] to see why solveWithIdentity
717 -- must work for Derived as well as Wanted
718 -- Returns: workItem where
719 -- workItem = the new Given constraint
720 solveWithIdentity cv wd tv xi
721 = do { traceTcS "Sneaky unification:" $
722 vcat [text "Coercion variable: " <+> ppr wd,
723 text "Coercion: " <+> pprEq (mkTyVarTy tv) xi,
724 text "Left Kind is : " <+> ppr (typeKind (mkTyVarTy tv)),
725 text "Right Kind is : " <+> ppr (typeKind xi)
728 ; setWantedTyBind tv xi
729 ; let refl_xi = mkReflCo xi
730 ; cv_given <- newGivenCoVar (mkTyVarTy tv) xi refl_xi
732 ; when (isWanted wd) (setCoBind cv refl_xi)
733 -- We don't want to do this for Derived, that's why we use 'when (isWanted wd)'
734 ; return $ SPSolved (CTyEqCan { cc_id = cv_given
735 , cc_flavor = mkSolvedFlavor wd UnkSkol
736 , cc_tyvar = tv, cc_rhs = xi }) }
740 *********************************************************************************
742 The interact-with-inert Stage
744 *********************************************************************************
746 Note [The Solver Invariant]
747 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
748 We always add Givens first. So you might think that the solver has
751 If the work-item is Given,
752 then the inert item must Given
754 But this isn't quite true. Suppose we have,
755 c1: [W] beta ~ [alpha], c2 : [W] blah, c3 :[W] alpha ~ Int
756 After processing the first two, we get
757 c1: [G] beta ~ [alpha], c2 : [W] blah
758 Now, c3 does not interact with the the given c1, so when we spontaneously
759 solve c3, we must re-react it with the inert set. So we can attempt a
760 reaction between inert c2 [W] and work-item c3 [G].
762 It *is* true that [Solver Invariant]
763 If the work-item is Given,
764 AND there is a reaction
765 then the inert item must Given
767 If the work-item is Given,
768 and the inert item is Wanted/Derived
769 then there is no reaction
772 -- Interaction result of WorkItem <~> AtomicInert
774 = IR { ir_stop :: StopOrContinue
776 -- => Reagent (work item) consumed.
777 -- ContinueWith new_reagent
778 -- => Reagent transformed but keep gathering interactions.
779 -- The transformed item remains inert with respect
780 -- to any previously encountered inerts.
782 , ir_inert_action :: InertAction
783 -- Whether the inert item should remain in the InertSet.
785 , ir_new_work :: WorkList
786 -- new work items to add to the WorkList
788 , ir_fire :: Maybe String -- Tells whether a rule fired, and if so what
791 -- What to do with the inert reactant.
792 data InertAction = KeepInert | DropInert
794 mkIRContinue :: String -> WorkItem -> InertAction -> WorkList -> TcS InteractResult
795 mkIRContinue rule wi keep newWork
796 = return $ IR { ir_stop = ContinueWith wi, ir_inert_action = keep
797 , ir_new_work = newWork, ir_fire = Just rule }
799 mkIRStopK :: String -> WorkList -> TcS InteractResult
800 mkIRStopK rule newWork
801 = return $ IR { ir_stop = Stop, ir_inert_action = KeepInert
802 , ir_new_work = newWork, ir_fire = Just rule }
804 mkIRStopD :: String -> WorkList -> TcS InteractResult
805 mkIRStopD rule newWork
806 = return $ IR { ir_stop = Stop, ir_inert_action = DropInert
807 , ir_new_work = newWork, ir_fire = Just rule }
809 noInteraction :: Monad m => WorkItem -> m InteractResult
811 = return $ IR { ir_stop = ContinueWith wi, ir_inert_action = KeepInert
812 , ir_new_work = emptyWorkList, ir_fire = Nothing }
814 data WhichComesFromInert = LeftComesFromInert | RightComesFromInert
815 -- See Note [Efficient Orientation]
818 ---------------------------------------------------
819 -- Interact a single WorkItem with the equalities of an inert set as
820 -- far as possible, i.e. until we get a Stop result from an individual
821 -- reaction (i.e. when the WorkItem is consumed), or until we've
822 -- interact the WorkItem with the entire equalities of the InertSet
824 interactWithInertEqsStage :: SimplifierStage
825 interactWithInertEqsStage depth workItem inert
826 = Bag.foldrBagM (interactNext depth) initITR (inert_eqs inert)
827 -- use foldr to preserve the order
829 initITR = SR { sr_inerts = inert { inert_eqs = emptyCCan }
830 , sr_new_work = emptyWorkList
831 , sr_stop = ContinueWith workItem }
833 ---------------------------------------------------
834 -- Interact a single WorkItem with *non-equality* constraints in the inert set.
835 -- Precondition: equality interactions must have already happened, hence we have
836 -- to pick up some information from the incoming inert, before folding over the
837 -- "Other" constraints it contains!
839 interactWithInertsStage :: SimplifierStage
840 interactWithInertsStage depth workItem inert
841 = let (relevant, inert_residual) = getISRelevant workItem inert
842 initITR = SR { sr_inerts = inert_residual
843 , sr_new_work = emptyWorkList
844 , sr_stop = ContinueWith workItem }
845 in Bag.foldrBagM (interactNext depth) initITR relevant
846 -- use foldr to preserve the order
848 getISRelevant :: CanonicalCt -> InertSet -> (CanonicalCts, InertSet)
849 getISRelevant (CFrozenErr {}) is = (emptyCCan, is)
850 -- Nothing s relevant; we have alread interacted
851 -- it with the equalities in the inert set
853 getISRelevant (CDictCan { cc_class = cls } ) is
854 = let (relevant, residual_map) = getRelevantCts cls (inert_dicts is)
855 in (relevant, is { inert_dicts = residual_map })
856 getISRelevant (CFunEqCan { cc_fun = tc } ) is
857 = let (relevant, residual_map) = getRelevantCts tc (inert_funeqs is)
858 in (relevant, is { inert_funeqs = residual_map })
859 getISRelevant (CIPCan { cc_ip_nm = nm }) is
860 = let (relevant, residual_map) = getRelevantCts nm (inert_ips is)
861 in (relevant, is { inert_ips = residual_map })
862 -- An equality, finally, may kick everything except equalities out
863 -- because we have already interacted the equalities in interactWithInertEqsStage
864 getISRelevant _eq_ct is -- Equality, everything is relevant for this one
865 -- TODO: if we were caching variables, we'd know that only
866 -- some are relevant. Experiment with this for now.
867 = let cts = cCanMapToBag (inert_ips is) `unionBags`
868 cCanMapToBag (inert_dicts is) `unionBags` cCanMapToBag (inert_funeqs is)
869 in (cts, is { inert_dicts = emptyCCanMap
870 , inert_ips = emptyCCanMap
871 , inert_funeqs = emptyCCanMap })
873 interactNext :: SubGoalDepth -> AtomicInert -> StageResult -> TcS StageResult
874 interactNext depth inert it
875 | ContinueWith work_item <- sr_stop it
876 = do { let inerts = sr_inerts it
878 ; IR { ir_new_work = new_work, ir_inert_action = inert_action
879 , ir_fire = fire_info, ir_stop = stop }
880 <- interactWithInert inert work_item
883 = text rule <+> keep_doc
884 <+> vcat [ ptext (sLit "Inert =") <+> ppr inert
885 , ptext (sLit "Work =") <+> ppr work_item
886 , ppUnless (isEmptyWorkList new_work) $
887 ptext (sLit "New =") <+> ppr new_work ]
888 keep_doc = case inert_action of
889 KeepInert -> ptext (sLit "[keep]")
890 DropInert -> ptext (sLit "[drop]")
892 Just rule -> do { bumpStepCountTcS
893 ; traceFireTcS depth (mk_msg rule) }
896 -- New inerts depend on whether we KeepInert or not
897 ; let inerts_new = case inert_action of
898 KeepInert -> inerts `updInertSet` inert
901 ; return $ SR { sr_inerts = inerts_new
902 , sr_new_work = sr_new_work it `unionWorkList` new_work
905 = return $ it { sr_inerts = (sr_inerts it) `updInertSet` inert }
907 -- Do a single interaction of two constraints.
908 interactWithInert :: AtomicInert -> WorkItem -> TcS InteractResult
909 interactWithInert inert workItem
910 = do { ctxt <- getTcSContext
911 ; let is_allowed = allowedInteraction (simplEqsOnly ctxt) inert workItem
914 doInteractWithInert inert workItem
916 noInteraction workItem
919 allowedInteraction :: Bool -> AtomicInert -> WorkItem -> Bool
920 -- Allowed interactions
921 allowedInteraction eqs_only (CDictCan {}) (CDictCan {}) = not eqs_only
922 allowedInteraction eqs_only (CIPCan {}) (CIPCan {}) = not eqs_only
923 allowedInteraction _ _ _ = True
925 --------------------------------------------
926 doInteractWithInert :: CanonicalCt -> CanonicalCt -> TcS InteractResult
927 -- Identical class constraints.
930 inertItem@(CDictCan { cc_id = d1, cc_flavor = fl1, cc_class = cls1, cc_tyargs = tys1 })
931 workItem@(CDictCan { cc_id = d2, cc_flavor = fl2, cc_class = cls2, cc_tyargs = tys2 })
932 | cls1 == cls2 && eqTypes tys1 tys2
933 = solveOneFromTheOther "Cls/Cls" (EvId d1,fl1) workItem
935 | cls1 == cls2 && (not (isGivenOrSolved fl1 && isGivenOrSolved fl2))
936 = -- See Note [When improvement happens]
937 do { let pty1 = ClassP cls1 tys1
938 pty2 = ClassP cls2 tys2
939 inert_pred_loc = (pty1, pprFlavorArising fl1)
940 work_item_pred_loc = (pty2, pprFlavorArising fl2)
941 fd_eqns = improveFromAnother
942 inert_pred_loc -- the template
943 work_item_pred_loc -- the one we aim to rewrite
944 -- See Note [Efficient Orientation]
946 ; m <- rewriteWithFunDeps fd_eqns tys2 fl2
948 Nothing -> noInteraction workItem
949 Just (rewritten_tys2, cos2, fd_work)
950 | eqTypes tys1 rewritten_tys2
951 -> -- Solve him on the spot in this case
953 Given {} -> pprPanic "Unexpected given" (ppr inertItem $$ ppr workItem)
954 Derived {} -> mkIRStopK "Cls/Cls fundep (solved)" fd_work
957 -> do { setDictBind d2 (EvCast d1 dict_co)
958 ; let inert_w = inertItem { cc_flavor = fl2 }
959 -- A bit naughty: we take the inert Derived,
960 -- turn it into a Wanted, use it to solve the work-item
961 -- and put it back into the work-list
962 -- Maybe rather than starting again, we could *replace* the
963 -- inert item, but its safe and simple to restart
964 ; mkIRStopD "Cls/Cls fundep (solved)" $
965 workListFromNonEq inert_w `unionWorkList` fd_work }
967 -> do { setDictBind d2 (EvCast d1 dict_co)
968 ; mkIRStopK "Cls/Cls fundep (solved)" fd_work }
971 -> -- We could not quite solve him, but we still rewrite him
972 -- Example: class C a b c | a -> b
973 -- Given: C Int Bool x, Wanted: C Int beta y
974 -- Then rewrite the wanted to C Int Bool y
975 -- but note that is still not identical to the given
976 -- The important thing is that the rewritten constraint is
977 -- inert wrt the given.
978 -- However it is not necessarily inert wrt previous inert-set items.
979 -- class C a b c d | a -> b, b c -> d
980 -- Inert: c1: C b Q R S, c2: C P Q a b
981 -- Work: C P alpha R beta
982 -- Does not react with c1; reacts with c2, with alpha:=Q
983 -- NOW it reacts with c1!
984 -- So we must stop, and put the rewritten constraint back in the work list
985 do { d2' <- newDictVar cls1 rewritten_tys2
987 Given {} -> pprPanic "Unexpected given" (ppr inertItem $$ ppr workItem)
988 Wanted {} -> setDictBind d2 (EvCast d2' dict_co)
989 Derived {} -> return ()
990 ; let workItem' = workItem { cc_id = d2', cc_tyargs = rewritten_tys2 }
991 ; mkIRStopK "Cls/Cls fundep (partial)" $
992 workListFromNonEq workItem' `unionWorkList` fd_work }
995 dict_co = mkTyConAppCo (classTyCon cls1) cos2
998 -- Class constraint and given equality: use the equality to rewrite
999 -- the class constraint.
1000 doInteractWithInert (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi })
1001 (CDictCan { cc_id = dv, cc_flavor = wfl, cc_class = cl, cc_tyargs = xis })
1002 | ifl `canRewrite` wfl
1003 , tv `elemVarSet` tyVarsOfTypes xis
1004 = do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,wfl,cl,xis)
1005 -- Continue with rewritten Dictionary because we can only be in the
1006 -- interactWithEqsStage, so the dictionary is inert.
1007 ; mkIRContinue "Eq/Cls" rewritten_dict KeepInert emptyWorkList }
1009 doInteractWithInert (CDictCan { cc_id = dv, cc_flavor = ifl, cc_class = cl, cc_tyargs = xis })
1010 workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
1011 | wfl `canRewrite` ifl
1012 , tv `elemVarSet` tyVarsOfTypes xis
1013 = do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,ifl,cl,xis)
1014 ; mkIRContinue "Cls/Eq" workItem DropInert (workListFromNonEq rewritten_dict) }
1016 -- Class constraint and given equality: use the equality to rewrite
1017 -- the class constraint.
1018 doInteractWithInert (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi })
1019 (CIPCan { cc_id = ipid, cc_flavor = wfl, cc_ip_nm = nm, cc_ip_ty = ty })
1020 | ifl `canRewrite` wfl
1021 , tv `elemVarSet` tyVarsOfType ty
1022 = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,wfl,nm,ty)
1023 ; mkIRContinue "Eq/IP" rewritten_ip KeepInert emptyWorkList }
1025 doInteractWithInert (CIPCan { cc_id = ipid, cc_flavor = ifl, cc_ip_nm = nm, cc_ip_ty = ty })
1026 workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
1027 | wfl `canRewrite` ifl
1028 , tv `elemVarSet` tyVarsOfType ty
1029 = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,ifl,nm,ty)
1030 ; mkIRContinue "IP/Eq" workItem DropInert (workListFromNonEq rewritten_ip) }
1032 -- Two implicit parameter constraints. If the names are the same,
1033 -- but their types are not, we generate a wanted type equality
1034 -- that equates the type (this is "improvement").
1035 -- However, we don't actually need the coercion evidence,
1036 -- so we just generate a fresh coercion variable that isn't used anywhere.
1037 doInteractWithInert (CIPCan { cc_id = id1, cc_flavor = ifl, cc_ip_nm = nm1, cc_ip_ty = ty1 })
1038 workItem@(CIPCan { cc_flavor = wfl, cc_ip_nm = nm2, cc_ip_ty = ty2 })
1039 | nm1 == nm2 && isGivenOrSolved wfl && isGivenOrSolved ifl
1040 = -- See Note [Overriding implicit parameters]
1041 -- Dump the inert item, override totally with the new one
1042 -- Do not require type equality
1043 -- For example, given let ?x::Int = 3 in let ?x::Bool = True in ...
1044 -- we must *override* the outer one with the inner one
1045 mkIRContinue "IP/IP override" workItem DropInert emptyWorkList
1047 | nm1 == nm2 && ty1 `eqType` ty2
1048 = solveOneFromTheOther "IP/IP" (EvId id1,ifl) workItem
1051 = -- See Note [When improvement happens]
1052 do { co_var <- newCoVar ty2 ty1 -- See Note [Efficient Orientation]
1053 ; let flav = Wanted (combineCtLoc ifl wfl)
1054 ; cans <- mkCanonical flav co_var
1056 Given {} -> pprPanic "Unexpected given IP" (ppr workItem)
1057 Derived {} -> pprPanic "Unexpected derived IP" (ppr workItem)
1059 do { setIPBind (cc_id workItem) $
1060 EvCast id1 (mkSymCo (mkCoVarCo co_var))
1061 ; mkIRStopK "IP/IP interaction (solved)" cans }
1064 -- Never rewrite a given with a wanted equality, and a type function
1065 -- equality can never rewrite an equality. We rewrite LHS *and* RHS
1066 -- of function equalities so that our inert set exposes everything that
1067 -- we know about equalities.
1069 -- Inert: equality, work item: function equality
1070 doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi1 })
1071 (CFunEqCan { cc_id = cv2, cc_flavor = wfl, cc_fun = tc
1072 , cc_tyargs = args, cc_rhs = xi2 })
1073 | ifl `canRewrite` wfl
1074 , tv `elemVarSet` tyVarsOfTypes (xi2:args) -- Rewrite RHS as well
1075 = do { rewritten_funeq <- rewriteFunEq (cv1,tv,xi1) (cv2,wfl,tc,args,xi2)
1076 ; mkIRStopK "Eq/FunEq" (workListFromEq rewritten_funeq) }
1077 -- Must Stop here, because we may no longer be inert after the rewritting.
1079 -- Inert: function equality, work item: equality
1080 doInteractWithInert (CFunEqCan {cc_id = cv1, cc_flavor = ifl, cc_fun = tc
1081 , cc_tyargs = args, cc_rhs = xi1 })
1082 workItem@(CTyEqCan { cc_id = cv2, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi2 })
1083 | wfl `canRewrite` ifl
1084 , tv `elemVarSet` tyVarsOfTypes (xi1:args) -- Rewrite RHS as well
1085 = do { rewritten_funeq <- rewriteFunEq (cv2,tv,xi2) (cv1,ifl,tc,args,xi1)
1086 ; mkIRContinue "FunEq/Eq" workItem DropInert (workListFromEq rewritten_funeq) }
1087 -- One may think that we could (KeepTransformedInert rewritten_funeq)
1088 -- but that is wrong, because it may end up not being inert with respect
1089 -- to future inerts. Example:
1090 -- Original inert = { F xis ~ [a], b ~ Maybe Int }
1091 -- Work item comes along = a ~ [b]
1092 -- If we keep { F xis ~ [b] } in the inert set we will end up with:
1093 -- { F xis ~ [b], b ~ Maybe Int, a ~ [Maybe Int] }
1094 -- At the end, which is *not* inert. So we should unfortunately DropInert here.
1096 doInteractWithInert (CFunEqCan { cc_id = cv1, cc_flavor = fl1, cc_fun = tc1
1097 , cc_tyargs = args1, cc_rhs = xi1 })
1098 workItem@(CFunEqCan { cc_id = cv2, cc_flavor = fl2, cc_fun = tc2
1099 , cc_tyargs = args2, cc_rhs = xi2 })
1100 | tc1 == tc2 && and (zipWith eqType args1 args2)
1101 , Just GivenSolved <- isGiven_maybe fl1
1102 = mkIRContinue "Funeq/Funeq" workItem DropInert emptyWorkList
1103 | tc1 == tc2 && and (zipWith eqType args1 args2)
1104 , Just GivenSolved <- isGiven_maybe fl2
1105 = mkIRStopK "Funeq/Funeq" emptyWorkList
1107 | fl1 `canSolve` fl2 && lhss_match
1108 = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCo cv1,xi1) (cv2,fl2,xi2)
1109 ; mkIRStopK "FunEq/FunEq" cans }
1110 | fl2 `canSolve` fl1 && lhss_match
1111 = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCo cv2,xi2) (cv1,fl1,xi1)
1112 ; mkIRContinue "FunEq/FunEq" workItem DropInert cans }
1114 lhss_match = tc1 == tc2 && eqTypes args1 args2
1116 doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
1117 workItem@(CTyEqCan { cc_id = cv2, cc_flavor = fl2, cc_tyvar = tv2, cc_rhs = xi2 })
1118 -- Check for matching LHS
1119 | fl1 `canSolve` fl2 && tv1 == tv2
1120 = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCo cv1,xi1) (cv2,fl2,xi2)
1121 ; mkIRStopK "Eq/Eq lhs" cans }
1123 | fl2 `canSolve` fl1 && tv1 == tv2
1124 = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCo cv2,xi2) (cv1,fl1,xi1)
1125 ; mkIRContinue "Eq/Eq lhs" workItem DropInert cans }
1127 -- Check for rewriting RHS
1128 | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfType xi2
1129 = do { rewritten_eq <- rewriteEqRHS (cv1,tv1,xi1) (cv2,fl2,tv2,xi2)
1130 ; mkIRStopK "Eq/Eq rhs" rewritten_eq }
1132 | fl2 `canRewrite` fl1 && tv2 `elemVarSet` tyVarsOfType xi1
1133 = do { rewritten_eq <- rewriteEqRHS (cv2,tv2,xi2) (cv1,fl1,tv1,xi1)
1134 ; mkIRContinue "Eq/Eq rhs" workItem DropInert rewritten_eq }
1136 doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
1137 (CFrozenErr { cc_id = cv2, cc_flavor = fl2 })
1138 | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfEvVar cv2
1139 = do { rewritten_frozen <- rewriteFrozen (cv1, tv1, xi1) (cv2, fl2)
1140 ; mkIRStopK "Frozen/Eq" rewritten_frozen }
1142 doInteractWithInert (CFrozenErr { cc_id = cv2, cc_flavor = fl2 })
1143 workItem@(CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
1144 | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfEvVar cv2
1145 = do { rewritten_frozen <- rewriteFrozen (cv1, tv1, xi1) (cv2, fl2)
1146 ; mkIRContinue "Frozen/Eq" workItem DropInert rewritten_frozen }
1148 -- Fall-through case for all other situations
1149 doInteractWithInert _ workItem = noInteraction workItem
1151 -------------------------
1152 -- Equational Rewriting
1153 rewriteDict :: (CoVar, TcTyVar, Xi) -> (DictId, CtFlavor, Class, [Xi]) -> TcS CanonicalCt
1154 rewriteDict (cv,tv,xi) (dv,gw,cl,xis)
1155 = do { let cos = map (liftCoSubstWith [tv] [mkCoVarCo cv]) xis -- xis[tv] ~ xis[xi]
1156 args = substTysWith [tv] [xi] xis
1158 dict_co = mkTyConAppCo con cos
1159 ; dv' <- newDictVar cl args
1161 Wanted {} -> setDictBind dv (EvCast dv' (mkSymCo dict_co))
1162 Given {} -> setDictBind dv' (EvCast dv dict_co)
1163 Derived {} -> return () -- Derived dicts we don't set any evidence
1165 ; return (CDictCan { cc_id = dv'
1168 , cc_tyargs = args }) }
1170 rewriteIP :: (CoVar,TcTyVar,Xi) -> (EvVar,CtFlavor, IPName Name, TcType) -> TcS CanonicalCt
1171 rewriteIP (cv,tv,xi) (ipid,gw,nm,ty)
1172 = do { let ip_co = liftCoSubstWith [tv] [mkCoVarCo cv] ty -- ty[tv] ~ t[xi]
1173 ty' = substTyWith [tv] [xi] ty
1174 ; ipid' <- newIPVar nm ty'
1176 Wanted {} -> setIPBind ipid (EvCast ipid' (mkSymCo ip_co))
1177 Given {} -> setIPBind ipid' (EvCast ipid ip_co)
1178 Derived {} -> return () -- Derived ips: we don't set any evidence
1180 ; return (CIPCan { cc_id = ipid'
1183 , cc_ip_ty = ty' }) }
1185 rewriteFunEq :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TyCon, [Xi], Xi) -> TcS CanonicalCt
1186 rewriteFunEq (cv1,tv,xi1) (cv2,gw, tc,args,xi2) -- cv2 :: F args ~ xi2
1187 = do { let co_subst = liftCoSubstWith [tv] [mkCoVarCo cv1]
1188 arg_cos = map co_subst args
1189 args' = substTysWith [tv] [xi1] args
1190 fun_co = mkTyConAppCo tc arg_cos -- fun_co :: F args ~ F args'
1192 xi2' = substTyWith [tv] [xi1] xi2
1193 xi2_co = co_subst xi2 -- xi2_co :: xi2 ~ xi2'
1195 ; cv2' <- newCoVar (mkTyConApp tc args') xi2'
1197 Wanted {} -> setCoBind cv2 (fun_co `mkTransCo`
1198 mkCoVarCo cv2' `mkTransCo`
1200 Given {} -> setCoBind cv2' (mkSymCo fun_co `mkTransCo`
1201 mkCoVarCo cv2 `mkTransCo`
1203 Derived {} -> return ()
1205 ; return (CFunEqCan { cc_id = cv2'
1209 , cc_rhs = xi2' }) }
1212 rewriteEqRHS :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TcTyVar,Xi) -> TcS WorkList
1213 -- Use the first equality to rewrite the second, flavors already checked.
1214 -- E.g. c1 : tv1 ~ xi1 c2 : tv2 ~ xi2
1215 -- rewrites c2 to give
1216 -- c2' : tv2 ~ xi2[xi1/tv1]
1217 -- We must do an occurs check to sure the new constraint is canonical
1218 -- So we might return an empty bag
1219 rewriteEqRHS (cv1,tv1,xi1) (cv2,gw,tv2,xi2)
1220 | Just tv2' <- tcGetTyVar_maybe xi2'
1221 , tv2 == tv2' -- In this case xi2[xi1/tv1] = tv2, so we have tv2~tv2
1222 = do { when (isWanted gw) (setCoBind cv2 (mkSymCo co2'))
1223 ; return emptyWorkList }
1225 = do { cv2' <- newCoVar (mkTyVarTy tv2) xi2'
1227 Wanted {} -> setCoBind cv2 $ mkCoVarCo cv2' `mkTransCo`
1229 Given {} -> setCoBind cv2' $ mkCoVarCo cv2 `mkTransCo`
1231 Derived {} -> return ()
1232 ; canEqToWorkList gw cv2' (mkTyVarTy tv2) xi2' }
1234 xi2' = substTyWith [tv1] [xi1] xi2
1235 co2' = liftCoSubstWith [tv1] [mkCoVarCo cv1] xi2 -- xi2 ~ xi2[xi1/tv1]
1237 rewriteEqLHS :: WhichComesFromInert -> (Coercion,Xi) -> (CoVar,CtFlavor,Xi) -> TcS WorkList
1238 -- Used to ineract two equalities of the following form:
1239 -- First Equality: co1: (XXX ~ xi1)
1240 -- Second Equality: cv2: (XXX ~ xi2)
1241 -- Where the cv1 `canRewrite` cv2 equality
1242 -- We have an option of creating new work (xi1 ~ xi2) OR (xi2 ~ xi1),
1243 -- See Note [Efficient Orientation] for that
1244 rewriteEqLHS LeftComesFromInert (co1,xi1) (cv2,gw,xi2)
1245 = do { cv2' <- newCoVar xi2 xi1
1247 Wanted {} -> setCoBind cv2 $
1248 co1 `mkTransCo` mkSymCo (mkCoVarCo cv2')
1249 Given {} -> setCoBind cv2' $
1250 mkSymCo (mkCoVarCo cv2) `mkTransCo` co1
1251 Derived {} -> return ()
1252 ; mkCanonical gw cv2' }
1254 rewriteEqLHS RightComesFromInert (co1,xi1) (cv2,gw,xi2)
1255 = do { cv2' <- newCoVar xi1 xi2
1257 Wanted {} -> setCoBind cv2 $
1258 co1 `mkTransCo` mkCoVarCo cv2'
1259 Given {} -> setCoBind cv2' $
1260 mkSymCo co1 `mkTransCo` mkCoVarCo cv2
1261 Derived {} -> return ()
1262 ; mkCanonical gw cv2' }
1264 rewriteFrozen :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor) -> TcS WorkList
1265 rewriteFrozen (cv1, tv1, xi1) (cv2, fl2)
1266 = do { cv2' <- newCoVar ty2a' ty2b' -- ty2a[xi1/tv1] ~ ty2b[xi1/tv1]
1268 Wanted {} -> setCoBind cv2 $ co2a' `mkTransCo`
1269 mkCoVarCo cv2' `mkTransCo`
1272 Given {} -> setCoBind cv2' $ mkSymCo co2a' `mkTransCo`
1273 mkCoVarCo cv2 `mkTransCo`
1276 Derived {} -> return ()
1278 ; return (workListFromNonEq $ CFrozenErr { cc_id = cv2', cc_flavor = fl2 }) }
1280 (ty2a, ty2b) = coVarKind cv2 -- cv2 : ty2a ~ ty2b
1281 ty2a' = substTyWith [tv1] [xi1] ty2a
1282 ty2b' = substTyWith [tv1] [xi1] ty2b
1284 co2a' = liftCoSubstWith [tv1] [mkCoVarCo cv1] ty2a -- ty2a ~ ty2a[xi1/tv1]
1285 co2b' = liftCoSubstWith [tv1] [mkCoVarCo cv1] ty2b -- ty2b ~ ty2b[xi1/tv1]
1287 solveOneFromTheOther :: String -> (EvTerm, CtFlavor) -> CanonicalCt -> TcS InteractResult
1288 -- First argument inert, second argument work-item. They both represent
1289 -- wanted/given/derived evidence for the *same* predicate so
1290 -- we can discharge one directly from the other.
1292 -- Precondition: value evidence only (implicit parameters, classes)
1294 solveOneFromTheOther info (ev_term,ifl) workItem
1296 = mkIRStopK ("Solved[DW] " ++ info) emptyWorkList
1298 | isDerived ifl -- The inert item is Derived, we can just throw it away,
1299 -- The workItem is inert wrt earlier inert-set items,
1300 -- so it's safe to continue on from this point
1301 = mkIRContinue ("Solved[DI] " ++ info) workItem DropInert emptyWorkList
1303 | Just GivenSolved <- isGiven_maybe ifl, isGivenOrSolved wfl
1304 -- Same if the inert is a GivenSolved -- just get rid of it
1305 = mkIRContinue ("Solved[SI] " ++ info) workItem DropInert emptyWorkList
1308 = ASSERT( ifl `canSolve` wfl )
1309 -- Because of Note [The Solver Invariant], plus Derived dealt with
1310 do { when (isWanted wfl) $ setEvBind wid ev_term
1311 -- Overwrite the binding, if one exists
1312 -- If both are Given, we already have evidence; no need to duplicate
1313 ; mkIRStopK ("Solved " ++ info) emptyWorkList }
1315 wfl = cc_flavor workItem
1316 wid = cc_id workItem
1319 Note [Superclasses and recursive dictionaries]
1320 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1321 Overlaps with Note [SUPERCLASS-LOOP 1]
1322 Note [SUPERCLASS-LOOP 2]
1323 Note [Recursive instances and superclases]
1324 ToDo: check overlap and delete redundant stuff
1326 Right before adding a given into the inert set, we must
1327 produce some more work, that will bring the superclasses
1328 of the given into scope. The superclass constraints go into
1331 When we simplify a wanted constraint, if we first see a matching
1332 instance, we may produce new wanted work. To (1) avoid doing this work
1333 twice in the future and (2) to handle recursive dictionaries we may ``cache''
1334 this item as given into our inert set WITHOUT adding its superclass constraints,
1335 otherwise we'd be in danger of creating a loop [In fact this was the exact reason
1336 for doing the isGoodRecEv check in an older version of the type checker].
1338 But now we have added partially solved constraints to the worklist which may
1339 interact with other wanteds. Consider the example:
1343 class Eq b => Foo a b --- 0-th selector
1344 instance Eq a => Foo [a] a --- fooDFun
1346 and wanted (Foo [t] t). We are first going to see that the instance matches
1347 and create an inert set that includes the solved (Foo [t] t) but not its superclasses:
1348 d1 :_g Foo [t] t d1 := EvDFunApp fooDFun d3
1349 Our work list is going to contain a new *wanted* goal
1352 Ok, so how do we get recursive dictionaries, at all:
1356 data D r = ZeroD | SuccD (r (D r));
1358 instance (Eq (r (D r))) => Eq (D r) where
1359 ZeroD == ZeroD = True
1360 (SuccD a) == (SuccD b) = a == b
1363 equalDC :: D [] -> D [] -> Bool;
1366 We need to prove (Eq (D [])). Here's how we go:
1370 by instance decl, holds if
1374 *BUT* we have an inert set which gives us (no superclasses):
1376 By the instance declaration of Eq we can show the 'd2' goal if
1378 where d2 = dfEqList d3
1380 Now, however this wanted can interact with our inert d1 to set:
1382 and solve the goal. Why was this interaction OK? Because, if we chase the
1383 evidence of d1 ~~> dfEqD d2 ~~-> dfEqList d3, so by setting d3 := d1 we
1385 d3 := dfEqD2 (dfEqList d3)
1386 which is FINE because the use of d3 is protected by the instance function
1389 So, our strategy is to try to put solved wanted dictionaries into the
1390 inert set along with their superclasses (when this is meaningful,
1391 i.e. when new wanted goals are generated) but solve a wanted dictionary
1392 from a given only in the case where the evidence variable of the
1393 wanted is mentioned in the evidence of the given (recursively through
1394 the evidence binds) in a protected way: more instance function applications
1395 than superclass selectors.
1397 Here are some more examples from GHC's previous type checker
1401 This code arises in the context of "Scrap Your Boilerplate with Class"
1405 instance Sat (ctx Char) => Data ctx Char -- dfunData1
1406 instance (Sat (ctx [a]), Data ctx a) => Data ctx [a] -- dfunData2
1408 class Data Maybe a => Foo a
1410 instance Foo t => Sat (Maybe t) -- dfunSat
1412 instance Data Maybe a => Foo a -- dfunFoo1
1413 instance Foo a => Foo [a] -- dfunFoo2
1414 instance Foo [Char] -- dfunFoo3
1416 Consider generating the superclasses of the instance declaration
1417 instance Foo a => Foo [a]
1419 So our problem is this
1421 d1 :_w Data Maybe [t]
1423 We may add the given in the inert set, along with its superclasses
1424 [assuming we don't fail because there is a matching instance, see
1425 tryTopReact, given case ]
1429 d01 :_g Data Maybe t -- d2 := EvDictSuperClass d0 0
1430 d1 :_w Data Maybe [t]
1431 Then d2 can readily enter the inert, and we also do solving of the wanted
1434 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1436 d2 :_w Sat (Maybe [t])
1438 d01 :_g Data Maybe t
1439 Now, we may simplify d2 more:
1442 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1443 d1 :_g Data Maybe [t]
1444 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1448 d01 :_g Data Maybe t
1450 Now, we can just solve d3.
1453 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1454 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1457 d01 :_g Data Maybe t
1458 And now we can simplify d4 again, but since it has superclasses we *add* them to the worklist:
1461 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1462 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1463 d4 :_g Foo [t] d4 := dfunFoo2 d5
1466 d6 :_g Data Maybe [t] d6 := EvDictSuperClass d4 0
1467 d01 :_g Data Maybe t
1468 Now, d5 can be solved! (and its superclass enter scope)
1471 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1472 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1473 d4 :_g Foo [t] d4 := dfunFoo2 d5
1474 d5 :_g Foo t d5 := dfunFoo1 d7
1477 d6 :_g Data Maybe [t]
1478 d8 :_g Data Maybe t d8 := EvDictSuperClass d5 0
1479 d01 :_g Data Maybe t
1482 [1] Suppose we pick d8 and we react him with d01. Which of the two givens should
1483 we keep? Well, we *MUST NOT* drop d01 because d8 contains recursive evidence
1484 that must not be used (look at case interactInert where both inert and workitem
1485 are givens). So we have several options:
1486 - Drop the workitem always (this will drop d8)
1487 This feels very unsafe -- what if the work item was the "good" one
1488 that should be used later to solve another wanted?
1489 - Don't drop anyone: the inert set may contain multiple givens!
1490 [This is currently implemented]
1492 The "don't drop anyone" seems the most safe thing to do, so now we come to problem 2:
1493 [2] We have added both d6 and d01 in the inert set, and we are interacting our wanted
1494 d7. Now the [isRecDictEv] function in the ineration solver
1495 [case inert-given workitem-wanted] will prevent us from interacting d7 := d8
1496 precisely because chasing the evidence of d8 leads us to an unguarded use of d7.
1498 So, no interaction happens there. Then we meet d01 and there is no recursion
1499 problem there [isRectDictEv] gives us the OK to interact and we do solve d7 := d01!
1501 Note [SUPERCLASS-LOOP 1]
1502 ~~~~~~~~~~~~~~~~~~~~~~~~
1503 We have to be very, very careful when generating superclasses, lest we
1504 accidentally build a loop. Here's an example:
1508 class S a => C a where { opc :: a -> a }
1509 class S b => D b where { opd :: b -> b }
1511 instance C Int where
1514 instance D Int where
1517 From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int}
1518 Simplifying, we may well get:
1519 $dfCInt = :C ds1 (opd dd)
1522 Notice that we spot that we can extract ds1 from dd.
1524 Alas! Alack! We can do the same for (instance D Int):
1526 $dfDInt = :D ds2 (opc dc)
1530 And now we've defined the superclass in terms of itself.
1531 Two more nasty cases are in
1536 - Satisfy the superclass context *all by itself*
1537 (tcSimplifySuperClasses)
1538 - And do so completely; i.e. no left-over constraints
1539 to mix with the constraints arising from method declarations
1542 Note [SUPERCLASS-LOOP 2]
1543 ~~~~~~~~~~~~~~~~~~~~~~~~
1544 We need to be careful when adding "the constaint we are trying to prove".
1545 Suppose we are *given* d1:Ord a, and want to deduce (d2:C [a]) where
1547 class Ord a => C a where
1548 instance Ord [a] => C [a] where ...
1550 Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the
1551 superclasses of C [a] to avails. But we must not overwrite the binding
1552 for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
1555 Here's another variant, immortalised in tcrun020
1556 class Monad m => C1 m
1557 class C1 m => C2 m x
1558 instance C2 Maybe Bool
1559 For the instance decl we need to build (C1 Maybe), and it's no good if
1560 we run around and add (C2 Maybe Bool) and its superclasses to the avails
1561 before we search for C1 Maybe.
1563 Here's another example
1564 class Eq b => Foo a b
1565 instance Eq a => Foo [a] a
1569 we'll first deduce that it holds (via the instance decl). We must not
1570 then overwrite the Eq t constraint with a superclass selection!
1572 At first I had a gross hack, whereby I simply did not add superclass constraints
1573 in addWanted, though I did for addGiven and addIrred. This was sub-optimal,
1574 becuase it lost legitimate superclass sharing, and it still didn't do the job:
1575 I found a very obscure program (now tcrun021) in which improvement meant the
1576 simplifier got two bites a the cherry... so something seemed to be an Stop
1577 first time, but reducible next time.
1579 Now we implement the Right Solution, which is to check for loops directly
1580 when adding superclasses. It's a bit like the occurs check in unification.
1582 Note [Recursive instances and superclases]
1583 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1584 Consider this code, which arises in the context of "Scrap Your
1585 Boilerplate with Class".
1589 instance Sat (ctx Char) => Data ctx Char
1590 instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]
1592 class Data Maybe a => Foo a
1594 instance Foo t => Sat (Maybe t)
1596 instance Data Maybe a => Foo a
1597 instance Foo a => Foo [a]
1600 In the instance for Foo [a], when generating evidence for the superclasses
1601 (ie in tcSimplifySuperClasses) we need a superclass (Data Maybe [a]).
1602 Using the instance for Data, we therefore need
1603 (Sat (Maybe [a], Data Maybe a)
1604 But we are given (Foo a), and hence its superclass (Data Maybe a).
1605 So that leaves (Sat (Maybe [a])). Using the instance for Sat means
1606 we need (Foo [a]). And that is the very dictionary we are bulding
1607 an instance for! So we must put that in the "givens". So in this
1609 Given: Foo a, Foo [a]
1610 Wanted: Data Maybe [a]
1612 BUT we must *not not not* put the *superclasses* of (Foo [a]) in
1613 the givens, which is what 'addGiven' would normally do. Why? Because
1614 (Data Maybe [a]) is the superclass, so we'd "satisfy" the wanted
1615 by selecting a superclass from Foo [a], which simply makes a loop.
1617 On the other hand we *must* put the superclasses of (Foo a) in
1618 the givens, as you can see from the derivation described above.
1620 Conclusion: in the very special case of tcSimplifySuperClasses
1621 we have one 'given' (namely the "this" dictionary) whose superclasses
1622 must not be added to 'givens' by addGiven.
1624 There is a complication though. Suppose there are equalities
1625 instance (Eq a, a~b) => Num (a,b)
1626 Then we normalise the 'givens' wrt the equalities, so the original
1627 given "this" dictionary is cast to one of a different type. So it's a
1628 bit trickier than before to identify the "special" dictionary whose
1629 superclasses must not be added. See test
1630 indexed-types/should_run/EqInInstance
1632 We need a persistent property of the dictionary to record this
1633 special-ness. Current I'm using the InstLocOrigin (a bit of a hack,
1634 but cool), which is maintained by dictionary normalisation.
1635 Specifically, the InstLocOrigin is
1637 then the no-superclass thing kicks in. WATCH OUT if you fiddle
1640 Note [MATCHING-SYNONYMS]
1641 ~~~~~~~~~~~~~~~~~~~~~~~~
1642 When trying to match a dictionary (D tau) to a top-level instance, or a
1643 type family equation (F taus_1 ~ tau_2) to a top-level family instance,
1644 we do *not* need to expand type synonyms because the matcher will do that for us.
1647 Note [RHS-FAMILY-SYNONYMS]
1648 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1649 The RHS of a family instance is represented as yet another constructor which is
1650 like a type synonym for the real RHS the programmer declared. Eg:
1651 type instance F (a,a) = [a]
1653 :R32 a = [a] -- internal type synonym introduced
1654 F (a,a) ~ :R32 a -- instance
1656 When we react a family instance with a type family equation in the work list
1657 we keep the synonym-using RHS without expansion.
1660 *********************************************************************************
1662 The top-reaction Stage
1664 *********************************************************************************
1667 -- If a work item has any form of interaction with top-level we get this
1668 data TopInteractResult
1669 = NoTopInt -- No top-level interaction
1670 -- Equivalent to (SomeTopInt emptyWorkList (ContinueWith work_item))
1672 { tir_new_work :: WorkList -- Sub-goals or new work (could be given,
1673 -- for superclasses)
1674 , tir_new_inert :: StopOrContinue -- The input work item, ready to become *inert* now:
1675 } -- NB: in ``given'' (solved) form if the
1676 -- original was wanted or given and instance match
1677 -- was found, but may also be in wanted form if we
1678 -- only reacted with functional dependencies
1679 -- arising from top-level instances.
1681 topReactionsStage :: SimplifierStage
1682 topReactionsStage depth workItem inerts
1683 = do { tir <- tryTopReact inerts workItem
1684 -- NB: we pass the inerts as well. See Note [Instance and Given overlap]
1687 return $ SR { sr_inerts = inerts
1688 , sr_new_work = emptyWorkList
1689 , sr_stop = ContinueWith workItem }
1690 SomeTopInt tir_new_work tir_new_inert ->
1691 do { bumpStepCountTcS
1692 ; traceFireTcS depth (ptext (sLit "Top react")
1693 <+> vcat [ ptext (sLit "Work =") <+> ppr workItem
1694 , ptext (sLit "New =") <+> ppr tir_new_work ])
1695 ; return $ SR { sr_inerts = inerts
1696 , sr_new_work = tir_new_work
1697 , sr_stop = tir_new_inert
1701 tryTopReact :: InertSet -> WorkItem -> TcS TopInteractResult
1702 tryTopReact inerts workitem
1703 = do { -- A flag controls the amount of interaction allowed
1704 -- See Note [Simplifying RULE lhs constraints]
1705 ctxt <- getTcSContext
1706 ; if allowedTopReaction (simplEqsOnly ctxt) workitem
1707 then do { traceTcS "tryTopReact / calling doTopReact" (ppr workitem)
1708 ; doTopReact inerts workitem }
1709 else return NoTopInt
1712 allowedTopReaction :: Bool -> WorkItem -> Bool
1713 allowedTopReaction eqs_only (CDictCan {}) = not eqs_only
1714 allowedTopReaction _ _ = True
1716 doTopReact :: InertSet -> WorkItem -> TcS TopInteractResult
1717 -- The work item does not react with the inert set, so try interaction with top-level instances
1718 -- NB: The place to add superclasses in *not* in doTopReact stage. Instead superclasses are
1719 -- added in the worklist as part of the canonicalisation process.
1720 -- See Note [Adding superclasses] in TcCanonical.
1723 -- See Note [Given constraint that matches an instance declaration]
1724 doTopReact _inerts (CDictCan { cc_flavor = Given {} })
1725 = return NoTopInt -- NB: Superclasses already added since it's canonical
1727 -- Derived dictionary: just look for functional dependencies
1728 doTopReact _inerts workItem@(CDictCan { cc_flavor = fl@(Derived loc)
1729 , cc_class = cls, cc_tyargs = xis })
1730 = do { instEnvs <- getInstEnvs
1731 ; let fd_eqns = improveFromInstEnv instEnvs
1732 (ClassP cls xis, pprArisingAt loc)
1733 ; m <- rewriteWithFunDeps fd_eqns xis fl
1735 Nothing -> return NoTopInt
1736 Just (xis',_,fd_work) ->
1737 let workItem' = workItem { cc_tyargs = xis' }
1738 -- Deriveds are not supposed to have identity (cc_id is unused!)
1739 in return $ SomeTopInt { tir_new_work = fd_work
1740 , tir_new_inert = ContinueWith workItem' } }
1742 -- Wanted dictionary
1743 doTopReact inerts workItem@(CDictCan { cc_id = dv, cc_flavor = fl@(Wanted loc)
1744 , cc_class = cls, cc_tyargs = xis })
1745 = do { -- See Note [MATCHING-SYNONYMS]
1746 ; lkp_inst_res <- matchClassInst inerts cls xis loc
1747 ; case lkp_inst_res of
1749 do { traceTcS "doTopReact/ no class instance for" (ppr dv)
1751 ; instEnvs <- getInstEnvs
1752 ; let fd_eqns = improveFromInstEnv instEnvs
1753 (ClassP cls xis, pprArisingAt loc)
1754 ; m <- rewriteWithFunDeps fd_eqns xis fl
1756 Nothing -> return NoTopInt
1757 Just (xis',cos,fd_work) ->
1758 do { let dict_co = mkTyConAppCo (classTyCon cls) cos
1759 ; dv'<- newDictVar cls xis'
1760 ; setDictBind dv (EvCast dv' dict_co)
1761 ; let workItem' = CDictCan { cc_id = dv', cc_flavor = fl,
1762 cc_class = cls, cc_tyargs = xis' }
1764 SomeTopInt { tir_new_work = workListFromNonEq workItem' `unionWorkList` fd_work
1765 , tir_new_inert = Stop } } }
1767 GenInst wtvs ev_term -- Solved
1768 -- No need to do fundeps stuff here; the instance
1769 -- matches already so we won't get any more info
1770 -- from functional dependencies
1772 -> do { traceTcS "doTopReact/found nullary class instance for" (ppr dv)
1773 ; setDictBind dv ev_term
1774 -- Solved in one step and no new wanted work produced.
1775 -- i.e we directly matched a top-level instance
1776 -- No point in caching this in 'inert'; hence Stop
1777 ; return $ SomeTopInt { tir_new_work = emptyWorkList
1778 , tir_new_inert = Stop } }
1781 -> do { traceTcS "doTopReact/found non-nullary class instance for" (ppr dv)
1782 ; setDictBind dv ev_term
1783 -- Solved and new wanted work produced, you may cache the
1784 -- (tentatively solved) dictionary as Solved given.
1785 ; let solved = workItem { cc_flavor = solved_fl }
1786 solved_fl = mkSolvedFlavor fl UnkSkol
1787 ; inst_work <- canWanteds wtvs
1788 ; return $ SomeTopInt { tir_new_work = inst_work
1789 , tir_new_inert = ContinueWith solved } }
1793 doTopReact _inerts (CFunEqCan { cc_flavor = fl })
1794 | Just GivenSolved <- isGiven_maybe fl
1795 = return NoTopInt -- If Solved, no more interactions should happen
1797 -- Otherwise, it's a Given, Derived, or Wanted
1798 doTopReact _inerts workItem@(CFunEqCan { cc_id = cv, cc_flavor = fl
1799 , cc_fun = tc, cc_tyargs = args, cc_rhs = xi })
1800 = ASSERT (isSynFamilyTyCon tc) -- No associated data families have reached that far
1801 do { match_res <- matchFam tc args -- See Note [MATCHING-SYNONYMS]
1803 MatchInstNo -> return NoTopInt
1804 MatchInstSingle (rep_tc, rep_tys)
1805 -> do { let Just coe_tc = tyConFamilyCoercion_maybe rep_tc
1806 Just rhs_ty = tcView (mkTyConApp rep_tc rep_tys)
1807 -- Eagerly expand away the type synonym on the
1808 -- RHS of a type function, so that it never
1809 -- appears in an error message
1810 -- See Note [Type synonym families] in TyCon
1811 coe = mkAxInstCo coe_tc rep_tys
1813 Wanted {} -> do { cv' <- newCoVar rhs_ty xi
1814 ; setCoBind cv $ coe `mkTransCo` mkCoVarCo cv'
1815 ; can_cts <- mkCanonical fl cv'
1816 ; let solved = workItem { cc_flavor = solved_fl }
1817 solved_fl = mkSolvedFlavor fl UnkSkol
1818 ; if isEmptyWorkList can_cts then
1819 return (SomeTopInt can_cts Stop) -- No point in caching
1821 SomeTopInt { tir_new_work = can_cts
1822 , tir_new_inert = ContinueWith solved }
1824 Given {} -> do { cv' <- newGivenCoVar xi rhs_ty $
1825 mkSymCo (mkCoVarCo cv) `mkTransCo` coe
1826 ; can_cts <- mkCanonical fl cv'
1828 SomeTopInt { tir_new_work = can_cts
1829 , tir_new_inert = Stop }
1831 Derived {} -> do { cv' <- newDerivedId (EqPred xi rhs_ty)
1832 ; can_cts <- mkCanonical fl cv'
1834 SomeTopInt { tir_new_work = can_cts
1835 , tir_new_inert = Stop }
1839 -> panicTcS $ text "TcSMonad.matchFam returned multiple instances!"
1843 -- Any other work item does not react with any top-level equations
1844 doTopReact _inerts _workItem = return NoTopInt
1848 Note [FunDep and implicit parameter reactions]
1849 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1850 Currently, our story of interacting two dictionaries (or a dictionary
1851 and top-level instances) for functional dependencies, and implicit
1852 paramters, is that we simply produce new wanted equalities. So for example
1854 class D a b | a -> b where ...
1860 We generate the extra work item
1862 where 'cv' is currently unused. However, this new item reacts with d2,
1863 discharging it in favour of a new constraint d2' thus:
1865 d2 := d2' |> D Int cv
1866 Now d2' can be discharged from d1
1868 We could be more aggressive and try to *immediately* solve the dictionary
1869 using those extra equalities. With the same inert set and work item we
1870 might dischard d2 directly:
1873 d2 := d1 |> D Int cv
1875 But in general it's a bit painful to figure out the necessary coercion,
1876 so we just take the first approach. Here is a better example. Consider:
1877 class C a b c | a -> b
1879 [Given] d1 : C T Int Char
1880 [Wanted] d2 : C T beta Int
1881 In this case, it's *not even possible* to solve the wanted immediately.
1882 So we should simply output the functional dependency and add this guy
1883 [but NOT its superclasses] back in the worklist. Even worse:
1884 [Given] d1 : C T Int beta
1885 [Wanted] d2: C T beta Int
1886 Then it is solvable, but its very hard to detect this on the spot.
1888 It's exactly the same with implicit parameters, except that the
1889 "aggressive" approach would be much easier to implement.
1891 Note [When improvement happens]
1892 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1893 We fire an improvement rule when
1895 * Two constraints match (modulo the fundep)
1896 e.g. C t1 t2, C t1 t3 where C a b | a->b
1897 The two match because the first arg is identical
1899 * At least one is not Given. If they are both given, we don't fire
1900 the reaction because we have no way of constructing evidence for a
1901 new equality nor does it seem right to create a new wanted goal
1902 (because the goal will most likely contain untouchables, which
1903 can't be solved anyway)!
1905 Note that we *do* fire the improvement if one is Given and one is Derived.
1906 The latter can be a superclass of a wanted goal. Example (tcfail138)
1907 class L a b | a -> b
1908 class (G a, L a b) => C a b
1910 instance C a b' => G (Maybe a)
1911 instance C a b => C (Maybe a) a
1912 instance L (Maybe a) a
1914 When solving the superclasses of the (C (Maybe a) a) instance, we get
1915 Given: C a b ... and hance by superclasses, (G a, L a b)
1917 Use the instance decl to get
1919 The (C a b') is inert, so we generate its Derived superclasses (L a b'),
1920 and now we need improvement between that derived superclass an the Given (L a b)
1922 Note [Overriding implicit parameters]
1923 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1925 f :: (?x::a) -> Bool -> a
1927 g v = let ?x::Int = 3
1928 in (f v, let ?x::Bool = True in f v)
1930 This should probably be well typed, with
1931 g :: Bool -> (Int, Bool)
1933 So the inner binding for ?x::Bool *overrides* the outer one.
1934 Hence a work-item Given overrides an inert-item Given.
1936 Note [Given constraint that matches an instance declaration]
1937 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1938 What should we do when we discover that one (or more) top-level
1939 instances match a given (or solved) class constraint? We have
1942 1. Reject the program. The reason is that there may not be a unique
1943 best strategy for the solver. Example, from the OutsideIn(X) paper:
1944 instance P x => Q [x]
1945 instance (x ~ y) => R [x] y
1947 wob :: forall a b. (Q [b], R b a) => a -> Int
1949 g :: forall a. Q [a] => [a] -> Int
1952 will generate the impliation constraint:
1953 Q [a] => (Q [beta], R beta [a])
1954 If we react (Q [beta]) with its top-level axiom, we end up with a
1955 (P beta), which we have no way of discharging. On the other hand,
1956 if we react R beta [a] with the top-level we get (beta ~ a), which
1957 is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
1958 now solvable by the given Q [a].
1960 However, this option is restrictive, for instance [Example 3] from
1961 Note [Recursive dictionaries] will fail to work.
1963 2. Ignore the problem, hoping that the situations where there exist indeed
1964 such multiple strategies are rare: Indeed the cause of the previous
1965 problem is that (R [x] y) yields the new work (x ~ y) which can be
1966 *spontaneously* solved, not using the givens.
1968 We are choosing option 2 below but we might consider having a flag as well.
1971 Note [New Wanted Superclass Work]
1972 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1973 Even in the case of wanted constraints, we may add some superclasses
1974 as new given work. The reason is:
1976 To allow FD-like improvement for type families. Assume that
1978 class C a b | a -> b
1979 and we have to solve the implication constraint:
1981 Then, FD improvement can help us to produce a new wanted (beta ~ b)
1983 We want to have the same effect with the type family encoding of
1984 functional dependencies. Namely, consider:
1985 class (F a ~ b) => C a b
1986 Now suppose that we have:
1989 By interacting the given we will get given (F a ~ b) which is not
1990 enough by itself to make us discharge (C a beta). However, we
1991 may create a new derived equality from the super-class of the
1992 wanted constraint (C a beta), namely derived (F a ~ beta).
1993 Now we may interact this with given (F a ~ b) to get:
1995 But 'beta' is a touchable unification variable, and hence OK to
1996 unify it with 'b', replacing the derived evidence with the identity.
1998 This requires trySpontaneousSolve to solve *derived*
1999 equalities that have a touchable in their RHS, *in addition*
2000 to solving wanted equalities.
2002 We also need to somehow use the superclasses to quantify over a minimal,
2003 constraint see note [Minimize by Superclasses] in TcSimplify.
2006 Finally, here is another example where this is useful.
2010 class (F a ~ b) => C a b
2011 And we are given the wanteds:
2015 We surely do *not* want to quantify over (b ~ c), since if someone provides
2016 dictionaries for (C a b) and (C a c), these dictionaries can provide a proof
2017 of (b ~ c), hence no extra evidence is necessary. Here is what will happen:
2019 Step 1: We will get new *given* superclass work,
2020 provisionally to our solving of w1 and w2
2022 g1: F a ~ b, g2 : F a ~ c,
2023 w1 : C a b, w2 : C a c, w3 : b ~ c
2025 The evidence for g1 and g2 is a superclass evidence term:
2027 g1 := sc w1, g2 := sc w2
2029 Step 2: The givens will solve the wanted w3, so that
2030 w3 := sym (sc w1) ; sc w2
2032 Step 3: Now, one may naively assume that then w2 can be solve from w1
2033 after rewriting with the (now solved equality) (b ~ c).
2035 But this rewriting is ruled out by the isGoodRectDict!
2037 Conclusion, we will (correctly) end up with the unsolved goals
2040 NB: The desugarer needs be more clever to deal with equalities
2041 that participate in recursive dictionary bindings.
2044 data LookupInstResult
2046 | GenInst [WantedEvVar] EvTerm
2048 matchClassInst :: InertSet -> Class -> [Type] -> WantedLoc -> TcS LookupInstResult
2049 matchClassInst inerts clas tys loc
2050 = do { let pred = mkClassPred clas tys
2051 ; mb_result <- matchClass clas tys
2052 ; untch <- getUntouchables
2054 MatchInstNo -> return NoInstance
2055 MatchInstMany -> return NoInstance -- defer any reactions of a multitude until
2056 -- we learn more about the reagent
2057 MatchInstSingle (_,_)
2058 | given_overlap untch ->
2059 do { traceTcS "Delaying instance application" $
2060 vcat [ text "Workitem=" <+> pprPredTy (ClassP clas tys)
2061 , text "Silents and their superclasses=" <+> ppr silents_and_their_scs
2062 , text "All given dictionaries=" <+> ppr all_given_dicts ]
2063 ; return NoInstance -- see Note [Instance and Given overlap]
2066 MatchInstSingle (dfun_id, mb_inst_tys) ->
2067 do { checkWellStagedDFun pred dfun_id loc
2069 -- It's possible that not all the tyvars are in
2070 -- the substitution, tenv. For example:
2071 -- instance C X a => D X where ...
2072 -- (presumably there's a functional dependency in class C)
2073 -- Hence mb_inst_tys :: Either TyVar TcType
2075 ; tys <- instDFunTypes mb_inst_tys
2076 ; let (theta, _) = tcSplitPhiTy (applyTys (idType dfun_id) tys)
2077 ; if null theta then
2078 return (GenInst [] (EvDFunApp dfun_id tys []))
2080 { ev_vars <- instDFunConstraints theta
2081 ; let wevs = [EvVarX w loc | w <- ev_vars]
2082 ; return $ GenInst wevs (EvDFunApp dfun_id tys ev_vars) }
2085 where given_overlap :: TcsUntouchables -> Bool
2087 = foldlBag (\r d -> r || matchable untch d) False all_given_dicts
2089 matchable untch (CDictCan { cc_class = clas', cc_tyargs = sys, cc_flavor = fl })
2090 | Just GivenOrig <- isGiven_maybe fl
2092 , does_not_originate_in_a_silent clas' sys
2093 = case tcUnifyTys (\tv -> if isTouchableMetaTyVar_InRange untch tv &&
2094 tv `elemVarSet` tyVarsOfTypes tys
2095 then BindMe else Skolem) tys sys of
2096 -- We can't learn anything more about any variable at this point, so the only
2097 -- cause of overlap can be by an instantiation of a touchable unification
2098 -- variable. Hence we only bind touchable unification variables. In addition,
2099 -- we use tcUnifyTys instead of tcMatchTys to rule out cyclic substitutions.
2102 | otherwise = False -- No overlap with a solved, already been taken care of
2103 -- by the overlap check with the instance environment.
2104 matchable _tys ct = pprPanic "Expecting dictionary!" (ppr ct)
2106 does_not_originate_in_a_silent clas sys
2107 -- UGLY: See Note [Silent parameters overlapping]
2108 = null $ filter (eqPred (ClassP clas sys)) silents_and_their_scs
2110 silents_and_their_scs
2111 = foldlBag (\acc rvnt -> case rvnt of
2112 CDictCan { cc_id = d, cc_class = c, cc_tyargs = s }
2113 | isSilentEvVar d -> (ClassP c s) : (transSuperClasses c s) ++ acc
2114 _ -> acc) [] all_given_dicts
2117 -- When silent parameters will go away we should simply select from
2118 -- the given map of the inert set.
2119 all_given_dicts = Map.fold unionBags emptyCCan (cts_given $ inert_dicts inerts)
2123 Note [Silent parameters overlapping]
2124 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2126 The long-term goal is to completely remove silent superclass
2127 parameters when checking instance declarations. But until then we must
2128 make sure that we never prevent the application of an instance
2129 declaration because of a potential match from a silent parameter --
2130 after all we are supposed to have solved that silent parameter from
2131 some instance, anyway! In effect silent parameters behave more like
2132 Solved than like Given.
2134 A concrete example appears in typecheck/SilentParametersOverlapping.hs
2136 Note [Instance and Given overlap]
2137 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2138 Assume that we have an inert set that looks as follows:
2140 And an instance declaration:
2141 instance C a => D [a]
2142 A new wanted comes along of the form:
2145 One possibility is to apply the instance declaration which will leave us
2146 with an unsolvable goal (C alpha). However, later on a new constraint may
2147 arise (for instance due to a functional dependency between two later dictionaries),
2148 that will add the equality (alpha ~ Int), in which case our ([Wanted] D [alpha])
2149 will be transformed to [Wanted] D [Int], which could have been discharged by the given.
2151 The solution is that in matchClassInst and eventually in topReact, we get back with
2152 a matching instance, only when there is no Given in the inerts which is unifiable to
2153 this particular dictionary.
2155 The end effect is that, much as we do for overlapping instances, we delay choosing a
2156 class instance if there is a possibility of another instance OR a given to match our
2157 constraint later on. This fixes bugs #4981 and #5002.
2159 This is arguably not easy to appear in practice due to our aggressive prioritization
2160 of equality solving over other constraints, but it is possible. I've added a test case
2161 in typecheck/should-compile/GivenOverlapping.hs
2163 Moreover notice that our goals here are different than the goals of the top-level
2164 overlapping checks. There we are interested in validating the following principle:
2166 If we inline a function f at a site where the same global instance environment
2167 is available as the instance environment at the definition site of f then we
2168 should get the same behaviour.
2170 But for the Given Overlap check our goal is just related to completeness of