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