New handling of overlapping inst in Safe Haskell
[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_safehask = safehask
1347 , inert_funeqs = funeqmap
1348 , inert_irreds = irreds
1349 , inert_insols = insols })
1350 = (kicked_out, inert_cans_in)
1351 where
1352 -- NB: Notice that don't rewrite
1353 -- inert_solved_dicts, and inert_solved_funeqs
1354 -- optimistically. But when we lookup we have to
1355 -- take the substitution into account
1356 inert_cans_in = IC { inert_eqs = tv_eqs_in
1357 , inert_dicts = dicts_in
1358 , inert_safehask = safehask
1359 , inert_funeqs = feqs_in
1360 , inert_irreds = irs_in
1361 , inert_insols = insols_in }
1362
1363 kicked_out = WL { wl_eqs = tv_eqs_out
1364 , wl_funeqs = feqs_out
1365 , wl_rest = bagToList (dicts_out `andCts` irs_out
1366 `andCts` insols_out)
1367 , wl_implics = emptyBag }
1368
1369 (tv_eqs_out, tv_eqs_in) = foldVarEnv kick_out_eqs ([], emptyVarEnv) tv_eqs
1370 (feqs_out, feqs_in) = partitionFunEqs kick_out_ct funeqmap
1371 (dicts_out, dicts_in) = partitionDicts kick_out_ct dictmap
1372 (irs_out, irs_in) = partitionBag kick_out_irred irreds
1373 (insols_out, insols_in) = partitionBag kick_out_ct insols
1374 -- Kick out even insolubles; see Note [Kick out insolubles]
1375
1376 can_rewrite :: CtEvidence -> Bool
1377 can_rewrite = ((new_flavour, new_eq_rel) `eqCanRewriteFR`) . ctEvFlavourRole
1378
1379 kick_out_ct :: Ct -> Bool
1380 kick_out_ct ct = kick_out_ctev (ctEvidence ct)
1381
1382 kick_out_ctev :: CtEvidence -> Bool
1383 kick_out_ctev ev = can_rewrite ev
1384 && new_tv `elemVarSet` tyVarsOfType (ctEvPred ev)
1385 -- See Note [Kicking out inert constraints]
1386
1387 kick_out_irred :: Ct -> Bool
1388 kick_out_irred ct = can_rewrite (cc_ev ct)
1389 && new_tv `elemVarSet` closeOverKinds (tyVarsOfCt ct)
1390 -- See Note [Kicking out Irreds]
1391
1392 kick_out_eqs :: EqualCtList -> ([Ct], TyVarEnv EqualCtList)
1393 -> ([Ct], TyVarEnv EqualCtList)
1394 kick_out_eqs eqs (acc_out, acc_in)
1395 = (eqs_out ++ acc_out, case eqs_in of
1396 [] -> acc_in
1397 (eq1:_) -> extendVarEnv acc_in (cc_tyvar eq1) eqs_in)
1398 where
1399 (eqs_in, eqs_out) = partition keep_eq eqs
1400
1401 -- implements criteria K1-K3 in Note [The inert equalities] in TcFlatten
1402 keep_eq (CTyEqCan { cc_tyvar = tv, cc_rhs = rhs_ty, cc_ev = ev
1403 , cc_eq_rel = eq_rel })
1404 | tv == new_tv
1405 = not (can_rewrite ev) -- (K1)
1406
1407 | otherwise
1408 = check_k2 && check_k3
1409 where
1410 check_k2 = not (ev `eqCanRewrite` ev)
1411 || not (can_rewrite ev)
1412 || not (new_tv `elemVarSet` tyVarsOfType rhs_ty)
1413
1414 check_k3
1415 | can_rewrite ev
1416 = case eq_rel of
1417 NomEq -> not (rhs_ty `eqType` mkTyVarTy new_tv)
1418 ReprEq -> not (isTyVarExposed new_tv rhs_ty)
1419
1420 | otherwise
1421 = True
1422
1423 keep_eq ct = pprPanic "keep_eq" (ppr ct)
1424
1425 {-
1426 Note [Kicking out inert constraints]
1427 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1428 Given a new (a -> ty) inert, we want to kick out an existing inert
1429 constraint if
1430 a) the new constraint can rewrite the inert one
1431 b) 'a' is free in the inert constraint (so that it *will*)
1432 rewrite it if we kick it out.
1433
1434 For (b) we use tyVarsOfCt, which returns the type variables /and
1435 the kind variables/ that are directly visible in the type. Hence we
1436 will have exposed all the rewriting we care about to make the most
1437 precise kinds visible for matching classes etc. No need to kick out
1438 constraints that mention type variables whose kinds contain this
1439 variable! (Except see Note [Kicking out Irreds].)
1440
1441 Note [Kicking out Irreds]
1442 ~~~~~~~~~~~~~~~~~~~~~~~~~
1443 There is an awkward special case for Irreds. When we have a
1444 kind-mis-matched equality constraint (a:k1) ~ (ty:k2), we turn it into
1445 an Irred (see Note [Equalities with incompatible kinds] in
1446 TcCanonical). So in this case the free kind variables of k1 and k2
1447 are not visible. More precisely, the type looks like
1448 (~) k1 (a:k1) (ty:k2)
1449 because (~) has kind forall k. k -> k -> Constraint. So the constraint
1450 itself is ill-kinded. We can "see" k1 but not k2. That's why we use
1451 closeOverKinds to make sure we see k2.
1452
1453 This is not pretty. Maybe (~) should have kind
1454 (~) :: forall k1 k1. k1 -> k2 -> Constraint
1455
1456 Note [Kick out insolubles]
1457 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1458 Suppose we have an insoluble alpha ~ [alpha], which is insoluble
1459 because an occurs check. And then we unify alpha := [Int].
1460 Then we really want to rewrite the insouluble to [Int] ~ [[Int]].
1461 Now it can be decomposed. Otherwise we end up with a "Can't match
1462 [Int] ~ [[Int]]" which is true, but a bit confusing because the
1463 outer type constructors match.
1464
1465
1466 Note [Avoid double unifications]
1467 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1468 The spontaneous solver has to return a given which mentions the unified unification
1469 variable *on the left* of the equality. Here is what happens if not:
1470 Original wanted: (a ~ alpha), (alpha ~ Int)
1471 We spontaneously solve the first wanted, without changing the order!
1472 given : a ~ alpha [having unified alpha := a]
1473 Now the second wanted comes along, but he cannot rewrite the given, so we simply continue.
1474 At the end we spontaneously solve that guy, *reunifying* [alpha := Int]
1475
1476 We avoid this problem by orienting the resulting given so that the unification
1477 variable is on the left. [Note that alternatively we could attempt to
1478 enforce this at canonicalization]
1479
1480 See also Note [No touchables as FunEq RHS] in TcSMonad; avoiding
1481 double unifications is the main reason we disallow touchable
1482 unification variables as RHS of type family equations: F xis ~ alpha.
1483
1484
1485 ************************************************************************
1486 * *
1487 * Functional dependencies, instantiation of equations
1488 * *
1489 ************************************************************************
1490
1491 When we spot an equality arising from a functional dependency,
1492 we now use that equality (a "wanted") to rewrite the work-item
1493 constraint right away. This avoids two dangers
1494
1495 Danger 1: If we send the original constraint on down the pipeline
1496 it may react with an instance declaration, and in delicate
1497 situations (when a Given overlaps with an instance) that
1498 may produce new insoluble goals: see Trac #4952
1499
1500 Danger 2: If we don't rewrite the constraint, it may re-react
1501 with the same thing later, and produce the same equality
1502 again --> termination worries.
1503
1504 To achieve this required some refactoring of FunDeps.hs (nicer
1505 now!).
1506 -}
1507
1508 emitFunDepDeriveds :: [FunDepEqn CtLoc] -> TcS ()
1509 emitFunDepDeriveds fd_eqns
1510 = mapM_ do_one_FDEqn fd_eqns
1511 where
1512 do_one_FDEqn (FDEqn { fd_qtvs = tvs, fd_eqs = eqs, fd_loc = loc })
1513 | null tvs -- Common shortcut
1514 = mapM_ (unifyDerived loc Nominal) eqs
1515 | otherwise
1516 = do { (subst, _) <- instFlexiTcS tvs -- Takes account of kind substitution
1517 ; mapM_ (do_one_eq loc subst) eqs }
1518
1519 do_one_eq loc subst (Pair ty1 ty2)
1520 = unifyDerived loc Nominal $
1521 Pair (Type.substTy subst ty1) (Type.substTy subst ty2)
1522
1523 {-
1524 *********************************************************************************
1525 * *
1526 The top-reaction Stage
1527 * *
1528 *********************************************************************************
1529 -}
1530
1531 topReactionsStage :: WorkItem -> TcS (StopOrContinue Ct)
1532 topReactionsStage wi
1533 = do { inerts <- getTcSInerts
1534 ; tir <- doTopReact inerts wi
1535 ; case tir of
1536 ContinueWith wi -> return (ContinueWith wi)
1537 Stop ev s -> return (Stop ev (ptext (sLit "Top react:") <+> s)) }
1538
1539 doTopReact :: InertSet -> WorkItem -> TcS (StopOrContinue Ct)
1540 -- The work item does not react with the inert set, so try interaction with top-level
1541 -- instances. Note:
1542 --
1543 -- (a) The place to add superclasses in not here in doTopReact stage.
1544 -- Instead superclasses are added in the worklist as part of the
1545 -- canonicalization process. See Note [Adding superclasses].
1546
1547 doTopReact inerts work_item
1548 = do { traceTcS "doTopReact" (ppr work_item)
1549 ; case work_item of
1550 CDictCan {} -> doTopReactDict inerts work_item
1551 CFunEqCan {} -> doTopReactFunEq work_item
1552 _ -> -- Any other work item does not react with any top-level equations
1553 return (ContinueWith work_item) }
1554
1555 --------------------
1556 doTopReactDict :: InertSet -> Ct -> TcS (StopOrContinue Ct)
1557 -- Try to use type-class instance declarations to simplify the constraint
1558 doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls
1559 , cc_tyargs = xis })
1560 | isGiven fl -- Never use instances for Given constraints
1561 = do { try_fundep_improvement
1562 ; continueWith work_item }
1563
1564 | Just ev <- lookupSolvedDict inerts cls xis -- Cached
1565 = do { setEvBindIfWanted fl (ctEvTerm ev);
1566 ; stopWith fl "Dict/Top (cached)" }
1567
1568 | isDerived fl -- Use type-class instances for Deriveds, in the hope
1569 -- of generating some improvements
1570 -- C.f. Example 3 of Note [The improvement story]
1571 -- It's easy because no evidence is involved
1572 = do { lkup_inst_res <- matchClassInst inerts cls xis dict_loc
1573 ; case lkup_inst_res of
1574 GenInst preds _ s -> do { mapM_ (emitNewDerived dict_loc) preds
1575 ; unless s $
1576 insertSafeOverlapFailureTcS work_item
1577 ; stopWith fl "Dict/Top (solved)" }
1578
1579 NoInstance -> do { -- If there is no instance, try improvement
1580 try_fundep_improvement
1581 ; continueWith work_item } }
1582
1583 | otherwise -- Wanted, but not cached
1584 = do { lkup_inst_res <- matchClassInst inerts cls xis dict_loc
1585 ; case lkup_inst_res of
1586 GenInst theta mk_ev s -> do { addSolvedDict fl cls xis
1587 ; unless s $
1588 insertSafeOverlapFailureTcS work_item
1589 ; solve_from_instance theta mk_ev }
1590 NoInstance -> continueWith work_item }
1591 where
1592 dict_pred = mkClassPred cls xis
1593 dict_loc = ctEvLoc fl
1594 dict_origin = ctLocOrigin dict_loc
1595 deeper_loc = bumpCtLocDepth dict_loc
1596
1597 solve_from_instance :: [TcPredType] -> ([EvId] -> EvTerm) -> TcS (StopOrContinue Ct)
1598 -- Precondition: evidence term matches the predicate workItem
1599 solve_from_instance theta mk_ev
1600 | null theta
1601 = do { traceTcS "doTopReact/found nullary instance for" $ ppr fl
1602 ; setWantedEvBind (ctEvId fl) (mk_ev [])
1603 ; stopWith fl "Dict/Top (solved, no new work)" }
1604 | otherwise
1605 = do { checkReductionDepth deeper_loc dict_pred
1606 ; traceTcS "doTopReact/found non-nullary instance for" $ ppr fl
1607 ; evc_vars <- mapM (newWantedEvVar deeper_loc) theta
1608 ; setWantedEvBind (ctEvId fl) (mk_ev (map (ctEvId . fst) evc_vars))
1609 ; emitWorkNC (freshGoals evc_vars)
1610 ; stopWith fl "Dict/Top (solved, more work)" }
1611
1612 -- We didn't solve it; so try functional dependencies with
1613 -- the instance environment, and return
1614 -- We just land here for Given and Derived;
1615 -- See Note [When improvement happens during solving]
1616 -- See also Note [Weird fundeps]
1617 try_fundep_improvement
1618 = do { instEnvs <- getInstEnvs
1619 ; emitFunDepDeriveds $
1620 improveFromInstEnv instEnvs mk_ct_loc dict_pred }
1621
1622 mk_ct_loc :: PredType -- From instance decl
1623 -> SrcSpan -- also from instance deol
1624 -> CtLoc
1625 mk_ct_loc inst_pred inst_loc
1626 = dict_loc { ctl_origin = FunDepOrigin2 dict_pred dict_origin
1627 inst_pred inst_loc }
1628
1629 doTopReactDict _ w = pprPanic "doTopReactDict" (ppr w)
1630
1631 --------------------
1632 doTopReactFunEq :: Ct -> TcS (StopOrContinue Ct)
1633 -- Note [Short cut for top-level reaction]
1634 doTopReactFunEq work_item@(CFunEqCan { cc_ev = old_ev, cc_fun = fam_tc
1635 , cc_tyargs = args , cc_fsk = fsk })
1636 = ASSERT(isTypeFamilyTyCon fam_tc) -- No associated data families
1637 -- have reached this far
1638 -- Look up in top-level instances, or built-in axiom
1639 do { match_res <- matchFam fam_tc args -- See Note [MATCHING-SYNONYMS]
1640 ; case match_res of {
1641 Nothing -> do { try_improve
1642 ; continueWith work_item } ;
1643 Just (ax_co, rhs_ty)
1644
1645 -- Found a top-level instance
1646
1647 | Just (tc, tc_args) <- tcSplitTyConApp_maybe rhs_ty
1648 , isTypeFamilyTyCon tc
1649 , tc_args `lengthIs` tyConArity tc -- Short-cut
1650 -> shortCutReduction old_ev fsk ax_co tc tc_args
1651 -- Try shortcut; see Note [Short cut for top-level reaction]
1652
1653 | isGiven old_ev -- Not shortcut
1654 -> do { let final_co = mkTcSymCo (ctEvCoercion old_ev) `mkTcTransCo` ax_co
1655 -- final_co :: fsk ~ rhs_ty
1656 ; new_ev <- newGivenEvVar deeper_loc (mkTcEqPred (mkTyVarTy fsk) rhs_ty,
1657 EvCoercion final_co)
1658 ; emitWorkNC [new_ev] -- Non-canonical; that will mean we flatten rhs_ty
1659 ; stopWith old_ev "Fun/Top (given)" }
1660
1661 | not (fsk `elemVarSet` tyVarsOfType rhs_ty)
1662 -> do { dischargeFmv old_ev fsk ax_co rhs_ty
1663 ; traceTcS "doTopReactFunEq" $
1664 vcat [ text "old_ev:" <+> ppr old_ev
1665 , nest 2 (text ":=") <+> ppr ax_co ]
1666 ; stopWith old_ev "Fun/Top (wanted)" }
1667
1668 | otherwise -- We must not assign ufsk := ...ufsk...!
1669 -> do { alpha_ty <- newFlexiTcSTy (tyVarKind fsk)
1670 ; new_ev <- newWantedEvVarNC loc (mkTcEqPred alpha_ty rhs_ty)
1671 ; emitWorkNC [new_ev]
1672 -- By emitting this as non-canonical, we deal with all
1673 -- flattening, occurs-check, and ufsk := ufsk issues
1674 ; let final_co = ax_co `mkTcTransCo` mkTcSymCo (ctEvCoercion new_ev)
1675 -- ax_co :: fam_tc args ~ rhs_ty
1676 -- new_ev :: alpha ~ rhs_ty
1677 -- ufsk := alpha
1678 -- final_co :: fam_tc args ~ alpha
1679 ; dischargeFmv old_ev fsk final_co alpha_ty
1680 ; traceTcS "doTopReactFunEq (occurs)" $
1681 vcat [ text "old_ev:" <+> ppr old_ev
1682 , nest 2 (text ":=") <+> ppr final_co
1683 , text "new_ev:" <+> ppr new_ev ]
1684 ; stopWith old_ev "Fun/Top (wanted)" } } }
1685 where
1686 loc = ctEvLoc old_ev
1687 deeper_loc = bumpCtLocDepth loc
1688
1689 try_improve
1690 | not (isWanted old_ev) -- Try improvement only for Given/Derived constraints
1691 -- See Note [When improvement happens during solving]
1692 , Just ops <- isBuiltInSynFamTyCon_maybe fam_tc
1693 = do { inert_eqs <- getInertEqs
1694 ; let eqns = sfInteractTop ops args (lookupFlattenTyVar inert_eqs fsk)
1695 ; mapM_ (unifyDerived loc Nominal) eqns }
1696 | otherwise
1697 = return ()
1698
1699 doTopReactFunEq w = pprPanic "doTopReactFunEq" (ppr w)
1700
1701 shortCutReduction :: CtEvidence -> TcTyVar -> TcCoercion
1702 -> TyCon -> [TcType] -> TcS (StopOrContinue Ct)
1703 -- See Note [Top-level reductions for type functions]
1704 shortCutReduction old_ev fsk ax_co fam_tc tc_args
1705 | isGiven old_ev
1706 = ASSERT( ctEvEqRel old_ev == NomEq )
1707 do { (xis, cos) <- flattenManyNom old_ev tc_args
1708 -- ax_co :: F args ~ G tc_args
1709 -- cos :: xis ~ tc_args
1710 -- old_ev :: F args ~ fsk
1711 -- G cos ; sym ax_co ; old_ev :: G xis ~ fsk
1712
1713 ; new_ev <- newGivenEvVar deeper_loc
1714 ( mkTcEqPred (mkTyConApp fam_tc xis) (mkTyVarTy fsk)
1715 , EvCoercion (mkTcTyConAppCo Nominal fam_tc cos
1716 `mkTcTransCo` mkTcSymCo ax_co
1717 `mkTcTransCo` ctEvCoercion old_ev) )
1718
1719 ; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc, cc_tyargs = xis, cc_fsk = fsk }
1720 ; emitWorkCt new_ct
1721 ; stopWith old_ev "Fun/Top (given, shortcut)" }
1722
1723 | otherwise
1724 = ASSERT( not (isDerived old_ev) ) -- Caller ensures this
1725 ASSERT( ctEvEqRel old_ev == NomEq )
1726 do { (xis, cos) <- flattenManyNom old_ev tc_args
1727 -- ax_co :: F args ~ G tc_args
1728 -- cos :: xis ~ tc_args
1729 -- G cos ; sym ax_co ; old_ev :: G xis ~ fsk
1730 -- new_ev :: G xis ~ fsk
1731 -- old_ev :: F args ~ fsk := ax_co ; sym (G cos) ; new_ev
1732
1733 ; new_ev <- newWantedEvVarNC deeper_loc
1734 (mkTcEqPred (mkTyConApp fam_tc xis) (mkTyVarTy fsk))
1735 ; setWantedEvBind (ctEvId old_ev)
1736 (EvCoercion (ax_co `mkTcTransCo` mkTcSymCo (mkTcTyConAppCo Nominal fam_tc cos)
1737 `mkTcTransCo` ctEvCoercion new_ev))
1738
1739 ; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc, cc_tyargs = xis, cc_fsk = fsk }
1740 ; emitWorkCt new_ct
1741 ; stopWith old_ev "Fun/Top (wanted, shortcut)" }
1742 where
1743 loc = ctEvLoc old_ev
1744 deeper_loc = bumpCtLocDepth loc
1745
1746 dischargeFmv :: CtEvidence -> TcTyVar -> TcCoercion -> TcType -> TcS ()
1747 -- (dischargeFmv x fmv co ty)
1748 -- [W] ev :: F tys ~ fmv
1749 -- co :: F tys ~ xi
1750 -- Precondition: fmv is not filled, and fuv `notElem` xi
1751 --
1752 -- Then set fmv := xi,
1753 -- set ev := co
1754 -- kick out any inert things that are now rewritable
1755 dischargeFmv ev fmv co xi
1756 = ASSERT2( not (fmv `elemVarSet` tyVarsOfType xi), ppr ev $$ ppr fmv $$ ppr xi )
1757 do { case ev of
1758 CtWanted { ctev_evar = evar } -> setWantedEvBind evar (EvCoercion co)
1759 CtDerived {} -> return () -- Happens during improvement
1760 CtGiven {} -> pprPanic "dischargeFmv" (ppr ev)
1761 ; unifyTyVar fmv xi
1762 ; n_kicked <- kickOutRewritable Given NomEq fmv
1763 ; traceTcS "dischargeFuv" (ppr fmv <+> equals <+> ppr xi $$ ppr_kicked n_kicked) }
1764
1765 {- Note [Top-level reductions for type functions]
1766 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1767 c.f. Note [The flattening story] in TcFlatten
1768
1769 Suppose we have a CFunEqCan F tys ~ fmv/fsk, and a matching axiom.
1770 Here is what we do, in four cases:
1771
1772 * Wanteds: general firing rule
1773 (work item) [W] x : F tys ~ fmv
1774 instantiate axiom: ax_co : F tys ~ rhs
1775
1776 Then:
1777 Discharge fmv := alpha
1778 Discharge x := ax_co ; sym x2
1779 New wanted [W] x2 : alpha ~ rhs (Non-canonical)
1780 This is *the* way that fmv's get unified; even though they are
1781 "untouchable".
1782
1783 NB: it can be the case that fmv appears in the (instantiated) rhs.
1784 In that case the new Non-canonical wanted will be loopy, but that's
1785 ok. But it's good reason NOT to claim that it is canonical!
1786
1787 * Wanteds: short cut firing rule
1788 Applies when the RHS of the axiom is another type-function application
1789 (work item) [W] x : F tys ~ fmv
1790 instantiate axiom: ax_co : F tys ~ G rhs_tys
1791
1792 It would be a waste to create yet another fmv for (G rhs_tys).
1793 Instead (shortCutReduction):
1794 - Flatten rhs_tys (cos : rhs_tys ~ rhs_xis)
1795 - Add G rhs_xis ~ fmv to flat cache (note: the same old fmv)
1796 - New canonical wanted [W] x2 : G rhs_xis ~ fmv (CFunEqCan)
1797 - Discharge x := ax_co ; G cos ; x2
1798
1799 * Givens: general firing rule
1800 (work item) [G] g : F tys ~ fsk
1801 instantiate axiom: ax_co : F tys ~ rhs
1802
1803 Now add non-canonical given (since rhs is not flat)
1804 [G] (sym g ; ax_co) : fsk ~ rhs (Non-canonical)
1805
1806 * Givens: short cut firing rule
1807 Applies when the RHS of the axiom is another type-function application
1808 (work item) [G] g : F tys ~ fsk
1809 instantiate axiom: ax_co : F tys ~ G rhs_tys
1810
1811 It would be a waste to create yet another fsk for (G rhs_tys).
1812 Instead (shortCutReduction):
1813 - Flatten rhs_tys: flat_cos : tys ~ flat_tys
1814 - Add new Canonical given
1815 [G] (sym (G flat_cos) ; co ; g) : G flat_tys ~ fsk (CFunEqCan)
1816
1817 Note [Cached solved FunEqs]
1818 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1819 When trying to solve, say (FunExpensive big-type ~ ty), it's important
1820 to see if we have reduced (FunExpensive big-type) before, lest we
1821 simply repeat it. Hence the lookup in inert_solved_funeqs. Moreover
1822 we must use `canRewriteOrSame` because both uses might (say) be Wanteds,
1823 and we *still* want to save the re-computation.
1824
1825 Note [MATCHING-SYNONYMS]
1826 ~~~~~~~~~~~~~~~~~~~~~~~~
1827 When trying to match a dictionary (D tau) to a top-level instance, or a
1828 type family equation (F taus_1 ~ tau_2) to a top-level family instance,
1829 we do *not* need to expand type synonyms because the matcher will do that for us.
1830
1831
1832 Note [RHS-FAMILY-SYNONYMS]
1833 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1834 The RHS of a family instance is represented as yet another constructor which is
1835 like a type synonym for the real RHS the programmer declared. Eg:
1836 type instance F (a,a) = [a]
1837 Becomes:
1838 :R32 a = [a] -- internal type synonym introduced
1839 F (a,a) ~ :R32 a -- instance
1840
1841 When we react a family instance with a type family equation in the work list
1842 we keep the synonym-using RHS without expansion.
1843
1844 Note [FunDep and implicit parameter reactions]
1845 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1846 Currently, our story of interacting two dictionaries (or a dictionary
1847 and top-level instances) for functional dependencies, and implicit
1848 paramters, is that we simply produce new Derived equalities. So for example
1849
1850 class D a b | a -> b where ...
1851 Inert:
1852 d1 :g D Int Bool
1853 WorkItem:
1854 d2 :w D Int alpha
1855
1856 We generate the extra work item
1857 cv :d alpha ~ Bool
1858 where 'cv' is currently unused. However, this new item can perhaps be
1859 spontaneously solved to become given and react with d2,
1860 discharging it in favour of a new constraint d2' thus:
1861 d2' :w D Int Bool
1862 d2 := d2' |> D Int cv
1863 Now d2' can be discharged from d1
1864
1865 We could be more aggressive and try to *immediately* solve the dictionary
1866 using those extra equalities, but that requires those equalities to carry
1867 evidence and derived do not carry evidence.
1868
1869 If that were the case with the same inert set and work item we might dischard
1870 d2 directly:
1871
1872 cv :w alpha ~ Bool
1873 d2 := d1 |> D Int cv
1874
1875 But in general it's a bit painful to figure out the necessary coercion,
1876 so we just take the first approach. Here is a better example. Consider:
1877 class C a b c | a -> b
1878 And:
1879 [Given] d1 : C T Int Char
1880 [Wanted] d2 : C T beta Int
1881 In this case, it's *not even possible* to solve the wanted immediately.
1882 So we should simply output the functional dependency and add this guy
1883 [but NOT its superclasses] back in the worklist. Even worse:
1884 [Given] d1 : C T Int beta
1885 [Wanted] d2: C T beta Int
1886 Then it is solvable, but its very hard to detect this on the spot.
1887
1888 It's exactly the same with implicit parameters, except that the
1889 "aggressive" approach would be much easier to implement.
1890
1891 Note [When improvement happens during solving]
1892 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1893 Improvement for functional dependencies or type-function injectivity
1894 means emitting a Derived equality constraint by interacting the work
1895 item with an inert item, or with the top-level instances. e.g.
1896
1897 class C a b | a -> b
1898 [W] C a b, [W] C a c ==> [D] b ~ c
1899
1900 We fire the fundep improvement if the "work item" is Given or Derived,
1901 but not Wanted. Reason:
1902
1903 * Given: we want to spot Given/Given inconsistencies because that means
1904 unreachable code. See typecheck/should_fail/FDsFromGivens
1905
1906 * Derived: during the improvement phase (i.e. when handling Derived
1907 constraints) we also do improvement for functional dependencies. e.g.
1908 And similarly wrt top-level instances.
1909
1910 * Wanted: spotting fundep improvements is somewhat inefficient, and
1911 and if we can solve without improvement so much the better.
1912 So we don't bother to do this when solving Wanteds, instead
1913 leaving it for the try_improvement loop
1914
1915 Example (tcfail138)
1916 class L a b | a -> b
1917 class (G a, L a b) => C a b
1918
1919 instance C a b' => G (Maybe a)
1920 instance C a b => C (Maybe a) a
1921 instance L (Maybe a) a
1922
1923 When solving the superclasses of the (C (Maybe a) a) instance, we get
1924 [G] C a b, and hance by superclasses, [G] G a, [G] L a b
1925 [W] G (Maybe a)
1926 Use the instance decl to get
1927 [W] C a beta
1928
1929 During improvement (see Note [The improvement story]) we generate the superclasses
1930 of (C a beta): [D] L a beta. Now using fundeps, combine with [G] L a b to get
1931 [D] beta ~ b, which is what we want.
1932
1933
1934 Note [Weird fundeps]
1935 ~~~~~~~~~~~~~~~~~~~~
1936 Consider class Het a b | a -> b where
1937 het :: m (f c) -> a -> m b
1938
1939 class GHet (a :: * -> *) (b :: * -> *) | a -> b
1940 instance GHet (K a) (K [a])
1941 instance Het a b => GHet (K a) (K b)
1942
1943 The two instances don't actually conflict on their fundeps,
1944 although it's pretty strange. So they are both accepted. Now
1945 try [W] GHet (K Int) (K Bool)
1946 This triggers fundeps from both instance decls;
1947 [D] K Bool ~ K [a]
1948 [D] K Bool ~ K beta
1949 And there's a risk of complaining about Bool ~ [a]. But in fact
1950 the Wanted matches the second instance, so we never get as far
1951 as the fundeps.
1952
1953 Trac #7875 is a case in point.
1954
1955 Note [Overriding implicit parameters]
1956 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1957 Consider
1958 f :: (?x::a) -> Bool -> a
1959
1960 g v = let ?x::Int = 3
1961 in (f v, let ?x::Bool = True in f v)
1962
1963 This should probably be well typed, with
1964 g :: Bool -> (Int, Bool)
1965
1966 So the inner binding for ?x::Bool *overrides* the outer one.
1967 Hence a work-item Given overrides an inert-item Given.
1968 -}
1969
1970 -- | Indicates if Instance met the Safe Haskell overlapping instances safety
1971 -- check.
1972 --
1973 -- See Note [Safe Haskell Overlapping Instances] in TcSimplify
1974 -- See Note [Safe Haskell Overlapping Instances Implementation] in TcSimplify
1975 type SafeOverlapping = Bool
1976
1977 data LookupInstResult
1978 = NoInstance
1979 | GenInst [TcPredType] ([EvId] -> EvTerm) SafeOverlapping
1980
1981 instance Outputable LookupInstResult where
1982 ppr NoInstance = text "NoInstance"
1983 ppr (GenInst ev _ s) = text "GenInst" <+> ppr ev <+> ss
1984 where ss = text $ if s then "[safe]" else "[unsafe]"
1985
1986
1987 matchClassInst :: InertSet -> Class -> [Type] -> CtLoc -> TcS LookupInstResult
1988
1989 matchClassInst _ clas [ ty ] _
1990 | className clas == knownNatClassName
1991 , Just n <- isNumLitTy ty = makeDict (EvNum n)
1992
1993 | className clas == knownSymbolClassName
1994 , Just s <- isStrLitTy ty = makeDict (EvStr s)
1995
1996 where
1997 {- This adds a coercion that will convert the literal into a dictionary
1998 of the appropriate type. See Note [KnownNat & KnownSymbol and EvLit]
1999 in TcEvidence. The coercion happens in 2 steps:
2000
2001 Integer -> SNat n -- representation of literal to singleton
2002 SNat n -> KnownNat n -- singleton to dictionary
2003
2004 The process is mirrored for Symbols:
2005 String -> SSymbol n
2006 SSymbol n -> KnownSymbol n
2007 -}
2008 makeDict evLit
2009 | Just (_, co_dict) <- tcInstNewTyCon_maybe (classTyCon clas) [ty]
2010 -- co_dict :: KnownNat n ~ SNat n
2011 , [ meth ] <- classMethods clas
2012 , Just tcRep <- tyConAppTyCon_maybe -- SNat
2013 $ funResultTy -- SNat n
2014 $ dropForAlls -- KnownNat n => SNat n
2015 $ idType meth -- forall n. KnownNat n => SNat n
2016 , Just (_, co_rep) <- tcInstNewTyCon_maybe tcRep [ty]
2017 -- SNat n ~ Integer
2018 , let ev_tm = mkEvCast (EvLit evLit) (mkTcSymCo (mkTcTransCo co_dict co_rep))
2019 = return $ GenInst [] (\_ -> ev_tm) True
2020
2021 | otherwise
2022 = panicTcS (text "Unexpected evidence for" <+> ppr (className clas)
2023 $$ vcat (map (ppr . idType) (classMethods clas)))
2024
2025 matchClassInst _ clas [k,t] _
2026 | className clas == typeableClassName = matchTypeableClass clas k t
2027
2028 matchClassInst inerts clas tys loc
2029 = do { dflags <- getDynFlags
2030 ; traceTcS "matchClassInst" $ vcat [ text "pred =" <+> ppr pred
2031 , text "inerts=" <+> ppr inerts ]
2032 ; instEnvs <- getInstEnvs
2033 ; safeOverlapCheck <- (`elem` [Sf_Safe, Sf_Trustworthy])
2034 <$> safeHaskell <$> getDynFlags
2035 ; let (matches, unify, unsafeOverlaps) = lookupInstEnv True instEnvs clas tys
2036 safeHaskFail = safeOverlapCheck && not (null unsafeOverlaps)
2037 ; case (matches, unify, safeHaskFail) of
2038
2039 -- Nothing matches
2040 ([], _, _)
2041 -> do { traceTcS "matchClass not matching" $
2042 vcat [ text "dict" <+> ppr pred ]
2043 ; return NoInstance }
2044
2045 -- A single match (& no safe haskell failure)
2046 ([(ispec, inst_tys)], [], False)
2047 | not (xopt Opt_IncoherentInstances dflags)
2048 , not (isEmptyBag unifiable_givens)
2049 -> -- See Note [Instance and Given overlap]
2050 do { traceTcS "Delaying instance application" $
2051 vcat [ text "Work item=" <+> pprType (mkClassPred clas tys)
2052 , text "Relevant given dictionaries="
2053 <+> ppr unifiable_givens ]
2054 ; return NoInstance }
2055
2056 | otherwise
2057 -> do { let dfun_id = instanceDFunId ispec
2058 ; traceTcS "matchClass success" $
2059 vcat [text "dict" <+> ppr pred,
2060 text "witness" <+> ppr dfun_id
2061 <+> ppr (idType dfun_id) ]
2062 -- Record that this dfun is needed
2063 ; match_one (null unsafeOverlaps) dfun_id inst_tys }
2064
2065 -- More than one matches (or Safe Haskell fail!). Defer any
2066 -- reactions of a multitude until we learn more about the reagent
2067 (matches, _, _)
2068 -> do { traceTcS "matchClass multiple matches, deferring choice" $
2069 vcat [text "dict" <+> ppr pred,
2070 text "matches" <+> ppr matches]
2071 ; return NoInstance } }
2072 where
2073 pred = mkClassPred clas tys
2074
2075 match_one :: SafeOverlapping -> DFunId -> [DFunInstType] -> TcS LookupInstResult
2076 -- See Note [DFunInstType: instantiating types] in InstEnv
2077 match_one so dfun_id mb_inst_tys
2078 = do { checkWellStagedDFun pred dfun_id loc
2079 ; (tys, theta) <- instDFunType dfun_id mb_inst_tys
2080 ; return $ GenInst theta (EvDFunApp dfun_id tys) so }
2081
2082 unifiable_givens :: Cts
2083 unifiable_givens = filterBag matchable $
2084 findDictsByClass (inert_dicts $ inert_cans inerts) clas
2085
2086 matchable (CDictCan { cc_class = clas_g, cc_tyargs = sys, cc_ev = fl })
2087 | isGiven fl
2088 , Just {} <- tcUnifyTys bind_meta_tv tys sys
2089 = ASSERT( clas_g == clas ) True
2090 | otherwise = False -- No overlap with a solved, already been taken care of
2091 -- by the overlap check with the instance environment.
2092 matchable ct = pprPanic "Expecting dictionary!" (ppr ct)
2093
2094 bind_meta_tv :: TcTyVar -> BindFlag
2095 -- Any meta tyvar may be unified later, so we treat it as
2096 -- bindable when unifying with givens. That ensures that we
2097 -- conservatively assume that a meta tyvar might get unified with
2098 -- something that matches the 'given', until demonstrated
2099 -- otherwise.
2100 bind_meta_tv tv | isMetaTyVar tv = BindMe
2101 | otherwise = Skolem
2102
2103 {- Note [Instance and Given overlap]
2104 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2105 Example, from the OutsideIn(X) paper:
2106 instance P x => Q [x]
2107 instance (x ~ y) => R y [x]
2108
2109 wob :: forall a b. (Q [b], R b a) => a -> Int
2110
2111 g :: forall a. Q [a] => [a] -> Int
2112 g x = wob x
2113
2114 This will generate the impliation constraint:
2115 Q [a] => (Q [beta], R beta [a])
2116 If we react (Q [beta]) with its top-level axiom, we end up with a
2117 (P beta), which we have no way of discharging. On the other hand,
2118 if we react R beta [a] with the top-level we get (beta ~ a), which
2119 is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
2120 now solvable by the given Q [a].
2121
2122 The solution is that:
2123 In matchClassInst (and thus in topReact), we return a matching
2124 instance only when there is no Given in the inerts which is
2125 unifiable to this particular dictionary.
2126
2127 We treat any meta-tyvar as "unifiable" for this purpose,
2128 *including* untouchable ones
2129
2130 The end effect is that, much as we do for overlapping instances, we
2131 delay choosing a class instance if there is a possibility of another
2132 instance OR a given to match our constraint later on. This fixes
2133 Trac #4981 and #5002.
2134
2135 Other notes:
2136
2137 * This is arguably not easy to appear in practice due to our
2138 aggressive prioritization of equality solving over other
2139 constraints, but it is possible. I've added a test case in
2140 typecheck/should-compile/GivenOverlapping.hs
2141
2142 * Another "live" example is Trac #10195
2143
2144 * We ignore the overlap problem if -XIncoherentInstances is in force:
2145 see Trac #6002 for a worked-out example where this makes a
2146 difference.
2147
2148 * Moreover notice that our goals here are different than the goals of
2149 the top-level overlapping checks. There we are interested in
2150 validating the following principle:
2151
2152 If we inline a function f at a site where the same global
2153 instance environment is available as the instance environment at
2154 the definition site of f then we should get the same behaviour.
2155
2156 But for the Given Overlap check our goal is just related to completeness of
2157 constraint solving.
2158 -}
2159
2160 -- | Is the constraint for an implicit CallStack parameter?
2161 isCallStackIP :: CtLoc -> Class -> Type -> Maybe (EvTerm -> EvCallStack)
2162 isCallStackIP loc cls ty
2163 | Just (tc, []) <- splitTyConApp_maybe ty
2164 , cls `hasKey` ipClassNameKey && tc `hasKey` callStackTyConKey
2165 = occOrigin (ctLocOrigin loc)
2166 where
2167 -- We only want to grab constraints that arose due to the use of an IP or a
2168 -- function call. See Note [Overview of implicit CallStacks]
2169 occOrigin (OccurrenceOf n)
2170 = Just (EvCsPushCall n locSpan)
2171 occOrigin (IPOccOrigin n)
2172 = Just (EvCsTop ('?' `consFS` hsIPNameFS n) locSpan)
2173 occOrigin _
2174 = Nothing
2175 locSpan
2176 = ctLocSpan loc
2177 isCallStackIP _ _ _
2178 = Nothing
2179
2180
2181
2182 -- | Assumes that we've checked that this is the 'Typeable' class,
2183 -- and it was applied to the correct argument.
2184 matchTypeableClass :: Class -> Kind -> Type -> TcS LookupInstResult
2185 matchTypeableClass clas _k t
2186
2187 -- See Note [No Typeable for qualified types]
2188 | isForAllTy t = return NoInstance
2189 -- Is the type of the form `C => t`?
2190 | Just (t1,_) <- splitFunTy_maybe t,
2191 isConstraintKind (typeKind t1) = return NoInstance
2192
2193 | Just (tc, ks) <- splitTyConApp_maybe t
2194 , all isKind ks = doTyCon tc ks
2195 | Just (f,kt) <- splitAppTy_maybe t = doTyApp f kt
2196 | Just _ <- isNumLitTy t = mkSimpEv (EvTypeableTyLit t)
2197 | Just _ <- isStrLitTy t = mkSimpEv (EvTypeableTyLit t)
2198 | otherwise = return NoInstance
2199
2200 where
2201 -- Representation for type constructor applied to some kinds
2202 doTyCon tc ks =
2203 case mapM kindRep ks of
2204 Nothing -> return NoInstance
2205 Just kReps -> mkSimpEv (EvTypeableTyCon tc kReps)
2206
2207 {- Representation for an application of a type to a type-or-kind.
2208 This may happen when the type expression starts with a type variable.
2209 Example (ignoring kind parameter):
2210 Typeable (f Int Char) -->
2211 (Typeable (f Int), Typeable Char) -->
2212 (Typeable f, Typeable Int, Typeable Char) --> (after some simp. steps)
2213 Typeable f
2214 -}
2215 doTyApp f tk
2216 | isKind tk
2217 = return NoInstance -- We can't solve until we know the ctr.
2218 | otherwise
2219 = return $ GenInst [mk_typeable_pred f, mk_typeable_pred tk]
2220 (\[t1,t2] -> EvTypeable $ EvTypeableTyApp (EvId t1,f) (EvId t2,tk))
2221 True
2222
2223 -- Representation for concrete kinds. We just use the kind itself,
2224 -- but first check to make sure that it is "simple" (i.e., made entirely
2225 -- out of kind constructors).
2226 kindRep ki = do (_,ks) <- splitTyConApp_maybe ki
2227 mapM_ kindRep ks
2228 return ki
2229
2230 -- Emit a `Typeable` constraint for the given type.
2231 mk_typeable_pred ty = mkClassPred clas [ typeKind ty, ty ]
2232
2233 mkSimpEv ev = return $ GenInst [] (\_ -> EvTypeable ev) True
2234
2235 {- Note [No Typeable for polytype or for constraints]
2236 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2237 We do not support impredicative typeable, such as
2238 Typeable (forall a. a->a)
2239 Typeable (Eq a => a -> a)
2240 Typeable (() => Int)
2241 Typeable (((),()) => Int)
2242
2243 See Trac #9858. For forall's the case is clear: we simply don't have
2244 a TypeRep for them. For qualified but not polymorphic types, like
2245 (Eq a => a -> a), things are murkier. But:
2246
2247 * We don't need a TypeRep for these things. TypeReps are for
2248 monotypes only.
2249
2250 * Perhaps we could treat `=>` as another type constructor for `Typeable`
2251 purposes, and thus support things like `Eq Int => Int`, however,
2252 at the current state of affairs this would be an odd exception as
2253 no other class works with impredicative types.
2254 For now we leave it off, until we have a better story for impredicativity.
2255 -}