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