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