3914db6c13e208963074baf05654b4f547dd2105
[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: overlap]
925 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
926 Suppose we have
927 instance {-# OVERLAPPABLE #-} C a where ...
928 and we are typechecking
929 f :: C a => a -> a
930 f = e -- Gives rise to [W] C a
931
932 We don't want to solve the wanted constraint with the overlappable
933 instance; rather we want to use the supplied (C a)! That was the whole
934 point of it being overlappable! Trac #14434 wwas an example.
935
936 Note [Shortcut solving: incoherence]
937 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
938 This optimization relies on coherence of dictionaries to be correct. When we
939 cannot assume coherence because of IncoherentInstances then this optimization
940 can change the behavior of the user's code.
941
942 The following four modules produce a program whose output would change depending
943 on whether we apply this optimization when IncoherentInstances is in effect:
944
945 #########
946 {-# LANGUAGE MultiParamTypeClasses #-}
947 module A where
948
949 class A a where
950 int :: a -> Int
951
952 class A a => C a b where
953 m :: b -> a -> a
954
955 #########
956 {-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
957 module B where
958
959 import A
960
961 instance A a where
962 int _ = 1
963
964 instance C a [b] where
965 m _ = id
966
967 #########
968 {-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, FlexibleContexts #-}
969 {-# LANGUAGE IncoherentInstances #-}
970 module C where
971
972 import A
973
974 instance A Int where
975 int _ = 2
976
977 instance C Int [Int] where
978 m _ = id
979
980 intC :: C Int a => a -> Int -> Int
981 intC _ x = int x
982
983 #########
984 module Main where
985
986 import A
987 import B
988 import C
989
990 main :: IO ()
991 main = print (intC [] (0::Int))
992
993 The output of `main` if we avoid the optimization under the effect of
994 IncoherentInstances is `1`. If we were to do the optimization, the output of
995 `main` would be `2`.
996
997 Note [Shortcut try_solve_from_instance]
998 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
999 The workhorse of the short-cut solver is
1000 try_solve_from_instance :: (EvBindMap, DictMap CtEvidence)
1001 -> CtEvidence -- Solve this
1002 -> MaybeT TcS (EvBindMap, DictMap CtEvidence)
1003 Note that:
1004
1005 * The CtEvidence is teh goal to be solved
1006
1007 * The MaybeT anages early failure if we find a subgoal that
1008 cannot be solved from instances.
1009
1010 * The (EvBindMap, DictMap CtEvidence) is an accumulating purely-functional
1011 state that allows try_solve_from_instance to augmennt the evidence
1012 bindings and inert_solved_dicts as it goes.
1013
1014 If it succeeds, we commit all these bindings and solved dicts to the
1015 main TcS InertSet. If not, we abandon it all entirely.
1016
1017 Passing along the solved_dicts important for two reasons:
1018
1019 * We need to be able to handle recursive super classes. The
1020 solved_dicts state ensures that we remember what we have already
1021 tried to solve to avoid looping.
1022
1023 * As Trac #15164 showed, it can be important to exploit sharing between
1024 goals. E.g. To solve G we may need G1 and G2. To solve G1 we may need H;
1025 and to solve G2 we may need H. If we don't spot this sharing we may
1026 solve H twice; and if this pattern repeats we may get exponentially bad
1027 behaviour.
1028 -}
1029
1030 interactDict :: InertCans -> Ct -> TcS (StopOrContinue Ct)
1031 interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs = tys })
1032 | Just ev_i <- lookupInertDict inerts (ctEvLoc ev_w) cls tys
1033 = -- There is a matching dictionary in the inert set
1034 do { -- First to try to solve it /completely/ from top level instances
1035 -- See Note [Shortcut solving]
1036 dflags <- getDynFlags
1037 ; short_cut_worked <- shortCutSolver dflags ev_w ev_i
1038 ; if short_cut_worked
1039 then stopWith ev_w "interactDict/solved from instance"
1040 else
1041
1042 do { -- Ths short-cut solver didn't fire, so we
1043 -- solve ev_w from the matching inert ev_i we found
1044 what_next <- solveOneFromTheOther ev_i ev_w
1045 ; traceTcS "lookupInertDict" (ppr what_next)
1046 ; case what_next of
1047 KeepInert -> do { setEvBindIfWanted ev_w (ctEvTerm ev_i)
1048 ; return $ Stop ev_w (text "Dict equal" <+> parens (ppr what_next)) }
1049 KeepWork -> do { setEvBindIfWanted ev_i (ctEvTerm ev_w)
1050 ; updInertDicts $ \ ds -> delDict ds cls tys
1051 ; continueWith workItem } } }
1052
1053 | cls `hasKey` ipClassKey
1054 , isGiven ev_w
1055 = interactGivenIP inerts workItem
1056
1057 | otherwise
1058 = do { addFunDepWork inerts ev_w cls
1059 ; continueWith workItem }
1060
1061 interactDict _ wi = pprPanic "interactDict" (ppr wi)
1062
1063 -- See Note [Shortcut solving]
1064 shortCutSolver :: DynFlags
1065 -> CtEvidence -- Work item
1066 -> CtEvidence -- Inert we want to try to replace
1067 -> TcS Bool -- True <=> success
1068 shortCutSolver dflags ev_w ev_i
1069 | isWanted ev_w
1070 && isGiven ev_i
1071 -- We are about to solve a [W] constraint from a [G] constraint. We take
1072 -- a moment to see if we can get a better solution using an instance.
1073 -- Note that we only do this for the sake of performance. Exactly the same
1074 -- programs should typecheck regardless of whether we take this step or
1075 -- not. See Note [Shortcut solving]
1076
1077 && not (xopt LangExt.IncoherentInstances dflags)
1078 -- If IncoherentInstances is on then we cannot rely on coherence of proofs
1079 -- in order to justify this optimization: The proof provided by the
1080 -- [G] constraint's superclass may be different from the top-level proof.
1081 -- See Note [Shortcut solving: incoherence]
1082
1083 && gopt Opt_SolveConstantDicts dflags
1084 -- Enabled by the -fsolve-constant-dicts flag
1085 = do { ev_binds_var <- getTcEvBindsVar
1086 ; ev_binds <- ASSERT2( not (isCoEvBindsVar ev_binds_var ), ppr ev_w )
1087 getTcEvBindsMap ev_binds_var
1088 ; solved_dicts <- getSolvedDicts
1089
1090 ; mb_stuff <- runMaybeT $ try_solve_from_instance
1091 (ev_binds, solved_dicts) ev_w
1092
1093 ; case mb_stuff of
1094 Nothing -> return False
1095 Just (ev_binds', solved_dicts')
1096 -> do { setTcEvBindsMap ev_binds_var ev_binds'
1097 ; setSolvedDicts solved_dicts'
1098 ; return True } }
1099
1100 | otherwise
1101 = return False
1102 where
1103 -- This `CtLoc` is used only to check the well-staged condition of any
1104 -- candidate DFun. Our subgoals all have the same stage as our root
1105 -- [W] constraint so it is safe to use this while solving them.
1106 loc_w = ctEvLoc ev_w
1107
1108 try_solve_from_instance -- See Note [Shortcut try_solve_from_instance]
1109 :: (EvBindMap, DictMap CtEvidence) -> CtEvidence
1110 -> MaybeT TcS (EvBindMap, DictMap CtEvidence)
1111 try_solve_from_instance (ev_binds, solved_dicts) ev
1112 | let pred = ctEvPred ev
1113 loc = ctEvLoc ev
1114 , ClassPred cls tys <- classifyPredType pred
1115 = do { inst_res <- lift $ matchGlobalInst dflags True cls tys
1116 ; case inst_res of
1117 OneInst { cir_new_theta = preds
1118 , cir_mk_ev = mk_ev
1119 , cir_what = what }
1120 | safeOverlap what
1121 , all isTyFamFree preds -- Note [Shortcut solving: type families]
1122 -> do { let solved_dicts' = addDict solved_dicts cls tys ev
1123 -- solved_dicts': it is important that we add our goal
1124 -- to the cache before we solve! Otherwise we may end
1125 -- up in a loop while solving recursive dictionaries.
1126
1127 ; lift $ traceTcS "shortCutSolver: found instance" (ppr preds)
1128 ; loc' <- lift $ checkInstanceOK loc what pred
1129
1130 ; evc_vs <- mapM (new_wanted_cached loc' solved_dicts') preds
1131 -- Emit work for subgoals but use our local cache
1132 -- so we can solve recursive dictionaries.
1133
1134 ; let ev_tm = mk_ev (map getEvExpr evc_vs)
1135 ev_binds' = extendEvBinds ev_binds $
1136 mkWantedEvBind (ctEvEvId ev) ev_tm
1137
1138 ; foldlM try_solve_from_instance
1139 (ev_binds', solved_dicts')
1140 (freshGoals evc_vs) }
1141
1142 _ -> mzero }
1143 | otherwise = mzero
1144
1145
1146 -- Use a local cache of solved dicts while emitting EvVars for new work
1147 -- We bail out of the entire computation if we need to emit an EvVar for
1148 -- a subgoal that isn't a ClassPred.
1149 new_wanted_cached :: CtLoc -> DictMap CtEvidence -> TcPredType -> MaybeT TcS MaybeNew
1150 new_wanted_cached loc cache pty
1151 | ClassPred cls tys <- classifyPredType pty
1152 = lift $ case findDict cache loc_w cls tys of
1153 Just ctev -> return $ Cached (ctEvExpr ctev)
1154 Nothing -> Fresh <$> newWantedNC loc pty
1155 | otherwise = mzero
1156
1157 addFunDepWork :: InertCans -> CtEvidence -> Class -> TcS ()
1158 -- Add derived constraints from type-class functional dependencies.
1159 addFunDepWork inerts work_ev cls
1160 | isImprovable work_ev
1161 = mapBagM_ add_fds (findDictsByClass (inert_dicts inerts) cls)
1162 -- No need to check flavour; fundeps work between
1163 -- any pair of constraints, regardless of flavour
1164 -- Importantly we don't throw workitem back in the
1165 -- worklist because this can cause loops (see #5236)
1166 | otherwise
1167 = return ()
1168 where
1169 work_pred = ctEvPred work_ev
1170 work_loc = ctEvLoc work_ev
1171
1172 add_fds inert_ct
1173 | isImprovable inert_ev
1174 = do { traceTcS "addFunDepWork" (vcat
1175 [ ppr work_ev
1176 , pprCtLoc work_loc, ppr (isGivenLoc work_loc)
1177 , pprCtLoc inert_loc, ppr (isGivenLoc inert_loc)
1178 , pprCtLoc derived_loc, ppr (isGivenLoc derived_loc) ]) ;
1179
1180 emitFunDepDeriveds $
1181 improveFromAnother derived_loc inert_pred work_pred
1182 -- We don't really rewrite tys2, see below _rewritten_tys2, so that's ok
1183 -- NB: We do create FDs for given to report insoluble equations that arise
1184 -- from pairs of Givens, and also because of floating when we approximate
1185 -- implications. The relevant test is: typecheck/should_fail/FDsFromGivens.hs
1186 }
1187 | otherwise
1188 = return ()
1189 where
1190 inert_ev = ctEvidence inert_ct
1191 inert_pred = ctEvPred inert_ev
1192 inert_loc = ctEvLoc inert_ev
1193 derived_loc = work_loc { ctl_depth = ctl_depth work_loc `maxSubGoalDepth`
1194 ctl_depth inert_loc
1195 , ctl_origin = FunDepOrigin1 work_pred work_loc
1196 inert_pred inert_loc }
1197
1198 {-
1199 **********************************************************************
1200 * *
1201 Implicit parameters
1202 * *
1203 **********************************************************************
1204 -}
1205
1206 interactGivenIP :: InertCans -> Ct -> TcS (StopOrContinue Ct)
1207 -- Work item is Given (?x:ty)
1208 -- See Note [Shadowing of Implicit Parameters]
1209 interactGivenIP inerts workItem@(CDictCan { cc_ev = ev, cc_class = cls
1210 , cc_tyargs = tys@(ip_str:_) })
1211 = do { updInertCans $ \cans -> cans { inert_dicts = addDict filtered_dicts cls tys workItem }
1212 ; stopWith ev "Given IP" }
1213 where
1214 dicts = inert_dicts inerts
1215 ip_dicts = findDictsByClass dicts cls
1216 other_ip_dicts = filterBag (not . is_this_ip) ip_dicts
1217 filtered_dicts = addDictsByClass dicts cls other_ip_dicts
1218
1219 -- Pick out any Given constraints for the same implicit parameter
1220 is_this_ip (CDictCan { cc_ev = ev, cc_tyargs = ip_str':_ })
1221 = isGiven ev && ip_str `tcEqType` ip_str'
1222 is_this_ip _ = False
1223
1224 interactGivenIP _ wi = pprPanic "interactGivenIP" (ppr wi)
1225
1226 {- Note [Shadowing of Implicit Parameters]
1227 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1228 Consider the following example:
1229
1230 f :: (?x :: Char) => Char
1231 f = let ?x = 'a' in ?x
1232
1233 The "let ?x = ..." generates an implication constraint of the form:
1234
1235 ?x :: Char => ?x :: Char
1236
1237 Furthermore, the signature for `f` also generates an implication
1238 constraint, so we end up with the following nested implication:
1239
1240 ?x :: Char => (?x :: Char => ?x :: Char)
1241
1242 Note that the wanted (?x :: Char) constraint may be solved in
1243 two incompatible ways: either by using the parameter from the
1244 signature, or by using the local definition. Our intention is
1245 that the local definition should "shadow" the parameter of the
1246 signature, and we implement this as follows: when we add a new
1247 *given* implicit parameter to the inert set, it replaces any existing
1248 givens for the same implicit parameter.
1249
1250 Similarly, consider
1251 f :: (?x::a) => Bool -> a
1252
1253 g v = let ?x::Int = 3
1254 in (f v, let ?x::Bool = True in f v)
1255
1256 This should probably be well typed, with
1257 g :: Bool -> (Int, Bool)
1258
1259 So the inner binding for ?x::Bool *overrides* the outer one.
1260
1261 All this works for the normal cases but it has an odd side effect in
1262 some pathological programs like this:
1263 -- This is accepted, the second parameter shadows
1264 f1 :: (?x :: Int, ?x :: Char) => Char
1265 f1 = ?x
1266
1267 -- This is rejected, the second parameter shadows
1268 f2 :: (?x :: Int, ?x :: Char) => Int
1269 f2 = ?x
1270
1271 Both of these are actually wrong: when we try to use either one,
1272 we'll get two incompatible wanted constraints (?x :: Int, ?x :: Char),
1273 which would lead to an error.
1274
1275 I can think of two ways to fix this:
1276
1277 1. Simply disallow multiple constraints for the same implicit
1278 parameter---this is never useful, and it can be detected completely
1279 syntactically.
1280
1281 2. Move the shadowing machinery to the location where we nest
1282 implications, and add some code here that will produce an
1283 error if we get multiple givens for the same implicit parameter.
1284
1285
1286 **********************************************************************
1287 * *
1288 interactFunEq
1289 * *
1290 **********************************************************************
1291 -}
1292
1293 interactFunEq :: InertCans -> Ct -> TcS (StopOrContinue Ct)
1294 -- Try interacting the work item with the inert set
1295 interactFunEq inerts work_item@(CFunEqCan { cc_ev = ev, cc_fun = tc
1296 , cc_tyargs = args, cc_fsk = fsk })
1297 | Just inert_ct@(CFunEqCan { cc_ev = ev_i
1298 , cc_fsk = fsk_i })
1299 <- findFunEq (inert_funeqs inerts) tc args
1300 , pr@(swap_flag, upgrade_flag) <- ev_i `funEqCanDischarge` ev
1301 = do { traceTcS "reactFunEq (rewrite inert item):" $
1302 vcat [ text "work_item =" <+> ppr work_item
1303 , text "inertItem=" <+> ppr ev_i
1304 , text "(swap_flag, upgrade)" <+> ppr pr ]
1305 ; if isSwapped swap_flag
1306 then do { -- Rewrite inert using work-item
1307 let work_item' | upgrade_flag = upgradeWanted work_item
1308 | otherwise = work_item
1309 ; updInertFunEqs $ \ feqs -> insertFunEq feqs tc args work_item'
1310 -- Do the updInertFunEqs before the reactFunEq, so that
1311 -- we don't kick out the inertItem as well as consuming it!
1312 ; reactFunEq ev fsk ev_i fsk_i
1313 ; stopWith ev "Work item rewrites inert" }
1314 else do { -- Rewrite work-item using inert
1315 ; when upgrade_flag $
1316 updInertFunEqs $ \ feqs -> insertFunEq feqs tc args
1317 (upgradeWanted inert_ct)
1318 ; reactFunEq ev_i fsk_i ev fsk
1319 ; stopWith ev "Inert rewrites work item" } }
1320
1321 | otherwise -- Try improvement
1322 = do { improveLocalFunEqs ev inerts tc args fsk
1323 ; continueWith work_item }
1324
1325 interactFunEq _ work_item = pprPanic "interactFunEq" (ppr work_item)
1326
1327 upgradeWanted :: Ct -> Ct
1328 -- We are combining a [W] F tys ~ fmv1 and [D] F tys ~ fmv2
1329 -- so upgrade the [W] to [WD] before putting it in the inert set
1330 upgradeWanted ct = ct { cc_ev = upgrade_ev (cc_ev ct) }
1331 where
1332 upgrade_ev ev = ASSERT2( isWanted ev, ppr ct )
1333 ev { ctev_nosh = WDeriv }
1334
1335 improveLocalFunEqs :: CtEvidence -> InertCans -> TyCon -> [TcType] -> TcTyVar
1336 -> TcS ()
1337 -- Generate derived improvement equalities, by comparing
1338 -- the current work item with inert CFunEqs
1339 -- E.g. x + y ~ z, x + y' ~ z => [D] y ~ y'
1340 --
1341 -- See Note [FunDep and implicit parameter reactions]
1342 improveLocalFunEqs work_ev inerts fam_tc args fsk
1343 | isGiven work_ev -- See Note [No FunEq improvement for Givens]
1344 || not (isImprovable work_ev)
1345 = return ()
1346
1347 | not (null improvement_eqns)
1348 = do { traceTcS "interactFunEq improvements: " $
1349 vcat [ text "Eqns:" <+> ppr improvement_eqns
1350 , text "Candidates:" <+> ppr funeqs_for_tc
1351 , text "Inert eqs:" <+> ppr ieqs ]
1352 ; emitFunDepDeriveds improvement_eqns }
1353
1354 | otherwise
1355 = return ()
1356
1357 where
1358 ieqs = inert_eqs inerts
1359 funeqs = inert_funeqs inerts
1360 funeqs_for_tc = findFunEqsByTyCon funeqs fam_tc
1361 rhs = lookupFlattenTyVar ieqs fsk
1362 work_loc = ctEvLoc work_ev
1363 work_pred = ctEvPred work_ev
1364 fam_inj_info = tyConInjectivityInfo fam_tc
1365
1366 --------------------
1367 improvement_eqns :: [FunDepEqn CtLoc]
1368 improvement_eqns
1369 | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc
1370 = -- Try built-in families, notably for arithmethic
1371 concatMap (do_one_built_in ops) funeqs_for_tc
1372
1373 | Injective injective_args <- fam_inj_info
1374 = -- Try improvement from type families with injectivity annotations
1375 concatMap (do_one_injective injective_args) funeqs_for_tc
1376
1377 | otherwise
1378 = []
1379
1380 --------------------
1381 do_one_built_in ops (CFunEqCan { cc_tyargs = iargs, cc_fsk = ifsk, cc_ev = inert_ev })
1382 = mk_fd_eqns inert_ev (sfInteractInert ops args rhs iargs
1383 (lookupFlattenTyVar ieqs ifsk))
1384
1385 do_one_built_in _ _ = pprPanic "interactFunEq 1" (ppr fam_tc)
1386
1387 --------------------
1388 -- See Note [Type inference for type families with injectivity]
1389 do_one_injective inj_args (CFunEqCan { cc_tyargs = inert_args
1390 , cc_fsk = ifsk, cc_ev = inert_ev })
1391 | isImprovable inert_ev
1392 , rhs `tcEqType` lookupFlattenTyVar ieqs ifsk
1393 = mk_fd_eqns inert_ev $
1394 [ Pair arg iarg
1395 | (arg, iarg, True) <- zip3 args inert_args inj_args ]
1396 | otherwise
1397 = []
1398
1399 do_one_injective _ _ = pprPanic "interactFunEq 2" (ppr fam_tc)
1400
1401 --------------------
1402 mk_fd_eqns :: CtEvidence -> [TypeEqn] -> [FunDepEqn CtLoc]
1403 mk_fd_eqns inert_ev eqns
1404 | null eqns = []
1405 | otherwise = [ FDEqn { fd_qtvs = [], fd_eqs = eqns
1406 , fd_pred1 = work_pred
1407 , fd_pred2 = ctEvPred inert_ev
1408 , fd_loc = loc } ]
1409 where
1410 inert_loc = ctEvLoc inert_ev
1411 loc = inert_loc { ctl_depth = ctl_depth inert_loc `maxSubGoalDepth`
1412 ctl_depth work_loc }
1413
1414 -------------
1415 reactFunEq :: CtEvidence -> TcTyVar -- From this :: F args1 ~ fsk1
1416 -> CtEvidence -> TcTyVar -- Solve this :: F args2 ~ fsk2
1417 -> TcS ()
1418 reactFunEq from_this fsk1 solve_this fsk2
1419 = do { traceTcS "reactFunEq"
1420 (vcat [ppr from_this, ppr fsk1, ppr solve_this, ppr fsk2])
1421 ; dischargeFunEq solve_this fsk2 (ctEvCoercion from_this) (mkTyVarTy fsk1)
1422 ; traceTcS "reactFunEq done" (ppr from_this $$ ppr fsk1 $$
1423 ppr solve_this $$ ppr fsk2) }
1424
1425 {- Note [Type inference for type families with injectivity]
1426 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1427 Suppose we have a type family with an injectivity annotation:
1428 type family F a b = r | r -> b
1429
1430 Then if we have two CFunEqCan constraints for F with the same RHS
1431 F s1 t1 ~ rhs
1432 F s2 t2 ~ rhs
1433 then we can use the injectivity to get a new Derived constraint on
1434 the injective argument
1435 [D] t1 ~ t2
1436
1437 That in turn can help GHC solve constraints that would otherwise require
1438 guessing. For example, consider the ambiguity check for
1439 f :: F Int b -> Int
1440 We get the constraint
1441 [W] F Int b ~ F Int beta
1442 where beta is a unification variable. Injectivity lets us pick beta ~ b.
1443
1444 Injectivity information is also used at the call sites. For example:
1445 g = f True
1446 gives rise to
1447 [W] F Int b ~ Bool
1448 from which we can derive b. This requires looking at the defining equations of
1449 a type family, ie. finding equation with a matching RHS (Bool in this example)
1450 and infering values of type variables (b in this example) from the LHS patterns
1451 of the matching equation. For closed type families we have to perform
1452 additional apartness check for the selected equation to check that the selected
1453 is guaranteed to fire for given LHS arguments.
1454
1455 These new constraints are simply *Derived* constraints; they have no evidence.
1456 We could go further and offer evidence from decomposing injective type-function
1457 applications, but that would require new evidence forms, and an extension to
1458 FC, so we don't do that right now (Dec 14).
1459
1460 See also Note [Injective type families] in TyCon
1461
1462
1463 Note [Cache-caused loops]
1464 ~~~~~~~~~~~~~~~~~~~~~~~~~
1465 It is very dangerous to cache a rewritten wanted family equation as 'solved' in our
1466 solved cache (which is the default behaviour or xCtEvidence), because the interaction
1467 may not be contributing towards a solution. Here is an example:
1468
1469 Initial inert set:
1470 [W] g1 : F a ~ beta1
1471 Work item:
1472 [W] g2 : F a ~ beta2
1473 The work item will react with the inert yielding the _same_ inert set plus:
1474 (i) Will set g2 := g1 `cast` g3
1475 (ii) Will add to our solved cache that [S] g2 : F a ~ beta2
1476 (iii) Will emit [W] g3 : beta1 ~ beta2
1477 Now, the g3 work item will be spontaneously solved to [G] g3 : beta1 ~ beta2
1478 and then it will react the item in the inert ([W] g1 : F a ~ beta1). So it
1479 will set
1480 g1 := g ; sym g3
1481 and what is g? Well it would ideally be a new goal of type (F a ~ beta2) but
1482 remember that we have this in our solved cache, and it is ... g2! In short we
1483 created the evidence loop:
1484
1485 g2 := g1 ; g3
1486 g3 := refl
1487 g1 := g2 ; sym g3
1488
1489 To avoid this situation we do not cache as solved any workitems (or inert)
1490 which did not really made a 'step' towards proving some goal. Solved's are
1491 just an optimization so we don't lose anything in terms of completeness of
1492 solving.
1493
1494
1495 Note [Efficient Orientation]
1496 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1497 Suppose we are interacting two FunEqCans with the same LHS:
1498 (inert) ci :: (F ty ~ xi_i)
1499 (work) cw :: (F ty ~ xi_w)
1500 We prefer to keep the inert (else we pass the work item on down
1501 the pipeline, which is a bit silly). If we keep the inert, we
1502 will (a) discharge 'cw'
1503 (b) produce a new equality work-item (xi_w ~ xi_i)
1504 Notice the orientation (xi_w ~ xi_i) NOT (xi_i ~ xi_w):
1505 new_work :: xi_w ~ xi_i
1506 cw := ci ; sym new_work
1507 Why? Consider the simplest case when xi1 is a type variable. If
1508 we generate xi1~xi2, porcessing that constraint will kick out 'ci'.
1509 If we generate xi2~xi1, there is less chance of that happening.
1510 Of course it can and should still happen if xi1=a, xi1=Int, say.
1511 But we want to avoid it happening needlessly.
1512
1513 Similarly, if we *can't* keep the inert item (because inert is Wanted,
1514 and work is Given, say), we prefer to orient the new equality (xi_i ~
1515 xi_w).
1516
1517 Note [Carefully solve the right CFunEqCan]
1518 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1519 ---- OLD COMMENT, NOW NOT NEEDED
1520 ---- because we now allow multiple
1521 ---- wanted FunEqs with the same head
1522 Consider the constraints
1523 c1 :: F Int ~ a -- Arising from an application line 5
1524 c2 :: F Int ~ Bool -- Arising from an application line 10
1525 Suppose that 'a' is a unification variable, arising only from
1526 flattening. So there is no error on line 5; it's just a flattening
1527 variable. But there is (or might be) an error on line 10.
1528
1529 Two ways to combine them, leaving either (Plan A)
1530 c1 :: F Int ~ a -- Arising from an application line 5
1531 c3 :: a ~ Bool -- Arising from an application line 10
1532 or (Plan B)
1533 c2 :: F Int ~ Bool -- Arising from an application line 10
1534 c4 :: a ~ Bool -- Arising from an application line 5
1535
1536 Plan A will unify c3, leaving c1 :: F Int ~ Bool as an error
1537 on the *totally innocent* line 5. An example is test SimpleFail16
1538 where the expected/actual message comes out backwards if we use
1539 the wrong plan.
1540
1541 The second is the right thing to do. Hence the isMetaTyVarTy
1542 test when solving pairwise CFunEqCan.
1543
1544
1545 **********************************************************************
1546 * *
1547 interactTyVarEq
1548 * *
1549 **********************************************************************
1550 -}
1551
1552 inertsCanDischarge :: InertCans -> TcTyVar -> TcType -> CtFlavourRole
1553 -> Maybe ( CtEvidence -- The evidence for the inert
1554 , SwapFlag -- Whether we need mkSymCo
1555 , Bool) -- True <=> keep a [D] version
1556 -- of the [WD] constraint
1557 inertsCanDischarge inerts tv rhs fr
1558 | (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i
1559 , cc_eq_rel = eq_rel }
1560 <- findTyEqs inerts tv
1561 , (ctEvFlavour ev_i, eq_rel) `eqCanDischargeFR` fr
1562 , rhs_i `tcEqType` rhs ]
1563 = -- Inert: a ~ ty
1564 -- Work item: a ~ ty
1565 Just (ev_i, NotSwapped, keep_deriv ev_i)
1566
1567 | Just tv_rhs <- getTyVar_maybe rhs
1568 , (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i
1569 , cc_eq_rel = eq_rel }
1570 <- findTyEqs inerts tv_rhs
1571 , (ctEvFlavour ev_i, eq_rel) `eqCanDischargeFR` fr
1572 , rhs_i `tcEqType` mkTyVarTy tv ]
1573 = -- Inert: a ~ b
1574 -- Work item: b ~ a
1575 Just (ev_i, IsSwapped, keep_deriv ev_i)
1576
1577 | otherwise
1578 = Nothing
1579
1580 where
1581 keep_deriv ev_i
1582 | Wanted WOnly <- ctEvFlavour ev_i -- inert is [W]
1583 , (Wanted WDeriv, _) <- fr -- work item is [WD]
1584 = True -- Keep a derived verison of the work item
1585 | otherwise
1586 = False -- Work item is fully discharged
1587
1588 interactTyVarEq :: InertCans -> Ct -> TcS (StopOrContinue Ct)
1589 -- CTyEqCans are always consumed, so always returns Stop
1590 interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv
1591 , cc_rhs = rhs
1592 , cc_ev = ev
1593 , cc_eq_rel = eq_rel })
1594 | Just (ev_i, swapped, keep_deriv)
1595 <- inertsCanDischarge inerts tv rhs (ctEvFlavour ev, eq_rel)
1596 = do { setEvBindIfWanted ev $
1597 evCoercion (maybeSym swapped $
1598 tcDowngradeRole (eqRelRole eq_rel)
1599 (ctEvRole ev_i)
1600 (ctEvCoercion ev_i))
1601
1602 ; let deriv_ev = CtDerived { ctev_pred = ctEvPred ev
1603 , ctev_loc = ctEvLoc ev }
1604 ; when keep_deriv $
1605 emitWork [workItem { cc_ev = deriv_ev }]
1606 -- As a Derived it might not be fully rewritten,
1607 -- so we emit it as new work
1608
1609 ; stopWith ev "Solved from inert" }
1610
1611 | ReprEq <- eq_rel -- See Note [Do not unify representational equalities]
1612 = do { traceTcS "Not unifying representational equality" (ppr workItem)
1613 ; continueWith workItem }
1614
1615 | isGiven ev -- See Note [Touchables and givens]
1616 = continueWith workItem
1617
1618 | otherwise
1619 = do { tclvl <- getTcLevel
1620 ; if canSolveByUnification tclvl tv rhs
1621 then do { solveByUnification ev tv rhs
1622 ; n_kicked <- kickOutAfterUnification tv
1623 ; return (Stop ev (text "Solved by unification" <+> pprKicked n_kicked)) }
1624
1625 else continueWith workItem }
1626
1627 interactTyVarEq _ wi = pprPanic "interactTyVarEq" (ppr wi)
1628
1629 solveByUnification :: CtEvidence -> TcTyVar -> Xi -> TcS ()
1630 -- Solve with the identity coercion
1631 -- Precondition: kind(xi) equals kind(tv)
1632 -- Precondition: CtEvidence is Wanted or Derived
1633 -- Precondition: CtEvidence is nominal
1634 -- Returns: workItem where
1635 -- workItem = the new Given constraint
1636 --
1637 -- NB: No need for an occurs check here, because solveByUnification always
1638 -- arises from a CTyEqCan, a *canonical* constraint. Its invariants
1639 -- say that in (a ~ xi), the type variable a does not appear in xi.
1640 -- See TcRnTypes.Ct invariants.
1641 --
1642 -- Post: tv is unified (by side effect) with xi;
1643 -- we often write tv := xi
1644 solveByUnification wd tv xi
1645 = do { let tv_ty = mkTyVarTy tv
1646 ; traceTcS "Sneaky unification:" $
1647 vcat [text "Unifies:" <+> ppr tv <+> text ":=" <+> ppr xi,
1648 text "Coercion:" <+> pprEq tv_ty xi,
1649 text "Left Kind is:" <+> ppr (typeKind tv_ty),
1650 text "Right Kind is:" <+> ppr (typeKind xi) ]
1651
1652 ; unifyTyVar tv xi
1653 ; setEvBindIfWanted wd (evCoercion (mkTcNomReflCo xi)) }
1654
1655 {- Note [Avoid double unifications]
1656 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1657 The spontaneous solver has to return a given which mentions the unified unification
1658 variable *on the left* of the equality. Here is what happens if not:
1659 Original wanted: (a ~ alpha), (alpha ~ Int)
1660 We spontaneously solve the first wanted, without changing the order!
1661 given : a ~ alpha [having unified alpha := a]
1662 Now the second wanted comes along, but he cannot rewrite the given, so we simply continue.
1663 At the end we spontaneously solve that guy, *reunifying* [alpha := Int]
1664
1665 We avoid this problem by orienting the resulting given so that the unification
1666 variable is on the left. [Note that alternatively we could attempt to
1667 enforce this at canonicalization]
1668
1669 See also Note [No touchables as FunEq RHS] in TcSMonad; avoiding
1670 double unifications is the main reason we disallow touchable
1671 unification variables as RHS of type family equations: F xis ~ alpha.
1672
1673 Note [Do not unify representational equalities]
1674 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1675 Consider [W] alpha ~R# b
1676 where alpha is touchable. Should we unify alpha := b?
1677
1678 Certainly not! Unifying forces alpha and be to be the same; but they
1679 only need to be representationally equal types.
1680
1681 For example, we might have another constraint [W] alpha ~# N b
1682 where
1683 newtype N b = MkN b
1684 and we want to get alpha := N b.
1685
1686 See also Trac #15144, which was caused by unifying a representational
1687 equality (in the unflattener).
1688
1689
1690 ************************************************************************
1691 * *
1692 * Functional dependencies, instantiation of equations
1693 * *
1694 ************************************************************************
1695
1696 When we spot an equality arising from a functional dependency,
1697 we now use that equality (a "wanted") to rewrite the work-item
1698 constraint right away. This avoids two dangers
1699
1700 Danger 1: If we send the original constraint on down the pipeline
1701 it may react with an instance declaration, and in delicate
1702 situations (when a Given overlaps with an instance) that
1703 may produce new insoluble goals: see Trac #4952
1704
1705 Danger 2: If we don't rewrite the constraint, it may re-react
1706 with the same thing later, and produce the same equality
1707 again --> termination worries.
1708
1709 To achieve this required some refactoring of FunDeps.hs (nicer
1710 now!).
1711
1712 Note [FunDep and implicit parameter reactions]
1713 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1714 Currently, our story of interacting two dictionaries (or a dictionary
1715 and top-level instances) for functional dependencies, and implicit
1716 parameters, is that we simply produce new Derived equalities. So for example
1717
1718 class D a b | a -> b where ...
1719 Inert:
1720 d1 :g D Int Bool
1721 WorkItem:
1722 d2 :w D Int alpha
1723
1724 We generate the extra work item
1725 cv :d alpha ~ Bool
1726 where 'cv' is currently unused. However, this new item can perhaps be
1727 spontaneously solved to become given and react with d2,
1728 discharging it in favour of a new constraint d2' thus:
1729 d2' :w D Int Bool
1730 d2 := d2' |> D Int cv
1731 Now d2' can be discharged from d1
1732
1733 We could be more aggressive and try to *immediately* solve the dictionary
1734 using those extra equalities, but that requires those equalities to carry
1735 evidence and derived do not carry evidence.
1736
1737 If that were the case with the same inert set and work item we might dischard
1738 d2 directly:
1739
1740 cv :w alpha ~ Bool
1741 d2 := d1 |> D Int cv
1742
1743 But in general it's a bit painful to figure out the necessary coercion,
1744 so we just take the first approach. Here is a better example. Consider:
1745 class C a b c | a -> b
1746 And:
1747 [Given] d1 : C T Int Char
1748 [Wanted] d2 : C T beta Int
1749 In this case, it's *not even possible* to solve the wanted immediately.
1750 So we should simply output the functional dependency and add this guy
1751 [but NOT its superclasses] back in the worklist. Even worse:
1752 [Given] d1 : C T Int beta
1753 [Wanted] d2: C T beta Int
1754 Then it is solvable, but its very hard to detect this on the spot.
1755
1756 It's exactly the same with implicit parameters, except that the
1757 "aggressive" approach would be much easier to implement.
1758
1759 Note [Weird fundeps]
1760 ~~~~~~~~~~~~~~~~~~~~
1761 Consider class Het a b | a -> b where
1762 het :: m (f c) -> a -> m b
1763
1764 class GHet (a :: * -> *) (b :: * -> *) | a -> b
1765 instance GHet (K a) (K [a])
1766 instance Het a b => GHet (K a) (K b)
1767
1768 The two instances don't actually conflict on their fundeps,
1769 although it's pretty strange. So they are both accepted. Now
1770 try [W] GHet (K Int) (K Bool)
1771 This triggers fundeps from both instance decls;
1772 [D] K Bool ~ K [a]
1773 [D] K Bool ~ K beta
1774 And there's a risk of complaining about Bool ~ [a]. But in fact
1775 the Wanted matches the second instance, so we never get as far
1776 as the fundeps.
1777
1778 Trac #7875 is a case in point.
1779 -}
1780
1781 emitFunDepDeriveds :: [FunDepEqn CtLoc] -> TcS ()
1782 -- See Note [FunDep and implicit parameter reactions]
1783 emitFunDepDeriveds fd_eqns
1784 = mapM_ do_one_FDEqn fd_eqns
1785 where
1786 do_one_FDEqn (FDEqn { fd_qtvs = tvs, fd_eqs = eqs, fd_loc = loc })
1787 | null tvs -- Common shortcut
1788 = do { traceTcS "emitFunDepDeriveds 1" (ppr (ctl_depth loc) $$ ppr eqs $$ ppr (isGivenLoc loc))
1789 ; mapM_ (unifyDerived loc Nominal) eqs }
1790 | otherwise
1791 = do { traceTcS "emitFunDepDeriveds 2" (ppr (ctl_depth loc) $$ ppr tvs $$ ppr eqs)
1792 ; subst <- instFlexi tvs -- Takes account of kind substitution
1793 ; mapM_ (do_one_eq loc subst) eqs }
1794
1795 do_one_eq loc subst (Pair ty1 ty2)
1796 = unifyDerived loc Nominal $
1797 Pair (Type.substTyUnchecked subst ty1) (Type.substTyUnchecked subst ty2)
1798
1799 {-
1800 **********************************************************************
1801 * *
1802 The top-reaction Stage
1803 * *
1804 **********************************************************************
1805 -}
1806
1807 topReactionsStage :: WorkItem -> TcS (StopOrContinue Ct)
1808 -- The work item does not react with the inert set,
1809 -- so try interaction with top-level instances. Note:
1810 topReactionsStage work_item
1811 = do { traceTcS "doTopReact" (ppr work_item)
1812 ; case work_item of
1813 CDictCan {} -> do { inerts <- getTcSInerts
1814 ; doTopReactDict inerts work_item }
1815 CFunEqCan {} -> doTopReactFunEq work_item
1816 CIrredCan {} -> doTopReactOther work_item
1817 CTyEqCan {} -> doTopReactOther work_item
1818 _ -> -- Any other work item does not react with any top-level equations
1819 continueWith work_item }
1820
1821
1822 --------------------
1823 doTopReactOther :: Ct -> TcS (StopOrContinue Ct)
1824 -- Try local quantified constraints for
1825 -- CTyEqCan e.g. (a ~# ty)
1826 -- and CIrredCan e.g. (c a)
1827 --
1828 -- Why equalities? See TcCanonical
1829 -- Note [Equality superclasses in quantified constraints]
1830 doTopReactOther work_item
1831 | isGiven ev
1832 = continueWith work_item
1833
1834 | EqPred eq_rel t1 t2 <- classifyPredType pred
1835 = -- See Note [Looking up primitive equalities in quantified constraints]
1836 case boxEqPred eq_rel t1 t2 of
1837 Nothing -> continueWith work_item
1838 Just (cls, tys)
1839 -> do { res <- matchLocalInst (mkClassPred cls tys) loc
1840 ; case res of
1841 OneInst { cir_mk_ev = mk_ev }
1842 -> chooseInstance work_item
1843 (res { cir_mk_ev = mk_eq_ev cls tys mk_ev })
1844 where
1845 _ -> continueWith work_item }
1846
1847 | otherwise
1848 = do { res <- matchLocalInst pred loc
1849 ; case res of
1850 OneInst {} -> chooseInstance work_item res
1851 _ -> continueWith work_item }
1852 where
1853 ev = ctEvidence work_item
1854 loc = ctEvLoc ev
1855 pred = ctEvPred ev
1856
1857 mk_eq_ev cls tys mk_ev evs
1858 = case (mk_ev evs) of
1859 EvExpr e -> EvExpr (Var sc_id `mkTyApps` tys `App` e)
1860 ev -> pprPanic "mk_eq_ev" (ppr ev)
1861 where
1862 [sc_id] = classSCSelIds cls
1863
1864 {- Note [Looking up primitive equalities in quantified constraints]
1865 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1866 For equalities (a ~# b) look up (a ~ b), and then do a superclass
1867 selection. This avoids having to support quantified constraints whose
1868 kind is not Constraint, such as (forall a. F a ~# b)
1869
1870 See
1871 * Note [Evidence for quantified constraints] in Type
1872 * Note [Equality superclasses in quantified constraints]
1873 in TcCanonical
1874 -}
1875
1876 --------------------
1877 doTopReactFunEq :: Ct -> TcS (StopOrContinue Ct)
1878 doTopReactFunEq work_item@(CFunEqCan { cc_ev = old_ev, cc_fun = fam_tc
1879 , cc_tyargs = args, cc_fsk = fsk })
1880
1881 | fsk `elemVarSet` tyCoVarsOfTypes args
1882 = no_reduction -- See Note [FunEq occurs-check principle]
1883
1884 | otherwise -- Note [Reduction for Derived CFunEqCans]
1885 = do { match_res <- matchFam fam_tc args
1886 -- Look up in top-level instances, or built-in axiom
1887 -- See Note [MATCHING-SYNONYMS]
1888 ; case match_res of
1889 Nothing -> no_reduction
1890 Just match_info -> reduce_top_fun_eq old_ev fsk match_info }
1891 where
1892 no_reduction
1893 = do { improveTopFunEqs old_ev fam_tc args fsk
1894 ; continueWith work_item }
1895
1896 doTopReactFunEq w = pprPanic "doTopReactFunEq" (ppr w)
1897
1898 reduce_top_fun_eq :: CtEvidence -> TcTyVar -> (TcCoercion, TcType)
1899 -> TcS (StopOrContinue Ct)
1900 -- We have found an applicable top-level axiom: use it to reduce
1901 -- Precondition: fsk is not free in rhs_ty
1902 reduce_top_fun_eq old_ev fsk (ax_co, rhs_ty)
1903 | not (isDerived old_ev) -- Precondition of shortCutReduction
1904 , Just (tc, tc_args) <- tcSplitTyConApp_maybe rhs_ty
1905 , isTypeFamilyTyCon tc
1906 , tc_args `lengthIs` tyConArity tc -- Short-cut
1907 = -- RHS is another type-family application
1908 -- Try shortcut; see Note [Top-level reductions for type functions]
1909 do { shortCutReduction old_ev fsk ax_co tc tc_args
1910 ; stopWith old_ev "Fun/Top (shortcut)" }
1911
1912 | otherwise
1913 = ASSERT2( not (fsk `elemVarSet` tyCoVarsOfType rhs_ty)
1914 , ppr old_ev $$ ppr rhs_ty )
1915 -- Guaranteed by Note [FunEq occurs-check principle]
1916 do { dischargeFunEq old_ev fsk ax_co rhs_ty
1917 ; traceTcS "doTopReactFunEq" $
1918 vcat [ text "old_ev:" <+> ppr old_ev
1919 , nest 2 (text ":=") <+> ppr ax_co ]
1920 ; stopWith old_ev "Fun/Top" }
1921
1922 improveTopFunEqs :: CtEvidence -> TyCon -> [TcType] -> TcTyVar -> TcS ()
1923 -- See Note [FunDep and implicit parameter reactions]
1924 improveTopFunEqs ev fam_tc args fsk
1925 | isGiven ev -- See Note [No FunEq improvement for Givens]
1926 || not (isImprovable ev)
1927 = return ()
1928
1929 | otherwise
1930 = do { ieqs <- getInertEqs
1931 ; fam_envs <- getFamInstEnvs
1932 ; eqns <- improve_top_fun_eqs fam_envs fam_tc args
1933 (lookupFlattenTyVar ieqs fsk)
1934 ; traceTcS "improveTopFunEqs" (vcat [ ppr fam_tc <+> ppr args <+> ppr fsk
1935 , ppr eqns ])
1936 ; mapM_ (unifyDerived loc Nominal) eqns }
1937 where
1938 loc = ctEvLoc ev -- ToDo: this location is wrong; it should be FunDepOrigin2
1939 -- See Trac #14778
1940
1941 improve_top_fun_eqs :: FamInstEnvs
1942 -> TyCon -> [TcType] -> TcType
1943 -> TcS [TypeEqn]
1944 improve_top_fun_eqs fam_envs fam_tc args rhs_ty
1945 | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc
1946 = return (sfInteractTop ops args rhs_ty)
1947
1948 -- see Note [Type inference for type families with injectivity]
1949 | isOpenTypeFamilyTyCon fam_tc
1950 , Injective injective_args <- tyConInjectivityInfo fam_tc
1951 , let fam_insts = lookupFamInstEnvByTyCon fam_envs fam_tc
1952 = -- it is possible to have several compatible equations in an open type
1953 -- family but we only want to derive equalities from one such equation.
1954 do { let improvs = buildImprovementData fam_insts
1955 fi_tvs fi_tys fi_rhs (const Nothing)
1956
1957 ; traceTcS "improve_top_fun_eqs2" (ppr improvs)
1958 ; concatMapM (injImproveEqns injective_args) $
1959 take 1 improvs }
1960
1961 | Just ax <- isClosedSynFamilyTyConWithAxiom_maybe fam_tc
1962 , Injective injective_args <- tyConInjectivityInfo fam_tc
1963 = concatMapM (injImproveEqns injective_args) $
1964 buildImprovementData (fromBranches (co_ax_branches ax))
1965 cab_tvs cab_lhs cab_rhs Just
1966
1967 | otherwise
1968 = return []
1969
1970 where
1971 buildImprovementData
1972 :: [a] -- axioms for a TF (FamInst or CoAxBranch)
1973 -> (a -> [TyVar]) -- get bound tyvars of an axiom
1974 -> (a -> [Type]) -- get LHS of an axiom
1975 -> (a -> Type) -- get RHS of an axiom
1976 -> (a -> Maybe CoAxBranch) -- Just => apartness check required
1977 -> [( [Type], TCvSubst, [TyVar], Maybe CoAxBranch )]
1978 -- Result:
1979 -- ( [arguments of a matching axiom]
1980 -- , RHS-unifying substitution
1981 -- , axiom variables without substitution
1982 -- , Maybe matching axiom [Nothing - open TF, Just - closed TF ] )
1983 buildImprovementData axioms axiomTVs axiomLHS axiomRHS wrap =
1984 [ (ax_args, subst, unsubstTvs, wrap axiom)
1985 | axiom <- axioms
1986 , let ax_args = axiomLHS axiom
1987 ax_rhs = axiomRHS axiom
1988 ax_tvs = axiomTVs axiom
1989 , Just subst <- [tcUnifyTyWithTFs False ax_rhs rhs_ty]
1990 , let notInSubst tv = not (tv `elemVarEnv` getTvSubstEnv subst)
1991 unsubstTvs = filter (notInSubst <&&> isTyVar) ax_tvs ]
1992 -- The order of unsubstTvs is important; it must be
1993 -- in telescope order e.g. (k:*) (a:k)
1994
1995 injImproveEqns :: [Bool]
1996 -> ([Type], TCvSubst, [TyCoVar], Maybe CoAxBranch)
1997 -> TcS [TypeEqn]
1998 injImproveEqns inj_args (ax_args, subst, unsubstTvs, cabr)
1999 = do { subst <- instFlexiX subst unsubstTvs
2000 -- If the current substitution bind [k -> *], and
2001 -- one of the un-substituted tyvars is (a::k), we'd better
2002 -- be sure to apply the current substitution to a's kind.
2003 -- Hence instFlexiX. Trac #13135 was an example.
2004
2005 ; return [ Pair (substTyUnchecked subst ax_arg) arg
2006 -- NB: the ax_arg part is on the left
2007 -- see Note [Improvement orientation]
2008 | case cabr of
2009 Just cabr' -> apartnessCheck (substTys subst ax_args) cabr'
2010 _ -> True
2011 , (ax_arg, arg, True) <- zip3 ax_args args inj_args ] }
2012
2013
2014 shortCutReduction :: CtEvidence -> TcTyVar -> TcCoercion
2015 -> TyCon -> [TcType] -> TcS ()
2016 -- See Note [Top-level reductions for type functions]
2017 -- Previously, we flattened the tc_args here, but there's no need to do so.
2018 -- And, if we did, this function would have all the complication of
2019 -- TcCanonical.canCFunEqCan. See Note [canCFunEqCan]
2020 shortCutReduction old_ev fsk ax_co fam_tc tc_args
2021 = ASSERT( ctEvEqRel old_ev == NomEq)
2022 -- ax_co :: F args ~ G tc_args
2023 -- old_ev :: F args ~ fsk
2024 do { new_ev <- case ctEvFlavour old_ev of
2025 Given -> newGivenEvVar deeper_loc
2026 ( mkPrimEqPred (mkTyConApp fam_tc tc_args) (mkTyVarTy fsk)
2027 , evCoercion (mkTcSymCo ax_co
2028 `mkTcTransCo` ctEvCoercion old_ev) )
2029
2030 Wanted {} ->
2031 do { (new_ev, new_co) <- newWantedEq deeper_loc Nominal
2032 (mkTyConApp fam_tc tc_args) (mkTyVarTy fsk)
2033 ; setWantedEq (ctev_dest old_ev) $ ax_co `mkTcTransCo` new_co
2034 ; return new_ev }
2035
2036 Derived -> pprPanic "shortCutReduction" (ppr old_ev)
2037
2038 ; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc
2039 , cc_tyargs = tc_args, cc_fsk = fsk }
2040 ; updWorkListTcS (extendWorkListFunEq new_ct) }
2041 where
2042 deeper_loc = bumpCtLocDepth (ctEvLoc old_ev)
2043
2044 {- Note [Top-level reductions for type functions]
2045 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2046 c.f. Note [The flattening story] in TcFlatten
2047
2048 Suppose we have a CFunEqCan F tys ~ fmv/fsk, and a matching axiom.
2049 Here is what we do, in four cases:
2050
2051 * Wanteds: general firing rule
2052 (work item) [W] x : F tys ~ fmv
2053 instantiate axiom: ax_co : F tys ~ rhs
2054
2055 Then:
2056 Discharge fmv := rhs
2057 Discharge x := ax_co ; sym x2
2058 This is *the* way that fmv's get unified; even though they are
2059 "untouchable".
2060
2061 NB: Given Note [FunEq occurs-check principle], fmv does not appear
2062 in tys, and hence does not appear in the instantiated RHS. So
2063 the unification can't make an infinite type.
2064
2065 * Wanteds: short cut firing rule
2066 Applies when the RHS of the axiom is another type-function application
2067 (work item) [W] x : F tys ~ fmv
2068 instantiate axiom: ax_co : F tys ~ G rhs_tys
2069
2070 It would be a waste to create yet another fmv for (G rhs_tys).
2071 Instead (shortCutReduction):
2072 - Flatten rhs_tys (cos : rhs_tys ~ rhs_xis)
2073 - Add G rhs_xis ~ fmv to flat cache (note: the same old fmv)
2074 - New canonical wanted [W] x2 : G rhs_xis ~ fmv (CFunEqCan)
2075 - Discharge x := ax_co ; G cos ; x2
2076
2077 * Givens: general firing rule
2078 (work item) [G] g : F tys ~ fsk
2079 instantiate axiom: ax_co : F tys ~ rhs
2080
2081 Now add non-canonical given (since rhs is not flat)
2082 [G] (sym g ; ax_co) : fsk ~ rhs (Non-canonical)
2083
2084 * Givens: short cut firing rule
2085 Applies when the RHS of the axiom is another type-function application
2086 (work item) [G] g : F tys ~ fsk
2087 instantiate axiom: ax_co : F tys ~ G rhs_tys
2088
2089 It would be a waste to create yet another fsk for (G rhs_tys).
2090 Instead (shortCutReduction):
2091 - Flatten rhs_tys: flat_cos : tys ~ flat_tys
2092 - Add new Canonical given
2093 [G] (sym (G flat_cos) ; co ; g) : G flat_tys ~ fsk (CFunEqCan)
2094
2095 Note [FunEq occurs-check principle]
2096 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2097 I have spent a lot of time finding a good way to deal with
2098 CFunEqCan constraints like
2099 F (fuv, a) ~ fuv
2100 where flatten-skolem occurs on the LHS. Now in principle we
2101 might may progress by doing a reduction, but in practice its
2102 hard to find examples where it is useful, and easy to find examples
2103 where we fall into an infinite reduction loop. A rule that works
2104 very well is this:
2105
2106 *** FunEq occurs-check principle ***
2107
2108 Do not reduce a CFunEqCan
2109 F tys ~ fsk
2110 if fsk appears free in tys
2111 Instead we treat it as stuck.
2112
2113 Examples:
2114
2115 * Trac #5837 has [G] a ~ TF (a,Int), with an instance
2116 type instance TF (a,b) = (TF a, TF b)
2117 This readily loops when solving givens. But with the FunEq occurs
2118 check principle, it rapidly gets stuck which is fine.
2119
2120 * Trac #12444 is a good example, explained in comment:2. We have
2121 type instance F (Succ x) = Succ (F x)
2122 [W] alpha ~ Succ (F alpha)
2123 If we allow the reduction to happen, we get an infinite loop
2124
2125 Note [Cached solved FunEqs]
2126 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
2127 When trying to solve, say (FunExpensive big-type ~ ty), it's important
2128 to see if we have reduced (FunExpensive big-type) before, lest we
2129 simply repeat it. Hence the lookup in inert_solved_funeqs. Moreover
2130 we must use `funEqCanDischarge` because both uses might (say) be Wanteds,
2131 and we *still* want to save the re-computation.
2132
2133 Note [MATCHING-SYNONYMS]
2134 ~~~~~~~~~~~~~~~~~~~~~~~~
2135 When trying to match a dictionary (D tau) to a top-level instance, or a
2136 type family equation (F taus_1 ~ tau_2) to a top-level family instance,
2137 we do *not* need to expand type synonyms because the matcher will do that for us.
2138
2139 Note [Improvement orientation]
2140 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2141 A very delicate point is the orientation of derived equalities
2142 arising from injectivity improvement (Trac #12522). Suppse we have
2143 type family F x = t | t -> x
2144 type instance F (a, Int) = (Int, G a)
2145 where G is injective; and wanted constraints
2146
2147 [W] TF (alpha, beta) ~ fuv
2148 [W] fuv ~ (Int, <some type>)
2149
2150 The injectivity will give rise to derived constraints
2151
2152 [D] gamma1 ~ alpha
2153 [D] Int ~ beta
2154
2155 The fresh unification variable gamma1 comes from the fact that we
2156 can only do "partial improvement" here; see Section 5.2 of
2157 "Injective type families for Haskell" (HS'15).
2158
2159 Now, it's very important to orient the equations this way round,
2160 so that the fresh unification variable will be eliminated in
2161 favour of alpha. If we instead had
2162 [D] alpha ~ gamma1
2163 then we would unify alpha := gamma1; and kick out the wanted
2164 constraint. But when we grough it back in, it'd look like
2165 [W] TF (gamma1, beta) ~ fuv
2166 and exactly the same thing would happen again! Infinite loop.
2167
2168 This all seems fragile, and it might seem more robust to avoid
2169 introducing gamma1 in the first place, in the case where the
2170 actual argument (alpha, beta) partly matches the improvement
2171 template. But that's a bit tricky, esp when we remember that the
2172 kinds much match too; so it's easier to let the normal machinery
2173 handle it. Instead we are careful to orient the new derived
2174 equality with the template on the left. Delicate, but it works.
2175
2176 Note [No FunEq improvement for Givens]
2177 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2178 We don't do improvements (injectivity etc) for Givens. Why?
2179
2180 * It generates Derived constraints on skolems, which don't do us
2181 much good, except perhaps identify inaccessible branches.
2182 (They'd be perfectly valid though.)
2183
2184 * For type-nat stuff the derived constraints include type families;
2185 e.g. (a < b), (b < c) ==> a < c If we generate a Derived for this,
2186 we'll generate a Derived/Wanted CFunEqCan; and, since the same
2187 InertCans (after solving Givens) are used for each iteration, that
2188 massively confused the unflattening step (TcFlatten.unflatten).
2189
2190 In fact it led to some infinite loops:
2191 indexed-types/should_compile/T10806
2192 indexed-types/should_compile/T10507
2193 polykinds/T10742
2194
2195 Note [Reduction for Derived CFunEqCans]
2196 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2197 You may wonder if it's important to use top-level instances to
2198 simplify [D] CFunEqCan's. But it is. Here's an example (T10226).
2199
2200 type instance F Int = Int
2201 type instance FInv Int = Int
2202
2203 Suppose we have to solve
2204 [WD] FInv (F alpha) ~ alpha
2205 [WD] F alpha ~ Int
2206
2207 --> flatten
2208 [WD] F alpha ~ fuv0
2209 [WD] FInv fuv0 ~ fuv1 -- (A)
2210 [WD] fuv1 ~ alpha
2211 [WD] fuv0 ~ Int -- (B)
2212
2213 --> Rewwrite (A) with (B), splitting it
2214 [WD] F alpha ~ fuv0
2215 [W] FInv fuv0 ~ fuv1
2216 [D] FInv Int ~ fuv1 -- (C)
2217 [WD] fuv1 ~ alpha
2218 [WD] fuv0 ~ Int
2219
2220 --> Reduce (C) with top-level instance
2221 **** This is the key step ***
2222 [WD] F alpha ~ fuv0
2223 [W] FInv fuv0 ~ fuv1
2224 [D] fuv1 ~ Int -- (D)
2225 [WD] fuv1 ~ alpha -- (E)
2226 [WD] fuv0 ~ Int
2227
2228 --> Rewrite (D) with (E)
2229 [WD] F alpha ~ fuv0
2230 [W] FInv fuv0 ~ fuv1
2231 [D] alpha ~ Int -- (F)
2232 [WD] fuv1 ~ alpha
2233 [WD] fuv0 ~ Int
2234
2235 --> unify (F) alpha := Int, and that solves it
2236
2237 Another example is indexed-types/should_compile/T10634
2238 -}
2239
2240 {- *******************************************************************
2241 * *
2242 Top-level reaction for class constraints (CDictCan)
2243 * *
2244 **********************************************************************-}
2245
2246 doTopReactDict :: InertSet -> Ct -> TcS (StopOrContinue Ct)
2247 -- Try to use type-class instance declarations to simplify the constraint
2248 doTopReactDict inerts work_item@(CDictCan { cc_ev = ev, cc_class = cls
2249 , cc_tyargs = xis })
2250 | isGiven ev -- Never use instances for Given constraints
2251 = do { try_fundep_improvement
2252 ; continueWith work_item }
2253
2254 | Just solved_ev <- lookupSolvedDict inerts dict_loc cls xis -- Cached
2255 = do { setEvBindIfWanted ev (ctEvTerm solved_ev)
2256 ; stopWith ev "Dict/Top (cached)" }
2257
2258 | otherwise -- Wanted or Derived, but not cached
2259 = do { dflags <- getDynFlags
2260 ; lkup_res <- matchClassInst dflags inerts cls xis dict_loc
2261 ; case lkup_res of
2262 OneInst { cir_what = what }
2263 -> do { unless (safeOverlap what) $
2264 insertSafeOverlapFailureTcS work_item
2265 ; when (isWanted ev) $ addSolvedDict ev cls xis
2266 ; chooseInstance work_item lkup_res }
2267 _ -> -- NoInstance or NotSure
2268 do { when (isImprovable ev) $
2269 try_fundep_improvement
2270 ; continueWith work_item } }
2271 where
2272 dict_pred = mkClassPred cls xis
2273 dict_loc = ctEvLoc ev
2274 dict_origin = ctLocOrigin dict_loc
2275
2276 -- We didn't solve it; so try functional dependencies with
2277 -- the instance environment, and return
2278 -- See also Note [Weird fundeps]
2279 try_fundep_improvement
2280 = do { traceTcS "try_fundeps" (ppr work_item)
2281 ; instEnvs <- getInstEnvs
2282 ; emitFunDepDeriveds $
2283 improveFromInstEnv instEnvs mk_ct_loc dict_pred }
2284
2285 mk_ct_loc :: PredType -- From instance decl
2286 -> SrcSpan -- also from instance deol
2287 -> CtLoc
2288 mk_ct_loc inst_pred inst_loc
2289 = dict_loc { ctl_origin = FunDepOrigin2 dict_pred dict_origin
2290 inst_pred inst_loc }
2291
2292 doTopReactDict _ w = pprPanic "doTopReactDict" (ppr w)
2293
2294
2295 chooseInstance :: Ct -> ClsInstResult -> TcS (StopOrContinue Ct)
2296 chooseInstance work_item
2297 (OneInst { cir_new_theta = theta
2298 , cir_what = what
2299 , cir_mk_ev = mk_ev })
2300 = do { traceTcS "doTopReact/found instance for" $ ppr ev
2301 ; deeper_loc <- checkInstanceOK loc what pred
2302 ; if isDerived ev then finish_derived deeper_loc theta
2303 else finish_wanted deeper_loc theta mk_ev }
2304 where
2305 ev = ctEvidence work_item
2306 pred = ctEvPred ev
2307 loc = ctEvLoc ev
2308
2309 finish_wanted :: CtLoc -> [TcPredType]
2310 -> ([EvExpr] -> EvTerm) -> TcS (StopOrContinue Ct)
2311 -- Precondition: evidence term matches the predicate workItem
2312 finish_wanted loc theta mk_ev
2313 = do { evb <- getTcEvBindsVar
2314 ; if isCoEvBindsVar evb
2315 then -- See Note [Instances in no-evidence implications]
2316 continueWith work_item
2317 else
2318 do { evc_vars <- mapM (newWanted loc) theta
2319 ; setEvBindIfWanted ev (mk_ev (map getEvExpr evc_vars))
2320 ; emitWorkNC (freshGoals evc_vars)
2321 ; stopWith ev "Dict/Top (solved wanted)" } }
2322
2323 finish_derived loc theta
2324 = -- Use type-class instances for Deriveds, in the hope
2325 -- of generating some improvements
2326 -- C.f. Example 3 of Note [The improvement story]
2327 -- It's easy because no evidence is involved
2328 do { emitNewDeriveds loc theta
2329 ; traceTcS "finish_derived" (ppr (ctl_depth loc))
2330 ; stopWith ev "Dict/Top (solved derived)" }
2331
2332 chooseInstance work_item lookup_res
2333 = pprPanic "chooseInstance" (ppr work_item $$ ppr lookup_res)
2334
2335 checkInstanceOK :: CtLoc -> InstanceWhat -> TcPredType -> TcS CtLoc
2336 -- Check that it's OK to use this insstance:
2337 -- (a) the use is well staged in the Template Haskell sense
2338 -- (b) we have not recursed too deep
2339 -- Returns the CtLoc to used for sub-goals
2340 checkInstanceOK loc what pred
2341 = do { checkWellStagedDFun loc what pred
2342 ; checkReductionDepth deeper_loc pred
2343 ; return deeper_loc }
2344 where
2345 deeper_loc = zap_origin (bumpCtLocDepth loc)
2346 origin = ctLocOrigin loc
2347
2348 zap_origin loc -- After applying an instance we can set ScOrigin to
2349 -- infinity, so that prohibitedSuperClassSolve never fires
2350 | ScOrigin {} <- origin
2351 = setCtLocOrigin loc (ScOrigin infinity)
2352 | otherwise
2353 = loc
2354
2355 {- Note [Instances in no-evidence implications]
2356 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2357 In Trac #15290 we had
2358 [G] forall p q. Coercible p q => Coercible (m p) (m q))
2359 [W] forall <no-ev> a. m (Int, IntStateT m a)
2360 ~R#
2361 m (Int, StateT Int m a)
2362
2363 The Given is an ordinary quantified constraint; the Wanted is an implication
2364 equality that arises from
2365 [W] (forall a. t1) ~R# (forall a. t2)
2366
2367 But because the (t1 ~R# t2) is solved "inside a type" (under that forall a)
2368 we can't generate any term evidence. So we can't actually use that
2369 lovely quantified constraint. Alas!
2370
2371 This test arranges to ignore the instance-based solution under these
2372 (rare) circumstances. It's sad, but I really don't see what else we can do.
2373 -}
2374
2375
2376 matchClassInst :: DynFlags -> InertSet
2377 -> Class -> [Type]
2378 -> CtLoc -> TcS ClsInstResult
2379 matchClassInst dflags inerts clas tys loc
2380 -- First check whether there is an in-scope Given that could
2381 -- match this constraint. In that case, do not use any instance
2382 -- whether top level, or local quantified constraints.
2383 -- ee Note [Instance and Given overlap]
2384 | not (xopt LangExt.IncoherentInstances dflags)
2385 , not (naturallyCoherentClass clas)
2386 , let matchable_givens = matchableGivens loc pred inerts
2387 , not (isEmptyBag matchable_givens)
2388 = do { traceTcS "Delaying instance application" $
2389 vcat [ text "Work item=" <+> pprClassPred clas tys
2390 , text "Potential matching givens:" <+> ppr matchable_givens ]
2391 ; return NotSure }
2392
2393 | otherwise
2394 = do { traceTcS "matchClassInst" $ text "pred =" <+> ppr pred <+> char '{'
2395 ; local_res <- matchLocalInst pred loc
2396 ; case local_res of
2397 OneInst {} -> -- See Note [Local instances and incoherence]
2398 do { traceTcS "} matchClassInst local match" $ ppr local_res
2399 ; return local_res }
2400
2401 NotSure -> -- In the NotSure case for local instances
2402 -- we don't want to try global instances
2403 do { traceTcS "} matchClassInst local not sure" empty
2404 ; return local_res }
2405
2406 NoInstance -- No local instances, so try global ones
2407 -> do { global_res <- matchGlobalInst dflags False clas tys
2408 ; traceTcS "} matchClassInst global result" $ ppr global_res
2409 ; return global_res } }
2410 where
2411 pred = mkClassPred clas tys
2412
2413 -- | If a class is "naturally coherent", then we needn't worry at all, in any
2414 -- way, about overlapping/incoherent instances. Just solve the thing!
2415 -- See Note [Naturally coherent classes]
2416 -- See also Note [The equality class story] in TysPrim.
2417 naturallyCoherentClass :: Class -> Bool
2418 naturallyCoherentClass cls
2419 = isCTupleClass cls
2420 || cls `hasKey` heqTyConKey
2421 || cls `hasKey` eqTyConKey
2422 || cls `hasKey` coercibleTyConKey
2423
2424
2425 {- Note [Instance and Given overlap]
2426 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2427 Example, from the OutsideIn(X) paper:
2428 instance P x => Q [x]
2429 instance (x ~ y) => R y [x]
2430
2431 wob :: forall a b. (Q [b], R b a) => a -> Int
2432
2433 g :: forall a. Q [a] => [a] -> Int
2434 g x = wob x
2435
2436 From 'g' we get the impliation constraint:
2437 forall a. Q [a] => (Q [beta], R beta [a])
2438 If we react (Q [beta]) with its top-level axiom, we end up with a
2439 (P beta), which we have no way of discharging. On the other hand,
2440 if we react R beta [a] with the top-level we get (beta ~ a), which
2441 is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
2442 now solvable by the given Q [a].
2443
2444 The partial solution is that:
2445 In matchClassInst (and thus in topReact), we return a matching
2446 instance only when there is no Given in the inerts which is
2447 unifiable to this particular dictionary.
2448
2449 We treat any meta-tyvar as "unifiable" for this purpose,
2450 *including* untouchable ones. But not skolems like 'a' in
2451 the implication constraint above.
2452
2453 The end effect is that, much as we do for overlapping instances, we
2454 delay choosing a class instance if there is a possibility of another
2455 instance OR a given to match our constraint later on. This fixes
2456 Trac #4981 and #5002.
2457
2458 Other notes:
2459
2460 * The check is done *first*, so that it also covers classes
2461 with built-in instance solving, such as
2462 - constraint tuples
2463 - natural numbers
2464 - Typeable
2465
2466 * Flatten-skolems: we do not treat a flatten-skolem as unifiable
2467 for this purpose.
2468 E.g. f :: Eq (F a) => [a] -> [a]
2469 f xs = ....(xs==xs).....
2470 Here we get [W] Eq [a], and we don't want to refrain from solving
2471 it because of the given (Eq (F a)) constraint!
2472
2473 * The given-overlap problem is arguably not easy to appear in practice
2474 due to our aggressive prioritization of equality solving over other
2475 constraints, but it is possible. I've added a test case in
2476 typecheck/should-compile/GivenOverlapping.hs
2477
2478 * Another "live" example is Trac #10195; another is #10177.
2479
2480 * We ignore the overlap problem if -XIncoherentInstances is in force:
2481 see Trac #6002 for a worked-out example where this makes a
2482 difference.
2483
2484 * Moreover notice that our goals here are different than the goals of
2485 the top-level overlapping checks. There we are interested in
2486 validating the following principle:
2487
2488 If we inline a function f at a site where the same global
2489 instance environment is available as the instance environment at
2490 the definition site of f then we should get the same behaviour.
2491
2492 But for the Given Overlap check our goal is just related to completeness of
2493 constraint solving.
2494
2495 * The solution is only a partial one. Consider the above example with
2496 g :: forall a. Q [a] => [a] -> Int
2497 g x = let v = wob x
2498 in v
2499 and suppose we have -XNoMonoLocalBinds, so that we attempt to find the most
2500 general type for 'v'. When generalising v's type we'll simplify its
2501 Q [alpha] constraint, but we don't have Q [a] in the 'givens', so we
2502 will use the instance declaration after all. Trac #11948 was a case
2503 in point.
2504
2505 All of this is disgustingly delicate, so to discourage people from writing
2506 simplifiable class givens, we warn about signatures that contain them;
2507 see TcValidity Note [Simplifiable given constraints].
2508
2509 Note [Naturally coherent classes]
2510 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2511 A few built-in classes are "naturally coherent". This term means that
2512 the "instance" for the class is bidirectional with its superclass(es).
2513 For example, consider (~~), which behaves as if it was defined like
2514 this:
2515 class a ~# b => a ~~ b
2516 instance a ~# b => a ~~ b
2517 (See Note [The equality types story] in TysPrim.)
2518
2519 Faced with [W] t1 ~~ t2, it's always OK to reduce it to [W] t1 ~# t2,
2520 without worrying about Note [Instance and Given overlap]. Why? Because
2521 if we had [G] s1 ~~ s2, then we'd get the superclass [G] s1 ~# s2, and
2522 so the reduction of the [W] constraint does not risk losing any solutions.
2523
2524 On the other hand, it can be fatal to /fail/ to reduce such
2525 equalities, on the grounds of Note [Instance and Given overlap],
2526 because many good things flow from [W] t1 ~# t2.
2527
2528 The same reasoning applies to
2529
2530 * (~~) heqTyCOn
2531 * (~) eqTyCon
2532 * Coercible coercibleTyCon
2533
2534 And less obviously to:
2535
2536 * Tuple classes. For reasons described in TcSMonad
2537 Note [Tuples hiding implicit parameters], we may have a constraint
2538 [W] (?x::Int, C a)
2539 with an exactly-matching Given constraint. We must decompose this
2540 tuple and solve the components separately, otherwise we won't solve
2541 it at all! It is perfectly safe to decompose it, because again the
2542 superclasses invert the instance; e.g.
2543 class (c1, c2) => (% c1, c2 %)
2544 instance (c1, c2) => (% c1, c2 %)
2545 Example in Trac #14218
2546
2547 Exammples: T5853, T10432, T5315, T9222, T2627b, T3028b
2548
2549 PS: the term "naturally coherent" doesn't really seem helpful.
2550 Perhaps "invertible" or something? I left it for now though.
2551
2552 Note [Local instances and incoherence]
2553 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2554 Consider
2555 f :: forall b c. (Eq b, forall a. Eq a => Eq (c a))
2556 => c b -> Bool
2557 f x = x==x
2558
2559 We get [W] Eq (c b), and we must use the local instance to solve it.
2560
2561 BUT that wanted also unifies with the top-level Eq [a] instance,
2562 and Eq (Maybe a) etc. We want the local instance to "win", otherwise
2563 we can't solve the wanted at all. So we mark it as Incohherent.
2564 According to Note [Rules for instance lookup] in InstEnv, that'll
2565 make it win even if there are other instances that unify.
2566
2567 Moreover this is not a hack! The evidence for this local instance
2568 will be constructed by GHC at a call site... from the very instances
2569 that unify with it here. It is not like an incoherent user-written
2570 instance which might have utterly different behaviour.
2571
2572 Consdider f :: Eq a => blah. If we have [W] Eq a, we certainly
2573 get it from the Eq a context, without worrying that there are
2574 lots of top-level instances that unify with [W] Eq a! We'll use
2575 those instances to build evidence to pass to f. That's just the
2576 nullary case of what's happening here.
2577 -}
2578
2579 matchLocalInst :: TcPredType -> CtLoc -> TcS ClsInstResult
2580 -- Look up the predicate in Given quantified constraints,
2581 -- which are effectively just local instance declarations.
2582 matchLocalInst pred loc
2583 = do { ics <- getInertCans
2584 ; case match_local_inst (inert_insts ics) of
2585 ([], False) -> return NoInstance
2586 ([(dfun_ev, inst_tys)], unifs)
2587 | not unifs
2588 -> do { let dfun_id = ctEvEvId dfun_ev
2589 ; (tys, theta) <- instDFunType dfun_id inst_tys
2590 ; return $ OneInst { cir_new_theta = theta
2591 , cir_mk_ev = evDFunApp dfun_id tys
2592 , cir_what = LocalInstance } }
2593 _ -> return NotSure }
2594 where
2595 pred_tv_set = tyCoVarsOfType pred
2596
2597 match_local_inst :: [QCInst]
2598 -> ( [(CtEvidence, [DFunInstType])]
2599 , Bool ) -- True <=> Some unify but do not match
2600 match_local_inst []
2601 = ([], False)
2602 match_local_inst (qci@(QCI { qci_tvs = qtvs, qci_pred = qpred
2603 , qci_ev = ev })
2604 : qcis)
2605 | let in_scope = mkInScopeSet (qtv_set `unionVarSet` pred_tv_set)
2606 , Just tv_subst <- ruleMatchTyKiX qtv_set (mkRnEnv2 in_scope)
2607 emptyTvSubstEnv qpred pred
2608 , let match = (ev, map (lookupVarEnv tv_subst) qtvs)
2609 = (match:matches, unif)
2610
2611 | otherwise
2612 = ASSERT2( disjointVarSet qtv_set (tyCoVarsOfType pred)
2613 , ppr qci $$ ppr pred )
2614 -- ASSERT: unification relies on the
2615 -- quantified variables being fresh
2616 (matches, unif || this_unif)
2617 where
2618 qtv_set = mkVarSet qtvs
2619 this_unif = mightMatchLater qpred (ctEvLoc ev) pred loc
2620 (matches, unif) = match_local_inst qcis
2621