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