Expose source locations via Implicit Parameters of type GHC.Location.Location
[ghc.git] / compiler / typecheck / TcInteract.hs
1 {-# LANGUAGE CPP #-}
2
3 module TcInteract (
4 solveSimpleGivens, -- Solves [EvVar],GivenLoc
5 solveSimpleWanteds -- Solves Cts
6 ) where
7
8 #include "HsVersions.h"
9
10 import BasicTypes ()
11 import HsTypes ( hsIPNameFS )
12 import FastString
13 import TcCanonical
14 import TcFlatten
15 import VarSet
16 import Type
17 import Unify
18 import InstEnv( DFunInstType, lookupInstEnv, instanceDFunId )
19 import CoAxiom(sfInteractTop, sfInteractInert)
20
21 import Var
22 import TcType
23 import PrelNames ( knownNatClassName, knownSymbolClassName, ipClassNameKey,
24 callStackTyConKey )
25 import Id( idType )
26 import Class
27 import TyCon
28 import FunDeps
29 import FamInst
30 import Inst( tyVarsOfCt )
31
32 import TcEvidence
33 import Outputable
34
35 import TcRnTypes
36 import TcErrors
37 import TcSMonad
38 import Bag
39
40 import Data.List( partition, foldl', deleteFirstsBy )
41
42 import VarEnv
43
44 import Control.Monad
45 import Maybes( isJust )
46 import Pair (Pair(..))
47 import Unique( hasKey )
48 import DynFlags
49 import Util
50
51 {-
52 **********************************************************************
53 * *
54 * Main Interaction Solver *
55 * *
56 **********************************************************************
57
58 Note [Basic Simplifier Plan]
59 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
60 1. Pick an element from the WorkList if there exists one with depth
61 less than our context-stack depth.
62
63 2. Run it down the 'stage' pipeline. Stages are:
64 - canonicalization
65 - inert reactions
66 - spontaneous reactions
67 - top-level intreactions
68 Each stage returns a StopOrContinue and may have sideffected
69 the inerts or worklist.
70
71 The threading of the stages is as follows:
72 - If (Stop) is returned by a stage then we start again from Step 1.
73 - If (ContinueWith ct) is returned by a stage, we feed 'ct' on to
74 the next stage in the pipeline.
75 4. If the element has survived (i.e. ContinueWith x) the last stage
76 then we add him in the inerts and jump back to Step 1.
77
78 If in Step 1 no such element exists, we have exceeded our context-stack
79 depth and will simply fail.
80
81 Note [Unflatten after solving the simple wanteds]
82 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
83 We unflatten after solving the wc_simples of an implication, and before attempting
84 to float. This means that
85
86 * The fsk/fmv flatten-skolems only survive during solveSimples. We don't
87 need to worry about then across successive passes over the constraint tree.
88 (E.g. we don't need the old ic_fsk field of an implication.
89
90 * When floating an equality outwards, we don't need to worry about floating its
91 associated flattening constraints.
92
93 * Another tricky case becomes easy: Trac #4935
94 type instance F True a b = a
95 type instance F False a b = b
96
97 [w] F c a b ~ gamma
98 (c ~ True) => a ~ gamma
99 (c ~ False) => b ~ gamma
100
101 Obviously this is soluble with gamma := F c a b, and unflattening
102 will do exactly that after solving the simple constraints and before
103 attempting the implications. Before, when we were not unflattening,
104 we had to push Wanted funeqs in as new givens. Yuk!
105
106 Another example that becomes easy: indexed_types/should_fail/T7786
107 [W] BuriedUnder sub k Empty ~ fsk
108 [W] Intersect fsk inv ~ s
109 [w] xxx[1] ~ s
110 [W] forall[2] . (xxx[1] ~ Empty)
111 => Intersect (BuriedUnder sub k Empty) inv ~ Empty
112
113 Note [Running plugins on unflattened wanteds]
114 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
115 There is an annoying mismatch between solveSimpleGivens and
116 solveSimpleWanteds, because the latter needs to fiddle with the inert
117 set, unflatten and and zonk the wanteds. It passes the zonked wanteds
118 to runTcPluginsWanteds, which produces a replacement set of wanteds,
119 some additional insolubles and a flag indicating whether to go round
120 the loop again. If so, prepareInertsForImplications is used to remove
121 the previous wanteds (which will still be in the inert set). Note
122 that prepareInertsForImplications will discard the insolubles, so we
123 must keep track of them separately.
124 -}
125
126 solveSimpleGivens :: CtLoc -> [EvVar] -> TcS ()
127 solveSimpleGivens loc givens
128 | null givens -- Shortcut for common case
129 = return ()
130 | otherwise
131 = go (map mk_given_ct givens)
132 where
133 mk_given_ct ev_id = mkNonCanonical (CtGiven { ctev_evtm = EvId ev_id
134 , ctev_pred = evVarPred ev_id
135 , ctev_loc = loc })
136 go givens = do { solveSimples (listToBag givens)
137 ; new_givens <- runTcPluginsGiven
138 ; when (notNull new_givens) (go new_givens)
139 }
140
141 solveSimpleWanteds :: Cts -> TcS WantedConstraints
142 solveSimpleWanteds = go emptyBag
143 where
144 go insols0 wanteds
145 = do { solveSimples wanteds
146 ; (implics, tv_eqs, fun_eqs, insols, others) <- getUnsolvedInerts
147 ; unflattened_eqs <- unflatten tv_eqs fun_eqs
148 -- See Note [Unflatten after solving the simple wanteds]
149
150 ; zonked <- zonkSimples (others `andCts` unflattened_eqs)
151 -- Postcondition is that the wl_simples are zonked
152
153 ; (wanteds', insols', rerun) <- runTcPluginsWanted zonked
154 -- See Note [Running plugins on unflattened wanteds]
155 ; let all_insols = insols0 `unionBags` insols `unionBags` insols'
156
157 ; if rerun then do { updInertTcS prepareInertsForImplications
158 ; go all_insols wanteds' }
159 else return (WC { wc_simple = wanteds'
160 , wc_insol = all_insols
161 , wc_impl = implics }) }
162
163
164 -- The main solver loop implements Note [Basic Simplifier Plan]
165 ---------------------------------------------------------------
166 solveSimples :: Cts -> TcS ()
167 -- Returns the final InertSet in TcS
168 -- Has no effect on work-list or residual-iplications
169 -- The constraints are initially examined in left-to-right order
170
171 solveSimples cts
172 = {-# SCC "solveSimples" #-}
173 do { dyn_flags <- getDynFlags
174 ; updWorkListTcS (\wl -> foldrBag extendWorkListCt wl cts)
175 ; solve_loop (maxSubGoalDepth dyn_flags) }
176 where
177 solve_loop max_depth
178 = {-# SCC "solve_loop" #-}
179 do { sel <- selectNextWorkItem max_depth
180 ; case sel of
181 NoWorkRemaining -- Done, successfuly (modulo frozen)
182 -> return ()
183 MaxDepthExceeded cnt ct -- Failure, depth exceeded
184 -> wrapErrTcS $ solverDepthErrorTcS cnt (ctEvidence ct)
185 NextWorkItem ct -- More work, loop around!
186 -> do { runSolverPipeline thePipeline ct; solve_loop max_depth } }
187
188
189 -- | Extract the (inert) givens and invoke the plugins on them.
190 -- Remove solved givens from the inert set and emit insolubles, but
191 -- return new work produced so that 'solveSimpleGivens' can feed it back
192 -- into the main solver.
193 runTcPluginsGiven :: TcS [Ct]
194 runTcPluginsGiven = do
195 (givens,_,_) <- fmap splitInertCans getInertCans
196 if null givens
197 then return []
198 else do
199 p <- runTcPlugins (givens,[],[])
200 let (solved_givens, _, _) = pluginSolvedCts p
201 updInertCans (removeInertCts solved_givens)
202 mapM_ emitInsoluble (pluginBadCts p)
203 return (pluginNewCts p)
204
205 -- | Given a bag of (flattened, zonked) wanteds, invoke the plugins on
206 -- them and produce an updated bag of wanteds (possibly with some new
207 -- work) and a bag of insolubles. The boolean indicates whether
208 -- 'solveSimpleWanteds' should feed the updated wanteds back into the
209 -- main solver.
210 runTcPluginsWanted :: Cts -> TcS (Cts, Cts, Bool)
211 runTcPluginsWanted zonked_wanteds
212 | isEmptyBag zonked_wanteds = return (zonked_wanteds, emptyBag, False)
213 | otherwise = do
214 (given,derived,_) <- fmap splitInertCans getInertCans
215 p <- runTcPlugins (given, derived, bagToList zonked_wanteds)
216 let (solved_givens, solved_deriveds, solved_wanteds) = pluginSolvedCts p
217 (_, _, wanteds) = pluginInputCts p
218 updInertCans (removeInertCts $ solved_givens ++ solved_deriveds)
219 mapM_ setEv solved_wanteds
220 return ( listToBag $ pluginNewCts p ++ wanteds
221 , listToBag $ pluginBadCts p
222 , notNull (pluginNewCts p) )
223 where
224 setEv :: (EvTerm,Ct) -> TcS ()
225 setEv (ev,ct) = case ctEvidence ct of
226 CtWanted {ctev_evar = evar} -> setWantedEvBind evar ev
227 _ -> panic "runTcPluginsWanted.setEv: attempt to solve non-wanted!"
228
229 -- | A triple of (given, derived, wanted) constraints to pass to plugins
230 type SplitCts = ([Ct], [Ct], [Ct])
231
232 -- | A solved triple of constraints, with evidence for wanteds
233 type SolvedCts = ([Ct], [Ct], [(EvTerm,Ct)])
234
235 -- | Represents collections of constraints generated by typechecker
236 -- plugins
237 data TcPluginProgress = TcPluginProgress
238 { pluginInputCts :: SplitCts
239 -- ^ Original inputs to the plugins with solved/bad constraints
240 -- removed, but otherwise unmodified
241 , pluginSolvedCts :: SolvedCts
242 -- ^ Constraints solved by plugins
243 , pluginBadCts :: [Ct]
244 -- ^ Constraints reported as insoluble by plugins
245 , pluginNewCts :: [Ct]
246 -- ^ New constraints emitted by plugins
247 }
248
249 -- | Starting from a triple of (given, derived, wanted) constraints,
250 -- invoke each of the typechecker plugins in turn and return
251 --
252 -- * the remaining unmodified constraints,
253 -- * constraints that have been solved,
254 -- * constraints that are insoluble, and
255 -- * new work.
256 --
257 -- Note that new work generated by one plugin will not be seen by
258 -- other plugins on this pass (but the main constraint solver will be
259 -- re-invoked and they will see it later). There is no check that new
260 -- work differs from the original constraints supplied to the plugin:
261 -- the plugin itself should perform this check if necessary.
262 runTcPlugins :: SplitCts -> TcS TcPluginProgress
263 runTcPlugins all_cts = do
264 gblEnv <- getGblEnv
265 foldM do_plugin initialProgress (tcg_tc_plugins gblEnv)
266 where
267 do_plugin :: TcPluginProgress -> TcPluginSolver -> TcS TcPluginProgress
268 do_plugin p solver = do
269 result <- runTcPluginTcS (uncurry3 solver (pluginInputCts p))
270 return $ progress p result
271
272 progress :: TcPluginProgress -> TcPluginResult -> TcPluginProgress
273 progress p (TcPluginContradiction bad_cts) =
274 p { pluginInputCts = discard bad_cts (pluginInputCts p)
275 , pluginBadCts = bad_cts ++ pluginBadCts p
276 }
277 progress p (TcPluginOk solved_cts new_cts) =
278 p { pluginInputCts = discard (map snd solved_cts) (pluginInputCts p)
279 , pluginSolvedCts = add solved_cts (pluginSolvedCts p)
280 , pluginNewCts = new_cts ++ pluginNewCts p
281 }
282
283 initialProgress = TcPluginProgress all_cts ([], [], []) [] []
284
285 discard :: [Ct] -> SplitCts -> SplitCts
286 discard cts (xs, ys, zs) =
287 (xs `without` cts, ys `without` cts, zs `without` cts)
288
289 without :: [Ct] -> [Ct] -> [Ct]
290 without = deleteFirstsBy eqCt
291
292 eqCt :: Ct -> Ct -> Bool
293 eqCt c c' = case (ctEvidence c, ctEvidence c') of
294 (CtGiven pred _ _, CtGiven pred' _ _) -> pred `eqType` pred'
295 (CtWanted pred _ _, CtWanted pred' _ _) -> pred `eqType` pred'
296 (CtDerived pred _ , CtDerived pred' _ ) -> pred `eqType` pred'
297 (_ , _ ) -> False
298
299 add :: [(EvTerm,Ct)] -> SolvedCts -> SolvedCts
300 add xs scs = foldl' addOne scs xs
301
302 addOne :: SolvedCts -> (EvTerm,Ct) -> SolvedCts
303 addOne (givens, deriveds, wanteds) (ev,ct) = case ctEvidence ct of
304 CtGiven {} -> (ct:givens, deriveds, wanteds)
305 CtDerived{} -> (givens, ct:deriveds, wanteds)
306 CtWanted {} -> (givens, deriveds, (ev,ct):wanteds)
307
308
309 type WorkItem = Ct
310 type SimplifierStage = WorkItem -> TcS (StopOrContinue Ct)
311
312 data SelectWorkItem
313 = NoWorkRemaining -- No more work left (effectively we're done!)
314 | MaxDepthExceeded SubGoalCounter Ct
315 -- More work left to do but this constraint has exceeded
316 -- the maximum depth for one of the subgoal counters and we
317 -- must stop
318 | NextWorkItem Ct -- More work left, here's the next item to look at
319
320 selectNextWorkItem :: SubGoalDepth -- Max depth allowed
321 -> TcS SelectWorkItem
322 selectNextWorkItem max_depth
323 = updWorkListTcS_return pick_next
324 where
325 pick_next :: WorkList -> (SelectWorkItem, WorkList)
326 pick_next wl
327 = case selectWorkItem wl of
328 (Nothing,_)
329 -> (NoWorkRemaining,wl) -- No more work
330 (Just ct, new_wl)
331 | Just cnt <- subGoalDepthExceeded max_depth (ctLocDepth (ctLoc ct)) -- Depth exceeded
332 -> (MaxDepthExceeded cnt ct,new_wl)
333 (Just ct, new_wl)
334 -> (NextWorkItem ct, new_wl) -- New workitem and worklist
335
336 runSolverPipeline :: [(String,SimplifierStage)] -- The pipeline
337 -> WorkItem -- The work item
338 -> TcS ()
339 -- Run this item down the pipeline, leaving behind new work and inerts
340 runSolverPipeline pipeline workItem
341 = do { initial_is <- getTcSInerts
342 ; traceTcS "Start solver pipeline {" $
343 vcat [ ptext (sLit "work item = ") <+> ppr workItem
344 , ptext (sLit "inerts = ") <+> ppr initial_is]
345
346 ; bumpStepCountTcS -- One step for each constraint processed
347 ; final_res <- run_pipeline pipeline (ContinueWith workItem)
348
349 ; final_is <- getTcSInerts
350 ; case final_res of
351 Stop ev s -> do { traceFireTcS ev s
352 ; traceTcS "End solver pipeline (discharged) }"
353 (ptext (sLit "inerts =") <+> ppr final_is)
354 ; return () }
355 ContinueWith ct -> do { traceFireTcS (ctEvidence ct) (ptext (sLit "Kept as inert"))
356 ; traceTcS "End solver pipeline (not discharged) }" $
357 vcat [ ptext (sLit "final_item =") <+> ppr ct
358 , pprTvBndrs (varSetElems $ tyVarsOfCt ct)
359 , ptext (sLit "inerts =") <+> ppr final_is]
360 ; insertInertItemTcS ct }
361 }
362 where run_pipeline :: [(String,SimplifierStage)] -> StopOrContinue Ct
363 -> TcS (StopOrContinue Ct)
364 run_pipeline [] res = return res
365 run_pipeline _ (Stop ev s) = return (Stop ev s)
366 run_pipeline ((stg_name,stg):stgs) (ContinueWith ct)
367 = do { traceTcS ("runStage " ++ stg_name ++ " {")
368 (text "workitem = " <+> ppr ct)
369 ; res <- stg ct
370 ; traceTcS ("end stage " ++ stg_name ++ " }") empty
371 ; run_pipeline stgs res }
372
373 {-
374 Example 1:
375 Inert: {c ~ d, F a ~ t, b ~ Int, a ~ ty} (all given)
376 Reagent: a ~ [b] (given)
377
378 React with (c~d) ==> IR (ContinueWith (a~[b])) True []
379 React with (F a ~ t) ==> IR (ContinueWith (a~[b])) False [F [b] ~ t]
380 React with (b ~ Int) ==> IR (ContinueWith (a~[Int]) True []
381
382 Example 2:
383 Inert: {c ~w d, F a ~g t, b ~w Int, a ~w ty}
384 Reagent: a ~w [b]
385
386 React with (c ~w d) ==> IR (ContinueWith (a~[b])) True []
387 React with (F a ~g t) ==> IR (ContinueWith (a~[b])) True [] (can't rewrite given with wanted!)
388 etc.
389
390 Example 3:
391 Inert: {a ~ Int, F Int ~ b} (given)
392 Reagent: F a ~ b (wanted)
393
394 React with (a ~ Int) ==> IR (ContinueWith (F Int ~ b)) True []
395 React with (F Int ~ b) ==> IR Stop True [] -- after substituting we re-canonicalize and get nothing
396 -}
397
398 thePipeline :: [(String,SimplifierStage)]
399 thePipeline = [ ("canonicalization", TcCanonical.canonicalize)
400 , ("interact with inerts", interactWithInertsStage)
401 , ("top-level reactions", topReactionsStage) ]
402
403 {-
404 *********************************************************************************
405 * *
406 The interact-with-inert Stage
407 * *
408 *********************************************************************************
409
410 Note [The Solver Invariant]
411 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
412 We always add Givens first. So you might think that the solver has
413 the invariant
414
415 If the work-item is Given,
416 then the inert item must Given
417
418 But this isn't quite true. Suppose we have,
419 c1: [W] beta ~ [alpha], c2 : [W] blah, c3 :[W] alpha ~ Int
420 After processing the first two, we get
421 c1: [G] beta ~ [alpha], c2 : [W] blah
422 Now, c3 does not interact with the the given c1, so when we spontaneously
423 solve c3, we must re-react it with the inert set. So we can attempt a
424 reaction between inert c2 [W] and work-item c3 [G].
425
426 It *is* true that [Solver Invariant]
427 If the work-item is Given,
428 AND there is a reaction
429 then the inert item must Given
430 or, equivalently,
431 If the work-item is Given,
432 and the inert item is Wanted/Derived
433 then there is no reaction
434 -}
435
436 -- Interaction result of WorkItem <~> Ct
437
438 type StopNowFlag = Bool -- True <=> stop after this interaction
439
440 interactWithInertsStage :: WorkItem -> TcS (StopOrContinue Ct)
441 -- Precondition: if the workitem is a CTyEqCan then it will not be able to
442 -- react with anything at this stage.
443
444 interactWithInertsStage wi
445 = do { inerts <- getTcSInerts
446 ; let ics = inert_cans inerts
447 ; case wi of
448 CTyEqCan {} -> interactTyVarEq ics wi
449 CFunEqCan {} -> interactFunEq ics wi
450 CIrredEvCan {} -> interactIrred ics wi
451 CDictCan {} -> interactDict ics wi
452 _ -> pprPanic "interactWithInerts" (ppr wi) }
453 -- CHoleCan are put straight into inert_frozen, so never get here
454 -- CNonCanonical have been canonicalised
455
456 data InteractResult
457 = IRKeep -- Keep the existing inert constraint in the inert set
458 | IRReplace -- Replace the existing inert constraint with the work item
459 | IRDelete -- Delete the existing inert constraint from the inert set
460
461 instance Outputable InteractResult where
462 ppr IRKeep = ptext (sLit "keep")
463 ppr IRReplace = ptext (sLit "replace")
464 ppr IRDelete = ptext (sLit "delete")
465
466 solveOneFromTheOther :: CtEvidence -- Inert
467 -> CtEvidence -- WorkItem
468 -> TcS (InteractResult, StopNowFlag)
469 -- Preconditions:
470 -- 1) inert and work item represent evidence for the /same/ predicate
471 -- 2) ip/class/irred evidence (no coercions) only
472 solveOneFromTheOther ev_i ev_w
473 | isDerived ev_w
474 = return (IRKeep, True)
475
476 | isDerived ev_i -- The inert item is Derived, we can just throw it away,
477 -- The ev_w is inert wrt earlier inert-set items,
478 -- so it's safe to continue on from this point
479 = return (IRDelete, False)
480
481 | CtWanted { ctev_evar = ev_id } <- ev_w
482 = do { setWantedEvBind ev_id (ctEvTerm ev_i)
483 ; return (IRKeep, True) }
484
485 | CtWanted { ctev_evar = ev_id } <- ev_i
486 = do { setWantedEvBind ev_id (ctEvTerm ev_w)
487 ; return (IRReplace, True) }
488
489 -- So they are both Given
490 -- See Note [Replacement vs keeping]
491 | lvl_i == lvl_w
492 = do { binds <- getTcEvBindsMap
493 ; if has_binding binds ev_w && not (has_binding binds ev_i)
494 then return (IRReplace, True)
495 else return (IRKeep, True) }
496
497 | otherwise -- Both are Given
498 = return (if use_replacement then IRReplace else IRKeep, True)
499 where
500 pred = ctEvPred ev_i
501 loc_i = ctEvLoc ev_i
502 loc_w = ctEvLoc ev_w
503 lvl_i = ctLocLevel loc_i
504 lvl_w = ctLocLevel loc_w
505
506 has_binding binds ev
507 | EvId v <- ctEvTerm ev = isJust (lookupEvBind binds v)
508 | otherwise = True
509
510 use_replacement
511 | isIPPred pred = lvl_w > lvl_i
512 | otherwise = lvl_w < lvl_i
513
514 {-
515 Note [Replacement vs keeping]
516 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
517 When we have two Given constraints both of type (C tys), say, which should
518 we keep?
519
520 * For implicit parameters we want to keep the innermost (deepest)
521 one, so that it overrides the outer one.
522 See Note [Shadowing of Implicit Parameters]
523
524 * For everything else, we want to keep the outermost one. Reason: that
525 makes it more likely that the inner one will turn out to be unused,
526 and can be reported as redundant. See Note [Tracking redundant constraints]
527 in TcSimplify.
528
529 It transpires that using the outermost one is reponsible for an
530 8% performance improvement in nofib cryptarithm2, compared to
531 just rolling the dice. I didn't investigate why.
532
533 * If there is no "outermost" one, we keep the one that has a non-trivial
534 evidence binding. Note [Tracking redundant constraints] again.
535 Example: f :: (Eq a, Ord a) => blah
536 then we may find [G] sc_sel (d1::Ord a) :: Eq a
537 [G] d2 :: Eq a
538 We want to discard d2 in favour of the superclass selection from
539 the Ord dictionary.
540
541 * Finally, when there is still a choice, use IRKeep rather than
542 IRReplace, to avoid unnecesary munging of the inert set.
543
544 Doing the depth-check for implicit parameters, rather than making the work item
545 always overrride, is important. Consider
546
547 data T a where { T1 :: (?x::Int) => T Int; T2 :: T a }
548
549 f :: (?x::a) => T a -> Int
550 f T1 = ?x
551 f T2 = 3
552
553 We have a [G] (?x::a) in the inert set, and at the pattern match on T1 we add
554 two new givens in the work-list: [G] (?x::Int)
555 [G] (a ~ Int)
556 Now consider these steps
557 - process a~Int, kicking out (?x::a)
558 - process (?x::Int), the inner given, adding to inert set
559 - process (?x::a), the outer given, overriding the inner given
560 Wrong! The depth-check ensures that the inner implicit parameter wins.
561 (Actually I think that the order in which the work-list is processed means
562 that this chain of events won't happen, but that's very fragile.)
563
564 *********************************************************************************
565 * *
566 interactIrred
567 * *
568 *********************************************************************************
569 -}
570
571 -- Two pieces of irreducible evidence: if their types are *exactly identical*
572 -- we can rewrite them. We can never improve using this:
573 -- if we want ty1 :: Constraint and have ty2 :: Constraint it clearly does not
574 -- mean that (ty1 ~ ty2)
575 interactIrred :: InertCans -> Ct -> TcS (StopOrContinue Ct)
576
577 interactIrred inerts workItem@(CIrredEvCan { cc_ev = ev_w })
578 | let pred = ctEvPred ev_w
579 (matching_irreds, others) = partitionBag (\ct -> ctPred ct `tcEqType` pred)
580 (inert_irreds inerts)
581 , (ct_i : rest) <- bagToList matching_irreds
582 , let ctev_i = ctEvidence ct_i
583 = ASSERT( null rest )
584 do { (inert_effect, stop_now) <- solveOneFromTheOther ctev_i ev_w
585 ; case inert_effect of
586 IRKeep -> return ()
587 IRDelete -> updInertIrreds (\_ -> others)
588 IRReplace -> updInertIrreds (\_ -> others `snocCts` workItem)
589 -- These const upd's assume that solveOneFromTheOther
590 -- has no side effects on InertCans
591 ; if stop_now then
592 return (Stop ev_w (ptext (sLit "Irred equal") <+> parens (ppr inert_effect)))
593 ; else
594 continueWith workItem }
595
596 | otherwise
597 = continueWith workItem
598
599 interactIrred _ wi = pprPanic "interactIrred" (ppr wi)
600
601 {-
602 *********************************************************************************
603 * *
604 interactDict
605 * *
606 *********************************************************************************
607 -}
608
609 interactDict :: InertCans -> Ct -> TcS (StopOrContinue Ct)
610 interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs = tys })
611 -- don't ever try to solve CallStack IPs directly from other dicts,
612 -- we always build new dicts instead.
613 -- See Note [Overview of implicit CallStacks]
614 | [_ip, ty] <- tys
615 , isWanted ev_w
616 , Just mkEvCs <- isCallStackIP (ctEvLoc ev_w) cls ty
617 = do let ev_cs =
618 case lookupInertDict inerts (ctEvLoc ev_w) cls tys of
619 Just ev | isGiven ev -> mkEvCs (ctEvTerm ev)
620 _ -> mkEvCs (EvCallStack EvCsEmpty)
621
622 -- now we have ev_cs :: CallStack, but the evidence term should
623 -- be a dictionary, so we have to coerce ev_cs to a
624 -- dictionary for `IP ip CallStack`
625 let ip_ty = mkClassPred cls tys
626 let ev_tm = mkEvCast (EvCallStack ev_cs) (TcCoercion $ wrapIP ip_ty)
627 addSolvedDict ev_w cls tys
628 setWantedEvBind (ctEvId ev_w) ev_tm
629 stopWith ev_w "Wanted CallStack IP"
630
631 | Just ctev_i <- lookupInertDict inerts (ctEvLoc ev_w) cls tys
632 = do { (inert_effect, stop_now) <- solveOneFromTheOther ctev_i ev_w
633 ; case inert_effect of
634 IRKeep -> return ()
635 IRDelete -> updInertDicts $ \ ds -> delDict ds cls tys
636 IRReplace -> updInertDicts $ \ ds -> addDict ds cls tys workItem
637 ; if stop_now then
638 return (Stop ev_w (ptext (sLit "Dict equal") <+> parens (ppr inert_effect)))
639 else
640 continueWith workItem }
641
642 | cls `hasKey` ipClassNameKey
643 , isGiven ev_w
644 = interactGivenIP inerts workItem
645
646 | otherwise
647 = do { mapBagM_ (addFunDepWork workItem) (findDictsByClass (inert_dicts inerts) cls)
648 -- Standard thing: create derived fds and keep on going. Importantly we don't
649 -- throw workitem back in the worklist because this can cause loops (see #5236)
650 ; continueWith workItem }
651
652 interactDict _ wi = pprPanic "interactDict" (ppr wi)
653
654 interactGivenIP :: InertCans -> Ct -> TcS (StopOrContinue Ct)
655 -- Work item is Given (?x:ty)
656 -- See Note [Shadowing of Implicit Parameters]
657 interactGivenIP inerts workItem@(CDictCan { cc_ev = ev, cc_class = cls
658 , cc_tyargs = tys@(ip_str:_) })
659 = do { updInertCans $ \cans -> cans { inert_dicts = addDict filtered_dicts cls tys workItem }
660 ; stopWith ev "Given IP" }
661 where
662 dicts = inert_dicts inerts
663 ip_dicts = findDictsByClass dicts cls
664 other_ip_dicts = filterBag (not . is_this_ip) ip_dicts
665 filtered_dicts = addDictsByClass dicts cls other_ip_dicts
666
667 -- Pick out any Given constraints for the same implicit parameter
668 is_this_ip (CDictCan { cc_ev = ev, cc_tyargs = ip_str':_ })
669 = isGiven ev && ip_str `tcEqType` ip_str'
670 is_this_ip _ = False
671
672 interactGivenIP _ wi = pprPanic "interactGivenIP" (ppr wi)
673
674 addFunDepWork :: Ct -> Ct -> TcS ()
675 addFunDepWork work_ct inert_ct
676 = do { let fd_eqns :: [Equation CtLoc]
677 fd_eqns = [ eqn { fd_loc = derived_loc }
678 | eqn <- improveFromAnother inert_pred work_pred ]
679 ; rewriteWithFunDeps fd_eqns
680 -- We don't really rewrite tys2, see below _rewritten_tys2, so that's ok
681 -- NB: We do create FDs for given to report insoluble equations that arise
682 -- from pairs of Givens, and also because of floating when we approximate
683 -- implications. The relevant test is: typecheck/should_fail/FDsFromGivens.hs
684 -- Also see Note [When improvement happens]
685 }
686 where
687 work_pred = ctPred work_ct
688 inert_pred = ctPred inert_ct
689 work_loc = ctLoc work_ct
690 inert_loc = ctLoc inert_ct
691 derived_loc = work_loc { ctl_origin = FunDepOrigin1 work_pred work_loc
692 inert_pred inert_loc }
693
694 {-
695 Note [Shadowing of Implicit Parameters]
696 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
697 Consider the following example:
698
699 f :: (?x :: Char) => Char
700 f = let ?x = 'a' in ?x
701
702 The "let ?x = ..." generates an implication constraint of the form:
703
704 ?x :: Char => ?x :: Char
705
706 Furthermore, the signature for `f` also generates an implication
707 constraint, so we end up with the following nested implication:
708
709 ?x :: Char => (?x :: Char => ?x :: Char)
710
711 Note that the wanted (?x :: Char) constraint may be solved in
712 two incompatible ways: either by using the parameter from the
713 signature, or by using the local definition. Our intention is
714 that the local definition should "shadow" the parameter of the
715 signature, and we implement this as follows: when we add a new
716 *given* implicit parameter to the inert set, it replaces any existing
717 givens for the same implicit parameter.
718
719 This works for the normal cases but it has an odd side effect
720 in some pathological programs like this:
721
722 -- This is accepted, the second parameter shadows
723 f1 :: (?x :: Int, ?x :: Char) => Char
724 f1 = ?x
725
726 -- This is rejected, the second parameter shadows
727 f2 :: (?x :: Int, ?x :: Char) => Int
728 f2 = ?x
729
730 Both of these are actually wrong: when we try to use either one,
731 we'll get two incompatible wnated constraints (?x :: Int, ?x :: Char),
732 which would lead to an error.
733
734 I can think of two ways to fix this:
735
736 1. Simply disallow multiple constratits for the same implicit
737 parameter---this is never useful, and it can be detected completely
738 syntactically.
739
740 2. Move the shadowing machinery to the location where we nest
741 implications, and add some code here that will produce an
742 error if we get multiple givens for the same implicit parameter.
743
744
745 *********************************************************************************
746 * *
747 interactFunEq
748 * *
749 *********************************************************************************
750 -}
751
752 interactFunEq :: InertCans -> Ct -> TcS (StopOrContinue Ct)
753 -- Try interacting the work item with the inert set
754 interactFunEq inerts workItem@(CFunEqCan { cc_ev = ev, cc_fun = tc
755 , cc_tyargs = args, cc_fsk = fsk })
756 | Just (CFunEqCan { cc_ev = ev_i, cc_fsk = fsk_i }) <- matching_inerts
757 = if ev_i `canRewriteOrSame` ev
758 then -- Rewrite work-item using inert
759 do { traceTcS "reactFunEq (discharge work item):" $
760 vcat [ text "workItem =" <+> ppr workItem
761 , text "inertItem=" <+> ppr ev_i ]
762 ; reactFunEq ev_i fsk_i ev fsk
763 ; stopWith ev "Inert rewrites work item" }
764 else -- Rewrite intert using work-item
765 do { traceTcS "reactFunEq (rewrite inert item):" $
766 vcat [ text "workItem =" <+> ppr workItem
767 , text "inertItem=" <+> ppr ev_i ]
768 ; updInertFunEqs $ \ feqs -> insertFunEq feqs tc args workItem
769 -- Do the updInertFunEqs before the reactFunEq, so that
770 -- we don't kick out the inertItem as well as consuming it!
771 ; reactFunEq ev fsk ev_i fsk_i
772 ; stopWith ev "Work item rewrites inert" }
773
774 | Just ops <- isBuiltInSynFamTyCon_maybe tc
775 = do { let matching_funeqs = findFunEqsByTyCon funeqs tc
776 ; let interact = sfInteractInert ops args (lookupFlattenTyVar eqs fsk)
777 do_one (CFunEqCan { cc_tyargs = iargs, cc_fsk = ifsk, cc_ev = iev })
778 = mapM_ (unifyDerived (ctEvLoc iev) Nominal)
779 (interact iargs (lookupFlattenTyVar eqs ifsk))
780 do_one ct = pprPanic "interactFunEq" (ppr ct)
781 ; mapM_ do_one matching_funeqs
782 ; traceTcS "builtInCandidates 1: " $ vcat [ ptext (sLit "Candidates:") <+> ppr matching_funeqs
783 , ptext (sLit "TvEqs:") <+> ppr eqs ]
784 ; return (ContinueWith workItem) }
785
786 | otherwise
787 = return (ContinueWith workItem)
788 where
789 eqs = inert_eqs inerts
790 funeqs = inert_funeqs inerts
791 matching_inerts = findFunEqs funeqs tc args
792
793 interactFunEq _ wi = pprPanic "interactFunEq" (ppr wi)
794
795 lookupFlattenTyVar :: TyVarEnv EqualCtList -> TcTyVar -> TcType
796 -- ^ Look up a flatten-tyvar in the inert nominal TyVarEqs;
797 -- this is used only when dealing with a CFunEqCan
798 lookupFlattenTyVar inert_eqs ftv
799 = case lookupVarEnv inert_eqs ftv of
800 Just (CTyEqCan { cc_rhs = rhs, cc_eq_rel = NomEq } : _) -> rhs
801 _ -> mkTyVarTy ftv
802
803 reactFunEq :: CtEvidence -> TcTyVar -- From this :: F tys ~ fsk1
804 -> CtEvidence -> TcTyVar -- Solve this :: F tys ~ fsk2
805 -> TcS ()
806 reactFunEq from_this fsk1 (CtGiven { ctev_evtm = tm, ctev_loc = loc }) fsk2
807 = do { let fsk_eq_co = mkTcSymCo (evTermCoercion tm)
808 `mkTcTransCo` ctEvCoercion from_this
809 -- :: fsk2 ~ fsk1
810 fsk_eq_pred = mkTcEqPred (mkTyVarTy fsk2) (mkTyVarTy fsk1)
811 ; new_ev <- newGivenEvVar loc (fsk_eq_pred, EvCoercion fsk_eq_co)
812 ; emitWorkNC [new_ev] }
813
814 reactFunEq from_this fuv1 (CtWanted { ctev_evar = evar }) fuv2
815 = dischargeFmv evar fuv2 (ctEvCoercion from_this) (mkTyVarTy fuv1)
816
817 reactFunEq _ _ solve_this@(CtDerived {}) _
818 = pprPanic "reactFunEq" (ppr solve_this)
819
820 {-
821 Note [Cache-caused loops]
822 ~~~~~~~~~~~~~~~~~~~~~~~~~
823 It is very dangerous to cache a rewritten wanted family equation as 'solved' in our
824 solved cache (which is the default behaviour or xCtEvidence), because the interaction
825 may not be contributing towards a solution. Here is an example:
826
827 Initial inert set:
828 [W] g1 : F a ~ beta1
829 Work item:
830 [W] g2 : F a ~ beta2
831 The work item will react with the inert yielding the _same_ inert set plus:
832 i) Will set g2 := g1 `cast` g3
833 ii) Will add to our solved cache that [S] g2 : F a ~ beta2
834 iii) Will emit [W] g3 : beta1 ~ beta2
835 Now, the g3 work item will be spontaneously solved to [G] g3 : beta1 ~ beta2
836 and then it will react the item in the inert ([W] g1 : F a ~ beta1). So it
837 will set
838 g1 := g ; sym g3
839 and what is g? Well it would ideally be a new goal of type (F a ~ beta2) but
840 remember that we have this in our solved cache, and it is ... g2! In short we
841 created the evidence loop:
842
843 g2 := g1 ; g3
844 g3 := refl
845 g1 := g2 ; sym g3
846
847 To avoid this situation we do not cache as solved any workitems (or inert)
848 which did not really made a 'step' towards proving some goal. Solved's are
849 just an optimization so we don't lose anything in terms of completeness of
850 solving.
851
852
853 Note [Efficient Orientation]
854 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
855 Suppose we are interacting two FunEqCans with the same LHS:
856 (inert) ci :: (F ty ~ xi_i)
857 (work) cw :: (F ty ~ xi_w)
858 We prefer to keep the inert (else we pass the work item on down
859 the pipeline, which is a bit silly). If we keep the inert, we
860 will (a) discharge 'cw'
861 (b) produce a new equality work-item (xi_w ~ xi_i)
862 Notice the orientation (xi_w ~ xi_i) NOT (xi_i ~ xi_w):
863 new_work :: xi_w ~ xi_i
864 cw := ci ; sym new_work
865 Why? Consider the simplest case when xi1 is a type variable. If
866 we generate xi1~xi2, porcessing that constraint will kick out 'ci'.
867 If we generate xi2~xi1, there is less chance of that happening.
868 Of course it can and should still happen if xi1=a, xi1=Int, say.
869 But we want to avoid it happening needlessly.
870
871 Similarly, if we *can't* keep the inert item (because inert is Wanted,
872 and work is Given, say), we prefer to orient the new equality (xi_i ~
873 xi_w).
874
875 Note [Carefully solve the right CFunEqCan]
876 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
877 ---- OLD COMMENT, NOW NOT NEEDED
878 ---- because we now allow multiple
879 ---- wanted FunEqs with the same head
880 Consider the constraints
881 c1 :: F Int ~ a -- Arising from an application line 5
882 c2 :: F Int ~ Bool -- Arising from an application line 10
883 Suppose that 'a' is a unification variable, arising only from
884 flattening. So there is no error on line 5; it's just a flattening
885 variable. But there is (or might be) an error on line 10.
886
887 Two ways to combine them, leaving either (Plan A)
888 c1 :: F Int ~ a -- Arising from an application line 5
889 c3 :: a ~ Bool -- Arising from an application line 10
890 or (Plan B)
891 c2 :: F Int ~ Bool -- Arising from an application line 10
892 c4 :: a ~ Bool -- Arising from an application line 5
893
894 Plan A will unify c3, leaving c1 :: F Int ~ Bool as an error
895 on the *totally innocent* line 5. An example is test SimpleFail16
896 where the expected/actual message comes out backwards if we use
897 the wrong plan.
898
899 The second is the right thing to do. Hence the isMetaTyVarTy
900 test when solving pairwise CFunEqCan.
901
902
903 *********************************************************************************
904 * *
905 interactTyVarEq
906 * *
907 *********************************************************************************
908 -}
909
910 interactTyVarEq :: InertCans -> Ct -> TcS (StopOrContinue Ct)
911 -- CTyEqCans are always consumed, so always returns Stop
912 interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv
913 , cc_rhs = rhs
914 , cc_ev = ev
915 , cc_eq_rel = eq_rel })
916 | (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i }
917 <- findTyEqs inerts tv
918 , ev_i `canRewriteOrSame` ev
919 , rhs_i `tcEqType` rhs ]
920 = -- Inert: a ~ b
921 -- Work item: a ~ b
922 do { setEvBindIfWanted ev (ctEvTerm ev_i)
923 ; stopWith ev "Solved from inert" }
924
925 | Just tv_rhs <- getTyVar_maybe rhs
926 , (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i }
927 <- findTyEqs inerts tv_rhs
928 , ev_i `canRewriteOrSame` ev
929 , rhs_i `tcEqType` mkTyVarTy tv ]
930 = -- Inert: a ~ b
931 -- Work item: b ~ a
932 do { setEvBindIfWanted ev
933 (EvCoercion (mkTcSymCo (ctEvCoercion ev_i)))
934 ; stopWith ev "Solved from inert (r)" }
935
936 | otherwise
937 = do { tclvl <- getTcLevel
938 ; if canSolveByUnification tclvl ev eq_rel tv rhs
939 then do { solveByUnification ev tv rhs
940 ; n_kicked <- kickOutRewritable Given NomEq tv
941 -- Given because the tv := xi is given
942 -- NomEq because only nom. equalities are solved
943 -- by unification
944 ; return (Stop ev (ptext (sLit "Spontaneously solved") <+> ppr_kicked n_kicked)) }
945
946 else do { traceTcS "Can't solve tyvar equality"
947 (vcat [ text "LHS:" <+> ppr tv <+> dcolon <+> ppr (tyVarKind tv)
948 , ppWhen (isMetaTyVar tv) $
949 nest 4 (text "TcLevel of" <+> ppr tv
950 <+> text "is" <+> ppr (metaTyVarTcLevel tv))
951 , text "RHS:" <+> ppr rhs <+> dcolon <+> ppr (typeKind rhs)
952 , text "TcLevel =" <+> ppr tclvl ])
953 ; n_kicked <- kickOutRewritable (ctEvFlavour ev)
954 (ctEvEqRel ev)
955 tv
956 ; updInertCans (\ ics -> addInertCan ics workItem)
957 ; return (Stop ev (ptext (sLit "Kept as inert") <+> ppr_kicked n_kicked)) } }
958
959 interactTyVarEq _ wi = pprPanic "interactTyVarEq" (ppr wi)
960
961 -- @trySpontaneousSolve wi@ solves equalities where one side is a
962 -- touchable unification variable.
963 -- Returns True <=> spontaneous solve happened
964 canSolveByUnification :: TcLevel -> CtEvidence -> EqRel
965 -> TcTyVar -> Xi -> Bool
966 canSolveByUnification tclvl gw eq_rel tv xi
967 | ReprEq <- eq_rel -- we never solve representational equalities this way.
968 = False
969
970 | isGiven gw -- See Note [Touchables and givens]
971 = False
972
973 | isTouchableMetaTyVar tclvl tv
974 = case metaTyVarInfo tv of
975 SigTv -> is_tyvar xi
976 _ -> True
977
978 | otherwise -- Untouchable
979 = False
980 where
981 is_tyvar xi
982 = case tcGetTyVar_maybe xi of
983 Nothing -> False
984 Just tv -> case tcTyVarDetails tv of
985 MetaTv { mtv_info = info }
986 -> case info of
987 SigTv -> True
988 _ -> False
989 SkolemTv {} -> True
990 FlatSkol {} -> False
991 RuntimeUnk -> True
992
993 solveByUnification :: CtEvidence -> TcTyVar -> Xi -> TcS ()
994 -- Solve with the identity coercion
995 -- Precondition: kind(xi) is a sub-kind of kind(tv)
996 -- Precondition: CtEvidence is Wanted or Derived
997 -- Precondition: CtEvidence is nominal
998 -- Returns: workItem where
999 -- workItem = the new Given constraint
1000 --
1001 -- NB: No need for an occurs check here, because solveByUnification always
1002 -- arises from a CTyEqCan, a *canonical* constraint. Its invariants
1003 -- say that in (a ~ xi), the type variable a does not appear in xi.
1004 -- See TcRnTypes.Ct invariants.
1005 --
1006 -- Post: tv is unified (by side effect) with xi;
1007 -- we often write tv := xi
1008 solveByUnification wd tv xi
1009 = do { let tv_ty = mkTyVarTy tv
1010 ; traceTcS "Sneaky unification:" $
1011 vcat [text "Unifies:" <+> ppr tv <+> ptext (sLit ":=") <+> ppr xi,
1012 text "Coercion:" <+> pprEq tv_ty xi,
1013 text "Left Kind is:" <+> ppr (typeKind tv_ty),
1014 text "Right Kind is:" <+> ppr (typeKind xi) ]
1015
1016 ; let xi' = defaultKind xi
1017 -- We only instantiate kind unification variables
1018 -- with simple kinds like *, not OpenKind or ArgKind
1019 -- cf TcUnify.uUnboundKVar
1020
1021 ; setWantedTyBind tv xi'
1022 ; setEvBindIfWanted wd (EvCoercion (mkTcNomReflCo xi')) }
1023
1024
1025 ppr_kicked :: Int -> SDoc
1026 ppr_kicked 0 = empty
1027 ppr_kicked n = parens (int n <+> ptext (sLit "kicked out"))
1028
1029 kickOutRewritable :: CtFlavour -- Flavour of the equality that is
1030 -- being added to the inert set
1031 -> EqRel -- of the new equality
1032 -> TcTyVar -- The new equality is tv ~ ty
1033 -> TcS Int
1034 kickOutRewritable new_flavour new_eq_rel new_tv
1035 | not ((new_flavour, new_eq_rel) `eqCanRewriteFR` (new_flavour, new_eq_rel))
1036 = return 0 -- If new_flavour can't rewrite itself, it can't rewrite
1037 -- anything else, so no need to kick out anything
1038 -- This is a common case: wanteds can't rewrite wanteds
1039
1040 | otherwise
1041 = do { ics <- getInertCans
1042 ; let (kicked_out, ics') = kick_out new_flavour new_eq_rel new_tv ics
1043 ; setInertCans ics'
1044 ; updWorkListTcS (appendWorkList kicked_out)
1045
1046 ; unless (isEmptyWorkList kicked_out) $
1047 csTraceTcS $
1048 hang (ptext (sLit "Kick out, tv =") <+> ppr new_tv)
1049 2 (vcat [ text "n-kicked =" <+> int (workListSize kicked_out)
1050 , text "n-kept fun-eqs =" <+> int (sizeFunEqMap (inert_funeqs ics'))
1051 , ppr kicked_out ])
1052 ; return (workListSize kicked_out) }
1053
1054 kick_out :: CtFlavour -> EqRel -> TcTyVar -> InertCans -> (WorkList, InertCans)
1055 kick_out new_flavour new_eq_rel new_tv (IC { inert_eqs = tv_eqs
1056 , inert_dicts = dictmap
1057 , inert_funeqs = funeqmap
1058 , inert_irreds = irreds
1059 , inert_insols = insols })
1060 = (kicked_out, inert_cans_in)
1061 where
1062 -- NB: Notice that don't rewrite
1063 -- inert_solved_dicts, and inert_solved_funeqs
1064 -- optimistically. But when we lookup we have to
1065 -- take the substitution into account
1066 inert_cans_in = IC { inert_eqs = tv_eqs_in
1067 , inert_dicts = dicts_in
1068 , inert_funeqs = feqs_in
1069 , inert_irreds = irs_in
1070 , inert_insols = insols_in }
1071
1072 kicked_out = WL { wl_eqs = tv_eqs_out
1073 , wl_funeqs = feqs_out
1074 , wl_rest = bagToList (dicts_out `andCts` irs_out
1075 `andCts` insols_out)
1076 , wl_implics = emptyBag }
1077
1078 (tv_eqs_out, tv_eqs_in) = foldVarEnv kick_out_eqs ([], emptyVarEnv) tv_eqs
1079 (feqs_out, feqs_in) = partitionFunEqs kick_out_ct funeqmap
1080 (dicts_out, dicts_in) = partitionDicts kick_out_ct dictmap
1081 (irs_out, irs_in) = partitionBag kick_out_irred irreds
1082 (insols_out, insols_in) = partitionBag kick_out_ct insols
1083 -- Kick out even insolubles; see Note [Kick out insolubles]
1084
1085 can_rewrite :: CtEvidence -> Bool
1086 can_rewrite = ((new_flavour, new_eq_rel) `eqCanRewriteFR`) . ctEvFlavourRole
1087
1088 kick_out_ct :: Ct -> Bool
1089 kick_out_ct ct = kick_out_ctev (ctEvidence ct)
1090
1091 kick_out_ctev :: CtEvidence -> Bool
1092 kick_out_ctev ev = can_rewrite ev
1093 && new_tv `elemVarSet` tyVarsOfType (ctEvPred ev)
1094 -- See Note [Kicking out inert constraints]
1095
1096 kick_out_irred :: Ct -> Bool
1097 kick_out_irred ct = can_rewrite (cc_ev ct)
1098 && new_tv `elemVarSet` closeOverKinds (tyVarsOfCt ct)
1099 -- See Note [Kicking out Irreds]
1100
1101 kick_out_eqs :: EqualCtList -> ([Ct], TyVarEnv EqualCtList)
1102 -> ([Ct], TyVarEnv EqualCtList)
1103 kick_out_eqs eqs (acc_out, acc_in)
1104 = (eqs_out ++ acc_out, case eqs_in of
1105 [] -> acc_in
1106 (eq1:_) -> extendVarEnv acc_in (cc_tyvar eq1) eqs_in)
1107 where
1108 (eqs_in, eqs_out) = partition keep_eq eqs
1109
1110 -- implements criteria K1-K3 in Note [The inert equalities] in TcFlatten
1111 keep_eq (CTyEqCan { cc_tyvar = tv, cc_rhs = rhs_ty, cc_ev = ev
1112 , cc_eq_rel = eq_rel })
1113 | tv == new_tv
1114 = not (can_rewrite ev) -- (K1)
1115
1116 | otherwise
1117 = check_k2 && check_k3
1118 where
1119 check_k2 = not (ev `eqCanRewrite` ev)
1120 || not (can_rewrite ev)
1121 || not (new_tv `elemVarSet` tyVarsOfType rhs_ty)
1122
1123 check_k3
1124 | can_rewrite ev
1125 = case eq_rel of
1126 NomEq -> not (rhs_ty `eqType` mkTyVarTy new_tv)
1127 ReprEq -> isTyVarExposed new_tv rhs_ty
1128
1129 | otherwise
1130 = True
1131
1132 keep_eq ct = pprPanic "keep_eq" (ppr ct)
1133
1134 {-
1135 Note [Kicking out inert constraints]
1136 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1137 Given a new (a -> ty) inert, we want to kick out an existing inert
1138 constraint if
1139 a) the new constraint can rewrite the inert one
1140 b) 'a' is free in the inert constraint (so that it *will*)
1141 rewrite it if we kick it out.
1142
1143 For (b) we use tyVarsOfCt, which returns the type variables /and
1144 the kind variables/ that are directly visible in the type. Hence we
1145 will have exposed all the rewriting we care about to make the most
1146 precise kinds visible for matching classes etc. No need to kick out
1147 constraints that mention type variables whose kinds contain this
1148 variable! (Except see Note [Kicking out Irreds].)
1149
1150 Note [Kicking out Irreds]
1151 ~~~~~~~~~~~~~~~~~~~~~~~~~
1152 There is an awkward special case for Irreds. When we have a
1153 kind-mis-matched equality constraint (a:k1) ~ (ty:k2), we turn it into
1154 an Irred (see Note [Equalities with incompatible kinds] in
1155 TcCanonical). So in this case the free kind variables of k1 and k2
1156 are not visible. More precisely, the type looks like
1157 (~) k1 (a:k1) (ty:k2)
1158 because (~) has kind forall k. k -> k -> Constraint. So the constraint
1159 itself is ill-kinded. We can "see" k1 but not k2. That's why we use
1160 closeOverKinds to make sure we see k2.
1161
1162 This is not pretty. Maybe (~) should have kind
1163 (~) :: forall k1 k1. k1 -> k2 -> Constraint
1164
1165 Note [Kick out insolubles]
1166 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1167 Suppose we have an insoluble alpha ~ [alpha], which is insoluble
1168 because an occurs check. And then we unify alpha := [Int].
1169 Then we really want to rewrite the insouluble to [Int] ~ [[Int]].
1170 Now it can be decomposed. Otherwise we end up with a "Can't match
1171 [Int] ~ [[Int]]" which is true, but a bit confusing because the
1172 outer type constructors match.
1173
1174
1175 Note [Avoid double unifications]
1176 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1177 The spontaneous solver has to return a given which mentions the unified unification
1178 variable *on the left* of the equality. Here is what happens if not:
1179 Original wanted: (a ~ alpha), (alpha ~ Int)
1180 We spontaneously solve the first wanted, without changing the order!
1181 given : a ~ alpha [having unified alpha := a]
1182 Now the second wanted comes along, but he cannot rewrite the given, so we simply continue.
1183 At the end we spontaneously solve that guy, *reunifying* [alpha := Int]
1184
1185 We avoid this problem by orienting the resulting given so that the unification
1186 variable is on the left. [Note that alternatively we could attempt to
1187 enforce this at canonicalization]
1188
1189 See also Note [No touchables as FunEq RHS] in TcSMonad; avoiding
1190 double unifications is the main reason we disallow touchable
1191 unification variables as RHS of type family equations: F xis ~ alpha.
1192
1193
1194 ************************************************************************
1195 * *
1196 * Functional dependencies, instantiation of equations
1197 * *
1198 ************************************************************************
1199
1200 When we spot an equality arising from a functional dependency,
1201 we now use that equality (a "wanted") to rewrite the work-item
1202 constraint right away. This avoids two dangers
1203
1204 Danger 1: If we send the original constraint on down the pipeline
1205 it may react with an instance declaration, and in delicate
1206 situations (when a Given overlaps with an instance) that
1207 may produce new insoluble goals: see Trac #4952
1208
1209 Danger 2: If we don't rewrite the constraint, it may re-react
1210 with the same thing later, and produce the same equality
1211 again --> termination worries.
1212
1213 To achieve this required some refactoring of FunDeps.lhs (nicer
1214 now!).
1215 -}
1216
1217 rewriteWithFunDeps :: [Equation CtLoc] -> TcS ()
1218 -- NB: The returned constraints are all Derived
1219 -- Post: returns no trivial equalities (identities) and all EvVars returned are fresh
1220 rewriteWithFunDeps eqn_pred_locs
1221 = mapM_ instFunDepEqn eqn_pred_locs
1222
1223 instFunDepEqn :: Equation CtLoc -> TcS ()
1224 -- Post: Returns the position index as well as the corresponding FunDep equality
1225 instFunDepEqn (FDEqn { fd_qtvs = tvs, fd_eqs = eqs, fd_loc = loc })
1226 = do { (subst, _) <- instFlexiTcS tvs -- Takes account of kind substitution
1227 ; mapM_ (do_one subst) eqs }
1228 where
1229 do_one subst (FDEq { fd_ty_left = ty1, fd_ty_right = ty2 })
1230 = unifyDerived loc Nominal $
1231 Pair (Type.substTy subst ty1) (Type.substTy subst ty2)
1232
1233 {-
1234 *********************************************************************************
1235 * *
1236 The top-reaction Stage
1237 * *
1238 *********************************************************************************
1239 -}
1240
1241 topReactionsStage :: WorkItem -> TcS (StopOrContinue Ct)
1242 topReactionsStage wi
1243 = do { inerts <- getTcSInerts
1244 ; tir <- doTopReact inerts wi
1245 ; case tir of
1246 ContinueWith wi -> return (ContinueWith wi)
1247 Stop ev s -> return (Stop ev (ptext (sLit "Top react:") <+> s)) }
1248
1249 doTopReact :: InertSet -> WorkItem -> TcS (StopOrContinue Ct)
1250 -- The work item does not react with the inert set, so try interaction with top-level
1251 -- instances. Note:
1252 --
1253 -- (a) The place to add superclasses in not here in doTopReact stage.
1254 -- Instead superclasses are added in the worklist as part of the
1255 -- canonicalization process. See Note [Adding superclasses].
1256
1257 doTopReact inerts work_item
1258 = do { traceTcS "doTopReact" (ppr work_item)
1259 ; case work_item of
1260 CDictCan {} -> doTopReactDict inerts work_item
1261 CFunEqCan {} -> doTopReactFunEq work_item
1262 _ -> -- Any other work item does not react with any top-level equations
1263 return (ContinueWith work_item) }
1264
1265 --------------------
1266 doTopReactDict :: InertSet -> Ct -> TcS (StopOrContinue Ct)
1267 -- Try to use type-class instance declarations to simplify the constraint
1268 doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls
1269 , cc_tyargs = xis })
1270 | not (isWanted fl) -- Never use instances for Given or Derived constraints
1271 = try_fundeps_and_return
1272
1273 | Just ev <- lookupSolvedDict inerts loc cls xis -- Cached
1274 = do { setWantedEvBind dict_id (ctEvTerm ev);
1275 ; stopWith fl "Dict/Top (cached)" }
1276
1277 | otherwise -- Not cached
1278 = do { lkup_inst_res <- matchClassInst inerts cls xis loc
1279 ; case lkup_inst_res of
1280 GenInst wtvs ev_term -> do { addSolvedDict fl cls xis
1281 ; solve_from_instance wtvs ev_term }
1282 NoInstance -> try_fundeps_and_return }
1283 where
1284 dict_id = ASSERT( isWanted fl ) ctEvId fl
1285 pred = mkClassPred cls xis
1286 loc = ctEvLoc fl
1287
1288 solve_from_instance :: [CtEvidence] -> EvTerm -> TcS (StopOrContinue Ct)
1289 -- Precondition: evidence term matches the predicate workItem
1290 solve_from_instance evs ev_term
1291 | null evs
1292 = do { traceTcS "doTopReact/found nullary instance for" $
1293 ppr dict_id
1294 ; setWantedEvBind dict_id ev_term
1295 ; stopWith fl "Dict/Top (solved, no new work)" }
1296 | otherwise
1297 = do { traceTcS "doTopReact/found non-nullary instance for" $
1298 ppr dict_id
1299 ; setWantedEvBind dict_id ev_term
1300 ; let mk_new_wanted ev
1301 = mkNonCanonical (ev {ctev_loc = bumpCtLocDepth CountConstraints loc })
1302 ; updWorkListTcS (extendWorkListCts (map mk_new_wanted evs))
1303 ; stopWith fl "Dict/Top (solved, more work)" }
1304
1305 -- We didn't solve it; so try functional dependencies with
1306 -- the instance environment, and return
1307 -- NB: even if there *are* some functional dependencies against the
1308 -- instance environment, there might be a unique match, and if
1309 -- so we make sure we get on and solve it first. See Note [Weird fundeps]
1310 try_fundeps_and_return
1311 = do { instEnvs <- getInstEnvs
1312 ; let fd_eqns :: [Equation CtLoc]
1313 fd_eqns = [ fd { fd_loc = loc { ctl_origin = FunDepOrigin2 pred (ctl_origin loc)
1314 inst_pred inst_loc } }
1315 | fd@(FDEqn { fd_loc = inst_loc, fd_pred1 = inst_pred })
1316 <- improveFromInstEnv instEnvs pred ]
1317 ; rewriteWithFunDeps fd_eqns
1318 ; continueWith work_item }
1319
1320 doTopReactDict _ w = pprPanic "doTopReactDict" (ppr w)
1321
1322 --------------------
1323 doTopReactFunEq :: Ct -> TcS (StopOrContinue Ct)
1324 doTopReactFunEq work_item@(CFunEqCan { cc_ev = old_ev, cc_fun = fam_tc
1325 , cc_tyargs = args , cc_fsk = fsk })
1326 = ASSERT(isTypeFamilyTyCon fam_tc) -- No associated data families
1327 -- have reached this far
1328 ASSERT( not (isDerived old_ev) ) -- CFunEqCan is never Derived
1329 -- Look up in top-level instances, or built-in axiom
1330 do { match_res <- matchFam fam_tc args -- See Note [MATCHING-SYNONYMS]
1331 ; case match_res of {
1332 Nothing -> do { try_improvement; continueWith work_item } ;
1333 Just (ax_co, rhs_ty)
1334
1335 -- Found a top-level instance
1336
1337 | Just (tc, tc_args) <- tcSplitTyConApp_maybe rhs_ty
1338 , isTypeFamilyTyCon tc
1339 , tc_args `lengthIs` tyConArity tc -- Short-cut
1340 -> shortCutReduction old_ev fsk ax_co tc tc_args
1341 -- Try shortcut; see Note [Short cut for top-level reaction]
1342
1343 | isGiven old_ev -- Not shortcut
1344 -> do { let final_co = mkTcSymCo (ctEvCoercion old_ev) `mkTcTransCo` ax_co
1345 -- final_co :: fsk ~ rhs_ty
1346 ; new_ev <- newGivenEvVar deeper_loc (mkTcEqPred (mkTyVarTy fsk) rhs_ty,
1347 EvCoercion final_co)
1348 ; emitWorkNC [new_ev] -- Non-cannonical; that will mean we flatten rhs_ty
1349 ; stopWith old_ev "Fun/Top (given)" }
1350
1351 | not (fsk `elemVarSet` tyVarsOfType rhs_ty)
1352 -> do { dischargeFmv (ctEvId old_ev) fsk ax_co rhs_ty
1353 ; traceTcS "doTopReactFunEq" $
1354 vcat [ text "old_ev:" <+> ppr old_ev
1355 , nest 2 (text ":=") <+> ppr ax_co ]
1356 ; stopWith old_ev "Fun/Top (wanted)" }
1357
1358 | otherwise -- We must not assign ufsk := ...ufsk...!
1359 -> do { alpha_ty <- newFlexiTcSTy (tyVarKind fsk)
1360 ; new_ev <- newWantedEvVarNC loc (mkTcEqPred alpha_ty rhs_ty)
1361 ; emitWorkNC [new_ev]
1362 -- By emitting this as non-canonical, we deal with all
1363 -- flattening, occurs-check, and ufsk := ufsk issues
1364 ; let final_co = ax_co `mkTcTransCo` mkTcSymCo (ctEvCoercion new_ev)
1365 -- ax_co :: fam_tc args ~ rhs_ty
1366 -- new_ev :: alpha ~ rhs_ty
1367 -- ufsk := alpha
1368 -- final_co :: fam_tc args ~ alpha
1369 ; dischargeFmv (ctEvId old_ev) fsk final_co alpha_ty
1370 ; traceTcS "doTopReactFunEq (occurs)" $
1371 vcat [ text "old_ev:" <+> ppr old_ev
1372 , nest 2 (text ":=") <+> ppr final_co
1373 , text "new_ev:" <+> ppr new_ev ]
1374 ; stopWith old_ev "Fun/Top (wanted)" } } }
1375 where
1376 loc = ctEvLoc old_ev
1377 deeper_loc = bumpCtLocDepth CountTyFunApps loc
1378
1379 try_improvement
1380 | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc
1381 = do { inert_eqs <- getInertEqs
1382 ; let eqns = sfInteractTop ops args (lookupFlattenTyVar inert_eqs fsk)
1383 ; mapM_ (unifyDerived loc Nominal) eqns }
1384 | otherwise
1385 = return ()
1386
1387 doTopReactFunEq w = pprPanic "doTopReactFunEq" (ppr w)
1388
1389 shortCutReduction :: CtEvidence -> TcTyVar -> TcCoercion
1390 -> TyCon -> [TcType] -> TcS (StopOrContinue Ct)
1391 shortCutReduction old_ev fsk ax_co fam_tc tc_args
1392 | isGiven old_ev
1393 = ASSERT( ctEvEqRel old_ev == NomEq )
1394 runFlatten $
1395 do { (xis, cos) <- flattenManyNom old_ev tc_args
1396 -- ax_co :: F args ~ G tc_args
1397 -- cos :: xis ~ tc_args
1398 -- old_ev :: F args ~ fsk
1399 -- G cos ; sym ax_co ; old_ev :: G xis ~ fsk
1400
1401 ; new_ev <- newGivenEvVar deeper_loc
1402 ( mkTcEqPred (mkTyConApp fam_tc xis) (mkTyVarTy fsk)
1403 , EvCoercion (mkTcTyConAppCo Nominal fam_tc cos
1404 `mkTcTransCo` mkTcSymCo ax_co
1405 `mkTcTransCo` ctEvCoercion old_ev) )
1406
1407 ; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc, cc_tyargs = xis, cc_fsk = fsk }
1408 ; emitFlatWork new_ct
1409 ; stopWith old_ev "Fun/Top (given, shortcut)" }
1410
1411 | otherwise
1412 = ASSERT( not (isDerived old_ev) ) -- Caller ensures this
1413 ASSERT( ctEvEqRel old_ev == NomEq )
1414 do { (xis, cos) <- flattenManyNom old_ev tc_args
1415 -- ax_co :: F args ~ G tc_args
1416 -- cos :: xis ~ tc_args
1417 -- G cos ; sym ax_co ; old_ev :: G xis ~ fsk
1418 -- new_ev :: G xis ~ fsk
1419 -- old_ev :: F args ~ fsk := ax_co ; sym (G cos) ; new_ev
1420
1421 ; new_ev <- newWantedEvVarNC deeper_loc
1422 (mkTcEqPred (mkTyConApp fam_tc xis) (mkTyVarTy fsk))
1423 ; setWantedEvBind (ctEvId old_ev)
1424 (EvCoercion (ax_co `mkTcTransCo` mkTcSymCo (mkTcTyConAppCo Nominal fam_tc cos)
1425 `mkTcTransCo` ctEvCoercion new_ev))
1426
1427 ; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc, cc_tyargs = xis, cc_fsk = fsk }
1428 ; emitFlatWork new_ct
1429 ; stopWith old_ev "Fun/Top (wanted, shortcut)" }
1430 where
1431 loc = ctEvLoc old_ev
1432 deeper_loc = bumpCtLocDepth CountTyFunApps loc
1433
1434 dischargeFmv :: EvVar -> TcTyVar -> TcCoercion -> TcType -> TcS ()
1435 -- (dischargeFmv x fmv co ty)
1436 -- [W] x :: F tys ~ fuv
1437 -- co :: F tys ~ ty
1438 -- Precondition: fuv is not filled, and fuv `notElem` ty
1439 --
1440 -- Then set fuv := ty,
1441 -- set x := co
1442 -- kick out any inert things that are now rewritable
1443 dischargeFmv evar fmv co xi
1444 = ASSERT2( not (fmv `elemVarSet` tyVarsOfType xi), ppr evar $$ ppr fmv $$ ppr xi )
1445 do { setWantedTyBind fmv xi
1446 ; setWantedEvBind evar (EvCoercion co)
1447 ; n_kicked <- kickOutRewritable Given NomEq fmv
1448 ; traceTcS "dischargeFuv" (ppr fmv <+> equals <+> ppr xi $$ ppr_kicked n_kicked) }
1449
1450 {-
1451 Note [Cached solved FunEqs]
1452 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1453 When trying to solve, say (FunExpensive big-type ~ ty), it's important
1454 to see if we have reduced (FunExpensive big-type) before, lest we
1455 simply repeat it. Hence the lookup in inert_solved_funeqs. Moreover
1456 we must use `canRewriteOrSame` because both uses might (say) be Wanteds,
1457 and we *still* want to save the re-computation.
1458
1459 Note [MATCHING-SYNONYMS]
1460 ~~~~~~~~~~~~~~~~~~~~~~~~
1461 When trying to match a dictionary (D tau) to a top-level instance, or a
1462 type family equation (F taus_1 ~ tau_2) to a top-level family instance,
1463 we do *not* need to expand type synonyms because the matcher will do that for us.
1464
1465
1466 Note [RHS-FAMILY-SYNONYMS]
1467 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1468 The RHS of a family instance is represented as yet another constructor which is
1469 like a type synonym for the real RHS the programmer declared. Eg:
1470 type instance F (a,a) = [a]
1471 Becomes:
1472 :R32 a = [a] -- internal type synonym introduced
1473 F (a,a) ~ :R32 a -- instance
1474
1475 When we react a family instance with a type family equation in the work list
1476 we keep the synonym-using RHS without expansion.
1477
1478 Note [FunDep and implicit parameter reactions]
1479 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1480 Currently, our story of interacting two dictionaries (or a dictionary
1481 and top-level instances) for functional dependencies, and implicit
1482 paramters, is that we simply produce new Derived equalities. So for example
1483
1484 class D a b | a -> b where ...
1485 Inert:
1486 d1 :g D Int Bool
1487 WorkItem:
1488 d2 :w D Int alpha
1489
1490 We generate the extra work item
1491 cv :d alpha ~ Bool
1492 where 'cv' is currently unused. However, this new item can perhaps be
1493 spontaneously solved to become given and react with d2,
1494 discharging it in favour of a new constraint d2' thus:
1495 d2' :w D Int Bool
1496 d2 := d2' |> D Int cv
1497 Now d2' can be discharged from d1
1498
1499 We could be more aggressive and try to *immediately* solve the dictionary
1500 using those extra equalities, but that requires those equalities to carry
1501 evidence and derived do not carry evidence.
1502
1503 If that were the case with the same inert set and work item we might dischard
1504 d2 directly:
1505
1506 cv :w alpha ~ Bool
1507 d2 := d1 |> D Int cv
1508
1509 But in general it's a bit painful to figure out the necessary coercion,
1510 so we just take the first approach. Here is a better example. Consider:
1511 class C a b c | a -> b
1512 And:
1513 [Given] d1 : C T Int Char
1514 [Wanted] d2 : C T beta Int
1515 In this case, it's *not even possible* to solve the wanted immediately.
1516 So we should simply output the functional dependency and add this guy
1517 [but NOT its superclasses] back in the worklist. Even worse:
1518 [Given] d1 : C T Int beta
1519 [Wanted] d2: C T beta Int
1520 Then it is solvable, but its very hard to detect this on the spot.
1521
1522 It's exactly the same with implicit parameters, except that the
1523 "aggressive" approach would be much easier to implement.
1524
1525 Note [When improvement happens]
1526 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1527 We fire an improvement rule when
1528
1529 * Two constraints match (modulo the fundep)
1530 e.g. C t1 t2, C t1 t3 where C a b | a->b
1531 The two match because the first arg is identical
1532
1533 Note that we *do* fire the improvement if one is Given and one is Derived (e.g. a
1534 superclass of a Wanted goal) or if both are Given.
1535
1536 Example (tcfail138)
1537 class L a b | a -> b
1538 class (G a, L a b) => C a b
1539
1540 instance C a b' => G (Maybe a)
1541 instance C a b => C (Maybe a) a
1542 instance L (Maybe a) a
1543
1544 When solving the superclasses of the (C (Maybe a) a) instance, we get
1545 Given: C a b ... and hance by superclasses, (G a, L a b)
1546 Wanted: G (Maybe a)
1547 Use the instance decl to get
1548 Wanted: C a b'
1549 The (C a b') is inert, so we generate its Derived superclasses (L a b'),
1550 and now we need improvement between that derived superclass an the Given (L a b)
1551
1552 Test typecheck/should_fail/FDsFromGivens also shows why it's a good idea to
1553 emit Derived FDs for givens as well.
1554
1555 Note [Weird fundeps]
1556 ~~~~~~~~~~~~~~~~~~~~
1557 Consider class Het a b | a -> b where
1558 het :: m (f c) -> a -> m b
1559
1560 class GHet (a :: * -> *) (b :: * -> *) | a -> b
1561 instance GHet (K a) (K [a])
1562 instance Het a b => GHet (K a) (K b)
1563
1564 The two instances don't actually conflict on their fundeps,
1565 although it's pretty strange. So they are both accepted. Now
1566 try [W] GHet (K Int) (K Bool)
1567 This triggers fudeps from both instance decls; but it also
1568 matches a *unique* instance decl, and we should go ahead and
1569 pick that one right now. Otherwise, if we don't, it ends up
1570 unsolved in the inert set and is reported as an error.
1571
1572 Trac #7875 is a case in point.
1573
1574 Note [Overriding implicit parameters]
1575 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1576 Consider
1577 f :: (?x::a) -> Bool -> a
1578
1579 g v = let ?x::Int = 3
1580 in (f v, let ?x::Bool = True in f v)
1581
1582 This should probably be well typed, with
1583 g :: Bool -> (Int, Bool)
1584
1585 So the inner binding for ?x::Bool *overrides* the outer one.
1586 Hence a work-item Given overrides an inert-item Given.
1587 -}
1588
1589 data LookupInstResult
1590 = NoInstance
1591 | GenInst [CtEvidence] EvTerm
1592
1593 instance Outputable LookupInstResult where
1594 ppr NoInstance = text "NoInstance"
1595 ppr (GenInst ev t) = text "GenInst" <+> ppr ev <+> ppr t
1596
1597
1598 matchClassInst :: InertSet -> Class -> [Type] -> CtLoc -> TcS LookupInstResult
1599
1600 matchClassInst _ clas [ ty ] _
1601 | className clas == knownNatClassName
1602 , Just n <- isNumLitTy ty = makeDict (EvNum n)
1603
1604 | className clas == knownSymbolClassName
1605 , Just s <- isStrLitTy ty = makeDict (EvStr s)
1606
1607 where
1608 {- This adds a coercion that will convert the literal into a dictionary
1609 of the appropriate type. See Note [KnownNat & KnownSymbol and EvLit]
1610 in TcEvidence. The coercion happens in 2 steps:
1611
1612 Integer -> SNat n -- representation of literal to singleton
1613 SNat n -> KnownNat n -- singleton to dictionary
1614
1615 The process is mirrored for Symbols:
1616 String -> SSymbol n
1617 SSymbol n -> KnownSymbol n
1618 -}
1619 makeDict evLit
1620 | Just (_, co_dict) <- tcInstNewTyCon_maybe (classTyCon clas) [ty]
1621 -- co_dict :: KnownNat n ~ SNat n
1622 , [ meth ] <- classMethods clas
1623 , Just tcRep <- tyConAppTyCon_maybe -- SNat
1624 $ funResultTy -- SNat n
1625 $ dropForAlls -- KnownNat n => SNat n
1626 $ idType meth -- forall n. KnownNat n => SNat n
1627 , Just (_, co_rep) <- tcInstNewTyCon_maybe tcRep [ty]
1628 -- SNat n ~ Integer
1629 = return (GenInst [] $ mkEvCast (EvLit evLit) (mkTcSymCo (mkTcTransCo co_dict co_rep)))
1630
1631 | otherwise
1632 = panicTcS (text "Unexpected evidence for" <+> ppr (className clas)
1633 $$ vcat (map (ppr . idType) (classMethods clas)))
1634
1635 matchClassInst inerts clas tys loc
1636 = do { dflags <- getDynFlags
1637 ; tclvl <- getTcLevel
1638 ; traceTcS "matchClassInst" $ vcat [ text "pred =" <+> ppr pred
1639 , text "inerts=" <+> ppr inerts
1640 , text "untouchables=" <+> ppr tclvl ]
1641 ; instEnvs <- getInstEnvs
1642 ; case lookupInstEnv instEnvs clas tys of
1643 ([], _, _) -- Nothing matches
1644 -> do { traceTcS "matchClass not matching" $
1645 vcat [ text "dict" <+> ppr pred ]
1646 ; return NoInstance }
1647
1648 ([(ispec, inst_tys)], [], _) -- A single match
1649 | not (xopt Opt_IncoherentInstances dflags)
1650 , given_overlap tclvl
1651 -> -- See Note [Instance and Given overlap]
1652 do { traceTcS "Delaying instance application" $
1653 vcat [ text "Workitem=" <+> pprType (mkClassPred clas tys)
1654 , text "Relevant given dictionaries=" <+> ppr givens_for_this_clas ]
1655 ; return NoInstance }
1656
1657 | otherwise
1658 -> do { let dfun_id = instanceDFunId ispec
1659 ; traceTcS "matchClass success" $
1660 vcat [text "dict" <+> ppr pred,
1661 text "witness" <+> ppr dfun_id
1662 <+> ppr (idType dfun_id) ]
1663 -- Record that this dfun is needed
1664 ; match_one dfun_id inst_tys }
1665
1666 (matches, _, _) -- More than one matches
1667 -- Defer any reactions of a multitude
1668 -- until we learn more about the reagent
1669 -> do { traceTcS "matchClass multiple matches, deferring choice" $
1670 vcat [text "dict" <+> ppr pred,
1671 text "matches" <+> ppr matches]
1672 ; return NoInstance } }
1673 where
1674 pred = mkClassPred clas tys
1675
1676 match_one :: DFunId -> [DFunInstType] -> TcS LookupInstResult
1677 -- See Note [DFunInstType: instantiating types] in InstEnv
1678 match_one dfun_id mb_inst_tys
1679 = do { checkWellStagedDFun pred dfun_id loc
1680 ; (tys, theta) <- instDFunType dfun_id mb_inst_tys
1681 ; evc_vars <- mapM (newWantedEvVar loc) theta
1682 ; let new_ev_vars = freshGoals evc_vars
1683 -- new_ev_vars are only the real new variables that can be emitted
1684 dfun_app = EvDFunApp dfun_id tys (map (ctEvTerm . fst) evc_vars)
1685 ; return $ GenInst new_ev_vars dfun_app }
1686
1687 givens_for_this_clas :: Cts
1688 givens_for_this_clas
1689 = filterBag isGivenCt (findDictsByClass (inert_dicts $ inert_cans inerts) clas)
1690
1691 given_overlap :: TcLevel -> Bool
1692 given_overlap tclvl = anyBag (matchable tclvl) givens_for_this_clas
1693
1694 matchable tclvl (CDictCan { cc_class = clas_g, cc_tyargs = sys
1695 , cc_ev = fl })
1696 | isGiven fl
1697 = ASSERT( clas_g == clas )
1698 case tcUnifyTys (\tv -> if isTouchableMetaTyVar tclvl tv &&
1699 tv `elemVarSet` tyVarsOfTypes tys
1700 then BindMe else Skolem) tys sys of
1701 -- We can't learn anything more about any variable at this point, so the only
1702 -- cause of overlap can be by an instantiation of a touchable unification
1703 -- variable. Hence we only bind touchable unification variables. In addition,
1704 -- we use tcUnifyTys instead of tcMatchTys to rule out cyclic substitutions.
1705 Nothing -> False
1706 Just _ -> True
1707 | otherwise = False -- No overlap with a solved, already been taken care of
1708 -- by the overlap check with the instance environment.
1709 matchable _tys ct = pprPanic "Expecting dictionary!" (ppr ct)
1710
1711 {-
1712 Note [Instance and Given overlap]
1713 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1714 Example, from the OutsideIn(X) paper:
1715 instance P x => Q [x]
1716 instance (x ~ y) => R y [x]
1717
1718 wob :: forall a b. (Q [b], R b a) => a -> Int
1719
1720 g :: forall a. Q [a] => [a] -> Int
1721 g x = wob x
1722
1723 This will generate the impliation constraint:
1724 Q [a] => (Q [beta], R beta [a])
1725 If we react (Q [beta]) with its top-level axiom, we end up with a
1726 (P beta), which we have no way of discharging. On the other hand,
1727 if we react R beta [a] with the top-level we get (beta ~ a), which
1728 is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
1729 now solvable by the given Q [a].
1730
1731 The solution is that:
1732 In matchClassInst (and thus in topReact), we return a matching
1733 instance only when there is no Given in the inerts which is
1734 unifiable to this particular dictionary.
1735
1736 The end effect is that, much as we do for overlapping instances, we delay choosing a
1737 class instance if there is a possibility of another instance OR a given to match our
1738 constraint later on. This fixes bugs #4981 and #5002.
1739
1740 This is arguably not easy to appear in practice due to our aggressive prioritization
1741 of equality solving over other constraints, but it is possible. I've added a test case
1742 in typecheck/should-compile/GivenOverlapping.hs
1743
1744 We ignore the overlap problem if -XIncoherentInstances is in force: see
1745 Trac #6002 for a worked-out example where this makes a difference.
1746
1747 Moreover notice that our goals here are different than the goals of the top-level
1748 overlapping checks. There we are interested in validating the following principle:
1749
1750 If we inline a function f at a site where the same global instance environment
1751 is available as the instance environment at the definition site of f then we
1752 should get the same behaviour.
1753
1754 But for the Given Overlap check our goal is just related to completeness of
1755 constraint solving.
1756 -}
1757
1758 -- | Is the constraint for an implicit CallStack parameter?
1759 isCallStackIP :: CtLoc -> Class -> Type -> Maybe (EvTerm -> EvCallStack)
1760 isCallStackIP loc cls ty
1761 | Just (tc, []) <- splitTyConApp_maybe ty
1762 , cls `hasKey` ipClassNameKey && tc `hasKey` callStackTyConKey
1763 = occOrigin (ctLocOrigin loc)
1764 where
1765 -- We only want to grab constraints that arose due to the use of an IP or a
1766 -- function call. See Note [Overview of implicit CallStacks]
1767 occOrigin (OccurrenceOf n)
1768 = Just (EvCsPushCall n locSpan)
1769 occOrigin (IPOccOrigin n)
1770 = Just (EvCsTop ('?' `consFS` hsIPNameFS n) locSpan)
1771 occOrigin _
1772 = Nothing
1773 locSpan
1774 = ctLocSpan loc
1775 isCallStackIP _ _ _
1776 = Nothing