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