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