2ccfcb1bb62ec14bbf4ff9ba559b4dbb5890d1c4
[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, isConstraintKind )
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_evar = 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 { updWorkListTcS (\wl -> foldrBag extendWorkListCt wl cts)
175 ; solve_loop }
176 where
177 solve_loop
178 = {-# SCC "solve_loop" #-}
179 do { sel <- selectNextWorkItem
180 ; case sel of
181 NoWorkRemaining -- Done, successfuly (modulo frozen)
182 -> return ()
183 MaxDepthExceeded ct -- Failure, depth exceeded
184 -> wrapErrTcS $ solverDepthErrorTcS (ctLoc ct) (ctPred ct)
185 NextWorkItem ct -- More work, loop around!
186 -> do { runSolverPipeline thePipeline ct
187 ; solve_loop } }
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 Ct
316 -- More work left to do but this constraint has exceeded
317 -- the maximum depth and we must stop
318 | NextWorkItem Ct -- More work left, here's the next item to look at
319
320 selectNextWorkItem :: TcS SelectWorkItem
321 selectNextWorkItem
322 = do { dflags <- getDynFlags
323 ; updWorkListTcS_return (pick_next dflags) }
324 where
325 pick_next :: DynFlags -> WorkList -> (SelectWorkItem, WorkList)
326 pick_next dflags wl
327 = case selectWorkItem wl of
328 (Nothing,_)
329 -> (NoWorkRemaining,wl) -- No more work
330 (Just ct, new_wl)
331 | subGoalDepthExceeded dflags (ctLocDepth (ctLoc ct))
332 -> (MaxDepthExceeded ct,new_wl) -- Depth exceeded
333
334 | otherwise
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 = isJust (lookupEvBind binds (ctEvId ev))
508
509 use_replacement
510 | isIPPred pred = lvl_w > lvl_i
511 | otherwise = lvl_w < lvl_i
512
513 {-
514 Note [Replacement vs keeping]
515 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
516 When we have two Given constraints both of type (C tys), say, which should
517 we keep?
518
519 * For implicit parameters we want to keep the innermost (deepest)
520 one, so that it overrides the outer one.
521 See Note [Shadowing of Implicit Parameters]
522
523 * For everything else, we want to keep the outermost one. Reason: that
524 makes it more likely that the inner one will turn out to be unused,
525 and can be reported as redundant. See Note [Tracking redundant constraints]
526 in TcSimplify.
527
528 It transpires that using the outermost one is reponsible for an
529 8% performance improvement in nofib cryptarithm2, compared to
530 just rolling the dice. I didn't investigate why.
531
532 * If there is no "outermost" one, we keep the one that has a non-trivial
533 evidence binding. Note [Tracking redundant constraints] again.
534 Example: f :: (Eq a, Ord a) => blah
535 then we may find [G] sc_sel (d1::Ord a) :: Eq a
536 [G] d2 :: Eq a
537 We want to discard d2 in favour of the superclass selection from
538 the Ord dictionary.
539
540 * Finally, when there is still a choice, use IRKeep rather than
541 IRReplace, to avoid unnecesary munging of the inert set.
542
543 Doing the depth-check for implicit parameters, rather than making the work item
544 always overrride, is important. Consider
545
546 data T a where { T1 :: (?x::Int) => T Int; T2 :: T a }
547
548 f :: (?x::a) => T a -> Int
549 f T1 = ?x
550 f T2 = 3
551
552 We have a [G] (?x::a) in the inert set, and at the pattern match on T1 we add
553 two new givens in the work-list: [G] (?x::Int)
554 [G] (a ~ Int)
555 Now consider these steps
556 - process a~Int, kicking out (?x::a)
557 - process (?x::Int), the inner given, adding to inert set
558 - process (?x::a), the outer given, overriding the inner given
559 Wrong! The depth-check ensures that the inner implicit parameter wins.
560 (Actually I think that the order in which the work-list is processed means
561 that this chain of events won't happen, but that's very fragile.)
562
563 *********************************************************************************
564 * *
565 interactIrred
566 * *
567 *********************************************************************************
568 -}
569
570 -- Two pieces of irreducible evidence: if their types are *exactly identical*
571 -- we can rewrite them. We can never improve using this:
572 -- if we want ty1 :: Constraint and have ty2 :: Constraint it clearly does not
573 -- mean that (ty1 ~ ty2)
574 interactIrred :: InertCans -> Ct -> TcS (StopOrContinue Ct)
575
576 interactIrred inerts workItem@(CIrredEvCan { cc_ev = ev_w })
577 | let pred = ctEvPred ev_w
578 (matching_irreds, others) = partitionBag (\ct -> ctPred ct `tcEqType` pred)
579 (inert_irreds inerts)
580 , (ct_i : rest) <- bagToList matching_irreds
581 , let ctev_i = ctEvidence ct_i
582 = ASSERT( null rest )
583 do { (inert_effect, stop_now) <- solveOneFromTheOther ctev_i ev_w
584 ; case inert_effect of
585 IRKeep -> return ()
586 IRDelete -> updInertIrreds (\_ -> others)
587 IRReplace -> updInertIrreds (\_ -> others `snocCts` workItem)
588 -- These const upd's assume that solveOneFromTheOther
589 -- has no side effects on InertCans
590 ; if stop_now then
591 return (Stop ev_w (ptext (sLit "Irred equal") <+> parens (ppr inert_effect)))
592 ; else
593 continueWith workItem }
594
595 | otherwise
596 = continueWith workItem
597
598 interactIrred _ wi = pprPanic "interactIrred" (ppr wi)
599
600 {-
601 *********************************************************************************
602 * *
603 interactDict
604 * *
605 *********************************************************************************
606 -}
607
608 interactDict :: InertCans -> Ct -> TcS (StopOrContinue Ct)
609 interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs = tys })
610 -- don't ever try to solve CallStack IPs directly from other dicts,
611 -- we always build new dicts instead.
612 -- See Note [Overview of implicit CallStacks]
613 | [_ip, ty] <- tys
614 , isWanted ev_w
615 , Just mkEvCs <- isCallStackIP (ctEvLoc ev_w) cls ty
616 = do let ev_cs =
617 case lookupInertDict inerts cls tys of
618 Just ev | isGiven ev -> mkEvCs (ctEvTerm ev)
619 _ -> mkEvCs (EvCallStack EvCsEmpty)
620
621 -- now we have ev_cs :: CallStack, but the evidence term should
622 -- be a dictionary, so we have to coerce ev_cs to a
623 -- dictionary for `IP ip CallStack`
624 let ip_ty = mkClassPred cls tys
625 let ev_tm = mkEvCast (EvCallStack ev_cs) (TcCoercion $ wrapIP ip_ty)
626 addSolvedDict ev_w cls tys
627 setWantedEvBind (ctEvId ev_w) ev_tm
628 stopWith ev_w "Wanted CallStack IP"
629
630 | Just ctev_i <- lookupInertDict inerts cls tys
631 = do { (inert_effect, stop_now) <- solveOneFromTheOther ctev_i ev_w
632 ; case inert_effect of
633 IRKeep -> return ()
634 IRDelete -> updInertDicts $ \ ds -> delDict ds cls tys
635 IRReplace -> updInertDicts $ \ ds -> addDict ds cls tys workItem
636 ; if stop_now then
637 return (Stop ev_w (ptext (sLit "Dict equal") <+> parens (ppr inert_effect)))
638 else
639 continueWith workItem }
640
641 | cls `hasKey` ipClassNameKey
642 , isGiven ev_w
643 = interactGivenIP inerts workItem
644
645 | otherwise
646 = do { mapBagM_ (addFunDepWork workItem)
647 (findDictsByClass (inert_dicts inerts) cls)
648 -- Create derived fds and keep on going.
649 -- No need to check flavour; fundeps work between
650 -- any pair of constraints, regardless of flavour
651 -- Importantly we don't throw workitem back in the
652 -- worklist bebcause this can cause loops (see #5236)
653 ; continueWith workItem }
654
655 interactDict _ wi = pprPanic "interactDict" (ppr wi)
656
657 interactGivenIP :: InertCans -> Ct -> TcS (StopOrContinue Ct)
658 -- Work item is Given (?x:ty)
659 -- See Note [Shadowing of Implicit Parameters]
660 interactGivenIP inerts workItem@(CDictCan { cc_ev = ev, cc_class = cls
661 , cc_tyargs = tys@(ip_str:_) })
662 = do { updInertCans $ \cans -> cans { inert_dicts = addDict filtered_dicts cls tys workItem }
663 ; stopWith ev "Given IP" }
664 where
665 dicts = inert_dicts inerts
666 ip_dicts = findDictsByClass dicts cls
667 other_ip_dicts = filterBag (not . is_this_ip) ip_dicts
668 filtered_dicts = addDictsByClass dicts cls other_ip_dicts
669
670 -- Pick out any Given constraints for the same implicit parameter
671 is_this_ip (CDictCan { cc_ev = ev, cc_tyargs = ip_str':_ })
672 = isGiven ev && ip_str `tcEqType` ip_str'
673 is_this_ip _ = False
674
675 interactGivenIP _ wi = pprPanic "interactGivenIP" (ppr wi)
676
677 addFunDepWork :: Ct -> Ct -> TcS ()
678 -- Add derived constraints from type-class functional dependencies.
679 addFunDepWork work_ct inert_ct
680 = emitFunDepDeriveds $
681 improveFromAnother derived_loc inert_pred work_pred
682 -- We don't really rewrite tys2, see below _rewritten_tys2, so that's ok
683 -- NB: We do create FDs for given to report insoluble equations that arise
684 -- from pairs of Givens, and also because of floating when we approximate
685 -- implications. The relevant test is: typecheck/should_fail/FDsFromGivens.hs
686 -- Also see Note [When improvement happens]
687 where
688 work_pred = ctPred work_ct
689 inert_pred = ctPred inert_ct
690 work_loc = ctLoc work_ct
691 inert_loc = ctLoc inert_ct
692 derived_loc = work_loc { ctl_origin = FunDepOrigin1 work_pred work_loc
693 inert_pred inert_loc }
694
695 {-
696 Note [Shadowing of Implicit Parameters]
697 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
698 Consider the following example:
699
700 f :: (?x :: Char) => Char
701 f = let ?x = 'a' in ?x
702
703 The "let ?x = ..." generates an implication constraint of the form:
704
705 ?x :: Char => ?x :: Char
706
707 Furthermore, the signature for `f` also generates an implication
708 constraint, so we end up with the following nested implication:
709
710 ?x :: Char => (?x :: Char => ?x :: Char)
711
712 Note that the wanted (?x :: Char) constraint may be solved in
713 two incompatible ways: either by using the parameter from the
714 signature, or by using the local definition. Our intention is
715 that the local definition should "shadow" the parameter of the
716 signature, and we implement this as follows: when we add a new
717 *given* implicit parameter to the inert set, it replaces any existing
718 givens for the same implicit parameter.
719
720 This works for the normal cases but it has an odd side effect
721 in some pathological programs like this:
722
723 -- This is accepted, the second parameter shadows
724 f1 :: (?x :: Int, ?x :: Char) => Char
725 f1 = ?x
726
727 -- This is rejected, the second parameter shadows
728 f2 :: (?x :: Int, ?x :: Char) => Int
729 f2 = ?x
730
731 Both of these are actually wrong: when we try to use either one,
732 we'll get two incompatible wnated constraints (?x :: Int, ?x :: Char),
733 which would lead to an error.
734
735 I can think of two ways to fix this:
736
737 1. Simply disallow multiple constratits for the same implicit
738 parameter---this is never useful, and it can be detected completely
739 syntactically.
740
741 2. Move the shadowing machinery to the location where we nest
742 implications, and add some code here that will produce an
743 error if we get multiple givens for the same implicit parameter.
744
745
746 *********************************************************************************
747 * *
748 interactFunEq
749 * *
750 *********************************************************************************
751 -}
752
753 interactFunEq :: InertCans -> Ct -> TcS (StopOrContinue Ct)
754 -- Try interacting the work item with the inert set
755 interactFunEq inerts workItem@(CFunEqCan { cc_ev = ev, cc_fun = tc
756 , cc_tyargs = args, cc_fsk = fsk })
757 | Just (CFunEqCan { cc_ev = ev_i, cc_fsk = fsk_i }) <- matching_inerts
758 = if ev_i `canRewriteOrSame` ev
759 then -- Rewrite work-item using inert
760 do { traceTcS "reactFunEq (discharge work item):" $
761 vcat [ text "workItem =" <+> ppr workItem
762 , text "inertItem=" <+> ppr ev_i ]
763 ; reactFunEq ev_i fsk_i ev fsk
764 ; stopWith ev "Inert rewrites work item" }
765 else -- Rewrite intert using work-item
766 do { traceTcS "reactFunEq (rewrite inert item):" $
767 vcat [ text "workItem =" <+> ppr workItem
768 , text "inertItem=" <+> ppr ev_i ]
769 ; updInertFunEqs $ \ feqs -> insertFunEq feqs tc args workItem
770 -- Do the updInertFunEqs before the reactFunEq, so that
771 -- we don't kick out the inertItem as well as consuming it!
772 ; reactFunEq ev fsk ev_i fsk_i
773 ; stopWith ev "Work item rewrites inert" }
774
775 | Just ops <- isBuiltInSynFamTyCon_maybe tc
776 = do { let matching_funeqs = findFunEqsByTyCon funeqs tc
777 ; let interact = sfInteractInert ops args (lookupFlattenTyVar eqs fsk)
778 do_one (CFunEqCan { cc_tyargs = iargs, cc_fsk = ifsk, cc_ev = iev })
779 = mapM_ (unifyDerived (ctEvLoc iev) Nominal)
780 (interact iargs (lookupFlattenTyVar eqs ifsk))
781 do_one ct = pprPanic "interactFunEq" (ppr ct)
782 ; mapM_ do_one matching_funeqs
783 ; traceTcS "builtInCandidates 1: " $ vcat [ ptext (sLit "Candidates:") <+> ppr matching_funeqs
784 , ptext (sLit "TvEqs:") <+> ppr eqs ]
785 ; return (ContinueWith workItem) }
786
787 | otherwise
788 = return (ContinueWith workItem)
789 where
790 eqs = inert_eqs inerts
791 funeqs = inert_funeqs inerts
792 matching_inerts = findFunEqs funeqs tc args
793
794 interactFunEq _ wi = pprPanic "interactFunEq" (ppr wi)
795
796 lookupFlattenTyVar :: TyVarEnv EqualCtList -> TcTyVar -> TcType
797 -- ^ Look up a flatten-tyvar in the inert nominal TyVarEqs;
798 -- this is used only when dealing with a CFunEqCan
799 lookupFlattenTyVar inert_eqs ftv
800 = case lookupVarEnv inert_eqs ftv of
801 Just (CTyEqCan { cc_rhs = rhs, cc_eq_rel = NomEq } : _) -> rhs
802 _ -> mkTyVarTy ftv
803
804 reactFunEq :: CtEvidence -> TcTyVar -- From this :: F tys ~ fsk1
805 -> CtEvidence -> TcTyVar -- Solve this :: F tys ~ fsk2
806 -> TcS ()
807 reactFunEq from_this fsk1 (CtGiven { ctev_evar = evar, ctev_loc = loc }) fsk2
808 = do { let fsk_eq_co = mkTcSymCo (mkTcCoVarCo evar)
809 `mkTcTransCo` ctEvCoercion from_this
810 -- :: fsk2 ~ fsk1
811 fsk_eq_pred = mkTcEqPred (mkTyVarTy fsk2) (mkTyVarTy fsk1)
812 ; new_ev <- newGivenEvVar loc (fsk_eq_pred, EvCoercion fsk_eq_co)
813 ; emitWorkNC [new_ev] }
814
815 reactFunEq from_this fuv1 (CtWanted { ctev_evar = evar }) fuv2
816 = dischargeFmv evar fuv2 (ctEvCoercion from_this) (mkTyVarTy fuv1)
817
818 reactFunEq _ _ solve_this@(CtDerived {}) _
819 = pprPanic "reactFunEq" (ppr solve_this)
820
821 {-
822 Note [Cache-caused loops]
823 ~~~~~~~~~~~~~~~~~~~~~~~~~
824 It is very dangerous to cache a rewritten wanted family equation as 'solved' in our
825 solved cache (which is the default behaviour or xCtEvidence), because the interaction
826 may not be contributing towards a solution. Here is an example:
827
828 Initial inert set:
829 [W] g1 : F a ~ beta1
830 Work item:
831 [W] g2 : F a ~ beta2
832 The work item will react with the inert yielding the _same_ inert set plus:
833 i) Will set g2 := g1 `cast` g3
834 ii) Will add to our solved cache that [S] g2 : F a ~ beta2
835 iii) Will emit [W] g3 : beta1 ~ beta2
836 Now, the g3 work item will be spontaneously solved to [G] g3 : beta1 ~ beta2
837 and then it will react the item in the inert ([W] g1 : F a ~ beta1). So it
838 will set
839 g1 := g ; sym g3
840 and what is g? Well it would ideally be a new goal of type (F a ~ beta2) but
841 remember that we have this in our solved cache, and it is ... g2! In short we
842 created the evidence loop:
843
844 g2 := g1 ; g3
845 g3 := refl
846 g1 := g2 ; sym g3
847
848 To avoid this situation we do not cache as solved any workitems (or inert)
849 which did not really made a 'step' towards proving some goal. Solved's are
850 just an optimization so we don't lose anything in terms of completeness of
851 solving.
852
853
854 Note [Efficient Orientation]
855 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
856 Suppose we are interacting two FunEqCans with the same LHS:
857 (inert) ci :: (F ty ~ xi_i)
858 (work) cw :: (F ty ~ xi_w)
859 We prefer to keep the inert (else we pass the work item on down
860 the pipeline, which is a bit silly). If we keep the inert, we
861 will (a) discharge 'cw'
862 (b) produce a new equality work-item (xi_w ~ xi_i)
863 Notice the orientation (xi_w ~ xi_i) NOT (xi_i ~ xi_w):
864 new_work :: xi_w ~ xi_i
865 cw := ci ; sym new_work
866 Why? Consider the simplest case when xi1 is a type variable. If
867 we generate xi1~xi2, porcessing that constraint will kick out 'ci'.
868 If we generate xi2~xi1, there is less chance of that happening.
869 Of course it can and should still happen if xi1=a, xi1=Int, say.
870 But we want to avoid it happening needlessly.
871
872 Similarly, if we *can't* keep the inert item (because inert is Wanted,
873 and work is Given, say), we prefer to orient the new equality (xi_i ~
874 xi_w).
875
876 Note [Carefully solve the right CFunEqCan]
877 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
878 ---- OLD COMMENT, NOW NOT NEEDED
879 ---- because we now allow multiple
880 ---- wanted FunEqs with the same head
881 Consider the constraints
882 c1 :: F Int ~ a -- Arising from an application line 5
883 c2 :: F Int ~ Bool -- Arising from an application line 10
884 Suppose that 'a' is a unification variable, arising only from
885 flattening. So there is no error on line 5; it's just a flattening
886 variable. But there is (or might be) an error on line 10.
887
888 Two ways to combine them, leaving either (Plan A)
889 c1 :: F Int ~ a -- Arising from an application line 5
890 c3 :: a ~ Bool -- Arising from an application line 10
891 or (Plan B)
892 c2 :: F Int ~ Bool -- Arising from an application line 10
893 c4 :: a ~ Bool -- Arising from an application line 5
894
895 Plan A will unify c3, leaving c1 :: F Int ~ Bool as an error
896 on the *totally innocent* line 5. An example is test SimpleFail16
897 where the expected/actual message comes out backwards if we use
898 the wrong plan.
899
900 The second is the right thing to do. Hence the isMetaTyVarTy
901 test when solving pairwise CFunEqCan.
902
903
904 *********************************************************************************
905 * *
906 interactTyVarEq
907 * *
908 *********************************************************************************
909 -}
910
911 interactTyVarEq :: InertCans -> Ct -> TcS (StopOrContinue Ct)
912 -- CTyEqCans are always consumed, so always returns Stop
913 interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv
914 , cc_rhs = rhs
915 , cc_ev = ev
916 , cc_eq_rel = eq_rel })
917 | (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i }
918 <- findTyEqs inerts tv
919 , ev_i `canRewriteOrSame` ev
920 , rhs_i `tcEqType` rhs ]
921 = -- Inert: a ~ b
922 -- Work item: a ~ b
923 do { setEvBindIfWanted ev (ctEvTerm ev_i)
924 ; stopWith ev "Solved from inert" }
925
926 | Just tv_rhs <- getTyVar_maybe rhs
927 , (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i }
928 <- findTyEqs inerts tv_rhs
929 , ev_i `canRewriteOrSame` ev
930 , rhs_i `tcEqType` mkTyVarTy tv ]
931 = -- Inert: a ~ b
932 -- Work item: b ~ a
933 do { setEvBindIfWanted ev
934 (EvCoercion (mkTcSymCo (ctEvCoercion ev_i)))
935 ; stopWith ev "Solved from inert (r)" }
936
937 | otherwise
938 = do { tclvl <- getTcLevel
939 ; if canSolveByUnification tclvl ev eq_rel tv rhs
940 then do { solveByUnification ev tv rhs
941 ; n_kicked <- kickOutRewritable Given NomEq tv
942 -- Given because the tv := xi is given
943 -- NomEq because only nom. equalities are solved
944 -- by unification
945 ; return (Stop ev (ptext (sLit "Spontaneously solved") <+> ppr_kicked n_kicked)) }
946
947 else do { traceTcS "Can't solve tyvar equality"
948 (vcat [ text "LHS:" <+> ppr tv <+> dcolon <+> ppr (tyVarKind tv)
949 , ppWhen (isMetaTyVar tv) $
950 nest 4 (text "TcLevel of" <+> ppr tv
951 <+> text "is" <+> ppr (metaTyVarTcLevel tv))
952 , text "RHS:" <+> ppr rhs <+> dcolon <+> ppr (typeKind rhs)
953 , text "TcLevel =" <+> ppr tclvl ])
954 ; n_kicked <- kickOutRewritable (ctEvFlavour ev)
955 (ctEvEqRel ev)
956 tv
957 ; updInertCans (\ ics -> addInertCan ics workItem)
958 ; return (Stop ev (ptext (sLit "Kept as inert") <+> ppr_kicked n_kicked)) } }
959
960 interactTyVarEq _ wi = pprPanic "interactTyVarEq" (ppr wi)
961
962 -- @trySpontaneousSolve wi@ solves equalities where one side is a
963 -- touchable unification variable.
964 -- Returns True <=> spontaneous solve happened
965 canSolveByUnification :: TcLevel -> CtEvidence -> EqRel
966 -> TcTyVar -> Xi -> Bool
967 canSolveByUnification tclvl gw eq_rel tv xi
968 | ReprEq <- eq_rel -- we never solve representational equalities this way.
969 = False
970
971 | isGiven gw -- See Note [Touchables and givens]
972 = False
973
974 | isTouchableMetaTyVar tclvl tv
975 = case metaTyVarInfo tv of
976 SigTv -> is_tyvar xi
977 _ -> True
978
979 | otherwise -- Untouchable
980 = False
981 where
982 is_tyvar xi
983 = case tcGetTyVar_maybe xi of
984 Nothing -> False
985 Just tv -> case tcTyVarDetails tv of
986 MetaTv { mtv_info = info }
987 -> case info of
988 SigTv -> True
989 _ -> False
990 SkolemTv {} -> True
991 FlatSkol {} -> False
992 RuntimeUnk -> True
993
994 solveByUnification :: CtEvidence -> TcTyVar -> Xi -> TcS ()
995 -- Solve with the identity coercion
996 -- Precondition: kind(xi) is a sub-kind of kind(tv)
997 -- Precondition: CtEvidence is Wanted or Derived
998 -- Precondition: CtEvidence is nominal
999 -- Returns: workItem where
1000 -- workItem = the new Given constraint
1001 --
1002 -- NB: No need for an occurs check here, because solveByUnification always
1003 -- arises from a CTyEqCan, a *canonical* constraint. Its invariants
1004 -- say that in (a ~ xi), the type variable a does not appear in xi.
1005 -- See TcRnTypes.Ct invariants.
1006 --
1007 -- Post: tv is unified (by side effect) with xi;
1008 -- we often write tv := xi
1009 solveByUnification wd tv xi
1010 = do { let tv_ty = mkTyVarTy tv
1011 ; traceTcS "Sneaky unification:" $
1012 vcat [text "Unifies:" <+> ppr tv <+> ptext (sLit ":=") <+> ppr xi,
1013 text "Coercion:" <+> pprEq tv_ty xi,
1014 text "Left Kind is:" <+> ppr (typeKind tv_ty),
1015 text "Right Kind is:" <+> ppr (typeKind xi) ]
1016
1017 ; let xi' = defaultKind xi
1018 -- We only instantiate kind unification variables
1019 -- with simple kinds like *, not OpenKind or ArgKind
1020 -- cf TcUnify.uUnboundKVar
1021
1022 ; setWantedTyBind tv xi'
1023 ; setEvBindIfWanted wd (EvCoercion (mkTcNomReflCo xi')) }
1024
1025
1026 ppr_kicked :: Int -> SDoc
1027 ppr_kicked 0 = empty
1028 ppr_kicked n = parens (int n <+> ptext (sLit "kicked out"))
1029
1030 kickOutRewritable :: CtFlavour -- Flavour of the equality that is
1031 -- being added to the inert set
1032 -> EqRel -- of the new equality
1033 -> TcTyVar -- The new equality is tv ~ ty
1034 -> TcS Int
1035 kickOutRewritable new_flavour new_eq_rel new_tv
1036 | not ((new_flavour, new_eq_rel) `eqCanRewriteFR` (new_flavour, new_eq_rel))
1037 = return 0 -- If new_flavour can't rewrite itself, it can't rewrite
1038 -- anything else, so no need to kick out anything
1039 -- This is a common case: wanteds can't rewrite wanteds
1040
1041 | otherwise
1042 = do { ics <- getInertCans
1043 ; let (kicked_out, ics') = kick_out new_flavour new_eq_rel new_tv ics
1044 ; setInertCans ics'
1045 ; updWorkListTcS (appendWorkList kicked_out)
1046
1047 ; unless (isEmptyWorkList kicked_out) $
1048 csTraceTcS $
1049 hang (ptext (sLit "Kick out, tv =") <+> ppr new_tv)
1050 2 (vcat [ text "n-kicked =" <+> int (workListSize kicked_out)
1051 , text "n-kept fun-eqs =" <+> int (sizeFunEqMap (inert_funeqs ics'))
1052 , ppr kicked_out ])
1053 ; return (workListSize kicked_out) }
1054
1055 kick_out :: CtFlavour -> EqRel -> TcTyVar -> InertCans -> (WorkList, InertCans)
1056 kick_out new_flavour new_eq_rel new_tv (IC { inert_eqs = tv_eqs
1057 , inert_dicts = dictmap
1058 , inert_funeqs = funeqmap
1059 , inert_irreds = irreds
1060 , inert_insols = insols })
1061 = (kicked_out, inert_cans_in)
1062 where
1063 -- NB: Notice that don't rewrite
1064 -- inert_solved_dicts, and inert_solved_funeqs
1065 -- optimistically. But when we lookup we have to
1066 -- take the substitution into account
1067 inert_cans_in = IC { inert_eqs = tv_eqs_in
1068 , inert_dicts = dicts_in
1069 , inert_funeqs = feqs_in
1070 , inert_irreds = irs_in
1071 , inert_insols = insols_in }
1072
1073 kicked_out = WL { wl_eqs = tv_eqs_out
1074 , wl_funeqs = feqs_out
1075 , wl_rest = bagToList (dicts_out `andCts` irs_out
1076 `andCts` insols_out)
1077 , wl_implics = emptyBag }
1078
1079 (tv_eqs_out, tv_eqs_in) = foldVarEnv kick_out_eqs ([], emptyVarEnv) tv_eqs
1080 (feqs_out, feqs_in) = partitionFunEqs kick_out_ct funeqmap
1081 (dicts_out, dicts_in) = partitionDicts kick_out_ct dictmap
1082 (irs_out, irs_in) = partitionBag kick_out_irred irreds
1083 (insols_out, insols_in) = partitionBag kick_out_ct insols
1084 -- Kick out even insolubles; see Note [Kick out insolubles]
1085
1086 can_rewrite :: CtEvidence -> Bool
1087 can_rewrite = ((new_flavour, new_eq_rel) `eqCanRewriteFR`) . ctEvFlavourRole
1088
1089 kick_out_ct :: Ct -> Bool
1090 kick_out_ct ct = kick_out_ctev (ctEvidence ct)
1091
1092 kick_out_ctev :: CtEvidence -> Bool
1093 kick_out_ctev ev = can_rewrite ev
1094 && new_tv `elemVarSet` tyVarsOfType (ctEvPred ev)
1095 -- See Note [Kicking out inert constraints]
1096
1097 kick_out_irred :: Ct -> Bool
1098 kick_out_irred ct = can_rewrite (cc_ev ct)
1099 && new_tv `elemVarSet` closeOverKinds (tyVarsOfCt ct)
1100 -- See Note [Kicking out Irreds]
1101
1102 kick_out_eqs :: EqualCtList -> ([Ct], TyVarEnv EqualCtList)
1103 -> ([Ct], TyVarEnv EqualCtList)
1104 kick_out_eqs eqs (acc_out, acc_in)
1105 = (eqs_out ++ acc_out, case eqs_in of
1106 [] -> acc_in
1107 (eq1:_) -> extendVarEnv acc_in (cc_tyvar eq1) eqs_in)
1108 where
1109 (eqs_in, eqs_out) = partition keep_eq eqs
1110
1111 -- implements criteria K1-K3 in Note [The inert equalities] in TcFlatten
1112 keep_eq (CTyEqCan { cc_tyvar = tv, cc_rhs = rhs_ty, cc_ev = ev
1113 , cc_eq_rel = eq_rel })
1114 | tv == new_tv
1115 = not (can_rewrite ev) -- (K1)
1116
1117 | otherwise
1118 = check_k2 && check_k3
1119 where
1120 check_k2 = not (ev `eqCanRewrite` ev)
1121 || not (can_rewrite ev)
1122 || not (new_tv `elemVarSet` tyVarsOfType rhs_ty)
1123
1124 check_k3
1125 | can_rewrite ev
1126 = case eq_rel of
1127 NomEq -> not (rhs_ty `eqType` mkTyVarTy new_tv)
1128 ReprEq -> not (isTyVarExposed new_tv rhs_ty)
1129
1130 | otherwise
1131 = True
1132
1133 keep_eq ct = pprPanic "keep_eq" (ppr ct)
1134
1135 {-
1136 Note [Kicking out inert constraints]
1137 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1138 Given a new (a -> ty) inert, we want to kick out an existing inert
1139 constraint if
1140 a) the new constraint can rewrite the inert one
1141 b) 'a' is free in the inert constraint (so that it *will*)
1142 rewrite it if we kick it out.
1143
1144 For (b) we use tyVarsOfCt, which returns the type variables /and
1145 the kind variables/ that are directly visible in the type. Hence we
1146 will have exposed all the rewriting we care about to make the most
1147 precise kinds visible for matching classes etc. No need to kick out
1148 constraints that mention type variables whose kinds contain this
1149 variable! (Except see Note [Kicking out Irreds].)
1150
1151 Note [Kicking out Irreds]
1152 ~~~~~~~~~~~~~~~~~~~~~~~~~
1153 There is an awkward special case for Irreds. When we have a
1154 kind-mis-matched equality constraint (a:k1) ~ (ty:k2), we turn it into
1155 an Irred (see Note [Equalities with incompatible kinds] in
1156 TcCanonical). So in this case the free kind variables of k1 and k2
1157 are not visible. More precisely, the type looks like
1158 (~) k1 (a:k1) (ty:k2)
1159 because (~) has kind forall k. k -> k -> Constraint. So the constraint
1160 itself is ill-kinded. We can "see" k1 but not k2. That's why we use
1161 closeOverKinds to make sure we see k2.
1162
1163 This is not pretty. Maybe (~) should have kind
1164 (~) :: forall k1 k1. k1 -> k2 -> Constraint
1165
1166 Note [Kick out insolubles]
1167 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1168 Suppose we have an insoluble alpha ~ [alpha], which is insoluble
1169 because an occurs check. And then we unify alpha := [Int].
1170 Then we really want to rewrite the insouluble to [Int] ~ [[Int]].
1171 Now it can be decomposed. Otherwise we end up with a "Can't match
1172 [Int] ~ [[Int]]" which is true, but a bit confusing because the
1173 outer type constructors match.
1174
1175
1176 Note [Avoid double unifications]
1177 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1178 The spontaneous solver has to return a given which mentions the unified unification
1179 variable *on the left* of the equality. Here is what happens if not:
1180 Original wanted: (a ~ alpha), (alpha ~ Int)
1181 We spontaneously solve the first wanted, without changing the order!
1182 given : a ~ alpha [having unified alpha := a]
1183 Now the second wanted comes along, but he cannot rewrite the given, so we simply continue.
1184 At the end we spontaneously solve that guy, *reunifying* [alpha := Int]
1185
1186 We avoid this problem by orienting the resulting given so that the unification
1187 variable is on the left. [Note that alternatively we could attempt to
1188 enforce this at canonicalization]
1189
1190 See also Note [No touchables as FunEq RHS] in TcSMonad; avoiding
1191 double unifications is the main reason we disallow touchable
1192 unification variables as RHS of type family equations: F xis ~ alpha.
1193
1194
1195 ************************************************************************
1196 * *
1197 * Functional dependencies, instantiation of equations
1198 * *
1199 ************************************************************************
1200
1201 When we spot an equality arising from a functional dependency,
1202 we now use that equality (a "wanted") to rewrite the work-item
1203 constraint right away. This avoids two dangers
1204
1205 Danger 1: If we send the original constraint on down the pipeline
1206 it may react with an instance declaration, and in delicate
1207 situations (when a Given overlaps with an instance) that
1208 may produce new insoluble goals: see Trac #4952
1209
1210 Danger 2: If we don't rewrite the constraint, it may re-react
1211 with the same thing later, and produce the same equality
1212 again --> termination worries.
1213
1214 To achieve this required some refactoring of FunDeps.hs (nicer
1215 now!).
1216 -}
1217
1218 emitFunDepDeriveds :: [FunDepEqn CtLoc] -> TcS ()
1219 emitFunDepDeriveds fd_eqns
1220 = mapM_ do_one_FDEqn fd_eqns
1221 where
1222 do_one_FDEqn (FDEqn { fd_qtvs = tvs, fd_eqs = eqs, fd_loc = loc })
1223 | null tvs -- Common shortcut
1224 = mapM_ (unifyDerived loc Nominal) eqs
1225 | otherwise
1226 = do { (subst, _) <- instFlexiTcS tvs -- Takes account of kind substitution
1227 ; mapM_ (do_one_eq loc subst) eqs }
1228
1229 do_one_eq loc subst (Pair ty1 ty2)
1230 = unifyDerived loc Nominal $
1231 Pair (Type.substTy subst ty1) (Type.substTy subst ty2)
1232
1233 {-
1234 *********************************************************************************
1235 * *
1236 The top-reaction Stage
1237 * *
1238 *********************************************************************************
1239 -}
1240
1241 topReactionsStage :: WorkItem -> TcS (StopOrContinue Ct)
1242 topReactionsStage wi
1243 = do { inerts <- getTcSInerts
1244 ; tir <- doTopReact inerts wi
1245 ; case tir of
1246 ContinueWith wi -> return (ContinueWith wi)
1247 Stop ev s -> return (Stop ev (ptext (sLit "Top react:") <+> s)) }
1248
1249 doTopReact :: InertSet -> WorkItem -> TcS (StopOrContinue Ct)
1250 -- The work item does not react with the inert set, so try interaction with top-level
1251 -- instances. Note:
1252 --
1253 -- (a) The place to add superclasses in not here in doTopReact stage.
1254 -- Instead superclasses are added in the worklist as part of the
1255 -- canonicalization process. See Note [Adding superclasses].
1256
1257 doTopReact inerts work_item
1258 = do { traceTcS "doTopReact" (ppr work_item)
1259 ; case work_item of
1260 CDictCan {} -> doTopReactDict inerts work_item
1261 CFunEqCan {} -> doTopReactFunEq work_item
1262 _ -> -- Any other work item does not react with any top-level equations
1263 return (ContinueWith work_item) }
1264
1265 --------------------
1266 doTopReactDict :: InertSet -> Ct -> TcS (StopOrContinue Ct)
1267 -- Try to use type-class instance declarations to simplify the constraint
1268 doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls
1269 , cc_tyargs = xis })
1270 | not (isWanted fl) -- Never use instances for Given or Derived constraints
1271 = try_fundeps_and_return
1272
1273 | Just ev <- lookupSolvedDict inerts cls xis -- Cached
1274 = do { setWantedEvBind dict_id (ctEvTerm ev);
1275 ; stopWith fl "Dict/Top (cached)" }
1276
1277 | otherwise -- Not cached
1278 = do { lkup_inst_res <- matchClassInst inerts cls xis dict_loc
1279 ; case lkup_inst_res of
1280 GenInst wtvs ev_term -> do { addSolvedDict fl cls xis
1281 ; solve_from_instance wtvs ev_term }
1282 NoInstance -> try_fundeps_and_return }
1283 where
1284 dict_id = ASSERT( isWanted fl ) ctEvId fl
1285 dict_pred = mkClassPred cls xis
1286 dict_loc = ctEvLoc fl
1287 dict_origin = ctLocOrigin dict_loc
1288 deeper_loc = bumpCtLocDepth dict_loc
1289
1290 solve_from_instance :: [CtEvidence] -> EvTerm -> TcS (StopOrContinue Ct)
1291 -- Precondition: evidence term matches the predicate workItem
1292 solve_from_instance evs ev_term
1293 | null evs
1294 = do { traceTcS "doTopReact/found nullary instance for" $
1295 ppr dict_id
1296 ; setWantedEvBind dict_id ev_term
1297 ; stopWith fl "Dict/Top (solved, no new work)" }
1298 | otherwise
1299 = do { checkReductionDepth deeper_loc dict_pred
1300 ; traceTcS "doTopReact/found non-nullary instance for" $
1301 ppr dict_id
1302 ; setWantedEvBind dict_id ev_term
1303 ; let mk_new_wanted ev
1304 = mkNonCanonical (ev {ctev_loc = deeper_loc })
1305 ; updWorkListTcS (extendWorkListCts (map mk_new_wanted evs))
1306 ; stopWith fl "Dict/Top (solved, more work)" }
1307
1308 -- We didn't solve it; so try functional dependencies with
1309 -- the instance environment, and return
1310 -- NB: even if there *are* some functional dependencies against the
1311 -- instance environment, there might be a unique match, and if
1312 -- so we make sure we get on and solve it first. See Note [Weird fundeps]
1313 try_fundeps_and_return
1314 = do { instEnvs <- getInstEnvs
1315 ; emitFunDepDeriveds $
1316 improveFromInstEnv instEnvs mk_ct_loc dict_pred
1317 ; continueWith work_item }
1318
1319 mk_ct_loc :: PredType -- From instance decl
1320 -> SrcSpan -- also from instance deol
1321 -> CtLoc
1322 mk_ct_loc inst_pred inst_loc
1323 = dict_loc { ctl_origin = FunDepOrigin2 dict_pred dict_origin
1324 inst_pred inst_loc }
1325
1326 doTopReactDict _ w = pprPanic "doTopReactDict" (ppr w)
1327
1328 --------------------
1329 doTopReactFunEq :: Ct -> TcS (StopOrContinue Ct)
1330 -- Note [Short cut for top-level reaction]
1331 doTopReactFunEq work_item@(CFunEqCan { cc_ev = old_ev, cc_fun = fam_tc
1332 , cc_tyargs = args , cc_fsk = fsk })
1333 = ASSERT(isTypeFamilyTyCon fam_tc) -- No associated data families
1334 -- have reached this far
1335 ASSERT( not (isDerived old_ev) ) -- CFunEqCan is never Derived
1336 -- Look up in top-level instances, or built-in axiom
1337 do { match_res <- matchFam fam_tc args -- See Note [MATCHING-SYNONYMS]
1338 ; case match_res of {
1339 Nothing -> do { try_improvement; continueWith work_item } ;
1340 Just (ax_co, rhs_ty)
1341
1342 -- Found a top-level instance
1343
1344 | Just (tc, tc_args) <- tcSplitTyConApp_maybe rhs_ty
1345 , isTypeFamilyTyCon tc
1346 , tc_args `lengthIs` tyConArity tc -- Short-cut
1347 -> shortCutReduction old_ev fsk ax_co tc tc_args
1348 -- Try shortcut; see Note [Short cut for top-level reaction]
1349
1350 | isGiven old_ev -- Not shortcut
1351 -> do { let final_co = mkTcSymCo (ctEvCoercion old_ev) `mkTcTransCo` ax_co
1352 -- final_co :: fsk ~ rhs_ty
1353 ; new_ev <- newGivenEvVar deeper_loc (mkTcEqPred (mkTyVarTy fsk) rhs_ty,
1354 EvCoercion final_co)
1355 ; emitWorkNC [new_ev] -- Non-cannonical; that will mean we flatten rhs_ty
1356 ; stopWith old_ev "Fun/Top (given)" }
1357
1358 | not (fsk `elemVarSet` tyVarsOfType rhs_ty)
1359 -> do { dischargeFmv (ctEvId old_ev) fsk ax_co rhs_ty
1360 ; traceTcS "doTopReactFunEq" $
1361 vcat [ text "old_ev:" <+> ppr old_ev
1362 , nest 2 (text ":=") <+> ppr ax_co ]
1363 ; stopWith old_ev "Fun/Top (wanted)" }
1364
1365 | otherwise -- We must not assign ufsk := ...ufsk...!
1366 -> do { alpha_ty <- newFlexiTcSTy (tyVarKind fsk)
1367 ; new_ev <- newWantedEvVarNC loc (mkTcEqPred alpha_ty rhs_ty)
1368 ; emitWorkNC [new_ev]
1369 -- By emitting this as non-canonical, we deal with all
1370 -- flattening, occurs-check, and ufsk := ufsk issues
1371 ; let final_co = ax_co `mkTcTransCo` mkTcSymCo (ctEvCoercion new_ev)
1372 -- ax_co :: fam_tc args ~ rhs_ty
1373 -- new_ev :: alpha ~ rhs_ty
1374 -- ufsk := alpha
1375 -- final_co :: fam_tc args ~ alpha
1376 ; dischargeFmv (ctEvId old_ev) fsk final_co alpha_ty
1377 ; traceTcS "doTopReactFunEq (occurs)" $
1378 vcat [ text "old_ev:" <+> ppr old_ev
1379 , nest 2 (text ":=") <+> ppr final_co
1380 , text "new_ev:" <+> ppr new_ev ]
1381 ; stopWith old_ev "Fun/Top (wanted)" } } }
1382 where
1383 loc = ctEvLoc old_ev
1384 deeper_loc = bumpCtLocDepth loc
1385
1386 try_improvement
1387 | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc
1388 = do { inert_eqs <- getInertEqs
1389 ; let eqns = sfInteractTop ops args (lookupFlattenTyVar inert_eqs fsk)
1390 ; mapM_ (unifyDerived loc Nominal) eqns }
1391 | otherwise
1392 = return ()
1393
1394 doTopReactFunEq w = pprPanic "doTopReactFunEq" (ppr w)
1395
1396 shortCutReduction :: CtEvidence -> TcTyVar -> TcCoercion
1397 -> TyCon -> [TcType] -> TcS (StopOrContinue Ct)
1398 -- See Note [Top-level reductions for type functions]
1399 shortCutReduction old_ev fsk ax_co fam_tc tc_args
1400 | isGiven old_ev
1401 = ASSERT( ctEvEqRel old_ev == NomEq )
1402 do { (xis, cos) <- flattenManyNom old_ev tc_args
1403 -- ax_co :: F args ~ G tc_args
1404 -- cos :: xis ~ tc_args
1405 -- old_ev :: F args ~ fsk
1406 -- G cos ; sym ax_co ; old_ev :: G xis ~ fsk
1407
1408 ; new_ev <- newGivenEvVar deeper_loc
1409 ( mkTcEqPred (mkTyConApp fam_tc xis) (mkTyVarTy fsk)
1410 , EvCoercion (mkTcTyConAppCo Nominal fam_tc cos
1411 `mkTcTransCo` mkTcSymCo ax_co
1412 `mkTcTransCo` ctEvCoercion old_ev) )
1413
1414 ; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc, cc_tyargs = xis, cc_fsk = fsk }
1415 ; emitWorkCt new_ct
1416 ; stopWith old_ev "Fun/Top (given, shortcut)" }
1417
1418 | otherwise
1419 = ASSERT( not (isDerived old_ev) ) -- Caller ensures this
1420 ASSERT( ctEvEqRel old_ev == NomEq )
1421 do { (xis, cos) <- flattenManyNom old_ev tc_args
1422 -- ax_co :: F args ~ G tc_args
1423 -- cos :: xis ~ tc_args
1424 -- G cos ; sym ax_co ; old_ev :: G xis ~ fsk
1425 -- new_ev :: G xis ~ fsk
1426 -- old_ev :: F args ~ fsk := ax_co ; sym (G cos) ; new_ev
1427
1428 ; new_ev <- newWantedEvVarNC deeper_loc
1429 (mkTcEqPred (mkTyConApp fam_tc xis) (mkTyVarTy fsk))
1430 ; setWantedEvBind (ctEvId old_ev)
1431 (EvCoercion (ax_co `mkTcTransCo` mkTcSymCo (mkTcTyConAppCo Nominal fam_tc cos)
1432 `mkTcTransCo` ctEvCoercion new_ev))
1433
1434 ; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc, cc_tyargs = xis, cc_fsk = fsk }
1435 ; emitWorkCt new_ct
1436 ; stopWith old_ev "Fun/Top (wanted, shortcut)" }
1437 where
1438 loc = ctEvLoc old_ev
1439 deeper_loc = bumpCtLocDepth loc
1440
1441 dischargeFmv :: EvVar -> TcTyVar -> TcCoercion -> TcType -> TcS ()
1442 -- (dischargeFmv x fmv co ty)
1443 -- [W] x :: F tys ~ fuv
1444 -- co :: F tys ~ ty
1445 -- Precondition: fuv is not filled, and fuv `notElem` ty
1446 --
1447 -- Then set fuv := ty,
1448 -- set x := co
1449 -- kick out any inert things that are now rewritable
1450 dischargeFmv evar fmv co xi
1451 = ASSERT2( not (fmv `elemVarSet` tyVarsOfType xi), ppr evar $$ ppr fmv $$ ppr xi )
1452 do { setWantedTyBind fmv xi
1453 ; setWantedEvBind evar (EvCoercion co)
1454 ; n_kicked <- kickOutRewritable Given NomEq fmv
1455 ; traceTcS "dischargeFuv" (ppr fmv <+> equals <+> ppr xi $$ ppr_kicked n_kicked) }
1456
1457 {- Note [Top-level reductions for type functions]
1458 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1459 c.f. Note [The flattening story] in TcFlatten
1460
1461 Suppose we have a CFunEqCan F tys ~ fmv/fsk, and a matching axiom.
1462 Here is what we do, in four cases:
1463
1464 * Wanteds: general firing rule
1465 (work item) [W] x : F tys ~ fmv
1466 instantiate axiom: ax_co : F tys ~ rhs
1467
1468 Then:
1469 Discharge fmv := alpha
1470 Discharge x := ax_co ; sym x2
1471 New wanted [W] x2 : alpha ~ rhs (Non-canonical)
1472 This is *the* way that fmv's get unified; even though they are
1473 "untouchable".
1474
1475 NB: it can be the case that fmv appears in the (instantiated) rhs.
1476 In that case the new Non-canonical wanted will be loopy, but that's
1477 ok. But it's good reason NOT to claim that it is canonical!
1478
1479 * Wanteds: short cut firing rule
1480 Applies when the RHS of the axiom is another type-function application
1481 (work item) [W] x : F tys ~ fmv
1482 instantiate axiom: ax_co : F tys ~ G rhs_tys
1483
1484 It would be a waste to create yet another fmv for (G rhs_tys).
1485 Instead (shortCutReduction):
1486 - Flatten rhs_tys (cos : rhs_tys ~ rhs_xis)
1487 - Add G rhs_xis ~ fmv to flat cache (note: the same old fmv)
1488 - New canonical wanted [W] x2 : G rhs_xis ~ fmv (CFunEqCan)
1489 - Discharge x := ax_co ; G cos ; x2
1490
1491 * Givens: general firing rule
1492 (work item) [G] g : F tys ~ fsk
1493 instantiate axiom: ax_co : F tys ~ rhs
1494
1495 Now add non-canonical given (since rhs is not flat)
1496 [G] (sym g ; ax_co) : fsk ~ rhs (Non-canonical)
1497
1498 * Givens: short cut firing rule
1499 Applies when the RHS of the axiom is another type-function application
1500 (work item) [G] g : F tys ~ fsk
1501 instantiate axiom: ax_co : F tys ~ G rhs_tys
1502
1503 It would be a waste to create yet another fsk for (G rhs_tys).
1504 Instead (shortCutReduction):
1505 - Flatten rhs_tys: flat_cos : tys ~ flat_tys
1506 - Add new Canonical given
1507 [G] (sym (G flat_cos) ; co ; g) : G flat_tys ~ fsk (CFunEqCan)
1508
1509 Note [Cached solved FunEqs]
1510 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1511 When trying to solve, say (FunExpensive big-type ~ ty), it's important
1512 to see if we have reduced (FunExpensive big-type) before, lest we
1513 simply repeat it. Hence the lookup in inert_solved_funeqs. Moreover
1514 we must use `canRewriteOrSame` because both uses might (say) be Wanteds,
1515 and we *still* want to save the re-computation.
1516
1517 Note [MATCHING-SYNONYMS]
1518 ~~~~~~~~~~~~~~~~~~~~~~~~
1519 When trying to match a dictionary (D tau) to a top-level instance, or a
1520 type family equation (F taus_1 ~ tau_2) to a top-level family instance,
1521 we do *not* need to expand type synonyms because the matcher will do that for us.
1522
1523
1524 Note [RHS-FAMILY-SYNONYMS]
1525 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1526 The RHS of a family instance is represented as yet another constructor which is
1527 like a type synonym for the real RHS the programmer declared. Eg:
1528 type instance F (a,a) = [a]
1529 Becomes:
1530 :R32 a = [a] -- internal type synonym introduced
1531 F (a,a) ~ :R32 a -- instance
1532
1533 When we react a family instance with a type family equation in the work list
1534 we keep the synonym-using RHS without expansion.
1535
1536 Note [FunDep and implicit parameter reactions]
1537 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1538 Currently, our story of interacting two dictionaries (or a dictionary
1539 and top-level instances) for functional dependencies, and implicit
1540 paramters, is that we simply produce new Derived equalities. So for example
1541
1542 class D a b | a -> b where ...
1543 Inert:
1544 d1 :g D Int Bool
1545 WorkItem:
1546 d2 :w D Int alpha
1547
1548 We generate the extra work item
1549 cv :d alpha ~ Bool
1550 where 'cv' is currently unused. However, this new item can perhaps be
1551 spontaneously solved to become given and react with d2,
1552 discharging it in favour of a new constraint d2' thus:
1553 d2' :w D Int Bool
1554 d2 := d2' |> D Int cv
1555 Now d2' can be discharged from d1
1556
1557 We could be more aggressive and try to *immediately* solve the dictionary
1558 using those extra equalities, but that requires those equalities to carry
1559 evidence and derived do not carry evidence.
1560
1561 If that were the case with the same inert set and work item we might dischard
1562 d2 directly:
1563
1564 cv :w alpha ~ Bool
1565 d2 := d1 |> D Int cv
1566
1567 But in general it's a bit painful to figure out the necessary coercion,
1568 so we just take the first approach. Here is a better example. Consider:
1569 class C a b c | a -> b
1570 And:
1571 [Given] d1 : C T Int Char
1572 [Wanted] d2 : C T beta Int
1573 In this case, it's *not even possible* to solve the wanted immediately.
1574 So we should simply output the functional dependency and add this guy
1575 [but NOT its superclasses] back in the worklist. Even worse:
1576 [Given] d1 : C T Int beta
1577 [Wanted] d2: C T beta Int
1578 Then it is solvable, but its very hard to detect this on the spot.
1579
1580 It's exactly the same with implicit parameters, except that the
1581 "aggressive" approach would be much easier to implement.
1582
1583 Note [When improvement happens]
1584 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1585 We fire an improvement rule when
1586
1587 * Two constraints match (modulo the fundep)
1588 e.g. C t1 t2, C t1 t3 where C a b | a->b
1589 The two match because the first arg is identical
1590
1591 Note that we *do* fire the improvement if one is Given and one is Derived (e.g. a
1592 superclass of a Wanted goal) or if both are Given.
1593
1594 Example (tcfail138)
1595 class L a b | a -> b
1596 class (G a, L a b) => C a b
1597
1598 instance C a b' => G (Maybe a)
1599 instance C a b => C (Maybe a) a
1600 instance L (Maybe a) a
1601
1602 When solving the superclasses of the (C (Maybe a) a) instance, we get
1603 Given: C a b ... and hance by superclasses, (G a, L a b)
1604 Wanted: G (Maybe a)
1605 Use the instance decl to get
1606 Wanted: C a b'
1607 The (C a b') is inert, so we generate its Derived superclasses (L a b'),
1608 and now we need improvement between that derived superclass an the Given (L a b)
1609
1610 Test typecheck/should_fail/FDsFromGivens also shows why it's a good idea to
1611 emit Derived FDs for givens as well.
1612
1613 Note [Weird fundeps]
1614 ~~~~~~~~~~~~~~~~~~~~
1615 Consider class Het a b | a -> b where
1616 het :: m (f c) -> a -> m b
1617
1618 class GHet (a :: * -> *) (b :: * -> *) | a -> b
1619 instance GHet (K a) (K [a])
1620 instance Het a b => GHet (K a) (K b)
1621
1622 The two instances don't actually conflict on their fundeps,
1623 although it's pretty strange. So they are both accepted. Now
1624 try [W] GHet (K Int) (K Bool)
1625 This triggers fudeps from both instance decls; but it also
1626 matches a *unique* instance decl, and we should go ahead and
1627 pick that one right now. Otherwise, if we don't, it ends up
1628 unsolved in the inert set and is reported as an error.
1629
1630 Trac #7875 is a case in point.
1631
1632 Note [Overriding implicit parameters]
1633 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1634 Consider
1635 f :: (?x::a) -> Bool -> a
1636
1637 g v = let ?x::Int = 3
1638 in (f v, let ?x::Bool = True in f v)
1639
1640 This should probably be well typed, with
1641 g :: Bool -> (Int, Bool)
1642
1643 So the inner binding for ?x::Bool *overrides* the outer one.
1644 Hence a work-item Given overrides an inert-item Given.
1645 -}
1646
1647 data LookupInstResult
1648 = NoInstance
1649 | GenInst [CtEvidence] EvTerm
1650
1651 instance Outputable LookupInstResult where
1652 ppr NoInstance = text "NoInstance"
1653 ppr (GenInst ev t) = text "GenInst" <+> ppr ev <+> ppr t
1654
1655
1656 matchClassInst :: InertSet -> Class -> [Type] -> CtLoc -> TcS LookupInstResult
1657
1658 matchClassInst _ clas [ ty ] _
1659 | className clas == knownNatClassName
1660 , Just n <- isNumLitTy ty = makeDict (EvNum n)
1661
1662 | className clas == knownSymbolClassName
1663 , Just s <- isStrLitTy ty = makeDict (EvStr s)
1664
1665 where
1666 {- This adds a coercion that will convert the literal into a dictionary
1667 of the appropriate type. See Note [KnownNat & KnownSymbol and EvLit]
1668 in TcEvidence. The coercion happens in 2 steps:
1669
1670 Integer -> SNat n -- representation of literal to singleton
1671 SNat n -> KnownNat n -- singleton to dictionary
1672
1673 The process is mirrored for Symbols:
1674 String -> SSymbol n
1675 SSymbol n -> KnownSymbol n
1676 -}
1677 makeDict evLit
1678 | Just (_, co_dict) <- tcInstNewTyCon_maybe (classTyCon clas) [ty]
1679 -- co_dict :: KnownNat n ~ SNat n
1680 , [ meth ] <- classMethods clas
1681 , Just tcRep <- tyConAppTyCon_maybe -- SNat
1682 $ funResultTy -- SNat n
1683 $ dropForAlls -- KnownNat n => SNat n
1684 $ idType meth -- forall n. KnownNat n => SNat n
1685 , Just (_, co_rep) <- tcInstNewTyCon_maybe tcRep [ty]
1686 -- SNat n ~ Integer
1687 = return (GenInst [] $ mkEvCast (EvLit evLit) (mkTcSymCo (mkTcTransCo co_dict co_rep)))
1688
1689 | otherwise
1690 = panicTcS (text "Unexpected evidence for" <+> ppr (className clas)
1691 $$ vcat (map (ppr . idType) (classMethods clas)))
1692
1693 matchClassInst _ clas [k,t] loc
1694 | className clas == typeableClassName = matchTypeableClass clas k t loc
1695
1696 matchClassInst inerts clas tys loc
1697 = do { dflags <- getDynFlags
1698 ; traceTcS "matchClassInst" $ vcat [ text "pred =" <+> ppr pred
1699 , text "inerts=" <+> ppr inerts ]
1700 ; instEnvs <- getInstEnvs
1701 ; case lookupInstEnv instEnvs clas tys of
1702 ([], _, _) -- Nothing matches
1703 -> do { traceTcS "matchClass not matching" $
1704 vcat [ text "dict" <+> ppr pred ]
1705 ; return NoInstance }
1706
1707 ([(ispec, inst_tys)], [], _) -- A single match
1708 | not (xopt Opt_IncoherentInstances dflags)
1709 , not (isEmptyBag unifiable_givens)
1710 -> -- See Note [Instance and Given overlap]
1711 do { traceTcS "Delaying instance application" $
1712 vcat [ text "Work item=" <+> pprType (mkClassPred clas tys)
1713 , text "Relevant given dictionaries=" <+> ppr unifiable_givens ]
1714 ; return NoInstance }
1715
1716 | otherwise
1717 -> do { let dfun_id = instanceDFunId ispec
1718 ; traceTcS "matchClass success" $
1719 vcat [text "dict" <+> ppr pred,
1720 text "witness" <+> ppr dfun_id
1721 <+> ppr (idType dfun_id) ]
1722 -- Record that this dfun is needed
1723 ; match_one dfun_id inst_tys }
1724
1725 (matches, _, _) -- More than one matches
1726 -- Defer any reactions of a multitude
1727 -- until we learn more about the reagent
1728 -> do { traceTcS "matchClass multiple matches, deferring choice" $
1729 vcat [text "dict" <+> ppr pred,
1730 text "matches" <+> ppr matches]
1731 ; return NoInstance } }
1732 where
1733 pred = mkClassPred clas tys
1734
1735 match_one :: DFunId -> [DFunInstType] -> TcS LookupInstResult
1736 -- See Note [DFunInstType: instantiating types] in InstEnv
1737 match_one dfun_id mb_inst_tys
1738 = do { checkWellStagedDFun pred dfun_id loc
1739 ; (tys, theta) <- instDFunType dfun_id mb_inst_tys
1740 ; evc_vars <- mapM (newWantedEvVar loc) theta
1741 ; let new_ev_vars = freshGoals evc_vars
1742 -- new_ev_vars are only the real new variables that can be emitted
1743 dfun_app = EvDFunApp dfun_id tys (map (ctEvId . fst) evc_vars)
1744 ; return $ GenInst new_ev_vars dfun_app }
1745
1746 unifiable_givens :: Cts
1747 unifiable_givens = filterBag matchable $
1748 findDictsByClass (inert_dicts $ inert_cans inerts) clas
1749
1750 matchable (CDictCan { cc_class = clas_g, cc_tyargs = sys, cc_ev = fl })
1751 | isGiven fl
1752 , Just {} <- tcUnifyTys bind_meta_tv tys sys
1753 = ASSERT( clas_g == clas ) True
1754 | otherwise = False -- No overlap with a solved, already been taken care of
1755 -- by the overlap check with the instance environment.
1756 matchable ct = pprPanic "Expecting dictionary!" (ppr ct)
1757
1758 bind_meta_tv :: TcTyVar -> BindFlag
1759 -- Any meta tyvar may be unified later, so we treat it as
1760 -- bindable when unifying with givens. That ensures that we
1761 -- conservatively assume that a meta tyvar might get unified with
1762 -- something that matches the 'given', until demonstrated
1763 -- otherwise.
1764 bind_meta_tv tv | isMetaTyVar tv = BindMe
1765 | otherwise = Skolem
1766
1767 {- Note [Instance and Given overlap]
1768 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1769 Example, from the OutsideIn(X) paper:
1770 instance P x => Q [x]
1771 instance (x ~ y) => R y [x]
1772
1773 wob :: forall a b. (Q [b], R b a) => a -> Int
1774
1775 g :: forall a. Q [a] => [a] -> Int
1776 g x = wob x
1777
1778 This will generate the impliation constraint:
1779 Q [a] => (Q [beta], R beta [a])
1780 If we react (Q [beta]) with its top-level axiom, we end up with a
1781 (P beta), which we have no way of discharging. On the other hand,
1782 if we react R beta [a] with the top-level we get (beta ~ a), which
1783 is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
1784 now solvable by the given Q [a].
1785
1786 The solution is that:
1787 In matchClassInst (and thus in topReact), we return a matching
1788 instance only when there is no Given in the inerts which is
1789 unifiable to this particular dictionary.
1790
1791 We treat any meta-tyvar as "unifiable" for this purpose,
1792 *including* untouchable ones
1793
1794 The end effect is that, much as we do for overlapping instances, we
1795 delay choosing a class instance if there is a possibility of another
1796 instance OR a given to match our constraint later on. This fixes
1797 Trac #4981 and #5002.
1798
1799 Other notes:
1800
1801 * This is arguably not easy to appear in practice due to our
1802 aggressive prioritization of equality solving over other
1803 constraints, but it is possible. I've added a test case in
1804 typecheck/should-compile/GivenOverlapping.hs
1805
1806 * Another "live" example is Trac #10195
1807
1808 * We ignore the overlap problem if -XIncoherentInstances is in force:
1809 see Trac #6002 for a worked-out example where this makes a
1810 difference.
1811
1812 * Moreover notice that our goals here are different than the goals of
1813 the top-level overlapping checks. There we are interested in
1814 validating the following principle:
1815
1816 If we inline a function f at a site where the same global
1817 instance environment is available as the instance environment at
1818 the definition site of f then we should get the same behaviour.
1819
1820 But for the Given Overlap check our goal is just related to completeness of
1821 constraint solving.
1822 -}
1823
1824 -- | Is the constraint for an implicit CallStack parameter?
1825 isCallStackIP :: CtLoc -> Class -> Type -> Maybe (EvTerm -> EvCallStack)
1826 isCallStackIP loc cls ty
1827 | Just (tc, []) <- splitTyConApp_maybe ty
1828 , cls `hasKey` ipClassNameKey && tc `hasKey` callStackTyConKey
1829 = occOrigin (ctLocOrigin loc)
1830 where
1831 -- We only want to grab constraints that arose due to the use of an IP or a
1832 -- function call. See Note [Overview of implicit CallStacks]
1833 occOrigin (OccurrenceOf n)
1834 = Just (EvCsPushCall n locSpan)
1835 occOrigin (IPOccOrigin n)
1836 = Just (EvCsTop ('?' `consFS` hsIPNameFS n) locSpan)
1837 occOrigin _
1838 = Nothing
1839 locSpan
1840 = ctLocSpan loc
1841 isCallStackIP _ _ _
1842 = Nothing
1843
1844
1845
1846 -- | Assumes that we've checked that this is the 'Typeable' class,
1847 -- and it was applied to the correct argument.
1848 matchTypeableClass :: Class -> Kind -> Type -> CtLoc -> TcS LookupInstResult
1849 matchTypeableClass clas _k t loc
1850
1851 -- See Note [No Typeable for qualified types]
1852 | isForAllTy t = return NoInstance
1853 -- Is the type of the form `C => t`?
1854 | Just (t1,_) <- splitFunTy_maybe t,
1855 isConstraintKind (typeKind t1) = return NoInstance
1856
1857 | Just (tc, ks) <- splitTyConApp_maybe t
1858 , all isKind ks = doTyCon tc ks
1859 | Just (f,kt) <- splitAppTy_maybe t = doTyApp f kt
1860 | Just _ <- isNumLitTy t = mkSimpEv (EvTypeableTyLit t)
1861 | Just _ <- isStrLitTy t = mkSimpEv (EvTypeableTyLit t)
1862 | otherwise = return NoInstance
1863
1864 where
1865 -- Representation for type constructor applied to some kinds
1866 doTyCon tc ks =
1867 case mapM kindRep ks of
1868 Nothing -> return NoInstance
1869 Just kReps -> mkSimpEv (EvTypeableTyCon tc kReps)
1870
1871 {- Representation for an application of a type to a type-or-kind.
1872 This may happen when the type expression starts with a type variable.
1873 Example (ignoring kind parameter):
1874 Typeable (f Int Char) -->
1875 (Typeable (f Int), Typeable Char) -->
1876 (Typeable f, Typeable Int, Typeable Char) --> (after some simp. steps)
1877 Typeable f
1878 -}
1879 doTyApp f tk
1880 | isKind tk = return NoInstance -- We can't solve until we know the ctr.
1881 | otherwise =
1882 do ct1 <- subGoal f
1883 ct2 <- subGoal tk
1884 let realSubs = [ c | (c,Fresh) <- [ct1,ct2] ]
1885 return $ GenInst realSubs
1886 $ EvTypeable $ EvTypeableTyApp (getEv ct1,f) (getEv ct2,tk)
1887
1888
1889 -- Representation for concrete kinds. We just use the kind itself,
1890 -- but first check to make sure that it is "simple" (i.e., made entirely
1891 -- out of kind constructors).
1892 kindRep ki = do (_,ks) <- splitTyConApp_maybe ki
1893 mapM_ kindRep ks
1894 return ki
1895
1896 getEv (ct,_fresh) = ctEvTerm ct
1897
1898 -- Emit a `Typeable` constraint for the given type.
1899 subGoal ty = do let goal = mkClassPred clas [ typeKind ty, ty ]
1900 newWantedEvVar loc goal
1901
1902 mkSimpEv ev = return (GenInst [] (EvTypeable ev))
1903
1904 {- Note [No Typeable for polytype or for constraints]
1905 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1906 We do not support impredicative typeable, such as
1907 Typeable (forall a. a->a)
1908 Typeable (Eq a => a -> a)
1909 Typeable (() => Int)
1910 Typeable (((),()) => Int)
1911
1912 See Trac #9858. For forall's the case is clear: we simply don't have
1913 a TypeRep for them. For qualified but not polymorphic types, like
1914 (Eq a => a -> a), things are murkier. But:
1915
1916 * We don't need a TypeRep for these things. TypeReps are for
1917 monotypes only.
1918
1919 * Perhaps we could treat `=>` as another type constructor for `Typeable`
1920 purposes, and thus support things like `Eq Int => Int`, however,
1921 at the current state of affairs this would be an odd exception as
1922 no other class works with impredicative types.
1923 For now we leave it off, until we have a better story for impredicativity.
1924 -}