tc-tracing only
[ghc.git] / compiler / typecheck / TcInteract.hs
1 {-# LANGUAGE CPP #-}
2
3 module TcInteract (
4 solveSimpleGivens, -- Solves [Ct]
5 solveSimpleWanteds, -- Solves Cts
6 ) where
7
8 #include "HsVersions.h"
9
10 import GhcPrelude
11 import BasicTypes ( SwapFlag(..), isSwapped,
12 infinity, IntWithInf, intGtLimit )
13 import TcCanonical
14 import TcFlatten
15 import TcUnify( canSolveByUnification )
16 import VarSet
17 import Type
18 import InstEnv( DFunInstType )
19 import CoAxiom( sfInteractTop, sfInteractInert )
20
21 import Var
22 import TcType
23 import PrelNames ( coercibleTyConKey,
24 heqTyConKey, eqTyConKey, ipClassKey )
25 import CoAxiom ( TypeEqn, CoAxiom(..), CoAxBranch(..), fromBranches )
26 import Class
27 import TyCon
28 import FunDeps
29 import FamInst
30 import ClsInst( ClsInstResult(..), InstanceWhat(..), safeOverlap )
31 import FamInstEnv
32 import Unify ( tcUnifyTyWithTFs, ruleMatchTyKiX )
33
34 import TcEvidence
35 import Outputable
36
37 import TcRnTypes
38 import TcSMonad
39 import Bag
40 import MonadUtils ( concatMapM, foldlM )
41
42 import Data.List( partition, foldl', deleteFirstsBy )
43 import SrcLoc
44 import VarEnv
45
46 import Control.Monad
47 import Maybes( isJust )
48 import Pair (Pair(..))
49 import Unique( hasKey )
50 import DynFlags
51 import Util
52 import qualified GHC.LanguageExtensions as LangExt
53
54 import Control.Monad.Trans.Class
55 import Control.Monad.Trans.Maybe
56
57 {-
58 **********************************************************************
59 * *
60 * Main Interaction Solver *
61 * *
62 **********************************************************************
63
64 Note [Basic Simplifier Plan]
65 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
66 1. Pick an element from the WorkList if there exists one with depth
67 less than our context-stack depth.
68
69 2. Run it down the 'stage' pipeline. Stages are:
70 - canonicalization
71 - inert reactions
72 - spontaneous reactions
73 - top-level intreactions
74 Each stage returns a StopOrContinue and may have sideffected
75 the inerts or worklist.
76
77 The threading of the stages is as follows:
78 - If (Stop) is returned by a stage then we start again from Step 1.
79 - If (ContinueWith ct) is returned by a stage, we feed 'ct' on to
80 the next stage in the pipeline.
81 4. If the element has survived (i.e. ContinueWith x) the last stage
82 then we add him in the inerts and jump back to Step 1.
83
84 If in Step 1 no such element exists, we have exceeded our context-stack
85 depth and will simply fail.
86
87 Note [Unflatten after solving the simple wanteds]
88 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
89 We unflatten after solving the wc_simples of an implication, and before attempting
90 to float. This means that
91
92 * The fsk/fmv flatten-skolems only survive during solveSimples. We don't
93 need to worry about them across successive passes over the constraint tree.
94 (E.g. we don't need the old ic_fsk field of an implication.
95
96 * When floating an equality outwards, we don't need to worry about floating its
97 associated flattening constraints.
98
99 * Another tricky case becomes easy: Trac #4935
100 type instance F True a b = a
101 type instance F False a b = b
102
103 [w] F c a b ~ gamma
104 (c ~ True) => a ~ gamma
105 (c ~ False) => b ~ gamma
106
107 Obviously this is soluble with gamma := F c a b, and unflattening
108 will do exactly that after solving the simple constraints and before
109 attempting the implications. Before, when we were not unflattening,
110 we had to push Wanted funeqs in as new givens. Yuk!
111
112 Another example that becomes easy: indexed_types/should_fail/T7786
113 [W] BuriedUnder sub k Empty ~ fsk
114 [W] Intersect fsk inv ~ s
115 [w] xxx[1] ~ s
116 [W] forall[2] . (xxx[1] ~ Empty)
117 => Intersect (BuriedUnder sub k Empty) inv ~ Empty
118
119 Note [Running plugins on unflattened wanteds]
120 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
121 There is an annoying mismatch between solveSimpleGivens and
122 solveSimpleWanteds, because the latter needs to fiddle with the inert
123 set, unflatten and zonk the wanteds. It passes the zonked wanteds
124 to runTcPluginsWanteds, which produces a replacement set of wanteds,
125 some additional insolubles and a flag indicating whether to go round
126 the loop again. If so, prepareInertsForImplications is used to remove
127 the previous wanteds (which will still be in the inert set). Note
128 that prepareInertsForImplications will discard the insolubles, so we
129 must keep track of them separately.
130 -}
131
132 solveSimpleGivens :: [Ct] -> TcS ()
133 solveSimpleGivens givens
134 | null givens -- Shortcut for common case
135 = return ()
136 | otherwise
137 = do { traceTcS "solveSimpleGivens {" (ppr givens)
138 ; go givens
139 ; traceTcS "End solveSimpleGivens }" empty }
140 where
141 go givens = do { solveSimples (listToBag givens)
142 ; new_givens <- runTcPluginsGiven
143 ; when (notNull new_givens) $
144 go new_givens }
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 -- The result is not necessarily zonked
150 solveSimpleWanteds simples
151 = do { traceTcS "solveSimpleWanteds {" (ppr simples)
152 ; dflags <- getDynFlags
153 ; (n,wc) <- go 1 (solverIterations dflags) (emptyWC { wc_simple = simples })
154 ; traceTcS "solveSimpleWanteds end }" $
155 vcat [ text "iterations =" <+> ppr n
156 , text "residual =" <+> ppr wc ]
157 ; return wc }
158 where
159 go :: Int -> IntWithInf -> WantedConstraints -> TcS (Int, WantedConstraints)
160 go n limit wc
161 | n `intGtLimit` limit
162 = failTcS (hang (text "solveSimpleWanteds: too many iterations"
163 <+> parens (text "limit =" <+> ppr limit))
164 2 (vcat [ text "Set limit with -fconstraint-solver-iterations=n; n=0 for no limit"
165 , text "Simples =" <+> ppr simples
166 , text "WC =" <+> ppr wc ]))
167
168 | isEmptyBag (wc_simple wc)
169 = return (n,wc)
170
171 | otherwise
172 = do { -- Solve
173 (unif_count, wc1) <- solve_simple_wanteds wc
174
175 -- Run plugins
176 ; (rerun_plugin, wc2) <- runTcPluginsWanted wc1
177 -- See Note [Running plugins on unflattened wanteds]
178
179 ; if unif_count == 0 && not rerun_plugin
180 then return (n, wc2) -- Done
181 else do { traceTcS "solveSimple going round again:" $
182 ppr unif_count $$ ppr rerun_plugin
183 ; go (n+1) limit wc2 } } -- Loop
184
185
186 solve_simple_wanteds :: WantedConstraints -> TcS (Int, WantedConstraints)
187 -- Try solving these constraints
188 -- Affects the unification state (of course) but not the inert set
189 -- The result is not necessarily zonked
190 solve_simple_wanteds (WC { wc_simple = simples1, wc_impl = implics1 })
191 = nestTcS $
192 do { solveSimples simples1
193 ; (implics2, tv_eqs, fun_eqs, others) <- getUnsolvedInerts
194 ; (unif_count, unflattened_eqs) <- reportUnifications $
195 unflattenWanteds tv_eqs fun_eqs
196 -- See Note [Unflatten after solving the simple wanteds]
197 ; return ( unif_count
198 , WC { wc_simple = others `andCts` unflattened_eqs
199 , wc_impl = implics1 `unionBags` implics2 }) }
200
201 {- Note [The solveSimpleWanteds loop]
202 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
203 Solving a bunch of simple constraints is done in a loop,
204 (the 'go' loop of 'solveSimpleWanteds'):
205 1. Try to solve them; unflattening may lead to improvement that
206 was not exploitable during solving
207 2. Try the plugin
208 3. If step 1 did improvement during unflattening; or if the plugin
209 wants to run again, go back to step 1
210
211 Non-obviously, improvement can also take place during
212 the unflattening that takes place in step (1). See TcFlatten,
213 See Note [Unflattening can force the solver to iterate]
214 -}
215
216 -- The main solver loop implements Note [Basic Simplifier Plan]
217 ---------------------------------------------------------------
218 solveSimples :: Cts -> TcS ()
219 -- Returns the final InertSet in TcS
220 -- Has no effect on work-list or residual-implications
221 -- The constraints are initially examined in left-to-right order
222
223 solveSimples cts
224 = {-# SCC "solveSimples" #-}
225 do { updWorkListTcS (\wl -> foldrBag extendWorkListCt wl cts)
226 ; solve_loop }
227 where
228 solve_loop
229 = {-# SCC "solve_loop" #-}
230 do { sel <- selectNextWorkItem
231 ; case sel of
232 Nothing -> return ()
233 Just ct -> do { runSolverPipeline thePipeline ct
234 ; solve_loop } }
235
236 -- | Extract the (inert) givens and invoke the plugins on them.
237 -- Remove solved givens from the inert set and emit insolubles, but
238 -- return new work produced so that 'solveSimpleGivens' can feed it back
239 -- into the main solver.
240 runTcPluginsGiven :: TcS [Ct]
241 runTcPluginsGiven
242 = do { plugins <- getTcPlugins
243 ; if null plugins then return [] else
244 do { givens <- getInertGivens
245 ; if null givens then return [] else
246 do { p <- runTcPlugins plugins (givens,[],[])
247 ; let (solved_givens, _, _) = pluginSolvedCts p
248 insols = pluginBadCts p
249 ; updInertCans (removeInertCts solved_givens)
250 ; updInertIrreds (\irreds -> extendCtsList irreds insols)
251 ; return (pluginNewCts p) } } }
252
253 -- | Given a bag of (flattened, zonked) wanteds, invoke the plugins on
254 -- them and produce an updated bag of wanteds (possibly with some new
255 -- work) and a bag of insolubles. The boolean indicates whether
256 -- 'solveSimpleWanteds' should feed the updated wanteds back into the
257 -- main solver.
258 runTcPluginsWanted :: WantedConstraints -> TcS (Bool, WantedConstraints)
259 runTcPluginsWanted wc@(WC { wc_simple = simples1, wc_impl = implics1 })
260 | isEmptyBag simples1
261 = return (False, wc)
262 | otherwise
263 = do { plugins <- getTcPlugins
264 ; if null plugins then return (False, wc) else
265
266 do { given <- getInertGivens
267 ; simples1 <- zonkSimples simples1 -- Plugin requires zonked inputs
268 ; let (wanted, derived) = partition isWantedCt (bagToList simples1)
269 ; p <- runTcPlugins plugins (given, derived, wanted)
270 ; let (_, _, solved_wanted) = pluginSolvedCts p
271 (_, unsolved_derived, unsolved_wanted) = pluginInputCts p
272 new_wanted = pluginNewCts p
273 insols = pluginBadCts p
274
275 -- SLPJ: I'm deeply suspicious of this
276 -- ; updInertCans (removeInertCts $ solved_givens ++ solved_deriveds)
277
278 ; mapM_ setEv solved_wanted
279 ; return ( notNull (pluginNewCts p)
280 , WC { wc_simple = listToBag new_wanted `andCts`
281 listToBag unsolved_wanted `andCts`
282 listToBag unsolved_derived `andCts`
283 listToBag insols
284 , wc_impl = implics1 } ) } }
285 where
286 setEv :: (EvTerm,Ct) -> TcS ()
287 setEv (ev,ct) = case ctEvidence ct of
288 CtWanted { ctev_dest = dest } -> setWantedEvTerm dest ev
289 _ -> panic "runTcPluginsWanted.setEv: attempt to solve non-wanted!"
290
291 -- | A triple of (given, derived, wanted) constraints to pass to plugins
292 type SplitCts = ([Ct], [Ct], [Ct])
293
294 -- | A solved triple of constraints, with evidence for wanteds
295 type SolvedCts = ([Ct], [Ct], [(EvTerm,Ct)])
296
297 -- | Represents collections of constraints generated by typechecker
298 -- plugins
299 data TcPluginProgress = TcPluginProgress
300 { pluginInputCts :: SplitCts
301 -- ^ Original inputs to the plugins with solved/bad constraints
302 -- removed, but otherwise unmodified
303 , pluginSolvedCts :: SolvedCts
304 -- ^ Constraints solved by plugins
305 , pluginBadCts :: [Ct]
306 -- ^ Constraints reported as insoluble by plugins
307 , pluginNewCts :: [Ct]
308 -- ^ New constraints emitted by plugins
309 }
310
311 getTcPlugins :: TcS [TcPluginSolver]
312 getTcPlugins = do { tcg_env <- getGblEnv; return (tcg_tc_plugins tcg_env) }
313
314 -- | Starting from a triple of (given, derived, wanted) constraints,
315 -- invoke each of the typechecker plugins in turn and return
316 --
317 -- * the remaining unmodified constraints,
318 -- * constraints that have been solved,
319 -- * constraints that are insoluble, and
320 -- * new work.
321 --
322 -- Note that new work generated by one plugin will not be seen by
323 -- other plugins on this pass (but the main constraint solver will be
324 -- re-invoked and they will see it later). There is no check that new
325 -- work differs from the original constraints supplied to the plugin:
326 -- the plugin itself should perform this check if necessary.
327 runTcPlugins :: [TcPluginSolver] -> SplitCts -> TcS TcPluginProgress
328 runTcPlugins plugins all_cts
329 = foldM do_plugin initialProgress plugins
330 where
331 do_plugin :: TcPluginProgress -> TcPluginSolver -> TcS TcPluginProgress
332 do_plugin p solver = do
333 result <- runTcPluginTcS (uncurry3 solver (pluginInputCts p))
334 return $ progress p result
335
336 progress :: TcPluginProgress -> TcPluginResult -> TcPluginProgress
337 progress p (TcPluginContradiction bad_cts) =
338 p { pluginInputCts = discard bad_cts (pluginInputCts p)
339 , pluginBadCts = bad_cts ++ pluginBadCts p
340 }
341 progress p (TcPluginOk solved_cts new_cts) =
342 p { pluginInputCts = discard (map snd solved_cts) (pluginInputCts p)
343 , pluginSolvedCts = add solved_cts (pluginSolvedCts p)
344 , pluginNewCts = new_cts ++ pluginNewCts p
345 }
346
347 initialProgress = TcPluginProgress all_cts ([], [], []) [] []
348
349 discard :: [Ct] -> SplitCts -> SplitCts
350 discard cts (xs, ys, zs) =
351 (xs `without` cts, ys `without` cts, zs `without` cts)
352
353 without :: [Ct] -> [Ct] -> [Ct]
354 without = deleteFirstsBy eqCt
355
356 eqCt :: Ct -> Ct -> Bool
357 eqCt c c' = ctFlavour c == ctFlavour c'
358 && ctPred c `tcEqType` ctPred c'
359
360 add :: [(EvTerm,Ct)] -> SolvedCts -> SolvedCts
361 add xs scs = foldl' addOne scs xs
362
363 addOne :: SolvedCts -> (EvTerm,Ct) -> SolvedCts
364 addOne (givens, deriveds, wanteds) (ev,ct) = case ctEvidence ct of
365 CtGiven {} -> (ct:givens, deriveds, wanteds)
366 CtDerived{} -> (givens, ct:deriveds, wanteds)
367 CtWanted {} -> (givens, deriveds, (ev,ct):wanteds)
368
369
370 type WorkItem = Ct
371 type SimplifierStage = WorkItem -> TcS (StopOrContinue Ct)
372
373 runSolverPipeline :: [(String,SimplifierStage)] -- The pipeline
374 -> WorkItem -- The work item
375 -> TcS ()
376 -- Run this item down the pipeline, leaving behind new work and inerts
377 runSolverPipeline pipeline workItem
378 = do { wl <- getWorkList
379 ; inerts <- getTcSInerts
380 ; tclevel <- getTcLevel
381 ; traceTcS "----------------------------- " empty
382 ; traceTcS "Start solver pipeline {" $
383 vcat [ text "tclevel =" <+> ppr tclevel
384 , text "work item =" <+> ppr workItem
385 , text "inerts =" <+> ppr inerts
386 , text "rest of worklist =" <+> ppr wl ]
387
388 ; bumpStepCountTcS -- One step for each constraint processed
389 ; final_res <- run_pipeline pipeline (ContinueWith workItem)
390
391 ; case final_res of
392 Stop ev s -> do { traceFireTcS ev s
393 ; traceTcS "End solver pipeline (discharged) }" empty
394 ; return () }
395 ContinueWith ct -> do { addInertCan ct
396 ; traceFireTcS (ctEvidence ct) (text "Kept as inert")
397 ; traceTcS "End solver pipeline (kept as inert) }" $
398 (text "final_item =" <+> ppr ct) }
399 }
400 where run_pipeline :: [(String,SimplifierStage)] -> StopOrContinue Ct
401 -> TcS (StopOrContinue Ct)
402 run_pipeline [] res = return res
403 run_pipeline _ (Stop ev s) = return (Stop ev s)
404 run_pipeline ((stg_name,stg):stgs) (ContinueWith ct)
405 = do { traceTcS ("runStage " ++ stg_name ++ " {")
406 (text "workitem = " <+> ppr ct)
407 ; res <- stg ct
408 ; traceTcS ("end stage " ++ stg_name ++ " }") empty
409 ; run_pipeline stgs res }
410
411 {-
412 Example 1:
413 Inert: {c ~ d, F a ~ t, b ~ Int, a ~ ty} (all given)
414 Reagent: a ~ [b] (given)
415
416 React with (c~d) ==> IR (ContinueWith (a~[b])) True []
417 React with (F a ~ t) ==> IR (ContinueWith (a~[b])) False [F [b] ~ t]
418 React with (b ~ Int) ==> IR (ContinueWith (a~[Int]) True []
419
420 Example 2:
421 Inert: {c ~w d, F a ~g t, b ~w Int, a ~w ty}
422 Reagent: a ~w [b]
423
424 React with (c ~w d) ==> IR (ContinueWith (a~[b])) True []
425 React with (F a ~g t) ==> IR (ContinueWith (a~[b])) True [] (can't rewrite given with wanted!)
426 etc.
427
428 Example 3:
429 Inert: {a ~ Int, F Int ~ b} (given)
430 Reagent: F a ~ b (wanted)
431
432 React with (a ~ Int) ==> IR (ContinueWith (F Int ~ b)) True []
433 React with (F Int ~ b) ==> IR Stop True [] -- after substituting we re-canonicalize and get nothing
434 -}
435
436 thePipeline :: [(String,SimplifierStage)]
437 thePipeline = [ ("canonicalization", TcCanonical.canonicalize)
438 , ("interact with inerts", interactWithInertsStage)
439 , ("top-level reactions", topReactionsStage) ]
440
441 {-
442 *********************************************************************************
443 * *
444 The interact-with-inert Stage
445 * *
446 *********************************************************************************
447
448 Note [The Solver Invariant]
449 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
450 We always add Givens first. So you might think that the solver has
451 the invariant
452
453 If the work-item is Given,
454 then the inert item must Given
455
456 But this isn't quite true. Suppose we have,
457 c1: [W] beta ~ [alpha], c2 : [W] blah, c3 :[W] alpha ~ Int
458 After processing the first two, we get
459 c1: [G] beta ~ [alpha], c2 : [W] blah
460 Now, c3 does not interact with the given c1, so when we spontaneously
461 solve c3, we must re-react it with the inert set. So we can attempt a
462 reaction between inert c2 [W] and work-item c3 [G].
463
464 It *is* true that [Solver Invariant]
465 If the work-item is Given,
466 AND there is a reaction
467 then the inert item must Given
468 or, equivalently,
469 If the work-item is Given,
470 and the inert item is Wanted/Derived
471 then there is no reaction
472 -}
473
474 -- Interaction result of WorkItem <~> Ct
475
476 interactWithInertsStage :: WorkItem -> TcS (StopOrContinue Ct)
477 -- Precondition: if the workitem is a CTyEqCan then it will not be able to
478 -- react with anything at this stage.
479
480 interactWithInertsStage wi
481 = do { inerts <- getTcSInerts
482 ; let ics = inert_cans inerts
483 ; case wi of
484 CTyEqCan {} -> interactTyVarEq ics wi
485 CFunEqCan {} -> interactFunEq ics wi
486 CIrredCan {} -> interactIrred ics wi
487 CDictCan {} -> interactDict ics wi
488 _ -> pprPanic "interactWithInerts" (ppr wi) }
489 -- CHoleCan are put straight into inert_frozen, so never get here
490 -- CNonCanonical have been canonicalised
491
492 data InteractResult
493 = KeepInert -- Keep the inert item, and solve the work item from it
494 -- (if the latter is Wanted; just discard it if not)
495 | KeepWork -- Keep the work item, and solve the intert item from it
496
497 instance Outputable InteractResult where
498 ppr KeepInert = text "keep inert"
499 ppr KeepWork = text "keep work-item"
500
501 solveOneFromTheOther :: CtEvidence -- Inert
502 -> CtEvidence -- WorkItem
503 -> TcS InteractResult
504 -- Precondition:
505 -- * inert and work item represent evidence for the /same/ predicate
506 --
507 -- We can always solve one from the other: even if both are wanted,
508 -- although we don't rewrite wanteds with wanteds, we can combine
509 -- two wanteds into one by solving one from the other
510
511 solveOneFromTheOther ev_i ev_w
512 | isDerived ev_w -- Work item is Derived; just discard it
513 = return KeepInert
514
515 | isDerived ev_i -- The inert item is Derived, we can just throw it away,
516 = return KeepWork -- The ev_w is inert wrt earlier inert-set items,
517 -- so it's safe to continue on from this point
518
519 | CtWanted { ctev_loc = loc_w } <- ev_w
520 , prohibitedSuperClassSolve (ctEvLoc ev_i) loc_w
521 = -- inert must be Given
522 do { traceTcS "prohibitedClassSolve1" (ppr ev_i $$ ppr ev_w)
523 ; return KeepWork }
524
525 | CtWanted {} <- ev_w
526 -- Inert is Given or Wanted
527 = return KeepInert
528
529 -- From here on the work-item is Given
530
531 | CtWanted { ctev_loc = loc_i } <- ev_i
532 , prohibitedSuperClassSolve (ctEvLoc ev_w) loc_i
533 = do { traceTcS "prohibitedClassSolve2" (ppr ev_i $$ ppr ev_w)
534 ; return KeepInert } -- Just discard the un-usable Given
535 -- This never actually happens because
536 -- Givens get processed first
537
538 | CtWanted {} <- ev_i
539 = return KeepWork
540
541 -- From here on both are Given
542 -- See Note [Replacement vs keeping]
543
544 | lvl_i == lvl_w
545 = do { ev_binds_var <- getTcEvBindsVar
546 ; binds <- getTcEvBindsMap ev_binds_var
547 ; return (same_level_strategy binds) }
548
549 | otherwise -- Both are Given, levels differ
550 = return different_level_strategy
551 where
552 pred = ctEvPred ev_i
553 loc_i = ctEvLoc ev_i
554 loc_w = ctEvLoc ev_w
555 lvl_i = ctLocLevel loc_i
556 lvl_w = ctLocLevel loc_w
557 ev_id_i = ctEvEvId ev_i
558 ev_id_w = ctEvEvId ev_w
559
560 different_level_strategy -- Both Given
561 | isIPPred pred, lvl_w > lvl_i = KeepWork
562 | lvl_w < lvl_i = KeepWork
563 | otherwise = KeepInert
564
565 same_level_strategy binds -- Both Given
566 | GivenOrigin (InstSC s_i) <- ctLocOrigin loc_i
567 = case ctLocOrigin loc_w of
568 GivenOrigin (InstSC s_w) | s_w < s_i -> KeepWork
569 | otherwise -> KeepInert
570 _ -> KeepWork
571
572 | GivenOrigin (InstSC {}) <- ctLocOrigin loc_w
573 = KeepInert
574
575 | has_binding binds ev_id_w
576 , not (has_binding binds ev_id_i)
577 , not (ev_id_i `elemVarSet` findNeededEvVars binds (unitVarSet ev_id_w))
578 = KeepWork
579
580 | otherwise
581 = KeepInert
582
583 has_binding binds ev_id = isJust (lookupEvBind binds ev_id)
584
585 {-
586 Note [Replacement vs keeping]
587 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
588 When we have two Given constraints both of type (C tys), say, which should
589 we keep? More subtle than you might think!
590
591 * Constraints come from different levels (different_level_strategy)
592
593 - For implicit parameters we want to keep the innermost (deepest)
594 one, so that it overrides the outer one.
595 See Note [Shadowing of Implicit Parameters]
596
597 - For everything else, we want to keep the outermost one. Reason: that
598 makes it more likely that the inner one will turn out to be unused,
599 and can be reported as redundant. See Note [Tracking redundant constraints]
600 in TcSimplify.
601
602 It transpires that using the outermost one is reponsible for an
603 8% performance improvement in nofib cryptarithm2, compared to
604 just rolling the dice. I didn't investigate why.
605
606 * Constraints coming from the same level (i.e. same implication)
607
608 (a) Always get rid of InstSC ones if possible, since they are less
609 useful for solving. If both are InstSC, choose the one with
610 the smallest TypeSize
611 See Note [Solving superclass constraints] in TcInstDcls
612
613 (b) Keep the one that has a non-trivial evidence binding.
614 Example: f :: (Eq a, Ord a) => blah
615 then we may find [G] d3 :: Eq a
616 [G] d2 :: Eq a
617 with bindings d3 = sc_sel (d1::Ord a)
618 We want to discard d2 in favour of the superclass selection from
619 the Ord dictionary.
620 Why? See Note [Tracking redundant constraints] in TcSimplify again.
621
622 (c) But don't do (b) if the evidence binding depends transitively on the
623 one without a binding. Example (with RecursiveSuperClasses)
624 class C a => D a
625 class D a => C a
626 Inert: d1 :: C a, d2 :: D a
627 Binds: d3 = sc_sel d2, d2 = sc_sel d1
628 Work item: d3 :: C a
629 Then it'd be ridiculous to replace d1 with d3 in the inert set!
630 Hence the findNeedEvVars test. See Trac #14774.
631
632 * Finally, when there is still a choice, use KeepInert rather than
633 KeepWork, for two reasons:
634 - to avoid unnecessary munging of the inert set.
635 - to cut off superclass loops; see Note [Superclass loops] in TcCanonical
636
637 Doing the depth-check for implicit parameters, rather than making the work item
638 always override, is important. Consider
639
640 data T a where { T1 :: (?x::Int) => T Int; T2 :: T a }
641
642 f :: (?x::a) => T a -> Int
643 f T1 = ?x
644 f T2 = 3
645
646 We have a [G] (?x::a) in the inert set, and at the pattern match on T1 we add
647 two new givens in the work-list: [G] (?x::Int)
648 [G] (a ~ Int)
649 Now consider these steps
650 - process a~Int, kicking out (?x::a)
651 - process (?x::Int), the inner given, adding to inert set
652 - process (?x::a), the outer given, overriding the inner given
653 Wrong! The depth-check ensures that the inner implicit parameter wins.
654 (Actually I think that the order in which the work-list is processed means
655 that this chain of events won't happen, but that's very fragile.)
656
657 *********************************************************************************
658 * *
659 interactIrred
660 * *
661 *********************************************************************************
662
663 Note [Multiple matching irreds]
664 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
665 You might think that it's impossible to have multiple irreds all match the
666 work item; after all, interactIrred looks for matches and solves one from the
667 other. However, note that interacting insoluble, non-droppable irreds does not
668 do this matching. We thus might end up with several insoluble, non-droppable,
669 matching irreds in the inert set. When another irred comes along that we have
670 not yet labeled insoluble, we can find multiple matches. These multiple matches
671 cause no harm, but it would be wrong to ASSERT that they aren't there (as we
672 once had done). This problem can be tickled by typecheck/should_compile/holes.
673
674 -}
675
676 -- Two pieces of irreducible evidence: if their types are *exactly identical*
677 -- we can rewrite them. We can never improve using this:
678 -- if we want ty1 :: Constraint and have ty2 :: Constraint it clearly does not
679 -- mean that (ty1 ~ ty2)
680 interactIrred :: InertCans -> Ct -> TcS (StopOrContinue Ct)
681
682 interactIrred inerts workItem@(CIrredCan { cc_ev = ev_w, cc_insol = insoluble })
683 | insoluble -- For insolubles, don't allow the constaint to be dropped
684 -- which can happen with solveOneFromTheOther, so that
685 -- we get distinct error messages with -fdefer-type-errors
686 -- See Note [Do not add duplicate derived insolubles]
687 , not (isDroppableCt workItem)
688 = continueWith workItem
689
690 | let (matching_irreds, others) = findMatchingIrreds (inert_irreds inerts) ev_w
691 , ((ct_i, swap) : _rest) <- bagToList matching_irreds
692 -- See Note [Multiple matching irreds]
693 , let ev_i = ctEvidence ct_i
694 = do { what_next <- solveOneFromTheOther ev_i ev_w
695 ; traceTcS "iteractIrred" (ppr workItem $$ ppr what_next $$ ppr ct_i)
696 ; case what_next of
697 KeepInert -> do { setEvBindIfWanted ev_w (swap_me swap ev_i)
698 ; return (Stop ev_w (text "Irred equal" <+> parens (ppr what_next))) }
699 KeepWork -> do { setEvBindIfWanted ev_i (swap_me swap ev_w)
700 ; updInertIrreds (\_ -> others)
701 ; continueWith workItem } }
702
703 | otherwise
704 = continueWith workItem
705
706 where
707 swap_me :: SwapFlag -> CtEvidence -> EvTerm
708 swap_me swap ev
709 = case swap of
710 NotSwapped -> ctEvTerm ev
711 IsSwapped -> evCoercion (mkTcSymCo (evTermCoercion (ctEvTerm ev)))
712
713 interactIrred _ wi = pprPanic "interactIrred" (ppr wi)
714
715 findMatchingIrreds :: Cts -> CtEvidence -> (Bag (Ct, SwapFlag), Bag Ct)
716 findMatchingIrreds irreds ev
717 | EqPred eq_rel1 lty1 rty1 <- classifyPredType pred
718 -- See Note [Solving irreducible equalities]
719 = partitionBagWith (match_eq eq_rel1 lty1 rty1) irreds
720 | otherwise
721 = partitionBagWith match_non_eq irreds
722 where
723 pred = ctEvPred ev
724 match_non_eq ct
725 | ctPred ct `tcEqTypeNoKindCheck` pred = Left (ct, NotSwapped)
726 | otherwise = Right ct
727
728 match_eq eq_rel1 lty1 rty1 ct
729 | EqPred eq_rel2 lty2 rty2 <- classifyPredType (ctPred ct)
730 , eq_rel1 == eq_rel2
731 , Just swap <- match_eq_help lty1 rty1 lty2 rty2
732 = Left (ct, swap)
733 | otherwise
734 = Right ct
735
736 match_eq_help lty1 rty1 lty2 rty2
737 | lty1 `tcEqTypeNoKindCheck` lty2, rty1 `tcEqTypeNoKindCheck` rty2
738 = Just NotSwapped
739 | lty1 `tcEqTypeNoKindCheck` rty2, rty1 `tcEqTypeNoKindCheck` lty2
740 = Just IsSwapped
741 | otherwise
742 = Nothing
743
744 {- Note [Solving irreducible equalities]
745 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
746 Consider (Trac #14333)
747 [G] a b ~R# c d
748 [W] c d ~R# a b
749 Clearly we should be able to solve this! Even though the constraints are
750 not decomposable. We solve this when looking up the work-item in the
751 irreducible constraints to look for an identical one. When doing this
752 lookup, findMatchingIrreds spots the equality case, and matches either
753 way around. It has to return a swap-flag so we can generate evidence
754 that is the right way round too.
755
756 Note [Do not add duplicate derived insolubles]
757 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
758 In general we *must* add an insoluble (Int ~ Bool) even if there is
759 one such there already, because they may come from distinct call
760 sites. Not only do we want an error message for each, but with
761 -fdefer-type-errors we must generate evidence for each. But for
762 *derived* insolubles, we only want to report each one once. Why?
763
764 (a) A constraint (C r s t) where r -> s, say, may generate the same fundep
765 equality many times, as the original constraint is successively rewritten.
766
767 (b) Ditto the successive iterations of the main solver itself, as it traverses
768 the constraint tree. See example below.
769
770 Also for *given* insolubles we may get repeated errors, as we
771 repeatedly traverse the constraint tree. These are relatively rare
772 anyway, so removing duplicates seems ok. (Alternatively we could take
773 the SrcLoc into account.)
774
775 Note that the test does not need to be particularly efficient because
776 it is only used if the program has a type error anyway.
777
778 Example of (b): assume a top-level class and instance declaration:
779
780 class D a b | a -> b
781 instance D [a] [a]
782
783 Assume we have started with an implication:
784
785 forall c. Eq c => { wc_simple = D [c] c [W] }
786
787 which we have simplified to:
788
789 forall c. Eq c => { wc_simple = D [c] c [W]
790 (c ~ [c]) [D] }
791
792 For some reason, e.g. because we floated an equality somewhere else,
793 we might try to re-solve this implication. If we do not do a
794 dropDerivedWC, then we will end up trying to solve the following
795 constraints the second time:
796
797 (D [c] c) [W]
798 (c ~ [c]) [D]
799
800 which will result in two Deriveds to end up in the insoluble set:
801
802 wc_simple = D [c] c [W]
803 (c ~ [c]) [D], (c ~ [c]) [D]
804 -}
805
806 {-
807 *********************************************************************************
808 * *
809 interactDict
810 * *
811 *********************************************************************************
812
813 Note [Shortcut solving]
814 ~~~~~~~~~~~~~~~~~~~~~~~
815 When we interact a [W] constraint with a [G] constraint that solves it, there is
816 a possibility that we could produce better code if instead we solved from a
817 top-level instance declaration (See #12791, #5835). For example:
818
819 class M a b where m :: a -> b
820
821 type C a b = (Num a, M a b)
822
823 f :: C Int b => b -> Int -> Int
824 f _ x = x + 1
825
826 The body of `f` requires a [W] `Num Int` instance. We could solve this
827 constraint from the givens because we have `C Int b` and that provides us a
828 solution for `Num Int`. This would let us produce core like the following
829 (with -O2):
830
831 f :: forall b. C Int b => b -> Int -> Int
832 f = \ (@ b) ($d(%,%) :: C Int b) _ (eta1 :: Int) ->
833 + @ Int
834 (GHC.Classes.$p1(%,%) @ (Num Int) @ (M Int b) $d(%,%))
835 eta1
836 A.f1
837
838 This is bad! We could do /much/ better if we solved [W] `Num Int` directly
839 from the instance that we have in scope:
840
841 f :: forall b. C Int b => b -> Int -> Int
842 f = \ (@ b) _ _ (x :: Int) ->
843 case x of { GHC.Types.I# x1 -> GHC.Types.I# (GHC.Prim.+# x1 1#) }
844
845 ** NB: It is important to emphasize that all this is purely an optimization:
846 ** exactly the same programs should typecheck with or without this
847 ** procedure.
848
849 Solving fully
850 ~~~~~~~~~~~~~
851 There is a reason why the solver does not simply try to solve such
852 constraints with top-level instances. If the solver finds a relevant
853 instance declaration in scope, that instance may require a context
854 that can't be solved for. A good example of this is:
855
856 f :: Ord [a] => ...
857 f x = ..Need Eq [a]...
858
859 If we have instance `Eq a => Eq [a]` in scope and we tried to use it, we would
860 be left with the obligation to solve the constraint Eq a, which we cannot. So we
861 must be conservative in our attempt to use an instance declaration to solve the
862 [W] constraint we're interested in.
863
864 Our rule is that we try to solve all of the instance's subgoals
865 recursively all at once. Precisely: We only attempt to solve
866 constraints of the form `C1, ... Cm => C t1 ... t n`, where all the Ci
867 are themselves class constraints of the form `C1', ... Cm' => C' t1'
868 ... tn'` and we only succeed if the entire tree of constraints is
869 solvable from instances.
870
871 An example that succeeds:
872
873 class Eq a => C a b | b -> a where
874 m :: b -> a
875
876 f :: C [Int] b => b -> Bool
877 f x = m x == []
878
879 We solve for `Eq [Int]`, which requires `Eq Int`, which we also have. This
880 produces the following core:
881
882 f :: forall b. C [Int] b => b -> Bool
883 f = \ (@ b) ($dC :: C [Int] b) (x :: b) ->
884 GHC.Classes.$fEq[]_$s$c==
885 (m @ [Int] @ b $dC x) (GHC.Types.[] @ Int)
886
887 An example that fails:
888
889 class Eq a => C a b | b -> a where
890 m :: b -> a
891
892 f :: C [a] b => b -> Bool
893 f x = m x == []
894
895 Which, because solving `Eq [a]` demands `Eq a` which we cannot solve, produces:
896
897 f :: forall a b. C [a] b => b -> Bool
898 f = \ (@ a) (@ b) ($dC :: C [a] b) (eta :: b) ->
899 ==
900 @ [a]
901 (A.$p1C @ [a] @ b $dC)
902 (m @ [a] @ b $dC eta)
903 (GHC.Types.[] @ a)
904
905 Note [Shortcut solving: type families]
906 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
907 Suppose we have (Trac #13943)
908 class Take (n :: Nat) where ...
909 instance {-# OVERLAPPING #-} Take 0 where ..
910 instance {-# OVERLAPPABLE #-} (Take (n - 1)) => Take n where ..
911
912 And we have [W] Take 3. That only matches one instance so we get
913 [W] Take (3-1). Really we should now flatten to reduce the (3-1) to 2, and
914 so on -- but that is reproducing yet more of the solver. Sigh. For now,
915 we just give up (remember all this is just an optimisation).
916
917 But we must not just naively try to lookup (Take (3-1)) in the
918 InstEnv, or it'll (wrongly) appear not to match (Take 0) and get a
919 unique match on the (Take n) instance. That leads immediately to an
920 infinite loop. Hence the check that 'preds' have no type families
921 (isTyFamFree).
922
923 Note [Shortcut solving: overlap]
924 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
925 Suppose we have
926 instance {-# OVERLAPPABLE #-} C a where ...
927 and we are typechecking
928 f :: C a => a -> a
929 f = e -- Gives rise to [W] C a
930
931 We don't want to solve the wanted constraint with the overlappable
932 instance; rather we want to use the supplied (C a)! That was the whole
933 point of it being overlappable! Trac #14434 wwas an example.
934
935 Note [Shortcut solving: incoherence]
936 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
937 This optimization relies on coherence of dictionaries to be correct. When we
938 cannot assume coherence because of IncoherentInstances then this optimization
939 can change the behavior of the user's code.
940
941 The following four modules produce a program whose output would change depending
942 on whether we apply this optimization when IncoherentInstances is in effect:
943
944 #########
945 {-# LANGUAGE MultiParamTypeClasses #-}
946 module A where
947
948 class A a where
949 int :: a -> Int
950
951 class A a => C a b where
952 m :: b -> a -> a
953
954 #########
955 {-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
956 module B where
957
958 import A
959
960 instance A a where
961 int _ = 1
962
963 instance C a [b] where
964 m _ = id
965
966 #########
967 {-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, FlexibleContexts #-}
968 {-# LANGUAGE IncoherentInstances #-}
969 module C where
970
971 import A
972
973 instance A Int where
974 int _ = 2
975
976 instance C Int [Int] where
977 m _ = id
978
979 intC :: C Int a => a -> Int -> Int
980 intC _ x = int x
981
982 #########
983 module Main where
984
985 import A
986 import B
987 import C
988
989 main :: IO ()
990 main = print (intC [] (0::Int))
991
992 The output of `main` if we avoid the optimization under the effect of
993 IncoherentInstances is `1`. If we were to do the optimization, the output of
994 `main` would be `2`.
995
996 Note [Shortcut try_solve_from_instance]
997 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
998 The workhorse of the short-cut solver is
999 try_solve_from_instance :: (EvBindMap, DictMap CtEvidence)
1000 -> CtEvidence -- Solve this
1001 -> MaybeT TcS (EvBindMap, DictMap CtEvidence)
1002 Note that:
1003
1004 * The CtEvidence is teh goal to be solved
1005
1006 * The MaybeT anages early failure if we find a subgoal that
1007 cannot be solved from instances.
1008
1009 * The (EvBindMap, DictMap CtEvidence) is an accumulating purely-functional
1010 state that allows try_solve_from_instance to augmennt the evidence
1011 bindings and inert_solved_dicts as it goes.
1012
1013 If it succeeds, we commit all these bindings and solved dicts to the
1014 main TcS InertSet. If not, we abandon it all entirely.
1015
1016 Passing along the solved_dicts important for two reasons:
1017
1018 * We need to be able to handle recursive super classes. The
1019 solved_dicts state ensures that we remember what we have already
1020 tried to solve to avoid looping.
1021
1022 * As Trac #15164 showed, it can be important to exploit sharing between
1023 goals. E.g. To solve G we may need G1 and G2. To solve G1 we may need H;
1024 and to solve G2 we may need H. If we don't spot this sharing we may
1025 solve H twice; and if this pattern repeats we may get exponentially bad
1026 behaviour.
1027 -}
1028
1029 interactDict :: InertCans -> Ct -> TcS (StopOrContinue Ct)
1030 interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs = tys })
1031 | Just ev_i <- lookupInertDict inerts (ctEvLoc ev_w) cls tys
1032 = -- There is a matching dictionary in the inert set
1033 do { -- First to try to solve it /completely/ from top level instances
1034 -- See Note [Shortcut solving]
1035 dflags <- getDynFlags
1036 ; short_cut_worked <- shortCutSolver dflags ev_w ev_i
1037 ; if short_cut_worked
1038 then stopWith ev_w "interactDict/solved from instance"
1039 else
1040
1041 do { -- Ths short-cut solver didn't fire, so we
1042 -- solve ev_w from the matching inert ev_i we found
1043 what_next <- solveOneFromTheOther ev_i ev_w
1044 ; traceTcS "lookupInertDict" (ppr what_next)
1045 ; case what_next of
1046 KeepInert -> do { setEvBindIfWanted ev_w (ctEvTerm ev_i)
1047 ; return $ Stop ev_w (text "Dict equal" <+> parens (ppr what_next)) }
1048 KeepWork -> do { setEvBindIfWanted ev_i (ctEvTerm ev_w)
1049 ; updInertDicts $ \ ds -> delDict ds cls tys
1050 ; continueWith workItem } } }
1051
1052 | cls `hasKey` ipClassKey
1053 , isGiven ev_w
1054 = interactGivenIP inerts workItem
1055
1056 | otherwise
1057 = do { addFunDepWork inerts ev_w cls
1058 ; continueWith workItem }
1059
1060 interactDict _ wi = pprPanic "interactDict" (ppr wi)
1061
1062 -- See Note [Shortcut solving]
1063 shortCutSolver :: DynFlags
1064 -> CtEvidence -- Work item
1065 -> CtEvidence -- Inert we want to try to replace
1066 -> TcS Bool -- True <=> success
1067 shortCutSolver dflags ev_w ev_i
1068 | isWanted ev_w
1069 && isGiven ev_i
1070 -- We are about to solve a [W] constraint from a [G] constraint. We take
1071 -- a moment to see if we can get a better solution using an instance.
1072 -- Note that we only do this for the sake of performance. Exactly the same
1073 -- programs should typecheck regardless of whether we take this step or
1074 -- not. See Note [Shortcut solving]
1075
1076 && not (xopt LangExt.IncoherentInstances dflags)
1077 -- If IncoherentInstances is on then we cannot rely on coherence of proofs
1078 -- in order to justify this optimization: The proof provided by the
1079 -- [G] constraint's superclass may be different from the top-level proof.
1080 -- See Note [Shortcut solving: incoherence]
1081
1082 && gopt Opt_SolveConstantDicts dflags
1083 -- Enabled by the -fsolve-constant-dicts flag
1084 = do { ev_binds_var <- getTcEvBindsVar
1085 ; ev_binds <- ASSERT2( not (isCoEvBindsVar ev_binds_var ), ppr ev_w )
1086 getTcEvBindsMap ev_binds_var
1087 ; solved_dicts <- getSolvedDicts
1088
1089 ; mb_stuff <- runMaybeT $ try_solve_from_instance
1090 (ev_binds, solved_dicts) ev_w
1091
1092 ; case mb_stuff of
1093 Nothing -> return False
1094 Just (ev_binds', solved_dicts')
1095 -> do { setTcEvBindsMap ev_binds_var ev_binds'
1096 ; setSolvedDicts solved_dicts'
1097 ; return True } }
1098
1099 | otherwise
1100 = return False
1101 where
1102 -- This `CtLoc` is used only to check the well-staged condition of any
1103 -- candidate DFun. Our subgoals all have the same stage as our root
1104 -- [W] constraint so it is safe to use this while solving them.
1105 loc_w = ctEvLoc ev_w
1106
1107 try_solve_from_instance -- See Note [Shortcut try_solve_from_instance]
1108 :: (EvBindMap, DictMap CtEvidence) -> CtEvidence
1109 -> MaybeT TcS (EvBindMap, DictMap CtEvidence)
1110 try_solve_from_instance (ev_binds, solved_dicts) ev
1111 | let pred = ctEvPred ev
1112 loc = ctEvLoc ev
1113 , ClassPred cls tys <- classifyPredType pred
1114 = do { inst_res <- lift $ matchGlobalInst dflags True cls tys
1115 ; case inst_res of
1116 OneInst { cir_new_theta = preds
1117 , cir_mk_ev = mk_ev
1118 , cir_what = what }
1119 | safeOverlap what
1120 , all isTyFamFree preds -- Note [Shortcut solving: type families]
1121 -> do { let solved_dicts' = addDict solved_dicts cls tys ev
1122 -- solved_dicts': it is important that we add our goal
1123 -- to the cache before we solve! Otherwise we may end
1124 -- up in a loop while solving recursive dictionaries.
1125
1126 ; lift $ traceTcS "shortCutSolver: found instance" (ppr preds)
1127 ; loc' <- lift $ checkInstanceOK loc what pred
1128
1129 ; evc_vs <- mapM (new_wanted_cached loc' solved_dicts') preds
1130 -- Emit work for subgoals but use our local cache
1131 -- so we can solve recursive dictionaries.
1132
1133 ; let ev_tm = mk_ev (map getEvExpr evc_vs)
1134 ev_binds' = extendEvBinds ev_binds $
1135 mkWantedEvBind (ctEvEvId ev) ev_tm
1136
1137 ; foldlM try_solve_from_instance
1138 (ev_binds', solved_dicts')
1139 (freshGoals evc_vs) }
1140
1141 _ -> mzero }
1142 | otherwise = mzero
1143
1144
1145 -- Use a local cache of solved dicts while emitting EvVars for new work
1146 -- We bail out of the entire computation if we need to emit an EvVar for
1147 -- a subgoal that isn't a ClassPred.
1148 new_wanted_cached :: CtLoc -> DictMap CtEvidence -> TcPredType -> MaybeT TcS MaybeNew
1149 new_wanted_cached loc cache pty
1150 | ClassPred cls tys <- classifyPredType pty
1151 = lift $ case findDict cache loc_w cls tys of
1152 Just ctev -> return $ Cached (ctEvExpr ctev)
1153 Nothing -> Fresh <$> newWantedNC loc pty
1154 | otherwise = mzero
1155
1156 addFunDepWork :: InertCans -> CtEvidence -> Class -> TcS ()
1157 -- Add derived constraints from type-class functional dependencies.
1158 addFunDepWork inerts work_ev cls
1159 | isImprovable work_ev
1160 = mapBagM_ add_fds (findDictsByClass (inert_dicts inerts) cls)
1161 -- No need to check flavour; fundeps work between
1162 -- any pair of constraints, regardless of flavour
1163 -- Importantly we don't throw workitem back in the
1164 -- worklist because this can cause loops (see #5236)
1165 | otherwise
1166 = return ()
1167 where
1168 work_pred = ctEvPred work_ev
1169 work_loc = ctEvLoc work_ev
1170
1171 add_fds inert_ct
1172 | isImprovable inert_ev
1173 = do { traceTcS "addFunDepWork" (vcat
1174 [ ppr work_ev
1175 , pprCtLoc work_loc, ppr (isGivenLoc work_loc)
1176 , pprCtLoc inert_loc, ppr (isGivenLoc inert_loc)
1177 , pprCtLoc derived_loc, ppr (isGivenLoc derived_loc) ]) ;
1178
1179 emitFunDepDeriveds $
1180 improveFromAnother derived_loc inert_pred work_pred
1181 -- We don't really rewrite tys2, see below _rewritten_tys2, so that's ok
1182 -- NB: We do create FDs for given to report insoluble equations that arise
1183 -- from pairs of Givens, and also because of floating when we approximate
1184 -- implications. The relevant test is: typecheck/should_fail/FDsFromGivens.hs
1185 }
1186 | otherwise
1187 = return ()
1188 where
1189 inert_ev = ctEvidence inert_ct
1190 inert_pred = ctEvPred inert_ev
1191 inert_loc = ctEvLoc inert_ev
1192 derived_loc = work_loc { ctl_depth = ctl_depth work_loc `maxSubGoalDepth`
1193 ctl_depth inert_loc
1194 , ctl_origin = FunDepOrigin1 work_pred work_loc
1195 inert_pred inert_loc }
1196
1197 {-
1198 **********************************************************************
1199 * *
1200 Implicit parameters
1201 * *
1202 **********************************************************************
1203 -}
1204
1205 interactGivenIP :: InertCans -> Ct -> TcS (StopOrContinue Ct)
1206 -- Work item is Given (?x:ty)
1207 -- See Note [Shadowing of Implicit Parameters]
1208 interactGivenIP inerts workItem@(CDictCan { cc_ev = ev, cc_class = cls
1209 , cc_tyargs = tys@(ip_str:_) })
1210 = do { updInertCans $ \cans -> cans { inert_dicts = addDict filtered_dicts cls tys workItem }
1211 ; stopWith ev "Given IP" }
1212 where
1213 dicts = inert_dicts inerts
1214 ip_dicts = findDictsByClass dicts cls
1215 other_ip_dicts = filterBag (not . is_this_ip) ip_dicts
1216 filtered_dicts = addDictsByClass dicts cls other_ip_dicts
1217
1218 -- Pick out any Given constraints for the same implicit parameter
1219 is_this_ip (CDictCan { cc_ev = ev, cc_tyargs = ip_str':_ })
1220 = isGiven ev && ip_str `tcEqType` ip_str'
1221 is_this_ip _ = False
1222
1223 interactGivenIP _ wi = pprPanic "interactGivenIP" (ppr wi)
1224
1225 {- Note [Shadowing of Implicit Parameters]
1226 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1227 Consider the following example:
1228
1229 f :: (?x :: Char) => Char
1230 f = let ?x = 'a' in ?x
1231
1232 The "let ?x = ..." generates an implication constraint of the form:
1233
1234 ?x :: Char => ?x :: Char
1235
1236 Furthermore, the signature for `f` also generates an implication
1237 constraint, so we end up with the following nested implication:
1238
1239 ?x :: Char => (?x :: Char => ?x :: Char)
1240
1241 Note that the wanted (?x :: Char) constraint may be solved in
1242 two incompatible ways: either by using the parameter from the
1243 signature, or by using the local definition. Our intention is
1244 that the local definition should "shadow" the parameter of the
1245 signature, and we implement this as follows: when we add a new
1246 *given* implicit parameter to the inert set, it replaces any existing
1247 givens for the same implicit parameter.
1248
1249 Similarly, consider
1250 f :: (?x::a) => Bool -> a
1251
1252 g v = let ?x::Int = 3
1253 in (f v, let ?x::Bool = True in f v)
1254
1255 This should probably be well typed, with
1256 g :: Bool -> (Int, Bool)
1257
1258 So the inner binding for ?x::Bool *overrides* the outer one.
1259
1260 All this works for the normal cases but it has an odd side effect in
1261 some pathological programs like this:
1262 -- This is accepted, the second parameter shadows
1263 f1 :: (?x :: Int, ?x :: Char) => Char
1264 f1 = ?x
1265
1266 -- This is rejected, the second parameter shadows
1267 f2 :: (?x :: Int, ?x :: Char) => Int
1268 f2 = ?x
1269
1270 Both of these are actually wrong: when we try to use either one,
1271 we'll get two incompatible wanted constraints (?x :: Int, ?x :: Char),
1272 which would lead to an error.
1273
1274 I can think of two ways to fix this:
1275
1276 1. Simply disallow multiple constraints for the same implicit
1277 parameter---this is never useful, and it can be detected completely
1278 syntactically.
1279
1280 2. Move the shadowing machinery to the location where we nest
1281 implications, and add some code here that will produce an
1282 error if we get multiple givens for the same implicit parameter.
1283
1284
1285 **********************************************************************
1286 * *
1287 interactFunEq
1288 * *
1289 **********************************************************************
1290 -}
1291
1292 interactFunEq :: InertCans -> Ct -> TcS (StopOrContinue Ct)
1293 -- Try interacting the work item with the inert set
1294 interactFunEq inerts work_item@(CFunEqCan { cc_ev = ev, cc_fun = tc
1295 , cc_tyargs = args, cc_fsk = fsk })
1296 | Just inert_ct@(CFunEqCan { cc_ev = ev_i
1297 , cc_fsk = fsk_i })
1298 <- findFunEq (inert_funeqs inerts) tc args
1299 , pr@(swap_flag, upgrade_flag) <- ev_i `funEqCanDischarge` ev
1300 = do { traceTcS "reactFunEq (rewrite inert item):" $
1301 vcat [ text "work_item =" <+> ppr work_item
1302 , text "inertItem=" <+> ppr ev_i
1303 , text "(swap_flag, upgrade)" <+> ppr pr ]
1304 ; if isSwapped swap_flag
1305 then do { -- Rewrite inert using work-item
1306 let work_item' | upgrade_flag = upgradeWanted work_item
1307 | otherwise = work_item
1308 ; updInertFunEqs $ \ feqs -> insertFunEq feqs tc args work_item'
1309 -- Do the updInertFunEqs before the reactFunEq, so that
1310 -- we don't kick out the inertItem as well as consuming it!
1311 ; reactFunEq ev fsk ev_i fsk_i
1312 ; stopWith ev "Work item rewrites inert" }
1313 else do { -- Rewrite work-item using inert
1314 ; when upgrade_flag $
1315 updInertFunEqs $ \ feqs -> insertFunEq feqs tc args
1316 (upgradeWanted inert_ct)
1317 ; reactFunEq ev_i fsk_i ev fsk
1318 ; stopWith ev "Inert rewrites work item" } }
1319
1320 | otherwise -- Try improvement
1321 = do { improveLocalFunEqs ev inerts tc args fsk
1322 ; continueWith work_item }
1323
1324 interactFunEq _ work_item = pprPanic "interactFunEq" (ppr work_item)
1325
1326 upgradeWanted :: Ct -> Ct
1327 -- We are combining a [W] F tys ~ fmv1 and [D] F tys ~ fmv2
1328 -- so upgrade the [W] to [WD] before putting it in the inert set
1329 upgradeWanted ct = ct { cc_ev = upgrade_ev (cc_ev ct) }
1330 where
1331 upgrade_ev ev = ASSERT2( isWanted ev, ppr ct )
1332 ev { ctev_nosh = WDeriv }
1333
1334 improveLocalFunEqs :: CtEvidence -> InertCans -> TyCon -> [TcType] -> TcTyVar
1335 -> TcS ()
1336 -- Generate derived improvement equalities, by comparing
1337 -- the current work item with inert CFunEqs
1338 -- E.g. x + y ~ z, x + y' ~ z => [D] y ~ y'
1339 --
1340 -- See Note [FunDep and implicit parameter reactions]
1341 improveLocalFunEqs work_ev inerts fam_tc args fsk
1342 | isGiven work_ev -- See Note [No FunEq improvement for Givens]
1343 || not (isImprovable work_ev)
1344 = return ()
1345
1346 | not (null improvement_eqns)
1347 = do { traceTcS "interactFunEq improvements: " $
1348 vcat [ text "Eqns:" <+> ppr improvement_eqns
1349 , text "Candidates:" <+> ppr funeqs_for_tc
1350 , text "Inert eqs:" <+> ppr ieqs ]
1351 ; emitFunDepDeriveds improvement_eqns }
1352
1353 | otherwise
1354 = return ()
1355
1356 where
1357 ieqs = inert_eqs inerts
1358 funeqs = inert_funeqs inerts
1359 funeqs_for_tc = findFunEqsByTyCon funeqs fam_tc
1360 rhs = lookupFlattenTyVar ieqs fsk
1361 work_loc = ctEvLoc work_ev
1362 work_pred = ctEvPred work_ev
1363 fam_inj_info = tyConInjectivityInfo fam_tc
1364
1365 --------------------
1366 improvement_eqns :: [FunDepEqn CtLoc]
1367 improvement_eqns
1368 | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc
1369 = -- Try built-in families, notably for arithmethic
1370 concatMap (do_one_built_in ops) funeqs_for_tc
1371
1372 | Injective injective_args <- fam_inj_info
1373 = -- Try improvement from type families with injectivity annotations
1374 concatMap (do_one_injective injective_args) funeqs_for_tc
1375
1376 | otherwise
1377 = []
1378
1379 --------------------
1380 do_one_built_in ops (CFunEqCan { cc_tyargs = iargs, cc_fsk = ifsk, cc_ev = inert_ev })
1381 = mk_fd_eqns inert_ev (sfInteractInert ops args rhs iargs
1382 (lookupFlattenTyVar ieqs ifsk))
1383
1384 do_one_built_in _ _ = pprPanic "interactFunEq 1" (ppr fam_tc)
1385
1386 --------------------
1387 -- See Note [Type inference for type families with injectivity]
1388 do_one_injective inj_args (CFunEqCan { cc_tyargs = inert_args
1389 , cc_fsk = ifsk, cc_ev = inert_ev })
1390 | isImprovable inert_ev
1391 , rhs `tcEqType` lookupFlattenTyVar ieqs ifsk
1392 = mk_fd_eqns inert_ev $
1393 [ Pair arg iarg
1394 | (arg, iarg, True) <- zip3 args inert_args inj_args ]
1395 | otherwise
1396 = []
1397
1398 do_one_injective _ _ = pprPanic "interactFunEq 2" (ppr fam_tc)
1399
1400 --------------------
1401 mk_fd_eqns :: CtEvidence -> [TypeEqn] -> [FunDepEqn CtLoc]
1402 mk_fd_eqns inert_ev eqns
1403 | null eqns = []
1404 | otherwise = [ FDEqn { fd_qtvs = [], fd_eqs = eqns
1405 , fd_pred1 = work_pred
1406 , fd_pred2 = ctEvPred inert_ev
1407 , fd_loc = loc } ]
1408 where
1409 inert_loc = ctEvLoc inert_ev
1410 loc = inert_loc { ctl_depth = ctl_depth inert_loc `maxSubGoalDepth`
1411 ctl_depth work_loc }
1412
1413 -------------
1414 reactFunEq :: CtEvidence -> TcTyVar -- From this :: F args1 ~ fsk1
1415 -> CtEvidence -> TcTyVar -- Solve this :: F args2 ~ fsk2
1416 -> TcS ()
1417 reactFunEq from_this fsk1 solve_this fsk2
1418 = do { traceTcS "reactFunEq"
1419 (vcat [ppr from_this, ppr fsk1, ppr solve_this, ppr fsk2])
1420 ; dischargeFunEq solve_this fsk2 (ctEvCoercion from_this) (mkTyVarTy fsk1)
1421 ; traceTcS "reactFunEq done" (ppr from_this $$ ppr fsk1 $$
1422 ppr solve_this $$ ppr fsk2) }
1423
1424 {- Note [Type inference for type families with injectivity]
1425 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1426 Suppose we have a type family with an injectivity annotation:
1427 type family F a b = r | r -> b
1428
1429 Then if we have two CFunEqCan constraints for F with the same RHS
1430 F s1 t1 ~ rhs
1431 F s2 t2 ~ rhs
1432 then we can use the injectivity to get a new Derived constraint on
1433 the injective argument
1434 [D] t1 ~ t2
1435
1436 That in turn can help GHC solve constraints that would otherwise require
1437 guessing. For example, consider the ambiguity check for
1438 f :: F Int b -> Int
1439 We get the constraint
1440 [W] F Int b ~ F Int beta
1441 where beta is a unification variable. Injectivity lets us pick beta ~ b.
1442
1443 Injectivity information is also used at the call sites. For example:
1444 g = f True
1445 gives rise to
1446 [W] F Int b ~ Bool
1447 from which we can derive b. This requires looking at the defining equations of
1448 a type family, ie. finding equation with a matching RHS (Bool in this example)
1449 and infering values of type variables (b in this example) from the LHS patterns
1450 of the matching equation. For closed type families we have to perform
1451 additional apartness check for the selected equation to check that the selected
1452 is guaranteed to fire for given LHS arguments.
1453
1454 These new constraints are simply *Derived* constraints; they have no evidence.
1455 We could go further and offer evidence from decomposing injective type-function
1456 applications, but that would require new evidence forms, and an extension to
1457 FC, so we don't do that right now (Dec 14).
1458
1459 See also Note [Injective type families] in TyCon
1460
1461
1462 Note [Cache-caused loops]
1463 ~~~~~~~~~~~~~~~~~~~~~~~~~
1464 It is very dangerous to cache a rewritten wanted family equation as 'solved' in our
1465 solved cache (which is the default behaviour or xCtEvidence), because the interaction
1466 may not be contributing towards a solution. Here is an example:
1467
1468 Initial inert set:
1469 [W] g1 : F a ~ beta1
1470 Work item:
1471 [W] g2 : F a ~ beta2
1472 The work item will react with the inert yielding the _same_ inert set plus:
1473 (i) Will set g2 := g1 `cast` g3
1474 (ii) Will add to our solved cache that [S] g2 : F a ~ beta2
1475 (iii) Will emit [W] g3 : beta1 ~ beta2
1476 Now, the g3 work item will be spontaneously solved to [G] g3 : beta1 ~ beta2
1477 and then it will react the item in the inert ([W] g1 : F a ~ beta1). So it
1478 will set
1479 g1 := g ; sym g3
1480 and what is g? Well it would ideally be a new goal of type (F a ~ beta2) but
1481 remember that we have this in our solved cache, and it is ... g2! In short we
1482 created the evidence loop:
1483
1484 g2 := g1 ; g3
1485 g3 := refl
1486 g1 := g2 ; sym g3
1487
1488 To avoid this situation we do not cache as solved any workitems (or inert)
1489 which did not really made a 'step' towards proving some goal. Solved's are
1490 just an optimization so we don't lose anything in terms of completeness of
1491 solving.
1492
1493
1494 Note [Efficient Orientation]
1495 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1496 Suppose we are interacting two FunEqCans with the same LHS:
1497 (inert) ci :: (F ty ~ xi_i)
1498 (work) cw :: (F ty ~ xi_w)
1499 We prefer to keep the inert (else we pass the work item on down
1500 the pipeline, which is a bit silly). If we keep the inert, we
1501 will (a) discharge 'cw'
1502 (b) produce a new equality work-item (xi_w ~ xi_i)
1503 Notice the orientation (xi_w ~ xi_i) NOT (xi_i ~ xi_w):
1504 new_work :: xi_w ~ xi_i
1505 cw := ci ; sym new_work
1506 Why? Consider the simplest case when xi1 is a type variable. If
1507 we generate xi1~xi2, porcessing that constraint will kick out 'ci'.
1508 If we generate xi2~xi1, there is less chance of that happening.
1509 Of course it can and should still happen if xi1=a, xi1=Int, say.
1510 But we want to avoid it happening needlessly.
1511
1512 Similarly, if we *can't* keep the inert item (because inert is Wanted,
1513 and work is Given, say), we prefer to orient the new equality (xi_i ~
1514 xi_w).
1515
1516 Note [Carefully solve the right CFunEqCan]
1517 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1518 ---- OLD COMMENT, NOW NOT NEEDED
1519 ---- because we now allow multiple
1520 ---- wanted FunEqs with the same head
1521 Consider the constraints
1522 c1 :: F Int ~ a -- Arising from an application line 5
1523 c2 :: F Int ~ Bool -- Arising from an application line 10
1524 Suppose that 'a' is a unification variable, arising only from
1525 flattening. So there is no error on line 5; it's just a flattening
1526 variable. But there is (or might be) an error on line 10.
1527
1528 Two ways to combine them, leaving either (Plan A)
1529 c1 :: F Int ~ a -- Arising from an application line 5
1530 c3 :: a ~ Bool -- Arising from an application line 10
1531 or (Plan B)
1532 c2 :: F Int ~ Bool -- Arising from an application line 10
1533 c4 :: a ~ Bool -- Arising from an application line 5
1534
1535 Plan A will unify c3, leaving c1 :: F Int ~ Bool as an error
1536 on the *totally innocent* line 5. An example is test SimpleFail16
1537 where the expected/actual message comes out backwards if we use
1538 the wrong plan.
1539
1540 The second is the right thing to do. Hence the isMetaTyVarTy
1541 test when solving pairwise CFunEqCan.
1542
1543
1544 **********************************************************************
1545 * *
1546 interactTyVarEq
1547 * *
1548 **********************************************************************
1549 -}
1550
1551 inertsCanDischarge :: InertCans -> TcTyVar -> TcType -> CtFlavourRole
1552 -> Maybe ( CtEvidence -- The evidence for the inert
1553 , SwapFlag -- Whether we need mkSymCo
1554 , Bool) -- True <=> keep a [D] version
1555 -- of the [WD] constraint
1556 inertsCanDischarge inerts tv rhs fr
1557 | (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i
1558 , cc_eq_rel = eq_rel }
1559 <- findTyEqs inerts tv
1560 , (ctEvFlavour ev_i, eq_rel) `eqCanDischargeFR` fr
1561 , rhs_i `tcEqType` rhs ]
1562 = -- Inert: a ~ ty
1563 -- Work item: a ~ ty
1564 Just (ev_i, NotSwapped, keep_deriv ev_i)
1565
1566 | Just tv_rhs <- getTyVar_maybe rhs
1567 , (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i
1568 , cc_eq_rel = eq_rel }
1569 <- findTyEqs inerts tv_rhs
1570 , (ctEvFlavour ev_i, eq_rel) `eqCanDischargeFR` fr
1571 , rhs_i `tcEqType` mkTyVarTy tv ]
1572 = -- Inert: a ~ b
1573 -- Work item: b ~ a
1574 Just (ev_i, IsSwapped, keep_deriv ev_i)
1575
1576 | otherwise
1577 = Nothing
1578
1579 where
1580 keep_deriv ev_i
1581 | Wanted WOnly <- ctEvFlavour ev_i -- inert is [W]
1582 , (Wanted WDeriv, _) <- fr -- work item is [WD]
1583 = True -- Keep a derived verison of the work item
1584 | otherwise
1585 = False -- Work item is fully discharged
1586
1587 interactTyVarEq :: InertCans -> Ct -> TcS (StopOrContinue Ct)
1588 -- CTyEqCans are always consumed, so always returns Stop
1589 interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv
1590 , cc_rhs = rhs
1591 , cc_ev = ev
1592 , cc_eq_rel = eq_rel })
1593 | Just (ev_i, swapped, keep_deriv)
1594 <- inertsCanDischarge inerts tv rhs (ctEvFlavour ev, eq_rel)
1595 = do { setEvBindIfWanted ev $
1596 evCoercion (maybeSym swapped $
1597 tcDowngradeRole (eqRelRole eq_rel)
1598 (ctEvRole ev_i)
1599 (ctEvCoercion ev_i))
1600
1601 ; let deriv_ev = CtDerived { ctev_pred = ctEvPred ev
1602 , ctev_loc = ctEvLoc ev }
1603 ; when keep_deriv $
1604 emitWork [workItem { cc_ev = deriv_ev }]
1605 -- As a Derived it might not be fully rewritten,
1606 -- so we emit it as new work
1607
1608 ; stopWith ev "Solved from inert" }
1609
1610 | ReprEq <- eq_rel -- See Note [Do not unify representational equalities]
1611 = do { traceTcS "Not unifying representational equality" (ppr workItem)
1612 ; continueWith workItem }
1613
1614 | isGiven ev -- See Note [Touchables and givens]
1615 = continueWith workItem
1616
1617 | otherwise
1618 = do { tclvl <- getTcLevel
1619 ; if canSolveByUnification tclvl tv rhs
1620 then do { solveByUnification ev tv rhs
1621 ; n_kicked <- kickOutAfterUnification tv
1622 ; return (Stop ev (text "Solved by unification" <+> pprKicked n_kicked)) }
1623
1624 else continueWith workItem }
1625
1626 interactTyVarEq _ wi = pprPanic "interactTyVarEq" (ppr wi)
1627
1628 solveByUnification :: CtEvidence -> TcTyVar -> Xi -> TcS ()
1629 -- Solve with the identity coercion
1630 -- Precondition: kind(xi) equals kind(tv)
1631 -- Precondition: CtEvidence is Wanted or Derived
1632 -- Precondition: CtEvidence is nominal
1633 -- Returns: workItem where
1634 -- workItem = the new Given constraint
1635 --
1636 -- NB: No need for an occurs check here, because solveByUnification always
1637 -- arises from a CTyEqCan, a *canonical* constraint. Its invariants
1638 -- say that in (a ~ xi), the type variable a does not appear in xi.
1639 -- See TcRnTypes.Ct invariants.
1640 --
1641 -- Post: tv is unified (by side effect) with xi;
1642 -- we often write tv := xi
1643 solveByUnification wd tv xi
1644 = do { let tv_ty = mkTyVarTy tv
1645 ; traceTcS "Sneaky unification:" $
1646 vcat [text "Unifies:" <+> ppr tv <+> text ":=" <+> ppr xi,
1647 text "Coercion:" <+> pprEq tv_ty xi,
1648 text "Left Kind is:" <+> ppr (typeKind tv_ty),
1649 text "Right Kind is:" <+> ppr (typeKind xi) ]
1650
1651 ; unifyTyVar tv xi
1652 ; setEvBindIfWanted wd (evCoercion (mkTcNomReflCo xi)) }
1653
1654 {- Note [Avoid double unifications]
1655 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1656 The spontaneous solver has to return a given which mentions the unified unification
1657 variable *on the left* of the equality. Here is what happens if not:
1658 Original wanted: (a ~ alpha), (alpha ~ Int)
1659 We spontaneously solve the first wanted, without changing the order!
1660 given : a ~ alpha [having unified alpha := a]
1661 Now the second wanted comes along, but he cannot rewrite the given, so we simply continue.
1662 At the end we spontaneously solve that guy, *reunifying* [alpha := Int]
1663
1664 We avoid this problem by orienting the resulting given so that the unification
1665 variable is on the left. [Note that alternatively we could attempt to
1666 enforce this at canonicalization]
1667
1668 See also Note [No touchables as FunEq RHS] in TcSMonad; avoiding
1669 double unifications is the main reason we disallow touchable
1670 unification variables as RHS of type family equations: F xis ~ alpha.
1671
1672 Note [Do not unify representational equalities]
1673 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1674 Consider [W] alpha ~R# b
1675 where alpha is touchable. Should we unify alpha := b?
1676
1677 Certainly not! Unifying forces alpha and be to be the same; but they
1678 only need to be representationally equal types.
1679
1680 For example, we might have another constraint [W] alpha ~# N b
1681 where
1682 newtype N b = MkN b
1683 and we want to get alpha := N b.
1684
1685 See also Trac #15144, which was caused by unifying a representational
1686 equality (in the unflattener).
1687
1688
1689 ************************************************************************
1690 * *
1691 * Functional dependencies, instantiation of equations
1692 * *
1693 ************************************************************************
1694
1695 When we spot an equality arising from a functional dependency,
1696 we now use that equality (a "wanted") to rewrite the work-item
1697 constraint right away. This avoids two dangers
1698
1699 Danger 1: If we send the original constraint on down the pipeline
1700 it may react with an instance declaration, and in delicate
1701 situations (when a Given overlaps with an instance) that
1702 may produce new insoluble goals: see Trac #4952
1703
1704 Danger 2: If we don't rewrite the constraint, it may re-react
1705 with the same thing later, and produce the same equality
1706 again --> termination worries.
1707
1708 To achieve this required some refactoring of FunDeps.hs (nicer
1709 now!).
1710
1711 Note [FunDep and implicit parameter reactions]
1712 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1713 Currently, our story of interacting two dictionaries (or a dictionary
1714 and top-level instances) for functional dependencies, and implicit
1715 parameters, is that we simply produce new Derived equalities. So for example
1716
1717 class D a b | a -> b where ...
1718 Inert:
1719 d1 :g D Int Bool
1720 WorkItem:
1721 d2 :w D Int alpha
1722
1723 We generate the extra work item
1724 cv :d alpha ~ Bool
1725 where 'cv' is currently unused. However, this new item can perhaps be
1726 spontaneously solved to become given and react with d2,
1727 discharging it in favour of a new constraint d2' thus:
1728 d2' :w D Int Bool
1729 d2 := d2' |> D Int cv
1730 Now d2' can be discharged from d1
1731
1732 We could be more aggressive and try to *immediately* solve the dictionary
1733 using those extra equalities, but that requires those equalities to carry
1734 evidence and derived do not carry evidence.
1735
1736 If that were the case with the same inert set and work item we might dischard
1737 d2 directly:
1738
1739 cv :w alpha ~ Bool
1740 d2 := d1 |> D Int cv
1741
1742 But in general it's a bit painful to figure out the necessary coercion,
1743 so we just take the first approach. Here is a better example. Consider:
1744 class C a b c | a -> b
1745 And:
1746 [Given] d1 : C T Int Char
1747 [Wanted] d2 : C T beta Int
1748 In this case, it's *not even possible* to solve the wanted immediately.
1749 So we should simply output the functional dependency and add this guy
1750 [but NOT its superclasses] back in the worklist. Even worse:
1751 [Given] d1 : C T Int beta
1752 [Wanted] d2: C T beta Int
1753 Then it is solvable, but its very hard to detect this on the spot.
1754
1755 It's exactly the same with implicit parameters, except that the
1756 "aggressive" approach would be much easier to implement.
1757
1758 Note [Weird fundeps]
1759 ~~~~~~~~~~~~~~~~~~~~
1760 Consider class Het a b | a -> b where
1761 het :: m (f c) -> a -> m b
1762
1763 class GHet (a :: * -> *) (b :: * -> *) | a -> b
1764 instance GHet (K a) (K [a])
1765 instance Het a b => GHet (K a) (K b)
1766
1767 The two instances don't actually conflict on their fundeps,
1768 although it's pretty strange. So they are both accepted. Now
1769 try [W] GHet (K Int) (K Bool)
1770 This triggers fundeps from both instance decls;
1771 [D] K Bool ~ K [a]
1772 [D] K Bool ~ K beta
1773 And there's a risk of complaining about Bool ~ [a]. But in fact
1774 the Wanted matches the second instance, so we never get as far
1775 as the fundeps.
1776
1777 Trac #7875 is a case in point.
1778 -}
1779
1780 emitFunDepDeriveds :: [FunDepEqn CtLoc] -> TcS ()
1781 -- See Note [FunDep and implicit parameter reactions]
1782 emitFunDepDeriveds fd_eqns
1783 = mapM_ do_one_FDEqn fd_eqns
1784 where
1785 do_one_FDEqn (FDEqn { fd_qtvs = tvs, fd_eqs = eqs, fd_loc = loc })
1786 | null tvs -- Common shortcut
1787 = do { traceTcS "emitFunDepDeriveds 1" (ppr (ctl_depth loc) $$ ppr eqs $$ ppr (isGivenLoc loc))
1788 ; mapM_ (unifyDerived loc Nominal) eqs }
1789 | otherwise
1790 = do { traceTcS "emitFunDepDeriveds 2" (ppr (ctl_depth loc) $$ ppr tvs $$ ppr eqs)
1791 ; subst <- instFlexi tvs -- Takes account of kind substitution
1792 ; mapM_ (do_one_eq loc subst) eqs }
1793
1794 do_one_eq loc subst (Pair ty1 ty2)
1795 = unifyDerived loc Nominal $
1796 Pair (Type.substTyUnchecked subst ty1) (Type.substTyUnchecked subst ty2)
1797
1798 {-
1799 **********************************************************************
1800 * *
1801 The top-reaction Stage
1802 * *
1803 **********************************************************************
1804 -}
1805
1806 topReactionsStage :: WorkItem -> TcS (StopOrContinue Ct)
1807 -- The work item does not react with the inert set,
1808 -- so try interaction with top-level instances. Note:
1809 topReactionsStage work_item
1810 = do { traceTcS "doTopReact" (ppr work_item)
1811 ; case work_item of
1812 CDictCan {} -> do { inerts <- getTcSInerts
1813 ; doTopReactDict inerts work_item }
1814 CFunEqCan {} -> doTopReactFunEq work_item
1815 CIrredCan {} -> doTopReactOther work_item
1816 CTyEqCan {} -> doTopReactOther work_item
1817 _ -> -- Any other work item does not react with any top-level equations
1818 continueWith work_item }
1819
1820
1821 --------------------
1822 doTopReactOther :: Ct -> TcS (StopOrContinue Ct)
1823 doTopReactOther work_item
1824 = do { -- Try local quantified constraints
1825 res <- matchLocalInst pred (ctEvLoc ev)
1826 ; case res of
1827 OneInst {} -> chooseInstance work_item res
1828 _ -> continueWith work_item }
1829 where
1830 ev = ctEvidence work_item
1831 pred = ctEvPred ev
1832
1833 --------------------
1834 doTopReactFunEq :: Ct -> TcS (StopOrContinue Ct)
1835 doTopReactFunEq work_item@(CFunEqCan { cc_ev = old_ev, cc_fun = fam_tc
1836 , cc_tyargs = args, cc_fsk = fsk })
1837
1838 | fsk `elemVarSet` tyCoVarsOfTypes args
1839 = no_reduction -- See Note [FunEq occurs-check principle]
1840
1841 | otherwise -- Note [Reduction for Derived CFunEqCans]
1842 = do { match_res <- matchFam fam_tc args
1843 -- Look up in top-level instances, or built-in axiom
1844 -- See Note [MATCHING-SYNONYMS]
1845 ; case match_res of
1846 Nothing -> no_reduction
1847 Just match_info -> reduce_top_fun_eq old_ev fsk match_info }
1848 where
1849 no_reduction
1850 = do { improveTopFunEqs old_ev fam_tc args fsk
1851 ; continueWith work_item }
1852
1853 doTopReactFunEq w = pprPanic "doTopReactFunEq" (ppr w)
1854
1855 reduce_top_fun_eq :: CtEvidence -> TcTyVar -> (TcCoercion, TcType)
1856 -> TcS (StopOrContinue Ct)
1857 -- We have found an applicable top-level axiom: use it to reduce
1858 -- Precondition: fsk is not free in rhs_ty
1859 reduce_top_fun_eq old_ev fsk (ax_co, rhs_ty)
1860 | not (isDerived old_ev) -- Precondition of shortCutReduction
1861 , Just (tc, tc_args) <- tcSplitTyConApp_maybe rhs_ty
1862 , isTypeFamilyTyCon tc
1863 , tc_args `lengthIs` tyConArity tc -- Short-cut
1864 = -- RHS is another type-family application
1865 -- Try shortcut; see Note [Top-level reductions for type functions]
1866 do { shortCutReduction old_ev fsk ax_co tc tc_args
1867 ; stopWith old_ev "Fun/Top (shortcut)" }
1868
1869 | otherwise
1870 = ASSERT2( not (fsk `elemVarSet` tyCoVarsOfType rhs_ty)
1871 , ppr old_ev $$ ppr rhs_ty )
1872 -- Guaranteed by Note [FunEq occurs-check principle]
1873 do { dischargeFunEq old_ev fsk ax_co rhs_ty
1874 ; traceTcS "doTopReactFunEq" $
1875 vcat [ text "old_ev:" <+> ppr old_ev
1876 , nest 2 (text ":=") <+> ppr ax_co ]
1877 ; stopWith old_ev "Fun/Top" }
1878
1879 improveTopFunEqs :: CtEvidence -> TyCon -> [TcType] -> TcTyVar -> TcS ()
1880 -- See Note [FunDep and implicit parameter reactions]
1881 improveTopFunEqs ev fam_tc args fsk
1882 | isGiven ev -- See Note [No FunEq improvement for Givens]
1883 || not (isImprovable ev)
1884 = return ()
1885
1886 | otherwise
1887 = do { ieqs <- getInertEqs
1888 ; fam_envs <- getFamInstEnvs
1889 ; eqns <- improve_top_fun_eqs fam_envs fam_tc args
1890 (lookupFlattenTyVar ieqs fsk)
1891 ; traceTcS "improveTopFunEqs" (vcat [ ppr fam_tc <+> ppr args <+> ppr fsk
1892 , ppr eqns ])
1893 ; mapM_ (unifyDerived loc Nominal) eqns }
1894 where
1895 loc = ctEvLoc ev -- ToDo: this location is wrong; it should be FunDepOrigin2
1896 -- See Trac #14778
1897
1898 improve_top_fun_eqs :: FamInstEnvs
1899 -> TyCon -> [TcType] -> TcType
1900 -> TcS [TypeEqn]
1901 improve_top_fun_eqs fam_envs fam_tc args rhs_ty
1902 | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc
1903 = return (sfInteractTop ops args rhs_ty)
1904
1905 -- see Note [Type inference for type families with injectivity]
1906 | isOpenTypeFamilyTyCon fam_tc
1907 , Injective injective_args <- tyConInjectivityInfo fam_tc
1908 , let fam_insts = lookupFamInstEnvByTyCon fam_envs fam_tc
1909 = -- it is possible to have several compatible equations in an open type
1910 -- family but we only want to derive equalities from one such equation.
1911 do { let improvs = buildImprovementData fam_insts
1912 fi_tvs fi_tys fi_rhs (const Nothing)
1913
1914 ; traceTcS "improve_top_fun_eqs2" (ppr improvs)
1915 ; concatMapM (injImproveEqns injective_args) $
1916 take 1 improvs }
1917
1918 | Just ax <- isClosedSynFamilyTyConWithAxiom_maybe fam_tc
1919 , Injective injective_args <- tyConInjectivityInfo fam_tc
1920 = concatMapM (injImproveEqns injective_args) $
1921 buildImprovementData (fromBranches (co_ax_branches ax))
1922 cab_tvs cab_lhs cab_rhs Just
1923
1924 | otherwise
1925 = return []
1926
1927 where
1928 buildImprovementData
1929 :: [a] -- axioms for a TF (FamInst or CoAxBranch)
1930 -> (a -> [TyVar]) -- get bound tyvars of an axiom
1931 -> (a -> [Type]) -- get LHS of an axiom
1932 -> (a -> Type) -- get RHS of an axiom
1933 -> (a -> Maybe CoAxBranch) -- Just => apartness check required
1934 -> [( [Type], TCvSubst, [TyVar], Maybe CoAxBranch )]
1935 -- Result:
1936 -- ( [arguments of a matching axiom]
1937 -- , RHS-unifying substitution
1938 -- , axiom variables without substitution
1939 -- , Maybe matching axiom [Nothing - open TF, Just - closed TF ] )
1940 buildImprovementData axioms axiomTVs axiomLHS axiomRHS wrap =
1941 [ (ax_args, subst, unsubstTvs, wrap axiom)
1942 | axiom <- axioms
1943 , let ax_args = axiomLHS axiom
1944 ax_rhs = axiomRHS axiom
1945 ax_tvs = axiomTVs axiom
1946 , Just subst <- [tcUnifyTyWithTFs False ax_rhs rhs_ty]
1947 , let notInSubst tv = not (tv `elemVarEnv` getTvSubstEnv subst)
1948 unsubstTvs = filter (notInSubst <&&> isTyVar) ax_tvs ]
1949 -- The order of unsubstTvs is important; it must be
1950 -- in telescope order e.g. (k:*) (a:k)
1951
1952 injImproveEqns :: [Bool]
1953 -> ([Type], TCvSubst, [TyCoVar], Maybe CoAxBranch)
1954 -> TcS [TypeEqn]
1955 injImproveEqns inj_args (ax_args, subst, unsubstTvs, cabr)
1956 = do { subst <- instFlexiX subst unsubstTvs
1957 -- If the current substitution bind [k -> *], and
1958 -- one of the un-substituted tyvars is (a::k), we'd better
1959 -- be sure to apply the current substitution to a's kind.
1960 -- Hence instFlexiX. Trac #13135 was an example.
1961
1962 ; return [ Pair (substTyUnchecked subst ax_arg) arg
1963 -- NB: the ax_arg part is on the left
1964 -- see Note [Improvement orientation]
1965 | case cabr of
1966 Just cabr' -> apartnessCheck (substTys subst ax_args) cabr'
1967 _ -> True
1968 , (ax_arg, arg, True) <- zip3 ax_args args inj_args ] }
1969
1970
1971 shortCutReduction :: CtEvidence -> TcTyVar -> TcCoercion
1972 -> TyCon -> [TcType] -> TcS ()
1973 -- See Note [Top-level reductions for type functions]
1974 -- Previously, we flattened the tc_args here, but there's no need to do so.
1975 -- And, if we did, this function would have all the complication of
1976 -- TcCanonical.canCFunEqCan. See Note [canCFunEqCan]
1977 shortCutReduction old_ev fsk ax_co fam_tc tc_args
1978 = ASSERT( ctEvEqRel old_ev == NomEq)
1979 -- ax_co :: F args ~ G tc_args
1980 -- old_ev :: F args ~ fsk
1981 do { new_ev <- case ctEvFlavour old_ev of
1982 Given -> newGivenEvVar deeper_loc
1983 ( mkPrimEqPred (mkTyConApp fam_tc tc_args) (mkTyVarTy fsk)
1984 , evCoercion (mkTcSymCo ax_co
1985 `mkTcTransCo` ctEvCoercion old_ev) )
1986
1987 Wanted {} ->
1988 do { (new_ev, new_co) <- newWantedEq deeper_loc Nominal
1989 (mkTyConApp fam_tc tc_args) (mkTyVarTy fsk)
1990 ; setWantedEq (ctev_dest old_ev) $ ax_co `mkTcTransCo` new_co
1991 ; return new_ev }
1992
1993 Derived -> pprPanic "shortCutReduction" (ppr old_ev)
1994
1995 ; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc
1996 , cc_tyargs = tc_args, cc_fsk = fsk }
1997 ; updWorkListTcS (extendWorkListFunEq new_ct) }
1998 where
1999 deeper_loc = bumpCtLocDepth (ctEvLoc old_ev)
2000
2001 {- Note [Top-level reductions for type functions]
2002 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2003 c.f. Note [The flattening story] in TcFlatten
2004
2005 Suppose we have a CFunEqCan F tys ~ fmv/fsk, and a matching axiom.
2006 Here is what we do, in four cases:
2007
2008 * Wanteds: general firing rule
2009 (work item) [W] x : F tys ~ fmv
2010 instantiate axiom: ax_co : F tys ~ rhs
2011
2012 Then:
2013 Discharge fmv := rhs
2014 Discharge x := ax_co ; sym x2
2015 This is *the* way that fmv's get unified; even though they are
2016 "untouchable".
2017
2018 NB: Given Note [FunEq occurs-check principle], fmv does not appear
2019 in tys, and hence does not appear in the instantiated RHS. So
2020 the unification can't make an infinite type.
2021
2022 * Wanteds: short cut firing rule
2023 Applies when the RHS of the axiom is another type-function application
2024 (work item) [W] x : F tys ~ fmv
2025 instantiate axiom: ax_co : F tys ~ G rhs_tys
2026
2027 It would be a waste to create yet another fmv for (G rhs_tys).
2028 Instead (shortCutReduction):
2029 - Flatten rhs_tys (cos : rhs_tys ~ rhs_xis)
2030 - Add G rhs_xis ~ fmv to flat cache (note: the same old fmv)
2031 - New canonical wanted [W] x2 : G rhs_xis ~ fmv (CFunEqCan)
2032 - Discharge x := ax_co ; G cos ; x2
2033
2034 * Givens: general firing rule
2035 (work item) [G] g : F tys ~ fsk
2036 instantiate axiom: ax_co : F tys ~ rhs
2037
2038 Now add non-canonical given (since rhs is not flat)
2039 [G] (sym g ; ax_co) : fsk ~ rhs (Non-canonical)
2040
2041 * Givens: short cut firing rule
2042 Applies when the RHS of the axiom is another type-function application
2043 (work item) [G] g : F tys ~ fsk
2044 instantiate axiom: ax_co : F tys ~ G rhs_tys
2045
2046 It would be a waste to create yet another fsk for (G rhs_tys).
2047 Instead (shortCutReduction):
2048 - Flatten rhs_tys: flat_cos : tys ~ flat_tys
2049 - Add new Canonical given
2050 [G] (sym (G flat_cos) ; co ; g) : G flat_tys ~ fsk (CFunEqCan)
2051
2052 Note [FunEq occurs-check principle]
2053 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2054 I have spent a lot of time finding a good way to deal with
2055 CFunEqCan constraints like
2056 F (fuv, a) ~ fuv
2057 where flatten-skolem occurs on the LHS. Now in principle we
2058 might may progress by doing a reduction, but in practice its
2059 hard to find examples where it is useful, and easy to find examples
2060 where we fall into an infinite reduction loop. A rule that works
2061 very well is this:
2062
2063 *** FunEq occurs-check principle ***
2064
2065 Do not reduce a CFunEqCan
2066 F tys ~ fsk
2067 if fsk appears free in tys
2068 Instead we treat it as stuck.
2069
2070 Examples:
2071
2072 * Trac #5837 has [G] a ~ TF (a,Int), with an instance
2073 type instance TF (a,b) = (TF a, TF b)
2074 This readily loops when solving givens. But with the FunEq occurs
2075 check principle, it rapidly gets stuck which is fine.
2076
2077 * Trac #12444 is a good example, explained in comment:2. We have
2078 type instance F (Succ x) = Succ (F x)
2079 [W] alpha ~ Succ (F alpha)
2080 If we allow the reduction to happen, we get an infinite loop
2081
2082 Note [Cached solved FunEqs]
2083 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
2084 When trying to solve, say (FunExpensive big-type ~ ty), it's important
2085 to see if we have reduced (FunExpensive big-type) before, lest we
2086 simply repeat it. Hence the lookup in inert_solved_funeqs. Moreover
2087 we must use `funEqCanDischarge` because both uses might (say) be Wanteds,
2088 and we *still* want to save the re-computation.
2089
2090 Note [MATCHING-SYNONYMS]
2091 ~~~~~~~~~~~~~~~~~~~~~~~~
2092 When trying to match a dictionary (D tau) to a top-level instance, or a
2093 type family equation (F taus_1 ~ tau_2) to a top-level family instance,
2094 we do *not* need to expand type synonyms because the matcher will do that for us.
2095
2096 Note [Improvement orientation]
2097 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2098 A very delicate point is the orientation of derived equalities
2099 arising from injectivity improvement (Trac #12522). Suppse we have
2100 type family F x = t | t -> x
2101 type instance F (a, Int) = (Int, G a)
2102 where G is injective; and wanted constraints
2103
2104 [W] TF (alpha, beta) ~ fuv
2105 [W] fuv ~ (Int, <some type>)
2106
2107 The injectivity will give rise to derived constraints
2108
2109 [D] gamma1 ~ alpha
2110 [D] Int ~ beta
2111
2112 The fresh unification variable gamma1 comes from the fact that we
2113 can only do "partial improvement" here; see Section 5.2 of
2114 "Injective type families for Haskell" (HS'15).
2115
2116 Now, it's very important to orient the equations this way round,
2117 so that the fresh unification variable will be eliminated in
2118 favour of alpha. If we instead had
2119 [D] alpha ~ gamma1
2120 then we would unify alpha := gamma1; and kick out the wanted
2121 constraint. But when we grough it back in, it'd look like
2122 [W] TF (gamma1, beta) ~ fuv
2123 and exactly the same thing would happen again! Infinite loop.
2124
2125 This all seems fragile, and it might seem more robust to avoid
2126 introducing gamma1 in the first place, in the case where the
2127 actual argument (alpha, beta) partly matches the improvement
2128 template. But that's a bit tricky, esp when we remember that the
2129 kinds much match too; so it's easier to let the normal machinery
2130 handle it. Instead we are careful to orient the new derived
2131 equality with the template on the left. Delicate, but it works.
2132
2133 Note [No FunEq improvement for Givens]
2134 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2135 We don't do improvements (injectivity etc) for Givens. Why?
2136
2137 * It generates Derived constraints on skolems, which don't do us
2138 much good, except perhaps identify inaccessible branches.
2139 (They'd be perfectly valid though.)
2140
2141 * For type-nat stuff the derived constraints include type families;
2142 e.g. (a < b), (b < c) ==> a < c If we generate a Derived for this,
2143 we'll generate a Derived/Wanted CFunEqCan; and, since the same
2144 InertCans (after solving Givens) are used for each iteration, that
2145 massively confused the unflattening step (TcFlatten.unflatten).
2146
2147 In fact it led to some infinite loops:
2148 indexed-types/should_compile/T10806
2149 indexed-types/should_compile/T10507
2150 polykinds/T10742
2151
2152 Note [Reduction for Derived CFunEqCans]
2153 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2154 You may wonder if it's important to use top-level instances to
2155 simplify [D] CFunEqCan's. But it is. Here's an example (T10226).
2156
2157 type instance F Int = Int
2158 type instance FInv Int = Int
2159
2160 Suppose we have to solve
2161 [WD] FInv (F alpha) ~ alpha
2162 [WD] F alpha ~ Int
2163
2164 --> flatten
2165 [WD] F alpha ~ fuv0
2166 [WD] FInv fuv0 ~ fuv1 -- (A)
2167 [WD] fuv1 ~ alpha
2168 [WD] fuv0 ~ Int -- (B)
2169
2170 --> Rewwrite (A) with (B), splitting it
2171 [WD] F alpha ~ fuv0
2172 [W] FInv fuv0 ~ fuv1
2173 [D] FInv Int ~ fuv1 -- (C)
2174 [WD] fuv1 ~ alpha
2175 [WD] fuv0 ~ Int
2176
2177 --> Reduce (C) with top-level instance
2178 **** This is the key step ***
2179 [WD] F alpha ~ fuv0
2180 [W] FInv fuv0 ~ fuv1
2181 [D] fuv1 ~ Int -- (D)
2182 [WD] fuv1 ~ alpha -- (E)
2183 [WD] fuv0 ~ Int
2184
2185 --> Rewrite (D) with (E)
2186 [WD] F alpha ~ fuv0
2187 [W] FInv fuv0 ~ fuv1
2188 [D] alpha ~ Int -- (F)
2189 [WD] fuv1 ~ alpha
2190 [WD] fuv0 ~ Int
2191
2192 --> unify (F) alpha := Int, and that solves it
2193
2194 Another example is indexed-types/should_compile/T10634
2195 -}
2196
2197 {- *******************************************************************
2198 * *
2199 Top-level reaction for class constraints (CDictCan)
2200 * *
2201 **********************************************************************-}
2202
2203 doTopReactDict :: InertSet -> Ct -> TcS (StopOrContinue Ct)
2204 -- Try to use type-class instance declarations to simplify the constraint
2205 doTopReactDict inerts work_item@(CDictCan { cc_ev = ev, cc_class = cls
2206 , cc_tyargs = xis })
2207 | isGiven ev -- Never use instances for Given constraints
2208 = do { try_fundep_improvement
2209 ; continueWith work_item }
2210
2211 | Just solved_ev <- lookupSolvedDict inerts dict_loc cls xis -- Cached
2212 = do { setEvBindIfWanted ev (ctEvTerm solved_ev)
2213 ; stopWith ev "Dict/Top (cached)" }
2214
2215 | otherwise -- Wanted or Derived, but not cached
2216 = do { dflags <- getDynFlags
2217 ; lkup_res <- matchClassInst dflags inerts cls xis dict_loc
2218 ; case lkup_res of
2219 OneInst { cir_what = what }
2220 -> do { unless (safeOverlap what) $
2221 insertSafeOverlapFailureTcS work_item
2222 ; when (isWanted ev) $ addSolvedDict ev cls xis
2223 ; chooseInstance work_item lkup_res }
2224 _ -> -- NoInstance or NotSure
2225 do { when (isImprovable ev) $
2226 try_fundep_improvement
2227 ; continueWith work_item } }
2228 where
2229 dict_pred = mkClassPred cls xis
2230 dict_loc = ctEvLoc ev
2231 dict_origin = ctLocOrigin dict_loc
2232
2233 -- We didn't solve it; so try functional dependencies with
2234 -- the instance environment, and return
2235 -- See also Note [Weird fundeps]
2236 try_fundep_improvement
2237 = do { traceTcS "try_fundeps" (ppr work_item)
2238 ; instEnvs <- getInstEnvs
2239 ; emitFunDepDeriveds $
2240 improveFromInstEnv instEnvs mk_ct_loc dict_pred }
2241
2242 mk_ct_loc :: PredType -- From instance decl
2243 -> SrcSpan -- also from instance deol
2244 -> CtLoc
2245 mk_ct_loc inst_pred inst_loc
2246 = dict_loc { ctl_origin = FunDepOrigin2 dict_pred dict_origin
2247 inst_pred inst_loc }
2248
2249 doTopReactDict _ w = pprPanic "doTopReactDict" (ppr w)
2250
2251
2252 chooseInstance :: Ct -> ClsInstResult -> TcS (StopOrContinue Ct)
2253 chooseInstance work_item
2254 (OneInst { cir_new_theta = theta
2255 , cir_what = what
2256 , cir_mk_ev = mk_ev })
2257 = do { traceTcS "doTopReact/found instance for" $ ppr ev
2258 ; deeper_loc <- checkInstanceOK loc what pred
2259 ; if isDerived ev then finish_derived deeper_loc theta
2260 else finish_wanted deeper_loc theta mk_ev }
2261 where
2262 ev = ctEvidence work_item
2263 pred = ctEvPred ev
2264 loc = ctEvLoc ev
2265
2266 finish_wanted :: CtLoc -> [TcPredType]
2267 -> ([EvExpr] -> EvTerm) -> TcS (StopOrContinue Ct)
2268 -- Precondition: evidence term matches the predicate workItem
2269 finish_wanted loc theta mk_ev
2270 = do { evb <- getTcEvBindsVar
2271 ; if isCoEvBindsVar evb
2272 then -- See Note [Instances in no-evidence implications]
2273 continueWith work_item
2274 else
2275 do { evc_vars <- mapM (newWanted loc) theta
2276 ; setEvBindIfWanted ev (mk_ev (map getEvExpr evc_vars))
2277 ; emitWorkNC (freshGoals evc_vars)
2278 ; stopWith ev "Dict/Top (solved wanted)" } }
2279
2280 finish_derived loc theta
2281 = -- Use type-class instances for Deriveds, in the hope
2282 -- of generating some improvements
2283 -- C.f. Example 3 of Note [The improvement story]
2284 -- It's easy because no evidence is involved
2285 do { emitNewDeriveds loc theta
2286 ; traceTcS "finish_derived" (ppr (ctl_depth loc))
2287 ; stopWith ev "Dict/Top (solved derived)" }
2288
2289 chooseInstance work_item lookup_res
2290 = pprPanic "chooseInstance" (ppr work_item $$ ppr lookup_res)
2291
2292 checkInstanceOK :: CtLoc -> InstanceWhat -> TcPredType -> TcS CtLoc
2293 -- Check that it's OK to use this insstance:
2294 -- (a) the use is well staged in the Template Haskell sense
2295 -- (b) we have not recursed too deep
2296 -- Returns the CtLoc to used for sub-goals
2297 checkInstanceOK loc what pred
2298 = do { checkWellStagedDFun loc what pred
2299 ; checkReductionDepth deeper_loc pred
2300 ; return deeper_loc }
2301 where
2302 deeper_loc = zap_origin (bumpCtLocDepth loc)
2303 origin = ctLocOrigin loc
2304
2305 zap_origin loc -- After applying an instance we can set ScOrigin to
2306 -- infinity, so that prohibitedSuperClassSolve never fires
2307 | ScOrigin {} <- origin
2308 = setCtLocOrigin loc (ScOrigin infinity)
2309 | otherwise
2310 = loc
2311
2312 {- Note [Instances in no-evidence implications]
2313 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2314 In Trac #15290 we had
2315 [G] forall p q. Coercible p q => Coercible (m p) (m q))
2316 [W] forall <no-ev> a. m (Int, IntStateT m a)
2317 ~R#
2318 m (Int, StateT Int m a)
2319
2320 The Given is an ordinary quantified constraint; the Wanted is an implication
2321 equality that arises from
2322 [W] (forall a. t1) ~R# (forall a. t2)
2323
2324 But because the (t1 ~R# t2) is solved "inside a type" (under that forall a)
2325 we can't generate any term evidence. So we can't actually use that
2326 lovely quantified constraint. Alas!
2327
2328 This test arranges to ignore the instance-based solution under these
2329 (rare) circumstances. It's sad, but I really don't see what else we can do.
2330 -}
2331
2332
2333 matchClassInst :: DynFlags -> InertSet
2334 -> Class -> [Type]
2335 -> CtLoc -> TcS ClsInstResult
2336 matchClassInst dflags inerts clas tys loc
2337 -- First check whether there is an in-scope Given that could
2338 -- match this constraint. In that case, do not use any instance
2339 -- whether top level, or local quantified constraints.
2340 -- ee Note [Instance and Given overlap]
2341 | not (xopt LangExt.IncoherentInstances dflags)
2342 , not (naturallyCoherentClass clas)
2343 , let matchable_givens = matchableGivens loc pred inerts
2344 , not (isEmptyBag matchable_givens)
2345 = do { traceTcS "Delaying instance application" $
2346 vcat [ text "Work item=" <+> pprClassPred clas tys
2347 , text "Potential matching givens:" <+> ppr matchable_givens ]
2348 ; return NotSure }
2349
2350 | otherwise
2351 = do { traceTcS "matchClassInst" $ text "pred =" <+> ppr pred <+> char '{'
2352 ; local_res <- matchLocalInst pred loc
2353 ; case local_res of
2354 OneInst {} -> -- See Note [Local instances and incoherence]
2355 do { traceTcS "} matchClassInst local match" $ ppr local_res
2356 ; return local_res }
2357
2358 NotSure -> -- In the NotSure case for local instances
2359 -- we don't want to try global instances
2360 do { traceTcS "} matchClassInst local not sure" empty
2361 ; return local_res }
2362
2363 NoInstance -- No local instances, so try global ones
2364 -> do { global_res <- matchGlobalInst dflags False clas tys
2365 ; traceTcS "} matchClassInst global result" $ ppr global_res
2366 ; return global_res } }
2367 where
2368 pred = mkClassPred clas tys
2369
2370 -- | If a class is "naturally coherent", then we needn't worry at all, in any
2371 -- way, about overlapping/incoherent instances. Just solve the thing!
2372 -- See Note [Naturally coherent classes]
2373 -- See also Note [The equality class story] in TysPrim.
2374 naturallyCoherentClass :: Class -> Bool
2375 naturallyCoherentClass cls
2376 = isCTupleClass cls
2377 || cls `hasKey` heqTyConKey
2378 || cls `hasKey` eqTyConKey
2379 || cls `hasKey` coercibleTyConKey
2380
2381
2382 {- Note [Instance and Given overlap]
2383 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2384 Example, from the OutsideIn(X) paper:
2385 instance P x => Q [x]
2386 instance (x ~ y) => R y [x]
2387
2388 wob :: forall a b. (Q [b], R b a) => a -> Int
2389
2390 g :: forall a. Q [a] => [a] -> Int
2391 g x = wob x
2392
2393 From 'g' we get the impliation constraint:
2394 forall a. Q [a] => (Q [beta], R beta [a])
2395 If we react (Q [beta]) with its top-level axiom, we end up with a
2396 (P beta), which we have no way of discharging. On the other hand,
2397 if we react R beta [a] with the top-level we get (beta ~ a), which
2398 is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
2399 now solvable by the given Q [a].
2400
2401 The partial solution is that:
2402 In matchClassInst (and thus in topReact), we return a matching
2403 instance only when there is no Given in the inerts which is
2404 unifiable to this particular dictionary.
2405
2406 We treat any meta-tyvar as "unifiable" for this purpose,
2407 *including* untouchable ones. But not skolems like 'a' in
2408 the implication constraint above.
2409
2410 The end effect is that, much as we do for overlapping instances, we
2411 delay choosing a class instance if there is a possibility of another
2412 instance OR a given to match our constraint later on. This fixes
2413 Trac #4981 and #5002.
2414
2415 Other notes:
2416
2417 * The check is done *first*, so that it also covers classes
2418 with built-in instance solving, such as
2419 - constraint tuples
2420 - natural numbers
2421 - Typeable
2422
2423 * Flatten-skolems: we do not treat a flatten-skolem as unifiable
2424 for this purpose.
2425 E.g. f :: Eq (F a) => [a] -> [a]
2426 f xs = ....(xs==xs).....
2427 Here we get [W] Eq [a], and we don't want to refrain from solving
2428 it because of the given (Eq (F a)) constraint!
2429
2430 * The given-overlap problem is arguably not easy to appear in practice
2431 due to our aggressive prioritization of equality solving over other
2432 constraints, but it is possible. I've added a test case in
2433 typecheck/should-compile/GivenOverlapping.hs
2434
2435 * Another "live" example is Trac #10195; another is #10177.
2436
2437 * We ignore the overlap problem if -XIncoherentInstances is in force:
2438 see Trac #6002 for a worked-out example where this makes a
2439 difference.
2440
2441 * Moreover notice that our goals here are different than the goals of
2442 the top-level overlapping checks. There we are interested in
2443 validating the following principle:
2444
2445 If we inline a function f at a site where the same global
2446 instance environment is available as the instance environment at
2447 the definition site of f then we should get the same behaviour.
2448
2449 But for the Given Overlap check our goal is just related to completeness of
2450 constraint solving.
2451
2452 * The solution is only a partial one. Consider the above example with
2453 g :: forall a. Q [a] => [a] -> Int
2454 g x = let v = wob x
2455 in v
2456 and suppose we have -XNoMonoLocalBinds, so that we attempt to find the most
2457 general type for 'v'. When generalising v's type we'll simplify its
2458 Q [alpha] constraint, but we don't have Q [a] in the 'givens', so we
2459 will use the instance declaration after all. Trac #11948 was a case
2460 in point.
2461
2462 All of this is disgustingly delicate, so to discourage people from writing
2463 simplifiable class givens, we warn about signatures that contain them;
2464 see TcValidity Note [Simplifiable given constraints].
2465
2466 Note [Naturally coherent classes]
2467 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2468 A few built-in classes are "naturally coherent". This term means that
2469 the "instance" for the class is bidirectional with its superclass(es).
2470 For example, consider (~~), which behaves as if it was defined like
2471 this:
2472 class a ~# b => a ~~ b
2473 instance a ~# b => a ~~ b
2474 (See Note [The equality types story] in TysPrim.)
2475
2476 Faced with [W] t1 ~~ t2, it's always OK to reduce it to [W] t1 ~# t2,
2477 without worrying about Note [Instance and Given overlap]. Why? Because
2478 if we had [G] s1 ~~ s2, then we'd get the superclass [G] s1 ~# s2, and
2479 so the reduction of the [W] constraint does not risk losing any solutions.
2480
2481 On the other hand, it can be fatal to /fail/ to reduce such
2482 equalities, on the grounds of Note [Instance and Given overlap],
2483 because many good things flow from [W] t1 ~# t2.
2484
2485 The same reasoning applies to
2486
2487 * (~~) heqTyCOn
2488 * (~) eqTyCon
2489 * Coercible coercibleTyCon
2490
2491 And less obviously to:
2492
2493 * Tuple classes. For reasons described in TcSMonad
2494 Note [Tuples hiding implicit parameters], we may have a constraint
2495 [W] (?x::Int, C a)
2496 with an exactly-matching Given constraint. We must decompose this
2497 tuple and solve the components separately, otherwise we won't solve
2498 it at all! It is perfectly safe to decompose it, because again the
2499 superclasses invert the instance; e.g.
2500 class (c1, c2) => (% c1, c2 %)
2501 instance (c1, c2) => (% c1, c2 %)
2502 Example in Trac #14218
2503
2504 Exammples: T5853, T10432, T5315, T9222, T2627b, T3028b
2505
2506 PS: the term "naturally coherent" doesn't really seem helpful.
2507 Perhaps "invertible" or something? I left it for now though.
2508
2509 Note [Local instances and incoherence]
2510 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2511 Consider
2512 f :: forall b c. (Eq b, forall a. Eq a => Eq (c a))
2513 => c b -> Bool
2514 f x = x==x
2515
2516 We get [W] Eq (c b), and we must use the local instance to solve it.
2517
2518 BUT that wanted also unifies with the top-level Eq [a] instance,
2519 and Eq (Maybe a) etc. We want the local instance to "win", otherwise
2520 we can't solve the wanted at all. So we mark it as Incohherent.
2521 According to Note [Rules for instance lookup] in InstEnv, that'll
2522 make it win even if there are other instances that unify.
2523
2524 Moreover this is not a hack! The evidence for this local instance
2525 will be constructed by GHC at a call site... from the very instances
2526 that unify with it here. It is not like an incoherent user-written
2527 instance which might have utterly different behaviour.
2528
2529 Consdider f :: Eq a => blah. If we have [W] Eq a, we certainly
2530 get it from the Eq a context, without worrying that there are
2531 lots of top-level instances that unify with [W] Eq a! We'll use
2532 those instances to build evidence to pass to f. That's just the
2533 nullary case of what's happening here.
2534 -}
2535
2536 matchLocalInst :: TcPredType -> CtLoc -> TcS ClsInstResult
2537 -- Try any Given quantified constraints, which are
2538 -- effectively just local instance declarations.
2539 matchLocalInst pred loc
2540 = do { ics <- getInertCans
2541 ; case match_local_inst (inert_insts ics) of
2542 ([], False) -> return NoInstance
2543 ([(dfun_ev, inst_tys)], unifs)
2544 | not unifs
2545 -> do { let dfun_id = ctEvEvId dfun_ev
2546 ; (tys, theta) <- instDFunType dfun_id inst_tys
2547 ; return $ OneInst { cir_new_theta = theta
2548 , cir_mk_ev = evDFunApp dfun_id tys
2549 , cir_what = LocalInstance } }
2550 _ -> return NotSure }
2551 where
2552 pred_tv_set = tyCoVarsOfType pred
2553
2554 match_local_inst :: [QCInst]
2555 -> ( [(CtEvidence, [DFunInstType])]
2556 , Bool ) -- True <=> Some unify but do not match
2557 match_local_inst []
2558 = ([], False)
2559 match_local_inst (qci@(QCI { qci_tvs = qtvs, qci_pred = qpred
2560 , qci_ev = ev })
2561 : qcis)
2562 | let in_scope = mkInScopeSet (qtv_set `unionVarSet` pred_tv_set)
2563 , Just tv_subst <- ruleMatchTyKiX qtv_set (mkRnEnv2 in_scope)
2564 emptyTvSubstEnv qpred pred
2565 , let match = (ev, map (lookupVarEnv tv_subst) qtvs)
2566 = (match:matches, unif)
2567
2568 | otherwise
2569 = ASSERT2( disjointVarSet qtv_set (tyCoVarsOfType pred)
2570 , ppr qci $$ ppr pred )
2571 -- ASSERT: unification relies on the
2572 -- quantified variables being fresh
2573 (matches, unif || this_unif)
2574 where
2575 qtv_set = mkVarSet qtvs
2576 this_unif = mightMatchLater qpred (ctEvLoc ev) pred loc
2577 (matches, unif) = match_local_inst qcis
2578