Comments only, mainly on superclasses
[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 = IRKeep | IRReplace | IRDelete
454 instance Outputable InteractResult where
455 ppr IRKeep = ptext (sLit "keep")
456 ppr IRReplace = ptext (sLit "replace")
457 ppr IRDelete = ptext (sLit "delete")
458
459 solveOneFromTheOther :: CtEvidence -- Inert
460 -> CtEvidence -- WorkItem
461 -> TcS (InteractResult, StopNowFlag)
462 -- Preconditions:
463 -- 1) inert and work item represent evidence for the /same/ predicate
464 -- 2) ip/class/irred evidence (no coercions) only
465 solveOneFromTheOther ev_i ev_w
466 | isDerived ev_w
467 = return (IRKeep, True)
468
469 | isDerived ev_i -- The inert item is Derived, we can just throw it away,
470 -- The ev_w is inert wrt earlier inert-set items,
471 -- so it's safe to continue on from this point
472 = return (IRDelete, False)
473
474 | CtWanted { ctev_evar = ev_id } <- ev_w
475 = do { setEvBind ev_id (ctEvTerm ev_i)
476 ; return (IRKeep, True) }
477
478 | CtWanted { ctev_evar = ev_id } <- ev_i
479 = do { setEvBind ev_id (ctEvTerm ev_w)
480 ; return (IRReplace, True) }
481
482 | otherwise -- If both are Given, we already have evidence; no need to duplicate
483 -- But the work item *overrides* the inert item (hence IRReplace)
484 -- See Note [Shadowing of Implicit Parameters]
485 = return (IRReplace, True)
486
487 {-
488 *********************************************************************************
489 * *
490 interactIrred
491 * *
492 *********************************************************************************
493 -}
494
495 -- Two pieces of irreducible evidence: if their types are *exactly identical*
496 -- we can rewrite them. We can never improve using this:
497 -- if we want ty1 :: Constraint and have ty2 :: Constraint it clearly does not
498 -- mean that (ty1 ~ ty2)
499 interactIrred :: InertCans -> Ct -> TcS (StopOrContinue Ct)
500
501 interactIrred inerts workItem@(CIrredEvCan { cc_ev = ev_w })
502 | let pred = ctEvPred ev_w
503 (matching_irreds, others) = partitionBag (\ct -> ctPred ct `tcEqType` pred)
504 (inert_irreds inerts)
505 , (ct_i : rest) <- bagToList matching_irreds
506 , let ctev_i = ctEvidence ct_i
507 = ASSERT( null rest )
508 do { (inert_effect, stop_now) <- solveOneFromTheOther ctev_i ev_w
509 ; case inert_effect of
510 IRKeep -> return ()
511 IRDelete -> updInertIrreds (\_ -> others)
512 IRReplace -> updInertIrreds (\_ -> others `snocCts` workItem)
513 -- These const upd's assume that solveOneFromTheOther
514 -- has no side effects on InertCans
515 ; if stop_now then
516 return (Stop ev_w (ptext (sLit "Irred equal") <+> parens (ppr inert_effect)))
517 ; else
518 continueWith workItem }
519
520 | otherwise
521 = continueWith workItem
522
523 interactIrred _ wi = pprPanic "interactIrred" (ppr wi)
524
525 {-
526 *********************************************************************************
527 * *
528 interactDict
529 * *
530 *********************************************************************************
531 -}
532
533 interactDict :: InertCans -> Ct -> TcS (StopOrContinue Ct)
534 interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs = tys })
535 | Just ctev_i <- lookupInertDict inerts (ctEvLoc ev_w) cls tys
536 = do { (inert_effect, stop_now) <- solveOneFromTheOther ctev_i ev_w
537 ; case inert_effect of
538 IRKeep -> return ()
539 IRDelete -> updInertDicts $ \ ds -> delDict ds cls tys
540 IRReplace -> updInertDicts $ \ ds -> addDict ds cls tys workItem
541 ; if stop_now then
542 return (Stop ev_w (ptext (sLit "Dict equal") <+> parens (ppr inert_effect)))
543 else
544 continueWith workItem }
545
546 | cls `hasKey` ipClassNameKey
547 , isGiven ev_w
548 = interactGivenIP inerts workItem
549
550 | otherwise
551 = do { mapBagM_ (addFunDepWork workItem) (findDictsByClass (inert_dicts inerts) cls)
552 -- Standard thing: create derived fds and keep on going. Importantly we don't
553 -- throw workitem back in the worklist because this can cause loops (see #5236)
554 ; continueWith workItem }
555
556 interactDict _ wi = pprPanic "interactDict" (ppr wi)
557
558 interactGivenIP :: InertCans -> Ct -> TcS (StopOrContinue Ct)
559 -- Work item is Given (?x:ty)
560 -- See Note [Shadowing of Implicit Parameters]
561 interactGivenIP inerts workItem@(CDictCan { cc_ev = ev, cc_class = cls
562 , cc_tyargs = tys@(ip_str:_) })
563 = do { updInertCans $ \cans -> cans { inert_dicts = addDict filtered_dicts cls tys workItem }
564 ; stopWith ev "Given IP" }
565 where
566 dicts = inert_dicts inerts
567 ip_dicts = findDictsByClass dicts cls
568 other_ip_dicts = filterBag (not . is_this_ip) ip_dicts
569 filtered_dicts = addDictsByClass dicts cls other_ip_dicts
570
571 -- Pick out any Given constraints for the same implicit parameter
572 is_this_ip (CDictCan { cc_ev = ev, cc_tyargs = ip_str':_ })
573 = isGiven ev && ip_str `tcEqType` ip_str'
574 is_this_ip _ = False
575
576 interactGivenIP _ wi = pprPanic "interactGivenIP" (ppr wi)
577
578 addFunDepWork :: Ct -> Ct -> TcS ()
579 addFunDepWork work_ct inert_ct
580 = do { let fd_eqns :: [Equation CtLoc]
581 fd_eqns = [ eqn { fd_loc = derived_loc }
582 | eqn <- improveFromAnother inert_pred work_pred ]
583 ; rewriteWithFunDeps fd_eqns
584 -- We don't really rewrite tys2, see below _rewritten_tys2, so that's ok
585 -- NB: We do create FDs for given to report insoluble equations that arise
586 -- from pairs of Givens, and also because of floating when we approximate
587 -- implications. The relevant test is: typecheck/should_fail/FDsFromGivens.hs
588 -- Also see Note [When improvement happens]
589 }
590 where
591 work_pred = ctPred work_ct
592 inert_pred = ctPred inert_ct
593 work_loc = ctLoc work_ct
594 inert_loc = ctLoc inert_ct
595 derived_loc = work_loc { ctl_origin = FunDepOrigin1 work_pred work_loc
596 inert_pred inert_loc }
597
598 {-
599 Note [Shadowing of Implicit Parameters]
600 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
601 Consider the following example:
602
603 f :: (?x :: Char) => Char
604 f = let ?x = 'a' in ?x
605
606 The "let ?x = ..." generates an implication constraint of the form:
607
608 ?x :: Char => ?x :: Char
609
610 Furthermore, the signature for `f` also generates an implication
611 constraint, so we end up with the following nested implication:
612
613 ?x :: Char => (?x :: Char => ?x :: Char)
614
615 Note that the wanted (?x :: Char) constraint may be solved in
616 two incompatible ways: either by using the parameter from the
617 signature, or by using the local definition. Our intention is
618 that the local definition should "shadow" the parameter of the
619 signature, and we implement this as follows: when we add a new
620 *given* implicit parameter to the inert set, it replaces any existing
621 givens for the same implicit parameter.
622
623 This works for the normal cases but it has an odd side effect
624 in some pathological programs like this:
625
626 -- This is accepted, the second parameter shadows
627 f1 :: (?x :: Int, ?x :: Char) => Char
628 f1 = ?x
629
630 -- This is rejected, the second parameter shadows
631 f2 :: (?x :: Int, ?x :: Char) => Int
632 f2 = ?x
633
634 Both of these are actually wrong: when we try to use either one,
635 we'll get two incompatible wnated constraints (?x :: Int, ?x :: Char),
636 which would lead to an error.
637
638 I can think of two ways to fix this:
639
640 1. Simply disallow multiple constratits for the same implicit
641 parameter---this is never useful, and it can be detected completely
642 syntactically.
643
644 2. Move the shadowing machinery to the location where we nest
645 implications, and add some code here that will produce an
646 error if we get multiple givens for the same implicit parameter.
647
648
649 *********************************************************************************
650 * *
651 interactFunEq
652 * *
653 *********************************************************************************
654 -}
655
656 interactFunEq :: InertCans -> Ct -> TcS (StopOrContinue Ct)
657 -- Try interacting the work item with the inert set
658 interactFunEq inerts workItem@(CFunEqCan { cc_ev = ev, cc_fun = tc
659 , cc_tyargs = args, cc_fsk = fsk })
660 | Just (CFunEqCan { cc_ev = ev_i, cc_fsk = fsk_i }) <- matching_inerts
661 = if ev_i `canRewriteOrSame` ev
662 then -- Rewrite work-item using inert
663 do { traceTcS "reactFunEq (discharge work item):" $
664 vcat [ text "workItem =" <+> ppr workItem
665 , text "inertItem=" <+> ppr ev_i ]
666 ; reactFunEq ev_i fsk_i ev fsk
667 ; stopWith ev "Inert rewrites work item" }
668 else -- Rewrite intert using work-item
669 do { traceTcS "reactFunEq (rewrite inert item):" $
670 vcat [ text "workItem =" <+> ppr workItem
671 , text "inertItem=" <+> ppr ev_i ]
672 ; updInertFunEqs $ \ feqs -> insertFunEq feqs tc args workItem
673 -- Do the updInertFunEqs before the reactFunEq, so that
674 -- we don't kick out the inertItem as well as consuming it!
675 ; reactFunEq ev fsk ev_i fsk_i
676 ; stopWith ev "Work item rewrites inert" }
677
678 | Just ops <- isBuiltInSynFamTyCon_maybe tc
679 = do { let matching_funeqs = findFunEqsByTyCon funeqs tc
680 ; let interact = sfInteractInert ops args (lookupFlattenTyVar eqs fsk)
681 do_one (CFunEqCan { cc_tyargs = iargs, cc_fsk = ifsk, cc_ev = iev })
682 = mapM_ (unifyDerived (ctEvLoc iev) Nominal)
683 (interact iargs (lookupFlattenTyVar eqs ifsk))
684 do_one ct = pprPanic "interactFunEq" (ppr ct)
685 ; mapM_ do_one matching_funeqs
686 ; traceTcS "builtInCandidates 1: " $ vcat [ ptext (sLit "Candidates:") <+> ppr matching_funeqs
687 , ptext (sLit "TvEqs:") <+> ppr eqs ]
688 ; return (ContinueWith workItem) }
689
690 | otherwise
691 = return (ContinueWith workItem)
692 where
693 eqs = inert_eqs inerts
694 funeqs = inert_funeqs inerts
695 matching_inerts = findFunEqs funeqs tc args
696
697 interactFunEq _ wi = pprPanic "interactFunEq" (ppr wi)
698
699 lookupFlattenTyVar :: TyVarEnv EqualCtList -> TcTyVar -> TcType
700 -- ^ Look up a flatten-tyvar in the inert nominal TyVarEqs;
701 -- this is used only when dealing with a CFunEqCan
702 lookupFlattenTyVar inert_eqs ftv
703 = case lookupVarEnv inert_eqs ftv of
704 Just (CTyEqCan { cc_rhs = rhs, cc_eq_rel = NomEq } : _) -> rhs
705 _ -> mkTyVarTy ftv
706
707 reactFunEq :: CtEvidence -> TcTyVar -- From this :: F tys ~ fsk1
708 -> CtEvidence -> TcTyVar -- Solve this :: F tys ~ fsk2
709 -> TcS ()
710 reactFunEq from_this fsk1 (CtGiven { ctev_evtm = tm, ctev_loc = loc }) fsk2
711 = do { let fsk_eq_co = mkTcSymCo (evTermCoercion tm)
712 `mkTcTransCo` ctEvCoercion from_this
713 -- :: fsk2 ~ fsk1
714 fsk_eq_pred = mkTcEqPred (mkTyVarTy fsk2) (mkTyVarTy fsk1)
715 ; new_ev <- newGivenEvVar loc (fsk_eq_pred, EvCoercion fsk_eq_co)
716 ; emitWorkNC [new_ev] }
717
718 reactFunEq from_this fuv1 (CtWanted { ctev_evar = evar }) fuv2
719 = dischargeFmv evar fuv2 (ctEvCoercion from_this) (mkTyVarTy fuv1)
720
721 reactFunEq _ _ solve_this@(CtDerived {}) _
722 = pprPanic "reactFunEq" (ppr solve_this)
723
724 {-
725 Note [Cache-caused loops]
726 ~~~~~~~~~~~~~~~~~~~~~~~~~
727 It is very dangerous to cache a rewritten wanted family equation as 'solved' in our
728 solved cache (which is the default behaviour or xCtEvidence), because the interaction
729 may not be contributing towards a solution. Here is an example:
730
731 Initial inert set:
732 [W] g1 : F a ~ beta1
733 Work item:
734 [W] g2 : F a ~ beta2
735 The work item will react with the inert yielding the _same_ inert set plus:
736 i) Will set g2 := g1 `cast` g3
737 ii) Will add to our solved cache that [S] g2 : F a ~ beta2
738 iii) Will emit [W] g3 : beta1 ~ beta2
739 Now, the g3 work item will be spontaneously solved to [G] g3 : beta1 ~ beta2
740 and then it will react the item in the inert ([W] g1 : F a ~ beta1). So it
741 will set
742 g1 := g ; sym g3
743 and what is g? Well it would ideally be a new goal of type (F a ~ beta2) but
744 remember that we have this in our solved cache, and it is ... g2! In short we
745 created the evidence loop:
746
747 g2 := g1 ; g3
748 g3 := refl
749 g1 := g2 ; sym g3
750
751 To avoid this situation we do not cache as solved any workitems (or inert)
752 which did not really made a 'step' towards proving some goal. Solved's are
753 just an optimization so we don't lose anything in terms of completeness of
754 solving.
755
756
757 Note [Efficient Orientation]
758 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
759 Suppose we are interacting two FunEqCans with the same LHS:
760 (inert) ci :: (F ty ~ xi_i)
761 (work) cw :: (F ty ~ xi_w)
762 We prefer to keep the inert (else we pass the work item on down
763 the pipeline, which is a bit silly). If we keep the inert, we
764 will (a) discharge 'cw'
765 (b) produce a new equality work-item (xi_w ~ xi_i)
766 Notice the orientation (xi_w ~ xi_i) NOT (xi_i ~ xi_w):
767 new_work :: xi_w ~ xi_i
768 cw := ci ; sym new_work
769 Why? Consider the simplest case when xi1 is a type variable. If
770 we generate xi1~xi2, porcessing that constraint will kick out 'ci'.
771 If we generate xi2~xi1, there is less chance of that happening.
772 Of course it can and should still happen if xi1=a, xi1=Int, say.
773 But we want to avoid it happening needlessly.
774
775 Similarly, if we *can't* keep the inert item (because inert is Wanted,
776 and work is Given, say), we prefer to orient the new equality (xi_i ~
777 xi_w).
778
779 Note [Carefully solve the right CFunEqCan]
780 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
781 ---- OLD COMMENT, NOW NOT NEEDED
782 ---- because we now allow multiple
783 ---- wanted FunEqs with the same head
784 Consider the constraints
785 c1 :: F Int ~ a -- Arising from an application line 5
786 c2 :: F Int ~ Bool -- Arising from an application line 10
787 Suppose that 'a' is a unification variable, arising only from
788 flattening. So there is no error on line 5; it's just a flattening
789 variable. But there is (or might be) an error on line 10.
790
791 Two ways to combine them, leaving either (Plan A)
792 c1 :: F Int ~ a -- Arising from an application line 5
793 c3 :: a ~ Bool -- Arising from an application line 10
794 or (Plan B)
795 c2 :: F Int ~ Bool -- Arising from an application line 10
796 c4 :: a ~ Bool -- Arising from an application line 5
797
798 Plan A will unify c3, leaving c1 :: F Int ~ Bool as an error
799 on the *totally innocent* line 5. An example is test SimpleFail16
800 where the expected/actual message comes out backwards if we use
801 the wrong plan.
802
803 The second is the right thing to do. Hence the isMetaTyVarTy
804 test when solving pairwise CFunEqCan.
805
806
807 *********************************************************************************
808 * *
809 interactTyVarEq
810 * *
811 *********************************************************************************
812 -}
813
814 interactTyVarEq :: InertCans -> Ct -> TcS (StopOrContinue Ct)
815 -- CTyEqCans are always consumed, so always returns Stop
816 interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv
817 , cc_rhs = rhs
818 , cc_ev = ev
819 , cc_eq_rel = eq_rel })
820 | (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i }
821 <- findTyEqs inerts tv
822 , ev_i `canRewriteOrSame` ev
823 , rhs_i `tcEqType` rhs ]
824 = -- Inert: a ~ b
825 -- Work item: a ~ b
826 do { when (isWanted ev) $
827 setEvBind (ctev_evar ev) (ctEvTerm ev_i)
828 ; stopWith ev "Solved from inert" }
829
830 | Just tv_rhs <- getTyVar_maybe rhs
831 , (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i }
832 <- findTyEqs inerts tv_rhs
833 , ev_i `canRewriteOrSame` ev
834 , rhs_i `tcEqType` mkTyVarTy tv ]
835 = -- Inert: a ~ b
836 -- Work item: b ~ a
837 do { when (isWanted ev) $
838 setEvBind (ctev_evar ev)
839 (EvCoercion (mkTcSymCo (ctEvCoercion ev_i)))
840 ; stopWith ev "Solved from inert (r)" }
841
842 | otherwise
843 = do { tclvl <- getTcLevel
844 ; if canSolveByUnification tclvl ev eq_rel tv rhs
845 then do { solveByUnification ev tv rhs
846 ; n_kicked <- kickOutRewritable Given NomEq tv
847 -- Given because the tv := xi is given
848 -- NomEq because only nom. equalities are solved
849 -- by unification
850 ; return (Stop ev (ptext (sLit "Spontaneously solved") <+> ppr_kicked n_kicked)) }
851
852 else do { traceTcS "Can't solve tyvar equality"
853 (vcat [ text "LHS:" <+> ppr tv <+> dcolon <+> ppr (tyVarKind tv)
854 , ppWhen (isMetaTyVar tv) $
855 nest 4 (text "TcLevel of" <+> ppr tv
856 <+> text "is" <+> ppr (metaTyVarTcLevel tv))
857 , text "RHS:" <+> ppr rhs <+> dcolon <+> ppr (typeKind rhs)
858 , text "TcLevel =" <+> ppr tclvl ])
859 ; n_kicked <- kickOutRewritable (ctEvFlavour ev)
860 (ctEvEqRel ev)
861 tv
862 ; updInertCans (\ ics -> addInertCan ics workItem)
863 ; return (Stop ev (ptext (sLit "Kept as inert") <+> ppr_kicked n_kicked)) } }
864
865 interactTyVarEq _ wi = pprPanic "interactTyVarEq" (ppr wi)
866
867 -- @trySpontaneousSolve wi@ solves equalities where one side is a
868 -- touchable unification variable.
869 -- Returns True <=> spontaneous solve happened
870 canSolveByUnification :: TcLevel -> CtEvidence -> EqRel
871 -> TcTyVar -> Xi -> Bool
872 canSolveByUnification tclvl gw eq_rel tv xi
873 | ReprEq <- eq_rel -- we never solve representational equalities this way.
874 = False
875
876 | isGiven gw -- See Note [Touchables and givens]
877 = False
878
879 | isTouchableMetaTyVar tclvl tv
880 = case metaTyVarInfo tv of
881 SigTv -> is_tyvar xi
882 _ -> True
883
884 | otherwise -- Untouchable
885 = False
886 where
887 is_tyvar xi
888 = case tcGetTyVar_maybe xi of
889 Nothing -> False
890 Just tv -> case tcTyVarDetails tv of
891 MetaTv { mtv_info = info }
892 -> case info of
893 SigTv -> True
894 _ -> False
895 SkolemTv {} -> True
896 FlatSkol {} -> False
897 RuntimeUnk -> True
898
899 solveByUnification :: CtEvidence -> TcTyVar -> Xi -> TcS ()
900 -- Solve with the identity coercion
901 -- Precondition: kind(xi) is a sub-kind of kind(tv)
902 -- Precondition: CtEvidence is Wanted or Derived
903 -- Precondition: CtEvidence is nominal
904 -- Returns: workItem where
905 -- workItem = the new Given constraint
906 --
907 -- NB: No need for an occurs check here, because solveByUnification always
908 -- arises from a CTyEqCan, a *canonical* constraint. Its invariants
909 -- say that in (a ~ xi), the type variable a does not appear in xi.
910 -- See TcRnTypes.Ct invariants.
911 --
912 -- Post: tv is unified (by side effect) with xi;
913 -- we often write tv := xi
914 solveByUnification wd tv xi
915 = do { let tv_ty = mkTyVarTy tv
916 ; traceTcS "Sneaky unification:" $
917 vcat [text "Unifies:" <+> ppr tv <+> ptext (sLit ":=") <+> ppr xi,
918 text "Coercion:" <+> pprEq tv_ty xi,
919 text "Left Kind is:" <+> ppr (typeKind tv_ty),
920 text "Right Kind is:" <+> ppr (typeKind xi) ]
921
922 ; let xi' = defaultKind xi
923 -- We only instantiate kind unification variables
924 -- with simple kinds like *, not OpenKind or ArgKind
925 -- cf TcUnify.uUnboundKVar
926
927 ; setWantedTyBind tv xi'
928 ; when (isWanted wd) $
929 setEvBind (ctEvId wd) (EvCoercion (mkTcNomReflCo xi')) }
930
931
932 ppr_kicked :: Int -> SDoc
933 ppr_kicked 0 = empty
934 ppr_kicked n = parens (int n <+> ptext (sLit "kicked out"))
935
936 kickOutRewritable :: CtFlavour -- Flavour of the equality that is
937 -- being added to the inert set
938 -> EqRel -- of the new equality
939 -> TcTyVar -- The new equality is tv ~ ty
940 -> TcS Int
941 kickOutRewritable new_flavour new_eq_rel new_tv
942 | not ((new_flavour, new_eq_rel) `eqCanRewriteFR` (new_flavour, new_eq_rel))
943 = return 0 -- If new_flavour can't rewrite itself, it can't rewrite
944 -- anything else, so no need to kick out anything
945 -- This is a common case: wanteds can't rewrite wanteds
946
947 | otherwise
948 = do { ics <- getInertCans
949 ; let (kicked_out, ics') = kick_out new_flavour new_eq_rel new_tv ics
950 ; setInertCans ics'
951 ; updWorkListTcS (appendWorkList kicked_out)
952
953 ; unless (isEmptyWorkList kicked_out) $
954 csTraceTcS $
955 hang (ptext (sLit "Kick out, tv =") <+> ppr new_tv)
956 2 (vcat [ text "n-kicked =" <+> int (workListSize kicked_out)
957 , text "n-kept fun-eqs =" <+> int (sizeFunEqMap (inert_funeqs ics'))
958 , ppr kicked_out ])
959 ; return (workListSize kicked_out) }
960
961 kick_out :: CtFlavour -> EqRel -> TcTyVar -> InertCans -> (WorkList, InertCans)
962 kick_out new_flavour new_eq_rel new_tv (IC { inert_eqs = tv_eqs
963 , inert_dicts = dictmap
964 , inert_funeqs = funeqmap
965 , inert_irreds = irreds
966 , inert_insols = insols })
967 = (kicked_out, inert_cans_in)
968 where
969 -- NB: Notice that don't rewrite
970 -- inert_solved_dicts, and inert_solved_funeqs
971 -- optimistically. But when we lookup we have to
972 -- take the substitution into account
973 inert_cans_in = IC { inert_eqs = tv_eqs_in
974 , inert_dicts = dicts_in
975 , inert_funeqs = feqs_in
976 , inert_irreds = irs_in
977 , inert_insols = insols_in }
978
979 kicked_out = WL { wl_eqs = tv_eqs_out
980 , wl_funeqs = feqs_out
981 , wl_rest = bagToList (dicts_out `andCts` irs_out
982 `andCts` insols_out)
983 , wl_implics = emptyBag }
984
985 (tv_eqs_out, tv_eqs_in) = foldVarEnv kick_out_eqs ([], emptyVarEnv) tv_eqs
986 (feqs_out, feqs_in) = partitionFunEqs kick_out_ct funeqmap
987 (dicts_out, dicts_in) = partitionDicts kick_out_ct dictmap
988 (irs_out, irs_in) = partitionBag kick_out_irred irreds
989 (insols_out, insols_in) = partitionBag kick_out_ct insols
990 -- Kick out even insolubles; see Note [Kick out insolubles]
991
992 can_rewrite :: CtEvidence -> Bool
993 can_rewrite = ((new_flavour, new_eq_rel) `eqCanRewriteFR`) . ctEvFlavourRole
994
995 kick_out_ct :: Ct -> Bool
996 kick_out_ct ct = kick_out_ctev (ctEvidence ct)
997
998 kick_out_ctev :: CtEvidence -> Bool
999 kick_out_ctev ev = can_rewrite ev
1000 && new_tv `elemVarSet` tyVarsOfType (ctEvPred ev)
1001 -- See Note [Kicking out inert constraints]
1002
1003 kick_out_irred :: Ct -> Bool
1004 kick_out_irred ct = can_rewrite (cc_ev ct)
1005 && new_tv `elemVarSet` closeOverKinds (tyVarsOfCt ct)
1006 -- See Note [Kicking out Irreds]
1007
1008 kick_out_eqs :: EqualCtList -> ([Ct], TyVarEnv EqualCtList)
1009 -> ([Ct], TyVarEnv EqualCtList)
1010 kick_out_eqs eqs (acc_out, acc_in)
1011 = (eqs_out ++ acc_out, case eqs_in of
1012 [] -> acc_in
1013 (eq1:_) -> extendVarEnv acc_in (cc_tyvar eq1) eqs_in)
1014 where
1015 (eqs_in, eqs_out) = partition keep_eq eqs
1016
1017 -- implements criteria K1-K3 in Note [The inert equalities] in TcFlatten
1018 keep_eq (CTyEqCan { cc_tyvar = tv, cc_rhs = rhs_ty, cc_ev = ev
1019 , cc_eq_rel = eq_rel })
1020 | tv == new_tv
1021 = not (can_rewrite ev) -- (K1)
1022
1023 | otherwise
1024 = check_k2 && check_k3
1025 where
1026 check_k2 = not (ev `eqCanRewrite` ev)
1027 || not (can_rewrite ev)
1028 || not (new_tv `elemVarSet` tyVarsOfType rhs_ty)
1029
1030 check_k3
1031 | can_rewrite ev
1032 = case eq_rel of
1033 NomEq -> not (rhs_ty `eqType` mkTyVarTy new_tv)
1034 ReprEq -> isTyVarExposed new_tv rhs_ty
1035
1036 | otherwise
1037 = True
1038
1039 keep_eq ct = pprPanic "keep_eq" (ppr ct)
1040
1041 {-
1042 Note [Kicking out inert constraints]
1043 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1044 Given a new (a -> ty) inert, we want to kick out an existing inert
1045 constraint if
1046 a) the new constraint can rewrite the inert one
1047 b) 'a' is free in the inert constraint (so that it *will*)
1048 rewrite it if we kick it out.
1049
1050 For (b) we use tyVarsOfCt, which returns the type variables /and
1051 the kind variables/ that are directly visible in the type. Hence we
1052 will have exposed all the rewriting we care about to make the most
1053 precise kinds visible for matching classes etc. No need to kick out
1054 constraints that mention type variables whose kinds contain this
1055 variable! (Except see Note [Kicking out Irreds].)
1056
1057 Note [Kicking out Irreds]
1058 ~~~~~~~~~~~~~~~~~~~~~~~~~
1059 There is an awkward special case for Irreds. When we have a
1060 kind-mis-matched equality constraint (a:k1) ~ (ty:k2), we turn it into
1061 an Irred (see Note [Equalities with incompatible kinds] in
1062 TcCanonical). So in this case the free kind variables of k1 and k2
1063 are not visible. More precisely, the type looks like
1064 (~) k1 (a:k1) (ty:k2)
1065 because (~) has kind forall k. k -> k -> Constraint. So the constraint
1066 itself is ill-kinded. We can "see" k1 but not k2. That's why we use
1067 closeOverKinds to make sure we see k2.
1068
1069 This is not pretty. Maybe (~) should have kind
1070 (~) :: forall k1 k1. k1 -> k2 -> Constraint
1071
1072 Note [Kick out insolubles]
1073 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1074 Suppose we have an insoluble alpha ~ [alpha], which is insoluble
1075 because an occurs check. And then we unify alpha := [Int].
1076 Then we really want to rewrite the insouluble to [Int] ~ [[Int]].
1077 Now it can be decomposed. Otherwise we end up with a "Can't match
1078 [Int] ~ [[Int]]" which is true, but a bit confusing because the
1079 outer type constructors match.
1080
1081
1082 Note [Avoid double unifications]
1083 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1084 The spontaneous solver has to return a given which mentions the unified unification
1085 variable *on the left* of the equality. Here is what happens if not:
1086 Original wanted: (a ~ alpha), (alpha ~ Int)
1087 We spontaneously solve the first wanted, without changing the order!
1088 given : a ~ alpha [having unified alpha := a]
1089 Now the second wanted comes along, but he cannot rewrite the given, so we simply continue.
1090 At the end we spontaneously solve that guy, *reunifying* [alpha := Int]
1091
1092 We avoid this problem by orienting the resulting given so that the unification
1093 variable is on the left. [Note that alternatively we could attempt to
1094 enforce this at canonicalization]
1095
1096 See also Note [No touchables as FunEq RHS] in TcSMonad; avoiding
1097 double unifications is the main reason we disallow touchable
1098 unification variables as RHS of type family equations: F xis ~ alpha.
1099
1100
1101 ************************************************************************
1102 * *
1103 * Functional dependencies, instantiation of equations
1104 * *
1105 ************************************************************************
1106
1107 When we spot an equality arising from a functional dependency,
1108 we now use that equality (a "wanted") to rewrite the work-item
1109 constraint right away. This avoids two dangers
1110
1111 Danger 1: If we send the original constraint on down the pipeline
1112 it may react with an instance declaration, and in delicate
1113 situations (when a Given overlaps with an instance) that
1114 may produce new insoluble goals: see Trac #4952
1115
1116 Danger 2: If we don't rewrite the constraint, it may re-react
1117 with the same thing later, and produce the same equality
1118 again --> termination worries.
1119
1120 To achieve this required some refactoring of FunDeps.lhs (nicer
1121 now!).
1122 -}
1123
1124 rewriteWithFunDeps :: [Equation CtLoc] -> TcS ()
1125 -- NB: The returned constraints are all Derived
1126 -- Post: returns no trivial equalities (identities) and all EvVars returned are fresh
1127 rewriteWithFunDeps eqn_pred_locs
1128 = mapM_ instFunDepEqn eqn_pred_locs
1129
1130 instFunDepEqn :: Equation CtLoc -> TcS ()
1131 -- Post: Returns the position index as well as the corresponding FunDep equality
1132 instFunDepEqn (FDEqn { fd_qtvs = tvs, fd_eqs = eqs, fd_loc = loc })
1133 = do { (subst, _) <- instFlexiTcS tvs -- Takes account of kind substitution
1134 ; mapM_ (do_one subst) eqs }
1135 where
1136 do_one subst (FDEq { fd_ty_left = ty1, fd_ty_right = ty2 })
1137 = unifyDerived loc Nominal $
1138 Pair (Type.substTy subst ty1) (Type.substTy subst ty2)
1139
1140 {-
1141 *********************************************************************************
1142 * *
1143 The top-reaction Stage
1144 * *
1145 *********************************************************************************
1146 -}
1147
1148 topReactionsStage :: WorkItem -> TcS (StopOrContinue Ct)
1149 topReactionsStage wi
1150 = do { inerts <- getTcSInerts
1151 ; tir <- doTopReact inerts wi
1152 ; case tir of
1153 ContinueWith wi -> return (ContinueWith wi)
1154 Stop ev s -> return (Stop ev (ptext (sLit "Top react:") <+> s)) }
1155
1156 doTopReact :: InertSet -> WorkItem -> TcS (StopOrContinue Ct)
1157 -- The work item does not react with the inert set, so try interaction with top-level
1158 -- instances. Note:
1159 --
1160 -- (a) The place to add superclasses in not here in doTopReact stage.
1161 -- Instead superclasses are added in the worklist as part of the
1162 -- canonicalization process. See Note [Adding superclasses].
1163
1164 doTopReact inerts work_item
1165 = do { traceTcS "doTopReact" (ppr work_item)
1166 ; case work_item of
1167 CDictCan {} -> doTopReactDict inerts work_item
1168 CFunEqCan {} -> doTopReactFunEq work_item
1169 _ -> -- Any other work item does not react with any top-level equations
1170 return (ContinueWith work_item) }
1171
1172 --------------------
1173 doTopReactDict :: InertSet -> Ct -> TcS (StopOrContinue Ct)
1174 -- Try to use type-class instance declarations to simplify the constraint
1175 doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls
1176 , cc_tyargs = xis })
1177 | not (isWanted fl) -- Never use instances for Given or Derived constraints
1178 = try_fundeps_and_return
1179
1180 | Just ev <- lookupSolvedDict inerts loc cls xis -- Cached
1181 = do { setEvBind dict_id (ctEvTerm ev);
1182 ; stopWith fl "Dict/Top (cached)" }
1183
1184 | otherwise -- Not cached
1185 = do { lkup_inst_res <- matchClassInst inerts cls xis loc
1186 ; case lkup_inst_res of
1187 GenInst wtvs ev_term -> do { addSolvedDict fl cls xis
1188 ; solve_from_instance wtvs ev_term }
1189 NoInstance -> try_fundeps_and_return }
1190 where
1191 dict_id = ASSERT( isWanted fl ) ctEvId fl
1192 pred = mkClassPred cls xis
1193 loc = ctEvLoc fl
1194
1195 solve_from_instance :: [CtEvidence] -> EvTerm -> TcS (StopOrContinue Ct)
1196 -- Precondition: evidence term matches the predicate workItem
1197 solve_from_instance evs ev_term
1198 | null evs
1199 = do { traceTcS "doTopReact/found nullary instance for" $
1200 ppr dict_id
1201 ; setEvBind dict_id ev_term
1202 ; stopWith fl "Dict/Top (solved, no new work)" }
1203 | otherwise
1204 = do { traceTcS "doTopReact/found non-nullary instance for" $
1205 ppr dict_id
1206 ; setEvBind dict_id ev_term
1207 ; let mk_new_wanted ev
1208 = mkNonCanonical (ev {ctev_loc = bumpCtLocDepth CountConstraints loc })
1209 ; updWorkListTcS (extendWorkListCts (map mk_new_wanted evs))
1210 ; stopWith fl "Dict/Top (solved, more work)" }
1211
1212 -- We didn't solve it; so try functional dependencies with
1213 -- the instance environment, and return
1214 -- NB: even if there *are* some functional dependencies against the
1215 -- instance environment, there might be a unique match, and if
1216 -- so we make sure we get on and solve it first. See Note [Weird fundeps]
1217 try_fundeps_and_return
1218 = do { instEnvs <- getInstEnvs
1219 ; let fd_eqns :: [Equation CtLoc]
1220 fd_eqns = [ fd { fd_loc = loc { ctl_origin = FunDepOrigin2 pred (ctl_origin loc)
1221 inst_pred inst_loc } }
1222 | fd@(FDEqn { fd_loc = inst_loc, fd_pred1 = inst_pred })
1223 <- improveFromInstEnv instEnvs pred ]
1224 ; rewriteWithFunDeps fd_eqns
1225 ; continueWith work_item }
1226
1227 doTopReactDict _ w = pprPanic "doTopReactDict" (ppr w)
1228
1229 --------------------
1230 doTopReactFunEq :: Ct -> TcS (StopOrContinue Ct)
1231 doTopReactFunEq work_item@(CFunEqCan { cc_ev = old_ev, cc_fun = fam_tc
1232 , cc_tyargs = args , cc_fsk = fsk })
1233 = ASSERT(isTypeFamilyTyCon fam_tc) -- No associated data families
1234 -- have reached this far
1235 ASSERT( not (isDerived old_ev) ) -- CFunEqCan is never Derived
1236 -- Look up in top-level instances, or built-in axiom
1237 do { match_res <- matchFam fam_tc args -- See Note [MATCHING-SYNONYMS]
1238 ; case match_res of {
1239 Nothing -> do { try_improvement; continueWith work_item } ;
1240 Just (ax_co, rhs_ty)
1241
1242 -- Found a top-level instance
1243
1244 | Just (tc, tc_args) <- tcSplitTyConApp_maybe rhs_ty
1245 , isTypeFamilyTyCon tc
1246 , tc_args `lengthIs` tyConArity tc -- Short-cut
1247 -> shortCutReduction old_ev fsk ax_co tc tc_args
1248 -- Try shortcut; see Note [Short cut for top-level reaction]
1249
1250 | isGiven old_ev -- Not shortcut
1251 -> do { let final_co = mkTcSymCo (ctEvCoercion old_ev) `mkTcTransCo` ax_co
1252 -- final_co :: fsk ~ rhs_ty
1253 ; new_ev <- newGivenEvVar deeper_loc (mkTcEqPred (mkTyVarTy fsk) rhs_ty,
1254 EvCoercion final_co)
1255 ; emitWorkNC [new_ev] -- Non-cannonical; that will mean we flatten rhs_ty
1256 ; stopWith old_ev "Fun/Top (given)" }
1257
1258 | not (fsk `elemVarSet` tyVarsOfType rhs_ty)
1259 -> do { dischargeFmv (ctEvId old_ev) fsk ax_co rhs_ty
1260 ; traceTcS "doTopReactFunEq" $
1261 vcat [ text "old_ev:" <+> ppr old_ev
1262 , nest 2 (text ":=") <+> ppr ax_co ]
1263 ; stopWith old_ev "Fun/Top (wanted)" }
1264
1265 | otherwise -- We must not assign ufsk := ...ufsk...!
1266 -> do { alpha_ty <- newFlexiTcSTy (tyVarKind fsk)
1267 ; new_ev <- newWantedEvVarNC loc (mkTcEqPred alpha_ty rhs_ty)
1268 ; emitWorkNC [new_ev]
1269 -- By emitting this as non-canonical, we deal with all
1270 -- flattening, occurs-check, and ufsk := ufsk issues
1271 ; let final_co = ax_co `mkTcTransCo` mkTcSymCo (ctEvCoercion new_ev)
1272 -- ax_co :: fam_tc args ~ rhs_ty
1273 -- ev :: alpha ~ rhs_ty
1274 -- ufsk := alpha
1275 -- final_co :: fam_tc args ~ alpha
1276 ; dischargeFmv (ctEvId old_ev) fsk final_co alpha_ty
1277 ; traceTcS "doTopReactFunEq (occurs)" $
1278 vcat [ text "old_ev:" <+> ppr old_ev
1279 , nest 2 (text ":=") <+> ppr final_co
1280 , text "new_ev:" <+> ppr new_ev ]
1281 ; stopWith old_ev "Fun/Top (wanted)" } } }
1282 where
1283 loc = ctEvLoc old_ev
1284 deeper_loc = bumpCtLocDepth CountTyFunApps loc
1285
1286 try_improvement
1287 | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc
1288 = do { inert_eqs <- getInertEqs
1289 ; let eqns = sfInteractTop ops args (lookupFlattenTyVar inert_eqs fsk)
1290 ; mapM_ (unifyDerived loc Nominal) eqns }
1291 | otherwise
1292 = return ()
1293
1294 doTopReactFunEq w = pprPanic "doTopReactFunEq" (ppr w)
1295
1296 shortCutReduction :: CtEvidence -> TcTyVar -> TcCoercion
1297 -> TyCon -> [TcType] -> TcS (StopOrContinue Ct)
1298 shortCutReduction old_ev fsk ax_co fam_tc tc_args
1299 | isGiven old_ev
1300 = ASSERT( ctEvEqRel old_ev == NomEq )
1301 runFlatten $
1302 do { let fmode = mkFlattenEnv FM_FlattenAll old_ev
1303 ; (xis, cos) <- flatten_many fmode (repeat Nominal) tc_args
1304 -- ax_co :: F args ~ G tc_args
1305 -- cos :: xis ~ tc_args
1306 -- old_ev :: F args ~ fsk
1307 -- G cos ; sym ax_co ; old_ev :: G xis ~ fsk
1308
1309 ; new_ev <- newGivenEvVar deeper_loc
1310 ( mkTcEqPred (mkTyConApp fam_tc xis) (mkTyVarTy fsk)
1311 , EvCoercion (mkTcTyConAppCo Nominal fam_tc cos
1312 `mkTcTransCo` mkTcSymCo ax_co
1313 `mkTcTransCo` ctEvCoercion old_ev) )
1314
1315 ; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc, cc_tyargs = xis, cc_fsk = fsk }
1316 ; emitFlatWork new_ct
1317 ; stopWith old_ev "Fun/Top (given, shortcut)" }
1318
1319 | otherwise
1320 = ASSERT( not (isDerived old_ev) ) -- Caller ensures this
1321 ASSERT( ctEvEqRel old_ev == NomEq )
1322 runFlatten $
1323 do { let fmode = mkFlattenEnv FM_FlattenAll old_ev
1324 ; (xis, cos) <- flatten_many fmode (repeat Nominal) tc_args
1325 -- ax_co :: F args ~ G tc_args
1326 -- cos :: xis ~ tc_args
1327 -- G cos ; sym ax_co ; old_ev :: G xis ~ fsk
1328 -- new_ev :: G xis ~ fsk
1329 -- old_ev :: F args ~ fsk := ax_co ; sym (G cos) ; new_ev
1330
1331 ; new_ev <- newWantedEvVarNC loc (mkTcEqPred (mkTyConApp fam_tc xis) (mkTyVarTy fsk))
1332 ; setEvBind (ctEvId old_ev)
1333 (EvCoercion (ax_co `mkTcTransCo` mkTcSymCo (mkTcTyConAppCo Nominal fam_tc cos)
1334 `mkTcTransCo` ctEvCoercion new_ev))
1335
1336 ; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc, cc_tyargs = xis, cc_fsk = fsk }
1337 ; emitFlatWork new_ct
1338 ; stopWith old_ev "Fun/Top (wanted, shortcut)" }
1339 where
1340 loc = ctEvLoc old_ev
1341 deeper_loc = bumpCtLocDepth CountTyFunApps loc
1342
1343 dischargeFmv :: EvVar -> TcTyVar -> TcCoercion -> TcType -> TcS ()
1344 -- (dischargeFmv x fmv co ty)
1345 -- [W] x :: F tys ~ fuv
1346 -- co :: F tys ~ ty
1347 -- Precondition: fuv is not filled, and fuv `notElem` ty
1348 --
1349 -- Then set fuv := ty,
1350 -- set x := co
1351 -- kick out any inert things that are now rewritable
1352 dischargeFmv evar fmv co xi
1353 = ASSERT2( not (fmv `elemVarSet` tyVarsOfType xi), ppr evar $$ ppr fmv $$ ppr xi )
1354 do { setWantedTyBind fmv xi
1355 ; setEvBind evar (EvCoercion co)
1356 ; n_kicked <- kickOutRewritable Given NomEq fmv
1357 ; traceTcS "dischargeFuv" (ppr fmv <+> equals <+> ppr xi $$ ppr_kicked n_kicked) }
1358
1359 {-
1360 Note [Cached solved FunEqs]
1361 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1362 When trying to solve, say (FunExpensive big-type ~ ty), it's important
1363 to see if we have reduced (FunExpensive big-type) before, lest we
1364 simply repeat it. Hence the lookup in inert_solved_funeqs. Moreover
1365 we must use `canRewriteOrSame` because both uses might (say) be Wanteds,
1366 and we *still* want to save the re-computation.
1367
1368 Note [MATCHING-SYNONYMS]
1369 ~~~~~~~~~~~~~~~~~~~~~~~~
1370 When trying to match a dictionary (D tau) to a top-level instance, or a
1371 type family equation (F taus_1 ~ tau_2) to a top-level family instance,
1372 we do *not* need to expand type synonyms because the matcher will do that for us.
1373
1374
1375 Note [RHS-FAMILY-SYNONYMS]
1376 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1377 The RHS of a family instance is represented as yet another constructor which is
1378 like a type synonym for the real RHS the programmer declared. Eg:
1379 type instance F (a,a) = [a]
1380 Becomes:
1381 :R32 a = [a] -- internal type synonym introduced
1382 F (a,a) ~ :R32 a -- instance
1383
1384 When we react a family instance with a type family equation in the work list
1385 we keep the synonym-using RHS without expansion.
1386
1387 Note [FunDep and implicit parameter reactions]
1388 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1389 Currently, our story of interacting two dictionaries (or a dictionary
1390 and top-level instances) for functional dependencies, and implicit
1391 paramters, is that we simply produce new Derived equalities. So for example
1392
1393 class D a b | a -> b where ...
1394 Inert:
1395 d1 :g D Int Bool
1396 WorkItem:
1397 d2 :w D Int alpha
1398
1399 We generate the extra work item
1400 cv :d alpha ~ Bool
1401 where 'cv' is currently unused. However, this new item can perhaps be
1402 spontaneously solved to become given and react with d2,
1403 discharging it in favour of a new constraint d2' thus:
1404 d2' :w D Int Bool
1405 d2 := d2' |> D Int cv
1406 Now d2' can be discharged from d1
1407
1408 We could be more aggressive and try to *immediately* solve the dictionary
1409 using those extra equalities, but that requires those equalities to carry
1410 evidence and derived do not carry evidence.
1411
1412 If that were the case with the same inert set and work item we might dischard
1413 d2 directly:
1414
1415 cv :w alpha ~ Bool
1416 d2 := d1 |> D Int cv
1417
1418 But in general it's a bit painful to figure out the necessary coercion,
1419 so we just take the first approach. Here is a better example. Consider:
1420 class C a b c | a -> b
1421 And:
1422 [Given] d1 : C T Int Char
1423 [Wanted] d2 : C T beta Int
1424 In this case, it's *not even possible* to solve the wanted immediately.
1425 So we should simply output the functional dependency and add this guy
1426 [but NOT its superclasses] back in the worklist. Even worse:
1427 [Given] d1 : C T Int beta
1428 [Wanted] d2: C T beta Int
1429 Then it is solvable, but its very hard to detect this on the spot.
1430
1431 It's exactly the same with implicit parameters, except that the
1432 "aggressive" approach would be much easier to implement.
1433
1434 Note [When improvement happens]
1435 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1436 We fire an improvement rule when
1437
1438 * Two constraints match (modulo the fundep)
1439 e.g. C t1 t2, C t1 t3 where C a b | a->b
1440 The two match because the first arg is identical
1441
1442 Note that we *do* fire the improvement if one is Given and one is Derived (e.g. a
1443 superclass of a Wanted goal) or if both are Given.
1444
1445 Example (tcfail138)
1446 class L a b | a -> b
1447 class (G a, L a b) => C a b
1448
1449 instance C a b' => G (Maybe a)
1450 instance C a b => C (Maybe a) a
1451 instance L (Maybe a) a
1452
1453 When solving the superclasses of the (C (Maybe a) a) instance, we get
1454 Given: C a b ... and hance by superclasses, (G a, L a b)
1455 Wanted: G (Maybe a)
1456 Use the instance decl to get
1457 Wanted: C a b'
1458 The (C a b') is inert, so we generate its Derived superclasses (L a b'),
1459 and now we need improvement between that derived superclass an the Given (L a b)
1460
1461 Test typecheck/should_fail/FDsFromGivens also shows why it's a good idea to
1462 emit Derived FDs for givens as well.
1463
1464 Note [Weird fundeps]
1465 ~~~~~~~~~~~~~~~~~~~~
1466 Consider class Het a b | a -> b where
1467 het :: m (f c) -> a -> m b
1468
1469 class GHet (a :: * -> *) (b :: * -> *) | a -> b
1470 instance GHet (K a) (K [a])
1471 instance Het a b => GHet (K a) (K b)
1472
1473 The two instances don't actually conflict on their fundeps,
1474 although it's pretty strange. So they are both accepted. Now
1475 try [W] GHet (K Int) (K Bool)
1476 This triggers fudeps from both instance decls; but it also
1477 matches a *unique* instance decl, and we should go ahead and
1478 pick that one right now. Otherwise, if we don't, it ends up
1479 unsolved in the inert set and is reported as an error.
1480
1481 Trac #7875 is a case in point.
1482
1483 Note [Overriding implicit parameters]
1484 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1485 Consider
1486 f :: (?x::a) -> Bool -> a
1487
1488 g v = let ?x::Int = 3
1489 in (f v, let ?x::Bool = True in f v)
1490
1491 This should probably be well typed, with
1492 g :: Bool -> (Int, Bool)
1493
1494 So the inner binding for ?x::Bool *overrides* the outer one.
1495 Hence a work-item Given overrides an inert-item Given.
1496 -}
1497
1498 data LookupInstResult
1499 = NoInstance
1500 | GenInst [CtEvidence] EvTerm
1501
1502 instance Outputable LookupInstResult where
1503 ppr NoInstance = text "NoInstance"
1504 ppr (GenInst ev t) = text "GenInst" <+> ppr ev <+> ppr t
1505
1506
1507 matchClassInst :: InertSet -> Class -> [Type] -> CtLoc -> TcS LookupInstResult
1508
1509 matchClassInst _ clas [ ty ] _
1510 | className clas == knownNatClassName
1511 , Just n <- isNumLitTy ty = makeDict (EvNum n)
1512
1513 | className clas == knownSymbolClassName
1514 , Just s <- isStrLitTy ty = makeDict (EvStr s)
1515
1516 where
1517 {- This adds a coercion that will convert the literal into a dictionary
1518 of the appropriate type. See Note [KnownNat & KnownSymbol and EvLit]
1519 in TcEvidence. The coercion happens in 2 steps:
1520
1521 Integer -> SNat n -- representation of literal to singleton
1522 SNat n -> KnownNat n -- singleton to dictionary
1523
1524 The process is mirrored for Symbols:
1525 String -> SSymbol n
1526 SSymbol n -> KnownSymbol n
1527 -}
1528 makeDict evLit
1529 | Just (_, co_dict) <- tcInstNewTyCon_maybe (classTyCon clas) [ty]
1530 -- co_dict :: KnownNat n ~ SNat n
1531 , [ meth ] <- classMethods clas
1532 , Just tcRep <- tyConAppTyCon_maybe -- SNat
1533 $ funResultTy -- SNat n
1534 $ dropForAlls -- KnownNat n => SNat n
1535 $ idType meth -- forall n. KnownNat n => SNat n
1536 , Just (_, co_rep) <- tcInstNewTyCon_maybe tcRep [ty]
1537 -- SNat n ~ Integer
1538 = return (GenInst [] $ mkEvCast (EvLit evLit) (mkTcSymCo (mkTcTransCo co_dict co_rep)))
1539
1540 | otherwise
1541 = panicTcS (text "Unexpected evidence for" <+> ppr (className clas)
1542 $$ vcat (map (ppr . idType) (classMethods clas)))
1543
1544 matchClassInst inerts clas tys loc
1545 = do { dflags <- getDynFlags
1546 ; tclvl <- getTcLevel
1547 ; traceTcS "matchClassInst" $ vcat [ text "pred =" <+> ppr pred
1548 , text "inerts=" <+> ppr inerts
1549 , text "untouchables=" <+> ppr tclvl ]
1550 ; instEnvs <- getInstEnvs
1551 ; case lookupInstEnv instEnvs clas tys of
1552 ([], _, _) -- Nothing matches
1553 -> do { traceTcS "matchClass not matching" $
1554 vcat [ text "dict" <+> ppr pred ]
1555 ; return NoInstance }
1556
1557 ([(ispec, inst_tys)], [], _) -- A single match
1558 | not (xopt Opt_IncoherentInstances dflags)
1559 , given_overlap tclvl
1560 -> -- See Note [Instance and Given overlap]
1561 do { traceTcS "Delaying instance application" $
1562 vcat [ text "Workitem=" <+> pprType (mkClassPred clas tys)
1563 , text "Relevant given dictionaries=" <+> ppr givens_for_this_clas ]
1564 ; return NoInstance }
1565
1566 | otherwise
1567 -> do { let dfun_id = instanceDFunId ispec
1568 ; traceTcS "matchClass success" $
1569 vcat [text "dict" <+> ppr pred,
1570 text "witness" <+> ppr dfun_id
1571 <+> ppr (idType dfun_id) ]
1572 -- Record that this dfun is needed
1573 ; match_one dfun_id inst_tys }
1574
1575 (matches, _, _) -- More than one matches
1576 -- Defer any reactions of a multitude
1577 -- until we learn more about the reagent
1578 -> do { traceTcS "matchClass multiple matches, deferring choice" $
1579 vcat [text "dict" <+> ppr pred,
1580 text "matches" <+> ppr matches]
1581 ; return NoInstance } }
1582 where
1583 pred = mkClassPred clas tys
1584
1585 match_one :: DFunId -> [DFunInstType] -> TcS LookupInstResult
1586 -- See Note [DFunInstType: instantiating types] in InstEnv
1587 match_one dfun_id mb_inst_tys
1588 = do { checkWellStagedDFun pred dfun_id loc
1589 ; (tys, theta) <- instDFunType dfun_id mb_inst_tys
1590 ; evc_vars <- mapM (newWantedEvVar loc) theta
1591 ; let new_ev_vars = freshGoals evc_vars
1592 -- new_ev_vars are only the real new variables that can be emitted
1593 dfun_app = EvDFunApp dfun_id tys (map (ctEvTerm . fst) evc_vars)
1594 ; return $ GenInst new_ev_vars dfun_app }
1595
1596 givens_for_this_clas :: Cts
1597 givens_for_this_clas
1598 = filterBag isGivenCt (findDictsByClass (inert_dicts $ inert_cans inerts) clas)
1599
1600 given_overlap :: TcLevel -> Bool
1601 given_overlap tclvl = anyBag (matchable tclvl) givens_for_this_clas
1602
1603 matchable tclvl (CDictCan { cc_class = clas_g, cc_tyargs = sys
1604 , cc_ev = fl })
1605 | isGiven fl
1606 = ASSERT( clas_g == clas )
1607 case tcUnifyTys (\tv -> if isTouchableMetaTyVar tclvl tv &&
1608 tv `elemVarSet` tyVarsOfTypes tys
1609 then BindMe else Skolem) tys sys of
1610 -- We can't learn anything more about any variable at this point, so the only
1611 -- cause of overlap can be by an instantiation of a touchable unification
1612 -- variable. Hence we only bind touchable unification variables. In addition,
1613 -- we use tcUnifyTys instead of tcMatchTys to rule out cyclic substitutions.
1614 Nothing -> False
1615 Just _ -> True
1616 | otherwise = False -- No overlap with a solved, already been taken care of
1617 -- by the overlap check with the instance environment.
1618 matchable _tys ct = pprPanic "Expecting dictionary!" (ppr ct)
1619
1620 {-
1621 Note [Instance and Given overlap]
1622 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1623 Example, from the OutsideIn(X) paper:
1624 instance P x => Q [x]
1625 instance (x ~ y) => R y [x]
1626
1627 wob :: forall a b. (Q [b], R b a) => a -> Int
1628
1629 g :: forall a. Q [a] => [a] -> Int
1630 g x = wob x
1631
1632 This will generate the impliation constraint:
1633 Q [a] => (Q [beta], R beta [a])
1634 If we react (Q [beta]) with its top-level axiom, we end up with a
1635 (P beta), which we have no way of discharging. On the other hand,
1636 if we react R beta [a] with the top-level we get (beta ~ a), which
1637 is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
1638 now solvable by the given Q [a].
1639
1640 The solution is that:
1641 In matchClassInst (and thus in topReact), we return a matching
1642 instance only when there is no Given in the inerts which is
1643 unifiable to this particular dictionary.
1644
1645 The end effect is that, much as we do for overlapping instances, we delay choosing a
1646 class instance if there is a possibility of another instance OR a given to match our
1647 constraint later on. This fixes bugs #4981 and #5002.
1648
1649 This is arguably not easy to appear in practice due to our aggressive prioritization
1650 of equality solving over other constraints, but it is possible. I've added a test case
1651 in typecheck/should-compile/GivenOverlapping.hs
1652
1653 We ignore the overlap problem if -XIncoherentInstances is in force: see
1654 Trac #6002 for a worked-out example where this makes a difference.
1655
1656 Moreover notice that our goals here are different than the goals of the top-level
1657 overlapping checks. There we are interested in validating the following principle:
1658
1659 If we inline a function f at a site where the same global instance environment
1660 is available as the instance environment at the definition site of f then we
1661 should get the same behaviour.
1662
1663 But for the Given Overlap check our goal is just related to completeness of
1664 constraint solving.
1665 -}