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