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