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