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