259c570d4fb275ae50ec1cecc6c378de913682de
[ghc.git] / compiler / typecheck / TcInteract.hs
1 {-# LANGUAGE CPP #-}
2
3 module TcInteract (
4 solveSimpleGivens, -- Solves [Ct]
5 solveSimpleWanteds, -- Solves Cts
6
7 solveCallStack, -- for use in TcSimplify
8 ) where
9
10 #include "HsVersions.h"
11
12 import BasicTypes ( infinity, IntWithInf, intGtLimit )
13 import HsTypes ( HsIPName(..) )
14 import TcCanonical
15 import TcFlatten
16 import TcUnify( canSolveByUnification )
17 import VarSet
18 import Type
19 import InstEnv( DFunInstType, lookupInstEnv, instanceDFunId )
20 import CoAxiom( sfInteractTop, sfInteractInert )
21
22 import Var
23 import TcType
24 import Name
25 import PrelNames ( knownNatClassName, knownSymbolClassName,
26 typeableClassName, coercibleTyConKey,
27 heqTyConKey, ipClassKey )
28 import TysWiredIn ( typeNatKind, typeSymbolKind, heqDataCon,
29 coercibleDataCon )
30 import TysPrim ( eqPrimTyCon, eqReprPrimTyCon )
31 import Id( idType )
32 import CoAxiom ( Eqn, CoAxiom(..), CoAxBranch(..), fromBranches )
33 import Class
34 import TyCon
35 import DataCon( dataConWrapId )
36 import FunDeps
37 import FamInst
38 import FamInstEnv
39 import Unify ( tcUnifyTyWithTFs )
40
41 import TcEvidence
42 import Outputable
43
44 import TcRnTypes
45 import TcSMonad
46 import Bag
47 import MonadUtils ( concatMapM )
48
49 import Data.List( partition, foldl', deleteFirstsBy )
50 import SrcLoc
51 import VarEnv
52
53 import Control.Monad
54 import Maybes( isJust )
55 import Pair (Pair(..))
56 import Unique( hasKey )
57 import DynFlags
58 import Util
59 import qualified GHC.LanguageExtensions as LangExt
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: Trac #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 Cts
137 solveSimpleGivens givens
138 | null givens -- Shortcut for common case
139 = return emptyCts
140 | otherwise
141 = do { go givens
142 ; takeGivenInsolubles }
143 where
144 go givens = do { solveSimples (listToBag givens)
145 ; new_givens <- runTcPluginsGiven
146 ; when (notNull new_givens) $
147 go new_givens }
148
149 solveSimpleWanteds :: Cts -> TcS WantedConstraints
150 -- NB: 'simples' may contain /derived/ equalities, floated
151 -- out from a nested implication. So don't discard deriveds!
152 solveSimpleWanteds simples
153 = do { traceTcS "solveSimples {" (ppr simples)
154 ; dflags <- getDynFlags
155 ; (n,wc) <- go 1 (solverIterations dflags) (emptyWC { wc_simple = simples })
156 ; traceTcS "solveSimples end }" $
157 vcat [ text "iterations =" <+> ppr n
158 , text "residual =" <+> ppr wc ]
159 ; return wc }
160 where
161 go :: Int -> IntWithInf -> WantedConstraints -> TcS (Int, WantedConstraints)
162 go n limit wc
163 | n `intGtLimit` limit
164 = failTcS (hang (text "solveSimpleWanteds: too many iterations"
165 <+> parens (text "limit =" <+> ppr limit))
166 2 (vcat [ text "Set limit with -fsolver-iterations=n; n=0 for no limit"
167 , text "Simples =" <+> ppr simples
168 , text "WC =" <+> ppr wc ]))
169
170 | isEmptyBag (wc_simple wc)
171 = return (n,wc)
172
173 | otherwise
174 = do { -- Solve
175 (unif_count, wc1) <- solve_simple_wanteds wc
176
177 -- Run plugins
178 ; (rerun_plugin, wc2) <- runTcPluginsWanted wc1
179 -- See Note [Running plugins on unflattened wanteds]
180
181 ; if unif_count == 0 && not rerun_plugin
182 then return (n, wc2) -- Done
183 else do { traceTcS "solveSimple going round again:" (ppr rerun_plugin)
184 ; go (n+1) limit wc2 } } -- Loop
185
186
187 solve_simple_wanteds :: WantedConstraints -> TcS (Int, WantedConstraints)
188 -- Try solving these constraints
189 -- Affects the unification state (of course) but not the inert set
190 solve_simple_wanteds (WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 })
191 = nestTcS $
192 do { solveSimples simples1
193 ; (implics2, tv_eqs, fun_eqs, insols2, others) <- getUnsolvedInerts
194 ; (unif_count, unflattened_eqs) <- reportUnifications $
195 unflatten tv_eqs fun_eqs
196 -- See Note [Unflatten after solving the simple wanteds]
197 ; return ( unif_count
198 , WC { wc_simple = others `andCts` unflattened_eqs
199 , wc_insol = insols1 `andCts` insols2
200 , wc_impl = implics1 `unionBags` implics2 }) }
201
202 {- Note [The solveSimpleWanteds loop]
203 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
204 Solving a bunch of simple constraints is done in a loop,
205 (the 'go' loop of 'solveSimpleWanteds'):
206 1. Try to solve them; unflattening may lead to improvement that
207 was not exploitable during solving
208 2. Try the plugin
209 3. If step 1 did improvement during unflattening; or if the plugin
210 wants to run again, go back to step 1
211
212 Non-obviously, improvement can also take place during
213 the unflattening that takes place in step (1). See TcFlatten,
214 See Note [Unflattening can force the solver to iterate]
215 -}
216
217 -- The main solver loop implements Note [Basic Simplifier Plan]
218 ---------------------------------------------------------------
219 solveSimples :: Cts -> TcS ()
220 -- Returns the final InertSet in TcS
221 -- Has no effect on work-list or residual-implications
222 -- The constraints are initially examined in left-to-right order
223
224 solveSimples cts
225 = {-# SCC "solveSimples" #-}
226 do { updWorkListTcS (\wl -> foldrBag extendWorkListCt wl cts)
227 ; solve_loop }
228 where
229 solve_loop
230 = {-# SCC "solve_loop" #-}
231 do { sel <- selectNextWorkItem
232 ; case sel of
233 Nothing -> return ()
234 Just ct -> do { runSolverPipeline thePipeline ct
235 ; solve_loop } }
236
237 -- | Extract the (inert) givens and invoke the plugins on them.
238 -- Remove solved givens from the inert set and emit insolubles, but
239 -- return new work produced so that 'solveSimpleGivens' can feed it back
240 -- into the main solver.
241 runTcPluginsGiven :: TcS [Ct]
242 runTcPluginsGiven
243 = do { plugins <- getTcPlugins
244 ; if null plugins then return [] else
245 do { givens <- getInertGivens
246 ; if null givens then return [] else
247 do { p <- runTcPlugins plugins (givens,[],[])
248 ; let (solved_givens, _, _) = pluginSolvedCts p
249 ; updInertCans (removeInertCts solved_givens)
250 ; mapM_ emitInsoluble (pluginBadCts p)
251 ; return (pluginNewCts p) } } }
252
253 -- | Given a bag of (flattened, zonked) wanteds, invoke the plugins on
254 -- them and produce an updated bag of wanteds (possibly with some new
255 -- work) and a bag of insolubles. The boolean indicates whether
256 -- 'solveSimpleWanteds' should feed the updated wanteds back into the
257 -- main solver.
258 runTcPluginsWanted :: WantedConstraints -> TcS (Bool, WantedConstraints)
259 runTcPluginsWanted wc@(WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 })
260 | isEmptyBag simples1
261 = return (False, wc)
262 | otherwise
263 = do { plugins <- getTcPlugins
264 ; if null plugins then return (False, wc) else
265
266 do { given <- getInertGivens
267 ; simples1 <- zonkSimples simples1 -- Plugin requires zonked inputs
268 ; let (wanted, derived) = partition isWantedCt (bagToList simples1)
269 ; p <- runTcPlugins plugins (given, derived, wanted)
270 ; let (_, _, solved_wanted) = pluginSolvedCts p
271 (_, unsolved_derived, unsolved_wanted) = pluginInputCts p
272 new_wanted = pluginNewCts p
273
274 -- SLPJ: I'm deeply suspicious of this
275 -- ; updInertCans (removeInertCts $ solved_givens ++ solved_deriveds)
276
277 ; mapM_ setEv solved_wanted
278 ; return ( notNull (pluginNewCts p)
279 , WC { wc_simple = listToBag new_wanted `andCts` listToBag unsolved_wanted
280 `andCts` listToBag unsolved_derived
281 , wc_insol = listToBag (pluginBadCts p) `andCts` insols1
282 , wc_impl = implics1 } ) } }
283 where
284 setEv :: (EvTerm,Ct) -> TcS ()
285 setEv (ev,ct) = case ctEvidence ct of
286 CtWanted { ctev_dest = dest } -> setWantedEvTerm dest ev
287 _ -> panic "runTcPluginsWanted.setEv: attempt to solve non-wanted!"
288
289 -- | A triple of (given, derived, wanted) constraints to pass to plugins
290 type SplitCts = ([Ct], [Ct], [Ct])
291
292 -- | A solved triple of constraints, with evidence for wanteds
293 type SolvedCts = ([Ct], [Ct], [(EvTerm,Ct)])
294
295 -- | Represents collections of constraints generated by typechecker
296 -- plugins
297 data TcPluginProgress = TcPluginProgress
298 { pluginInputCts :: SplitCts
299 -- ^ Original inputs to the plugins with solved/bad constraints
300 -- removed, but otherwise unmodified
301 , pluginSolvedCts :: SolvedCts
302 -- ^ Constraints solved by plugins
303 , pluginBadCts :: [Ct]
304 -- ^ Constraints reported as insoluble by plugins
305 , pluginNewCts :: [Ct]
306 -- ^ New constraints emitted by plugins
307 }
308
309 getTcPlugins :: TcS [TcPluginSolver]
310 getTcPlugins = do { tcg_env <- getGblEnv; return (tcg_tc_plugins tcg_env) }
311
312 -- | Starting from a triple of (given, derived, wanted) constraints,
313 -- invoke each of the typechecker plugins in turn and return
314 --
315 -- * the remaining unmodified constraints,
316 -- * constraints that have been solved,
317 -- * constraints that are insoluble, and
318 -- * new work.
319 --
320 -- Note that new work generated by one plugin will not be seen by
321 -- other plugins on this pass (but the main constraint solver will be
322 -- re-invoked and they will see it later). There is no check that new
323 -- work differs from the original constraints supplied to the plugin:
324 -- the plugin itself should perform this check if necessary.
325 runTcPlugins :: [TcPluginSolver] -> SplitCts -> TcS TcPluginProgress
326 runTcPlugins plugins all_cts
327 = foldM do_plugin initialProgress plugins
328 where
329 do_plugin :: TcPluginProgress -> TcPluginSolver -> TcS TcPluginProgress
330 do_plugin p solver = do
331 result <- runTcPluginTcS (uncurry3 solver (pluginInputCts p))
332 return $ progress p result
333
334 progress :: TcPluginProgress -> TcPluginResult -> TcPluginProgress
335 progress p (TcPluginContradiction bad_cts) =
336 p { pluginInputCts = discard bad_cts (pluginInputCts p)
337 , pluginBadCts = bad_cts ++ pluginBadCts p
338 }
339 progress p (TcPluginOk solved_cts new_cts) =
340 p { pluginInputCts = discard (map snd solved_cts) (pluginInputCts p)
341 , pluginSolvedCts = add solved_cts (pluginSolvedCts p)
342 , pluginNewCts = new_cts ++ pluginNewCts p
343 }
344
345 initialProgress = TcPluginProgress all_cts ([], [], []) [] []
346
347 discard :: [Ct] -> SplitCts -> SplitCts
348 discard cts (xs, ys, zs) =
349 (xs `without` cts, ys `without` cts, zs `without` cts)
350
351 without :: [Ct] -> [Ct] -> [Ct]
352 without = deleteFirstsBy eqCt
353
354 eqCt :: Ct -> Ct -> Bool
355 eqCt c c' = case (ctEvidence c, ctEvidence c') of
356 (CtGiven pred _ _, CtGiven pred' _ _) -> pred `eqType` pred'
357 (CtWanted pred _ _, CtWanted pred' _ _) -> pred `eqType` pred'
358 (CtDerived pred _ , CtDerived pred' _ ) -> pred `eqType` pred'
359 (_ , _ ) -> False
360
361 add :: [(EvTerm,Ct)] -> SolvedCts -> SolvedCts
362 add xs scs = foldl' addOne scs xs
363
364 addOne :: SolvedCts -> (EvTerm,Ct) -> SolvedCts
365 addOne (givens, deriveds, wanteds) (ev,ct) = case ctEvidence ct of
366 CtGiven {} -> (ct:givens, deriveds, wanteds)
367 CtDerived{} -> (givens, ct:deriveds, wanteds)
368 CtWanted {} -> (givens, deriveds, (ev,ct):wanteds)
369
370
371 type WorkItem = Ct
372 type SimplifierStage = WorkItem -> TcS (StopOrContinue Ct)
373
374 runSolverPipeline :: [(String,SimplifierStage)] -- The pipeline
375 -> WorkItem -- The work item
376 -> TcS ()
377 -- Run this item down the pipeline, leaving behind new work and inerts
378 runSolverPipeline pipeline workItem
379 = do { initial_is <- getTcSInerts
380 ; traceTcS "Start solver pipeline {" $
381 vcat [ text "work item = " <+> ppr workItem
382 , text "inerts = " <+> ppr initial_is]
383
384 ; bumpStepCountTcS -- One step for each constraint processed
385 ; final_res <- run_pipeline pipeline (ContinueWith workItem)
386
387 ; final_is <- getTcSInerts
388 ; case final_res of
389 Stop ev s -> do { traceFireTcS ev s
390 ; traceTcS "End solver pipeline (discharged) }"
391 (text "inerts =" <+> ppr final_is)
392 ; return () }
393 ContinueWith ct -> do { traceFireTcS (ctEvidence ct) (text "Kept as inert")
394 ; traceTcS "End solver pipeline (kept as inert) }" $
395 vcat [ text "final_item =" <+> ppr ct
396 , pprTvBndrs $ tyCoVarsOfCtList ct
397 , text "inerts =" <+> ppr final_is]
398 ; addInertCan ct }
399 }
400 where run_pipeline :: [(String,SimplifierStage)] -> StopOrContinue Ct
401 -> TcS (StopOrContinue Ct)
402 run_pipeline [] res = return res
403 run_pipeline _ (Stop ev s) = return (Stop ev s)
404 run_pipeline ((stg_name,stg):stgs) (ContinueWith ct)
405 = do { traceTcS ("runStage " ++ stg_name ++ " {")
406 (text "workitem = " <+> ppr ct)
407 ; res <- stg ct
408 ; traceTcS ("end stage " ++ stg_name ++ " }") empty
409 ; run_pipeline stgs res }
410
411 {-
412 Example 1:
413 Inert: {c ~ d, F a ~ t, b ~ Int, a ~ ty} (all given)
414 Reagent: a ~ [b] (given)
415
416 React with (c~d) ==> IR (ContinueWith (a~[b])) True []
417 React with (F a ~ t) ==> IR (ContinueWith (a~[b])) False [F [b] ~ t]
418 React with (b ~ Int) ==> IR (ContinueWith (a~[Int]) True []
419
420 Example 2:
421 Inert: {c ~w d, F a ~g t, b ~w Int, a ~w ty}
422 Reagent: a ~w [b]
423
424 React with (c ~w d) ==> IR (ContinueWith (a~[b])) True []
425 React with (F a ~g t) ==> IR (ContinueWith (a~[b])) True [] (can't rewrite given with wanted!)
426 etc.
427
428 Example 3:
429 Inert: {a ~ Int, F Int ~ b} (given)
430 Reagent: F a ~ b (wanted)
431
432 React with (a ~ Int) ==> IR (ContinueWith (F Int ~ b)) True []
433 React with (F Int ~ b) ==> IR Stop True [] -- after substituting we re-canonicalize and get nothing
434 -}
435
436 thePipeline :: [(String,SimplifierStage)]
437 thePipeline = [ ("canonicalization", TcCanonical.canonicalize)
438 , ("interact with inerts", interactWithInertsStage)
439 , ("top-level reactions", topReactionsStage) ]
440
441 {-
442 *********************************************************************************
443 * *
444 The interact-with-inert Stage
445 * *
446 *********************************************************************************
447
448 Note [The Solver Invariant]
449 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
450 We always add Givens first. So you might think that the solver has
451 the invariant
452
453 If the work-item is Given,
454 then the inert item must Given
455
456 But this isn't quite true. Suppose we have,
457 c1: [W] beta ~ [alpha], c2 : [W] blah, c3 :[W] alpha ~ Int
458 After processing the first two, we get
459 c1: [G] beta ~ [alpha], c2 : [W] blah
460 Now, c3 does not interact with the the given c1, so when we spontaneously
461 solve c3, we must re-react it with the inert set. So we can attempt a
462 reaction between inert c2 [W] and work-item c3 [G].
463
464 It *is* true that [Solver Invariant]
465 If the work-item is Given,
466 AND there is a reaction
467 then the inert item must Given
468 or, equivalently,
469 If the work-item is Given,
470 and the inert item is Wanted/Derived
471 then there is no reaction
472 -}
473
474 -- Interaction result of WorkItem <~> Ct
475
476 type StopNowFlag = Bool -- True <=> stop after this interaction
477
478 interactWithInertsStage :: WorkItem -> TcS (StopOrContinue Ct)
479 -- Precondition: if the workitem is a CTyEqCan then it will not be able to
480 -- react with anything at this stage.
481
482 interactWithInertsStage wi
483 = do { inerts <- getTcSInerts
484 ; let ics = inert_cans inerts
485 ; case wi of
486 CTyEqCan {} -> interactTyVarEq ics wi
487 CFunEqCan {} -> interactFunEq ics wi
488 CIrredEvCan {} -> interactIrred ics wi
489 CDictCan {} -> interactDict ics wi
490 _ -> pprPanic "interactWithInerts" (ppr wi) }
491 -- CHoleCan are put straight into inert_frozen, so never get here
492 -- CNonCanonical have been canonicalised
493
494 data InteractResult
495 = IRKeep -- Keep the existing inert constraint in the inert set
496 | IRReplace -- Replace the existing inert constraint with the work item
497 | IRDelete -- Delete the existing inert constraint from the inert set
498
499 instance Outputable InteractResult where
500 ppr IRKeep = text "keep"
501 ppr IRReplace = text "replace"
502 ppr IRDelete = text "delete"
503
504 solveOneFromTheOther :: CtEvidence -- Inert
505 -> CtEvidence -- WorkItem
506 -> TcS (InteractResult, StopNowFlag)
507 -- Preconditions:
508 -- 1) inert and work item represent evidence for the /same/ predicate
509 -- 2) ip/class/irred constraints only; not used for equalities
510 solveOneFromTheOther ev_i ev_w
511 | isDerived ev_w -- Work item is Derived; just discard it
512 = return (IRKeep, True)
513
514 | isDerived ev_i -- The inert item is Derived, we can just throw it away,
515 = return (IRDelete, False) -- The ev_w is inert wrt earlier inert-set items,
516 -- so it's safe to continue on from this point
517
518 | CtWanted { ctev_loc = loc_w } <- ev_w
519 , prohibitedSuperClassSolve (ctEvLoc ev_i) loc_w
520 = return (IRDelete, False)
521
522 | CtWanted { ctev_dest = dest } <- ev_w
523 -- Inert is Given or Wanted
524 = do { setWantedEvTerm dest (ctEvTerm ev_i)
525 ; return (IRKeep, True) }
526
527 | CtWanted { ctev_loc = loc_i } <- ev_i -- Work item is Given
528 , prohibitedSuperClassSolve (ctEvLoc ev_w) loc_i
529 = return (IRKeep, False) -- Just discard the un-usable Given
530 -- This never actually happens because
531 -- Givens get processed first
532
533 | CtWanted { ctev_dest = dest } <- ev_i
534 = do { setWantedEvTerm dest (ctEvTerm ev_w)
535 ; return (IRReplace, True) }
536
537 -- So they are both Given
538 -- See Note [Replacement vs keeping]
539 | lvl_i == lvl_w
540 = do { binds <- getTcEvBindsMap
541 ; return (same_level_strategy binds, True) }
542
543 | otherwise -- Both are Given, levels differ
544 = return (different_level_strategy, True)
545 where
546 pred = ctEvPred ev_i
547 loc_i = ctEvLoc ev_i
548 loc_w = ctEvLoc ev_w
549 lvl_i = ctLocLevel loc_i
550 lvl_w = ctLocLevel loc_w
551
552 different_level_strategy
553 | isIPPred pred, lvl_w > lvl_i = IRReplace
554 | lvl_w < lvl_i = IRReplace
555 | otherwise = IRKeep
556
557 same_level_strategy binds -- Both Given
558 | GivenOrigin (InstSC s_i) <- ctLocOrigin loc_i
559 = case ctLocOrigin loc_w of
560 GivenOrigin (InstSC s_w) | s_w < s_i -> IRReplace
561 | otherwise -> IRKeep
562 _ -> IRReplace
563
564 | GivenOrigin (InstSC {}) <- ctLocOrigin loc_w
565 = IRKeep
566
567 | has_binding binds ev_w
568 , not (has_binding binds ev_i)
569 = IRReplace
570
571 | otherwise = IRKeep
572
573 has_binding binds ev = isJust (lookupEvBind binds (ctEvId ev))
574
575 {-
576 Note [Replacement vs keeping]
577 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
578 When we have two Given constraints both of type (C tys), say, which should
579 we keep? More subtle than you might think!
580
581 * Constraints come from different levels (different_level_strategy)
582
583 - For implicit parameters we want to keep the innermost (deepest)
584 one, so that it overrides the outer one.
585 See Note [Shadowing of Implicit Parameters]
586
587 - For everything else, we want to keep the outermost one. Reason: that
588 makes it more likely that the inner one will turn out to be unused,
589 and can be reported as redundant. See Note [Tracking redundant constraints]
590 in TcSimplify.
591
592 It transpires that using the outermost one is reponsible for an
593 8% performance improvement in nofib cryptarithm2, compared to
594 just rolling the dice. I didn't investigate why.
595
596 * Constaints coming from the same level (i.e. same implication)
597
598 - Always get rid of InstSC ones if possible, since they are less
599 useful for solving. If both are InstSC, choose the one with
600 the smallest TypeSize
601 See Note [Solving superclass constraints] in TcInstDcls
602
603 - Keep the one that has a non-trivial evidence binding.
604 Example: f :: (Eq a, Ord a) => blah
605 then we may find [G] d3 :: Eq a
606 [G] d2 :: Eq a
607 with bindings d3 = sc_sel (d1::Ord a)
608 We want to discard d2 in favour of the superclass selection from
609 the Ord dictionary.
610 Why? See Note [Tracking redundant constraints] in TcSimplify again.
611
612 * Finally, when there is still a choice, use IRKeep rather than
613 IRReplace, to avoid unnecessary munging of the inert set.
614
615 Doing the depth-check for implicit parameters, rather than making the work item
616 always overrride, is important. Consider
617
618 data T a where { T1 :: (?x::Int) => T Int; T2 :: T a }
619
620 f :: (?x::a) => T a -> Int
621 f T1 = ?x
622 f T2 = 3
623
624 We have a [G] (?x::a) in the inert set, and at the pattern match on T1 we add
625 two new givens in the work-list: [G] (?x::Int)
626 [G] (a ~ Int)
627 Now consider these steps
628 - process a~Int, kicking out (?x::a)
629 - process (?x::Int), the inner given, adding to inert set
630 - process (?x::a), the outer given, overriding the inner given
631 Wrong! The depth-check ensures that the inner implicit parameter wins.
632 (Actually I think that the order in which the work-list is processed means
633 that this chain of events won't happen, but that's very fragile.)
634
635 *********************************************************************************
636 * *
637 interactIrred
638 * *
639 *********************************************************************************
640 -}
641
642 -- Two pieces of irreducible evidence: if their types are *exactly identical*
643 -- we can rewrite them. We can never improve using this:
644 -- if we want ty1 :: Constraint and have ty2 :: Constraint it clearly does not
645 -- mean that (ty1 ~ ty2)
646 interactIrred :: InertCans -> Ct -> TcS (StopOrContinue Ct)
647
648 interactIrred inerts workItem@(CIrredEvCan { cc_ev = ev_w })
649 | let pred = ctEvPred ev_w
650 (matching_irreds, others)
651 = partitionBag (\ct -> ctPred ct `tcEqTypeNoKindCheck` pred)
652 (inert_irreds inerts)
653 , (ct_i : rest) <- bagToList matching_irreds
654 , let ctev_i = ctEvidence ct_i
655 = ASSERT( null rest )
656 do { (inert_effect, stop_now) <- solveOneFromTheOther ctev_i ev_w
657 ; case inert_effect of
658 IRKeep -> return ()
659 IRDelete -> updInertIrreds (\_ -> others)
660 IRReplace -> updInertIrreds (\_ -> others `snocCts` workItem)
661 -- These const upd's assume that solveOneFromTheOther
662 -- has no side effects on InertCans
663 ; if stop_now then
664 return (Stop ev_w (text "Irred equal" <+> parens (ppr inert_effect)))
665 ; else
666 continueWith workItem }
667
668 | otherwise
669 = continueWith workItem
670
671 interactIrred _ wi = pprPanic "interactIrred" (ppr wi)
672
673 {-
674 *********************************************************************************
675 * *
676 interactDict
677 * *
678 *********************************************************************************
679 -}
680
681 interactDict :: InertCans -> Ct -> TcS (StopOrContinue Ct)
682 interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs = tys })
683 | isWanted ev_w
684 , Just ip_name <- isCallStackPred (ctPred workItem)
685 , OccurrenceOf func <- ctLocOrigin (ctEvLoc ev_w)
686 -- If we're given a CallStack constraint that arose from a function
687 -- call, we need to push the current call-site onto the stack instead
688 -- of solving it directly from a given.
689 -- See Note [Overview of implicit CallStacks]
690 = do { let loc = ctEvLoc ev_w
691
692 -- First we emit a new constraint that will capture the
693 -- given CallStack.
694 ; let new_loc = setCtLocOrigin loc (IPOccOrigin (HsIPName ip_name))
695 -- We change the origin to IPOccOrigin so
696 -- this rule does not fire again.
697 -- See Note [Overview of implicit CallStacks]
698
699 ; mb_new <- newWantedEvVar new_loc (ctEvPred ev_w)
700 ; emitWorkNC (freshGoals [mb_new])
701
702 -- Then we solve the wanted by pushing the call-site onto the
703 -- newly emitted CallStack.
704 ; let ev_cs = EvCsPushCall func (ctLocSpan loc) (getEvTerm mb_new)
705 ; solveCallStack ev_w ev_cs
706 ; stopWith ev_w "Wanted CallStack IP" }
707
708 | Just ctev_i <- lookupInertDict inerts cls tys
709 = do { (inert_effect, stop_now) <- solveOneFromTheOther ctev_i ev_w
710 ; case inert_effect of
711 IRKeep -> return ()
712 IRDelete -> updInertDicts $ \ ds -> delDict ds cls tys
713 IRReplace -> updInertDicts $ \ ds -> addDict ds cls tys workItem
714 ; if stop_now then
715 return (Stop ev_w (text "Dict equal" <+> parens (ppr inert_effect)))
716 else
717 continueWith workItem }
718
719 | cls `hasKey` ipClassKey
720 , isGiven ev_w
721 = interactGivenIP inerts workItem
722
723 | otherwise
724 = do { addFunDepWork inerts ev_w cls
725 ; continueWith workItem }
726
727 interactDict _ wi = pprPanic "interactDict" (ppr wi)
728
729 addFunDepWork :: InertCans -> CtEvidence -> Class -> TcS ()
730 -- Add derived constraints from type-class functional dependencies.
731 addFunDepWork inerts work_ev cls
732 = mapBagM_ add_fds (findDictsByClass (inert_dicts inerts) cls)
733 -- No need to check flavour; fundeps work between
734 -- any pair of constraints, regardless of flavour
735 -- Importantly we don't throw workitem back in the
736 -- worklist because this can cause loops (see #5236)
737 where
738 work_pred = ctEvPred work_ev
739 work_loc = ctEvLoc work_ev
740 add_fds inert_ct
741 = emitFunDepDeriveds $
742 improveFromAnother derived_loc inert_pred work_pred
743 -- We don't really rewrite tys2, see below _rewritten_tys2, so that's ok
744 -- NB: We do create FDs for given to report insoluble equations that arise
745 -- from pairs of Givens, and also because of floating when we approximate
746 -- implications. The relevant test is: typecheck/should_fail/FDsFromGivens.hs
747 where
748 inert_pred = ctPred inert_ct
749 inert_loc = ctLoc inert_ct
750 derived_loc = work_loc { ctl_origin = FunDepOrigin1 work_pred work_loc
751 inert_pred inert_loc }
752
753 {-
754 **********************************************************************
755 * *
756 Implicit parameters
757 * *
758 **********************************************************************
759 -}
760
761 interactGivenIP :: InertCans -> Ct -> TcS (StopOrContinue Ct)
762 -- Work item is Given (?x:ty)
763 -- See Note [Shadowing of Implicit Parameters]
764 interactGivenIP inerts workItem@(CDictCan { cc_ev = ev, cc_class = cls
765 , cc_tyargs = tys@(ip_str:_) })
766 = do { updInertCans $ \cans -> cans { inert_dicts = addDict filtered_dicts cls tys workItem }
767 ; stopWith ev "Given IP" }
768 where
769 dicts = inert_dicts inerts
770 ip_dicts = findDictsByClass dicts cls
771 other_ip_dicts = filterBag (not . is_this_ip) ip_dicts
772 filtered_dicts = addDictsByClass dicts cls other_ip_dicts
773
774 -- Pick out any Given constraints for the same implicit parameter
775 is_this_ip (CDictCan { cc_ev = ev, cc_tyargs = ip_str':_ })
776 = isGiven ev && ip_str `tcEqType` ip_str'
777 is_this_ip _ = False
778
779 interactGivenIP _ wi = pprPanic "interactGivenIP" (ppr wi)
780
781
782 {-
783 Note [Shadowing of Implicit Parameters]
784 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
785 Consider the following example:
786
787 f :: (?x :: Char) => Char
788 f = let ?x = 'a' in ?x
789
790 The "let ?x = ..." generates an implication constraint of the form:
791
792 ?x :: Char => ?x :: Char
793
794 Furthermore, the signature for `f` also generates an implication
795 constraint, so we end up with the following nested implication:
796
797 ?x :: Char => (?x :: Char => ?x :: Char)
798
799 Note that the wanted (?x :: Char) constraint may be solved in
800 two incompatible ways: either by using the parameter from the
801 signature, or by using the local definition. Our intention is
802 that the local definition should "shadow" the parameter of the
803 signature, and we implement this as follows: when we add a new
804 *given* implicit parameter to the inert set, it replaces any existing
805 givens for the same implicit parameter.
806
807 This works for the normal cases but it has an odd side effect
808 in some pathological programs like this:
809
810 -- This is accepted, the second parameter shadows
811 f1 :: (?x :: Int, ?x :: Char) => Char
812 f1 = ?x
813
814 -- This is rejected, the second parameter shadows
815 f2 :: (?x :: Int, ?x :: Char) => Int
816 f2 = ?x
817
818 Both of these are actually wrong: when we try to use either one,
819 we'll get two incompatible wnated constraints (?x :: Int, ?x :: Char),
820 which would lead to an error.
821
822 I can think of two ways to fix this:
823
824 1. Simply disallow multiple constratits for the same implicit
825 parameter---this is never useful, and it can be detected completely
826 syntactically.
827
828 2. Move the shadowing machinery to the location where we nest
829 implications, and add some code here that will produce an
830 error if we get multiple givens for the same implicit parameter.
831
832
833 **********************************************************************
834 * *
835 interactFunEq
836 * *
837 **********************************************************************
838 -}
839
840 interactFunEq :: InertCans -> Ct -> TcS (StopOrContinue Ct)
841 -- Try interacting the work item with the inert set
842 interactFunEq inerts workItem@(CFunEqCan { cc_ev = ev, cc_fun = tc
843 , cc_tyargs = args, cc_fsk = fsk })
844 | Just (CFunEqCan { cc_ev = ev_i
845 , cc_fsk = fsk_i }) <- matching_inerts
846 = if ev_i `funEqCanDischarge` ev
847 then -- Rewrite work-item using inert
848 do { traceTcS "reactFunEq (discharge work item):" $
849 vcat [ text "workItem =" <+> ppr workItem
850 , text "inertItem=" <+> ppr ev_i ]
851 ; reactFunEq ev_i fsk_i ev fsk
852 ; stopWith ev "Inert rewrites work item" }
853 else -- Rewrite inert using work-item
854 ASSERT2( ev `funEqCanDischarge` ev_i, ppr ev $$ ppr ev_i )
855 do { traceTcS "reactFunEq (rewrite inert item):" $
856 vcat [ text "workItem =" <+> ppr workItem
857 , text "inertItem=" <+> ppr ev_i ]
858 ; updInertFunEqs $ \ feqs -> insertFunEq feqs tc args workItem
859 -- Do the updInertFunEqs before the reactFunEq, so that
860 -- we don't kick out the inertItem as well as consuming it!
861 ; reactFunEq ev fsk ev_i fsk_i
862 ; stopWith ev "Work item rewrites inert" }
863
864 | otherwise -- Try improvement
865 = do { improveLocalFunEqs loc inerts tc args fsk
866 ; continueWith workItem }
867 where
868 loc = ctEvLoc ev
869 funeqs = inert_funeqs inerts
870 matching_inerts = findFunEq funeqs tc args
871
872 interactFunEq _ workItem = pprPanic "interactFunEq" (ppr workItem)
873
874 improveLocalFunEqs :: CtLoc -> InertCans -> TyCon -> [TcType] -> TcTyVar
875 -> TcS ()
876 -- Generate derived improvement equalities, by comparing
877 -- the current work item with inert CFunEqs
878 -- E.g. x + y ~ z, x + y' ~ z => [D] y ~ y'
879 improveLocalFunEqs loc inerts fam_tc args fsk
880 | not (null improvement_eqns)
881 = do { traceTcS "interactFunEq improvements: " $
882 vcat [ text "Eqns:" <+> ppr improvement_eqns
883 , text "Candidates:" <+> ppr funeqs_for_tc
884 , text "Model:" <+> ppr model ]
885 ; mapM_ (unifyDerived loc Nominal) improvement_eqns }
886 | otherwise
887 = return ()
888 where
889 model = inert_model inerts
890 funeqs = inert_funeqs inerts
891 funeqs_for_tc = findFunEqsByTyCon funeqs fam_tc
892 rhs = lookupFlattenTyVar model fsk
893
894 --------------------
895 improvement_eqns
896 | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc
897 = -- Try built-in families, notably for arithmethic
898 concatMap (do_one_built_in ops) funeqs_for_tc
899
900 | Injective injective_args <- familyTyConInjectivityInfo fam_tc
901 = -- Try improvement from type families with injectivity annotations
902 concatMap (do_one_injective injective_args) funeqs_for_tc
903
904 | otherwise
905 = []
906
907 --------------------
908 do_one_built_in ops (CFunEqCan { cc_tyargs = iargs, cc_fsk = ifsk })
909 = sfInteractInert ops args rhs iargs (lookupFlattenTyVar model ifsk)
910 do_one_built_in _ _ = pprPanic "interactFunEq 1" (ppr fam_tc)
911
912 --------------------
913 -- See Note [Type inference for type families with injectivity]
914 do_one_injective injective_args
915 (CFunEqCan { cc_tyargs = iargs, cc_fsk = ifsk })
916 | rhs `tcEqType` lookupFlattenTyVar model ifsk
917 = [Pair arg iarg | (arg, iarg, True)
918 <- zip3 args iargs injective_args ]
919 | otherwise
920 = []
921 do_one_injective _ _ = pprPanic "interactFunEq 2" (ppr fam_tc)
922
923 -------------
924 lookupFlattenTyVar :: InertModel -> TcTyVar -> TcType
925 -- See Note [lookupFlattenTyVar]
926 lookupFlattenTyVar model ftv
927 = case lookupDVarEnv model ftv of
928 Just (CTyEqCan { cc_rhs = rhs, cc_eq_rel = NomEq }) -> rhs
929 _ -> mkTyVarTy ftv
930
931 reactFunEq :: CtEvidence -> TcTyVar -- From this :: F args1 ~ fsk1
932 -> CtEvidence -> TcTyVar -- Solve this :: F args2 ~ fsk2
933 -> TcS ()
934 reactFunEq from_this fsk1 solve_this fsk2
935 | CtGiven { ctev_evar = evar, ctev_loc = loc } <- solve_this
936 = do { let fsk_eq_co = mkTcSymCo (mkTcCoVarCo evar) `mkTcTransCo`
937 ctEvCoercion from_this
938 -- :: fsk2 ~ fsk1
939 fsk_eq_pred = mkTcEqPredLikeEv solve_this
940 (mkTyVarTy fsk2) (mkTyVarTy fsk1)
941
942 ; new_ev <- newGivenEvVar loc (fsk_eq_pred, EvCoercion fsk_eq_co)
943 ; emitWorkNC [new_ev] }
944
945 | otherwise
946 = do { traceTcS "reactFunEq" (ppr from_this $$ ppr fsk1 $$
947 ppr solve_this $$ ppr fsk2)
948 ; dischargeFmv solve_this fsk2 (ctEvCoercion from_this) (mkTyVarTy fsk1)
949 ; traceTcS "reactFunEq done" (ppr from_this $$ ppr fsk1 $$
950 ppr solve_this $$ ppr fsk2) }
951
952 {- Note [lookupFlattenTyVar]
953 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
954 Supppose we have an injective function F and
955 inert_funeqs: F t1 ~ fsk1
956 F t2 ~ fsk2
957 model fsk1 ~ fsk2
958
959 We never rewrite the RHS (cc_fsk) of a CFunEqCan. But we /do/ want to
960 get the [D] t1 ~ t2 from the injectiveness of F. So we look up the
961 cc_fsk of CFunEqCans in the model when trying to find derived
962 equalities arising from injectivity.
963
964 Note [Type inference for type families with injectivity]
965 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
966 Suppose we have a type family with an injectivity annotation:
967 type family F a b = r | r -> b
968
969 Then if we have two CFunEqCan constraints for F with the same RHS
970 F s1 t1 ~ rhs
971 F s2 t2 ~ rhs
972 then we can use the injectivity to get a new Derived constraint on
973 the injective argument
974 [D] t1 ~ t2
975
976 That in turn can help GHC solve constraints that would otherwise require
977 guessing. For example, consider the ambiguity check for
978 f :: F Int b -> Int
979 We get the constraint
980 [W] F Int b ~ F Int beta
981 where beta is a unification variable. Injectivity lets us pick beta ~ b.
982
983 Injectivity information is also used at the call sites. For example:
984 g = f True
985 gives rise to
986 [W] F Int b ~ Bool
987 from which we can derive b. This requires looking at the defining equations of
988 a type family, ie. finding equation with a matching RHS (Bool in this example)
989 and infering values of type variables (b in this example) from the LHS patterns
990 of the matching equation. For closed type families we have to perform
991 additional apartness check for the selected equation to check that the selected
992 is guaranteed to fire for given LHS arguments.
993
994 These new constraints are simply *Derived* constraints; they have no evidence.
995 We could go further and offer evidence from decomposing injective type-function
996 applications, but that would require new evidence forms, and an extension to
997 FC, so we don't do that right now (Dec 14).
998
999 See also Note [Injective type families] in TyCon
1000
1001
1002 Note [Cache-caused loops]
1003 ~~~~~~~~~~~~~~~~~~~~~~~~~
1004 It is very dangerous to cache a rewritten wanted family equation as 'solved' in our
1005 solved cache (which is the default behaviour or xCtEvidence), because the interaction
1006 may not be contributing towards a solution. Here is an example:
1007
1008 Initial inert set:
1009 [W] g1 : F a ~ beta1
1010 Work item:
1011 [W] g2 : F a ~ beta2
1012 The work item will react with the inert yielding the _same_ inert set plus:
1013 i) Will set g2 := g1 `cast` g3
1014 ii) Will add to our solved cache that [S] g2 : F a ~ beta2
1015 iii) Will emit [W] g3 : beta1 ~ beta2
1016 Now, the g3 work item will be spontaneously solved to [G] g3 : beta1 ~ beta2
1017 and then it will react the item in the inert ([W] g1 : F a ~ beta1). So it
1018 will set
1019 g1 := g ; sym g3
1020 and what is g? Well it would ideally be a new goal of type (F a ~ beta2) but
1021 remember that we have this in our solved cache, and it is ... g2! In short we
1022 created the evidence loop:
1023
1024 g2 := g1 ; g3
1025 g3 := refl
1026 g1 := g2 ; sym g3
1027
1028 To avoid this situation we do not cache as solved any workitems (or inert)
1029 which did not really made a 'step' towards proving some goal. Solved's are
1030 just an optimization so we don't lose anything in terms of completeness of
1031 solving.
1032
1033
1034 Note [Efficient Orientation]
1035 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1036 Suppose we are interacting two FunEqCans with the same LHS:
1037 (inert) ci :: (F ty ~ xi_i)
1038 (work) cw :: (F ty ~ xi_w)
1039 We prefer to keep the inert (else we pass the work item on down
1040 the pipeline, which is a bit silly). If we keep the inert, we
1041 will (a) discharge 'cw'
1042 (b) produce a new equality work-item (xi_w ~ xi_i)
1043 Notice the orientation (xi_w ~ xi_i) NOT (xi_i ~ xi_w):
1044 new_work :: xi_w ~ xi_i
1045 cw := ci ; sym new_work
1046 Why? Consider the simplest case when xi1 is a type variable. If
1047 we generate xi1~xi2, porcessing that constraint will kick out 'ci'.
1048 If we generate xi2~xi1, there is less chance of that happening.
1049 Of course it can and should still happen if xi1=a, xi1=Int, say.
1050 But we want to avoid it happening needlessly.
1051
1052 Similarly, if we *can't* keep the inert item (because inert is Wanted,
1053 and work is Given, say), we prefer to orient the new equality (xi_i ~
1054 xi_w).
1055
1056 Note [Carefully solve the right CFunEqCan]
1057 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1058 ---- OLD COMMENT, NOW NOT NEEDED
1059 ---- because we now allow multiple
1060 ---- wanted FunEqs with the same head
1061 Consider the constraints
1062 c1 :: F Int ~ a -- Arising from an application line 5
1063 c2 :: F Int ~ Bool -- Arising from an application line 10
1064 Suppose that 'a' is a unification variable, arising only from
1065 flattening. So there is no error on line 5; it's just a flattening
1066 variable. But there is (or might be) an error on line 10.
1067
1068 Two ways to combine them, leaving either (Plan A)
1069 c1 :: F Int ~ a -- Arising from an application line 5
1070 c3 :: a ~ Bool -- Arising from an application line 10
1071 or (Plan B)
1072 c2 :: F Int ~ Bool -- Arising from an application line 10
1073 c4 :: a ~ Bool -- Arising from an application line 5
1074
1075 Plan A will unify c3, leaving c1 :: F Int ~ Bool as an error
1076 on the *totally innocent* line 5. An example is test SimpleFail16
1077 where the expected/actual message comes out backwards if we use
1078 the wrong plan.
1079
1080 The second is the right thing to do. Hence the isMetaTyVarTy
1081 test when solving pairwise CFunEqCan.
1082
1083
1084 **********************************************************************
1085 * *
1086 interactTyVarEq
1087 * *
1088 **********************************************************************
1089 -}
1090
1091 interactTyVarEq :: InertCans -> Ct -> TcS (StopOrContinue Ct)
1092 -- CTyEqCans are always consumed, so always returns Stop
1093 interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv
1094 , cc_rhs = rhs
1095 , cc_ev = ev
1096 , cc_eq_rel = eq_rel })
1097 | (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i }
1098 <- findTyEqs inerts tv
1099 , ev_i `eqCanDischarge` ev
1100 , rhs_i `tcEqType` rhs ]
1101 = -- Inert: a ~ ty
1102 -- Work item: a ~ ty
1103 do { setEvBindIfWanted ev $
1104 EvCoercion (tcDowngradeRole (eqRelRole eq_rel)
1105 (ctEvRole ev_i)
1106 (ctEvCoercion ev_i))
1107
1108 ; stopWith ev "Solved from inert" }
1109
1110 | Just tv_rhs <- getTyVar_maybe rhs
1111 , (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i }
1112 <- findTyEqs inerts tv_rhs
1113 , ev_i `eqCanDischarge` ev
1114 , rhs_i `tcEqType` mkTyVarTy tv ]
1115 = -- Inert: a ~ b
1116 -- Work item: b ~ a
1117 do { setEvBindIfWanted ev $
1118 EvCoercion (mkTcSymCo $
1119 tcDowngradeRole (eqRelRole eq_rel)
1120 (ctEvRole ev_i)
1121 (ctEvCoercion ev_i))
1122
1123 ; stopWith ev "Solved from inert (r)" }
1124
1125 | ReprEq <- eq_rel -- We never solve representational
1126 = unsolved_inert -- equalities by unification
1127
1128 | isGiven ev -- See Note [Touchables and givens]
1129 = unsolved_inert
1130
1131 | otherwise
1132 = do { tclvl <- getTcLevel
1133 ; if canSolveByUnification tclvl tv rhs
1134 then do { solveByUnification ev tv rhs
1135 ; n_kicked <- kickOutAfterUnification tv
1136 ; return (Stop ev (text "Solved by unification" <+> ppr_kicked n_kicked)) }
1137
1138 else unsolved_inert }
1139
1140 where
1141 unsolved_inert
1142 = do { traceTcS "Can't solve tyvar equality"
1143 (vcat [ text "LHS:" <+> ppr tv <+> dcolon <+> ppr (tyVarKind tv)
1144 , ppWhen (isMetaTyVar tv) $
1145 nest 4 (text "TcLevel of" <+> ppr tv
1146 <+> text "is" <+> ppr (metaTyVarTcLevel tv))
1147 , text "RHS:" <+> ppr rhs <+> dcolon <+> ppr (typeKind rhs) ])
1148 ; addInertEq workItem
1149 ; return (Stop ev (text "Kept as inert")) }
1150
1151 interactTyVarEq _ wi = pprPanic "interactTyVarEq" (ppr wi)
1152
1153 solveByUnification :: CtEvidence -> TcTyVar -> Xi -> TcS ()
1154 -- Solve with the identity coercion
1155 -- Precondition: kind(xi) equals kind(tv)
1156 -- Precondition: CtEvidence is Wanted or Derived
1157 -- Precondition: CtEvidence is nominal
1158 -- Returns: workItem where
1159 -- workItem = the new Given constraint
1160 --
1161 -- NB: No need for an occurs check here, because solveByUnification always
1162 -- arises from a CTyEqCan, a *canonical* constraint. Its invariants
1163 -- say that in (a ~ xi), the type variable a does not appear in xi.
1164 -- See TcRnTypes.Ct invariants.
1165 --
1166 -- Post: tv is unified (by side effect) with xi;
1167 -- we often write tv := xi
1168 solveByUnification wd tv xi
1169 = do { let tv_ty = mkTyVarTy tv
1170 ; traceTcS "Sneaky unification:" $
1171 vcat [text "Unifies:" <+> ppr tv <+> text ":=" <+> ppr xi,
1172 text "Coercion:" <+> pprEq tv_ty xi,
1173 text "Left Kind is:" <+> ppr (typeKind tv_ty),
1174 text "Right Kind is:" <+> ppr (typeKind xi) ]
1175
1176 ; unifyTyVar tv xi
1177 ; setEvBindIfWanted wd (EvCoercion (mkTcNomReflCo xi)) }
1178
1179 ppr_kicked :: Int -> SDoc
1180 ppr_kicked 0 = empty
1181 ppr_kicked n = parens (int n <+> text "kicked out")
1182
1183 {- Note [Avoid double unifications]
1184 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1185 The spontaneous solver has to return a given which mentions the unified unification
1186 variable *on the left* of the equality. Here is what happens if not:
1187 Original wanted: (a ~ alpha), (alpha ~ Int)
1188 We spontaneously solve the first wanted, without changing the order!
1189 given : a ~ alpha [having unified alpha := a]
1190 Now the second wanted comes along, but he cannot rewrite the given, so we simply continue.
1191 At the end we spontaneously solve that guy, *reunifying* [alpha := Int]
1192
1193 We avoid this problem by orienting the resulting given so that the unification
1194 variable is on the left. [Note that alternatively we could attempt to
1195 enforce this at canonicalization]
1196
1197 See also Note [No touchables as FunEq RHS] in TcSMonad; avoiding
1198 double unifications is the main reason we disallow touchable
1199 unification variables as RHS of type family equations: F xis ~ alpha.
1200
1201
1202 ************************************************************************
1203 * *
1204 * Functional dependencies, instantiation of equations
1205 * *
1206 ************************************************************************
1207
1208 When we spot an equality arising from a functional dependency,
1209 we now use that equality (a "wanted") to rewrite the work-item
1210 constraint right away. This avoids two dangers
1211
1212 Danger 1: If we send the original constraint on down the pipeline
1213 it may react with an instance declaration, and in delicate
1214 situations (when a Given overlaps with an instance) that
1215 may produce new insoluble goals: see Trac #4952
1216
1217 Danger 2: If we don't rewrite the constraint, it may re-react
1218 with the same thing later, and produce the same equality
1219 again --> termination worries.
1220
1221 To achieve this required some refactoring of FunDeps.hs (nicer
1222 now!).
1223 -}
1224
1225 emitFunDepDeriveds :: [FunDepEqn CtLoc] -> TcS ()
1226 emitFunDepDeriveds fd_eqns
1227 = mapM_ do_one_FDEqn fd_eqns
1228 where
1229 do_one_FDEqn (FDEqn { fd_qtvs = tvs, fd_eqs = eqs, fd_loc = loc })
1230 | null tvs -- Common shortcut
1231 = mapM_ (unifyDerived loc Nominal) eqs
1232 | otherwise
1233 = do { (subst, _) <- instFlexiTcS tvs -- Takes account of kind substitution
1234 ; mapM_ (do_one_eq loc subst) eqs }
1235
1236 do_one_eq loc subst (Pair ty1 ty2)
1237 = unifyDerived loc Nominal $
1238 Pair (Type.substTyUnchecked subst ty1) (Type.substTyUnchecked subst ty2)
1239
1240 {-
1241 **********************************************************************
1242 * *
1243 The top-reaction Stage
1244 * *
1245 **********************************************************************
1246 -}
1247
1248 topReactionsStage :: WorkItem -> TcS (StopOrContinue Ct)
1249 topReactionsStage wi
1250 = do { tir <- doTopReact wi
1251 ; case tir of
1252 ContinueWith wi -> continueWith wi
1253 Stop ev s -> return (Stop ev (text "Top react:" <+> s)) }
1254
1255 doTopReact :: WorkItem -> TcS (StopOrContinue Ct)
1256 -- The work item does not react with the inert set, so try interaction with top-level
1257 -- instances. Note:
1258 --
1259 -- (a) The place to add superclasses in not here in doTopReact stage.
1260 -- Instead superclasses are added in the worklist as part of the
1261 -- canonicalization process. See Note [Adding superclasses].
1262
1263 doTopReact work_item
1264 = do { traceTcS "doTopReact" (ppr work_item)
1265 ; case work_item of
1266 CDictCan {} -> do { inerts <- getTcSInerts
1267 ; doTopReactDict inerts work_item }
1268 CFunEqCan {} -> doTopReactFunEq work_item
1269 _ -> -- Any other work item does not react with any top-level equations
1270 continueWith work_item }
1271
1272 --------------------
1273 doTopReactDict :: InertSet -> Ct -> TcS (StopOrContinue Ct)
1274 -- Try to use type-class instance declarations to simplify the constraint
1275 doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls
1276 , cc_tyargs = xis })
1277 | isGiven fl -- Never use instances for Given constraints
1278 = do { try_fundep_improvement
1279 ; continueWith work_item }
1280
1281 | Just ev <- lookupSolvedDict inerts cls xis -- Cached
1282 = do { setEvBindIfWanted fl (ctEvTerm ev)
1283 ; stopWith fl "Dict/Top (cached)" }
1284
1285 | isDerived fl -- Use type-class instances for Deriveds, in the hope
1286 -- of generating some improvements
1287 -- C.f. Example 3 of Note [The improvement story]
1288 -- It's easy because no evidence is involved
1289 = do { dflags <- getDynFlags
1290 ; lkup_inst_res <- matchClassInst dflags inerts cls xis dict_loc
1291 ; case lkup_inst_res of
1292 GenInst { lir_new_theta = preds
1293 , lir_safe_over = s } ->
1294 do { emitNewDeriveds dict_loc preds
1295 ; unless s $ insertSafeOverlapFailureTcS work_item
1296 ; stopWith fl "Dict/Top (solved)" }
1297
1298 NoInstance ->
1299 do { -- If there is no instance, try improvement
1300 try_fundep_improvement
1301 ; continueWith work_item } }
1302
1303 | otherwise -- Wanted, but not cached
1304 = do { dflags <- getDynFlags
1305 ; lkup_inst_res <- matchClassInst dflags inerts cls xis dict_loc
1306 ; case lkup_inst_res of
1307 GenInst { lir_new_theta = theta
1308 , lir_mk_ev = mk_ev
1309 , lir_safe_over = s } ->
1310 do { addSolvedDict fl cls xis
1311 ; unless s $ insertSafeOverlapFailureTcS work_item
1312 ; solve_from_instance theta mk_ev }
1313 NoInstance ->
1314 do { try_fundep_improvement
1315 ; continueWith work_item } }
1316 where
1317 dict_pred = mkClassPred cls xis
1318 dict_loc = ctEvLoc fl
1319 dict_origin = ctLocOrigin dict_loc
1320 deeper_loc = zap_origin (bumpCtLocDepth dict_loc)
1321
1322 zap_origin loc -- After applying an instance we can set ScOrigin to
1323 -- infinity, so that prohibitedSuperClassSolve never fires
1324 | ScOrigin {} <- dict_origin
1325 = setCtLocOrigin loc (ScOrigin infinity)
1326 | otherwise
1327 = loc
1328
1329 solve_from_instance :: [TcPredType]
1330 -> ([EvTerm] -> EvTerm) -> TcS (StopOrContinue Ct)
1331 -- Precondition: evidence term matches the predicate workItem
1332 solve_from_instance theta mk_ev
1333 | null theta
1334 = do { traceTcS "doTopReact/found nullary instance for" $ ppr fl
1335 ; setWantedEvBind (ctEvId fl) (mk_ev [])
1336 ; stopWith fl "Dict/Top (solved, no new work)" }
1337 | otherwise
1338 = do { checkReductionDepth deeper_loc dict_pred
1339 ; traceTcS "doTopReact/found non-nullary instance for" $ ppr fl
1340 ; evc_vars <- mapM (newWanted deeper_loc) theta
1341 ; setWantedEvBind (ctEvId fl) (mk_ev (map getEvTerm evc_vars))
1342 ; emitWorkNC (freshGoals evc_vars)
1343 ; stopWith fl "Dict/Top (solved, more work)" }
1344
1345 -- We didn't solve it; so try functional dependencies with
1346 -- the instance environment, and return
1347 -- See also Note [Weird fundeps]
1348 try_fundep_improvement
1349 = do { traceTcS "try_fundeps" (ppr work_item)
1350 ; instEnvs <- getInstEnvs
1351 ; emitFunDepDeriveds $
1352 improveFromInstEnv instEnvs mk_ct_loc dict_pred }
1353
1354 mk_ct_loc :: PredType -- From instance decl
1355 -> SrcSpan -- also from instance deol
1356 -> CtLoc
1357 mk_ct_loc inst_pred inst_loc
1358 = dict_loc { ctl_origin = FunDepOrigin2 dict_pred dict_origin
1359 inst_pred inst_loc }
1360
1361 doTopReactDict _ w = pprPanic "doTopReactDict" (ppr w)
1362
1363 --------------------
1364 doTopReactFunEq :: Ct -> TcS (StopOrContinue Ct)
1365 doTopReactFunEq work_item@(CFunEqCan { cc_ev = old_ev, cc_fun = fam_tc
1366 , cc_tyargs = args, cc_fsk = fsk })
1367 = do { match_res <- matchFam fam_tc args
1368 -- Look up in top-level instances, or built-in axiom
1369 -- See Note [MATCHING-SYNONYMS]
1370 ; case match_res of
1371 Nothing -> do { improveTopFunEqs (ctEvLoc old_ev) fam_tc args fsk
1372 ; continueWith work_item }
1373 Just (ax_co, rhs_ty)
1374 -> reduce_top_fun_eq old_ev fsk ax_co rhs_ty }
1375
1376 doTopReactFunEq w = pprPanic "doTopReactFunEq" (ppr w)
1377
1378 reduce_top_fun_eq :: CtEvidence -> TcTyVar -> TcCoercion -> TcType
1379 -> TcS (StopOrContinue Ct)
1380 -- Found an applicable top-level axiom: use it to reduce
1381 reduce_top_fun_eq old_ev fsk ax_co rhs_ty
1382 | Just (tc, tc_args) <- tcSplitTyConApp_maybe rhs_ty
1383 , isTypeFamilyTyCon tc
1384 , tc_args `lengthIs` tyConArity tc -- Short-cut
1385 = shortCutReduction old_ev fsk ax_co tc tc_args
1386 -- Try shortcut; see Note [Short cut for top-level reaction]
1387
1388 | isGiven old_ev -- Not shortcut
1389 = do { let final_co = mkTcSymCo (ctEvCoercion old_ev) `mkTcTransCo` ax_co
1390 -- final_co :: fsk ~ rhs_ty
1391 ; new_ev <- newGivenEvVar deeper_loc (mkPrimEqPred (mkTyVarTy fsk) rhs_ty,
1392 EvCoercion final_co)
1393 ; emitWorkNC [new_ev] -- Non-cannonical; that will mean we flatten rhs_ty
1394 ; stopWith old_ev "Fun/Top (given)" }
1395
1396 -- So old_ev is Wanted or Derived
1397 | not (fsk `elemVarSet` tyCoVarsOfType rhs_ty)
1398 = do { dischargeFmv old_ev fsk ax_co rhs_ty
1399 ; traceTcS "doTopReactFunEq" $
1400 vcat [ text "old_ev:" <+> ppr old_ev
1401 , nest 2 (text ":=") <+> ppr ax_co ]
1402 ; stopWith old_ev "Fun/Top (wanted)" }
1403
1404 | otherwise -- We must not assign ufsk := ...ufsk...!
1405 = do { alpha_ty <- newFlexiTcSTy (tyVarKind fsk)
1406 ; new_ev <- case old_ev of
1407 CtWanted {} -> do { (ev, _) <- newWantedEq loc Nominal alpha_ty rhs_ty
1408 ; updWorkListTcS $
1409 extendWorkListEq (mkNonCanonical ev)
1410 ; return ev }
1411 CtDerived {} -> do { ev <- newDerivedNC loc pred
1412 ; updWorkListTcS (extendWorkListDerived loc ev)
1413 ; return ev }
1414 where pred = mkPrimEqPred alpha_ty rhs_ty
1415 _ -> pprPanic "reduce_top_fun_eq" (ppr old_ev)
1416
1417 -- By emitting this as non-canonical, we deal with all
1418 -- flattening, occurs-check, and ufsk := ufsk issues
1419 ; let final_co = ax_co `mkTcTransCo` mkTcSymCo (ctEvCoercion new_ev)
1420 -- ax_co :: fam_tc args ~ rhs_ty
1421 -- ev :: alpha ~ rhs_ty
1422 -- ufsk := alpha
1423 -- final_co :: fam_tc args ~ alpha
1424 ; dischargeFmv old_ev fsk final_co alpha_ty
1425 ; traceTcS "doTopReactFunEq (occurs)" $
1426 vcat [ text "old_ev:" <+> ppr old_ev
1427 , nest 2 (text ":=") <+>
1428 if isDerived old_ev then text "(derived)"
1429 else ppr final_co
1430 , text "new_ev:" <+> ppr new_ev ]
1431 ; stopWith old_ev "Fun/Top (wanted)" }
1432 where
1433 loc = ctEvLoc old_ev
1434 deeper_loc = bumpCtLocDepth loc
1435
1436 improveTopFunEqs :: CtLoc -> TyCon -> [TcType] -> TcTyVar -> TcS ()
1437 improveTopFunEqs loc fam_tc args fsk
1438 = do { model <- getInertModel
1439 ; fam_envs <- getFamInstEnvs
1440 ; eqns <- improve_top_fun_eqs fam_envs fam_tc args
1441 (lookupFlattenTyVar model fsk)
1442 ; mapM_ (unifyDerived loc Nominal) eqns }
1443
1444 improve_top_fun_eqs :: FamInstEnvs
1445 -> TyCon -> [TcType] -> TcType
1446 -> TcS [Eqn]
1447 improve_top_fun_eqs fam_envs fam_tc args rhs_ty
1448 | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc
1449 = return (sfInteractTop ops args rhs_ty)
1450
1451 -- see Note [Type inference for type families with injectivity]
1452 | isOpenTypeFamilyTyCon fam_tc
1453 , Injective injective_args <- familyTyConInjectivityInfo fam_tc
1454 = -- it is possible to have several compatible equations in an open type
1455 -- family but we only want to derive equalities from one such equation.
1456 concatMapM (injImproveEqns injective_args) (take 1 $
1457 buildImprovementData (lookupFamInstEnvByTyCon fam_envs fam_tc)
1458 fi_tys fi_rhs (const Nothing))
1459
1460 | Just ax <- isClosedSynFamilyTyConWithAxiom_maybe fam_tc
1461 , Injective injective_args <- familyTyConInjectivityInfo fam_tc
1462 = concatMapM (injImproveEqns injective_args) $
1463 buildImprovementData (fromBranches (co_ax_branches ax))
1464 cab_lhs cab_rhs Just
1465
1466 | otherwise
1467 = return []
1468 where
1469 buildImprovementData
1470 :: [a] -- axioms for a TF (FamInst or CoAxBranch)
1471 -> (a -> [Type]) -- get LHS of an axiom
1472 -> (a -> Type) -- get RHS of an axiom
1473 -> (a -> Maybe CoAxBranch) -- Just => apartness check required
1474 -> [( [Type], TCvSubst, [TyVar], Maybe CoAxBranch )]
1475 -- Result:
1476 -- ( [arguments of a matching axiom]
1477 -- , RHS-unifying substitution
1478 -- , axiom variables without substitution
1479 -- , Maybe matching axiom [Nothing - open TF, Just - closed TF ] )
1480 buildImprovementData axioms axiomLHS axiomRHS wrap =
1481 [ (ax_args, subst, unsubstTvs, wrap axiom)
1482 | axiom <- axioms
1483 , let ax_args = axiomLHS axiom
1484 , let ax_rhs = axiomRHS axiom
1485 , Just subst <- [tcUnifyTyWithTFs False ax_rhs rhs_ty]
1486 , let tvs = tyCoVarsOfTypesList ax_args
1487 notInSubst tv = not (tv `elemVarEnv` getTvSubstEnv subst)
1488 unsubstTvs = filter (notInSubst <&&> isTyVar) tvs ]
1489
1490 injImproveEqns :: [Bool]
1491 -> ([Type], TCvSubst, [TyCoVar], Maybe CoAxBranch)
1492 -> TcS [Eqn]
1493 injImproveEqns inj_args (ax_args, theta, unsubstTvs, cabr) = do
1494 (theta', _) <- instFlexiTcS unsubstTvs
1495 -- The use of deterministically ordered list for `unsubstTvs`
1496 -- is not strictly necessary here, we only use the substitution
1497 -- part of the result of instFlexiTcS. If we used the second
1498 -- part of the tuple, which is the range of the substitution then
1499 -- the order could be important.
1500 let subst = theta `unionTCvSubst` theta'
1501 return [ Pair arg (substTyUnchecked subst ax_arg)
1502 | case cabr of
1503 Just cabr' -> apartnessCheck (substTys subst ax_args) cabr'
1504 _ -> True
1505 , (arg, ax_arg, True) <- zip3 args ax_args inj_args ]
1506
1507
1508 shortCutReduction :: CtEvidence -> TcTyVar -> TcCoercion
1509 -> TyCon -> [TcType] -> TcS (StopOrContinue Ct)
1510 -- See Note [Top-level reductions for type functions]
1511 shortCutReduction old_ev fsk ax_co fam_tc tc_args
1512 = ASSERT( ctEvEqRel old_ev == NomEq)
1513 do { (xis, cos) <- flattenManyNom old_ev tc_args
1514 -- ax_co :: F args ~ G tc_args
1515 -- cos :: xis ~ tc_args
1516 -- old_ev :: F args ~ fsk
1517 -- G cos ; sym ax_co ; old_ev :: G xis ~ fsk
1518
1519 ; new_ev <- case ctEvFlavour old_ev of
1520 Given -> newGivenEvVar deeper_loc
1521 ( mkPrimEqPred (mkTyConApp fam_tc xis) (mkTyVarTy fsk)
1522 , EvCoercion (mkTcTyConAppCo Nominal fam_tc cos
1523 `mkTcTransCo` mkTcSymCo ax_co
1524 `mkTcTransCo` ctEvCoercion old_ev) )
1525
1526 Derived -> newDerivedNC deeper_loc $
1527 mkPrimEqPred (mkTyConApp fam_tc xis)
1528 (mkTyVarTy fsk)
1529
1530 Wanted ->
1531 do { (new_ev, new_co) <- newWantedEq deeper_loc Nominal
1532 (mkTyConApp fam_tc xis) (mkTyVarTy fsk)
1533 ; setWantedEq (ctev_dest old_ev) $
1534 ax_co `mkTcTransCo` mkTcSymCo (mkTcTyConAppCo Nominal
1535 fam_tc cos)
1536 `mkTcTransCo` new_co
1537 ; return new_ev }
1538
1539 ; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc
1540 , cc_tyargs = xis, cc_fsk = fsk }
1541 ; updWorkListTcS (extendWorkListFunEq new_ct)
1542 ; stopWith old_ev "Fun/Top (shortcut)" }
1543 where
1544 deeper_loc = bumpCtLocDepth (ctEvLoc old_ev)
1545
1546 dischargeFmv :: CtEvidence -> TcTyVar -> TcCoercion -> TcType -> TcS ()
1547 -- (dischargeFmv x fmv co ty)
1548 -- [W] ev :: F tys ~ fmv
1549 -- co :: F tys ~ xi
1550 -- Precondition: fmv is not filled, and fuv `notElem` xi
1551 --
1552 -- Then set fmv := xi,
1553 -- set ev := co
1554 -- kick out any inert things that are now rewritable
1555 --
1556 -- Does not evaluate 'co' if 'ev' is Derived
1557 dischargeFmv ev fmv co xi
1558 = ASSERT2( not (fmv `elemVarSet` tyCoVarsOfType xi), ppr ev $$ ppr fmv $$ ppr xi )
1559 do { setEvBindIfWanted ev (EvCoercion co)
1560 ; unflattenFmv fmv xi
1561 ; n_kicked <- kickOutAfterUnification fmv
1562 ; traceTcS "dischargeFmv" (ppr fmv <+> equals <+> ppr xi $$ ppr_kicked n_kicked) }
1563
1564 {- Note [Top-level reductions for type functions]
1565 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1566 c.f. Note [The flattening story] in TcFlatten
1567
1568 Suppose we have a CFunEqCan F tys ~ fmv/fsk, and a matching axiom.
1569 Here is what we do, in four cases:
1570
1571 * Wanteds: general firing rule
1572 (work item) [W] x : F tys ~ fmv
1573 instantiate axiom: ax_co : F tys ~ rhs
1574
1575 Then:
1576 Discharge fmv := alpha
1577 Discharge x := ax_co ; sym x2
1578 New wanted [W] x2 : alpha ~ rhs (Non-canonical)
1579 This is *the* way that fmv's get unified; even though they are
1580 "untouchable".
1581
1582 NB: it can be the case that fmv appears in the (instantiated) rhs.
1583 In that case the new Non-canonical wanted will be loopy, but that's
1584 ok. But it's good reason NOT to claim that it is canonical!
1585
1586 * Wanteds: short cut firing rule
1587 Applies when the RHS of the axiom is another type-function application
1588 (work item) [W] x : F tys ~ fmv
1589 instantiate axiom: ax_co : F tys ~ G rhs_tys
1590
1591 It would be a waste to create yet another fmv for (G rhs_tys).
1592 Instead (shortCutReduction):
1593 - Flatten rhs_tys (cos : rhs_tys ~ rhs_xis)
1594 - Add G rhs_xis ~ fmv to flat cache (note: the same old fmv)
1595 - New canonical wanted [W] x2 : G rhs_xis ~ fmv (CFunEqCan)
1596 - Discharge x := ax_co ; G cos ; x2
1597
1598 * Givens: general firing rule
1599 (work item) [G] g : F tys ~ fsk
1600 instantiate axiom: ax_co : F tys ~ rhs
1601
1602 Now add non-canonical given (since rhs is not flat)
1603 [G] (sym g ; ax_co) : fsk ~ rhs (Non-canonical)
1604
1605 * Givens: short cut firing rule
1606 Applies when the RHS of the axiom is another type-function application
1607 (work item) [G] g : F tys ~ fsk
1608 instantiate axiom: ax_co : F tys ~ G rhs_tys
1609
1610 It would be a waste to create yet another fsk for (G rhs_tys).
1611 Instead (shortCutReduction):
1612 - Flatten rhs_tys: flat_cos : tys ~ flat_tys
1613 - Add new Canonical given
1614 [G] (sym (G flat_cos) ; co ; g) : G flat_tys ~ fsk (CFunEqCan)
1615
1616 Note [Cached solved FunEqs]
1617 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1618 When trying to solve, say (FunExpensive big-type ~ ty), it's important
1619 to see if we have reduced (FunExpensive big-type) before, lest we
1620 simply repeat it. Hence the lookup in inert_solved_funeqs. Moreover
1621 we must use `funEqCanDischarge` because both uses might (say) be Wanteds,
1622 and we *still* want to save the re-computation.
1623
1624 Note [MATCHING-SYNONYMS]
1625 ~~~~~~~~~~~~~~~~~~~~~~~~
1626 When trying to match a dictionary (D tau) to a top-level instance, or a
1627 type family equation (F taus_1 ~ tau_2) to a top-level family instance,
1628 we do *not* need to expand type synonyms because the matcher will do that for us.
1629
1630
1631 Note [RHS-FAMILY-SYNONYMS]
1632 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1633 The RHS of a family instance is represented as yet another constructor which is
1634 like a type synonym for the real RHS the programmer declared. Eg:
1635 type instance F (a,a) = [a]
1636 Becomes:
1637 :R32 a = [a] -- internal type synonym introduced
1638 F (a,a) ~ :R32 a -- instance
1639
1640 When we react a family instance with a type family equation in the work list
1641 we keep the synonym-using RHS without expansion.
1642
1643 Note [FunDep and implicit parameter reactions]
1644 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1645 Currently, our story of interacting two dictionaries (or a dictionary
1646 and top-level instances) for functional dependencies, and implicit
1647 paramters, is that we simply produce new Derived equalities. So for example
1648
1649 class D a b | a -> b where ...
1650 Inert:
1651 d1 :g D Int Bool
1652 WorkItem:
1653 d2 :w D Int alpha
1654
1655 We generate the extra work item
1656 cv :d alpha ~ Bool
1657 where 'cv' is currently unused. However, this new item can perhaps be
1658 spontaneously solved to become given and react with d2,
1659 discharging it in favour of a new constraint d2' thus:
1660 d2' :w D Int Bool
1661 d2 := d2' |> D Int cv
1662 Now d2' can be discharged from d1
1663
1664 We could be more aggressive and try to *immediately* solve the dictionary
1665 using those extra equalities, but that requires those equalities to carry
1666 evidence and derived do not carry evidence.
1667
1668 If that were the case with the same inert set and work item we might dischard
1669 d2 directly:
1670
1671 cv :w alpha ~ Bool
1672 d2 := d1 |> D Int cv
1673
1674 But in general it's a bit painful to figure out the necessary coercion,
1675 so we just take the first approach. Here is a better example. Consider:
1676 class C a b c | a -> b
1677 And:
1678 [Given] d1 : C T Int Char
1679 [Wanted] d2 : C T beta Int
1680 In this case, it's *not even possible* to solve the wanted immediately.
1681 So we should simply output the functional dependency and add this guy
1682 [but NOT its superclasses] back in the worklist. Even worse:
1683 [Given] d1 : C T Int beta
1684 [Wanted] d2: C T beta Int
1685 Then it is solvable, but its very hard to detect this on the spot.
1686
1687 It's exactly the same with implicit parameters, except that the
1688 "aggressive" approach would be much easier to implement.
1689
1690
1691 Note [Weird fundeps]
1692 ~~~~~~~~~~~~~~~~~~~~
1693 Consider class Het a b | a -> b where
1694 het :: m (f c) -> a -> m b
1695
1696 class GHet (a :: * -> *) (b :: * -> *) | a -> b
1697 instance GHet (K a) (K [a])
1698 instance Het a b => GHet (K a) (K b)
1699
1700 The two instances don't actually conflict on their fundeps,
1701 although it's pretty strange. So they are both accepted. Now
1702 try [W] GHet (K Int) (K Bool)
1703 This triggers fundeps from both instance decls;
1704 [D] K Bool ~ K [a]
1705 [D] K Bool ~ K beta
1706 And there's a risk of complaining about Bool ~ [a]. But in fact
1707 the Wanted matches the second instance, so we never get as far
1708 as the fundeps.
1709
1710 Trac #7875 is a case in point.
1711
1712 Note [Overriding implicit parameters]
1713 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1714 Consider
1715 f :: (?x::a) -> Bool -> a
1716
1717 g v = let ?x::Int = 3
1718 in (f v, let ?x::Bool = True in f v)
1719
1720 This should probably be well typed, with
1721 g :: Bool -> (Int, Bool)
1722
1723 So the inner binding for ?x::Bool *overrides* the outer one.
1724 Hence a work-item Given overrides an inert-item Given.
1725 -}
1726
1727 {- *******************************************************************
1728 * *
1729 Class lookup
1730 * *
1731 **********************************************************************-}
1732
1733 -- | Indicates if Instance met the Safe Haskell overlapping instances safety
1734 -- check.
1735 --
1736 -- See Note [Safe Haskell Overlapping Instances] in TcSimplify
1737 -- See Note [Safe Haskell Overlapping Instances Implementation] in TcSimplify
1738 type SafeOverlapping = Bool
1739
1740 data LookupInstResult
1741 = NoInstance
1742 | GenInst { lir_new_theta :: [TcPredType]
1743 , lir_mk_ev :: [EvTerm] -> EvTerm
1744 , lir_safe_over :: SafeOverlapping }
1745
1746 instance Outputable LookupInstResult where
1747 ppr NoInstance = text "NoInstance"
1748 ppr (GenInst { lir_new_theta = ev
1749 , lir_safe_over = s })
1750 = text "GenInst" <+> vcat [ppr ev, ss]
1751 where ss = text $ if s then "[safe]" else "[unsafe]"
1752
1753
1754 matchClassInst :: DynFlags -> InertSet -> Class -> [Type] -> CtLoc -> TcS LookupInstResult
1755 matchClassInst dflags inerts clas tys loc
1756 -- First check whether there is an in-scope Given that could
1757 -- match this constraint. In that case, do not use top-level
1758 -- instances. See Note [Instance and Given overlap]
1759 | not (xopt LangExt.IncoherentInstances dflags)
1760 , not (naturallyCoherentClass clas)
1761 , let matchable_givens = matchableGivens loc pred inerts
1762 , not (isEmptyBag matchable_givens)
1763 = do { traceTcS "Delaying instance application" $
1764 vcat [ text "Work item=" <+> pprClassPred clas tys
1765 , text "Potential matching givens:" <+> ppr matchable_givens ]
1766 ; return NoInstance }
1767 where
1768 pred = mkClassPred clas tys
1769
1770 matchClassInst dflags _ clas tys loc
1771 = do { traceTcS "matchClassInst" $ vcat [ text "pred =" <+> ppr (mkClassPred clas tys) ]
1772 ; res <- match_class_inst dflags clas tys loc
1773 ; traceTcS "matchClassInst result" $ ppr res
1774 ; return res }
1775
1776 match_class_inst :: DynFlags -> Class -> [Type] -> CtLoc -> TcS LookupInstResult
1777 match_class_inst dflags clas tys loc
1778 | cls_name == knownNatClassName = matchKnownNat clas tys
1779 | cls_name == knownSymbolClassName = matchKnownSymbol clas tys
1780 | isCTupleClass clas = matchCTuple clas tys
1781 | cls_name == typeableClassName = matchTypeable clas tys
1782 | clas `hasKey` heqTyConKey = matchLiftedEquality tys
1783 | clas `hasKey` coercibleTyConKey = matchLiftedCoercible tys
1784 | otherwise = matchInstEnv dflags clas tys loc
1785 where
1786 cls_name = className clas
1787
1788 {- Note [Instance and Given overlap]
1789 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1790 Example, from the OutsideIn(X) paper:
1791 instance P x => Q [x]
1792 instance (x ~ y) => R y [x]
1793
1794 wob :: forall a b. (Q [b], R b a) => a -> Int
1795
1796 g :: forall a. Q [a] => [a] -> Int
1797 g x = wob x
1798
1799 From 'g' we get the impliation constraint:
1800 forall a. Q [a] => (Q [beta], R beta [a])
1801 If we react (Q [beta]) with its top-level axiom, we end up with a
1802 (P beta), which we have no way of discharging. On the other hand,
1803 if we react R beta [a] with the top-level we get (beta ~ a), which
1804 is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
1805 now solvable by the given Q [a].
1806
1807 The partial solution is that:
1808 In matchClassInst (and thus in topReact), we return a matching
1809 instance only when there is no Given in the inerts which is
1810 unifiable to this particular dictionary.
1811
1812 We treat any meta-tyvar as "unifiable" for this purpose,
1813 *including* untouchable ones. But not skolems like 'a' in
1814 the implication constraint above.
1815
1816 The end effect is that, much as we do for overlapping instances, we
1817 delay choosing a class instance if there is a possibility of another
1818 instance OR a given to match our constraint later on. This fixes
1819 Trac #4981 and #5002.
1820
1821 Other notes:
1822
1823 * The check is done *first*, so that it also covers classes
1824 with built-in instance solving, such as
1825 - constraint tuples
1826 - natural numbers
1827 - Typeable
1828
1829 * The given-overlap problem is arguably not easy to appear in practice
1830 due to our aggressive prioritization of equality solving over other
1831 constraints, but it is possible. I've added a test case in
1832 typecheck/should-compile/GivenOverlapping.hs
1833
1834 * Another "live" example is Trac #10195; another is #10177.
1835
1836 * We ignore the overlap problem if -XIncoherentInstances is in force:
1837 see Trac #6002 for a worked-out example where this makes a
1838 difference.
1839
1840 * Moreover notice that our goals here are different than the goals of
1841 the top-level overlapping checks. There we are interested in
1842 validating the following principle:
1843
1844 If we inline a function f at a site where the same global
1845 instance environment is available as the instance environment at
1846 the definition site of f then we should get the same behaviour.
1847
1848 But for the Given Overlap check our goal is just related to completeness of
1849 constraint solving.
1850
1851 * The solution is only a partial one. Consider the above example with
1852 g :: forall a. Q [a] => [a] -> Int
1853 g x = let v = wob x
1854 in v
1855 and suppose we have -XNoMonoLocalBinds, so that we attempt to find the most
1856 general type for 'v'. When generalising v's type we'll simplify its
1857 Q [alpha] constraint, but we don't have Q [a] in the 'givens', so we
1858 will use the instance declaration after all. Trac #11948 was a case in point
1859
1860 All of this is disgustingly delicate, so to discourage people from writing
1861 simplifiable class givens, we warn about signatures that contain them;#
1862 see TcValidity Note [Simplifiable given constraints].
1863 -}
1864
1865
1866 {- *******************************************************************
1867 * *
1868 Class lookup in the instance environment
1869 * *
1870 **********************************************************************-}
1871
1872 matchInstEnv :: DynFlags -> Class -> [Type] -> CtLoc -> TcS LookupInstResult
1873 matchInstEnv dflags clas tys loc
1874 = do { instEnvs <- getInstEnvs
1875 ; let safeOverlapCheck = safeHaskell dflags `elem` [Sf_Safe, Sf_Trustworthy]
1876 (matches, unify, unsafeOverlaps) = lookupInstEnv True instEnvs clas tys
1877 safeHaskFail = safeOverlapCheck && not (null unsafeOverlaps)
1878 ; case (matches, unify, safeHaskFail) of
1879
1880 -- Nothing matches
1881 ([], _, _)
1882 -> do { traceTcS "matchClass not matching" $
1883 vcat [ text "dict" <+> ppr pred ]
1884 ; return NoInstance }
1885
1886 -- A single match (& no safe haskell failure)
1887 ([(ispec, inst_tys)], [], False)
1888 -> do { let dfun_id = instanceDFunId ispec
1889 ; traceTcS "matchClass success" $
1890 vcat [text "dict" <+> ppr pred,
1891 text "witness" <+> ppr dfun_id
1892 <+> ppr (idType dfun_id) ]
1893 -- Record that this dfun is needed
1894 ; match_one (null unsafeOverlaps) dfun_id inst_tys }
1895
1896 -- More than one matches (or Safe Haskell fail!). Defer any
1897 -- reactions of a multitude until we learn more about the reagent
1898 (matches, _, _)
1899 -> do { traceTcS "matchClass multiple matches, deferring choice" $
1900 vcat [text "dict" <+> ppr pred,
1901 text "matches" <+> ppr matches]
1902 ; return NoInstance } }
1903 where
1904 pred = mkClassPred clas tys
1905
1906 match_one :: SafeOverlapping -> DFunId -> [DFunInstType] -> TcS LookupInstResult
1907 -- See Note [DFunInstType: instantiating types] in InstEnv
1908 match_one so dfun_id mb_inst_tys
1909 = do { checkWellStagedDFun pred dfun_id loc
1910 ; (tys, theta) <- instDFunType dfun_id mb_inst_tys
1911 ; return $ GenInst { lir_new_theta = theta
1912 , lir_mk_ev = EvDFunApp dfun_id tys
1913 , lir_safe_over = so } }
1914
1915
1916 {- ********************************************************************
1917 * *
1918 Class lookup for CTuples
1919 * *
1920 ***********************************************************************-}
1921
1922 matchCTuple :: Class -> [Type] -> TcS LookupInstResult
1923 matchCTuple clas tys -- (isCTupleClass clas) holds
1924 = return (GenInst { lir_new_theta = tys
1925 , lir_mk_ev = tuple_ev
1926 , lir_safe_over = True })
1927 -- The dfun *is* the data constructor!
1928 where
1929 data_con = tyConSingleDataCon (classTyCon clas)
1930 tuple_ev = EvDFunApp (dataConWrapId data_con) tys
1931
1932 {- ********************************************************************
1933 * *
1934 Class lookup for Literals
1935 * *
1936 ***********************************************************************-}
1937
1938 matchKnownNat :: Class -> [Type] -> TcS LookupInstResult
1939 matchKnownNat clas [ty] -- clas = KnownNat
1940 | Just n <- isNumLitTy ty = makeLitDict clas ty (EvNum n)
1941 matchKnownNat _ _ = return NoInstance
1942
1943 matchKnownSymbol :: Class -> [Type] -> TcS LookupInstResult
1944 matchKnownSymbol clas [ty] -- clas = KnownSymbol
1945 | Just n <- isStrLitTy ty = makeLitDict clas ty (EvStr n)
1946 matchKnownSymbol _ _ = return NoInstance
1947
1948
1949 makeLitDict :: Class -> Type -> EvLit -> TcS LookupInstResult
1950 -- makeLitDict adds a coercion that will convert the literal into a dictionary
1951 -- of the appropriate type. See Note [KnownNat & KnownSymbol and EvLit]
1952 -- in TcEvidence. The coercion happens in 2 steps:
1953 --
1954 -- Integer -> SNat n -- representation of literal to singleton
1955 -- SNat n -> KnownNat n -- singleton to dictionary
1956 --
1957 -- The process is mirrored for Symbols:
1958 -- String -> SSymbol n
1959 -- SSymbol n -> KnownSymbol n -}
1960 makeLitDict clas ty evLit
1961 | Just (_, co_dict) <- tcInstNewTyCon_maybe (classTyCon clas) [ty]
1962 -- co_dict :: KnownNat n ~ SNat n
1963 , [ meth ] <- classMethods clas
1964 , Just tcRep <- tyConAppTyCon_maybe -- SNat
1965 $ funResultTy -- SNat n
1966 $ dropForAlls -- KnownNat n => SNat n
1967 $ idType meth -- forall n. KnownNat n => SNat n
1968 , Just (_, co_rep) <- tcInstNewTyCon_maybe tcRep [ty]
1969 -- SNat n ~ Integer
1970 , let ev_tm = mkEvCast (EvLit evLit) (mkTcSymCo (mkTcTransCo co_dict co_rep))
1971 = return $ GenInst { lir_new_theta = []
1972 , lir_mk_ev = \_ -> ev_tm
1973 , lir_safe_over = True }
1974
1975 | otherwise
1976 = panicTcS (text "Unexpected evidence for" <+> ppr (className clas)
1977 $$ vcat (map (ppr . idType) (classMethods clas)))
1978
1979
1980 {- ********************************************************************
1981 * *
1982 Class lookup for Typeable
1983 * *
1984 ***********************************************************************-}
1985
1986 -- | Assumes that we've checked that this is the 'Typeable' class,
1987 -- and it was applied to the correct argument.
1988 matchTypeable :: Class -> [Type] -> TcS LookupInstResult
1989 matchTypeable clas [k,t] -- clas = Typeable
1990 -- For the first two cases, See Note [No Typeable for polytypes or qualified types]
1991 | isForAllTy k = return NoInstance -- Polytype
1992 | isJust (tcSplitPredFunTy_maybe t) = return NoInstance -- Qualified type
1993
1994 -- Now cases that do work
1995 | k `eqType` typeNatKind = doTyLit knownNatClassName t
1996 | k `eqType` typeSymbolKind = doTyLit knownSymbolClassName t
1997 | Just (tc, ks) <- splitTyConApp_maybe t -- See Note [Typeable (T a b c)]
1998 , onlyNamedBndrsApplied tc ks = doTyConApp clas t ks
1999 | Just (f,kt) <- splitAppTy_maybe t = doTyApp clas t f kt
2000
2001 matchTypeable _ _ = return NoInstance
2002
2003 doTyConApp :: Class -> Type -> [Kind] -> TcS LookupInstResult
2004 -- Representation for type constructor applied to some kinds
2005 doTyConApp clas ty args
2006 = return $ GenInst (map (mk_typeable_pred clas) args)
2007 (\tms -> EvTypeable ty $ EvTypeableTyCon tms)
2008 True
2009
2010 -- Representation for concrete kinds. We just use the kind itself,
2011 -- but first we must make sure that we've instantiated all kind-
2012 -- polymorphism, but no more.
2013 onlyNamedBndrsApplied :: TyCon -> [KindOrType] -> Bool
2014 onlyNamedBndrsApplied tc ks
2015 = all isNamedBinder used_bndrs &&
2016 not (any isNamedBinder leftover_bndrs)
2017 where
2018 bndrs = tyConBinders tc
2019 (used_bndrs, leftover_bndrs) = splitAtList ks bndrs
2020
2021 doTyApp :: Class -> Type -> Type -> KindOrType -> TcS LookupInstResult
2022 -- Representation for an application of a type to a type-or-kind.
2023 -- This may happen when the type expression starts with a type variable.
2024 -- Example (ignoring kind parameter):
2025 -- Typeable (f Int Char) -->
2026 -- (Typeable (f Int), Typeable Char) -->
2027 -- (Typeable f, Typeable Int, Typeable Char) --> (after some simp. steps)
2028 -- Typeable f
2029 doTyApp clas ty f tk
2030 | isForAllTy (typeKind f)
2031 = return NoInstance -- We can't solve until we know the ctr.
2032 | otherwise
2033 = return $ GenInst [mk_typeable_pred clas f, mk_typeable_pred clas tk]
2034 (\[t1,t2] -> EvTypeable ty $ EvTypeableTyApp t1 t2)
2035 True
2036
2037 -- Emit a `Typeable` constraint for the given type.
2038 mk_typeable_pred :: Class -> Type -> PredType
2039 mk_typeable_pred clas ty = mkClassPred clas [ typeKind ty, ty ]
2040
2041 -- Typeable is implied by KnownNat/KnownSymbol. In the case of a type literal
2042 -- we generate a sub-goal for the appropriate class. See #10348 for what
2043 -- happens when we fail to do this.
2044 doTyLit :: Name -> Type -> TcS LookupInstResult
2045 doTyLit kc t = do { kc_clas <- tcLookupClass kc
2046 ; let kc_pred = mkClassPred kc_clas [ t ]
2047 mk_ev [ev] = EvTypeable t $ EvTypeableTyLit ev
2048 mk_ev _ = panic "doTyLit"
2049 ; return (GenInst [kc_pred] mk_ev True) }
2050
2051 {- Note [Typeable (T a b c)]
2052 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2053 For type applications we always decompose using binary application,
2054 vai doTyApp, until we get to a *kind* instantiation. Exmaple
2055 Proxy :: forall k. k -> *
2056
2057 To solve Typeable (Proxy (* -> *) Maybe) we
2058 - First decompose with doTyApp,
2059 to get (Typeable (Proxy (* -> *))) and Typeable Maybe
2060 - Then sovle (Typeable (Proxy (* -> *))) with doTyConApp
2061
2062 If we attempt to short-cut by solving it all at once, via
2063 doTyCOnAPp
2064
2065
2066 Note [No Typeable for polytypes or qualified types]
2067 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2068 We do not support impredicative typeable, such as
2069 Typeable (forall a. a->a)
2070 Typeable (Eq a => a -> a)
2071 Typeable (() => Int)
2072 Typeable (((),()) => Int)
2073
2074 See Trac #9858. For forall's the case is clear: we simply don't have
2075 a TypeRep for them. For qualified but not polymorphic types, like
2076 (Eq a => a -> a), things are murkier. But:
2077
2078 * We don't need a TypeRep for these things. TypeReps are for
2079 monotypes only.
2080
2081 * Perhaps we could treat `=>` as another type constructor for `Typeable`
2082 purposes, and thus support things like `Eq Int => Int`, however,
2083 at the current state of affairs this would be an odd exception as
2084 no other class works with impredicative types.
2085 For now we leave it off, until we have a better story for impredicativity.
2086 -}
2087
2088 solveCallStack :: CtEvidence -> EvCallStack -> TcS ()
2089 solveCallStack ev ev_cs = do
2090 -- We're given ev_cs :: CallStack, but the evidence term should be a
2091 -- dictionary, so we have to coerce ev_cs to a dictionary for
2092 -- `IP ip CallStack`. See Note [Overview of implicit CallStacks]
2093 let ev_tm = mkEvCast (EvCallStack ev_cs) (wrapIP (ctEvPred ev))
2094 setWantedEvBind (ctEvId ev) ev_tm
2095
2096 {- ********************************************************************
2097 * *
2098 Class lookup for lifted equality
2099 * *
2100 ***********************************************************************-}
2101
2102 -- See also Note [The equality types story] in TysPrim
2103 matchLiftedEquality :: [Type] -> TcS LookupInstResult
2104 matchLiftedEquality args
2105 = return (GenInst { lir_new_theta = [ mkTyConApp eqPrimTyCon args ]
2106 , lir_mk_ev = EvDFunApp (dataConWrapId heqDataCon) args
2107 , lir_safe_over = True })
2108
2109 -- See also Note [The equality types story] in TysPrim
2110 matchLiftedCoercible :: [Type] -> TcS LookupInstResult
2111 matchLiftedCoercible args@[k, t1, t2]
2112 = return (GenInst { lir_new_theta = [ mkTyConApp eqReprPrimTyCon args' ]
2113 , lir_mk_ev = EvDFunApp (dataConWrapId coercibleDataCon)
2114 args
2115 , lir_safe_over = True })
2116 where
2117 args' = [k, k, t1, t2]
2118 matchLiftedCoercible args = pprPanic "matchLiftedCoercible" (ppr args)