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