18d952501dab06524cb37c3e1db2fb7718b928ab
[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 (isNoEvBindsVar 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 = continueWith workItem
1612
1613 | isGiven ev -- See Note [Touchables and givens]
1614 = continueWith workItem
1615
1616 | otherwise
1617 = do { tclvl <- getTcLevel
1618 ; if canSolveByUnification tclvl tv rhs
1619 then do { solveByUnification ev tv rhs
1620 ; n_kicked <- kickOutAfterUnification tv
1621 ; return (Stop ev (text "Solved by unification" <+> pprKicked n_kicked)) }
1622
1623 else continueWith workItem }
1624
1625 interactTyVarEq _ wi = pprPanic "interactTyVarEq" (ppr wi)
1626
1627 solveByUnification :: CtEvidence -> TcTyVar -> Xi -> TcS ()
1628 -- Solve with the identity coercion
1629 -- Precondition: kind(xi) equals kind(tv)
1630 -- Precondition: CtEvidence is Wanted or Derived
1631 -- Precondition: CtEvidence is nominal
1632 -- Returns: workItem where
1633 -- workItem = the new Given constraint
1634 --
1635 -- NB: No need for an occurs check here, because solveByUnification always
1636 -- arises from a CTyEqCan, a *canonical* constraint. Its invariants
1637 -- say that in (a ~ xi), the type variable a does not appear in xi.
1638 -- See TcRnTypes.Ct invariants.
1639 --
1640 -- Post: tv is unified (by side effect) with xi;
1641 -- we often write tv := xi
1642 solveByUnification wd tv xi
1643 = do { let tv_ty = mkTyVarTy tv
1644 ; traceTcS "Sneaky unification:" $
1645 vcat [text "Unifies:" <+> ppr tv <+> text ":=" <+> ppr xi,
1646 text "Coercion:" <+> pprEq tv_ty xi,
1647 text "Left Kind is:" <+> ppr (typeKind tv_ty),
1648 text "Right Kind is:" <+> ppr (typeKind xi) ]
1649
1650 ; unifyTyVar tv xi
1651 ; setEvBindIfWanted wd (evCoercion (mkTcNomReflCo xi)) }
1652
1653 {- Note [Avoid double unifications]
1654 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1655 The spontaneous solver has to return a given which mentions the unified unification
1656 variable *on the left* of the equality. Here is what happens if not:
1657 Original wanted: (a ~ alpha), (alpha ~ Int)
1658 We spontaneously solve the first wanted, without changing the order!
1659 given : a ~ alpha [having unified alpha := a]
1660 Now the second wanted comes along, but he cannot rewrite the given, so we simply continue.
1661 At the end we spontaneously solve that guy, *reunifying* [alpha := Int]
1662
1663 We avoid this problem by orienting the resulting given so that the unification
1664 variable is on the left. [Note that alternatively we could attempt to
1665 enforce this at canonicalization]
1666
1667 See also Note [No touchables as FunEq RHS] in TcSMonad; avoiding
1668 double unifications is the main reason we disallow touchable
1669 unification variables as RHS of type family equations: F xis ~ alpha.
1670
1671 Note [Do not unify representational equalities]
1672 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1673 Consider [W] alpha ~R# b
1674 where alpha is touchable. Should we unify alpha := b?
1675
1676 Certainly not! Unifying forces alpha and be to be the same; but they
1677 only need to be representationally equal types.
1678
1679 For example, we might have another constraint [W] alpha ~# N b
1680 where
1681 newtype N b = MkN b
1682 and we want to get alpha := N b.
1683
1684 See also Trac #15144, which was caused by unifying a representational
1685 equality (in the unflattener).
1686
1687
1688 ************************************************************************
1689 * *
1690 * Functional dependencies, instantiation of equations
1691 * *
1692 ************************************************************************
1693
1694 When we spot an equality arising from a functional dependency,
1695 we now use that equality (a "wanted") to rewrite the work-item
1696 constraint right away. This avoids two dangers
1697
1698 Danger 1: If we send the original constraint on down the pipeline
1699 it may react with an instance declaration, and in delicate
1700 situations (when a Given overlaps with an instance) that
1701 may produce new insoluble goals: see Trac #4952
1702
1703 Danger 2: If we don't rewrite the constraint, it may re-react
1704 with the same thing later, and produce the same equality
1705 again --> termination worries.
1706
1707 To achieve this required some refactoring of FunDeps.hs (nicer
1708 now!).
1709
1710 Note [FunDep and implicit parameter reactions]
1711 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1712 Currently, our story of interacting two dictionaries (or a dictionary
1713 and top-level instances) for functional dependencies, and implicit
1714 parameters, is that we simply produce new Derived equalities. So for example
1715
1716 class D a b | a -> b where ...
1717 Inert:
1718 d1 :g D Int Bool
1719 WorkItem:
1720 d2 :w D Int alpha
1721
1722 We generate the extra work item
1723 cv :d alpha ~ Bool
1724 where 'cv' is currently unused. However, this new item can perhaps be
1725 spontaneously solved to become given and react with d2,
1726 discharging it in favour of a new constraint d2' thus:
1727 d2' :w D Int Bool
1728 d2 := d2' |> D Int cv
1729 Now d2' can be discharged from d1
1730
1731 We could be more aggressive and try to *immediately* solve the dictionary
1732 using those extra equalities, but that requires those equalities to carry
1733 evidence and derived do not carry evidence.
1734
1735 If that were the case with the same inert set and work item we might dischard
1736 d2 directly:
1737
1738 cv :w alpha ~ Bool
1739 d2 := d1 |> D Int cv
1740
1741 But in general it's a bit painful to figure out the necessary coercion,
1742 so we just take the first approach. Here is a better example. Consider:
1743 class C a b c | a -> b
1744 And:
1745 [Given] d1 : C T Int Char
1746 [Wanted] d2 : C T beta Int
1747 In this case, it's *not even possible* to solve the wanted immediately.
1748 So we should simply output the functional dependency and add this guy
1749 [but NOT its superclasses] back in the worklist. Even worse:
1750 [Given] d1 : C T Int beta
1751 [Wanted] d2: C T beta Int
1752 Then it is solvable, but its very hard to detect this on the spot.
1753
1754 It's exactly the same with implicit parameters, except that the
1755 "aggressive" approach would be much easier to implement.
1756
1757 Note [Weird fundeps]
1758 ~~~~~~~~~~~~~~~~~~~~
1759 Consider class Het a b | a -> b where
1760 het :: m (f c) -> a -> m b
1761
1762 class GHet (a :: * -> *) (b :: * -> *) | a -> b
1763 instance GHet (K a) (K [a])
1764 instance Het a b => GHet (K a) (K b)
1765
1766 The two instances don't actually conflict on their fundeps,
1767 although it's pretty strange. So they are both accepted. Now
1768 try [W] GHet (K Int) (K Bool)
1769 This triggers fundeps from both instance decls;
1770 [D] K Bool ~ K [a]
1771 [D] K Bool ~ K beta
1772 And there's a risk of complaining about Bool ~ [a]. But in fact
1773 the Wanted matches the second instance, so we never get as far
1774 as the fundeps.
1775
1776 Trac #7875 is a case in point.
1777 -}
1778
1779 emitFunDepDeriveds :: [FunDepEqn CtLoc] -> TcS ()
1780 -- See Note [FunDep and implicit parameter reactions]
1781 emitFunDepDeriveds fd_eqns
1782 = mapM_ do_one_FDEqn fd_eqns
1783 where
1784 do_one_FDEqn (FDEqn { fd_qtvs = tvs, fd_eqs = eqs, fd_loc = loc })
1785 | null tvs -- Common shortcut
1786 = do { traceTcS "emitFunDepDeriveds 1" (ppr (ctl_depth loc) $$ ppr eqs $$ ppr (isGivenLoc loc))
1787 ; mapM_ (unifyDerived loc Nominal) eqs }
1788 | otherwise
1789 = do { traceTcS "emitFunDepDeriveds 2" (ppr (ctl_depth loc) $$ ppr tvs $$ ppr eqs)
1790 ; subst <- instFlexi tvs -- Takes account of kind substitution
1791 ; mapM_ (do_one_eq loc subst) eqs }
1792
1793 do_one_eq loc subst (Pair ty1 ty2)
1794 = unifyDerived loc Nominal $
1795 Pair (Type.substTyUnchecked subst ty1) (Type.substTyUnchecked subst ty2)
1796
1797 {-
1798 **********************************************************************
1799 * *
1800 The top-reaction Stage
1801 * *
1802 **********************************************************************
1803 -}
1804
1805 topReactionsStage :: WorkItem -> TcS (StopOrContinue Ct)
1806 -- The work item does not react with the inert set,
1807 -- so try interaction with top-level instances. Note:
1808 topReactionsStage work_item
1809 = do { traceTcS "doTopReact" (ppr work_item)
1810 ; case work_item of
1811 CDictCan {} -> do { inerts <- getTcSInerts
1812 ; doTopReactDict inerts work_item }
1813 CFunEqCan {} -> doTopReactFunEq work_item
1814 CIrredCan {} -> doTopReactOther work_item
1815 CTyEqCan {} -> doTopReactOther work_item
1816 _ -> -- Any other work item does not react with any top-level equations
1817 continueWith work_item }
1818
1819
1820 --------------------
1821 doTopReactOther :: Ct -> TcS (StopOrContinue Ct)
1822 doTopReactOther work_item
1823 = do { -- Try local quantified constraints
1824 res <- matchLocalInst pred (ctEvLoc ev)
1825 ; case res of
1826 OneInst {} -> chooseInstance work_item res
1827 _ -> continueWith work_item }
1828 where
1829 ev = ctEvidence work_item
1830 pred = ctEvPred ev
1831
1832 --------------------
1833 doTopReactFunEq :: Ct -> TcS (StopOrContinue Ct)
1834 doTopReactFunEq work_item@(CFunEqCan { cc_ev = old_ev, cc_fun = fam_tc
1835 , cc_tyargs = args, cc_fsk = fsk })
1836
1837 | fsk `elemVarSet` tyCoVarsOfTypes args
1838 = no_reduction -- See Note [FunEq occurs-check principle]
1839
1840 | otherwise -- Note [Reduction for Derived CFunEqCans]
1841 = do { match_res <- matchFam fam_tc args
1842 -- Look up in top-level instances, or built-in axiom
1843 -- See Note [MATCHING-SYNONYMS]
1844 ; case match_res of
1845 Nothing -> no_reduction
1846 Just match_info -> reduce_top_fun_eq old_ev fsk match_info }
1847 where
1848 no_reduction
1849 = do { improveTopFunEqs old_ev fam_tc args fsk
1850 ; continueWith work_item }
1851
1852 doTopReactFunEq w = pprPanic "doTopReactFunEq" (ppr w)
1853
1854 reduce_top_fun_eq :: CtEvidence -> TcTyVar -> (TcCoercion, TcType)
1855 -> TcS (StopOrContinue Ct)
1856 -- We have found an applicable top-level axiom: use it to reduce
1857 -- Precondition: fsk is not free in rhs_ty
1858 reduce_top_fun_eq old_ev fsk (ax_co, rhs_ty)
1859 | not (isDerived old_ev) -- Precondition of shortCutReduction
1860 , Just (tc, tc_args) <- tcSplitTyConApp_maybe rhs_ty
1861 , isTypeFamilyTyCon tc
1862 , tc_args `lengthIs` tyConArity tc -- Short-cut
1863 = -- RHS is another type-family application
1864 -- Try shortcut; see Note [Top-level reductions for type functions]
1865 do { shortCutReduction old_ev fsk ax_co tc tc_args
1866 ; stopWith old_ev "Fun/Top (shortcut)" }
1867
1868 | otherwise
1869 = ASSERT2( not (fsk `elemVarSet` tyCoVarsOfType rhs_ty)
1870 , ppr old_ev $$ ppr rhs_ty )
1871 -- Guaranteed by Note [FunEq occurs-check principle]
1872 do { dischargeFunEq old_ev fsk ax_co rhs_ty
1873 ; traceTcS "doTopReactFunEq" $
1874 vcat [ text "old_ev:" <+> ppr old_ev
1875 , nest 2 (text ":=") <+> ppr ax_co ]
1876 ; stopWith old_ev "Fun/Top" }
1877
1878 improveTopFunEqs :: CtEvidence -> TyCon -> [TcType] -> TcTyVar -> TcS ()
1879 -- See Note [FunDep and implicit parameter reactions]
1880 improveTopFunEqs ev fam_tc args fsk
1881 | isGiven ev -- See Note [No FunEq improvement for Givens]
1882 || not (isImprovable ev)
1883 = return ()
1884
1885 | otherwise
1886 = do { ieqs <- getInertEqs
1887 ; fam_envs <- getFamInstEnvs
1888 ; eqns <- improve_top_fun_eqs fam_envs fam_tc args
1889 (lookupFlattenTyVar ieqs fsk)
1890 ; traceTcS "improveTopFunEqs" (vcat [ ppr fam_tc <+> ppr args <+> ppr fsk
1891 , ppr eqns ])
1892 ; mapM_ (unifyDerived loc Nominal) eqns }
1893 where
1894 loc = ctEvLoc ev -- ToDo: this location is wrong; it should be FunDepOrigin2
1895 -- See Trac #14778
1896
1897 improve_top_fun_eqs :: FamInstEnvs
1898 -> TyCon -> [TcType] -> TcType
1899 -> TcS [TypeEqn]
1900 improve_top_fun_eqs fam_envs fam_tc args rhs_ty
1901 | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc
1902 = return (sfInteractTop ops args rhs_ty)
1903
1904 -- see Note [Type inference for type families with injectivity]
1905 | isOpenTypeFamilyTyCon fam_tc
1906 , Injective injective_args <- tyConInjectivityInfo fam_tc
1907 , let fam_insts = lookupFamInstEnvByTyCon fam_envs fam_tc
1908 = -- it is possible to have several compatible equations in an open type
1909 -- family but we only want to derive equalities from one such equation.
1910 do { let improvs = buildImprovementData fam_insts
1911 fi_tvs fi_tys fi_rhs (const Nothing)
1912
1913 ; traceTcS "improve_top_fun_eqs2" (ppr improvs)
1914 ; concatMapM (injImproveEqns injective_args) $
1915 take 1 improvs }
1916
1917 | Just ax <- isClosedSynFamilyTyConWithAxiom_maybe fam_tc
1918 , Injective injective_args <- tyConInjectivityInfo fam_tc
1919 = concatMapM (injImproveEqns injective_args) $
1920 buildImprovementData (fromBranches (co_ax_branches ax))
1921 cab_tvs cab_lhs cab_rhs Just
1922
1923 | otherwise
1924 = return []
1925
1926 where
1927 buildImprovementData
1928 :: [a] -- axioms for a TF (FamInst or CoAxBranch)
1929 -> (a -> [TyVar]) -- get bound tyvars of an axiom
1930 -> (a -> [Type]) -- get LHS of an axiom
1931 -> (a -> Type) -- get RHS of an axiom
1932 -> (a -> Maybe CoAxBranch) -- Just => apartness check required
1933 -> [( [Type], TCvSubst, [TyVar], Maybe CoAxBranch )]
1934 -- Result:
1935 -- ( [arguments of a matching axiom]
1936 -- , RHS-unifying substitution
1937 -- , axiom variables without substitution
1938 -- , Maybe matching axiom [Nothing - open TF, Just - closed TF ] )
1939 buildImprovementData axioms axiomTVs axiomLHS axiomRHS wrap =
1940 [ (ax_args, subst, unsubstTvs, wrap axiom)
1941 | axiom <- axioms
1942 , let ax_args = axiomLHS axiom
1943 ax_rhs = axiomRHS axiom
1944 ax_tvs = axiomTVs axiom
1945 , Just subst <- [tcUnifyTyWithTFs False ax_rhs rhs_ty]
1946 , let notInSubst tv = not (tv `elemVarEnv` getTvSubstEnv subst)
1947 unsubstTvs = filter (notInSubst <&&> isTyVar) ax_tvs ]
1948 -- The order of unsubstTvs is important; it must be
1949 -- in telescope order e.g. (k:*) (a:k)
1950
1951 injImproveEqns :: [Bool]
1952 -> ([Type], TCvSubst, [TyCoVar], Maybe CoAxBranch)
1953 -> TcS [TypeEqn]
1954 injImproveEqns inj_args (ax_args, subst, unsubstTvs, cabr)
1955 = do { subst <- instFlexiX subst unsubstTvs
1956 -- If the current substitution bind [k -> *], and
1957 -- one of the un-substituted tyvars is (a::k), we'd better
1958 -- be sure to apply the current substitution to a's kind.
1959 -- Hence instFlexiX. Trac #13135 was an example.
1960
1961 ; return [ Pair (substTyUnchecked subst ax_arg) arg
1962 -- NB: the ax_arg part is on the left
1963 -- see Note [Improvement orientation]
1964 | case cabr of
1965 Just cabr' -> apartnessCheck (substTys subst ax_args) cabr'
1966 _ -> True
1967 , (ax_arg, arg, True) <- zip3 ax_args args inj_args ] }
1968
1969
1970 shortCutReduction :: CtEvidence -> TcTyVar -> TcCoercion
1971 -> TyCon -> [TcType] -> TcS ()
1972 -- See Note [Top-level reductions for type functions]
1973 -- Previously, we flattened the tc_args here, but there's no need to do so.
1974 -- And, if we did, this function would have all the complication of
1975 -- TcCanonical.canCFunEqCan. See Note [canCFunEqCan]
1976 shortCutReduction old_ev fsk ax_co fam_tc tc_args
1977 = ASSERT( ctEvEqRel old_ev == NomEq)
1978 -- ax_co :: F args ~ G tc_args
1979 -- old_ev :: F args ~ fsk
1980 do { new_ev <- case ctEvFlavour old_ev of
1981 Given -> newGivenEvVar deeper_loc
1982 ( mkPrimEqPred (mkTyConApp fam_tc tc_args) (mkTyVarTy fsk)
1983 , evCoercion (mkTcSymCo ax_co
1984 `mkTcTransCo` ctEvCoercion old_ev) )
1985
1986 Wanted {} ->
1987 do { (new_ev, new_co) <- newWantedEq deeper_loc Nominal
1988 (mkTyConApp fam_tc tc_args) (mkTyVarTy fsk)
1989 ; setWantedEq (ctev_dest old_ev) $ ax_co `mkTcTransCo` new_co
1990 ; return new_ev }
1991
1992 Derived -> pprPanic "shortCutReduction" (ppr old_ev)
1993
1994 ; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc
1995 , cc_tyargs = tc_args, cc_fsk = fsk }
1996 ; updWorkListTcS (extendWorkListFunEq new_ct) }
1997 where
1998 deeper_loc = bumpCtLocDepth (ctEvLoc old_ev)
1999
2000 {- Note [Top-level reductions for type functions]
2001 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2002 c.f. Note [The flattening story] in TcFlatten
2003
2004 Suppose we have a CFunEqCan F tys ~ fmv/fsk, and a matching axiom.
2005 Here is what we do, in four cases:
2006
2007 * Wanteds: general firing rule
2008 (work item) [W] x : F tys ~ fmv
2009 instantiate axiom: ax_co : F tys ~ rhs
2010
2011 Then:
2012 Discharge fmv := rhs
2013 Discharge x := ax_co ; sym x2
2014 This is *the* way that fmv's get unified; even though they are
2015 "untouchable".
2016
2017 NB: Given Note [FunEq occurs-check principle], fmv does not appear
2018 in tys, and hence does not appear in the instantiated RHS. So
2019 the unification can't make an infinite type.
2020
2021 * Wanteds: short cut firing rule
2022 Applies when the RHS of the axiom is another type-function application
2023 (work item) [W] x : F tys ~ fmv
2024 instantiate axiom: ax_co : F tys ~ G rhs_tys
2025
2026 It would be a waste to create yet another fmv for (G rhs_tys).
2027 Instead (shortCutReduction):
2028 - Flatten rhs_tys (cos : rhs_tys ~ rhs_xis)
2029 - Add G rhs_xis ~ fmv to flat cache (note: the same old fmv)
2030 - New canonical wanted [W] x2 : G rhs_xis ~ fmv (CFunEqCan)
2031 - Discharge x := ax_co ; G cos ; x2
2032
2033 * Givens: general firing rule
2034 (work item) [G] g : F tys ~ fsk
2035 instantiate axiom: ax_co : F tys ~ rhs
2036
2037 Now add non-canonical given (since rhs is not flat)
2038 [G] (sym g ; ax_co) : fsk ~ rhs (Non-canonical)
2039
2040 * Givens: short cut firing rule
2041 Applies when the RHS of the axiom is another type-function application
2042 (work item) [G] g : F tys ~ fsk
2043 instantiate axiom: ax_co : F tys ~ G rhs_tys
2044
2045 It would be a waste to create yet another fsk for (G rhs_tys).
2046 Instead (shortCutReduction):
2047 - Flatten rhs_tys: flat_cos : tys ~ flat_tys
2048 - Add new Canonical given
2049 [G] (sym (G flat_cos) ; co ; g) : G flat_tys ~ fsk (CFunEqCan)
2050
2051 Note [FunEq occurs-check principle]
2052 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2053 I have spent a lot of time finding a good way to deal with
2054 CFunEqCan constraints like
2055 F (fuv, a) ~ fuv
2056 where flatten-skolem occurs on the LHS. Now in principle we
2057 might may progress by doing a reduction, but in practice its
2058 hard to find examples where it is useful, and easy to find examples
2059 where we fall into an infinite reduction loop. A rule that works
2060 very well is this:
2061
2062 *** FunEq occurs-check principle ***
2063
2064 Do not reduce a CFunEqCan
2065 F tys ~ fsk
2066 if fsk appears free in tys
2067 Instead we treat it as stuck.
2068
2069 Examples:
2070
2071 * Trac #5837 has [G] a ~ TF (a,Int), with an instance
2072 type instance TF (a,b) = (TF a, TF b)
2073 This readily loops when solving givens. But with the FunEq occurs
2074 check principle, it rapidly gets stuck which is fine.
2075
2076 * Trac #12444 is a good example, explained in comment:2. We have
2077 type instance F (Succ x) = Succ (F x)
2078 [W] alpha ~ Succ (F alpha)
2079 If we allow the reduction to happen, we get an infinite loop
2080
2081 Note [Cached solved FunEqs]
2082 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
2083 When trying to solve, say (FunExpensive big-type ~ ty), it's important
2084 to see if we have reduced (FunExpensive big-type) before, lest we
2085 simply repeat it. Hence the lookup in inert_solved_funeqs. Moreover
2086 we must use `funEqCanDischarge` because both uses might (say) be Wanteds,
2087 and we *still* want to save the re-computation.
2088
2089 Note [MATCHING-SYNONYMS]
2090 ~~~~~~~~~~~~~~~~~~~~~~~~
2091 When trying to match a dictionary (D tau) to a top-level instance, or a
2092 type family equation (F taus_1 ~ tau_2) to a top-level family instance,
2093 we do *not* need to expand type synonyms because the matcher will do that for us.
2094
2095 Note [Improvement orientation]
2096 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2097 A very delicate point is the orientation of derived equalities
2098 arising from injectivity improvement (Trac #12522). Suppse we have
2099 type family F x = t | t -> x
2100 type instance F (a, Int) = (Int, G a)
2101 where G is injective; and wanted constraints
2102
2103 [W] TF (alpha, beta) ~ fuv
2104 [W] fuv ~ (Int, <some type>)
2105
2106 The injectivity will give rise to derived constraints
2107
2108 [D] gamma1 ~ alpha
2109 [D] Int ~ beta
2110
2111 The fresh unification variable gamma1 comes from the fact that we
2112 can only do "partial improvement" here; see Section 5.2 of
2113 "Injective type families for Haskell" (HS'15).
2114
2115 Now, it's very important to orient the equations this way round,
2116 so that the fresh unification variable will be eliminated in
2117 favour of alpha. If we instead had
2118 [D] alpha ~ gamma1
2119 then we would unify alpha := gamma1; and kick out the wanted
2120 constraint. But when we grough it back in, it'd look like
2121 [W] TF (gamma1, beta) ~ fuv
2122 and exactly the same thing would happen again! Infinite loop.
2123
2124 This all seems fragile, and it might seem more robust to avoid
2125 introducing gamma1 in the first place, in the case where the
2126 actual argument (alpha, beta) partly matches the improvement
2127 template. But that's a bit tricky, esp when we remember that the
2128 kinds much match too; so it's easier to let the normal machinery
2129 handle it. Instead we are careful to orient the new derived
2130 equality with the template on the left. Delicate, but it works.
2131
2132 Note [No FunEq improvement for Givens]
2133 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2134 We don't do improvements (injectivity etc) for Givens. Why?
2135
2136 * It generates Derived constraints on skolems, which don't do us
2137 much good, except perhaps identify inaccessible branches.
2138 (They'd be perfectly valid though.)
2139
2140 * For type-nat stuff the derived constraints include type families;
2141 e.g. (a < b), (b < c) ==> a < c If we generate a Derived for this,
2142 we'll generate a Derived/Wanted CFunEqCan; and, since the same
2143 InertCans (after solving Givens) are used for each iteration, that
2144 massively confused the unflattening step (TcFlatten.unflatten).
2145
2146 In fact it led to some infinite loops:
2147 indexed-types/should_compile/T10806
2148 indexed-types/should_compile/T10507
2149 polykinds/T10742
2150
2151 Note [Reduction for Derived CFunEqCans]
2152 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2153 You may wonder if it's important to use top-level instances to
2154 simplify [D] CFunEqCan's. But it is. Here's an example (T10226).
2155
2156 type instance F Int = Int
2157 type instance FInv Int = Int
2158
2159 Suppose we have to solve
2160 [WD] FInv (F alpha) ~ alpha
2161 [WD] F alpha ~ Int
2162
2163 --> flatten
2164 [WD] F alpha ~ fuv0
2165 [WD] FInv fuv0 ~ fuv1 -- (A)
2166 [WD] fuv1 ~ alpha
2167 [WD] fuv0 ~ Int -- (B)
2168
2169 --> Rewwrite (A) with (B), splitting it
2170 [WD] F alpha ~ fuv0
2171 [W] FInv fuv0 ~ fuv1
2172 [D] FInv Int ~ fuv1 -- (C)
2173 [WD] fuv1 ~ alpha
2174 [WD] fuv0 ~ Int
2175
2176 --> Reduce (C) with top-level instance
2177 **** This is the key step ***
2178 [WD] F alpha ~ fuv0
2179 [W] FInv fuv0 ~ fuv1
2180 [D] fuv1 ~ Int -- (D)
2181 [WD] fuv1 ~ alpha -- (E)
2182 [WD] fuv0 ~ Int
2183
2184 --> Rewrite (D) with (E)
2185 [WD] F alpha ~ fuv0
2186 [W] FInv fuv0 ~ fuv1
2187 [D] alpha ~ Int -- (F)
2188 [WD] fuv1 ~ alpha
2189 [WD] fuv0 ~ Int
2190
2191 --> unify (F) alpha := Int, and that solves it
2192
2193 Another example is indexed-types/should_compile/T10634
2194 -}
2195
2196 {- *******************************************************************
2197 * *
2198 Top-level reaction for class constraints (CDictCan)
2199 * *
2200 **********************************************************************-}
2201
2202 doTopReactDict :: InertSet -> Ct -> TcS (StopOrContinue Ct)
2203 -- Try to use type-class instance declarations to simplify the constraint
2204 doTopReactDict inerts work_item@(CDictCan { cc_ev = ev, cc_class = cls
2205 , cc_tyargs = xis })
2206 | isGiven ev -- Never use instances for Given constraints
2207 = do { try_fundep_improvement
2208 ; continueWith work_item }
2209
2210 | Just solved_ev <- lookupSolvedDict inerts dict_loc cls xis -- Cached
2211 = do { setEvBindIfWanted ev (ctEvTerm solved_ev)
2212 ; stopWith ev "Dict/Top (cached)" }
2213
2214 | otherwise -- Wanted or Derived, but not cached
2215 = do { dflags <- getDynFlags
2216 ; lkup_res <- matchClassInst dflags inerts cls xis dict_loc
2217 ; case lkup_res of
2218 OneInst { cir_what = what }
2219 -> do { unless (safeOverlap what) $
2220 insertSafeOverlapFailureTcS work_item
2221 ; when (isWanted ev) $ addSolvedDict ev cls xis
2222 ; chooseInstance work_item lkup_res }
2223 _ -> -- NoInstance or NotSure
2224 do { when (isImprovable ev) $
2225 try_fundep_improvement
2226 ; continueWith work_item } }
2227 where
2228 dict_pred = mkClassPred cls xis
2229 dict_loc = ctEvLoc ev
2230 dict_origin = ctLocOrigin dict_loc
2231
2232 -- We didn't solve it; so try functional dependencies with
2233 -- the instance environment, and return
2234 -- See also Note [Weird fundeps]
2235 try_fundep_improvement
2236 = do { traceTcS "try_fundeps" (ppr work_item)
2237 ; instEnvs <- getInstEnvs
2238 ; emitFunDepDeriveds $
2239 improveFromInstEnv instEnvs mk_ct_loc dict_pred }
2240
2241 mk_ct_loc :: PredType -- From instance decl
2242 -> SrcSpan -- also from instance deol
2243 -> CtLoc
2244 mk_ct_loc inst_pred inst_loc
2245 = dict_loc { ctl_origin = FunDepOrigin2 dict_pred dict_origin
2246 inst_pred inst_loc }
2247
2248 doTopReactDict _ w = pprPanic "doTopReactDict" (ppr w)
2249
2250
2251 chooseInstance :: Ct -> ClsInstResult -> TcS (StopOrContinue Ct)
2252 chooseInstance work_item
2253 (OneInst { cir_new_theta = theta
2254 , cir_what = what
2255 , cir_mk_ev = mk_ev })
2256 = do { traceTcS "doTopReact/found instance for" $ ppr ev
2257 ; deeper_loc <- checkInstanceOK loc what pred
2258 ; if isDerived ev then finish_derived deeper_loc theta
2259 else finish_wanted deeper_loc theta mk_ev }
2260 where
2261 ev = ctEvidence work_item
2262 pred = ctEvPred ev
2263 loc = ctEvLoc ev
2264
2265 finish_wanted :: CtLoc -> [TcPredType]
2266 -> ([EvExpr] -> EvTerm) -> TcS (StopOrContinue Ct)
2267 -- Precondition: evidence term matches the predicate workItem
2268 finish_wanted loc theta mk_ev
2269 = do { evb <- getTcEvBindsVar
2270 ; if isNoEvBindsVar evb
2271 then -- See Note [Instances in no-evidence implications]
2272 continueWith work_item
2273 else
2274 do { evc_vars <- mapM (newWanted loc) theta
2275 ; setEvBindIfWanted ev (mk_ev (map getEvExpr evc_vars))
2276 ; emitWorkNC (freshGoals evc_vars)
2277 ; stopWith ev "Dict/Top (solved wanted)" } }
2278
2279 finish_derived loc theta
2280 = -- Use type-class instances for Deriveds, in the hope
2281 -- of generating some improvements
2282 -- C.f. Example 3 of Note [The improvement story]
2283 -- It's easy because no evidence is involved
2284 do { emitNewDeriveds loc theta
2285 ; traceTcS "finish_derived" (ppr (ctl_depth loc))
2286 ; stopWith ev "Dict/Top (solved derived)" }
2287
2288 chooseInstance work_item lookup_res
2289 = pprPanic "chooseInstance" (ppr work_item $$ ppr lookup_res)
2290
2291 checkInstanceOK :: CtLoc -> InstanceWhat -> TcPredType -> TcS CtLoc
2292 -- Check that it's OK to use this insstance:
2293 -- (a) the use is well staged in the Template Haskell sense
2294 -- (b) we have not recursed too deep
2295 -- Returns the CtLoc to used for sub-goals
2296 checkInstanceOK loc what pred
2297 = do { checkWellStagedDFun loc what pred
2298 ; checkReductionDepth deeper_loc pred
2299 ; return deeper_loc }
2300 where
2301 deeper_loc = zap_origin (bumpCtLocDepth loc)
2302 origin = ctLocOrigin loc
2303
2304 zap_origin loc -- After applying an instance we can set ScOrigin to
2305 -- infinity, so that prohibitedSuperClassSolve never fires
2306 | ScOrigin {} <- origin
2307 = setCtLocOrigin loc (ScOrigin infinity)
2308 | otherwise
2309 = loc
2310
2311 {- Note [Instances in no-evidence implications]
2312 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2313 In Trac #15290 we had
2314 [G] forall p q. Coercible p q => Coercible (m p) (m q))
2315 [W] forall <no-ev> a. m (Int, IntStateT m a)
2316 ~R#
2317 m (Int, StateT Int m a)
2318
2319 The Given is an ordinary quantified constraint; the Wanted is an implication
2320 equality that arises from
2321 [W] (forall a. t1) ~R# (forall a. t2)
2322
2323 But because the (t1 ~R# t2) is solved "inside a type" (under that forall a)
2324 we can't generate any term evidence. So we can't actually use that
2325 lovely quantified constraint. Alas!
2326
2327 This test arranges to ignore the instance-based solution under these
2328 (rare) circumstances. It's sad, but I really don't see what else we can do.
2329 -}
2330
2331
2332 matchClassInst :: DynFlags -> InertSet
2333 -> Class -> [Type]
2334 -> CtLoc -> TcS ClsInstResult
2335 matchClassInst dflags inerts clas tys loc
2336 -- First check whether there is an in-scope Given that could
2337 -- match this constraint. In that case, do not use any instance
2338 -- whether top level, or local quantified constraints.
2339 -- ee Note [Instance and Given overlap]
2340 | not (xopt LangExt.IncoherentInstances dflags)
2341 , not (naturallyCoherentClass clas)
2342 , let matchable_givens = matchableGivens loc pred inerts
2343 , not (isEmptyBag matchable_givens)
2344 = do { traceTcS "Delaying instance application" $
2345 vcat [ text "Work item=" <+> pprClassPred clas tys
2346 , text "Potential matching givens:" <+> ppr matchable_givens ]
2347 ; return NotSure }
2348
2349 | otherwise
2350 = do { traceTcS "matchClassInst" $ text "pred =" <+> ppr pred <+> char '{'
2351 ; local_res <- matchLocalInst pred loc
2352 ; case local_res of
2353 OneInst {} -> -- See Note [Local instances and incoherence]
2354 do { traceTcS "} matchClassInst local match" $ ppr local_res
2355 ; return local_res }
2356
2357 NotSure -> -- In the NotSure case for local instances
2358 -- we don't want to try global instances
2359 do { traceTcS "} matchClassInst local not sure" empty
2360 ; return local_res }
2361
2362 NoInstance -- No local instances, so try global ones
2363 -> do { global_res <- matchGlobalInst dflags False clas tys
2364 ; traceTcS "} matchClassInst global result" $ ppr global_res
2365 ; return global_res } }
2366 where
2367 pred = mkClassPred clas tys
2368
2369 -- | If a class is "naturally coherent", then we needn't worry at all, in any
2370 -- way, about overlapping/incoherent instances. Just solve the thing!
2371 -- See Note [Naturally coherent classes]
2372 -- See also Note [The equality class story] in TysPrim.
2373 naturallyCoherentClass :: Class -> Bool
2374 naturallyCoherentClass cls
2375 = isCTupleClass cls
2376 || cls `hasKey` heqTyConKey
2377 || cls `hasKey` eqTyConKey
2378 || cls `hasKey` coercibleTyConKey
2379
2380
2381 {- Note [Instance and Given overlap]
2382 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2383 Example, from the OutsideIn(X) paper:
2384 instance P x => Q [x]
2385 instance (x ~ y) => R y [x]
2386
2387 wob :: forall a b. (Q [b], R b a) => a -> Int
2388
2389 g :: forall a. Q [a] => [a] -> Int
2390 g x = wob x
2391
2392 From 'g' we get the impliation constraint:
2393 forall a. Q [a] => (Q [beta], R beta [a])
2394 If we react (Q [beta]) with its top-level axiom, we end up with a
2395 (P beta), which we have no way of discharging. On the other hand,
2396 if we react R beta [a] with the top-level we get (beta ~ a), which
2397 is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
2398 now solvable by the given Q [a].
2399
2400 The partial solution is that:
2401 In matchClassInst (and thus in topReact), we return a matching
2402 instance only when there is no Given in the inerts which is
2403 unifiable to this particular dictionary.
2404
2405 We treat any meta-tyvar as "unifiable" for this purpose,
2406 *including* untouchable ones. But not skolems like 'a' in
2407 the implication constraint above.
2408
2409 The end effect is that, much as we do for overlapping instances, we
2410 delay choosing a class instance if there is a possibility of another
2411 instance OR a given to match our constraint later on. This fixes
2412 Trac #4981 and #5002.
2413
2414 Other notes:
2415
2416 * The check is done *first*, so that it also covers classes
2417 with built-in instance solving, such as
2418 - constraint tuples
2419 - natural numbers
2420 - Typeable
2421
2422 * Flatten-skolems: we do not treat a flatten-skolem as unifiable
2423 for this purpose.
2424 E.g. f :: Eq (F a) => [a] -> [a]
2425 f xs = ....(xs==xs).....
2426 Here we get [W] Eq [a], and we don't want to refrain from solving
2427 it because of the given (Eq (F a)) constraint!
2428
2429 * The given-overlap problem is arguably not easy to appear in practice
2430 due to our aggressive prioritization of equality solving over other
2431 constraints, but it is possible. I've added a test case in
2432 typecheck/should-compile/GivenOverlapping.hs
2433
2434 * Another "live" example is Trac #10195; another is #10177.
2435
2436 * We ignore the overlap problem if -XIncoherentInstances is in force:
2437 see Trac #6002 for a worked-out example where this makes a
2438 difference.
2439
2440 * Moreover notice that our goals here are different than the goals of
2441 the top-level overlapping checks. There we are interested in
2442 validating the following principle:
2443
2444 If we inline a function f at a site where the same global
2445 instance environment is available as the instance environment at
2446 the definition site of f then we should get the same behaviour.
2447
2448 But for the Given Overlap check our goal is just related to completeness of
2449 constraint solving.
2450
2451 * The solution is only a partial one. Consider the above example with
2452 g :: forall a. Q [a] => [a] -> Int
2453 g x = let v = wob x
2454 in v
2455 and suppose we have -XNoMonoLocalBinds, so that we attempt to find the most
2456 general type for 'v'. When generalising v's type we'll simplify its
2457 Q [alpha] constraint, but we don't have Q [a] in the 'givens', so we
2458 will use the instance declaration after all. Trac #11948 was a case
2459 in point.
2460
2461 All of this is disgustingly delicate, so to discourage people from writing
2462 simplifiable class givens, we warn about signatures that contain them;
2463 see TcValidity Note [Simplifiable given constraints].
2464
2465 Note [Naturally coherent classes]
2466 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2467 A few built-in classes are "naturally coherent". This term means that
2468 the "instance" for the class is bidirectional with its superclass(es).
2469 For example, consider (~~), which behaves as if it was defined like
2470 this:
2471 class a ~# b => a ~~ b
2472 instance a ~# b => a ~~ b
2473 (See Note [The equality types story] in TysPrim.)
2474
2475 Faced with [W] t1 ~~ t2, it's always OK to reduce it to [W] t1 ~# t2,
2476 without worrying about Note [Instance and Given overlap]. Why? Because
2477 if we had [G] s1 ~~ s2, then we'd get the superclass [G] s1 ~# s2, and
2478 so the reduction of the [W] constraint does not risk losing any solutions.
2479
2480 On the other hand, it can be fatal to /fail/ to reduce such
2481 equalities, on the grounds of Note [Instance and Given overlap],
2482 because many good things flow from [W] t1 ~# t2.
2483
2484 The same reasoning applies to
2485
2486 * (~~) heqTyCOn
2487 * (~) eqTyCon
2488 * Coercible coercibleTyCon
2489
2490 And less obviously to:
2491
2492 * Tuple classes. For reasons described in TcSMonad
2493 Note [Tuples hiding implicit parameters], we may have a constraint
2494 [W] (?x::Int, C a)
2495 with an exactly-matching Given constraint. We must decompose this
2496 tuple and solve the components separately, otherwise we won't solve
2497 it at all! It is perfectly safe to decompose it, because again the
2498 superclasses invert the instance; e.g.
2499 class (c1, c2) => (% c1, c2 %)
2500 instance (c1, c2) => (% c1, c2 %)
2501 Example in Trac #14218
2502
2503 Exammples: T5853, T10432, T5315, T9222, T2627b, T3028b
2504
2505 PS: the term "naturally coherent" doesn't really seem helpful.
2506 Perhaps "invertible" or something? I left it for now though.
2507
2508 Note [Local instances and incoherence]
2509 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2510 Consider
2511 f :: forall b c. (Eq b, forall a. Eq a => Eq (c a))
2512 => c b -> Bool
2513 f x = x==x
2514
2515 We get [W] Eq (c b), and we must use the local instance to solve it.
2516
2517 BUT that wanted also unifies with the top-level Eq [a] instance,
2518 and Eq (Maybe a) etc. We want the local instance to "win", otherwise
2519 we can't solve the wanted at all. So we mark it as Incohherent.
2520 According to Note [Rules for instance lookup] in InstEnv, that'll
2521 make it win even if there are other instances that unify.
2522
2523 Moreover this is not a hack! The evidence for this local instance
2524 will be constructed by GHC at a call site... from the very instances
2525 that unify with it here. It is not like an incoherent user-written
2526 instance which might have utterly different behaviour.
2527
2528 Consdider f :: Eq a => blah. If we have [W] Eq a, we certainly
2529 get it from the Eq a context, without worrying that there are
2530 lots of top-level instances that unify with [W] Eq a! We'll use
2531 those instances to build evidence to pass to f. That's just the
2532 nullary case of what's happening here.
2533 -}
2534
2535 matchLocalInst :: TcPredType -> CtLoc -> TcS ClsInstResult
2536 -- Try any Given quantified constraints, which are
2537 -- effectively just local instance declarations.
2538 matchLocalInst pred loc
2539 = do { ics <- getInertCans
2540 ; case match_local_inst (inert_insts ics) of
2541 ([], False) -> return NoInstance
2542 ([(dfun_ev, inst_tys)], unifs)
2543 | not unifs
2544 -> do { let dfun_id = ctEvEvId dfun_ev
2545 ; (tys, theta) <- instDFunType dfun_id inst_tys
2546 ; return $ OneInst { cir_new_theta = theta
2547 , cir_mk_ev = evDFunApp dfun_id tys
2548 , cir_what = LocalInstance } }
2549 _ -> return NotSure }
2550 where
2551 pred_tv_set = tyCoVarsOfType pred
2552
2553 match_local_inst :: [QCInst]
2554 -> ( [(CtEvidence, [DFunInstType])]
2555 , Bool ) -- True <=> Some unify but do not match
2556 match_local_inst []
2557 = ([], False)
2558 match_local_inst (qci@(QCI { qci_tvs = qtvs, qci_pred = qpred
2559 , qci_ev = ev })
2560 : qcis)
2561 | let in_scope = mkInScopeSet (qtv_set `unionVarSet` pred_tv_set)
2562 , Just tv_subst <- ruleMatchTyKiX qtv_set (mkRnEnv2 in_scope)
2563 emptyTvSubstEnv qpred pred
2564 , let match = (ev, map (lookupVarEnv tv_subst) qtvs)
2565 = (match:matches, unif)
2566
2567 | otherwise
2568 = ASSERT2( disjointVarSet qtv_set (tyCoVarsOfType pred)
2569 , ppr qci $$ ppr pred )
2570 -- ASSERT: unification relies on the
2571 -- quantified variables being fresh
2572 (matches, unif || this_unif)
2573 where
2574 qtv_set = mkVarSet qtvs
2575 this_unif = mightMatchLater qpred (ctEvLoc ev) pred loc
2576 (matches, unif) = match_local_inst qcis
2577