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 , text "Frozen errors =" <+> -- Clearly print frozen errors
167 vcat (map ppr (Bag.bagToList $ inert_frozen is))
170 emptyInert :: InertSet
171 emptyInert = IS { inert_eqs = Bag.emptyBag
172 , inert_frozen = Bag.emptyBag
173 , inert_dicts = emptyCCanMap
174 , inert_ips = emptyCCanMap
175 , inert_funeqs = emptyCCanMap }
177 updInertSet :: InertSet -> AtomicInert -> InertSet
179 | isCTyEqCan item -- Other equality
180 = let eqs' = inert_eqs is `Bag.snocBag` item
181 in is { inert_eqs = eqs' }
182 | Just cls <- isCDictCan_Maybe item -- Dictionary
183 = is { inert_dicts = updCCanMap (cls,item) (inert_dicts is) }
184 | Just x <- isCIPCan_Maybe item -- IP
185 = is { inert_ips = updCCanMap (x,item) (inert_ips is) }
186 | Just tc <- isCFunEqCan_Maybe item -- Function equality
187 = is { inert_funeqs = updCCanMap (tc,item) (inert_funeqs is) }
189 = is { inert_frozen = inert_frozen is `Bag.snocBag` item }
191 extractUnsolved :: InertSet -> (InertSet, CanonicalCts)
192 -- Postcondition: the returned canonical cts are either Derived, or Wanted.
193 extractUnsolved is@(IS {inert_eqs = eqs})
194 = let is_solved = is { inert_eqs = solved_eqs
195 , inert_dicts = solved_dicts
196 , inert_ips = solved_ips
197 , inert_frozen = emptyCCan
198 , inert_funeqs = solved_funeqs }
199 in (is_solved, unsolved)
201 where (unsolved_eqs, solved_eqs) = Bag.partitionBag (not.isGivenOrSolvedCt) eqs
202 (unsolved_ips, solved_ips) = extractUnsolvedCMap (inert_ips is)
203 (unsolved_dicts, solved_dicts) = extractUnsolvedCMap (inert_dicts is)
204 (unsolved_funeqs, solved_funeqs) = extractUnsolvedCMap (inert_funeqs is)
206 unsolved = unsolved_eqs `unionBags` inert_frozen is `unionBags`
207 unsolved_ips `unionBags` unsolved_dicts `unionBags` unsolved_funeqs
210 %*********************************************************************
212 * Main Interaction Solver *
214 **********************************************************************
218 1. Canonicalise (unary)
219 2. Pairwise interaction (binary)
220 * Take one from work list
221 * Try all pair-wise interactions with each constraint in inert
223 As an optimisation, we prioritize the equalities both in the
224 worklist and in the inerts.
226 3. Try to solve spontaneously for equalities involving touchables
227 4. Top-level interaction (binary wrt top-level)
228 Superclass decomposition belongs in (4), see note [Superclasses]
231 type AtomicInert = CanonicalCt -- constraint pulled from InertSet
232 type WorkItem = CanonicalCt -- constraint pulled from WorkList
234 ------------------------
236 = Stop -- Work item is consumed
237 | ContinueWith WorkItem -- Not consumed
239 instance Outputable StopOrContinue where
240 ppr Stop = ptext (sLit "Stop")
241 ppr (ContinueWith w) = ptext (sLit "ContinueWith") <+> ppr w
243 -- Results after interacting a WorkItem as far as possible with an InertSet
245 = SR { sr_inerts :: InertSet
246 -- The new InertSet to use (REPLACES the old InertSet)
247 , sr_new_work :: WorkList
248 -- Any new work items generated (should be ADDED to the old WorkList)
250 -- sr_stop = Just workitem => workitem is *not* in sr_inerts and
251 -- workitem is inert wrt to sr_inerts
252 , sr_stop :: StopOrContinue
255 instance Outputable StageResult where
256 ppr (SR { sr_inerts = inerts, sr_new_work = work, sr_stop = stop })
257 = ptext (sLit "SR") <+>
258 braces (sep [ ptext (sLit "inerts =") <+> ppr inerts <> comma
259 , ptext (sLit "new work =") <+> ppr work <> comma
260 , ptext (sLit "stop =") <+> ppr stop])
262 type SubGoalDepth = Int -- Starts at zero; used to limit infinite
263 -- recursion of sub-goals
264 type SimplifierStage = SubGoalDepth -> WorkItem -> InertSet -> TcS StageResult
266 -- Combine a sequence of simplifier 'stages' to create a pipeline
267 runSolverPipeline :: SubGoalDepth
268 -> [(String, SimplifierStage)]
269 -> InertSet -> WorkItem
270 -> TcS (InertSet, WorkList)
271 -- Precondition: non-empty list of stages
272 runSolverPipeline depth pipeline inerts workItem
273 = do { traceTcS "Start solver pipeline" $
274 vcat [ ptext (sLit "work item =") <+> ppr workItem
275 , ptext (sLit "inerts =") <+> ppr inerts]
277 ; let itr_in = SR { sr_inerts = inerts
278 , sr_new_work = emptyWorkList
279 , sr_stop = ContinueWith workItem }
280 ; itr_out <- run_pipeline pipeline itr_in
282 = case sr_stop itr_out of
283 Stop -> sr_inerts itr_out
284 ContinueWith item -> sr_inerts itr_out `updInertSet` item
285 ; return (new_inert, sr_new_work itr_out) }
287 run_pipeline :: [(String, SimplifierStage)]
288 -> StageResult -> TcS StageResult
289 run_pipeline [] itr = return itr
290 run_pipeline _ itr@(SR { sr_stop = Stop }) = return itr
292 run_pipeline ((name,stage):stages)
293 (SR { sr_new_work = accum_work
295 , sr_stop = ContinueWith work_item })
296 = do { itr <- stage depth work_item inerts
297 ; traceTcS ("Stage result (" ++ name ++ ")") (ppr itr)
298 ; let itr' = itr { sr_new_work = accum_work `unionWorkList` sr_new_work itr }
299 ; run_pipeline stages itr' }
303 Inert: {c ~ d, F a ~ t, b ~ Int, a ~ ty} (all given)
304 Reagent: a ~ [b] (given)
306 React with (c~d) ==> IR (ContinueWith (a~[b])) True []
307 React with (F a ~ t) ==> IR (ContinueWith (a~[b])) False [F [b] ~ t]
308 React with (b ~ Int) ==> IR (ContinueWith (a~[Int]) True []
311 Inert: {c ~w d, F a ~g t, b ~w Int, a ~w ty}
314 React with (c ~w d) ==> IR (ContinueWith (a~[b])) True []
315 React with (F a ~g t) ==> IR (ContinueWith (a~[b])) True [] (can't rewrite given with wanted!)
319 Inert: {a ~ Int, F Int ~ b} (given)
320 Reagent: F a ~ b (wanted)
322 React with (a ~ Int) ==> IR (ContinueWith (F Int ~ b)) True []
323 React with (F Int ~ b) ==> IR Stop True [] -- after substituting we re-canonicalize and get nothing
326 -- Main interaction solver: we fully solve the worklist 'in one go',
327 -- returning an extended inert set.
329 -- See Note [Touchables and givens].
330 solveInteractGiven :: InertSet -> GivenLoc -> [EvVar] -> TcS InertSet
331 solveInteractGiven inert gloc evs
332 = do { (_, inert_ret) <- solveInteract inert $ listToBag $
336 flav = Given gloc GivenOrig
337 mk_given ev = mkEvVarX ev flav
339 solveInteractWanted :: InertSet -> [WantedEvVar] -> TcS InertSet
340 solveInteractWanted inert wvs
341 = do { (_,inert_ret) <- solveInteract inert $ listToBag $
342 map wantedToFlavored wvs
345 solveInteract :: InertSet -> Bag FlavoredEvVar -> TcS (Bool, InertSet)
346 -- Post: (True, inert_set) means we managed to discharge all constraints
347 -- without actually doing any interactions!
348 -- (False, inert_set) means some interactions occurred
349 solveInteract inert ws
350 = do { dyn_flags <- getDynFlags
351 ; sctx <- getTcSContext
353 ; traceTcS "solveInteract, before clever canonicalization:" $
354 vcat [ text "ws = " <+> ppr (mapBag (\(EvVarX ev ct)
355 -> (ct,evVarPred ev)) ws)
356 , text "inert = " <+> ppr inert ]
358 ; can_ws <- mkCanonicalFEVs ws
361 <- foldrWorkListM (tryPreSolveAndInteract sctx dyn_flags) (True,inert) can_ws
363 ; traceTcS "solveInteract, after clever canonicalization (and interaction):" $
364 vcat [ text "No interaction happened = " <+> ppr flag
365 , text "inert_ret = " <+> ppr inert_ret ]
367 ; return (flag, inert_ret) }
369 tryPreSolveAndInteract :: SimplContext
373 -> TcS (Bool, InertSet)
374 -- Returns: True if it was able to discharge this constraint AND all previous ones
375 tryPreSolveAndInteract sctx dyn_flags ct (all_previous_discharged, inert)
376 = do { let inert_cts = get_inert_cts (evVarPred ev_var)
378 ; this_one_discharged <-
379 if isCFrozenErr ct then
382 dischargeFromCCans inert_cts ev_var fl
384 ; if this_one_discharged
385 then return (all_previous_discharged, inert)
388 { inert_ret <- solveOneWithDepth (ctxtStkDepth dyn_flags,0,[]) ct inert
389 ; return (False, inert_ret) } }
395 get_inert_cts (ClassP clas _)
396 | simplEqsOnly sctx = emptyCCan
397 | otherwise = fst (getRelevantCts clas (inert_dicts inert))
398 get_inert_cts (IParam {})
399 = emptyCCan -- We must not do the same thing for IParams, because (contrary
400 -- to dictionaries), work items /must/ override inert items.
401 -- See Note [Overriding implicit parameters] in TcInteract.
402 get_inert_cts (EqPred {})
403 = inert_eqs inert `unionBags` cCanMapToBag (inert_funeqs inert)
405 dischargeFromCCans :: CanonicalCts -> EvVar -> CtFlavor -> TcS Bool
406 -- See if this (pre-canonicalised) work-item is identical to a
407 -- one already in the inert set. Reasons:
408 -- a) Avoid creating superclass constraints for millions of incoming (Num a) constraints
409 -- b) Termination for improve_eqs in TcSimplify.simpl_loop
410 dischargeFromCCans cans ev fl
411 = Bag.foldrBag discharge_ct (return False) cans
413 the_pred = evVarPred ev
415 discharge_ct :: CanonicalCt -> TcS Bool -> TcS Bool
416 discharge_ct ct _rest
417 | evVarPred (cc_id ct) `eqPred` the_pred
418 , cc_flavor ct `canSolve` fl
419 = do { when (isWanted fl) $ setEvBind ev (evVarTerm (cc_id ct))
420 -- Deriveds need no evidence
421 -- For Givens, we already have evidence, and we don't need it twice
424 discharge_ct _ct rest = rest
427 Note [Avoiding the superclass explosion]
428 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
429 This note now is not as significant as it used to be because we no
430 longer add the superclasses of Wanted as Derived, except only if they
431 have equality superclasses or superclasses with functional
432 dependencies. The fear was that hundreds of identical wanteds would
433 give rise each to the same superclass or equality Derived's which
434 would lead to a blo-up in the number of interactions.
436 Instead, what we do with tryPreSolveAndCanon, is when we encounter a
437 new constraint, we very quickly see if it can be immediately
438 discharged by a class constraint in our inert set or the previous
439 canonicals. If so, we add nothing to the returned canonical
443 solveOne :: WorkItem -> InertSet -> TcS InertSet
444 solveOne workItem inerts
445 = do { dyn_flags <- getDynFlags
446 ; solveOneWithDepth (ctxtStkDepth dyn_flags,0,[]) workItem inerts
450 solveInteractWithDepth :: (Int, Int, [WorkItem])
451 -> WorkList -> InertSet -> TcS InertSet
452 solveInteractWithDepth ctxt@(max_depth,n,stack) ws inert
457 = solverDepthErrorTcS n stack
460 = do { traceTcS "solveInteractWithDepth" $
461 vcat [ text "Current depth =" <+> ppr n
462 , text "Max depth =" <+> ppr max_depth
463 , text "ws =" <+> ppr ws ]
466 ; foldrWorkListM (solveOneWithDepth ctxt) inert ws }
467 -- use foldr to preserve the order
470 -- Fully interact the given work item with an inert set, and return a
471 -- new inert set which has assimilated the new information.
472 solveOneWithDepth :: (Int, Int, [WorkItem])
473 -> WorkItem -> InertSet -> TcS InertSet
474 solveOneWithDepth (max_depth, depth, stack) work inert
475 = do { traceFireTcS depth (text "Solving {" <+> ppr work)
476 ; (new_inert, new_work) <- runSolverPipeline depth thePipeline inert work
478 -- Recursively solve the new work generated
479 -- from workItem, with a greater depth
480 ; res_inert <- solveInteractWithDepth (max_depth, depth+1, work:stack) new_work new_inert
482 ; traceFireTcS depth (text "Done }" <+> ppr work)
486 thePipeline :: [(String,SimplifierStage)]
487 thePipeline = [ ("interact with inert eqs", interactWithInertEqsStage)
488 , ("interact with inerts", interactWithInertsStage)
489 , ("spontaneous solve", spontaneousSolveStage)
490 , ("top-level reactions", topReactionsStage) ]
493 *********************************************************************************
495 The spontaneous-solve Stage
497 *********************************************************************************
499 Note [Efficient Orientation]
500 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
502 There are two cases where we have to be careful about
503 orienting equalities to get better efficiency.
505 Case 1: In Rewriting Equalities (function rewriteEqLHS)
507 When rewriting two equalities with the same LHS:
510 We have a choice of producing work (xi1 ~ xi2) (up-to the
511 canonicalization invariants) However, to prevent the inert items
512 from getting kicked out of the inerts first, we prefer to
513 canonicalize (xi1 ~ xi2) if (b) comes from the inert set, or (xi2
514 ~ xi1) if (a) comes from the inert set.
516 This choice is implemented using the WhichComesFromInert flag.
518 Case 2: Functional Dependencies
519 Again, we should prefer, if possible, the inert variables on the RHS
521 Case 3: IP improvement work
522 We must always rewrite so that the inert type is on the right.
525 spontaneousSolveStage :: SimplifierStage
526 spontaneousSolveStage depth workItem inerts
527 = do { mSolve <- trySpontaneousSolve workItem
530 SPCantSolve -> -- No spontaneous solution for him, keep going
531 return $ SR { sr_new_work = emptyWorkList
533 , sr_stop = ContinueWith workItem }
536 | not (isGivenOrSolvedCt workItem)
537 -- Original was wanted or derived but we have now made him
538 -- given so we have to interact him with the inerts due to
539 -- its status change. This in turn may produce more work.
540 -- We do this *right now* (rather than just putting workItem'
541 -- back into the work-list) because we've solved
542 -> do { bumpStepCountTcS
543 ; traceFireTcS depth (ptext (sLit "Spontaneous (w/d)") <+> ppr workItem)
544 ; (new_inert, new_work) <- runSolverPipeline depth
545 [ ("recursive interact with inert eqs", interactWithInertEqsStage)
546 , ("recursive interact with inerts", interactWithInertsStage)
548 ; return $ SR { sr_new_work = new_work
549 , sr_inerts = new_inert -- will include workItem'
553 -> -- Original was given; he must then be inert all right, and
554 -- workList' are all givens from flattening
555 do { bumpStepCountTcS
556 ; traceFireTcS depth (ptext (sLit "Spontaneous (g)") <+> ppr workItem)
557 ; return $ SR { sr_new_work = emptyWorkList
558 , sr_inerts = inerts `updInertSet` workItem'
560 SPError -> -- Return with no new work
561 return $ SR { sr_new_work = emptyWorkList
566 data SPSolveResult = SPCantSolve | SPSolved WorkItem | SPError
567 -- SPCantSolve means that we can't do the unification because e.g. the variable is untouchable
568 -- SPSolved workItem' gives us a new *given* to go on
569 -- SPError means that it's completely impossible to solve this equality, eg due to a kind error
572 -- @trySpontaneousSolve wi@ solves equalities where one side is a
573 -- touchable unification variable.
574 -- See Note [Touchables and givens]
575 trySpontaneousSolve :: WorkItem -> TcS SPSolveResult
576 trySpontaneousSolve workItem@(CTyEqCan { cc_id = cv, cc_flavor = gw, cc_tyvar = tv1, cc_rhs = xi })
579 | Just tv2 <- tcGetTyVar_maybe xi
580 = do { tch1 <- isTouchableMetaTyVar tv1
581 ; tch2 <- isTouchableMetaTyVar tv2
582 ; case (tch1, tch2) of
583 (True, True) -> trySpontaneousEqTwoWay cv gw tv1 tv2
584 (True, False) -> trySpontaneousEqOneWay cv gw tv1 xi
585 (False, True) -> trySpontaneousEqOneWay cv gw tv2 (mkTyVarTy tv1)
586 _ -> return SPCantSolve }
588 = do { tch1 <- isTouchableMetaTyVar tv1
589 ; if tch1 then trySpontaneousEqOneWay cv gw tv1 xi
590 else do { traceTcS "Untouchable LHS, can't spontaneously solve workitem:"
592 ; return SPCantSolve }
596 -- trySpontaneousSolve (CFunEqCan ...) = ...
597 -- See Note [No touchables as FunEq RHS] in TcSMonad
598 trySpontaneousSolve _ = return SPCantSolve
601 trySpontaneousEqOneWay :: CoVar -> CtFlavor -> TcTyVar -> Xi -> TcS SPSolveResult
602 -- tv is a MetaTyVar, not untouchable
603 trySpontaneousEqOneWay cv gw tv xi
604 | not (isSigTyVar tv) || isTyVarTy xi
605 = do { let kxi = typeKind xi -- NB: 'xi' is fully rewritten according to the inerts
606 -- so we have its more specific kind in our hands
607 ; if kxi `isSubKind` tyVarKind tv then
608 solveWithIdentity cv gw tv xi
609 else return SPCantSolve
611 else if tyVarKind tv `isSubKind` kxi then
612 return SPCantSolve -- kinds are compatible but we can't solveWithIdentity this way
613 -- This case covers the a_touchable :: * ~ b_untouchable :: ??
614 -- which has to be deferred or floated out for someone else to solve
615 -- it in a scope where 'b' is no longer untouchable.
616 else do { addErrorTcS KindError gw (mkTyVarTy tv) xi -- See Note [Kind errors]
620 | otherwise -- Still can't solve, sig tyvar and non-variable rhs
624 trySpontaneousEqTwoWay :: CoVar -> CtFlavor -> TcTyVar -> TcTyVar -> TcS SPSolveResult
625 -- Both tyvars are *touchable* MetaTyvars so there is only a chance for kind error here
626 trySpontaneousEqTwoWay cv gw tv1 tv2
628 , nicer_to_update_tv2 = solveWithIdentity cv gw tv2 (mkTyVarTy tv1)
630 = solveWithIdentity cv gw tv1 (mkTyVarTy tv2)
631 | otherwise -- None is a subkind of the other, but they are both touchable!
633 -- do { addErrorTcS KindError gw (mkTyVarTy tv1) (mkTyVarTy tv2)
634 -- ; return SPError }
638 nicer_to_update_tv2 = isSigTyVar tv1 || isSystemName (Var.varName tv2)
642 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
643 Consider the wanted problem:
644 alpha ~ (# Int, Int #)
645 where alpha :: ?? and (# Int, Int #) :: (#). We can't spontaneously solve this constraint,
646 but we should rather reject the program that give rise to it. If 'trySpontaneousEqTwoWay'
647 simply returns @CantSolve@ then that wanted constraint is going to propagate all the way and
648 get quantified over in inference mode. That's bad because we do know at this point that the
649 constraint is insoluble. Instead, we call 'recKindErrorTcS' here, which will fail later on.
651 The same applies in canonicalization code in case of kind errors in the givens.
653 However, when we canonicalize givens we only check for compatibility (@compatKind@).
654 If there were a kind error in the givens, this means some form of inconsistency or dead code.
656 You may think that when we spontaneously solve wanteds we may have to look through the
657 bindings to determine the right kind of the RHS type. E.g one may be worried that xi is
658 @alpha@ where alpha :: ? and a previous spontaneous solving has set (alpha := f) with (f :: *).
659 But we orient our constraints so that spontaneously solved ones can rewrite all other constraint
660 so this situation can't happen.
662 Note [Spontaneous solving and kind compatibility]
663 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
664 Note that our canonical constraints insist that *all* equalities (tv ~
665 xi) or (F xis ~ rhs) require the LHS and the RHS to have *compatible*
666 the same kinds. ("compatible" means one is a subKind of the other.)
668 - It can't be *equal* kinds, because
669 b) wanted constraints don't necessarily have identical kinds
671 b) a solved wanted constraint becomes a given
673 - SPJ thinks that *given* constraints (tv ~ tau) always have that
674 tau has a sub-kind of tv; and when solving wanted constraints
675 in trySpontaneousEqTwoWay we re-orient to achieve this.
677 - Note that the kind invariant is maintained by rewriting.
678 Eg wanted1 rewrites wanted2; if both were compatible kinds before,
679 wanted2 will be afterwards. Similarly givens.
682 - Givens from higher-rank, such as:
683 type family T b :: * -> * -> *
684 type instance T Bool = (->)
686 f :: forall a. ((T a ~ (->)) => ...) -> a -> ...
688 Whereas we would be able to apply the type instance, we would not be able to
689 use the given (T Bool ~ (->)) in the body of 'flop'
692 Note [Avoid double unifications]
693 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
694 The spontaneous solver has to return a given which mentions the unified unification
695 variable *on the left* of the equality. Here is what happens if not:
696 Original wanted: (a ~ alpha), (alpha ~ Int)
697 We spontaneously solve the first wanted, without changing the order!
698 given : a ~ alpha [having unified alpha := a]
699 Now the second wanted comes along, but he cannot rewrite the given, so we simply continue.
700 At the end we spontaneously solve that guy, *reunifying* [alpha := Int]
702 We avoid this problem by orienting the resulting given so that the unification
703 variable is on the left. [Note that alternatively we could attempt to
704 enforce this at canonicalization]
706 See also Note [No touchables as FunEq RHS] in TcSMonad; avoiding
707 double unifications is the main reason we disallow touchable
708 unification variables as RHS of type family equations: F xis ~ alpha.
713 solveWithIdentity :: CoVar -> CtFlavor -> TcTyVar -> Xi -> TcS SPSolveResult
714 -- Solve with the identity coercion
715 -- Precondition: kind(xi) is a sub-kind of kind(tv)
716 -- Precondition: CtFlavor is Wanted or Derived
717 -- See [New Wanted Superclass Work] to see why solveWithIdentity
718 -- must work for Derived as well as Wanted
719 -- Returns: workItem where
720 -- workItem = the new Given constraint
721 solveWithIdentity cv wd tv xi
722 = do { traceTcS "Sneaky unification:" $
723 vcat [text "Coercion variable: " <+> ppr wd,
724 text "Coercion: " <+> pprEq (mkTyVarTy tv) xi,
725 text "Left Kind is : " <+> ppr (typeKind (mkTyVarTy tv)),
726 text "Right Kind is : " <+> ppr (typeKind xi)
729 ; setWantedTyBind tv xi
730 ; let refl_xi = mkReflCo xi
731 ; cv_given <- newGivenCoVar (mkTyVarTy tv) xi refl_xi
733 ; when (isWanted wd) (setCoBind cv refl_xi)
734 -- We don't want to do this for Derived, that's why we use 'when (isWanted wd)'
735 ; return $ SPSolved (CTyEqCan { cc_id = cv_given
736 , cc_flavor = mkSolvedFlavor wd UnkSkol
737 , cc_tyvar = tv, cc_rhs = xi }) }
741 *********************************************************************************
743 The interact-with-inert Stage
745 *********************************************************************************
747 Note [The Solver Invariant]
748 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
749 We always add Givens first. So you might think that the solver has
752 If the work-item is Given,
753 then the inert item must Given
755 But this isn't quite true. Suppose we have,
756 c1: [W] beta ~ [alpha], c2 : [W] blah, c3 :[W] alpha ~ Int
757 After processing the first two, we get
758 c1: [G] beta ~ [alpha], c2 : [W] blah
759 Now, c3 does not interact with the the given c1, so when we spontaneously
760 solve c3, we must re-react it with the inert set. So we can attempt a
761 reaction between inert c2 [W] and work-item c3 [G].
763 It *is* true that [Solver Invariant]
764 If the work-item is Given,
765 AND there is a reaction
766 then the inert item must Given
768 If the work-item is Given,
769 and the inert item is Wanted/Derived
770 then there is no reaction
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_fire :: Maybe String -- Tells whether a rule fired, and if so what
792 -- What to do with the inert reactant.
793 data InertAction = KeepInert | DropInert
795 mkIRContinue :: String -> WorkItem -> InertAction -> WorkList -> TcS InteractResult
796 mkIRContinue rule wi keep newWork
797 = return $ IR { ir_stop = ContinueWith wi, ir_inert_action = keep
798 , ir_new_work = newWork, ir_fire = Just rule }
800 mkIRStopK :: String -> WorkList -> TcS InteractResult
801 mkIRStopK rule newWork
802 = return $ IR { ir_stop = Stop, ir_inert_action = KeepInert
803 , ir_new_work = newWork, ir_fire = Just rule }
805 mkIRStopD :: String -> WorkList -> TcS InteractResult
806 mkIRStopD rule newWork
807 = return $ IR { ir_stop = Stop, ir_inert_action = DropInert
808 , ir_new_work = newWork, ir_fire = Just rule }
810 noInteraction :: Monad m => WorkItem -> m InteractResult
812 = return $ IR { ir_stop = ContinueWith wi, ir_inert_action = KeepInert
813 , ir_new_work = emptyWorkList, ir_fire = Nothing }
815 data WhichComesFromInert = LeftComesFromInert | RightComesFromInert
816 -- See Note [Efficient Orientation]
819 ---------------------------------------------------
820 -- Interact a single WorkItem with the equalities of an inert set as
821 -- far as possible, i.e. until we get a Stop result from an individual
822 -- reaction (i.e. when the WorkItem is consumed), or until we've
823 -- interact the WorkItem with the entire equalities of the InertSet
825 interactWithInertEqsStage :: SimplifierStage
826 interactWithInertEqsStage depth workItem inert
827 = Bag.foldrBagM (interactNext depth) initITR (inert_eqs inert)
828 -- use foldr to preserve the order
830 initITR = SR { sr_inerts = inert { inert_eqs = emptyCCan }
831 , sr_new_work = emptyWorkList
832 , 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 depth 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.foldrBagM (interactNext depth) initITR relevant
847 -- use foldr to preserve the order
849 getISRelevant :: CanonicalCt -> InertSet -> (CanonicalCts, InertSet)
850 getISRelevant (CFrozenErr {}) is = (emptyCCan, is)
851 -- Nothing s relevant; we have alread interacted
852 -- it with the equalities in the inert set
854 getISRelevant (CDictCan { cc_class = cls } ) is
855 = let (relevant, residual_map) = getRelevantCts cls (inert_dicts is)
856 in (relevant, is { inert_dicts = residual_map })
857 getISRelevant (CFunEqCan { cc_fun = tc } ) is
858 = let (relevant, residual_map) = getRelevantCts tc (inert_funeqs is)
859 in (relevant, is { inert_funeqs = residual_map })
860 getISRelevant (CIPCan { cc_ip_nm = nm }) is
861 = let (relevant, residual_map) = getRelevantCts nm (inert_ips is)
862 in (relevant, is { inert_ips = residual_map })
863 -- An equality, finally, may kick everything except equalities out
864 -- because we have already interacted the equalities in interactWithInertEqsStage
865 getISRelevant _eq_ct is -- Equality, everything is relevant for this one
866 -- TODO: if we were caching variables, we'd know that only
867 -- some are relevant. Experiment with this for now.
868 = let cts = cCanMapToBag (inert_ips is) `unionBags`
869 cCanMapToBag (inert_dicts is) `unionBags` cCanMapToBag (inert_funeqs is)
870 in (cts, is { inert_dicts = emptyCCanMap
871 , inert_ips = emptyCCanMap
872 , inert_funeqs = emptyCCanMap })
874 interactNext :: SubGoalDepth -> AtomicInert -> StageResult -> TcS StageResult
875 interactNext depth inert it
876 | ContinueWith work_item <- sr_stop it
877 = do { let inerts = sr_inerts it
879 ; IR { ir_new_work = new_work, ir_inert_action = inert_action
880 , ir_fire = fire_info, ir_stop = stop }
881 <- interactWithInert inert work_item
884 = text rule <+> keep_doc
885 <+> vcat [ ptext (sLit "Inert =") <+> ppr inert
886 , ptext (sLit "Work =") <+> ppr work_item
887 , ppUnless (isEmptyWorkList new_work) $
888 ptext (sLit "New =") <+> ppr new_work ]
889 keep_doc = case inert_action of
890 KeepInert -> ptext (sLit "[keep]")
891 DropInert -> ptext (sLit "[drop]")
893 Just rule -> do { bumpStepCountTcS
894 ; traceFireTcS depth (mk_msg rule) }
897 -- New inerts depend on whether we KeepInert or not
898 ; let inerts_new = case inert_action of
899 KeepInert -> inerts `updInertSet` inert
902 ; return $ SR { sr_inerts = inerts_new
903 , sr_new_work = sr_new_work it `unionWorkList` new_work
906 = return $ it { sr_inerts = (sr_inerts it) `updInertSet` inert }
908 -- Do a single interaction of two constraints.
909 interactWithInert :: AtomicInert -> WorkItem -> TcS InteractResult
910 interactWithInert inert workItem
911 = do { ctxt <- getTcSContext
912 ; let is_allowed = allowedInteraction (simplEqsOnly ctxt) inert workItem
915 doInteractWithInert inert workItem
917 noInteraction workItem
920 allowedInteraction :: Bool -> AtomicInert -> WorkItem -> Bool
921 -- Allowed interactions
922 allowedInteraction eqs_only (CDictCan {}) (CDictCan {}) = not eqs_only
923 allowedInteraction eqs_only (CIPCan {}) (CIPCan {}) = not eqs_only
924 allowedInteraction _ _ _ = True
926 --------------------------------------------
927 doInteractWithInert :: CanonicalCt -> CanonicalCt -> TcS InteractResult
928 -- Identical class constraints.
931 inertItem@(CDictCan { cc_id = d1, cc_flavor = fl1, cc_class = cls1, cc_tyargs = tys1 })
932 workItem@(CDictCan { cc_id = d2, cc_flavor = fl2, cc_class = cls2, cc_tyargs = tys2 })
935 = do { let pty1 = ClassP cls1 tys1
936 pty2 = ClassP cls2 tys2
937 inert_pred_loc = (pty1, pprFlavorArising fl1)
938 work_item_pred_loc = (pty2, pprFlavorArising fl2)
941 <- if isGivenOrSolved fl1 && isGivenOrSolved fl2 then return Nothing
942 -- NB: We don't create fds for given (and even solved), have not seen a useful
943 -- situation for these and even if we did we'd have to be very careful to only
944 -- create Derived's and not Wanteds.
946 else let fd_eqns = improveFromAnother inert_pred_loc work_item_pred_loc
947 wloc = get_workitem_wloc fl2
948 in rewriteWithFunDeps fd_eqns tys2 wloc
949 -- See Note [Efficient Orientation], [When improvement happens]
951 ; case any_fundeps of
952 -- No Functional Dependencies
954 | eqTypes tys1 tys2 -> solveOneFromTheOther "Cls/Cls" (EvId d1,fl1) workItem
955 | otherwise -> noInteraction workItem
957 -- Actual Functional Dependencies
958 Just (rewritten_tys2,cos2,fd_work)
959 | not (eqTypes tys1 rewritten_tys2)
960 -- Standard thing: create derived fds and keep on going. Importantly we don't
961 -- throw workitem back in the worklist because this can cause loops. See #5236.
962 -> do { fd_cans <- mkCanonicalFDAsDerived fd_work
963 ; mkIRContinue "Cls/Cls fundep (not solved)" workItem KeepInert fd_cans }
965 -- This WHOLE otherwise branch is an optimization where the fd made the things match
967 , let dict_co = mkTyConAppCo (classTyCon cls1) cos2
970 -> pprPanic "Unexpected given!" (ppr inertItem $$ ppr workItem)
971 -- The only way to have created a fundep is if the inert was
972 -- wanted or derived, in which case the workitem can't be given!
974 -- The types were made to exactly match so we don't need
975 -- the workitem any longer.
976 -> do { fd_cans <- mkCanonicalFDAsDerived fd_work
977 -- No rewriting really, so let's create deriveds fds
978 ; mkIRStopK "Cls/Cls fundep (solved)" fd_cans }
981 -> do { setDictBind d2 (EvCast d1 dict_co)
982 ; let inert_w = inertItem { cc_flavor = fl2 }
983 -- A bit naughty: we take the inert Derived,
984 -- turn it into a Wanted, use it to solve the work-item
985 -- and put it back into the work-list
986 -- Maybe rather than starting again, we could keep going
987 -- with the rewritten workitem, having dropped the inert, but its
990 -- Also: we have rewriting so lets create wanted fds
991 ; fd_cans <- mkCanonicalFDAsWanted fd_work
992 ; mkIRStopD "Cls/Cls fundep (solved)" $
993 workListFromNonEq inert_w `unionWorkList` fd_cans }
995 -> do { setDictBind d2 (EvCast d1 dict_co)
996 -- Rewriting is happening, so we have to create wanted fds
997 ; fd_cans <- mkCanonicalFDAsWanted fd_work
998 ; mkIRStopK "Cls/Cls fundep (solved)" fd_cans }
1000 where get_workitem_wloc (Wanted wl) = wl
1001 get_workitem_wloc (Derived wl) = wl
1002 get_workitem_wloc (Given {}) = panic "Unexpected given!"
1005 -- Class constraint and given equality: use the equality to rewrite
1006 -- the class constraint.
1007 doInteractWithInert (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi })
1008 (CDictCan { cc_id = dv, cc_flavor = wfl, cc_class = cl, cc_tyargs = xis })
1009 | ifl `canRewrite` wfl
1010 , tv `elemVarSet` tyVarsOfTypes xis
1011 = do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,wfl,cl,xis)
1012 -- Continue with rewritten Dictionary because we can only be in the
1013 -- interactWithEqsStage, so the dictionary is inert.
1014 ; mkIRContinue "Eq/Cls" rewritten_dict KeepInert emptyWorkList }
1016 doInteractWithInert (CDictCan { cc_id = dv, cc_flavor = ifl, cc_class = cl, cc_tyargs = xis })
1017 workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
1018 | wfl `canRewrite` ifl
1019 , tv `elemVarSet` tyVarsOfTypes xis
1020 = do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,ifl,cl,xis)
1021 ; mkIRContinue "Cls/Eq" workItem DropInert (workListFromNonEq rewritten_dict) }
1023 -- Class constraint and given equality: use the equality to rewrite
1024 -- the class constraint.
1025 doInteractWithInert (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi })
1026 (CIPCan { cc_id = ipid, cc_flavor = wfl, cc_ip_nm = nm, cc_ip_ty = ty })
1027 | ifl `canRewrite` wfl
1028 , tv `elemVarSet` tyVarsOfType ty
1029 = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,wfl,nm,ty)
1030 ; mkIRContinue "Eq/IP" rewritten_ip KeepInert emptyWorkList }
1032 doInteractWithInert (CIPCan { cc_id = ipid, cc_flavor = ifl, cc_ip_nm = nm, cc_ip_ty = ty })
1033 workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
1034 | wfl `canRewrite` ifl
1035 , tv `elemVarSet` tyVarsOfType ty
1036 = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,ifl,nm,ty)
1037 ; mkIRContinue "IP/Eq" workItem DropInert (workListFromNonEq rewritten_ip) }
1039 -- Two implicit parameter constraints. If the names are the same,
1040 -- but their types are not, we generate a wanted type equality
1041 -- that equates the type (this is "improvement").
1042 -- However, we don't actually need the coercion evidence,
1043 -- so we just generate a fresh coercion variable that isn't used anywhere.
1044 doInteractWithInert (CIPCan { cc_id = id1, cc_flavor = ifl, cc_ip_nm = nm1, cc_ip_ty = ty1 })
1045 workItem@(CIPCan { cc_flavor = wfl, cc_ip_nm = nm2, cc_ip_ty = ty2 })
1046 | nm1 == nm2 && isGivenOrSolved wfl && isGivenOrSolved ifl
1047 = -- See Note [Overriding implicit parameters]
1048 -- Dump the inert item, override totally with the new one
1049 -- Do not require type equality
1050 -- For example, given let ?x::Int = 3 in let ?x::Bool = True in ...
1051 -- we must *override* the outer one with the inner one
1052 mkIRContinue "IP/IP override" workItem DropInert emptyWorkList
1054 | nm1 == nm2 && ty1 `eqType` ty2
1055 = solveOneFromTheOther "IP/IP" (EvId id1,ifl) workItem
1058 = -- See Note [When improvement happens]
1059 do { co_var <- newCoVar ty2 ty1 -- See Note [Efficient Orientation]
1060 ; let flav = Wanted (combineCtLoc ifl wfl)
1061 ; cans <- mkCanonical flav co_var
1063 Given {} -> pprPanic "Unexpected given IP" (ppr workItem)
1064 Derived {} -> pprPanic "Unexpected derived IP" (ppr workItem)
1066 do { setIPBind (cc_id workItem) $
1067 EvCast id1 (mkSymCo (mkCoVarCo co_var))
1068 ; mkIRStopK "IP/IP interaction (solved)" cans }
1071 -- Never rewrite a given with a wanted equality, and a type function
1072 -- equality can never rewrite an equality. We rewrite LHS *and* RHS
1073 -- of function equalities so that our inert set exposes everything that
1074 -- we know about equalities.
1076 -- Inert: equality, work item: function equality
1077 doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi1 })
1078 (CFunEqCan { cc_id = cv2, cc_flavor = wfl, cc_fun = tc
1079 , cc_tyargs = args, cc_rhs = xi2 })
1080 | ifl `canRewrite` wfl
1081 , tv `elemVarSet` tyVarsOfTypes (xi2:args) -- Rewrite RHS as well
1082 = do { rewritten_funeq <- rewriteFunEq (cv1,tv,xi1) (cv2,wfl,tc,args,xi2)
1083 ; mkIRStopK "Eq/FunEq" (workListFromEq rewritten_funeq) }
1084 -- Must Stop here, because we may no longer be inert after the rewritting.
1086 -- Inert: function equality, work item: equality
1087 doInteractWithInert (CFunEqCan {cc_id = cv1, cc_flavor = ifl, cc_fun = tc
1088 , cc_tyargs = args, cc_rhs = xi1 })
1089 workItem@(CTyEqCan { cc_id = cv2, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi2 })
1090 | wfl `canRewrite` ifl
1091 , tv `elemVarSet` tyVarsOfTypes (xi1:args) -- Rewrite RHS as well
1092 = do { rewritten_funeq <- rewriteFunEq (cv2,tv,xi2) (cv1,ifl,tc,args,xi1)
1093 ; mkIRContinue "FunEq/Eq" workItem DropInert (workListFromEq rewritten_funeq) }
1094 -- One may think that we could (KeepTransformedInert rewritten_funeq)
1095 -- but that is wrong, because it may end up not being inert with respect
1096 -- to future inerts. Example:
1097 -- Original inert = { F xis ~ [a], b ~ Maybe Int }
1098 -- Work item comes along = a ~ [b]
1099 -- If we keep { F xis ~ [b] } in the inert set we will end up with:
1100 -- { F xis ~ [b], b ~ Maybe Int, a ~ [Maybe Int] }
1101 -- At the end, which is *not* inert. So we should unfortunately DropInert here.
1103 doInteractWithInert (CFunEqCan { cc_id = cv1, cc_flavor = fl1, cc_fun = tc1
1104 , cc_tyargs = args1, cc_rhs = xi1 })
1105 workItem@(CFunEqCan { cc_id = cv2, cc_flavor = fl2, cc_fun = tc2
1106 , cc_tyargs = args2, cc_rhs = xi2 })
1107 | tc1 == tc2 && and (zipWith eqType args1 args2)
1108 , Just GivenSolved <- isGiven_maybe fl1
1109 = mkIRContinue "Funeq/Funeq" workItem DropInert emptyWorkList
1110 | tc1 == tc2 && and (zipWith eqType args1 args2)
1111 , Just GivenSolved <- isGiven_maybe fl2
1112 = mkIRStopK "Funeq/Funeq" emptyWorkList
1114 | fl1 `canSolve` fl2 && lhss_match
1115 = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCo cv1,xi1) (cv2,fl2,xi2)
1116 ; mkIRStopK "FunEq/FunEq" cans }
1117 | fl2 `canSolve` fl1 && lhss_match
1118 = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCo cv2,xi2) (cv1,fl1,xi1)
1119 ; mkIRContinue "FunEq/FunEq" workItem DropInert cans }
1121 lhss_match = tc1 == tc2 && eqTypes args1 args2
1123 doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
1124 workItem@(CTyEqCan { cc_id = cv2, cc_flavor = fl2, cc_tyvar = tv2, cc_rhs = xi2 })
1125 -- Check for matching LHS
1126 | fl1 `canSolve` fl2 && tv1 == tv2
1127 = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCo cv1,xi1) (cv2,fl2,xi2)
1128 ; mkIRStopK "Eq/Eq lhs" cans }
1130 | fl2 `canSolve` fl1 && tv1 == tv2
1131 = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCo cv2,xi2) (cv1,fl1,xi1)
1132 ; mkIRContinue "Eq/Eq lhs" workItem DropInert cans }
1134 -- Check for rewriting RHS
1135 | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfType xi2
1136 = do { rewritten_eq <- rewriteEqRHS (cv1,tv1,xi1) (cv2,fl2,tv2,xi2)
1137 ; mkIRStopK "Eq/Eq rhs" rewritten_eq }
1139 | fl2 `canRewrite` fl1 && tv2 `elemVarSet` tyVarsOfType xi1
1140 = do { rewritten_eq <- rewriteEqRHS (cv2,tv2,xi2) (cv1,fl1,tv1,xi1)
1141 ; mkIRContinue "Eq/Eq rhs" workItem DropInert rewritten_eq }
1143 doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
1144 (CFrozenErr { cc_id = cv2, cc_flavor = fl2 })
1145 | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfEvVar cv2
1146 = do { rewritten_frozen <- rewriteFrozen (cv1, tv1, xi1) (cv2, fl2)
1147 ; mkIRStopK "Frozen/Eq" rewritten_frozen }
1149 doInteractWithInert (CFrozenErr { cc_id = cv2, cc_flavor = fl2 })
1150 workItem@(CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
1151 | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfEvVar cv2
1152 = do { rewritten_frozen <- rewriteFrozen (cv1, tv1, xi1) (cv2, fl2)
1153 ; mkIRContinue "Frozen/Eq" workItem DropInert rewritten_frozen }
1155 -- Fall-through case for all other situations
1156 doInteractWithInert _ workItem = noInteraction workItem
1158 -------------------------
1159 -- Equational Rewriting
1160 rewriteDict :: (CoVar, TcTyVar, Xi) -> (DictId, CtFlavor, Class, [Xi]) -> TcS CanonicalCt
1161 rewriteDict (cv,tv,xi) (dv,gw,cl,xis)
1162 = do { let cos = map (liftCoSubstWith [tv] [mkCoVarCo cv]) xis -- xis[tv] ~ xis[xi]
1163 args = substTysWith [tv] [xi] xis
1165 dict_co = mkTyConAppCo con cos
1166 ; dv' <- newDictVar cl args
1168 Wanted {} -> setDictBind dv (EvCast dv' (mkSymCo dict_co))
1169 Given {} -> setDictBind dv' (EvCast dv dict_co)
1170 Derived {} -> return () -- Derived dicts we don't set any evidence
1172 ; return (CDictCan { cc_id = dv'
1175 , cc_tyargs = args }) }
1177 rewriteIP :: (CoVar,TcTyVar,Xi) -> (EvVar,CtFlavor, IPName Name, TcType) -> TcS CanonicalCt
1178 rewriteIP (cv,tv,xi) (ipid,gw,nm,ty)
1179 = do { let ip_co = liftCoSubstWith [tv] [mkCoVarCo cv] ty -- ty[tv] ~ t[xi]
1180 ty' = substTyWith [tv] [xi] ty
1181 ; ipid' <- newIPVar nm ty'
1183 Wanted {} -> setIPBind ipid (EvCast ipid' (mkSymCo ip_co))
1184 Given {} -> setIPBind ipid' (EvCast ipid ip_co)
1185 Derived {} -> return () -- Derived ips: we don't set any evidence
1187 ; return (CIPCan { cc_id = ipid'
1190 , cc_ip_ty = ty' }) }
1192 rewriteFunEq :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TyCon, [Xi], Xi) -> TcS CanonicalCt
1193 rewriteFunEq (cv1,tv,xi1) (cv2,gw, tc,args,xi2) -- cv2 :: F args ~ xi2
1194 = do { let co_subst = liftCoSubstWith [tv] [mkCoVarCo cv1]
1195 arg_cos = map co_subst args
1196 args' = substTysWith [tv] [xi1] args
1197 fun_co = mkTyConAppCo tc arg_cos -- fun_co :: F args ~ F args'
1199 xi2' = substTyWith [tv] [xi1] xi2
1200 xi2_co = co_subst xi2 -- xi2_co :: xi2 ~ xi2'
1202 ; cv2' <- newCoVar (mkTyConApp tc args') xi2'
1204 Wanted {} -> setCoBind cv2 (fun_co `mkTransCo`
1205 mkCoVarCo cv2' `mkTransCo`
1207 Given {} -> setCoBind cv2' (mkSymCo fun_co `mkTransCo`
1208 mkCoVarCo cv2 `mkTransCo`
1210 Derived {} -> return ()
1212 ; return (CFunEqCan { cc_id = cv2'
1216 , cc_rhs = xi2' }) }
1219 rewriteEqRHS :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TcTyVar,Xi) -> TcS WorkList
1220 -- Use the first equality to rewrite the second, flavors already checked.
1221 -- E.g. c1 : tv1 ~ xi1 c2 : tv2 ~ xi2
1222 -- rewrites c2 to give
1223 -- c2' : tv2 ~ xi2[xi1/tv1]
1224 -- We must do an occurs check to sure the new constraint is canonical
1225 -- So we might return an empty bag
1226 rewriteEqRHS (cv1,tv1,xi1) (cv2,gw,tv2,xi2)
1227 | Just tv2' <- tcGetTyVar_maybe xi2'
1228 , tv2 == tv2' -- In this case xi2[xi1/tv1] = tv2, so we have tv2~tv2
1229 = do { when (isWanted gw) (setCoBind cv2 (mkSymCo co2'))
1230 ; return emptyWorkList }
1232 = do { cv2' <- newCoVar (mkTyVarTy tv2) xi2'
1234 Wanted {} -> setCoBind cv2 $ mkCoVarCo cv2' `mkTransCo`
1236 Given {} -> setCoBind cv2' $ mkCoVarCo cv2 `mkTransCo`
1238 Derived {} -> return ()
1239 ; canEqToWorkList gw cv2' (mkTyVarTy tv2) xi2' }
1241 xi2' = substTyWith [tv1] [xi1] xi2
1242 co2' = liftCoSubstWith [tv1] [mkCoVarCo cv1] xi2 -- xi2 ~ xi2[xi1/tv1]
1244 rewriteEqLHS :: WhichComesFromInert -> (Coercion,Xi) -> (CoVar,CtFlavor,Xi) -> TcS WorkList
1245 -- Used to ineract two equalities of the following form:
1246 -- First Equality: co1: (XXX ~ xi1)
1247 -- Second Equality: cv2: (XXX ~ xi2)
1248 -- Where the cv1 `canRewrite` cv2 equality
1249 -- We have an option of creating new work (xi1 ~ xi2) OR (xi2 ~ xi1),
1250 -- See Note [Efficient Orientation] for that
1251 rewriteEqLHS LeftComesFromInert (co1,xi1) (cv2,gw,xi2)
1252 = do { cv2' <- newCoVar xi2 xi1
1254 Wanted {} -> setCoBind cv2 $
1255 co1 `mkTransCo` mkSymCo (mkCoVarCo cv2')
1256 Given {} -> setCoBind cv2' $
1257 mkSymCo (mkCoVarCo cv2) `mkTransCo` co1
1258 Derived {} -> return ()
1259 ; mkCanonical gw cv2' }
1261 rewriteEqLHS RightComesFromInert (co1,xi1) (cv2,gw,xi2)
1262 = do { cv2' <- newCoVar xi1 xi2
1264 Wanted {} -> setCoBind cv2 $
1265 co1 `mkTransCo` mkCoVarCo cv2'
1266 Given {} -> setCoBind cv2' $
1267 mkSymCo co1 `mkTransCo` mkCoVarCo cv2
1268 Derived {} -> return ()
1269 ; mkCanonical gw cv2' }
1271 rewriteFrozen :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor) -> TcS WorkList
1272 rewriteFrozen (cv1, tv1, xi1) (cv2, fl2)
1273 = do { cv2' <- newCoVar ty2a' ty2b' -- ty2a[xi1/tv1] ~ ty2b[xi1/tv1]
1275 Wanted {} -> setCoBind cv2 $ co2a' `mkTransCo`
1276 mkCoVarCo cv2' `mkTransCo`
1279 Given {} -> setCoBind cv2' $ mkSymCo co2a' `mkTransCo`
1280 mkCoVarCo cv2 `mkTransCo`
1283 Derived {} -> return ()
1285 ; return (workListFromNonEq $ CFrozenErr { cc_id = cv2', cc_flavor = fl2 }) }
1287 (ty2a, ty2b) = coVarKind cv2 -- cv2 : ty2a ~ ty2b
1288 ty2a' = substTyWith [tv1] [xi1] ty2a
1289 ty2b' = substTyWith [tv1] [xi1] ty2b
1291 co2a' = liftCoSubstWith [tv1] [mkCoVarCo cv1] ty2a -- ty2a ~ ty2a[xi1/tv1]
1292 co2b' = liftCoSubstWith [tv1] [mkCoVarCo cv1] ty2b -- ty2b ~ ty2b[xi1/tv1]
1294 solveOneFromTheOther_ExtraWork :: String -> (EvTerm, CtFlavor)
1295 -> CanonicalCt -> WorkList -> TcS InteractResult
1296 -- First argument inert, second argument work-item. They both represent
1297 -- wanted/given/derived evidence for the *same* predicate so
1298 -- we can discharge one directly from the other.
1300 -- Precondition: value evidence only (implicit parameters, classes)
1302 solveOneFromTheOther_ExtraWork info (ev_term,ifl) workItem extra_work
1304 = mkIRStopK ("Solved[DW] " ++ info) extra_work
1306 | isDerived ifl -- The inert item is Derived, we can just throw it away,
1307 -- The workItem is inert wrt earlier inert-set items,
1308 -- so it's safe to continue on from this point
1309 = mkIRContinue ("Solved[DI] " ++ info) workItem DropInert extra_work
1311 | Just GivenSolved <- isGiven_maybe ifl, isGivenOrSolved wfl
1312 -- Same if the inert is a GivenSolved -- just get rid of it
1313 = mkIRContinue ("Solved[SI] " ++ info) workItem DropInert extra_work
1316 = ASSERT( ifl `canSolve` wfl )
1317 -- Because of Note [The Solver Invariant], plus Derived dealt with
1318 do { when (isWanted wfl) $ setEvBind wid ev_term
1319 -- Overwrite the binding, if one exists
1320 -- If both are Given, we already have evidence; no need to duplicate
1321 ; mkIRStopK ("Solved " ++ info) extra_work }
1323 wfl = cc_flavor workItem
1324 wid = cc_id workItem
1327 solveOneFromTheOther :: String -> (EvTerm, CtFlavor) -> CanonicalCt -> TcS InteractResult
1328 solveOneFromTheOther str evfl ct
1329 = solveOneFromTheOther_ExtraWork str evfl ct emptyWorkList -- extra work is empty
1333 Note [Superclasses and recursive dictionaries]
1334 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1335 Overlaps with Note [SUPERCLASS-LOOP 1]
1336 Note [SUPERCLASS-LOOP 2]
1337 Note [Recursive instances and superclases]
1338 ToDo: check overlap and delete redundant stuff
1340 Right before adding a given into the inert set, we must
1341 produce some more work, that will bring the superclasses
1342 of the given into scope. The superclass constraints go into
1345 When we simplify a wanted constraint, if we first see a matching
1346 instance, we may produce new wanted work. To (1) avoid doing this work
1347 twice in the future and (2) to handle recursive dictionaries we may ``cache''
1348 this item as given into our inert set WITHOUT adding its superclass constraints,
1349 otherwise we'd be in danger of creating a loop [In fact this was the exact reason
1350 for doing the isGoodRecEv check in an older version of the type checker].
1352 But now we have added partially solved constraints to the worklist which may
1353 interact with other wanteds. Consider the example:
1357 class Eq b => Foo a b --- 0-th selector
1358 instance Eq a => Foo [a] a --- fooDFun
1360 and wanted (Foo [t] t). We are first going to see that the instance matches
1361 and create an inert set that includes the solved (Foo [t] t) but not its superclasses:
1362 d1 :_g Foo [t] t d1 := EvDFunApp fooDFun d3
1363 Our work list is going to contain a new *wanted* goal
1366 Ok, so how do we get recursive dictionaries, at all:
1370 data D r = ZeroD | SuccD (r (D r));
1372 instance (Eq (r (D r))) => Eq (D r) where
1373 ZeroD == ZeroD = True
1374 (SuccD a) == (SuccD b) = a == b
1377 equalDC :: D [] -> D [] -> Bool;
1380 We need to prove (Eq (D [])). Here's how we go:
1384 by instance decl, holds if
1388 *BUT* we have an inert set which gives us (no superclasses):
1390 By the instance declaration of Eq we can show the 'd2' goal if
1392 where d2 = dfEqList d3
1394 Now, however this wanted can interact with our inert d1 to set:
1396 and solve the goal. Why was this interaction OK? Because, if we chase the
1397 evidence of d1 ~~> dfEqD d2 ~~-> dfEqList d3, so by setting d3 := d1 we
1399 d3 := dfEqD2 (dfEqList d3)
1400 which is FINE because the use of d3 is protected by the instance function
1403 So, our strategy is to try to put solved wanted dictionaries into the
1404 inert set along with their superclasses (when this is meaningful,
1405 i.e. when new wanted goals are generated) but solve a wanted dictionary
1406 from a given only in the case where the evidence variable of the
1407 wanted is mentioned in the evidence of the given (recursively through
1408 the evidence binds) in a protected way: more instance function applications
1409 than superclass selectors.
1411 Here are some more examples from GHC's previous type checker
1415 This code arises in the context of "Scrap Your Boilerplate with Class"
1419 instance Sat (ctx Char) => Data ctx Char -- dfunData1
1420 instance (Sat (ctx [a]), Data ctx a) => Data ctx [a] -- dfunData2
1422 class Data Maybe a => Foo a
1424 instance Foo t => Sat (Maybe t) -- dfunSat
1426 instance Data Maybe a => Foo a -- dfunFoo1
1427 instance Foo a => Foo [a] -- dfunFoo2
1428 instance Foo [Char] -- dfunFoo3
1430 Consider generating the superclasses of the instance declaration
1431 instance Foo a => Foo [a]
1433 So our problem is this
1435 d1 :_w Data Maybe [t]
1437 We may add the given in the inert set, along with its superclasses
1438 [assuming we don't fail because there is a matching instance, see
1439 tryTopReact, given case ]
1443 d01 :_g Data Maybe t -- d2 := EvDictSuperClass d0 0
1444 d1 :_w Data Maybe [t]
1445 Then d2 can readily enter the inert, and we also do solving of the wanted
1448 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1450 d2 :_w Sat (Maybe [t])
1452 d01 :_g Data Maybe t
1453 Now, we may simplify d2 more:
1456 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1457 d1 :_g Data Maybe [t]
1458 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1462 d01 :_g Data Maybe t
1464 Now, we can just solve d3.
1467 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1468 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1471 d01 :_g Data Maybe t
1472 And now we can simplify d4 again, but since it has superclasses we *add* them to the worklist:
1475 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1476 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1477 d4 :_g Foo [t] d4 := dfunFoo2 d5
1480 d6 :_g Data Maybe [t] d6 := EvDictSuperClass d4 0
1481 d01 :_g Data Maybe t
1482 Now, d5 can be solved! (and its superclass enter scope)
1485 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1486 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1487 d4 :_g Foo [t] d4 := dfunFoo2 d5
1488 d5 :_g Foo t d5 := dfunFoo1 d7
1491 d6 :_g Data Maybe [t]
1492 d8 :_g Data Maybe t d8 := EvDictSuperClass d5 0
1493 d01 :_g Data Maybe t
1496 [1] Suppose we pick d8 and we react him with d01. Which of the two givens should
1497 we keep? Well, we *MUST NOT* drop d01 because d8 contains recursive evidence
1498 that must not be used (look at case interactInert where both inert and workitem
1499 are givens). So we have several options:
1500 - Drop the workitem always (this will drop d8)
1501 This feels very unsafe -- what if the work item was the "good" one
1502 that should be used later to solve another wanted?
1503 - Don't drop anyone: the inert set may contain multiple givens!
1504 [This is currently implemented]
1506 The "don't drop anyone" seems the most safe thing to do, so now we come to problem 2:
1507 [2] We have added both d6 and d01 in the inert set, and we are interacting our wanted
1508 d7. Now the [isRecDictEv] function in the ineration solver
1509 [case inert-given workitem-wanted] will prevent us from interacting d7 := d8
1510 precisely because chasing the evidence of d8 leads us to an unguarded use of d7.
1512 So, no interaction happens there. Then we meet d01 and there is no recursion
1513 problem there [isRectDictEv] gives us the OK to interact and we do solve d7 := d01!
1515 Note [SUPERCLASS-LOOP 1]
1516 ~~~~~~~~~~~~~~~~~~~~~~~~
1517 We have to be very, very careful when generating superclasses, lest we
1518 accidentally build a loop. Here's an example:
1522 class S a => C a where { opc :: a -> a }
1523 class S b => D b where { opd :: b -> b }
1525 instance C Int where
1528 instance D Int where
1531 From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int}
1532 Simplifying, we may well get:
1533 $dfCInt = :C ds1 (opd dd)
1536 Notice that we spot that we can extract ds1 from dd.
1538 Alas! Alack! We can do the same for (instance D Int):
1540 $dfDInt = :D ds2 (opc dc)
1544 And now we've defined the superclass in terms of itself.
1545 Two more nasty cases are in
1550 - Satisfy the superclass context *all by itself*
1551 (tcSimplifySuperClasses)
1552 - And do so completely; i.e. no left-over constraints
1553 to mix with the constraints arising from method declarations
1556 Note [SUPERCLASS-LOOP 2]
1557 ~~~~~~~~~~~~~~~~~~~~~~~~
1558 We need to be careful when adding "the constaint we are trying to prove".
1559 Suppose we are *given* d1:Ord a, and want to deduce (d2:C [a]) where
1561 class Ord a => C a where
1562 instance Ord [a] => C [a] where ...
1564 Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the
1565 superclasses of C [a] to avails. But we must not overwrite the binding
1566 for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
1569 Here's another variant, immortalised in tcrun020
1570 class Monad m => C1 m
1571 class C1 m => C2 m x
1572 instance C2 Maybe Bool
1573 For the instance decl we need to build (C1 Maybe), and it's no good if
1574 we run around and add (C2 Maybe Bool) and its superclasses to the avails
1575 before we search for C1 Maybe.
1577 Here's another example
1578 class Eq b => Foo a b
1579 instance Eq a => Foo [a] a
1583 we'll first deduce that it holds (via the instance decl). We must not
1584 then overwrite the Eq t constraint with a superclass selection!
1586 At first I had a gross hack, whereby I simply did not add superclass constraints
1587 in addWanted, though I did for addGiven and addIrred. This was sub-optimal,
1588 becuase it lost legitimate superclass sharing, and it still didn't do the job:
1589 I found a very obscure program (now tcrun021) in which improvement meant the
1590 simplifier got two bites a the cherry... so something seemed to be an Stop
1591 first time, but reducible next time.
1593 Now we implement the Right Solution, which is to check for loops directly
1594 when adding superclasses. It's a bit like the occurs check in unification.
1596 Note [Recursive instances and superclases]
1597 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1598 Consider this code, which arises in the context of "Scrap Your
1599 Boilerplate with Class".
1603 instance Sat (ctx Char) => Data ctx Char
1604 instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]
1606 class Data Maybe a => Foo a
1608 instance Foo t => Sat (Maybe t)
1610 instance Data Maybe a => Foo a
1611 instance Foo a => Foo [a]
1614 In the instance for Foo [a], when generating evidence for the superclasses
1615 (ie in tcSimplifySuperClasses) we need a superclass (Data Maybe [a]).
1616 Using the instance for Data, we therefore need
1617 (Sat (Maybe [a], Data Maybe a)
1618 But we are given (Foo a), and hence its superclass (Data Maybe a).
1619 So that leaves (Sat (Maybe [a])). Using the instance for Sat means
1620 we need (Foo [a]). And that is the very dictionary we are bulding
1621 an instance for! So we must put that in the "givens". So in this
1623 Given: Foo a, Foo [a]
1624 Wanted: Data Maybe [a]
1626 BUT we must *not not not* put the *superclasses* of (Foo [a]) in
1627 the givens, which is what 'addGiven' would normally do. Why? Because
1628 (Data Maybe [a]) is the superclass, so we'd "satisfy" the wanted
1629 by selecting a superclass from Foo [a], which simply makes a loop.
1631 On the other hand we *must* put the superclasses of (Foo a) in
1632 the givens, as you can see from the derivation described above.
1634 Conclusion: in the very special case of tcSimplifySuperClasses
1635 we have one 'given' (namely the "this" dictionary) whose superclasses
1636 must not be added to 'givens' by addGiven.
1638 There is a complication though. Suppose there are equalities
1639 instance (Eq a, a~b) => Num (a,b)
1640 Then we normalise the 'givens' wrt the equalities, so the original
1641 given "this" dictionary is cast to one of a different type. So it's a
1642 bit trickier than before to identify the "special" dictionary whose
1643 superclasses must not be added. See test
1644 indexed-types/should_run/EqInInstance
1646 We need a persistent property of the dictionary to record this
1647 special-ness. Current I'm using the InstLocOrigin (a bit of a hack,
1648 but cool), which is maintained by dictionary normalisation.
1649 Specifically, the InstLocOrigin is
1651 then the no-superclass thing kicks in. WATCH OUT if you fiddle
1654 Note [MATCHING-SYNONYMS]
1655 ~~~~~~~~~~~~~~~~~~~~~~~~
1656 When trying to match a dictionary (D tau) to a top-level instance, or a
1657 type family equation (F taus_1 ~ tau_2) to a top-level family instance,
1658 we do *not* need to expand type synonyms because the matcher will do that for us.
1661 Note [RHS-FAMILY-SYNONYMS]
1662 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1663 The RHS of a family instance is represented as yet another constructor which is
1664 like a type synonym for the real RHS the programmer declared. Eg:
1665 type instance F (a,a) = [a]
1667 :R32 a = [a] -- internal type synonym introduced
1668 F (a,a) ~ :R32 a -- instance
1670 When we react a family instance with a type family equation in the work list
1671 we keep the synonym-using RHS without expansion.
1674 *********************************************************************************
1676 The top-reaction Stage
1678 *********************************************************************************
1681 -- If a work item has any form of interaction with top-level we get this
1682 data TopInteractResult
1683 = NoTopInt -- No top-level interaction
1684 -- Equivalent to (SomeTopInt emptyWorkList (ContinueWith work_item))
1686 { tir_new_work :: WorkList -- Sub-goals or new work (could be given,
1687 -- for superclasses)
1688 , tir_new_inert :: StopOrContinue -- The input work item, ready to become *inert* now:
1689 } -- NB: in ``given'' (solved) form if the
1690 -- original was wanted or given and instance match
1691 -- was found, but may also be in wanted form if we
1692 -- only reacted with functional dependencies
1693 -- arising from top-level instances.
1695 topReactionsStage :: SimplifierStage
1696 topReactionsStage depth workItem inerts
1697 = do { tir <- tryTopReact inerts workItem
1698 -- NB: we pass the inerts as well. See Note [Instance and Given overlap]
1701 return $ SR { sr_inerts = inerts
1702 , sr_new_work = emptyWorkList
1703 , sr_stop = ContinueWith workItem }
1704 SomeTopInt tir_new_work tir_new_inert ->
1705 do { bumpStepCountTcS
1706 ; traceFireTcS depth (ptext (sLit "Top react")
1707 <+> vcat [ ptext (sLit "Work =") <+> ppr workItem
1708 , ptext (sLit "New =") <+> ppr tir_new_work ])
1709 ; return $ SR { sr_inerts = inerts
1710 , sr_new_work = tir_new_work
1711 , sr_stop = tir_new_inert
1715 tryTopReact :: InertSet -> WorkItem -> TcS TopInteractResult
1716 tryTopReact inerts workitem
1717 = do { -- A flag controls the amount of interaction allowed
1718 -- See Note [Simplifying RULE lhs constraints]
1719 ctxt <- getTcSContext
1720 ; if allowedTopReaction (simplEqsOnly ctxt) workitem
1721 then do { traceTcS "tryTopReact / calling doTopReact" (ppr workitem)
1722 ; doTopReact inerts workitem }
1723 else return NoTopInt
1726 allowedTopReaction :: Bool -> WorkItem -> Bool
1727 allowedTopReaction eqs_only (CDictCan {}) = not eqs_only
1728 allowedTopReaction _ _ = True
1730 doTopReact :: InertSet -> WorkItem -> TcS TopInteractResult
1731 -- The work item does not react with the inert set, so try interaction with top-level instances
1732 -- NB: The place to add superclasses in *not* in doTopReact stage. Instead superclasses are
1733 -- added in the worklist as part of the canonicalisation process.
1734 -- See Note [Adding superclasses] in TcCanonical.
1737 -- See Note [Given constraint that matches an instance declaration]
1738 doTopReact _inerts (CDictCan { cc_flavor = Given {} })
1739 = return NoTopInt -- NB: Superclasses already added since it's canonical
1741 -- Derived dictionary: just look for functional dependencies
1742 doTopReact _inerts workItem@(CDictCan { cc_flavor = Derived loc
1743 , cc_class = cls, cc_tyargs = xis })
1744 = do { instEnvs <- getInstEnvs
1745 ; let fd_eqns = improveFromInstEnv instEnvs
1746 (ClassP cls xis, pprArisingAt loc)
1747 ; m <- rewriteWithFunDeps fd_eqns xis loc
1749 Nothing -> return NoTopInt
1750 Just (xis',_,fd_work) ->
1751 let workItem' = workItem { cc_tyargs = xis' }
1752 -- Deriveds are not supposed to have identity (cc_id is unused!)
1753 in do { fd_cans <- mkCanonicalFDAsDerived fd_work
1754 ; return $ SomeTopInt { tir_new_work = fd_cans
1755 , tir_new_inert = ContinueWith workItem' }
1760 -- Wanted dictionary
1761 doTopReact inerts workItem@(CDictCan { cc_flavor = fl@(Wanted loc)
1762 , cc_class = cls, cc_tyargs = xis })
1763 -- See Note [MATCHING-SYNONYMS]
1764 = do { traceTcS "doTopReact" (ppr workItem)
1765 ; instEnvs <- getInstEnvs
1766 ; let fd_eqns = improveFromInstEnv instEnvs $ (ClassP cls xis, pprArisingAt loc)
1768 ; any_fundeps <- rewriteWithFunDeps fd_eqns xis loc
1769 ; case any_fundeps of
1770 -- No Functional Dependencies
1772 do { lkup_inst_res <- matchClassInst inerts cls xis loc
1773 ; case lkup_inst_res of
1774 GenInst wtvs ev_term
1775 -> doSolveFromInstance wtvs ev_term workItem emptyWorkList
1779 -- Actual Functional Dependencies
1780 Just (xis',cos,fd_work) ->
1781 do { lkup_inst_res <- matchClassInst inerts cls xis' loc
1782 ; case lkup_inst_res of
1784 -> do { fd_cans <- mkCanonicalFDAsDerived fd_work
1786 SomeTopInt { tir_new_work = fd_cans
1787 , tir_new_inert = ContinueWith workItem } }
1788 -- This WHOLE branch is an optimization: we can immediately discharge the dictionary
1789 GenInst wtvs ev_term
1790 -> do { let dict_co = mkTyConAppCo (classTyCon cls) cos
1791 ; fd_cans <- mkCanonicalFDAsWanted fd_work
1792 ; dv' <- newDictVar cls xis'
1793 ; setDictBind dv' ev_term
1794 ; doSolveFromInstance wtvs (EvCast dv' dict_co) workItem fd_cans }
1797 where doSolveFromInstance :: [WantedEvVar]
1800 -> WorkList -> TcS TopInteractResult
1801 -- Precondition: evidence term matches the predicate of cc_id of workItem
1802 doSolveFromInstance wtvs ev_term workItem extra_work
1804 = do { traceTcS "doTopReact/found nullary instance for" (ppr (cc_id workItem))
1805 ; setDictBind (cc_id workItem) ev_term
1806 ; return $ SomeTopInt { tir_new_work = extra_work
1807 , tir_new_inert = Stop } }
1809 = do { traceTcS "doTopReact/found non-nullary instance for" (ppr (cc_id workItem))
1810 ; setDictBind (cc_id workItem) ev_term
1811 -- Solved and new wanted work produced, you may cache the
1812 -- (tentatively solved) dictionary as Solved given.
1813 ; let solved = workItem { cc_flavor = solved_fl }
1814 solved_fl = mkSolvedFlavor fl UnkSkol
1815 ; inst_work <- canWanteds wtvs
1816 ; return $ SomeTopInt { tir_new_work = inst_work `unionWorkList` extra_work
1817 , tir_new_inert = ContinueWith solved } }
1821 doTopReact _inerts (CFunEqCan { cc_flavor = fl })
1822 | Just GivenSolved <- isGiven_maybe fl
1823 = return NoTopInt -- If Solved, no more interactions should happen
1825 -- Otherwise, it's a Given, Derived, or Wanted
1826 doTopReact _inerts workItem@(CFunEqCan { cc_id = cv, cc_flavor = fl
1827 , cc_fun = tc, cc_tyargs = args, cc_rhs = xi })
1828 = ASSERT (isSynFamilyTyCon tc) -- No associated data families have reached that far
1829 do { match_res <- matchFam tc args -- See Note [MATCHING-SYNONYMS]
1831 MatchInstNo -> return NoTopInt
1832 MatchInstSingle (rep_tc, rep_tys)
1833 -> do { let Just coe_tc = tyConFamilyCoercion_maybe rep_tc
1834 Just rhs_ty = tcView (mkTyConApp rep_tc rep_tys)
1835 -- Eagerly expand away the type synonym on the
1836 -- RHS of a type function, so that it never
1837 -- appears in an error message
1838 -- See Note [Type synonym families] in TyCon
1839 coe = mkAxInstCo coe_tc rep_tys
1841 Wanted {} -> do { cv' <- newCoVar rhs_ty xi
1842 ; setCoBind cv $ coe `mkTransCo` mkCoVarCo cv'
1843 ; can_cts <- mkCanonical fl cv'
1844 ; let solved = workItem { cc_flavor = solved_fl }
1845 solved_fl = mkSolvedFlavor fl UnkSkol
1846 ; if isEmptyWorkList can_cts then
1847 return (SomeTopInt can_cts Stop) -- No point in caching
1849 SomeTopInt { tir_new_work = can_cts
1850 , tir_new_inert = ContinueWith solved }
1852 Given {} -> do { cv' <- newGivenCoVar xi rhs_ty $
1853 mkSymCo (mkCoVarCo cv) `mkTransCo` coe
1854 ; can_cts <- mkCanonical fl cv'
1856 SomeTopInt { tir_new_work = can_cts
1857 , tir_new_inert = Stop }
1859 Derived {} -> do { cv' <- newDerivedId (EqPred xi rhs_ty)
1860 ; can_cts <- mkCanonical fl cv'
1862 SomeTopInt { tir_new_work = can_cts
1863 , tir_new_inert = Stop }
1867 -> panicTcS $ text "TcSMonad.matchFam returned multiple instances!"
1871 -- Any other work item does not react with any top-level equations
1872 doTopReact _inerts _workItem = return NoTopInt
1876 Note [FunDep and implicit parameter reactions]
1877 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1878 Currently, our story of interacting two dictionaries (or a dictionary
1879 and top-level instances) for functional dependencies, and implicit
1880 paramters, is that we simply produce new wanted equalities. So for example
1882 class D a b | a -> b where ...
1888 We generate the extra work item
1890 where 'cv' is currently unused. However, this new item reacts with d2,
1891 discharging it in favour of a new constraint d2' thus:
1893 d2 := d2' |> D Int cv
1894 Now d2' can be discharged from d1
1896 We could be more aggressive and try to *immediately* solve the dictionary
1897 using those extra equalities. With the same inert set and work item we
1898 might dischard d2 directly:
1901 d2 := d1 |> D Int cv
1903 But in general it's a bit painful to figure out the necessary coercion,
1904 so we just take the first approach. Here is a better example. Consider:
1905 class C a b c | a -> b
1907 [Given] d1 : C T Int Char
1908 [Wanted] d2 : C T beta Int
1909 In this case, it's *not even possible* to solve the wanted immediately.
1910 So we should simply output the functional dependency and add this guy
1911 [but NOT its superclasses] back in the worklist. Even worse:
1912 [Given] d1 : C T Int beta
1913 [Wanted] d2: C T beta Int
1914 Then it is solvable, but its very hard to detect this on the spot.
1916 It's exactly the same with implicit parameters, except that the
1917 "aggressive" approach would be much easier to implement.
1919 Note [When improvement happens]
1920 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1921 We fire an improvement rule when
1923 * Two constraints match (modulo the fundep)
1924 e.g. C t1 t2, C t1 t3 where C a b | a->b
1925 The two match because the first arg is identical
1927 * At least one is not Given. If they are both given, we don't fire
1928 the reaction because we have no way of constructing evidence for a
1929 new equality nor does it seem right to create a new wanted goal
1930 (because the goal will most likely contain untouchables, which
1931 can't be solved anyway)!
1933 Note that we *do* fire the improvement if one is Given and one is Derived.
1934 The latter can be a superclass of a wanted goal. Example (tcfail138)
1935 class L a b | a -> b
1936 class (G a, L a b) => C a b
1938 instance C a b' => G (Maybe a)
1939 instance C a b => C (Maybe a) a
1940 instance L (Maybe a) a
1942 When solving the superclasses of the (C (Maybe a) a) instance, we get
1943 Given: C a b ... and hance by superclasses, (G a, L a b)
1945 Use the instance decl to get
1947 The (C a b') is inert, so we generate its Derived superclasses (L a b'),
1948 and now we need improvement between that derived superclass an the Given (L a b)
1950 Note [Overriding implicit parameters]
1951 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1953 f :: (?x::a) -> Bool -> a
1955 g v = let ?x::Int = 3
1956 in (f v, let ?x::Bool = True in f v)
1958 This should probably be well typed, with
1959 g :: Bool -> (Int, Bool)
1961 So the inner binding for ?x::Bool *overrides* the outer one.
1962 Hence a work-item Given overrides an inert-item Given.
1964 Note [Given constraint that matches an instance declaration]
1965 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1966 What should we do when we discover that one (or more) top-level
1967 instances match a given (or solved) class constraint? We have
1970 1. Reject the program. The reason is that there may not be a unique
1971 best strategy for the solver. Example, from the OutsideIn(X) paper:
1972 instance P x => Q [x]
1973 instance (x ~ y) => R [x] y
1975 wob :: forall a b. (Q [b], R b a) => a -> Int
1977 g :: forall a. Q [a] => [a] -> Int
1980 will generate the impliation constraint:
1981 Q [a] => (Q [beta], R beta [a])
1982 If we react (Q [beta]) with its top-level axiom, we end up with a
1983 (P beta), which we have no way of discharging. On the other hand,
1984 if we react R beta [a] with the top-level we get (beta ~ a), which
1985 is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
1986 now solvable by the given Q [a].
1988 However, this option is restrictive, for instance [Example 3] from
1989 Note [Recursive dictionaries] will fail to work.
1991 2. Ignore the problem, hoping that the situations where there exist indeed
1992 such multiple strategies are rare: Indeed the cause of the previous
1993 problem is that (R [x] y) yields the new work (x ~ y) which can be
1994 *spontaneously* solved, not using the givens.
1996 We are choosing option 2 below but we might consider having a flag as well.
1999 Note [New Wanted Superclass Work]
2000 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2001 Even in the case of wanted constraints, we may add some superclasses
2002 as new given work. The reason is:
2004 To allow FD-like improvement for type families. Assume that
2006 class C a b | a -> b
2007 and we have to solve the implication constraint:
2009 Then, FD improvement can help us to produce a new wanted (beta ~ b)
2011 We want to have the same effect with the type family encoding of
2012 functional dependencies. Namely, consider:
2013 class (F a ~ b) => C a b
2014 Now suppose that we have:
2017 By interacting the given we will get given (F a ~ b) which is not
2018 enough by itself to make us discharge (C a beta). However, we
2019 may create a new derived equality from the super-class of the
2020 wanted constraint (C a beta), namely derived (F a ~ beta).
2021 Now we may interact this with given (F a ~ b) to get:
2023 But 'beta' is a touchable unification variable, and hence OK to
2024 unify it with 'b', replacing the derived evidence with the identity.
2026 This requires trySpontaneousSolve to solve *derived*
2027 equalities that have a touchable in their RHS, *in addition*
2028 to solving wanted equalities.
2030 We also need to somehow use the superclasses to quantify over a minimal,
2031 constraint see note [Minimize by Superclasses] in TcSimplify.
2034 Finally, here is another example where this is useful.
2038 class (F a ~ b) => C a b
2039 And we are given the wanteds:
2043 We surely do *not* want to quantify over (b ~ c), since if someone provides
2044 dictionaries for (C a b) and (C a c), these dictionaries can provide a proof
2045 of (b ~ c), hence no extra evidence is necessary. Here is what will happen:
2047 Step 1: We will get new *given* superclass work,
2048 provisionally to our solving of w1 and w2
2050 g1: F a ~ b, g2 : F a ~ c,
2051 w1 : C a b, w2 : C a c, w3 : b ~ c
2053 The evidence for g1 and g2 is a superclass evidence term:
2055 g1 := sc w1, g2 := sc w2
2057 Step 2: The givens will solve the wanted w3, so that
2058 w3 := sym (sc w1) ; sc w2
2060 Step 3: Now, one may naively assume that then w2 can be solve from w1
2061 after rewriting with the (now solved equality) (b ~ c).
2063 But this rewriting is ruled out by the isGoodRectDict!
2065 Conclusion, we will (correctly) end up with the unsolved goals
2068 NB: The desugarer needs be more clever to deal with equalities
2069 that participate in recursive dictionary bindings.
2072 data LookupInstResult
2074 | GenInst [WantedEvVar] EvTerm
2076 matchClassInst :: InertSet -> Class -> [Type] -> WantedLoc -> TcS LookupInstResult
2077 matchClassInst inerts clas tys loc
2078 = do { let pred = mkClassPred clas tys
2079 ; mb_result <- matchClass clas tys
2080 ; untch <- getUntouchables
2082 MatchInstNo -> return NoInstance
2083 MatchInstMany -> return NoInstance -- defer any reactions of a multitude until
2084 -- we learn more about the reagent
2085 MatchInstSingle (_,_)
2086 | given_overlap untch ->
2087 do { traceTcS "Delaying instance application" $
2088 vcat [ text "Workitem=" <+> pprPredTy (ClassP clas tys)
2089 , text "Silents and their superclasses=" <+> ppr silents_and_their_scs
2090 , text "All given dictionaries=" <+> ppr all_given_dicts ]
2091 ; return NoInstance -- see Note [Instance and Given overlap]
2094 MatchInstSingle (dfun_id, mb_inst_tys) ->
2095 do { checkWellStagedDFun pred dfun_id loc
2097 -- It's possible that not all the tyvars are in
2098 -- the substitution, tenv. For example:
2099 -- instance C X a => D X where ...
2100 -- (presumably there's a functional dependency in class C)
2101 -- Hence mb_inst_tys :: Either TyVar TcType
2103 ; tys <- instDFunTypes mb_inst_tys
2104 ; let (theta, _) = tcSplitPhiTy (applyTys (idType dfun_id) tys)
2105 ; if null theta then
2106 return (GenInst [] (EvDFunApp dfun_id tys []))
2108 { ev_vars <- instDFunConstraints theta
2109 ; let wevs = [EvVarX w loc | w <- ev_vars]
2110 ; return $ GenInst wevs (EvDFunApp dfun_id tys ev_vars) }
2113 where given_overlap :: TcsUntouchables -> Bool
2115 = foldlBag (\r d -> r || matchable untch d) False all_given_dicts
2117 matchable untch (CDictCan { cc_class = clas', cc_tyargs = sys, cc_flavor = fl })
2118 | Just GivenOrig <- isGiven_maybe fl
2120 , does_not_originate_in_a_silent clas' sys
2121 = case tcUnifyTys (\tv -> if isTouchableMetaTyVar_InRange untch tv &&
2122 tv `elemVarSet` tyVarsOfTypes tys
2123 then BindMe else Skolem) tys sys of
2124 -- We can't learn anything more about any variable at this point, so the only
2125 -- cause of overlap can be by an instantiation of a touchable unification
2126 -- variable. Hence we only bind touchable unification variables. In addition,
2127 -- we use tcUnifyTys instead of tcMatchTys to rule out cyclic substitutions.
2130 | otherwise = False -- No overlap with a solved, already been taken care of
2131 -- by the overlap check with the instance environment.
2132 matchable _tys ct = pprPanic "Expecting dictionary!" (ppr ct)
2134 does_not_originate_in_a_silent clas sys
2135 -- UGLY: See Note [Silent parameters overlapping]
2136 = null $ filter (eqPred (ClassP clas sys)) silents_and_their_scs
2138 silents_and_their_scs
2139 = foldlBag (\acc rvnt -> case rvnt of
2140 CDictCan { cc_id = d, cc_class = c, cc_tyargs = s }
2141 | isSilentEvVar d -> (ClassP c s) : (transSuperClasses c s) ++ acc
2142 _ -> acc) [] all_given_dicts
2145 -- When silent parameters will go away we should simply select from
2146 -- the given map of the inert set.
2147 all_given_dicts = Map.fold unionBags emptyCCan (cts_given $ inert_dicts inerts)
2151 Note [Silent parameters overlapping]
2152 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2154 The long-term goal is to completely remove silent superclass
2155 parameters when checking instance declarations. But until then we must
2156 make sure that we never prevent the application of an instance
2157 declaration because of a potential match from a silent parameter --
2158 after all we are supposed to have solved that silent parameter from
2159 some instance, anyway! In effect silent parameters behave more like
2160 Solved than like Given.
2162 A concrete example appears in typecheck/SilentParametersOverlapping.hs
2164 Note [Instance and Given overlap]
2165 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2166 Assume that we have an inert set that looks as follows:
2168 And an instance declaration:
2169 instance C a => D [a]
2170 A new wanted comes along of the form:
2173 One possibility is to apply the instance declaration which will leave us
2174 with an unsolvable goal (C alpha). However, later on a new constraint may
2175 arise (for instance due to a functional dependency between two later dictionaries),
2176 that will add the equality (alpha ~ Int), in which case our ([Wanted] D [alpha])
2177 will be transformed to [Wanted] D [Int], which could have been discharged by the given.
2179 The solution is that in matchClassInst and eventually in topReact, we get back with
2180 a matching instance, only when there is no Given in the inerts which is unifiable to
2181 this particular dictionary.
2183 The end effect is that, much as we do for overlapping instances, we delay choosing a
2184 class instance if there is a possibility of another instance OR a given to match our
2185 constraint later on. This fixes bugs #4981 and #5002.
2187 This is arguably not easy to appear in practice due to our aggressive prioritization
2188 of equality solving over other constraints, but it is possible. I've added a test case
2189 in typecheck/should-compile/GivenOverlapping.hs
2191 Moreover notice that our goals here are different than the goals of the top-level
2192 overlapping checks. There we are interested in validating the following principle:
2194 If we inline a function f at a site where the same global instance environment
2195 is available as the instance environment at the definition site of f then we
2196 should get the same behaviour.
2198 But for the Given Overlap check our goal is just related to completeness of