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