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