3 solveInteract, solveInteractGiven, solveInteractWanted,
4 AtomicInert, tyVarsOfInert,
5 InertSet, emptyInert, updInertSet, extractUnsolved, solveOne,
8 #include "HsVersions.h"
22 import Inst( tyVarsOfEvVar )
36 import qualified Data.Map as Map
38 import Control.Monad( when )
40 import FastString ( sLit )
44 Note [InertSet invariants]
45 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
46 An InertSet is a bag of canonical constraints, with the following invariants:
48 1 No two constraints react with each other.
50 A tricky case is when there exists a given (solved) dictionary
51 constraint and a wanted identical constraint in the inert set, but do
52 not react because reaction would create loopy dictionary evidence for
53 the wanted. See note [Recursive dictionaries]
55 2 Given equalities form an idempotent substitution [none of the
56 given LHS's occur in any of the given RHS's or reactant parts]
58 3 Wanted equalities also form an idempotent substitution
60 4 The entire set of equalities is acyclic.
62 5 Wanted dictionaries are inert with the top-level axiom set
64 6 Equalities of the form tv1 ~ tv2 always have a touchable variable
65 on the left (if possible).
67 7 No wanted constraints tv1 ~ tv2 with tv1 touchable. Such constraints
68 will be marked as solved right before being pushed into the inert set.
69 See note [Touchables and givens].
71 8 No Given constraint mentions a touchable unification variable,
74 Note that 6 and 7 are /not/ enforced by canonicalization but rather by
75 insertion in the inert list, ie by TcInteract.
77 During the process of solving, the inert set will contain some
78 previously given constraints, some wanted constraints, and some given
79 constraints which have arisen from solving wanted constraints. For
80 now we do not distinguish between given and solved constraints.
82 Note that we must switch wanted inert items to given when going under an
83 implication constraint (when in top-level inference mode).
87 data CCanMap a = CCanMap { cts_given :: Map.Map a CanonicalCts
88 -- Invariant: all Given
89 , cts_derived :: Map.Map a CanonicalCts
90 -- Invariant: all Derived
91 , cts_wanted :: Map.Map a CanonicalCts }
92 -- Invariant: all Wanted
94 cCanMapToBag :: Ord a => CCanMap a -> CanonicalCts
95 cCanMapToBag cmap = Map.fold unionBags rest_wder (cts_given cmap)
96 where rest_wder = Map.fold unionBags rest_der (cts_wanted cmap)
97 rest_der = Map.fold unionBags emptyCCan (cts_derived cmap)
99 emptyCCanMap :: CCanMap a
100 emptyCCanMap = CCanMap { cts_given = Map.empty
101 , cts_derived = Map.empty, cts_wanted = Map.empty }
103 updCCanMap:: Ord a => (a,CanonicalCt) -> CCanMap a -> CCanMap a
104 updCCanMap (a,ct) cmap
105 = case cc_flavor ct of
107 -> cmap { cts_wanted = Map.insertWith unionBags a this_ct (cts_wanted cmap) }
109 -> cmap { cts_given = Map.insertWith unionBags a this_ct (cts_given cmap) }
111 -> cmap { cts_derived = Map.insertWith unionBags a this_ct (cts_derived cmap) }
112 where this_ct = singleCCan ct
114 getRelevantCts :: Ord a => a -> CCanMap a -> (CanonicalCts, CCanMap a)
115 -- Gets the relevant constraints and returns the rest of the CCanMap
116 getRelevantCts a cmap
117 = let relevant = unionManyBags [ Map.findWithDefault emptyCCan a (cts_wanted cmap)
118 , Map.findWithDefault emptyCCan a (cts_given cmap)
119 , Map.findWithDefault emptyCCan a (cts_derived cmap) ]
120 residual_map = cmap { cts_wanted = Map.delete a (cts_wanted cmap)
121 , cts_given = Map.delete a (cts_given cmap)
122 , cts_derived = Map.delete a (cts_derived cmap) }
123 in (relevant, residual_map)
125 extractUnsolvedCMap :: Ord a => CCanMap a -> (CanonicalCts, CCanMap a)
126 -- Gets the wanted or derived constraints and returns a residual
127 -- CCanMap with only givens.
128 extractUnsolvedCMap cmap =
129 let wntd = Map.fold unionBags emptyCCan (cts_wanted cmap)
130 derd = Map.fold unionBags emptyCCan (cts_derived cmap)
131 in (wntd `unionBags` derd,
132 cmap { cts_wanted = Map.empty, cts_derived = Map.empty })
135 -- See Note [InertSet invariants]
137 = IS { inert_eqs :: CanonicalCts -- Equalities only (CTyEqCan)
138 , inert_dicts :: CCanMap Class -- Dictionaries only
139 , inert_ips :: CCanMap (IPName Name) -- Implicit parameters
140 , inert_frozen :: CanonicalCts
141 , inert_funeqs :: CCanMap TyCon -- Type family equalities only
142 -- This representation allows us to quickly get to the relevant
143 -- inert constraints when interacting a work item with the inert set.
146 tyVarsOfInert :: InertSet -> TcTyVarSet
147 tyVarsOfInert (IS { inert_eqs = eqs
148 , inert_dicts = dictmap
150 , inert_frozen = frozen
151 , inert_funeqs = funeqmap }) = tyVarsOfCanonicals cts
153 cts = eqs `andCCan` frozen `andCCan` cCanMapToBag dictmap
154 `andCCan` cCanMapToBag ipmap `andCCan` cCanMapToBag funeqmap
156 instance Outputable InertSet where
157 ppr is = vcat [ vcat (map ppr (Bag.bagToList $ inert_eqs is))
158 , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_dicts is)))
159 , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_ips is)))
160 , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_funeqs is)))
161 , vcat (map ppr (Bag.bagToList $ inert_frozen is))
164 emptyInert :: InertSet
165 emptyInert = IS { inert_eqs = Bag.emptyBag
166 , inert_frozen = Bag.emptyBag
167 , inert_dicts = emptyCCanMap
168 , inert_ips = emptyCCanMap
169 , inert_funeqs = emptyCCanMap }
171 updInertSet :: InertSet -> AtomicInert -> InertSet
173 | isCTyEqCan item -- Other equality
174 = let eqs' = inert_eqs is `Bag.snocBag` item
175 in is { inert_eqs = eqs' }
176 | Just cls <- isCDictCan_Maybe item -- Dictionary
177 = is { inert_dicts = updCCanMap (cls,item) (inert_dicts is) }
178 | Just x <- isCIPCan_Maybe item -- IP
179 = is { inert_ips = updCCanMap (x,item) (inert_ips is) }
180 | Just tc <- isCFunEqCan_Maybe item -- Function equality
181 = is { inert_funeqs = updCCanMap (tc,item) (inert_funeqs is) }
183 = is { inert_frozen = inert_frozen is `Bag.snocBag` item }
185 extractUnsolved :: InertSet -> (InertSet, CanonicalCts)
186 -- Postcondition: the returned canonical cts are either Derived, or Wanted.
187 extractUnsolved is@(IS {inert_eqs = eqs})
188 = let is_solved = is { inert_eqs = solved_eqs
189 , inert_dicts = solved_dicts
190 , inert_ips = solved_ips
191 , inert_frozen = emptyCCan
192 , inert_funeqs = solved_funeqs }
193 in (is_solved, unsolved)
195 where (unsolved_eqs, solved_eqs) = Bag.partitionBag (not.isGivenCt) eqs
196 (unsolved_ips, solved_ips) = extractUnsolvedCMap (inert_ips is)
197 (unsolved_dicts, solved_dicts) = extractUnsolvedCMap (inert_dicts is)
198 (unsolved_funeqs, solved_funeqs) = extractUnsolvedCMap (inert_funeqs is)
200 unsolved = unsolved_eqs `unionBags` inert_frozen is `unionBags`
201 unsolved_ips `unionBags` unsolved_dicts `unionBags` unsolved_funeqs
204 %*********************************************************************
206 * Main Interaction Solver *
208 **********************************************************************
212 1. Canonicalise (unary)
213 2. Pairwise interaction (binary)
214 * Take one from work list
215 * Try all pair-wise interactions with each constraint in inert
217 As an optimisation, we prioritize the equalities both in the
218 worklist and in the inerts.
220 3. Try to solve spontaneously for equalities involving touchables
221 4. Top-level interaction (binary wrt top-level)
222 Superclass decomposition belongs in (4), see note [Superclasses]
225 type AtomicInert = CanonicalCt -- constraint pulled from InertSet
226 type WorkItem = CanonicalCt -- constraint pulled from WorkList
228 -- A mixture of Given, Wanted, and Derived constraints.
229 -- We split between equalities and the rest to process equalities first.
230 type WorkList = CanonicalCts
232 unionWorkLists :: WorkList -> WorkList -> WorkList
233 unionWorkLists = andCCan
235 isEmptyWorkList :: WorkList -> Bool
236 isEmptyWorkList = isEmptyCCan
238 emptyWorkList :: WorkList
239 emptyWorkList = emptyCCan
241 workListFromCCan :: CanonicalCt -> WorkList
242 workListFromCCan = singleCCan
244 ------------------------
246 = Stop -- Work item is consumed
247 | ContinueWith WorkItem -- Not consumed
249 instance Outputable StopOrContinue where
250 ppr Stop = ptext (sLit "Stop")
251 ppr (ContinueWith w) = ptext (sLit "ContinueWith") <+> ppr w
253 -- Results after interacting a WorkItem as far as possible with an InertSet
255 = SR { sr_inerts :: InertSet
256 -- The new InertSet to use (REPLACES the old InertSet)
257 , sr_new_work :: WorkList
258 -- Any new work items generated (should be ADDED to the old WorkList)
260 -- sr_stop = Just workitem => workitem is *not* in sr_inerts and
261 -- workitem is inert wrt to sr_inerts
262 , sr_stop :: StopOrContinue
265 instance Outputable StageResult where
266 ppr (SR { sr_inerts = inerts, sr_new_work = work, sr_stop = stop })
267 = ptext (sLit "SR") <+>
268 braces (sep [ ptext (sLit "inerts =") <+> ppr inerts <> comma
269 , ptext (sLit "new work =") <+> ppr work <> comma
270 , ptext (sLit "stop =") <+> ppr stop])
272 type SubGoalDepth = Int -- Starts at zero; used to limit infinite
273 -- recursion of sub-goals
274 type SimplifierStage = SubGoalDepth -> WorkItem -> InertSet -> TcS StageResult
276 -- Combine a sequence of simplifier 'stages' to create a pipeline
277 runSolverPipeline :: SubGoalDepth
278 -> [(String, SimplifierStage)]
279 -> InertSet -> WorkItem
280 -> TcS (InertSet, WorkList)
281 -- Precondition: non-empty list of stages
282 runSolverPipeline depth pipeline inerts workItem
283 = do { traceTcS "Start solver pipeline" $
284 vcat [ ptext (sLit "work item =") <+> ppr workItem
285 , ptext (sLit "inerts =") <+> ppr inerts]
287 ; let itr_in = SR { sr_inerts = inerts
288 , sr_new_work = emptyWorkList
289 , sr_stop = ContinueWith workItem }
290 ; itr_out <- run_pipeline pipeline itr_in
292 = case sr_stop itr_out of
293 Stop -> sr_inerts itr_out
294 ContinueWith item -> sr_inerts itr_out `updInertSet` item
295 ; return (new_inert, sr_new_work itr_out) }
297 run_pipeline :: [(String, SimplifierStage)]
298 -> StageResult -> TcS StageResult
299 run_pipeline [] itr = return itr
300 run_pipeline _ itr@(SR { sr_stop = Stop }) = return itr
302 run_pipeline ((name,stage):stages)
303 (SR { sr_new_work = accum_work
305 , sr_stop = ContinueWith work_item })
306 = do { itr <- stage depth work_item inerts
307 ; traceTcS ("Stage result (" ++ name ++ ")") (ppr itr)
308 ; let itr' = itr { sr_new_work = accum_work `unionWorkLists` sr_new_work itr }
309 ; run_pipeline stages itr' }
313 Inert: {c ~ d, F a ~ t, b ~ Int, a ~ ty} (all given)
314 Reagent: a ~ [b] (given)
316 React with (c~d) ==> IR (ContinueWith (a~[b])) True []
317 React with (F a ~ t) ==> IR (ContinueWith (a~[b])) False [F [b] ~ t]
318 React with (b ~ Int) ==> IR (ContinueWith (a~[Int]) True []
321 Inert: {c ~w d, F a ~g t, b ~w Int, a ~w ty}
324 React with (c ~w d) ==> IR (ContinueWith (a~[b])) True []
325 React with (F a ~g t) ==> IR (ContinueWith (a~[b])) True [] (can't rewrite given with wanted!)
329 Inert: {a ~ Int, F Int ~ b} (given)
330 Reagent: F a ~ b (wanted)
332 React with (a ~ Int) ==> IR (ContinueWith (F Int ~ b)) True []
333 React with (F Int ~ b) ==> IR Stop True [] -- after substituting we re-canonicalize and get nothing
336 -- Main interaction solver: we fully solve the worklist 'in one go',
337 -- returning an extended inert set.
339 -- See Note [Touchables and givens].
340 solveInteractGiven :: InertSet -> GivenLoc -> [EvVar] -> TcS InertSet
341 solveInteractGiven inert gloc evs
342 = do { (_, inert_ret) <- solveInteract inert $ listToBag $
347 mk_given ev = mkEvVarX ev flav
349 solveInteractWanted :: InertSet -> [WantedEvVar] -> TcS InertSet
350 solveInteractWanted inert wvs
351 = do { (_,inert_ret) <- solveInteract inert $ listToBag $
352 map wantedToFlavored wvs
355 solveInteract :: InertSet -> Bag FlavoredEvVar -> TcS (Bool, InertSet)
356 -- Post: (True, inert_set) means we managed to discharge all constraints
357 -- without actually doing any interactions!
358 -- (False, inert_set) means some interactions occurred
359 solveInteract inert ws
360 = do { dyn_flags <- getDynFlags
361 ; sctx <- getTcSContext
363 ; traceTcS "solveInteract, before clever canonicalization:" $
364 vcat [ text "ws = " <+> ppr (mapBag (\(EvVarX ev ct)
365 -> (ct,evVarPred ev)) ws)
366 , text "inert = " <+> ppr inert ]
368 ; (flag, inert_ret) <- foldrBagM (tryPreSolveAndInteract sctx dyn_flags) (True,inert) ws
369 -- use foldr to preserve the order
371 ; traceTcS "solveInteract, after clever canonicalization (and interaction):" $
372 vcat [ text "No interaction happened = " <+> ppr flag
373 , text "inert_ret = " <+> ppr inert_ret ]
375 ; return (flag, inert_ret) }
378 tryPreSolveAndInteract :: SimplContext
382 -> TcS (Bool, InertSet)
383 -- Returns: True if it was able to discharge this constraint AND all previous ones
384 tryPreSolveAndInteract sctx dyn_flags flavev@(EvVarX ev_var fl) (all_previous_discharged, inert)
385 = do { let inert_cts = get_inert_cts (evVarPred ev_var)
387 ; this_one_discharged <- dischargeFromCCans inert_cts flavev
389 ; if this_one_discharged
390 then return (all_previous_discharged, inert)
393 { extra_cts <- mkCanonical fl ev_var
394 ; inert_ret <- solveInteractWithDepth (ctxtStkDepth dyn_flags,0,[]) extra_cts inert
395 ; return (False, inert_ret) } }
398 get_inert_cts (ClassP clas _)
399 | simplEqsOnly sctx = emptyCCan
400 | otherwise = fst (getRelevantCts clas (inert_dicts inert))
401 get_inert_cts (IParam {})
402 = emptyCCan -- We must not do the same thing for IParams, because (contrary
403 -- to dictionaries), work items /must/ override inert items.
404 -- See Note [Overriding implicit parameters] in TcInteract.
405 get_inert_cts (EqPred {})
406 = inert_eqs inert `unionBags` cCanMapToBag (inert_funeqs inert)
408 dischargeFromCCans :: CanonicalCts -> FlavoredEvVar -> TcS Bool
409 dischargeFromCCans cans (EvVarX ev fl)
410 = Bag.foldlBagM discharge_ct False cans
411 where discharge_ct :: Bool -> CanonicalCt -> TcS Bool
412 discharge_ct True _ct = return True
413 discharge_ct False ct
414 | evVarPred (cc_id ct) `tcEqPred` evVarPred ev
415 , cc_flavor ct `canSolve` fl
416 = do { when (isWanted fl) $ set_ev_bind ev (cc_id ct)
418 where set_ev_bind x y
419 | EqPred {} <- evVarPred y
420 = setEvBind x (EvCoercion (mkCoVarCoercion y))
421 | otherwise = setEvBind x (EvId y)
422 discharge_ct False _ct = return False
425 Note [Avoiding the superclass explosion]
426 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
427 This note now is not as significant as it used to be because we no
428 longer add the superclasses of Wanted as Derived, except only if they
429 have equality superclasses or superclasses with functional
430 dependencies. The fear was that hundreds of identical wanteds would
431 give rise each to the same superclass or equality Derived's which
432 would lead to a blo-up in the number of interactions.
434 Instead, what we do with tryPreSolveAndCanon, is when we encounter a
435 new constraint, we very quickly see if it can be immediately
436 discharged by a class constraint in our inert set or the previous
437 canonicals. If so, we add nothing to the returned canonical
441 solveOne :: WorkItem -> InertSet -> TcS InertSet
442 solveOne workItem inerts
443 = do { dyn_flags <- getDynFlags
444 ; solveOneWithDepth (ctxtStkDepth dyn_flags,0,[]) workItem inerts
448 solveInteractWithDepth :: (Int, Int, [WorkItem])
449 -> WorkList -> InertSet -> TcS InertSet
450 solveInteractWithDepth ctxt@(max_depth,n,stack) ws inert
455 = solverDepthErrorTcS n stack
458 = do { traceTcS "solveInteractWithDepth" $
459 vcat [ text "Current depth =" <+> ppr n
460 , text "Max depth =" <+> ppr max_depth
461 , text "ws =" <+> ppr ws ]
463 -- Solve equalities first
464 ; let (eqs, non_eqs) = Bag.partitionBag isCTyEqCan ws
465 ; is_from_eqs <- Bag.foldrBagM (solveOneWithDepth ctxt) inert eqs
466 ; Bag.foldrBagM (solveOneWithDepth ctxt) is_from_eqs non_eqs }
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 (isGivenCt 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 ; cv_given <- newGivenCoVar (mkTyVarTy tv) xi xi
732 ; when (isWanted wd) (setWantedCoBind cv xi)
733 -- 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 = mkGivenFlavor wd UnkSkol
737 , cc_tyvar = tv, cc_rhs = xi }) }
743 *********************************************************************************
745 The interact-with-inert Stage
747 *********************************************************************************
750 -- Interaction result of WorkItem <~> AtomicInert
752 = IR { ir_stop :: StopOrContinue
754 -- => Reagent (work item) consumed.
755 -- ContinueWith new_reagent
756 -- => Reagent transformed but keep gathering interactions.
757 -- The transformed item remains inert with respect
758 -- to any previously encountered inerts.
760 , ir_inert_action :: InertAction
761 -- Whether the inert item should remain in the InertSet.
763 , ir_new_work :: WorkList
764 -- new work items to add to the WorkList
766 , ir_fire :: Maybe String -- Tells whether a rule fired, and if so what
769 -- What to do with the inert reactant.
770 data InertAction = KeepInert | DropInert
772 mkIRContinue :: String -> WorkItem -> InertAction -> WorkList -> TcS InteractResult
773 mkIRContinue rule wi keep newWork
774 = return $ IR { ir_stop = ContinueWith wi, ir_inert_action = keep
775 , ir_new_work = newWork, ir_fire = Just rule }
777 mkIRStop :: String -> WorkList -> TcS InteractResult
778 mkIRStop rule newWork
779 = return $ IR { ir_stop = Stop, ir_inert_action = KeepInert
780 , ir_new_work = newWork, ir_fire = Just rule }
782 noInteraction :: Monad m => WorkItem -> m InteractResult
784 = return $ IR { ir_stop = ContinueWith wi, ir_inert_action = KeepInert
785 , ir_new_work = emptyWorkList, ir_fire = Nothing }
787 data WhichComesFromInert = LeftComesFromInert | RightComesFromInert
788 -- See Note [Efficient Orientation]
791 ---------------------------------------------------
792 -- Interact a single WorkItem with the equalities of an inert set as
793 -- far as possible, i.e. until we get a Stop result from an individual
794 -- reaction (i.e. when the WorkItem is consumed), or until we've
795 -- interact the WorkItem with the entire equalities of the InertSet
797 interactWithInertEqsStage :: SimplifierStage
798 interactWithInertEqsStage depth workItem inert
799 = Bag.foldrBagM (interactNext depth) initITR (inert_eqs inert)
800 -- use foldr to preserve the order
802 initITR = SR { sr_inerts = inert { inert_eqs = emptyCCan }
803 , sr_new_work = emptyWorkList
804 , sr_stop = ContinueWith workItem }
806 ---------------------------------------------------
807 -- Interact a single WorkItem with *non-equality* constraints in the inert set.
808 -- Precondition: equality interactions must have already happened, hence we have
809 -- to pick up some information from the incoming inert, before folding over the
810 -- "Other" constraints it contains!
812 interactWithInertsStage :: SimplifierStage
813 interactWithInertsStage depth workItem inert
814 = let (relevant, inert_residual) = getISRelevant workItem inert
815 initITR = SR { sr_inerts = inert_residual
816 , sr_new_work = emptyWorkList
817 , sr_stop = ContinueWith workItem }
818 in Bag.foldrBagM (interactNext depth) initITR relevant
819 -- use foldr to preserve the order
821 getISRelevant :: CanonicalCt -> InertSet -> (CanonicalCts, InertSet)
822 getISRelevant (CFrozenErr {}) is = (emptyCCan, is)
823 -- Nothing s relevant; we have alread interacted
824 -- it with the equalities in the inert set
826 getISRelevant (CDictCan { cc_class = cls } ) is
827 = let (relevant, residual_map) = getRelevantCts cls (inert_dicts is)
828 in (relevant, is { inert_dicts = residual_map })
829 getISRelevant (CFunEqCan { cc_fun = tc } ) is
830 = let (relevant, residual_map) = getRelevantCts tc (inert_funeqs is)
831 in (relevant, is { inert_funeqs = residual_map })
832 getISRelevant (CIPCan { cc_ip_nm = nm }) is
833 = let (relevant, residual_map) = getRelevantCts nm (inert_ips is)
834 in (relevant, is { inert_ips = residual_map })
835 -- An equality, finally, may kick everything except equalities out
836 -- because we have already interacted the equalities in interactWithInertEqsStage
837 getISRelevant _eq_ct is -- Equality, everything is relevant for this one
838 -- TODO: if we were caching variables, we'd know that only
839 -- some are relevant. Experiment with this for now.
840 = let cts = cCanMapToBag (inert_ips is) `unionBags`
841 cCanMapToBag (inert_dicts is) `unionBags` cCanMapToBag (inert_funeqs is)
842 in (cts, is { inert_dicts = emptyCCanMap
843 , inert_ips = emptyCCanMap
844 , inert_funeqs = emptyCCanMap })
846 interactNext :: SubGoalDepth -> AtomicInert -> StageResult -> TcS StageResult
847 interactNext depth inert it
848 | ContinueWith work_item <- sr_stop it
849 = do { let inerts = sr_inerts it
851 ; IR { ir_new_work = new_work, ir_inert_action = inert_action
852 , ir_fire = fire_info, ir_stop = stop }
853 <- interactWithInert inert work_item
856 = text rule <+> keep_doc
857 <+> vcat [ ptext (sLit "Inert =") <+> ppr inert
858 , ptext (sLit "Work =") <+> ppr work_item
859 , ppUnless (isEmptyBag new_work) $
860 ptext (sLit "New =") <+> ppr new_work ]
861 keep_doc = case inert_action of
862 KeepInert -> ptext (sLit "[keep]")
863 DropInert -> ptext (sLit "[drop]")
865 Just rule -> do { bumpStepCountTcS
866 ; traceFireTcS depth (mk_msg rule) }
869 -- New inerts depend on whether we KeepInert or not
870 ; let inerts_new = case inert_action of
871 KeepInert -> inerts `updInertSet` inert
874 ; return $ SR { sr_inerts = inerts_new
875 , sr_new_work = sr_new_work it `unionWorkLists` new_work
878 = return $ it { sr_inerts = (sr_inerts it) `updInertSet` inert }
880 -- Do a single interaction of two constraints.
881 interactWithInert :: AtomicInert -> WorkItem -> TcS InteractResult
882 interactWithInert inert workitem
883 = do { ctxt <- getTcSContext
884 ; let is_allowed = allowedInteraction (simplEqsOnly ctxt) inert workitem
887 doInteractWithInert inert workitem
889 noInteraction workitem
892 allowedInteraction :: Bool -> AtomicInert -> WorkItem -> Bool
893 -- Allowed interactions
894 allowedInteraction eqs_only (CDictCan {}) (CDictCan {}) = not eqs_only
895 allowedInteraction eqs_only (CIPCan {}) (CIPCan {}) = not eqs_only
896 allowedInteraction _ _ _ = True
898 --------------------------------------------
899 doInteractWithInert :: CanonicalCt -> CanonicalCt -> TcS InteractResult
900 -- Identical class constraints.
903 (CDictCan { cc_id = d1, cc_flavor = fl1, cc_class = cls1, cc_tyargs = tys1 })
904 workItem@(CDictCan { cc_id = d2, cc_flavor = fl2, cc_class = cls2, cc_tyargs = tys2 })
905 | cls1 == cls2 && (and $ zipWith tcEqType tys1 tys2)
906 = solveOneFromTheOther (d1,fl1) workItem
908 | cls1 == cls2 && (not (isGiven fl1 && isGiven fl2))
909 = -- See Note [When improvement happens]
910 do { let pty1 = ClassP cls1 tys1
911 pty2 = ClassP cls2 tys2
912 inert_pred_loc = (pty1, pprFlavorArising fl1)
913 work_item_pred_loc = (pty2, pprFlavorArising fl2)
914 fd_eqns = improveFromAnother
915 inert_pred_loc -- the template
916 work_item_pred_loc -- the one we aim to rewrite
917 -- See Note [Efficient Orientation]
919 ; m <- rewriteWithFunDeps fd_eqns tys2 fl2
921 Nothing -> noInteraction workItem
922 Just (rewritten_tys2, cos2, fd_work)
924 | tcEqTypes tys1 rewritten_tys2
925 -> -- Solve him on the spot in this case
926 do { let dict_co = mkTyConCoercion (classTyCon cls1) cos2
927 ; when (isWanted fl2) $ setDictBind d2 (EvCast d1 dict_co)
928 ; mkIRStop "Cls/Cls fundep (solved)" fd_work }
931 -> -- We could not quite solve him, but we stil rewrite him
932 -- Example: class C a b c | a -> b
933 -- Given: C Int Bool x, Wanted: C Int beta y
934 -- Then rewrite the wanted to C Int Bool y
935 -- but note that is still not identical to the given
936 -- The important thing is that the rewritten constraint is
937 -- inert wrt the given.
938 -- In fact, it is inert wrt all the previous inerts too, so
939 -- we can keep on going rather than sending it back to the work list
940 do { let dict_co = mkTyConCoercion (classTyCon cls1) cos2
941 ; d2' <- newDictVar cls1 rewritten_tys2
942 ; setDictBind d2 (EvCast d2' dict_co)
943 ; let workItem' = workItem { cc_id = d2', cc_tyargs = rewritten_tys2 }
944 ; mkIRContinue "Cls/Cls fundep (partial)" workItem' KeepInert fd_work }
947 -> ASSERT (isDerived fl2) -- Derived constraints have no evidence,
948 -- so just produce the rewritten constraint
949 let workItem' = workItem { cc_tyargs = rewritten_tys2 }
950 in mkIRContinue "Cls/Cls fundep" workItem' KeepInert fd_work
953 -- Class constraint and given equality: use the equality to rewrite
954 -- the class constraint.
955 doInteractWithInert (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi })
956 (CDictCan { cc_id = dv, cc_flavor = wfl, cc_class = cl, cc_tyargs = xis })
957 | ifl `canRewrite` wfl
958 , tv `elemVarSet` tyVarsOfTypes xis
959 = do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,wfl,cl,xis)
960 -- Continue with rewritten Dictionary because we can only be in the
961 -- interactWithEqsStage, so the dictionary is inert.
962 ; mkIRContinue "Eq/Cls" rewritten_dict KeepInert emptyWorkList }
964 doInteractWithInert (CDictCan { cc_id = dv, cc_flavor = ifl, cc_class = cl, cc_tyargs = xis })
965 workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
966 | wfl `canRewrite` ifl
967 , tv `elemVarSet` tyVarsOfTypes xis
968 = do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,ifl,cl,xis)
969 ; mkIRContinue "Cls/Eq" workItem DropInert (workListFromCCan rewritten_dict) }
971 -- Class constraint and given equality: use the equality to rewrite
972 -- the class constraint.
973 doInteractWithInert (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi })
974 (CIPCan { cc_id = ipid, cc_flavor = wfl, cc_ip_nm = nm, cc_ip_ty = ty })
975 | ifl `canRewrite` wfl
976 , tv `elemVarSet` tyVarsOfType ty
977 = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,wfl,nm,ty)
978 ; mkIRContinue "Eq/IP" rewritten_ip KeepInert emptyWorkList }
980 doInteractWithInert (CIPCan { cc_id = ipid, cc_flavor = ifl, cc_ip_nm = nm, cc_ip_ty = ty })
981 workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
982 | wfl `canRewrite` ifl
983 , tv `elemVarSet` tyVarsOfType ty
984 = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,ifl,nm,ty)
985 ; mkIRContinue "IP/Eq" workItem DropInert (workListFromCCan rewritten_ip) }
987 -- Two implicit parameter constraints. If the names are the same,
988 -- but their types are not, we generate a wanted type equality
989 -- that equates the type (this is "improvement").
990 -- However, we don't actually need the coercion evidence,
991 -- so we just generate a fresh coercion variable that isn't used anywhere.
992 doInteractWithInert (CIPCan { cc_id = id1, cc_flavor = ifl, cc_ip_nm = nm1, cc_ip_ty = ty1 })
993 workItem@(CIPCan { cc_flavor = wfl, cc_ip_nm = nm2, cc_ip_ty = ty2 })
994 | nm1 == nm2 && isGiven wfl && isGiven ifl
995 = -- See Note [Overriding implicit parameters]
996 -- Dump the inert item, override totally with the new one
997 -- Do not require type equality
998 -- For example, given let ?x::Int = 3 in let ?x::Bool = True in ...
999 -- we must *override* the outer one with the inner one
1000 mkIRContinue "IP/IP override" workItem DropInert emptyWorkList
1002 | nm1 == nm2 && ty1 `tcEqType` ty2
1003 = solveOneFromTheOther (id1,ifl) workItem
1006 = -- See Note [When improvement happens]
1007 do { co_var <- newWantedCoVar ty2 ty1 -- See Note [Efficient Orientation]
1008 ; let flav = Wanted (combineCtLoc ifl wfl)
1009 ; cans <- mkCanonical flav co_var
1010 ; mkIRContinue "IP/IP fundep" workItem KeepInert cans }
1012 -- Never rewrite a given with a wanted equality, and a type function
1013 -- equality can never rewrite an equality. We rewrite LHS *and* RHS
1014 -- of function equalities so that our inert set exposes everything that
1015 -- we know about equalities.
1017 -- Inert: equality, work item: function equality
1018 doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi1 })
1019 (CFunEqCan { cc_id = cv2, cc_flavor = wfl, cc_fun = tc
1020 , cc_tyargs = args, cc_rhs = xi2 })
1021 | ifl `canRewrite` wfl
1022 , tv `elemVarSet` tyVarsOfTypes (xi2:args) -- Rewrite RHS as well
1023 = do { rewritten_funeq <- rewriteFunEq (cv1,tv,xi1) (cv2,wfl,tc,args,xi2)
1024 ; mkIRStop "Eq/FunEq" (workListFromCCan rewritten_funeq) }
1025 -- Must Stop here, because we may no longer be inert after the rewritting.
1027 -- Inert: function equality, work item: equality
1028 doInteractWithInert (CFunEqCan {cc_id = cv1, cc_flavor = ifl, cc_fun = tc
1029 , cc_tyargs = args, cc_rhs = xi1 })
1030 workItem@(CTyEqCan { cc_id = cv2, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi2 })
1031 | wfl `canRewrite` ifl
1032 , tv `elemVarSet` tyVarsOfTypes (xi1:args) -- Rewrite RHS as well
1033 = do { rewritten_funeq <- rewriteFunEq (cv2,tv,xi2) (cv1,ifl,tc,args,xi1)
1034 ; mkIRContinue "FunEq/Eq" workItem DropInert (workListFromCCan rewritten_funeq) }
1035 -- One may think that we could (KeepTransformedInert rewritten_funeq)
1036 -- but that is wrong, because it may end up not being inert with respect
1037 -- to future inerts. Example:
1038 -- Original inert = { F xis ~ [a], b ~ Maybe Int }
1039 -- Work item comes along = a ~ [b]
1040 -- If we keep { F xis ~ [b] } in the inert set we will end up with:
1041 -- { F xis ~ [b], b ~ Maybe Int, a ~ [Maybe Int] }
1042 -- At the end, which is *not* inert. So we should unfortunately DropInert here.
1044 doInteractWithInert (CFunEqCan { cc_id = cv1, cc_flavor = fl1, cc_fun = tc1
1045 , cc_tyargs = args1, cc_rhs = xi1 })
1046 workItem@(CFunEqCan { cc_id = cv2, cc_flavor = fl2, cc_fun = tc2
1047 , cc_tyargs = args2, cc_rhs = xi2 })
1048 | fl1 `canSolve` fl2 && lhss_match
1049 = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
1050 ; mkIRStop "FunEq/FunEq" cans }
1051 | fl2 `canSolve` fl1 && lhss_match
1052 = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
1053 ; mkIRContinue "FunEq/FunEq" workItem DropInert cans }
1055 lhss_match = tc1 == tc2 && and (zipWith tcEqType args1 args2)
1057 doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
1058 workItem@(CTyEqCan { cc_id = cv2, cc_flavor = fl2, cc_tyvar = tv2, cc_rhs = xi2 })
1059 -- Check for matching LHS
1060 | fl1 `canSolve` fl2 && tv1 == tv2
1061 = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
1062 ; mkIRStop "Eq/Eq lhs" cans }
1064 | fl2 `canSolve` fl1 && tv1 == tv2
1065 = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
1066 ; mkIRContinue "Eq/Eq lhs" workItem DropInert cans }
1068 -- Check for rewriting RHS
1069 | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfType xi2
1070 = do { rewritten_eq <- rewriteEqRHS (cv1,tv1,xi1) (cv2,fl2,tv2,xi2)
1071 ; mkIRStop "Eq/Eq rhs" rewritten_eq }
1073 | fl2 `canRewrite` fl1 && tv2 `elemVarSet` tyVarsOfType xi1
1074 = do { rewritten_eq <- rewriteEqRHS (cv2,tv2,xi2) (cv1,fl1,tv1,xi1)
1075 ; mkIRContinue "Eq/Eq rhs" workItem DropInert rewritten_eq }
1077 doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
1078 (CFrozenErr { cc_id = cv2, cc_flavor = fl2 })
1079 | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfEvVar cv2
1080 = do { rewritten_frozen <- rewriteFrozen (cv1, tv1, xi1) (cv2, fl2)
1081 ; mkIRStop "Frozen/Eq" rewritten_frozen }
1083 doInteractWithInert (CFrozenErr { cc_id = cv2, cc_flavor = fl2 })
1084 workItem@(CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
1085 | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfEvVar cv2
1086 = do { rewritten_frozen <- rewriteFrozen (cv1, tv1, xi1) (cv2, fl2)
1087 ; mkIRContinue "Frozen/Eq" workItem DropInert rewritten_frozen }
1089 -- Fall-through case for all other situations
1090 doInteractWithInert _ workItem = noInteraction workItem
1092 -------------------------
1093 -- Equational Rewriting
1094 rewriteDict :: (CoVar, TcTyVar, Xi) -> (DictId, CtFlavor, Class, [Xi]) -> TcS CanonicalCt
1095 rewriteDict (cv,tv,xi) (dv,gw,cl,xis)
1096 = do { let cos = substTysWith [tv] [mkCoVarCoercion cv] xis -- xis[tv] ~ xis[xi]
1097 args = substTysWith [tv] [xi] xis
1099 dict_co = mkTyConCoercion con cos
1100 ; dv' <- newDictVar cl args
1102 Wanted {} -> setDictBind dv (EvCast dv' (mkSymCoercion dict_co))
1103 Given {} -> setDictBind dv' (EvCast dv dict_co)
1104 Derived {} -> return () -- Derived dicts we don't set any evidence
1106 ; return (CDictCan { cc_id = dv'
1109 , cc_tyargs = args }) }
1111 rewriteIP :: (CoVar,TcTyVar,Xi) -> (EvVar,CtFlavor, IPName Name, TcType) -> TcS CanonicalCt
1112 rewriteIP (cv,tv,xi) (ipid,gw,nm,ty)
1113 = do { let ip_co = substTyWith [tv] [mkCoVarCoercion cv] ty -- ty[tv] ~ t[xi]
1114 ty' = substTyWith [tv] [xi] ty
1115 ; ipid' <- newIPVar nm ty'
1117 Wanted {} -> setIPBind ipid (EvCast ipid' (mkSymCoercion ip_co))
1118 Given {} -> setIPBind ipid' (EvCast ipid ip_co)
1119 Derived {} -> return () -- Derived ips: we don't set any evidence
1121 ; return (CIPCan { cc_id = ipid'
1124 , cc_ip_ty = ty' }) }
1126 rewriteFunEq :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TyCon, [Xi], Xi) -> TcS CanonicalCt
1127 rewriteFunEq (cv1,tv,xi1) (cv2,gw, tc,args,xi2) -- cv2 :: F args ~ xi2
1128 = do { let arg_cos = substTysWith [tv] [mkCoVarCoercion cv1] args
1129 args' = substTysWith [tv] [xi1] args
1130 fun_co = mkTyConCoercion tc arg_cos -- fun_co :: F args ~ F args'
1132 xi2' = substTyWith [tv] [xi1] xi2
1133 xi2_co = substTyWith [tv] [mkCoVarCoercion cv1] xi2 -- xi2_co :: xi2 ~ xi2'
1134 ; cv2' <- case gw of
1135 Wanted {} -> do { cv2' <- newWantedCoVar (mkTyConApp tc args') xi2'
1136 ; setWantedCoBind cv2 $
1137 fun_co `mkTransCoercion`
1138 mkCoVarCoercion cv2' `mkTransCoercion` mkSymCoercion xi2_co
1140 Given {} -> newGivenCoVar (mkTyConApp tc args') xi2' $
1141 mkSymCoercion fun_co `mkTransCoercion`
1142 mkCoVarCoercion cv2 `mkTransCoercion` xi2_co
1143 Derived {} -> newDerivedId (EqPred (mkTyConApp tc args') xi2')
1145 ; return (CFunEqCan { cc_id = cv2'
1149 , cc_rhs = xi2' }) }
1152 rewriteEqRHS :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TcTyVar,Xi) -> TcS WorkList
1153 -- Use the first equality to rewrite the second, flavors already checked.
1154 -- E.g. c1 : tv1 ~ xi1 c2 : tv2 ~ xi2
1155 -- rewrites c2 to give
1156 -- c2' : tv2 ~ xi2[xi1/tv1]
1157 -- We must do an occurs check to sure the new constraint is canonical
1158 -- So we might return an empty bag
1159 rewriteEqRHS (cv1,tv1,xi1) (cv2,gw,tv2,xi2)
1160 | Just tv2' <- tcGetTyVar_maybe xi2'
1161 , tv2 == tv2' -- In this case xi2[xi1/tv1] = tv2, so we have tv2~tv2
1162 = do { when (isWanted gw) (setWantedCoBind cv2 (mkSymCoercion co2'))
1163 ; return emptyCCan }
1168 -> do { cv2' <- newWantedCoVar (mkTyVarTy tv2) xi2'
1169 ; setWantedCoBind cv2 $
1170 mkCoVarCoercion cv2' `mkTransCoercion` mkSymCoercion co2'
1173 -> newGivenCoVar (mkTyVarTy tv2) xi2' $
1174 mkCoVarCoercion cv2 `mkTransCoercion` co2'
1176 -> newDerivedId (EqPred (mkTyVarTy tv2) xi2')
1178 ; canEq gw cv2' (mkTyVarTy tv2) xi2'
1181 xi2' = substTyWith [tv1] [xi1] xi2
1182 co2' = substTyWith [tv1] [mkCoVarCoercion cv1] xi2 -- xi2 ~ xi2[xi1/tv1]
1185 rewriteEqLHS :: WhichComesFromInert -> (Coercion,Xi) -> (CoVar,CtFlavor,Xi) -> TcS WorkList
1186 -- Used to ineract two equalities of the following form:
1187 -- First Equality: co1: (XXX ~ xi1)
1188 -- Second Equality: cv2: (XXX ~ xi2)
1189 -- Where the cv1 `canSolve` cv2 equality
1190 -- We have an option of creating new work (xi1 ~ xi2) OR (xi2 ~ xi1),
1191 -- See Note [Efficient Orientation] for that
1192 rewriteEqLHS which (co1,xi1) (cv2,gw,xi2)
1193 = do { cv2' <- case (isWanted gw, which) of
1194 (True,LeftComesFromInert) ->
1195 do { cv2' <- newWantedCoVar xi2 xi1
1196 ; setWantedCoBind cv2 $
1197 co1 `mkTransCoercion` mkSymCoercion (mkCoVarCoercion cv2')
1199 (True,RightComesFromInert) ->
1200 do { cv2' <- newWantedCoVar xi1 xi2
1201 ; setWantedCoBind cv2 $
1202 co1 `mkTransCoercion` mkCoVarCoercion cv2'
1204 (False,LeftComesFromInert) ->
1206 newGivenCoVar xi2 xi1 $
1207 mkSymCoercion (mkCoVarCoercion cv2) `mkTransCoercion` co1
1208 else newDerivedId (EqPred xi2 xi1)
1209 (False,RightComesFromInert) ->
1211 newGivenCoVar xi1 xi2 $
1212 mkSymCoercion co1 `mkTransCoercion` mkCoVarCoercion cv2
1213 else newDerivedId (EqPred xi1 xi2)
1214 ; mkCanonical gw cv2' }
1216 rewriteFrozen :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor) -> TcS WorkList
1217 rewriteFrozen (cv1, tv1, xi1) (cv2, fl2)
1220 Wanted {} -> do { cv2' <- newWantedCoVar ty2a' ty2b'
1221 -- ty2a[xi1/tv1] ~ ty2b[xi1/tv1]
1222 ; setWantedCoBind cv2 $
1223 co2a' `mkTransCoercion`
1224 mkCoVarCoercion cv2' `mkTransCoercion`
1228 Given {} -> newGivenCoVar ty2a' ty2b' $
1229 mkSymCoercion co2a' `mkTransCoercion`
1230 mkCoVarCoercion cv2 `mkTransCoercion`
1233 Derived {} -> newDerivedId (EqPred ty2a' ty2b')
1234 ; return (singleCCan $ CFrozenErr { cc_id = cv2', cc_flavor = fl2 }) }
1236 (ty2a, ty2b) = coVarKind cv2 -- cv2 : ty2a ~ ty2b
1237 ty2a' = substTyWith [tv1] [xi1] ty2a
1238 ty2b' = substTyWith [tv1] [xi1] ty2b
1240 co2a' = substTyWith [tv1] [mkCoVarCoercion cv1] ty2a -- ty2a ~ ty2a[xi1/tv1]
1241 co2b' = substTyWith [tv1] [mkCoVarCoercion cv1] ty2b -- ty2b ~ ty2b[xi1/tv1]
1243 solveOneFromTheOther :: (EvVar, CtFlavor) -> CanonicalCt -> TcS InteractResult
1244 -- First argument inert, second argument work-item. They both represent
1245 -- wanted/given/derived evidence for the *same* predicate so we try here to
1246 -- discharge one directly from the other.
1248 -- Precondition: value evidence only (implicit parameters, classes)
1250 solveOneFromTheOther (iid,ifl) workItem
1252 = mkIRStop "Solved (derived)" emptyWorkList
1254 | ifl `canSolve` wfl
1255 = do { when (isWanted wfl) $ setEvBind wid (EvId iid)
1256 -- Overwrite the binding, if one exists
1257 -- For Givens, which are lambda-bound, nothing to overwrite,
1258 ; mkIRStop "Solved" emptyWorkList }
1260 | wfl `canSolve` ifl
1261 = do { when (isWanted ifl) $ setEvBind iid (EvId wid)
1262 ; mkIRContinue "Solved inert" workItem DropInert emptyWorkList }
1264 | otherwise -- The inert item is Derived, we can just throw it away,
1265 = mkIRContinue "Discard derived inert" workItem DropInert emptyWorkList
1268 wfl = cc_flavor workItem
1269 wid = cc_id workItem
1272 Note [Superclasses and recursive dictionaries]
1273 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1274 Overlaps with Note [SUPERCLASS-LOOP 1]
1275 Note [SUPERCLASS-LOOP 2]
1276 Note [Recursive instances and superclases]
1277 ToDo: check overlap and delete redundant stuff
1279 Right before adding a given into the inert set, we must
1280 produce some more work, that will bring the superclasses
1281 of the given into scope. The superclass constraints go into
1284 When we simplify a wanted constraint, if we first see a matching
1285 instance, we may produce new wanted work. To (1) avoid doing this work
1286 twice in the future and (2) to handle recursive dictionaries we may ``cache''
1287 this item as given into our inert set WITHOUT adding its superclass constraints,
1288 otherwise we'd be in danger of creating a loop [In fact this was the exact reason
1289 for doing the isGoodRecEv check in an older version of the type checker].
1291 But now we have added partially solved constraints to the worklist which may
1292 interact with other wanteds. Consider the example:
1296 class Eq b => Foo a b --- 0-th selector
1297 instance Eq a => Foo [a] a --- fooDFun
1299 and wanted (Foo [t] t). We are first going to see that the instance matches
1300 and create an inert set that includes the solved (Foo [t] t) but not its superclasses:
1301 d1 :_g Foo [t] t d1 := EvDFunApp fooDFun d3
1302 Our work list is going to contain a new *wanted* goal
1305 Ok, so how do we get recursive dictionaries, at all:
1309 data D r = ZeroD | SuccD (r (D r));
1311 instance (Eq (r (D r))) => Eq (D r) where
1312 ZeroD == ZeroD = True
1313 (SuccD a) == (SuccD b) = a == b
1316 equalDC :: D [] -> D [] -> Bool;
1319 We need to prove (Eq (D [])). Here's how we go:
1323 by instance decl, holds if
1327 *BUT* we have an inert set which gives us (no superclasses):
1329 By the instance declaration of Eq we can show the 'd2' goal if
1331 where d2 = dfEqList d3
1333 Now, however this wanted can interact with our inert d1 to set:
1335 and solve the goal. Why was this interaction OK? Because, if we chase the
1336 evidence of d1 ~~> dfEqD d2 ~~-> dfEqList d3, so by setting d3 := d1 we
1338 d3 := dfEqD2 (dfEqList d3)
1339 which is FINE because the use of d3 is protected by the instance function
1342 So, our strategy is to try to put solved wanted dictionaries into the
1343 inert set along with their superclasses (when this is meaningful,
1344 i.e. when new wanted goals are generated) but solve a wanted dictionary
1345 from a given only in the case where the evidence variable of the
1346 wanted is mentioned in the evidence of the given (recursively through
1347 the evidence binds) in a protected way: more instance function applications
1348 than superclass selectors.
1350 Here are some more examples from GHC's previous type checker
1354 This code arises in the context of "Scrap Your Boilerplate with Class"
1358 instance Sat (ctx Char) => Data ctx Char -- dfunData1
1359 instance (Sat (ctx [a]), Data ctx a) => Data ctx [a] -- dfunData2
1361 class Data Maybe a => Foo a
1363 instance Foo t => Sat (Maybe t) -- dfunSat
1365 instance Data Maybe a => Foo a -- dfunFoo1
1366 instance Foo a => Foo [a] -- dfunFoo2
1367 instance Foo [Char] -- dfunFoo3
1369 Consider generating the superclasses of the instance declaration
1370 instance Foo a => Foo [a]
1372 So our problem is this
1374 d1 :_w Data Maybe [t]
1376 We may add the given in the inert set, along with its superclasses
1377 [assuming we don't fail because there is a matching instance, see
1378 tryTopReact, given case ]
1382 d01 :_g Data Maybe t -- d2 := EvDictSuperClass d0 0
1383 d1 :_w Data Maybe [t]
1384 Then d2 can readily enter the inert, and we also do solving of the wanted
1387 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1389 d2 :_w Sat (Maybe [t])
1391 d01 :_g Data Maybe t
1392 Now, we may simplify d2 more:
1395 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1396 d1 :_g Data Maybe [t]
1397 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1401 d01 :_g Data Maybe t
1403 Now, we can just solve d3.
1406 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1407 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1410 d01 :_g Data Maybe t
1411 And now we can simplify d4 again, but since it has superclasses we *add* them to the worklist:
1414 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1415 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1416 d4 :_g Foo [t] d4 := dfunFoo2 d5
1419 d6 :_g Data Maybe [t] d6 := EvDictSuperClass d4 0
1420 d01 :_g Data Maybe t
1421 Now, d5 can be solved! (and its superclass enter scope)
1424 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1425 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1426 d4 :_g Foo [t] d4 := dfunFoo2 d5
1427 d5 :_g Foo t d5 := dfunFoo1 d7
1430 d6 :_g Data Maybe [t]
1431 d8 :_g Data Maybe t d8 := EvDictSuperClass d5 0
1432 d01 :_g Data Maybe t
1435 [1] Suppose we pick d8 and we react him with d01. Which of the two givens should
1436 we keep? Well, we *MUST NOT* drop d01 because d8 contains recursive evidence
1437 that must not be used (look at case interactInert where both inert and workitem
1438 are givens). So we have several options:
1439 - Drop the workitem always (this will drop d8)
1440 This feels very unsafe -- what if the work item was the "good" one
1441 that should be used later to solve another wanted?
1442 - Don't drop anyone: the inert set may contain multiple givens!
1443 [This is currently implemented]
1445 The "don't drop anyone" seems the most safe thing to do, so now we come to problem 2:
1446 [2] We have added both d6 and d01 in the inert set, and we are interacting our wanted
1447 d7. Now the [isRecDictEv] function in the ineration solver
1448 [case inert-given workitem-wanted] will prevent us from interacting d7 := d8
1449 precisely because chasing the evidence of d8 leads us to an unguarded use of d7.
1451 So, no interaction happens there. Then we meet d01 and there is no recursion
1452 problem there [isRectDictEv] gives us the OK to interact and we do solve d7 := d01!
1454 Note [SUPERCLASS-LOOP 1]
1455 ~~~~~~~~~~~~~~~~~~~~~~~~
1456 We have to be very, very careful when generating superclasses, lest we
1457 accidentally build a loop. Here's an example:
1461 class S a => C a where { opc :: a -> a }
1462 class S b => D b where { opd :: b -> b }
1464 instance C Int where
1467 instance D Int where
1470 From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int}
1471 Simplifying, we may well get:
1472 $dfCInt = :C ds1 (opd dd)
1475 Notice that we spot that we can extract ds1 from dd.
1477 Alas! Alack! We can do the same for (instance D Int):
1479 $dfDInt = :D ds2 (opc dc)
1483 And now we've defined the superclass in terms of itself.
1484 Two more nasty cases are in
1489 - Satisfy the superclass context *all by itself*
1490 (tcSimplifySuperClasses)
1491 - And do so completely; i.e. no left-over constraints
1492 to mix with the constraints arising from method declarations
1495 Note [SUPERCLASS-LOOP 2]
1496 ~~~~~~~~~~~~~~~~~~~~~~~~
1497 We need to be careful when adding "the constaint we are trying to prove".
1498 Suppose we are *given* d1:Ord a, and want to deduce (d2:C [a]) where
1500 class Ord a => C a where
1501 instance Ord [a] => C [a] where ...
1503 Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the
1504 superclasses of C [a] to avails. But we must not overwrite the binding
1505 for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
1508 Here's another variant, immortalised in tcrun020
1509 class Monad m => C1 m
1510 class C1 m => C2 m x
1511 instance C2 Maybe Bool
1512 For the instance decl we need to build (C1 Maybe), and it's no good if
1513 we run around and add (C2 Maybe Bool) and its superclasses to the avails
1514 before we search for C1 Maybe.
1516 Here's another example
1517 class Eq b => Foo a b
1518 instance Eq a => Foo [a] a
1522 we'll first deduce that it holds (via the instance decl). We must not
1523 then overwrite the Eq t constraint with a superclass selection!
1525 At first I had a gross hack, whereby I simply did not add superclass constraints
1526 in addWanted, though I did for addGiven and addIrred. This was sub-optimal,
1527 becuase it lost legitimate superclass sharing, and it still didn't do the job:
1528 I found a very obscure program (now tcrun021) in which improvement meant the
1529 simplifier got two bites a the cherry... so something seemed to be an Stop
1530 first time, but reducible next time.
1532 Now we implement the Right Solution, which is to check for loops directly
1533 when adding superclasses. It's a bit like the occurs check in unification.
1535 Note [Recursive instances and superclases]
1536 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1537 Consider this code, which arises in the context of "Scrap Your
1538 Boilerplate with Class".
1542 instance Sat (ctx Char) => Data ctx Char
1543 instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]
1545 class Data Maybe a => Foo a
1547 instance Foo t => Sat (Maybe t)
1549 instance Data Maybe a => Foo a
1550 instance Foo a => Foo [a]
1553 In the instance for Foo [a], when generating evidence for the superclasses
1554 (ie in tcSimplifySuperClasses) we need a superclass (Data Maybe [a]).
1555 Using the instance for Data, we therefore need
1556 (Sat (Maybe [a], Data Maybe a)
1557 But we are given (Foo a), and hence its superclass (Data Maybe a).
1558 So that leaves (Sat (Maybe [a])). Using the instance for Sat means
1559 we need (Foo [a]). And that is the very dictionary we are bulding
1560 an instance for! So we must put that in the "givens". So in this
1562 Given: Foo a, Foo [a]
1563 Wanted: Data Maybe [a]
1565 BUT we must *not not not* put the *superclasses* of (Foo [a]) in
1566 the givens, which is what 'addGiven' would normally do. Why? Because
1567 (Data Maybe [a]) is the superclass, so we'd "satisfy" the wanted
1568 by selecting a superclass from Foo [a], which simply makes a loop.
1570 On the other hand we *must* put the superclasses of (Foo a) in
1571 the givens, as you can see from the derivation described above.
1573 Conclusion: in the very special case of tcSimplifySuperClasses
1574 we have one 'given' (namely the "this" dictionary) whose superclasses
1575 must not be added to 'givens' by addGiven.
1577 There is a complication though. Suppose there are equalities
1578 instance (Eq a, a~b) => Num (a,b)
1579 Then we normalise the 'givens' wrt the equalities, so the original
1580 given "this" dictionary is cast to one of a different type. So it's a
1581 bit trickier than before to identify the "special" dictionary whose
1582 superclasses must not be added. See test
1583 indexed-types/should_run/EqInInstance
1585 We need a persistent property of the dictionary to record this
1586 special-ness. Current I'm using the InstLocOrigin (a bit of a hack,
1587 but cool), which is maintained by dictionary normalisation.
1588 Specifically, the InstLocOrigin is
1590 then the no-superclass thing kicks in. WATCH OUT if you fiddle
1593 Note [MATCHING-SYNONYMS]
1594 ~~~~~~~~~~~~~~~~~~~~~~~~
1595 When trying to match a dictionary (D tau) to a top-level instance, or a
1596 type family equation (F taus_1 ~ tau_2) to a top-level family instance,
1597 we do *not* need to expand type synonyms because the matcher will do that for us.
1600 Note [RHS-FAMILY-SYNONYMS]
1601 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1602 The RHS of a family instance is represented as yet another constructor which is
1603 like a type synonym for the real RHS the programmer declared. Eg:
1604 type instance F (a,a) = [a]
1606 :R32 a = [a] -- internal type synonym introduced
1607 F (a,a) ~ :R32 a -- instance
1609 When we react a family instance with a type family equation in the work list
1610 we keep the synonym-using RHS without expansion.
1613 *********************************************************************************
1615 The top-reaction Stage
1617 *********************************************************************************
1620 -- If a work item has any form of interaction with top-level we get this
1621 data TopInteractResult
1622 = NoTopInt -- No top-level interaction
1623 -- Equivalent to (SomeTopInt emptyWorkList (ContinueWith work_item))
1625 { tir_new_work :: WorkList -- Sub-goals or new work (could be given,
1626 -- for superclasses)
1627 , tir_new_inert :: StopOrContinue -- The input work item, ready to become *inert* now:
1628 } -- NB: in ``given'' (solved) form if the
1629 -- original was wanted or given and instance match
1630 -- was found, but may also be in wanted form if we
1631 -- only reacted with functional dependencies
1632 -- arising from top-level instances.
1634 topReactionsStage :: SimplifierStage
1635 topReactionsStage depth workItem inerts
1636 = do { tir <- tryTopReact workItem
1639 return $ SR { sr_inerts = inerts
1640 , sr_new_work = emptyWorkList
1641 , sr_stop = ContinueWith workItem }
1642 SomeTopInt tir_new_work tir_new_inert ->
1643 do { bumpStepCountTcS
1644 ; traceFireTcS depth (ptext (sLit "Top react")
1645 <+> vcat [ ptext (sLit "Work =") <+> ppr workItem
1646 , ptext (sLit "New =") <+> ppr tir_new_work ])
1647 ; return $ SR { sr_inerts = inerts
1648 , sr_new_work = tir_new_work
1649 , sr_stop = tir_new_inert
1653 tryTopReact :: WorkItem -> TcS TopInteractResult
1654 tryTopReact workitem
1655 = do { -- A flag controls the amount of interaction allowed
1656 -- See Note [Simplifying RULE lhs constraints]
1657 ctxt <- getTcSContext
1658 ; if allowedTopReaction (simplEqsOnly ctxt) workitem
1659 then do { traceTcS "tryTopReact / calling doTopReact" (ppr workitem)
1660 ; doTopReact workitem }
1661 else return NoTopInt
1664 allowedTopReaction :: Bool -> WorkItem -> Bool
1665 allowedTopReaction eqs_only (CDictCan {}) = not eqs_only
1666 allowedTopReaction _ _ = True
1668 doTopReact :: WorkItem -> TcS TopInteractResult
1669 -- The work item does not react with the inert set, so try interaction with top-level instances
1670 -- NB: The place to add superclasses in *not* in doTopReact stage. Instead superclasses are
1671 -- added in the worklist as part of the canonicalisation process.
1672 -- See Note [Adding superclasses] in TcCanonical.
1675 -- See Note [Given constraint that matches an instance declaration]
1676 doTopReact (CDictCan { cc_flavor = Given {} })
1677 = return NoTopInt -- NB: Superclasses already added since it's canonical
1679 -- Derived dictionary: just look for functional dependencies
1680 doTopReact workItem@(CDictCan { cc_flavor = fl@(Derived loc)
1681 , cc_class = cls, cc_tyargs = xis })
1682 = do { instEnvs <- getInstEnvs
1683 ; let fd_eqns = improveFromInstEnv instEnvs
1684 (ClassP cls xis, pprArisingAt loc)
1685 ; m <- rewriteWithFunDeps fd_eqns xis fl
1687 Nothing -> return NoTopInt
1688 Just (xis',_,fd_work) ->
1689 let workItem' = workItem { cc_tyargs = xis' }
1690 -- Deriveds are not supposed to have identity (cc_id is unused!)
1691 in return $ SomeTopInt { tir_new_work = fd_work
1692 , tir_new_inert = ContinueWith workItem' } }
1694 -- Wanted dictionary
1695 doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = fl@(Wanted loc)
1696 , cc_class = cls, cc_tyargs = xis })
1697 = do { -- See Note [MATCHING-SYNONYMS]
1698 ; lkp_inst_res <- matchClassInst cls xis loc
1699 ; case lkp_inst_res of
1701 do { traceTcS "doTopReact/ no class instance for" (ppr dv)
1703 ; instEnvs <- getInstEnvs
1704 ; let fd_eqns = improveFromInstEnv instEnvs
1705 (ClassP cls xis, pprArisingAt loc)
1706 ; m <- rewriteWithFunDeps fd_eqns xis fl
1708 Nothing -> return NoTopInt
1709 Just (xis',cos,fd_work) ->
1710 do { let dict_co = mkTyConCoercion (classTyCon cls) cos
1711 ; dv'<- newDictVar cls xis'
1712 ; setDictBind dv (EvCast dv' dict_co)
1713 ; let workItem' = CDictCan { cc_id = dv', cc_flavor = fl,
1714 cc_class = cls, cc_tyargs = xis' }
1716 SomeTopInt { tir_new_work = singleCCan workItem' `andCCan` fd_work
1717 , tir_new_inert = Stop } } }
1719 GenInst wtvs ev_term -- Solved
1720 -- No need to do fundeps stuff here; the instance
1721 -- matches already so we won't get any more info
1722 -- from functional dependencies
1724 -> do { traceTcS "doTopReact/ found nullary class instance for" (ppr dv)
1725 ; setDictBind dv ev_term
1726 -- Solved in one step and no new wanted work produced.
1727 -- i.e we directly matched a top-level instance
1728 -- No point in caching this in 'inert'; hence Stop
1729 ; return $ SomeTopInt { tir_new_work = emptyWorkList
1730 , tir_new_inert = Stop } }
1733 -> do { traceTcS "doTopReact/ found nullary class instance for" (ppr dv)
1734 ; setDictBind dv ev_term
1735 -- Solved and new wanted work produced, you may cache the
1736 -- (tentatively solved) dictionary as Given! (used to be: Derived)
1737 ; let solved = workItem { cc_flavor = given_fl }
1738 given_fl = Given (setCtLocOrigin loc UnkSkol)
1739 ; inst_work <- canWanteds wtvs
1740 ; return $ SomeTopInt { tir_new_work = inst_work
1741 , tir_new_inert = ContinueWith solved } }
1745 doTopReact (CFunEqCan { cc_id = cv, cc_flavor = fl
1746 , cc_fun = tc, cc_tyargs = args, cc_rhs = xi })
1747 = ASSERT (isSynFamilyTyCon tc) -- No associated data families have reached that far
1748 do { match_res <- matchFam tc args -- See Note [MATCHING-SYNONYMS]
1752 MatchInstSingle (rep_tc, rep_tys)
1753 -> do { let Just coe_tc = tyConFamilyCoercion_maybe rep_tc
1754 Just rhs_ty = tcView (mkTyConApp rep_tc rep_tys)
1755 -- Eagerly expand away the type synonym on the
1756 -- RHS of a type function, so that it never
1757 -- appears in an error message
1758 -- See Note [Type synonym families] in TyCon
1759 coe = mkTyConApp coe_tc rep_tys
1761 Wanted {} -> do { cv' <- newWantedCoVar rhs_ty xi
1762 ; setWantedCoBind cv $
1763 coe `mkTransCoercion`
1766 Given {} -> newGivenCoVar xi rhs_ty $
1767 mkSymCoercion (mkCoVarCoercion cv) `mkTransCoercion` coe
1768 Derived {} -> newDerivedId (EqPred xi rhs_ty)
1769 ; can_cts <- mkCanonical fl cv'
1770 ; return $ SomeTopInt can_cts Stop }
1772 -> panicTcS $ text "TcSMonad.matchFam returned multiple instances!"
1776 -- Any other work item does not react with any top-level equations
1777 doTopReact _workItem = return NoTopInt
1781 Note [FunDep and implicit parameter reactions]
1782 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1783 Currently, our story of interacting two dictionaries (or a dictionary
1784 and top-level instances) for functional dependencies, and implicit
1785 paramters, is that we simply produce new wanted equalities. So for example
1787 class D a b | a -> b where ...
1793 We generate the extra work item
1795 where 'cv' is currently unused. However, this new item reacts with d2,
1796 discharging it in favour of a new constraint d2' thus:
1798 d2 := d2' |> D Int cv
1799 Now d2' can be discharged from d1
1801 We could be more aggressive and try to *immediately* solve the dictionary
1802 using those extra equalities. With the same inert set and work item we
1803 might dischard d2 directly:
1806 d2 := d1 |> D Int cv
1808 But in general it's a bit painful to figure out the necessary coercion,
1809 so we just take the first approach. Here is a better example. Consider:
1810 class C a b c | a -> b
1812 [Given] d1 : C T Int Char
1813 [Wanted] d2 : C T beta Int
1814 In this case, it's *not even possible* to solve the wanted immediately.
1815 So we should simply output the functional dependency and add this guy
1816 [but NOT its superclasses] back in the worklist. Even worse:
1817 [Given] d1 : C T Int beta
1818 [Wanted] d2: C T beta Int
1819 Then it is solvable, but its very hard to detect this on the spot.
1821 It's exactly the same with implicit parameters, except that the
1822 "aggressive" approach would be much easier to implement.
1824 Note [When improvement happens]
1825 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1826 We fire an improvement rule when
1828 * Two constraints match (modulo the fundep)
1829 e.g. C t1 t2, C t1 t3 where C a b | a->b
1830 The two match because the first arg is identical
1832 * At least one is not Given. If they are both given, we don't fire
1833 the reaction because we have no way of constructing evidence for a
1834 new equality nor does it seem right to create a new wanted goal
1835 (because the goal will most likely contain untouchables, which
1836 can't be solved anyway)!
1838 Note that we *do* fire the improvement if one is Given and one is Derived.
1839 The latter can be a superclass of a wanted goal. Example (tcfail138)
1840 class L a b | a -> b
1841 class (G a, L a b) => C a b
1843 instance C a b' => G (Maybe a)
1844 instance C a b => C (Maybe a) a
1845 instance L (Maybe a) a
1847 When solving the superclasses of the (C (Maybe a) a) instance, we get
1848 Given: C a b ... and hance by superclasses, (G a, L a b)
1850 Use the instance decl to get
1852 The (C a b') is inert, so we generate its Derived superclasses (L a b'),
1853 and now we need improvement between that derived superclass an the Given (L a b)
1855 Note [Overriding implicit parameters]
1856 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1858 f :: (?x::a) -> Bool -> a
1860 g v = let ?x::Int = 3
1861 in (f v, let ?x::Bool = True in f v)
1863 This should probably be well typed, with
1864 g :: Bool -> (Int, Bool)
1866 So the inner binding for ?x::Bool *overrides* the outer one.
1867 Hence a work-item Given overrides an inert-item Given.
1869 Note [Given constraint that matches an instance declaration]
1870 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1871 What should we do when we discover that one (or more) top-level
1872 instances match a given (or solved) class constraint? We have
1875 1. Reject the program. The reason is that there may not be a unique
1876 best strategy for the solver. Example, from the OutsideIn(X) paper:
1877 instance P x => Q [x]
1878 instance (x ~ y) => R [x] y
1880 wob :: forall a b. (Q [b], R b a) => a -> Int
1882 g :: forall a. Q [a] => [a] -> Int
1885 will generate the impliation constraint:
1886 Q [a] => (Q [beta], R beta [a])
1887 If we react (Q [beta]) with its top-level axiom, we end up with a
1888 (P beta), which we have no way of discharging. On the other hand,
1889 if we react R beta [a] with the top-level we get (beta ~ a), which
1890 is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
1891 now solvable by the given Q [a].
1893 However, this option is restrictive, for instance [Example 3] from
1894 Note [Recursive dictionaries] will fail to work.
1896 2. Ignore the problem, hoping that the situations where there exist indeed
1897 such multiple strategies are rare: Indeed the cause of the previous
1898 problem is that (R [x] y) yields the new work (x ~ y) which can be
1899 *spontaneously* solved, not using the givens.
1901 We are choosing option 2 below but we might consider having a flag as well.
1904 Note [New Wanted Superclass Work]
1905 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1906 Even in the case of wanted constraints, we may add some superclasses
1907 as new given work. The reason is:
1909 To allow FD-like improvement for type families. Assume that
1911 class C a b | a -> b
1912 and we have to solve the implication constraint:
1914 Then, FD improvement can help us to produce a new wanted (beta ~ b)
1916 We want to have the same effect with the type family encoding of
1917 functional dependencies. Namely, consider:
1918 class (F a ~ b) => C a b
1919 Now suppose that we have:
1922 By interacting the given we will get given (F a ~ b) which is not
1923 enough by itself to make us discharge (C a beta). However, we
1924 may create a new derived equality from the super-class of the
1925 wanted constraint (C a beta), namely derived (F a ~ beta).
1926 Now we may interact this with given (F a ~ b) to get:
1928 But 'beta' is a touchable unification variable, and hence OK to
1929 unify it with 'b', replacing the derived evidence with the identity.
1931 This requires trySpontaneousSolve to solve *derived*
1932 equalities that have a touchable in their RHS, *in addition*
1933 to solving wanted equalities.
1935 We also need to somehow use the superclasses to quantify over a minimal,
1936 constraint see note [Minimize by Superclasses] in TcSimplify.
1939 Finally, here is another example where this is useful.
1943 class (F a ~ b) => C a b
1944 And we are given the wanteds:
1948 We surely do *not* want to quantify over (b ~ c), since if someone provides
1949 dictionaries for (C a b) and (C a c), these dictionaries can provide a proof
1950 of (b ~ c), hence no extra evidence is necessary. Here is what will happen:
1952 Step 1: We will get new *given* superclass work,
1953 provisionally to our solving of w1 and w2
1955 g1: F a ~ b, g2 : F a ~ c,
1956 w1 : C a b, w2 : C a c, w3 : b ~ c
1958 The evidence for g1 and g2 is a superclass evidence term:
1960 g1 := sc w1, g2 := sc w2
1962 Step 2: The givens will solve the wanted w3, so that
1963 w3 := sym (sc w1) ; sc w2
1965 Step 3: Now, one may naively assume that then w2 can be solve from w1
1966 after rewriting with the (now solved equality) (b ~ c).
1968 But this rewriting is ruled out by the isGoodRectDict!
1970 Conclusion, we will (correctly) end up with the unsolved goals
1973 NB: The desugarer needs be more clever to deal with equalities
1974 that participate in recursive dictionary bindings.
1977 data LookupInstResult
1979 | GenInst [WantedEvVar] EvTerm
1981 matchClassInst :: Class -> [Type] -> WantedLoc -> TcS LookupInstResult
1982 matchClassInst clas tys loc
1983 = do { let pred = mkClassPred clas tys
1984 ; mb_result <- matchClass clas tys
1986 MatchInstNo -> return NoInstance
1987 MatchInstMany -> return NoInstance -- defer any reactions of a multitude until
1988 -- we learn more about the reagent
1989 MatchInstSingle (dfun_id, mb_inst_tys) ->
1990 do { checkWellStagedDFun pred dfun_id loc
1992 -- It's possible that not all the tyvars are in
1993 -- the substitution, tenv. For example:
1994 -- instance C X a => D X where ...
1995 -- (presumably there's a functional dependency in class C)
1996 -- Hence mb_inst_tys :: Either TyVar TcType
1998 ; tys <- instDFunTypes mb_inst_tys
1999 ; let (theta, _) = tcSplitPhiTy (applyTys (idType dfun_id) tys)
2000 ; if null theta then
2001 return (GenInst [] (EvDFunApp dfun_id tys []))
2003 { ev_vars <- instDFunConstraints theta
2004 ; let wevs = [EvVarX w loc | w <- ev_vars]
2005 ; return $ GenInst wevs (EvDFunApp dfun_id tys ev_vars) }