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