3 solveInteract, AtomicInert, tyVarsOfInert,
4 InertSet, emptyInert, updInertSet, extractUnsolved, solveOne, foldISEqCts
7 #include "HsVersions.h"
28 import Control.Monad ( when )
37 import qualified Data.Map as Map
39 import Control.Monad( unless )
40 import FastString ( sLit )
44 Note [InertSet invariants]
45 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
46 An InertSet is a bag of canonical constraints, with the following invariants:
48 1 No two constraints react with each other.
50 A tricky case is when there exists a given (solved) dictionary
51 constraint and a wanted identical constraint in the inert set, but do
52 not react because reaction would create loopy dictionary evidence for
53 the wanted. See note [Recursive dictionaries]
55 2 Given equalities form an idempotent substitution [none of the
56 given LHS's occur in any of the given RHS's or reactant parts]
58 3 Wanted equalities also form an idempotent substitution
60 4 The entire set of equalities is acyclic.
62 5 Wanted dictionaries are inert with the top-level axiom set
64 6 Equalities of the form tv1 ~ tv2 always have a touchable variable
65 on the left (if possible).
67 7 No wanted constraints tv1 ~ tv2 with tv1 touchable. Such constraints
68 will be marked as solved right before being pushed into the inert set.
69 See note [Touchables and givens].
71 8 No Given constraint mentions a touchable unification variable,
74 Note that 6 and 7 are /not/ enforced by canonicalization but rather by
75 insertion in the inert list, ie by TcInteract.
77 During the process of solving, the inert set will contain some
78 previously given constraints, some wanted constraints, and some given
79 constraints which have arisen from solving wanted constraints. For
80 now we do not distinguish between given and solved constraints.
82 Note that we must switch wanted inert items to given when going under an
83 implication constraint (when in top-level inference mode).
87 data CCanMap a = CCanMap { cts_givder :: Map.Map a CanonicalCts
88 -- Invariant: all Given or Derived
89 , cts_wanted :: Map.Map a CanonicalCts }
90 -- Invariant: all Wanted
91 cCanMapToBag :: Ord a => CCanMap a -> CanonicalCts
92 cCanMapToBag cmap = Map.fold unionBags rest_cts (cts_givder cmap)
93 where rest_cts = Map.fold unionBags emptyCCan (cts_wanted cmap)
95 emptyCCanMap :: CCanMap a
96 emptyCCanMap = CCanMap { cts_givder = Map.empty, cts_wanted = Map.empty }
98 updCCanMap:: Ord a => (a,CanonicalCt) -> CCanMap a -> CCanMap a
99 updCCanMap (a,ct) cmap
100 = case cc_flavor ct of
102 -> cmap { cts_wanted = Map.insertWith unionBags a this_ct (cts_wanted cmap) }
104 -> cmap { cts_givder = Map.insertWith unionBags a this_ct (cts_givder cmap) }
105 where this_ct = singleCCan ct
107 getRelevantCts :: Ord a => a -> CCanMap a -> (CanonicalCts, CCanMap a)
108 -- Gets the relevant constraints and returns the rest of the CCanMap
109 getRelevantCts a cmap
110 = let relevant = unionBags (Map.findWithDefault emptyCCan a (cts_wanted cmap))
111 (Map.findWithDefault emptyCCan a (cts_givder cmap))
112 residual_map = cmap { cts_wanted = Map.delete a (cts_wanted cmap)
113 , cts_givder = Map.delete a (cts_givder cmap) }
114 in (relevant, residual_map)
116 extractUnsolvedCMap :: Ord a => CCanMap a -> (CanonicalCts, CCanMap a)
117 -- Gets the wanted constraints and returns a residual CCanMap
118 extractUnsolvedCMap cmap =
119 let unsolved = Map.fold unionBags emptyCCan (cts_wanted cmap)
120 in (unsolved, cmap { cts_wanted = Map.empty})
122 -- See Note [InertSet invariants]
124 = IS { inert_eqs :: CanonicalCts -- Equalities only (CTyEqCan)
126 , inert_dicts :: CCanMap Class -- Dictionaries only
127 , inert_ips :: CCanMap (IPName Name) -- Implicit parameters
128 , inert_funeqs :: CCanMap TyCon -- Type family equalities only
129 -- This representation allows us to quickly get to the relevant
130 -- inert constraints when interacting a work item with the inert set.
133 , inert_fds :: FDImprovements -- List of pairwise improvements that have kicked in already
134 -- and reside either in the worklist or in the inerts
137 tyVarsOfInert :: InertSet -> TcTyVarSet
138 tyVarsOfInert (IS { inert_eqs = eqs
139 , inert_dicts = dictmap
141 , inert_funeqs = funeqmap }) = tyVarsOfCanonicals cts
142 where cts = eqs `andCCan` cCanMapToBag dictmap
143 `andCCan` cCanMapToBag ipmap `andCCan` cCanMapToBag funeqmap
145 type FDImprovement = (PredType,PredType)
146 type FDImprovements = [(PredType,PredType)]
148 instance Outputable InertSet where
149 ppr is = vcat [ vcat (map ppr (Bag.bagToList $ inert_eqs is))
150 , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_dicts is)))
151 , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_ips is)))
152 , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_funeqs is)))
155 emptyInert :: InertSet
156 emptyInert = IS { inert_eqs = Bag.emptyBag
157 , inert_dicts = emptyCCanMap
158 , inert_ips = emptyCCanMap
159 , inert_funeqs = emptyCCanMap
162 updInertSet :: InertSet -> AtomicInert -> InertSet
164 | isCTyEqCan item -- Other equality
165 = let eqs' = inert_eqs is `Bag.snocBag` item
166 in is { inert_eqs = eqs' }
167 | Just cls <- isCDictCan_Maybe item -- Dictionary
168 = is { inert_dicts = updCCanMap (cls,item) (inert_dicts is) }
169 | Just x <- isCIPCan_Maybe item -- IP
170 = is { inert_ips = updCCanMap (x,item) (inert_ips is) }
171 | Just tc <- isCFunEqCan_Maybe item -- Function equality
172 = is { inert_funeqs = updCCanMap (tc,item) (inert_funeqs is) }
174 = pprPanic "Unknown form of constraint!" (ppr item)
176 updInertSetFDImprs :: InertSet -> Maybe FDImprovement -> InertSet
177 updInertSetFDImprs is (Just fdi) = is { inert_fds = fdi : inert_fds is }
178 updInertSetFDImprs is Nothing = is
180 foldISEqCtsM :: Monad m => (a -> AtomicInert -> m a) -> a -> InertSet -> m a
181 -- Fold over the equalities of the inerts
182 foldISEqCtsM k z IS { inert_eqs = eqs }
183 = Bag.foldlBagM k z eqs
185 foldISEqCts :: (a -> AtomicInert -> a) -> a -> InertSet -> a
186 foldISEqCts k z IS { inert_eqs = eqs }
187 = Bag.foldlBag k z eqs
189 extractUnsolved :: InertSet -> (InertSet, CanonicalCts)
190 extractUnsolved is@(IS {inert_eqs = eqs})
191 = let is_solved = is { inert_eqs = solved_eqs
192 , inert_dicts = solved_dicts
193 , inert_ips = solved_ips
194 , inert_funeqs = solved_funeqs }
195 in (is_solved, unsolved)
197 where (unsolved_eqs, solved_eqs) = Bag.partitionBag isWantedCt eqs
198 (unsolved_ips, solved_ips) = extractUnsolvedCMap (inert_ips is)
199 (unsolved_dicts, solved_dicts) = extractUnsolvedCMap (inert_dicts is)
200 (unsolved_funeqs, solved_funeqs) = extractUnsolvedCMap (inert_funeqs is)
202 unsolved = unsolved_eqs `unionBags`
203 unsolved_ips `unionBags` unsolved_dicts `unionBags` unsolved_funeqs
205 haveBeenImproved :: FDImprovements -> PredType -> PredType -> Bool
206 haveBeenImproved [] _ _ = False
207 haveBeenImproved ((pty1,pty2):fdimprs) pty1' pty2'
208 | tcEqPred pty1 pty1' && tcEqPred pty2 pty2'
210 | tcEqPred pty1 pty2' && tcEqPred pty2 pty1'
213 = haveBeenImproved fdimprs pty1' pty2'
215 getFDImprovements :: InertSet -> FDImprovements
216 -- Return a list of the improvements that have kicked in so far
217 getFDImprovements = inert_fds
221 {-- DV: This note will go away!
223 Note [Touchables and givens]
224 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
225 Touchable variables will never show up in givens which are inputs to
226 the solver. However, touchables may show up in givens generated by the flattener.
241 which can be put in the inert set. Suppose we also have a wanted
245 We cannot rewrite the given G alpha ~g b using the wanted alpha ~w
246 Int. Instead, after reacting alpha ~w Int with the whole inert set,
247 we observe that we can solve it by unifying alpha with Int, so we mark
248 it as solved and put it back in the *work list*. [We also immediately unify
249 alpha := Int, without telling anyone, see trySpontaneousSolve function, to
250 avoid doing this in the end.]
252 Later, because it is solved (given, in effect), we can use it to rewrite
253 G alpha ~g b to G Int ~g b, which gets put back in the work list. Eventually,
254 we will dispatch the remaining wanted constraints using the top-level axioms.
256 Finally, note that after reacting a wanted equality with the entire inert set
257 we may end up with something like
261 which we should flip around to generate the solved constraint alpha ~s b.
267 %*********************************************************************
269 * Main Interaction Solver *
271 **********************************************************************
275 1. Canonicalise (unary)
276 2. Pairwise interaction (binary)
277 * Take one from work list
278 * Try all pair-wise interactions with each constraint in inert
280 As an optimisation, we prioritize the equalities both in the
281 worklist and in the inerts.
283 3. Try to solve spontaneously for equalities involving touchables
284 4. Top-level interaction (binary wrt top-level)
285 Superclass decomposition belongs in (4), see note [Superclasses]
288 type AtomicInert = CanonicalCt -- constraint pulled from InertSet
289 type WorkItem = CanonicalCt -- constraint pulled from WorkList
291 -- A mixture of Given, Wanted, and Derived constraints.
292 -- We split between equalities and the rest to process equalities first.
293 type WorkList = CanonicalCts
295 unionWorkLists :: WorkList -> WorkList -> WorkList
296 unionWorkLists = andCCan
298 isEmptyWorkList :: WorkList -> Bool
299 isEmptyWorkList = isEmptyCCan
301 emptyWorkList :: WorkList
302 emptyWorkList = emptyCCan
304 workListFromCCan :: CanonicalCt -> WorkList
305 workListFromCCan = singleCCan
307 ------------------------
309 = Stop -- Work item is consumed
310 | ContinueWith WorkItem -- Not consumed
312 instance Outputable StopOrContinue where
313 ppr Stop = ptext (sLit "Stop")
314 ppr (ContinueWith w) = ptext (sLit "ContinueWith") <+> ppr w
316 -- Results after interacting a WorkItem as far as possible with an InertSet
318 = SR { sr_inerts :: InertSet
319 -- The new InertSet to use (REPLACES the old InertSet)
320 , sr_new_work :: WorkList
321 -- Any new work items generated (should be ADDED to the old WorkList)
323 -- sr_stop = Just workitem => workitem is *not* in sr_inerts and
324 -- workitem is inert wrt to sr_inerts
325 , sr_stop :: StopOrContinue
328 instance Outputable StageResult where
329 ppr (SR { sr_inerts = inerts, sr_new_work = work, sr_stop = stop })
330 = ptext (sLit "SR") <+>
331 braces (sep [ ptext (sLit "inerts =") <+> ppr inerts <> comma
332 , ptext (sLit "new work =") <+> ppr work <> comma
333 , ptext (sLit "stop =") <+> ppr stop])
335 type SimplifierStage = WorkItem -> InertSet -> TcS StageResult
337 -- Combine a sequence of simplifier 'stages' to create a pipeline
338 runSolverPipeline :: [(String, SimplifierStage)]
339 -> InertSet -> WorkItem
340 -> TcS (InertSet, WorkList)
341 -- Precondition: non-empty list of stages
342 runSolverPipeline pipeline inerts workItem
343 = do { traceTcS "Start solver pipeline" $
344 vcat [ ptext (sLit "work item =") <+> ppr workItem
345 , ptext (sLit "inerts =") <+> ppr inerts]
347 ; let itr_in = SR { sr_inerts = inerts
348 , sr_new_work = emptyWorkList
349 , sr_stop = ContinueWith workItem }
350 ; itr_out <- run_pipeline pipeline itr_in
352 = case sr_stop itr_out of
353 Stop -> sr_inerts itr_out
354 ContinueWith item -> sr_inerts itr_out `updInertSet` item
355 ; return (new_inert, sr_new_work itr_out) }
357 run_pipeline :: [(String, SimplifierStage)]
358 -> StageResult -> TcS StageResult
359 run_pipeline [] itr = return itr
360 run_pipeline _ itr@(SR { sr_stop = Stop }) = return itr
362 run_pipeline ((name,stage):stages)
363 (SR { sr_new_work = accum_work
365 , sr_stop = ContinueWith work_item })
366 = do { itr <- stage work_item inerts
367 ; traceTcS ("Stage result (" ++ name ++ ")") (ppr itr)
368 ; let itr' = itr { sr_new_work = accum_work `unionWorkLists` sr_new_work itr }
369 ; run_pipeline stages itr' }
373 Inert: {c ~ d, F a ~ t, b ~ Int, a ~ ty} (all given)
374 Reagent: a ~ [b] (given)
376 React with (c~d) ==> IR (ContinueWith (a~[b])) True []
377 React with (F a ~ t) ==> IR (ContinueWith (a~[b])) False [F [b] ~ t]
378 React with (b ~ Int) ==> IR (ContinueWith (a~[Int]) True []
381 Inert: {c ~w d, F a ~g t, b ~w Int, a ~w ty}
384 React with (c ~w d) ==> IR (ContinueWith (a~[b])) True []
385 React with (F a ~g t) ==> IR (ContinueWith (a~[b])) True [] (can't rewrite given with wanted!)
389 Inert: {a ~ Int, F Int ~ b} (given)
390 Reagent: F a ~ b (wanted)
392 React with (a ~ Int) ==> IR (ContinueWith (F Int ~ b)) True []
393 React with (F Int ~ b) ==> IR Stop True [] -- after substituting we re-canonicalize and get nothing
396 -- Main interaction solver: we fully solve the worklist 'in one go',
397 -- returning an extended inert set.
399 -- See Note [Touchables and givens].
400 solveInteract :: InertSet -> CanonicalCts -> TcS InertSet
401 solveInteract inert ws
402 = do { dyn_flags <- getDynFlags
403 ; solveInteractWithDepth (ctxtStkDepth dyn_flags,0,[]) inert ws
405 solveOne :: InertSet -> WorkItem -> TcS InertSet
406 solveOne inerts workItem
407 = do { dyn_flags <- getDynFlags
408 ; solveOneWithDepth (ctxtStkDepth dyn_flags,0,[]) inerts workItem
412 solveInteractWithDepth :: (Int, Int, [WorkItem])
413 -> InertSet -> WorkList -> TcS InertSet
414 solveInteractWithDepth ctxt@(max_depth,n,stack) inert ws
419 = solverDepthErrorTcS n stack
422 = do { traceTcS "solveInteractWithDepth" $
423 vcat [ text "Current depth =" <+> ppr n
424 , text "Max depth =" <+> ppr max_depth ]
426 -- Solve equalities first
427 ; let (eqs, non_eqs) = Bag.partitionBag isCTyEqCan ws
428 ; is_from_eqs <- Bag.foldlBagM (solveOneWithDepth ctxt) inert eqs
429 ; Bag.foldlBagM (solveOneWithDepth ctxt) is_from_eqs non_eqs }
432 -- Fully interact the given work item with an inert set, and return a
433 -- new inert set which has assimilated the new information.
434 solveOneWithDepth :: (Int, Int, [WorkItem])
435 -> InertSet -> WorkItem -> TcS InertSet
436 solveOneWithDepth (max_depth, n, stack) inert work
437 = do { traceTcS0 (indent ++ "Solving {") (ppr work)
438 ; (new_inert, new_work) <- runSolverPipeline thePipeline inert work
440 ; traceTcS0 (indent ++ "Subgoals:") (ppr new_work)
442 -- Recursively solve the new work generated
443 -- from workItem, with a greater depth
444 ; res_inert <- solveInteractWithDepth (max_depth, n+1, work:stack)
447 ; traceTcS0 (indent ++ "Done }") (ppr work)
450 indent = replicate (2*n) ' '
452 thePipeline :: [(String,SimplifierStage)]
453 thePipeline = [ ("interact with inert eqs", interactWithInertEqsStage)
454 , ("interact with inerts", interactWithInertsStage)
455 , ("spontaneous solve", spontaneousSolveStage)
456 , ("top-level reactions", topReactionsStage) ]
459 *********************************************************************************
461 The spontaneous-solve Stage
463 *********************************************************************************
465 Note [Efficient Orientation]
466 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
468 There are two cases where we have to be careful about
469 orienting equalities to get better efficiency.
471 Case 1: In Rewriting Equalities (function rewriteEqLHS)
473 When rewriting two equalities with the same LHS:
476 We have a choice of producing work (xi1 ~ xi2) (up-to the
477 canonicalization invariants) However, to prevent the inert items
478 from getting kicked out of the inerts first, we prefer to
479 canonicalize (xi1 ~ xi2) if (b) comes from the inert set, or (xi2
480 ~ xi1) if (a) comes from the inert set.
482 This choice is implemented using the WhichComesFromInert flag.
484 Case 2: Functional Dependencies
485 Again, we should prefer, if possible, the inert variables on the RHS
487 Case 3: IP improvement work
488 We must always rewrite so that the inert type is on the right.
491 spontaneousSolveStage :: SimplifierStage
492 spontaneousSolveStage workItem inerts
493 = do { mSolve <- trySpontaneousSolve workItem
496 SPCantSolve -> -- No spontaneous solution for him, keep going
497 return $ SR { sr_new_work = emptyWorkList
499 , sr_stop = ContinueWith workItem }
502 | not (isGivenCt workItem)
503 -- Original was wanted or derived but we have now made him
504 -- given so we have to interact him with the inerts due to
505 -- its status change. This in turn may produce more work.
506 -- We do this *right now* (rather than just putting workItem'
507 -- back into the work-list) because we've solved
508 -> do { (new_inert, new_work) <- runSolverPipeline
509 [ ("recursive interact with inert eqs", interactWithInertEqsStage)
510 , ("recursive interact with inerts", interactWithInertsStage)
512 ; return $ SR { sr_new_work = new_work
513 , sr_inerts = new_inert -- will include workItem'
517 -> -- Original was given; he must then be inert all right, and
518 -- workList' are all givens from flattening
519 return $ SR { sr_new_work = emptyWorkList
520 , sr_inerts = inerts `updInertSet` workItem'
522 SPError -> -- Return with no new work
523 return $ SR { sr_new_work = emptyWorkList
528 data SPSolveResult = SPCantSolve | SPSolved WorkItem | SPError
529 -- SPCantSolve means that we can't do the unification because e.g. the variable is untouchable
530 -- SPSolved workItem' gives us a new *given* to go on
531 -- SPError means that it's completely impossible to solve this equality, eg due to a kind error
534 -- @trySpontaneousSolve wi@ solves equalities where one side is a
535 -- touchable unification variable.
536 -- See Note [Touchables and givens]
537 trySpontaneousSolve :: WorkItem -> TcS SPSolveResult
538 trySpontaneousSolve workItem@(CTyEqCan { cc_id = cv, cc_flavor = gw, cc_tyvar = tv1, cc_rhs = xi })
541 | Just tv2 <- tcGetTyVar_maybe xi
542 = do { tch1 <- isTouchableMetaTyVar tv1
543 ; tch2 <- isTouchableMetaTyVar tv2
544 ; case (tch1, tch2) of
545 (True, True) -> trySpontaneousEqTwoWay cv gw tv1 tv2
546 (True, False) -> trySpontaneousEqOneWay cv gw tv1 xi
547 (False, True) -> trySpontaneousEqOneWay cv gw tv2 (mkTyVarTy tv1)
548 _ -> return SPCantSolve }
550 = do { tch1 <- isTouchableMetaTyVar tv1
551 ; if tch1 then trySpontaneousEqOneWay cv gw tv1 xi
552 else do { traceTcS "Untouchable LHS, can't spontaneously solve workitem:" (ppr workItem)
553 ; return SPCantSolve }
557 -- trySpontaneousSolve (CFunEqCan ...) = ...
558 -- See Note [No touchables as FunEq RHS] in TcSMonad
559 trySpontaneousSolve _ = return SPCantSolve
562 trySpontaneousEqOneWay :: CoVar -> CtFlavor -> TcTyVar -> Xi -> TcS SPSolveResult
563 -- tv is a MetaTyVar, not untouchable
564 trySpontaneousEqOneWay cv gw tv xi
565 | not (isSigTyVar tv) || isTyVarTy xi
566 = do { let kxi = typeKind xi -- NB: 'xi' is fully rewritten according to the inerts
567 -- so we have its more specific kind in our hands
568 ; if kxi `isSubKind` tyVarKind tv then
569 solveWithIdentity cv gw tv xi
570 else if tyVarKind tv `isSubKind` kxi then
571 return SPCantSolve -- kinds are compatible but we can't solveWithIdentity this way
572 -- This case covers the a_touchable :: * ~ b_untouchable :: ??
573 -- which has to be deferred or floated out for someone else to solve
574 -- it in a scope where 'b' is no longer untouchable.
575 else do { addErrorTcS KindError gw (mkTyVarTy tv) xi -- See Note [Kind errors]
578 | otherwise -- Still can't solve, sig tyvar and non-variable rhs
582 trySpontaneousEqTwoWay :: CoVar -> CtFlavor -> TcTyVar -> TcTyVar -> TcS SPSolveResult
583 -- Both tyvars are *touchable* MetaTyvars so there is only a chance for kind error here
584 trySpontaneousEqTwoWay cv gw tv1 tv2
586 , nicer_to_update_tv2 = solveWithIdentity cv gw tv2 (mkTyVarTy tv1)
588 = solveWithIdentity cv gw tv1 (mkTyVarTy tv2)
589 | otherwise -- None is a subkind of the other, but they are both touchable!
590 = do { addErrorTcS KindError gw (mkTyVarTy tv1) (mkTyVarTy tv2)
595 nicer_to_update_tv2 = isSigTyVar tv1 || isSystemName (Var.varName tv2)
599 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
600 Consider the wanted problem:
601 alpha ~ (# Int, Int #)
602 where alpha :: ?? and (# Int, Int #) :: (#). We can't spontaneously solve this constraint,
603 but we should rather reject the program that give rise to it. If 'trySpontaneousEqTwoWay'
604 simply returns @CantSolve@ then that wanted constraint is going to propagate all the way and
605 get quantified over in inference mode. That's bad because we do know at this point that the
606 constraint is insoluble. Instead, we call 'recKindErrorTcS' here, which will fail later on.
608 The same applies in canonicalization code in case of kind errors in the givens.
610 However, when we canonicalize givens we only check for compatibility (@compatKind@).
611 If there were a kind error in the givens, this means some form of inconsistency or dead code.
613 You may think that when we spontaneously solve wanteds we may have to look through the
614 bindings to determine the right kind of the RHS type. E.g one may be worried that xi is
615 @alpha@ where alpha :: ? and a previous spontaneous solving has set (alpha := f) with (f :: *).
616 But we orient our constraints so that spontaneously solved ones can rewrite all other constraint
617 so this situation can't happen.
619 Note [Spontaneous solving and kind compatibility]
620 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
622 Note that our canonical constraints insist that only *given* equalities (tv ~ xi)
623 or (F xis ~ rhs) require the LHS and the RHS to have exactly the same kinds.
625 - We have to require this because:
626 Given equalities can be freely used to rewrite inside
627 other types or constraints.
628 - We do not have to do the same for wanteds because:
629 First, wanted equations (tv ~ xi) where tv is a touchable
630 unification variable may have kinds that do not agree (the
631 kind of xi must be a sub kind of the kind of tv). Second, any
632 potential kind mismatch will result in the constraint not
633 being soluble, which will be reported anyway. This is the
634 reason that @trySpontaneousOneWay@ and @trySpontaneousTwoWay@
635 will perform a kind compatibility check, and only then will
636 they proceed to @solveWithIdentity@.
639 - Givens from higher-rank, such as:
640 type family T b :: * -> * -> *
641 type instance T Bool = (->)
643 f :: forall a. ((T a ~ (->)) => ...) -> a -> ...
645 Whereas we would be able to apply the type instance, we would not be able to
646 use the given (T Bool ~ (->)) in the body of 'flop'
649 Note [Avoid double unifications]
650 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
651 The spontaneous solver has to return a given which mentions the unified unification
652 variable *on the left* of the equality. Here is what happens if not:
653 Original wanted: (a ~ alpha), (alpha ~ Int)
654 We spontaneously solve the first wanted, without changing the order!
655 given : a ~ alpha [having unified alpha := a]
656 Now the second wanted comes along, but he cannot rewrite the given, so we simply continue.
657 At the end we spontaneously solve that guy, *reunifying* [alpha := Int]
659 We avoid this problem by orienting the resulting given so that the unification
660 variable is on the left. [Note that alternatively we could attempt to
661 enforce this at canonicalization]
663 See also Note [No touchables as FunEq RHS] in TcSMonad; avoiding
664 double unifications is the main reason we disallow touchable
665 unification variables as RHS of type family equations: F xis ~ alpha.
670 solveWithIdentity :: CoVar -> CtFlavor -> TcTyVar -> Xi -> TcS SPSolveResult
671 -- Solve with the identity coercion
672 -- Precondition: kind(xi) is a sub-kind of kind(tv)
673 -- Precondition: CtFlavor is Wanted or Derived
674 -- See [New Wanted Superclass Work] to see why solveWithIdentity
675 -- must work for Derived as well as Wanted
676 -- Returns: workItem where
677 -- workItem = the new Given constraint
678 solveWithIdentity cv wd tv xi
679 = do { traceTcS "Sneaky unification:" $
680 vcat [text "Coercion variable: " <+> ppr wd,
681 text "Coercion: " <+> pprEq (mkTyVarTy tv) xi,
682 text "Left Kind is : " <+> ppr (typeKind (mkTyVarTy tv)),
683 text "Right Kind is : " <+> ppr (typeKind xi)
686 ; setWantedTyBind tv xi -- Set tv := xi_unflat
687 ; cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi xi
689 ; case wd of Wanted {} -> setWantedCoBind cv xi
690 Derived {} -> setDerivedCoBind cv xi
691 _ -> pprPanic "Can't spontaneously solve given!" empty
693 ; return $ SPSolved (CTyEqCan { cc_id = cv_given
694 , cc_flavor = mkGivenFlavor wd UnkSkol
695 , cc_tyvar = tv, cc_rhs = xi })
703 *********************************************************************************
705 The interact-with-inert Stage
707 *********************************************************************************
710 -- Interaction result of WorkItem <~> AtomicInert
712 = IR { ir_stop :: StopOrContinue
714 -- => Reagent (work item) consumed.
715 -- ContinueWith new_reagent
716 -- => Reagent transformed but keep gathering interactions.
717 -- The transformed item remains inert with respect
718 -- to any previously encountered inerts.
720 , ir_inert_action :: InertAction
721 -- Whether the inert item should remain in the InertSet.
723 , ir_new_work :: WorkList
724 -- new work items to add to the WorkList
726 , ir_improvement :: Maybe FDImprovement -- In case improvement kicked in
729 -- What to do with the inert reactant.
730 data InertAction = KeepInert
732 | KeepTransformedInert CanonicalCt -- Keep a slightly transformed inert
734 mkIRContinue :: Monad m => WorkItem -> InertAction -> WorkList -> m InteractResult
735 mkIRContinue wi keep newWork = return $ IR (ContinueWith wi) keep newWork Nothing
737 mkIRStop :: Monad m => InertAction -> WorkList -> m InteractResult
738 mkIRStop keep newWork = return $ IR Stop keep newWork Nothing
740 mkIRStop_RecordImprovement :: Monad m => InertAction -> WorkList -> FDImprovement -> m InteractResult
741 mkIRStop_RecordImprovement keep newWork fdimpr = return $ IR Stop keep newWork (Just fdimpr)
743 dischargeWorkItem :: Monad m => m InteractResult
744 dischargeWorkItem = mkIRStop KeepInert emptyWorkList
746 noInteraction :: Monad m => WorkItem -> m InteractResult
747 noInteraction workItem = mkIRContinue workItem KeepInert emptyWorkList
749 data WhichComesFromInert = LeftComesFromInert | RightComesFromInert
750 -- See Note [Efficient Orientation]
753 ---------------------------------------------------
754 -- Interact a single WorkItem with the equalities of an inert set as far as possible, i.e. until we
755 -- get a Stop result from an individual reaction (i.e. when the WorkItem is consumed), or until we've
756 -- interact the WorkItem with the entire equalities of the InertSet
758 interactWithInertEqsStage :: SimplifierStage
759 interactWithInertEqsStage workItem inert
760 = foldISEqCtsM interactNext initITR inert
761 where initITR = SR { sr_inerts = IS { inert_eqs = emptyCCan -- Will fold over equalities
762 , inert_dicts = inert_dicts inert
763 , inert_ips = inert_ips inert
764 , inert_funeqs = inert_funeqs inert
765 , inert_fds = inert_fds inert
767 , sr_new_work = emptyWorkList
768 , sr_stop = ContinueWith workItem }
771 ---------------------------------------------------
772 -- Interact a single WorkItem with *non-equality* constraints in the inert set.
773 -- Precondition: equality interactions must have already happened, hence we have
774 -- to pick up some information from the incoming inert, before folding over the
775 -- "Other" constraints it contains!
777 interactWithInertsStage :: SimplifierStage
778 interactWithInertsStage workItem inert
779 = let (relevant, inert_residual) = getISRelevant workItem inert
780 initITR = SR { sr_inerts = inert_residual
781 , sr_new_work = emptyWorkList
782 , sr_stop = ContinueWith workItem }
783 in Bag.foldlBagM interactNext initITR relevant
785 getISRelevant :: CanonicalCt -> InertSet -> (CanonicalCts, InertSet)
786 getISRelevant (CDictCan { cc_class = cls } ) is
787 = let (relevant, residual_map) = getRelevantCts cls (inert_dicts is)
788 in (relevant, is { inert_dicts = residual_map })
789 getISRelevant (CFunEqCan { cc_fun = tc } ) is
790 = let (relevant, residual_map) = getRelevantCts tc (inert_funeqs is)
791 in (relevant, is { inert_funeqs = residual_map })
792 getISRelevant (CIPCan { cc_ip_nm = nm }) is
793 = let (relevant, residual_map) = getRelevantCts nm (inert_ips is)
794 in (relevant, is { inert_ips = residual_map })
795 -- An equality, finally, may kick everything except equalities out
796 -- because we have already interacted the equalities in interactWithInertEqsStage
797 getISRelevant _eq_ct is -- Equality, everything is relevant for this one
798 -- TODO: if we were caching variables, we'd know that only
799 -- some are relevant. Experiment with this for now.
800 = let cts = cCanMapToBag (inert_ips is) `unionBags`
801 cCanMapToBag (inert_dicts is) `unionBags` cCanMapToBag (inert_funeqs is)
802 in (cts, is { inert_dicts = emptyCCanMap
803 , inert_ips = emptyCCanMap
804 , inert_funeqs = emptyCCanMap })
806 interactNext :: StageResult -> AtomicInert -> TcS StageResult
807 interactNext it inert
808 | ContinueWith workItem <- sr_stop it
809 = do { let inerts = sr_inerts it
810 fdimprs_old = getFDImprovements inerts
812 ; ir <- interactWithInert fdimprs_old inert workItem
814 -- New inerts depend on whether we KeepInert or not and must
815 -- be updated with FD improvement information from the interaction result (ir)
816 ; let inerts_new = updInertSetFDImprs upd_inert (ir_improvement ir)
817 upd_inert = case ir_inert_action ir of
818 KeepInert -> inerts `updInertSet` inert
820 KeepTransformedInert inert' -> inerts `updInertSet` inert'
822 ; return $ SR { sr_inerts = inerts_new
823 , sr_new_work = sr_new_work it `unionWorkLists` ir_new_work ir
824 , sr_stop = ir_stop ir } }
826 = return $ it { sr_inerts = (sr_inerts it) `updInertSet` inert }
828 -- Do a single interaction of two constraints.
829 interactWithInert :: FDImprovements -> AtomicInert -> WorkItem -> TcS InteractResult
830 interactWithInert fdimprs inert workitem
831 = do { ctxt <- getTcSContext
832 ; let is_allowed = allowedInteraction (simplEqsOnly ctxt) inert workitem
833 inert_ev = cc_id inert
834 work_ev = cc_id workitem
836 -- Never interact a wanted and a derived where the derived's evidence
837 -- mentions the wanted evidence in an unguarded way.
838 -- See Note [Superclasses and recursive dictionaries]
839 -- and Note [New Wanted Superclass Work]
840 -- We don't have to do this for givens, as we fully know the evidence for them.
842 case (cc_flavor inert, cc_flavor workitem) of
843 (Wanted {}, Derived {}) -> isGoodRecEv work_ev inert_ev
844 (Derived {}, Wanted {}) -> isGoodRecEv inert_ev work_ev
847 ; if is_allowed && rec_ev_ok then
848 doInteractWithInert fdimprs inert workitem
850 noInteraction workitem
853 allowedInteraction :: Bool -> AtomicInert -> WorkItem -> Bool
854 -- Allowed interactions
855 allowedInteraction eqs_only (CDictCan {}) (CDictCan {}) = not eqs_only
856 allowedInteraction eqs_only (CIPCan {}) (CIPCan {}) = not eqs_only
857 allowedInteraction _ _ _ = True
859 --------------------------------------------
860 doInteractWithInert :: FDImprovements -> CanonicalCt -> CanonicalCt -> TcS InteractResult
861 -- Identical class constraints.
863 doInteractWithInert fdimprs
864 (CDictCan { cc_id = d1, cc_flavor = fl1, cc_class = cls1, cc_tyargs = tys1 })
865 workItem@(CDictCan { cc_flavor = fl2, cc_class = cls2, cc_tyargs = tys2 })
866 | cls1 == cls2 && (and $ zipWith tcEqType tys1 tys2)
867 = solveOneFromTheOther (d1,fl1) workItem
869 | cls1 == cls2 && (not (isGiven fl1 && isGiven fl2))
870 = -- See Note [When improvement happens]
871 do { let pty1 = ClassP cls1 tys1
872 pty2 = ClassP cls2 tys2
873 work_item_pred_loc = (pty2, pprFlavorArising fl2)
874 inert_pred_loc = (pty1, pprFlavorArising fl1)
875 loc = combineCtLoc fl1 fl2
876 eqn_pred_locs = improveFromAnother work_item_pred_loc inert_pred_loc
877 -- See Note [Efficient Orientation]
879 ; wevvars <- mkWantedFunDepEqns loc eqn_pred_locs
880 ; fd_work <- canWanteds wevvars
881 -- See Note [Generating extra equalities]
882 ; traceTcS "Checking if improvements existed." (ppr fdimprs)
883 ; if isEmptyWorkList fd_work || haveBeenImproved fdimprs pty1 pty2 then
885 mkIRContinue workItem KeepInert fd_work
886 else do { traceTcS "Recording improvement and throwing item back in worklist." (ppr (pty1,pty2))
887 ; mkIRStop_RecordImprovement KeepInert
888 (fd_work `unionWorkLists` workListFromCCan workItem) (pty1,pty2)
890 -- See Note [FunDep Reactions]
893 -- Class constraint and given equality: use the equality to rewrite
894 -- the class constraint.
895 doInteractWithInert _fdimprs
896 (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi })
897 (CDictCan { cc_id = dv, cc_flavor = wfl, cc_class = cl, cc_tyargs = xis })
898 | ifl `canRewrite` wfl
899 , tv `elemVarSet` tyVarsOfTypes xis
900 = do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,wfl,cl,xis)
901 -- Continue with rewritten Dictionary because we can only be in the
902 -- interactWithEqsStage, so the dictionary is inert.
903 ; mkIRContinue rewritten_dict KeepInert emptyWorkList }
905 doInteractWithInert _fdimprs
906 (CDictCan { cc_id = dv, cc_flavor = ifl, cc_class = cl, cc_tyargs = xis })
907 workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
908 | wfl `canRewrite` ifl
909 , tv `elemVarSet` tyVarsOfTypes xis
910 = do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,ifl,cl,xis)
911 ; mkIRContinue workItem DropInert (workListFromCCan rewritten_dict) }
913 -- Class constraint and given equality: use the equality to rewrite
914 -- the class constraint.
915 doInteractWithInert _fdimprs
916 (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi })
917 (CIPCan { cc_id = ipid, cc_flavor = wfl, cc_ip_nm = nm, cc_ip_ty = ty })
918 | ifl `canRewrite` wfl
919 , tv `elemVarSet` tyVarsOfType ty
920 = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,wfl,nm,ty)
921 ; mkIRContinue rewritten_ip KeepInert emptyWorkList }
923 doInteractWithInert _fdimprs
924 (CIPCan { cc_id = ipid, cc_flavor = ifl, cc_ip_nm = nm, cc_ip_ty = ty })
925 workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
926 | wfl `canRewrite` ifl
927 , tv `elemVarSet` tyVarsOfType ty
928 = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,ifl,nm,ty)
929 ; mkIRContinue workItem DropInert (workListFromCCan rewritten_ip) }
931 -- Two implicit parameter constraints. If the names are the same,
932 -- but their types are not, we generate a wanted type equality
933 -- that equates the type (this is "improvement").
934 -- However, we don't actually need the coercion evidence,
935 -- so we just generate a fresh coercion variable that isn't used anywhere.
936 doInteractWithInert _fdimprs
937 (CIPCan { cc_id = id1, cc_flavor = ifl, cc_ip_nm = nm1, cc_ip_ty = ty1 })
938 workItem@(CIPCan { cc_flavor = wfl, cc_ip_nm = nm2, cc_ip_ty = ty2 })
939 | nm1 == nm2 && isGiven wfl && isGiven ifl
940 = -- See Note [Overriding implicit parameters]
941 -- Dump the inert item, override totally with the new one
942 -- Do not require type equality
943 mkIRContinue workItem DropInert emptyWorkList
945 | nm1 == nm2 && ty1 `tcEqType` ty2
946 = solveOneFromTheOther (id1,ifl) workItem
949 = -- See Note [When improvement happens]
950 do { co_var <- newWantedCoVar ty2 ty1 -- See Note [Efficient Orientation]
951 ; let flav = Wanted (combineCtLoc ifl wfl)
952 ; cans <- mkCanonical flav co_var
953 ; mkIRContinue workItem KeepInert cans }
957 -- Never rewrite a given with a wanted equality, and a type function
958 -- equality can never rewrite an equality. We rewrite LHS *and* RHS
959 -- of function equalities so that our inert set exposes everything that
960 -- we know about equalities.
962 -- Inert: equality, work item: function equality
963 doInteractWithInert _fdimprs
964 (CTyEqCan { cc_id = cv1, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi1 })
965 (CFunEqCan { cc_id = cv2, cc_flavor = wfl, cc_fun = tc
966 , cc_tyargs = args, cc_rhs = xi2 })
967 | ifl `canRewrite` wfl
968 , tv `elemVarSet` tyVarsOfTypes (xi2:args) -- Rewrite RHS as well
969 = do { rewritten_funeq <- rewriteFunEq (cv1,tv,xi1) (cv2,wfl,tc,args,xi2)
970 ; mkIRStop KeepInert (workListFromCCan rewritten_funeq) }
971 -- Must Stop here, because we may no longer be inert after the rewritting.
973 -- Inert: function equality, work item: equality
974 doInteractWithInert _fdimprs
975 (CFunEqCan {cc_id = cv1, cc_flavor = ifl, cc_fun = tc
976 , cc_tyargs = args, cc_rhs = xi1 })
977 workItem@(CTyEqCan { cc_id = cv2, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi2 })
978 | wfl `canRewrite` ifl
979 , tv `elemVarSet` tyVarsOfTypes (xi1:args) -- Rewrite RHS as well
980 = do { rewritten_funeq <- rewriteFunEq (cv2,tv,xi2) (cv1,ifl,tc,args,xi1)
981 ; mkIRContinue workItem DropInert (workListFromCCan rewritten_funeq) }
982 -- One may think that we could (KeepTransformedInert rewritten_funeq)
983 -- but that is wrong, because it may end up not being inert with respect
984 -- to future inerts. Example:
985 -- Original inert = { F xis ~ [a], b ~ Maybe Int }
986 -- Work item comes along = a ~ [b]
987 -- If we keep { F xis ~ [b] } in the inert set we will end up with:
988 -- { F xis ~ [b], b ~ Maybe Int, a ~ [Maybe Int] }
989 -- At the end, which is *not* inert. So we should unfortunately DropInert here.
991 doInteractWithInert _fdimprs
992 (CFunEqCan { cc_id = cv1, cc_flavor = fl1, cc_fun = tc1
993 , cc_tyargs = args1, cc_rhs = xi1 })
994 workItem@(CFunEqCan { cc_id = cv2, cc_flavor = fl2, cc_fun = tc2
995 , cc_tyargs = args2, cc_rhs = xi2 })
996 | fl1 `canSolve` fl2 && lhss_match
997 = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
998 ; mkIRStop KeepInert cans }
999 | fl2 `canSolve` fl1 && lhss_match
1000 = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
1001 ; mkIRContinue workItem DropInert cans }
1003 lhss_match = tc1 == tc2 && and (zipWith tcEqType args1 args2)
1005 doInteractWithInert _fdimprs
1006 (CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
1007 workItem@(CTyEqCan { cc_id = cv2, cc_flavor = fl2, cc_tyvar = tv2, cc_rhs = xi2 })
1008 -- Check for matching LHS
1009 | fl1 `canSolve` fl2 && tv1 == tv2
1010 = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
1011 ; mkIRStop KeepInert cans }
1013 | fl2 `canSolve` fl1 && tv1 == tv2
1014 = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
1015 ; mkIRContinue workItem DropInert cans }
1016 -- Check for rewriting RHS
1017 | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfType xi2
1018 = do { rewritten_eq <- rewriteEqRHS (cv1,tv1,xi1) (cv2,fl2,tv2,xi2)
1019 ; mkIRStop KeepInert rewritten_eq }
1020 | fl2 `canRewrite` fl1 && tv2 `elemVarSet` tyVarsOfType xi1
1021 = do { rewritten_eq <- rewriteEqRHS (cv2,tv2,xi2) (cv1,fl1,tv1,xi1)
1022 ; mkIRContinue workItem DropInert rewritten_eq }
1024 -- Fall-through case for all other situations
1025 doInteractWithInert _fdimprs _ workItem = noInteraction workItem
1027 -------------------------
1028 -- Equational Rewriting
1029 rewriteDict :: (CoVar, TcTyVar, Xi) -> (DictId, CtFlavor, Class, [Xi]) -> TcS CanonicalCt
1030 rewriteDict (cv,tv,xi) (dv,gw,cl,xis)
1031 = do { let cos = substTysWith [tv] [mkCoVarCoercion cv] xis -- xis[tv] ~ xis[xi]
1032 args = substTysWith [tv] [xi] xis
1034 dict_co = mkTyConCoercion con cos
1035 ; dv' <- newDictVar cl args
1037 Wanted {} -> setDictBind dv (EvCast dv' (mkSymCoercion dict_co))
1038 _given_or_derived -> setDictBind dv' (EvCast dv dict_co)
1039 ; return (CDictCan { cc_id = dv'
1042 , cc_tyargs = args }) }
1044 rewriteIP :: (CoVar,TcTyVar,Xi) -> (EvVar,CtFlavor, IPName Name, TcType) -> TcS CanonicalCt
1045 rewriteIP (cv,tv,xi) (ipid,gw,nm,ty)
1046 = do { let ip_co = substTyWith [tv] [mkCoVarCoercion cv] ty -- ty[tv] ~ t[xi]
1047 ty' = substTyWith [tv] [xi] ty
1048 ; ipid' <- newIPVar nm ty'
1050 Wanted {} -> setIPBind ipid (EvCast ipid' (mkSymCoercion ip_co))
1051 _given_or_derived -> setIPBind ipid' (EvCast ipid ip_co)
1052 ; return (CIPCan { cc_id = ipid'
1055 , cc_ip_ty = ty' }) }
1057 rewriteFunEq :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TyCon, [Xi], Xi) -> TcS CanonicalCt
1058 rewriteFunEq (cv1,tv,xi1) (cv2,gw, tc,args,xi2) -- cv2 :: F args ~ xi2
1059 = do { let arg_cos = substTysWith [tv] [mkCoVarCoercion cv1] args
1060 args' = substTysWith [tv] [xi1] args
1061 fun_co = mkTyConCoercion tc arg_cos -- fun_co :: F args ~ F args'
1063 xi2' = substTyWith [tv] [xi1] xi2
1064 xi2_co = substTyWith [tv] [mkCoVarCoercion cv1] xi2 -- xi2_co :: xi2 ~ xi2'
1065 ; cv2' <- case gw of
1066 Wanted {} -> do { cv2' <- newWantedCoVar (mkTyConApp tc args') xi2'
1067 ; setWantedCoBind cv2 $
1068 fun_co `mkTransCoercion`
1069 mkCoVarCoercion cv2' `mkTransCoercion` mkSymCoercion xi2_co
1071 _giv_or_der -> newGivOrDerCoVar (mkTyConApp tc args') xi2' $
1072 mkSymCoercion fun_co `mkTransCoercion`
1073 mkCoVarCoercion cv2 `mkTransCoercion` xi2_co
1074 ; return (CFunEqCan { cc_id = cv2'
1078 , cc_rhs = xi2' }) }
1081 rewriteEqRHS :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TcTyVar,Xi) -> TcS WorkList
1082 -- Use the first equality to rewrite the second, flavors already checked.
1083 -- E.g. c1 : tv1 ~ xi1 c2 : tv2 ~ xi2
1084 -- rewrites c2 to give
1085 -- c2' : tv2 ~ xi2[xi1/tv1]
1086 -- We must do an occurs check to sure the new constraint is canonical
1087 -- So we might return an empty bag
1088 rewriteEqRHS (cv1,tv1,xi1) (cv2,gw,tv2,xi2)
1089 | Just tv2' <- tcGetTyVar_maybe xi2'
1090 , tv2 == tv2' -- In this case xi2[xi1/tv1] = tv2, so we have tv2~tv2
1091 = do { when (isWanted gw) (setWantedCoBind cv2 (mkSymCoercion co2'))
1092 ; return emptyCCan }
1097 -> do { cv2' <- newWantedCoVar (mkTyVarTy tv2) xi2'
1098 ; setWantedCoBind cv2 $
1099 mkCoVarCoercion cv2' `mkTransCoercion` mkSymCoercion co2'
1102 -> newGivOrDerCoVar (mkTyVarTy tv2) xi2' $
1103 mkCoVarCoercion cv2 `mkTransCoercion` co2'
1105 ; canEq gw cv2' (mkTyVarTy tv2) xi2'
1108 xi2' = substTyWith [tv1] [xi1] xi2
1109 co2' = substTyWith [tv1] [mkCoVarCoercion cv1] xi2 -- xi2 ~ xi2[xi1/tv1]
1112 rewriteEqLHS :: WhichComesFromInert -> (Coercion,Xi) -> (CoVar,CtFlavor,Xi) -> TcS WorkList
1113 -- Used to ineract two equalities of the following form:
1114 -- First Equality: co1: (XXX ~ xi1)
1115 -- Second Equality: cv2: (XXX ~ xi2)
1116 -- Where the cv1 `canSolve` cv2 equality
1117 -- We have an option of creating new work (xi1 ~ xi2) OR (xi2 ~ xi1),
1118 -- See Note [Efficient Orientation] for that
1119 rewriteEqLHS which (co1,xi1) (cv2,gw,xi2)
1120 = do { cv2' <- case (isWanted gw, which) of
1121 (True,LeftComesFromInert) ->
1122 do { cv2' <- newWantedCoVar xi2 xi1
1123 ; setWantedCoBind cv2 $
1124 co1 `mkTransCoercion` mkSymCoercion (mkCoVarCoercion cv2')
1126 (True,RightComesFromInert) ->
1127 do { cv2' <- newWantedCoVar xi1 xi2
1128 ; setWantedCoBind cv2 $
1129 co1 `mkTransCoercion` mkCoVarCoercion cv2'
1131 (False,LeftComesFromInert) ->
1132 newGivOrDerCoVar xi2 xi1 $
1133 mkSymCoercion (mkCoVarCoercion cv2) `mkTransCoercion` co1
1134 (False,RightComesFromInert) ->
1135 newGivOrDerCoVar xi1 xi2 $
1136 mkSymCoercion co1 `mkTransCoercion` mkCoVarCoercion cv2
1137 ; mkCanonical gw cv2'
1140 solveOneFromTheOther :: (EvVar, CtFlavor) -> CanonicalCt -> TcS InteractResult
1141 -- First argument inert, second argument workitem. They both represent
1142 -- wanted/given/derived evidence for the *same* predicate so we try here to
1143 -- discharge one directly from the other.
1145 -- Precondition: value evidence only (implicit parameters, classes)
1147 solveOneFromTheOther (iid,ifl) workItem
1148 -- Both derived needs a special case. You might think that we do not need
1149 -- two evidence terms for the same claim. But, since the evidence is partial,
1150 -- either evidence may do in some cases; see TcSMonad.isGoodRecEv.
1151 -- See also Example 3 in Note [Superclasses and recursive dictionaries]
1152 | isDerived ifl && isDerived wfl
1153 = noInteraction workItem
1155 | ifl `canSolve` wfl
1156 = do { unless (isGiven wfl) $ setEvBind wid (EvId iid)
1157 -- Overwrite the binding, if one exists
1158 -- For Givens, which are lambda-bound, nothing to overwrite,
1159 ; dischargeWorkItem }
1161 | otherwise -- wfl `canSolve` ifl
1162 = do { unless (isGiven ifl) $ setEvBind iid (EvId wid)
1163 ; mkIRContinue workItem DropInert emptyWorkList }
1166 wfl = cc_flavor workItem
1167 wid = cc_id workItem
1170 Note [Superclasses and recursive dictionaries]
1171 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1172 Overlaps with Note [SUPERCLASS-LOOP 1]
1173 Note [SUPERCLASS-LOOP 2]
1174 Note [Recursive instances and superclases]
1175 ToDo: check overlap and delete redundant stuff
1177 Right before adding a given into the inert set, we must
1178 produce some more work, that will bring the superclasses
1179 of the given into scope. The superclass constraints go into
1182 When we simplify a wanted constraint, if we first see a matching
1183 instance, we may produce new wanted work. To (1) avoid doing this work
1184 twice in the future and (2) to handle recursive dictionaries we may ``cache''
1185 this item as solved (in effect, given) into our inert set and with that add
1186 its superclass constraints (as given) in our worklist.
1188 But now we have added partially solved constraints to the worklist which may
1189 interact with other wanteds. Consider the example:
1193 class Eq b => Foo a b --- 0-th selector
1194 instance Eq a => Foo [a] a --- fooDFun
1196 and wanted (Foo [t] t). We are first going to see that the instance matches
1197 and create an inert set that includes the solved (Foo [t] t) and its
1199 d1 :_g Foo [t] t d1 := EvDFunApp fooDFun d3
1200 d2 :_g Eq t d2 := EvSuperClass d1 0
1201 Our work list is going to contain a new *wanted* goal
1203 It is wrong to react the wanted (Eq t) with the given (Eq t) because that would
1204 construct loopy evidence. Hence the check isGoodRecEv in doInteractWithInert.
1206 OK, so we have ruled out bad behaviour, but how do we ge recursive dictionaries,
1211 data D r = ZeroD | SuccD (r (D r));
1213 instance (Eq (r (D r))) => Eq (D r) where
1214 ZeroD == ZeroD = True
1215 (SuccD a) == (SuccD b) = a == b
1218 equalDC :: D [] -> D [] -> Bool;
1221 We need to prove (Eq (D [])). Here's how we go:
1225 by instance decl, holds if
1229 *BUT* we have an inert set which gives us (no superclasses):
1231 By the instance declaration of Eq we can show the 'd2' goal if
1233 where d2 = dfEqList d3
1235 Now, however this wanted can interact with our inert d1 to set:
1237 and solve the goal. Why was this interaction OK? Because, if we chase the
1238 evidence of d1 ~~> dfEqD d2 ~~-> dfEqList d3, so by setting d3 := d1 we
1240 d3 := dfEqD2 (dfEqList d3)
1241 which is FINE because the use of d3 is protected by the instance function
1244 So, our strategy is to try to put solved wanted dictionaries into the
1245 inert set along with their superclasses (when this is meaningful,
1246 i.e. when new wanted goals are generated) but solve a wanted dictionary
1247 from a given only in the case where the evidence variable of the
1248 wanted is mentioned in the evidence of the given (recursively through
1249 the evidence binds) in a protected way: more instance function applications
1250 than superclass selectors.
1252 Here are some more examples from GHC's previous type checker
1256 This code arises in the context of "Scrap Your Boilerplate with Class"
1260 instance Sat (ctx Char) => Data ctx Char -- dfunData1
1261 instance (Sat (ctx [a]), Data ctx a) => Data ctx [a] -- dfunData2
1263 class Data Maybe a => Foo a
1265 instance Foo t => Sat (Maybe t) -- dfunSat
1267 instance Data Maybe a => Foo a -- dfunFoo1
1268 instance Foo a => Foo [a] -- dfunFoo2
1269 instance Foo [Char] -- dfunFoo3
1271 Consider generating the superclasses of the instance declaration
1272 instance Foo a => Foo [a]
1274 So our problem is this
1276 d1 :_w Data Maybe [t]
1278 We may add the given in the inert set, along with its superclasses
1279 [assuming we don't fail because there is a matching instance, see
1280 tryTopReact, given case ]
1284 d01 :_g Data Maybe t -- d2 := EvDictSuperClass d0 0
1285 d1 :_w Data Maybe [t]
1286 Then d2 can readily enter the inert, and we also do solving of the wanted
1289 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1291 d2 :_w Sat (Maybe [t])
1293 d01 :_g Data Maybe t
1294 Now, we may simplify d2 more:
1297 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1298 d1 :_g Data Maybe [t]
1299 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1303 d01 :_g Data Maybe t
1305 Now, we can just solve d3.
1308 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1309 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1312 d01 :_g Data Maybe t
1313 And now we can simplify d4 again, but since it has superclasses we *add* them to the worklist:
1316 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1317 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1318 d4 :_g Foo [t] d4 := dfunFoo2 d5
1321 d6 :_g Data Maybe [t] d6 := EvDictSuperClass d4 0
1322 d01 :_g Data Maybe t
1323 Now, d5 can be solved! (and its superclass enter scope)
1326 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1327 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1328 d4 :_g Foo [t] d4 := dfunFoo2 d5
1329 d5 :_g Foo t d5 := dfunFoo1 d7
1332 d6 :_g Data Maybe [t]
1333 d8 :_g Data Maybe t d8 := EvDictSuperClass d5 0
1334 d01 :_g Data Maybe t
1337 [1] Suppose we pick d8 and we react him with d01. Which of the two givens should
1338 we keep? Well, we *MUST NOT* drop d01 because d8 contains recursive evidence
1339 that must not be used (look at case interactInert where both inert and workitem
1340 are givens). So we have several options:
1341 - Drop the workitem always (this will drop d8)
1342 This feels very unsafe -- what if the work item was the "good" one
1343 that should be used later to solve another wanted?
1344 - Don't drop anyone: the inert set may contain multiple givens!
1345 [This is currently implemented]
1347 The "don't drop anyone" seems the most safe thing to do, so now we come to problem 2:
1348 [2] We have added both d6 and d01 in the inert set, and we are interacting our wanted
1349 d7. Now the [isRecDictEv] function in the ineration solver
1350 [case inert-given workitem-wanted] will prevent us from interacting d7 := d8
1351 precisely because chasing the evidence of d8 leads us to an unguarded use of d7.
1353 So, no interaction happens there. Then we meet d01 and there is no recursion
1354 problem there [isRectDictEv] gives us the OK to interact and we do solve d7 := d01!
1356 Note [SUPERCLASS-LOOP 1]
1357 ~~~~~~~~~~~~~~~~~~~~~~~~
1358 We have to be very, very careful when generating superclasses, lest we
1359 accidentally build a loop. Here's an example:
1363 class S a => C a where { opc :: a -> a }
1364 class S b => D b where { opd :: b -> b }
1366 instance C Int where
1369 instance D Int where
1372 From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int}
1373 Simplifying, we may well get:
1374 $dfCInt = :C ds1 (opd dd)
1377 Notice that we spot that we can extract ds1 from dd.
1379 Alas! Alack! We can do the same for (instance D Int):
1381 $dfDInt = :D ds2 (opc dc)
1385 And now we've defined the superclass in terms of itself.
1386 Two more nasty cases are in
1391 - Satisfy the superclass context *all by itself*
1392 (tcSimplifySuperClasses)
1393 - And do so completely; i.e. no left-over constraints
1394 to mix with the constraints arising from method declarations
1397 Note [SUPERCLASS-LOOP 2]
1398 ~~~~~~~~~~~~~~~~~~~~~~~~
1399 We need to be careful when adding "the constaint we are trying to prove".
1400 Suppose we are *given* d1:Ord a, and want to deduce (d2:C [a]) where
1402 class Ord a => C a where
1403 instance Ord [a] => C [a] where ...
1405 Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the
1406 superclasses of C [a] to avails. But we must not overwrite the binding
1407 for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
1410 Here's another variant, immortalised in tcrun020
1411 class Monad m => C1 m
1412 class C1 m => C2 m x
1413 instance C2 Maybe Bool
1414 For the instance decl we need to build (C1 Maybe), and it's no good if
1415 we run around and add (C2 Maybe Bool) and its superclasses to the avails
1416 before we search for C1 Maybe.
1418 Here's another example
1419 class Eq b => Foo a b
1420 instance Eq a => Foo [a] a
1424 we'll first deduce that it holds (via the instance decl). We must not
1425 then overwrite the Eq t constraint with a superclass selection!
1427 At first I had a gross hack, whereby I simply did not add superclass constraints
1428 in addWanted, though I did for addGiven and addIrred. This was sub-optimal,
1429 becuase it lost legitimate superclass sharing, and it still didn't do the job:
1430 I found a very obscure program (now tcrun021) in which improvement meant the
1431 simplifier got two bites a the cherry... so something seemed to be an Stop
1432 first time, but reducible next time.
1434 Now we implement the Right Solution, which is to check for loops directly
1435 when adding superclasses. It's a bit like the occurs check in unification.
1437 Note [Recursive instances and superclases]
1438 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1439 Consider this code, which arises in the context of "Scrap Your
1440 Boilerplate with Class".
1444 instance Sat (ctx Char) => Data ctx Char
1445 instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]
1447 class Data Maybe a => Foo a
1449 instance Foo t => Sat (Maybe t)
1451 instance Data Maybe a => Foo a
1452 instance Foo a => Foo [a]
1455 In the instance for Foo [a], when generating evidence for the superclasses
1456 (ie in tcSimplifySuperClasses) we need a superclass (Data Maybe [a]).
1457 Using the instance for Data, we therefore need
1458 (Sat (Maybe [a], Data Maybe a)
1459 But we are given (Foo a), and hence its superclass (Data Maybe a).
1460 So that leaves (Sat (Maybe [a])). Using the instance for Sat means
1461 we need (Foo [a]). And that is the very dictionary we are bulding
1462 an instance for! So we must put that in the "givens". So in this
1464 Given: Foo a, Foo [a]
1465 Wanted: Data Maybe [a]
1467 BUT we must *not not not* put the *superclasses* of (Foo [a]) in
1468 the givens, which is what 'addGiven' would normally do. Why? Because
1469 (Data Maybe [a]) is the superclass, so we'd "satisfy" the wanted
1470 by selecting a superclass from Foo [a], which simply makes a loop.
1472 On the other hand we *must* put the superclasses of (Foo a) in
1473 the givens, as you can see from the derivation described above.
1475 Conclusion: in the very special case of tcSimplifySuperClasses
1476 we have one 'given' (namely the "this" dictionary) whose superclasses
1477 must not be added to 'givens' by addGiven.
1479 There is a complication though. Suppose there are equalities
1480 instance (Eq a, a~b) => Num (a,b)
1481 Then we normalise the 'givens' wrt the equalities, so the original
1482 given "this" dictionary is cast to one of a different type. So it's a
1483 bit trickier than before to identify the "special" dictionary whose
1484 superclasses must not be added. See test
1485 indexed-types/should_run/EqInInstance
1487 We need a persistent property of the dictionary to record this
1488 special-ness. Current I'm using the InstLocOrigin (a bit of a hack,
1489 but cool), which is maintained by dictionary normalisation.
1490 Specifically, the InstLocOrigin is
1492 then the no-superclass thing kicks in. WATCH OUT if you fiddle
1495 Note [MATCHING-SYNONYMS]
1496 ~~~~~~~~~~~~~~~~~~~~~~~~
1497 When trying to match a dictionary (D tau) to a top-level instance, or a
1498 type family equation (F taus_1 ~ tau_2) to a top-level family instance,
1499 we do *not* need to expand type synonyms because the matcher will do that for us.
1502 Note [RHS-FAMILY-SYNONYMS]
1503 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1504 The RHS of a family instance is represented as yet another constructor which is
1505 like a type synonym for the real RHS the programmer declared. Eg:
1506 type instance F (a,a) = [a]
1508 :R32 a = [a] -- internal type synonym introduced
1509 F (a,a) ~ :R32 a -- instance
1511 When we react a family instance with a type family equation in the work list
1512 we keep the synonym-using RHS without expansion.
1515 *********************************************************************************
1517 The top-reaction Stage
1519 *********************************************************************************
1522 -- If a work item has any form of interaction with top-level we get this
1523 data TopInteractResult
1524 = NoTopInt -- No top-level interaction
1526 { tir_new_work :: WorkList -- Sub-goals or new work (could be given,
1527 -- for superclasses)
1528 , tir_new_inert :: StopOrContinue -- The input work item, ready to become *inert* now:
1529 } -- NB: in ``given'' (solved) form if the
1530 -- original was wanted or given and instance match
1531 -- was found, but may also be in wanted form if we
1532 -- only reacted with functional dependencies
1533 -- arising from top-level instances.
1535 topReactionsStage :: SimplifierStage
1536 topReactionsStage workItem inerts
1537 = do { tir <- tryTopReact workItem
1540 return $ SR { sr_inerts = inerts
1541 , sr_new_work = emptyWorkList
1542 , sr_stop = ContinueWith workItem }
1543 SomeTopInt tir_new_work tir_new_inert ->
1544 return $ SR { sr_inerts = inerts
1545 , sr_new_work = tir_new_work
1546 , sr_stop = tir_new_inert
1550 tryTopReact :: WorkItem -> TcS TopInteractResult
1551 tryTopReact workitem
1552 = do { -- A flag controls the amount of interaction allowed
1553 -- See Note [Simplifying RULE lhs constraints]
1554 ctxt <- getTcSContext
1555 ; if allowedTopReaction (simplEqsOnly ctxt) workitem
1556 then do { traceTcS "tryTopReact / calling doTopReact" (ppr workitem)
1557 ; doTopReact workitem }
1558 else return NoTopInt
1561 allowedTopReaction :: Bool -> WorkItem -> Bool
1562 allowedTopReaction eqs_only (CDictCan {}) = not eqs_only
1563 allowedTopReaction _ _ = True
1566 doTopReact :: WorkItem -> TcS TopInteractResult
1567 -- The work item does not react with the inert set, so try interaction with top-level instances
1568 -- NB: The place to add superclasses in *not* in doTopReact stage. Instead superclasses are
1569 -- added in the worklist as part of the canonicalisation process.
1570 -- See Note [Adding superclasses] in TcCanonical.
1573 -- See Note [Given constraint that matches an instance declaration]
1574 doTopReact (CDictCan { cc_flavor = Given {} })
1575 = return NoTopInt -- NB: Superclasses already added since it's canonical
1577 -- Derived dictionary: just look for functional dependencies
1578 doTopReact workItem@(CDictCan { cc_flavor = Derived loc _
1579 , cc_class = cls, cc_tyargs = xis })
1580 = do { fd_work <- findClassFunDeps cls xis loc
1581 ; if isEmptyWorkList fd_work then
1583 else return $ SomeTopInt { tir_new_work = fd_work
1584 , tir_new_inert = ContinueWith workItem } }
1585 -- Wanted dictionary
1586 doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Wanted loc
1587 , cc_class = cls, cc_tyargs = xis })
1588 = do { -- See Note [MATCHING-SYNONYMS]
1589 ; lkp_inst_res <- matchClassInst cls xis loc
1590 ; case lkp_inst_res of
1592 do { traceTcS "doTopReact/ no class instance for" (ppr dv)
1593 ; fd_work <- findClassFunDeps cls xis loc
1594 ; if isEmptyWorkList fd_work then
1596 { tir_new_work = emptyWorkList
1597 , tir_new_inert = ContinueWith workItem }
1598 else -- More fundep work produced, just thow him back in the
1599 -- worklist to prioritize the solution of fd equalities
1601 { tir_new_work = fd_work `unionWorkLists` workListFromCCan workItem
1602 , tir_new_inert = Stop } }
1604 GenInst wtvs ev_term -> -- Solved
1605 -- No need to do fundeps stuff here; the instance
1606 -- matches already so we won't get any more info
1607 -- from functional dependencies
1608 do { traceTcS "doTopReact/ found class instance for" (ppr dv)
1609 ; setDictBind dv ev_term
1610 ; inst_work <- canWanteds wtvs
1612 -- Solved in one step and no new wanted work produced.
1613 -- i.e we directly matched a top-level instance
1614 -- No point in caching this in 'inert'
1615 then return $ SomeTopInt { tir_new_work = emptyWorkList
1616 , tir_new_inert = Stop }
1618 -- Solved and new wanted work produced, you may cache the
1619 -- (tentatively solved) dictionary as Derived
1620 else do { let solved = makeSolvedByInst workItem
1621 ; return $ SomeTopInt
1622 { tir_new_work = inst_work
1623 , tir_new_inert = ContinueWith solved } }
1627 doTopReact (CFunEqCan { cc_id = cv, cc_flavor = fl
1628 , cc_fun = tc, cc_tyargs = args, cc_rhs = xi })
1629 = ASSERT (isSynFamilyTyCon tc) -- No associated data families have reached that far
1630 do { match_res <- matchFam tc args -- See Note [MATCHING-SYNONYMS]
1634 MatchInstSingle (rep_tc, rep_tys)
1635 -> do { let Just coe_tc = tyConFamilyCoercion_maybe rep_tc
1636 Just rhs_ty = tcView (mkTyConApp rep_tc rep_tys)
1637 -- Eagerly expand away the type synonym on the
1638 -- RHS of a type function, so that it never
1639 -- appears in an error message
1640 -- See Note [Type synonym families] in TyCon
1641 coe = mkTyConApp coe_tc rep_tys
1643 Wanted {} -> do { cv' <- newWantedCoVar rhs_ty xi
1644 ; setWantedCoBind cv $
1645 coe `mkTransCoercion`
1648 _ -> newGivOrDerCoVar xi rhs_ty $
1649 mkSymCoercion (mkCoVarCoercion cv) `mkTransCoercion` coe
1651 ; can_cts <- mkCanonical fl cv'
1652 ; return $ SomeTopInt can_cts Stop }
1654 -> panicTcS $ text "TcSMonad.matchFam returned multiple instances!"
1658 -- Any other work item does not react with any top-level equations
1659 doTopReact _workItem = return NoTopInt
1661 ----------------------
1662 findClassFunDeps :: Class -> [Xi] -> WantedLoc -> TcS WorkList
1663 -- Look for a fundep reaction beween the wanted item
1664 -- and a top-level instance declaration
1665 findClassFunDeps cls xis loc
1666 = do { instEnvs <- getInstEnvs
1667 ; let eqn_pred_locs = improveFromInstEnv (classInstances instEnvs)
1668 (ClassP cls xis, pprArisingAt loc)
1669 ; wevvars <- mkWantedFunDepEqns loc eqn_pred_locs
1670 -- NB: fundeps generate some wanted equalities, but
1671 -- we don't use their evidence for anything
1672 ; canWanteds wevvars }
1676 Note [FunDep and implicit parameter reactions]
1677 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1678 Currently, our story of interacting two dictionaries (or a dictionary
1679 and top-level instances) for functional dependencies, and implicit
1680 paramters, is that we simply produce new wanted equalities. So for example
1682 class D a b | a -> b where ...
1688 We generate the extra work item
1690 where 'cv' is currently unused. However, this new item reacts with d2,
1691 discharging it in favour of a new constraint d2' thus:
1693 d2 := d2' |> D Int cv
1694 Now d2' can be discharged from d1
1696 We could be more aggressive and try to *immediately* solve the dictionary
1697 using those extra equalities. With the same inert set and work item we
1698 might dischard d2 directly:
1701 d2 := d1 |> D Int cv
1703 But in general it's a bit painful to figure out the necessary coercion,
1704 so we just take the first approach. Here is a better example. Consider:
1705 class C a b c | a -> b
1707 [Given] d1 : C T Int Char
1708 [Wanted] d2 : C T beta Int
1709 In this case, it's *not even possible* to solve the wanted immediately.
1710 So we should simply output the functional dependency and add this guy
1711 [but NOT its superclasses] back in the worklist. Even worse:
1712 [Given] d1 : C T Int beta
1713 [Wanted] d2: C T beta Int
1714 Then it is solvable, but its very hard to detect this on the spot.
1716 It's exactly the same with implicit parameters, except that the
1717 "aggressive" approach would be much easier to implement.
1719 Note [When improvement happens]
1720 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1721 We fire an improvement rule when
1723 * Two constraints match (modulo the fundep)
1724 e.g. C t1 t2, C t1 t3 where C a b | a->b
1725 The two match because the first arg is identical
1727 * At least one is not Given. If they are both given, we don't fire
1728 the reaction because we have no way of constructing evidence for a
1729 new equality nor does it seem right to create a new wanted goal
1730 (because the goal will most likely contain untouchables, which
1731 can't be solved anyway)!
1733 Note that we *do* fire the improvement if one is Given and one is Derived.
1734 The latter can be a superclass of a wanted goal. Example (tcfail138)
1735 class L a b | a -> b
1736 class (G a, L a b) => C a b
1738 instance C a b' => G (Maybe a)
1739 instance C a b => C (Maybe a) a
1740 instance L (Maybe a) a
1742 When solving the superclasses of the (C (Maybe a) a) instance, we get
1743 Given: C a b ... and hance by superclasses, (G a, L a b)
1745 Use the instance decl to get
1747 The (C a b') is inert, so we generate its Derived superclasses (L a b'),
1748 and now we need improvement between that derived superclass an the Given (L a b)
1750 Note [Overriding implicit parameters]
1751 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1753 f :: (?x::a) -> Bool -> a
1755 g v = let ?x::Int = 3
1756 in (f v, let ?x::Bool = True in f v)
1758 This should probably be well typed, with
1759 g :: Bool -> (Int, Bool)
1761 So the inner binding for ?x::Bool *overrides* the outer one.
1762 Hence a work-item Given overrides an inert-item Given.
1764 Note [Given constraint that matches an instance declaration]
1765 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1766 What should we do when we discover that one (or more) top-level
1767 instances match a given (or solved) class constraint? We have
1770 1. Reject the program. The reason is that there may not be a unique
1771 best strategy for the solver. Example, from the OutsideIn(X) paper:
1772 instance P x => Q [x]
1773 instance (x ~ y) => R [x] y
1775 wob :: forall a b. (Q [b], R b a) => a -> Int
1777 g :: forall a. Q [a] => [a] -> Int
1780 will generate the impliation constraint:
1781 Q [a] => (Q [beta], R beta [a])
1782 If we react (Q [beta]) with its top-level axiom, we end up with a
1783 (P beta), which we have no way of discharging. On the other hand,
1784 if we react R beta [a] with the top-level we get (beta ~ a), which
1785 is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
1786 now solvable by the given Q [a].
1788 However, this option is restrictive, for instance [Example 3] from
1789 Note [Recursive dictionaries] will fail to work.
1791 2. Ignore the problem, hoping that the situations where there exist indeed
1792 such multiple strategies are rare: Indeed the cause of the previous
1793 problem is that (R [x] y) yields the new work (x ~ y) which can be
1794 *spontaneously* solved, not using the givens.
1796 We are choosing option 2 below but we might consider having a flag as well.
1799 Note [New Wanted Superclass Work]
1800 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1801 Even in the case of wanted constraints, we add all of its superclasses as
1802 new given work. There are several reasons for this:
1803 a) to minimise error messages;
1804 eg suppose we have wanted (Eq a, Ord a)
1805 then we report only (Ord a) unsoluble
1807 b) to make the smallest number of constraints when *inferring* a type
1808 (same Eq/Ord example)
1810 c) for recursive dictionaries we *must* add the superclasses
1811 so that we can use them when solving a sub-problem
1813 d) To allow FD-like improvement for type families. Assume that
1815 class C a b | a -> b
1816 and we have to solve the implication constraint:
1818 Then, FD improvement can help us to produce a new wanted (beta ~ b)
1820 We want to have the same effect with the type family encoding of
1821 functional dependencies. Namely, consider:
1822 class (F a ~ b) => C a b
1823 Now suppose that we have:
1826 By interacting the given we will get given (F a ~ b) which is not
1827 enough by itself to make us discharge (C a beta). However, we
1828 may create a new derived equality from the super-class of the
1829 wanted constraint (C a beta), namely derived (F a ~ beta).
1830 Now we may interact this with given (F a ~ b) to get:
1832 But 'beta' is a touchable unification variable, and hence OK to
1833 unify it with 'b', replacing the derived evidence with the identity.
1835 This requires trySpontaneousSolve to solve *derived*
1836 equalities that have a touchable in their RHS, *in addition*
1837 to solving wanted equalities.
1839 Here is another example where this is useful.
1843 class (F a ~ b) => C a b
1844 And we are given the wanteds:
1848 We surely do *not* want to quantify over (b ~ c), since if someone provides
1849 dictionaries for (C a b) and (C a c), these dictionaries can provide a proof
1850 of (b ~ c), hence no extra evidence is necessary. Here is what will happen:
1852 Step 1: We will get new *given* superclass work,
1853 provisionally to our solving of w1 and w2
1855 g1: F a ~ b, g2 : F a ~ c,
1856 w1 : C a b, w2 : C a c, w3 : b ~ c
1858 The evidence for g1 and g2 is a superclass evidence term:
1860 g1 := sc w1, g2 := sc w2
1862 Step 2: The givens will solve the wanted w3, so that
1863 w3 := sym (sc w1) ; sc w2
1865 Step 3: Now, one may naively assume that then w2 can be solve from w1
1866 after rewriting with the (now solved equality) (b ~ c).
1868 But this rewriting is ruled out by the isGoodRectDict!
1870 Conclusion, we will (correctly) end up with the unsolved goals
1873 NB: The desugarer needs be more clever to deal with equalities
1874 that participate in recursive dictionary bindings.
1879 newGivenSCWork :: EvVar -> GivenLoc -> Class -> [Xi] -> TcS WorkList
1880 newGivenSCWork ev loc cls xis
1881 | NoScSkol <- ctLocOrigin loc -- Very important!
1882 = return emptyWorkList
1884 = newImmSCWorkFromFlavored ev (Given loc) cls xis >>= return
1886 newDerivedSCWork :: EvVar -> WantedLoc -> Class -> [Xi] -> TcS WorkList
1887 newDerivedSCWork ev loc cls xis
1888 = do { ims <- newImmSCWorkFromFlavored ev flavor cls xis
1891 rec_sc_work :: CanonicalCts -> TcS CanonicalCts
1893 = do { bg <- mapBagM (\c -> do { ims <- imm_sc_work c
1894 ; recs_ims <- rec_sc_work ims
1895 ; return $ consBag c recs_ims }) cts
1896 ; return $ concatBag bg }
1897 imm_sc_work (CDictCan { cc_id = dv, cc_flavor = fl, cc_class = cls, cc_tyargs = xis })
1898 = newImmSCWorkFromFlavored dv fl cls xis
1899 imm_sc_work _ct = return emptyCCan
1901 flavor = Derived loc DerSC
1906 data LookupInstResult
1908 | GenInst [WantedEvVar] EvTerm
1910 matchClassInst :: Class -> [Type] -> WantedLoc -> TcS LookupInstResult
1911 matchClassInst clas tys loc
1912 = do { let pred = mkClassPred clas tys
1913 ; mb_result <- matchClass clas tys
1915 MatchInstNo -> return NoInstance
1916 MatchInstMany -> return NoInstance -- defer any reactions of a multitude until
1917 -- we learn more about the reagent
1918 MatchInstSingle (dfun_id, mb_inst_tys) ->
1919 do { checkWellStagedDFun pred dfun_id loc
1921 -- It's possible that not all the tyvars are in
1922 -- the substitution, tenv. For example:
1923 -- instance C X a => D X where ...
1924 -- (presumably there's a functional dependency in class C)
1925 -- Hence mb_inst_tys :: Either TyVar TcType
1927 ; tys <- instDFunTypes mb_inst_tys
1928 ; let (theta, _) = tcSplitPhiTy (applyTys (idType dfun_id) tys)
1929 ; if null theta then
1930 return (GenInst [] (EvDFunApp dfun_id tys []))
1932 { ev_vars <- instDFunConstraints theta
1933 ; let wevs = [WantedEvVar w loc | w <- ev_vars]
1934 ; return $ GenInst wevs (EvDFunApp dfun_id tys ev_vars) }