d26275b83976665508df20fc1cd06b49540ece29
[ghc.git] / compiler / typecheck / TcSMonad.hs
1 {-# LANGUAGE CPP, TypeFamilies #-}
2
3 -- Type definitions for the constraint solver
4 module TcSMonad (
5
6 -- The work list
7 WorkList(..), isEmptyWorkList, emptyWorkList,
8 extendWorkListNonEq, extendWorkListCt,
9 extendWorkListCts, extendWorkListEq, extendWorkListFunEq,
10 appendWorkList, extendWorkListImplic,
11 selectNextWorkItem,
12 workListSize, workListWantedCount,
13 getWorkList, updWorkListTcS,
14
15 -- The TcS monad
16 TcS, runTcS, runTcSDeriveds, runTcSWithEvBinds,
17 failTcS, warnTcS, addErrTcS,
18 runTcSEqualities,
19 nestTcS, nestImplicTcS, setEvBindsTcS, checkConstraintsTcS,
20
21 runTcPluginTcS, addUsedGRE, addUsedGREs,
22
23 -- Tracing etc
24 panicTcS, traceTcS,
25 traceFireTcS, bumpStepCountTcS, csTraceTcS,
26 wrapErrTcS, wrapWarnTcS,
27
28 -- Evidence creation and transformation
29 MaybeNew(..), freshGoals, isFresh, getEvExpr,
30
31 newTcEvBinds, newNoTcEvBinds,
32 newWantedEq, emitNewWantedEq,
33 newWanted, newWantedEvVar, newWantedNC, newWantedEvVarNC, newDerivedNC,
34 newBoundEvVarId,
35 unifyTyVar, unflattenFmv, reportUnifications,
36 setEvBind, setWantedEq, setEqIfWanted,
37 setWantedEvTerm, setWantedEvBind, setEvBindIfWanted,
38 newEvVar, newGivenEvVar, newGivenEvVars,
39 emitNewDeriveds, emitNewDerivedEq,
40 checkReductionDepth,
41 getSolvedDicts, setSolvedDicts,
42
43 getInstEnvs, getFamInstEnvs, -- Getting the environments
44 getTopEnv, getGblEnv, getLclEnv,
45 getTcEvBindsVar, getTcLevel,
46 getTcEvTyCoVars, getTcEvBindsMap, setTcEvBindsMap,
47 tcLookupClass, tcLookupId,
48
49 -- Inerts
50 InertSet(..), InertCans(..),
51 updInertTcS, updInertCans, updInertDicts, updInertIrreds,
52 getNoGivenEqs, setInertCans,
53 getInertEqs, getInertCans, getInertGivens,
54 getInertInsols,
55 getTcSInerts, setTcSInerts,
56 matchableGivens, prohibitedSuperClassSolve,
57 getUnsolvedInerts,
58 removeInertCts, getPendingScDicts,
59 addInertCan, addInertEq, insertFunEq,
60 emitWorkNC, emitWork,
61 isImprovable,
62
63 -- The Model
64 kickOutAfterUnification,
65
66 -- Inert Safe Haskell safe-overlap failures
67 addInertSafehask, insertSafeOverlapFailureTcS, updInertSafehask,
68 getSafeOverlapFailures,
69
70 -- Inert CDictCans
71 DictMap, emptyDictMap, lookupInertDict, findDictsByClass, addDict,
72 addDictsByClass, delDict, foldDicts, filterDicts, findDict,
73
74 -- Inert CTyEqCans
75 EqualCtList, findTyEqs, foldTyEqs, isInInertEqs,
76 lookupFlattenTyVar, lookupInertTyVar,
77
78 -- Inert solved dictionaries
79 addSolvedDict, lookupSolvedDict,
80
81 -- Irreds
82 foldIrreds,
83
84 -- The flattening cache
85 lookupFlatCache, extendFlatCache, newFlattenSkolem, -- Flatten skolems
86 dischargeFunEq, pprKicked,
87
88 -- Inert CFunEqCans
89 updInertFunEqs, findFunEq,
90 findFunEqsByTyCon,
91
92 instDFunType, -- Instantiation
93
94 -- MetaTyVars
95 newFlexiTcSTy, instFlexi, instFlexiX,
96 cloneMetaTyVar, demoteUnfilledFmv,
97 tcInstType, tcInstSkolTyVarsX,
98
99 TcLevel,
100 isFilledMetaTyVar_maybe, isFilledMetaTyVar,
101 zonkTyCoVarsAndFV, zonkTcType, zonkTcTypes, zonkTcTyVar, zonkCo,
102 zonkTyCoVarsAndFVList,
103 zonkSimples, zonkWC,
104 zonkTcTyCoVarBndr,
105
106 -- References
107 newTcRef, readTcRef, updTcRef,
108
109 -- Misc
110 getDefaultInfo, getDynFlags, getGlobalRdrEnvTcS,
111 matchFam, matchFamTcM,
112 checkWellStagedDFun,
113 pprEq -- Smaller utils, re-exported from TcM
114 -- TODO (DV): these are only really used in the
115 -- instance matcher in TcSimplify. I am wondering
116 -- if the whole instance matcher simply belongs
117 -- here
118 ) where
119
120 #include "HsVersions.h"
121
122 import GhcPrelude
123
124 import HscTypes
125
126 import qualified Inst as TcM
127 import InstEnv
128 import FamInst
129 import FamInstEnv
130
131 import qualified TcRnMonad as TcM
132 import qualified TcMType as TcM
133 import qualified TcEnv as TcM
134 ( checkWellStaged, topIdLvl, tcGetDefaultTys, tcLookupClass, tcLookupId )
135 import PrelNames( heqTyConKey, eqTyConKey )
136 import Kind
137 import TcType
138 import DynFlags
139 import Type
140 import Coercion
141 import Unify
142
143 import TcEvidence
144 import Class
145 import TyCon
146 import TcErrors ( solverDepthErrorTcS )
147
148 import Name
149 import Module ( HasModule, getModule )
150 import RdrName ( GlobalRdrEnv, GlobalRdrElt )
151 import qualified RnEnv as TcM
152 import Var
153 import VarEnv
154 import VarSet
155 import Outputable
156 import Bag
157 import UniqSupply
158 import Util
159 import TcRnTypes
160
161 import Unique
162 import UniqFM
163 import UniqDFM
164 import Maybes
165
166 import CoreMap
167 import Control.Monad
168 import qualified Control.Monad.Fail as MonadFail
169 import MonadUtils
170 import Data.IORef
171 import Data.List ( foldl', partition )
172
173 #if defined(DEBUG)
174 import Digraph
175 import UniqSet
176 #endif
177
178 {-
179 ************************************************************************
180 * *
181 * Worklists *
182 * Canonical and non-canonical constraints that the simplifier has to *
183 * work on. Including their simplification depths. *
184 * *
185 * *
186 ************************************************************************
187
188 Note [WorkList priorities]
189 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
190 A WorkList contains canonical and non-canonical items (of all flavors).
191 Notice that each Ct now has a simplification depth. We may
192 consider using this depth for prioritization as well in the future.
193
194 As a simple form of priority queue, our worklist separates out
195
196 * equalities (wl_eqs); see Note [Prioritise equalities]
197 * type-function equalities (wl_funeqs)
198 * all the rest (wl_rest)
199
200 Note [Prioritise equalities]
201 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
202 It's very important to process equalities /first/:
203
204 * (Efficiency) The general reason to do so is that if we process a
205 class constraint first, we may end up putting it into the inert set
206 and then kicking it out later. That's extra work compared to just
207 doing the equality first.
208
209 * (Avoiding fundep iteration) As Trac #14723 showed, it's possible to
210 get non-termination if we
211 - Emit the Derived fundep equalities for a class constraint,
212 generating some fresh unification variables.
213 - That leads to some unification
214 - Which kicks out the class constraint
215 - Which isn't solved (because there are still some more Derived
216 equalities in the work-list), but generates yet more fundeps
217 Solution: prioritise derived equalities over class constraints
218
219 * (Class equalities) We need to prioritise equalities even if they
220 are hidden inside a class constraint;
221 see Note [Prioritise class equalities]
222
223 * (Kick-out) We want to apply this priority scheme to kicked-out
224 constraints too (see the call to extendWorkListCt in kick_out_rewritable
225 E.g. a CIrredCan can be a hetero-kinded (t1 ~ t2), which may become
226 homo-kinded when kicked out, and hence we want to priotitise it.
227
228 * (Derived equalities) Originally we tried to postpone processing
229 Derived equalities, in the hope that we might never need to deal
230 with them at all; but in fact we must process Derived equalities
231 eagerly, partly for the (Efficiency) reason, and more importantly
232 for (Avoiding fundep iteration).
233
234 Note [Prioritise class equalities]
235 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
236 We prioritise equalities in the solver (see selectWorkItem). But class
237 constraints like (a ~ b) and (a ~~ b) are actually equalities too;
238 see Note [The equality types story] in TysPrim.
239
240 Failing to prioritise these is inefficient (more kick-outs etc).
241 But, worse, it can prevent us spotting a "recursive knot" among
242 Wanted constraints. See comment:10 of Trac #12734 for a worked-out
243 example.
244
245 So we arrange to put these particular class constraints in the wl_eqs.
246
247 NB: since we do not currently apply the substitution to the
248 inert_solved_dicts, the knot-tying still seems a bit fragile.
249 But this makes it better.
250 -}
251
252 -- See Note [WorkList priorities]
253 data WorkList
254 = WL { wl_eqs :: [Ct] -- CTyEqCan, CDictCan, CIrredCan
255 -- Given, Wanted, and Derived
256 -- Contains both equality constraints and their
257 -- class-level variants (a~b) and (a~~b);
258 -- See Note [Prioritise equalities]
259 -- See Note [Prioritise class equalities]
260
261 , wl_funeqs :: [Ct]
262
263 , wl_rest :: [Ct]
264
265 , wl_implics :: Bag Implication -- See Note [Residual implications]
266 }
267
268 appendWorkList :: WorkList -> WorkList -> WorkList
269 appendWorkList
270 (WL { wl_eqs = eqs1, wl_funeqs = funeqs1, wl_rest = rest1
271 , wl_implics = implics1 })
272 (WL { wl_eqs = eqs2, wl_funeqs = funeqs2, wl_rest = rest2
273 , wl_implics = implics2 })
274 = WL { wl_eqs = eqs1 ++ eqs2
275 , wl_funeqs = funeqs1 ++ funeqs2
276 , wl_rest = rest1 ++ rest2
277 , wl_implics = implics1 `unionBags` implics2 }
278
279 workListSize :: WorkList -> Int
280 workListSize (WL { wl_eqs = eqs, wl_funeqs = funeqs, wl_rest = rest })
281 = length eqs + length funeqs + length rest
282
283 workListWantedCount :: WorkList -> Int
284 -- Count the things we need to solve
285 -- excluding the insolubles (c.f. inert_count)
286 workListWantedCount (WL { wl_eqs = eqs, wl_rest = rest })
287 = count isWantedCt eqs + count is_wanted rest
288 where
289 is_wanted ct
290 | CIrredCan { cc_ev = ev, cc_insol = insol } <- ct
291 = not insol && isWanted ev
292 | otherwise
293 = isWantedCt ct
294
295 extendWorkListEq :: Ct -> WorkList -> WorkList
296 extendWorkListEq ct wl = wl { wl_eqs = ct : wl_eqs wl }
297
298 extendWorkListFunEq :: Ct -> WorkList -> WorkList
299 extendWorkListFunEq ct wl = wl { wl_funeqs = ct : wl_funeqs wl }
300
301 extendWorkListNonEq :: Ct -> WorkList -> WorkList
302 -- Extension by non equality
303 extendWorkListNonEq ct wl = wl { wl_rest = ct : wl_rest wl }
304
305 extendWorkListDeriveds :: [CtEvidence] -> WorkList -> WorkList
306 extendWorkListDeriveds evs wl
307 = extendWorkListCts (map mkNonCanonical evs) wl
308
309 extendWorkListImplic :: Bag Implication -> WorkList -> WorkList
310 extendWorkListImplic implics wl = wl { wl_implics = implics `unionBags` wl_implics wl }
311
312 extendWorkListCt :: Ct -> WorkList -> WorkList
313 -- Agnostic
314 extendWorkListCt ct wl
315 = case classifyPredType (ctPred ct) of
316 EqPred NomEq ty1 _
317 | Just tc <- tcTyConAppTyCon_maybe ty1
318 , isTypeFamilyTyCon tc
319 -> extendWorkListFunEq ct wl
320
321 EqPred {}
322 -> extendWorkListEq ct wl
323
324 ClassPred cls _ -- See Note [Prioritise class equalities]
325 | cls `hasKey` heqTyConKey
326 || cls `hasKey` eqTyConKey
327 -> extendWorkListEq ct wl
328
329 _ -> extendWorkListNonEq ct wl
330
331 extendWorkListCts :: [Ct] -> WorkList -> WorkList
332 -- Agnostic
333 extendWorkListCts cts wl = foldr extendWorkListCt wl cts
334
335 isEmptyWorkList :: WorkList -> Bool
336 isEmptyWorkList (WL { wl_eqs = eqs, wl_funeqs = funeqs
337 , wl_rest = rest, wl_implics = implics })
338 = null eqs && null rest && null funeqs && isEmptyBag implics
339
340 emptyWorkList :: WorkList
341 emptyWorkList = WL { wl_eqs = [], wl_rest = []
342 , wl_funeqs = [], wl_implics = emptyBag }
343
344 selectWorkItem :: WorkList -> Maybe (Ct, WorkList)
345 -- See Note [Prioritise equalities]
346 selectWorkItem wl@(WL { wl_eqs = eqs, wl_funeqs = feqs
347 , wl_rest = rest })
348 | ct:cts <- eqs = Just (ct, wl { wl_eqs = cts })
349 | ct:fes <- feqs = Just (ct, wl { wl_funeqs = fes })
350 | ct:cts <- rest = Just (ct, wl { wl_rest = cts })
351 | otherwise = Nothing
352
353 getWorkList :: TcS WorkList
354 getWorkList = do { wl_var <- getTcSWorkListRef
355 ; wrapTcS (TcM.readTcRef wl_var) }
356
357 selectNextWorkItem :: TcS (Maybe Ct)
358 -- Pick which work item to do next
359 -- See Note [Prioritise equalities]
360 selectNextWorkItem
361 = do { wl_var <- getTcSWorkListRef
362 ; wl <- wrapTcS (TcM.readTcRef wl_var)
363 ; case selectWorkItem wl of {
364 Nothing -> return Nothing ;
365 Just (ct, new_wl) ->
366 do { checkReductionDepth (ctLoc ct) (ctPred ct)
367 ; wrapTcS (TcM.writeTcRef wl_var new_wl)
368 ; return (Just ct) } } }
369
370 -- Pretty printing
371 instance Outputable WorkList where
372 ppr (WL { wl_eqs = eqs, wl_funeqs = feqs
373 , wl_rest = rest, wl_implics = implics })
374 = text "WL" <+> (braces $
375 vcat [ ppUnless (null eqs) $
376 text "Eqs =" <+> vcat (map ppr eqs)
377 , ppUnless (null feqs) $
378 text "Funeqs =" <+> vcat (map ppr feqs)
379 , ppUnless (null rest) $
380 text "Non-eqs =" <+> vcat (map ppr rest)
381 , ppUnless (isEmptyBag implics) $
382 ifPprDebug (text "Implics =" <+> vcat (map ppr (bagToList implics)))
383 (text "(Implics omitted)")
384 ])
385
386
387 {- *********************************************************************
388 * *
389 InertSet: the inert set
390 * *
391 * *
392 ********************************************************************* -}
393
394 data InertSet
395 = IS { inert_cans :: InertCans
396 -- Canonical Given, Wanted, Derived
397 -- Sometimes called "the inert set"
398
399 , inert_fsks :: [(TcTyVar, TcType)]
400 -- A list of (fsk, ty) pairs; we add one element when we flatten
401 -- a function application in a Given constraint, creating
402 -- a new fsk in newFlattenSkolem. When leaving a nested scope,
403 -- unflattenGivens unifies fsk := ty
404 --
405 -- We could also get this info from inert_funeqs, filtered by
406 -- level, but it seems simpler and more direct to capture the
407 -- fsk as we generate them.
408
409 , inert_flat_cache :: ExactFunEqMap (TcCoercion, TcType, CtFlavour)
410 -- See Note [Type family equations]
411 -- If F tys :-> (co, rhs, flav),
412 -- then co :: F tys ~ rhs
413 -- flav is [G] or [WD]
414 --
415 -- Just a hash-cons cache for use when flattening only
416 -- These include entirely un-processed goals, so don't use
417 -- them to solve a top-level goal, else you may end up solving
418 -- (w:F ty ~ a) by setting w:=w! We just use the flat-cache
419 -- when allocating a new flatten-skolem.
420 -- Not necessarily inert wrt top-level equations (or inert_cans)
421
422 -- NB: An ExactFunEqMap -- this doesn't match via loose types!
423
424 , inert_solved_dicts :: DictMap CtEvidence
425 -- All Wanteds, of form ev :: C t1 .. tn
426 -- See Note [Solved dictionaries]
427 -- and Note [Do not add superclasses of solved dictionaries]
428 }
429
430 instance Outputable InertSet where
431 ppr (IS { inert_cans = ics
432 , inert_fsks = ifsks
433 , inert_solved_dicts = solved_dicts })
434 = vcat [ ppr ics
435 , text "Inert fsks =" <+> ppr ifsks
436 , ppUnless (null dicts) $
437 text "Solved dicts =" <+> vcat (map ppr dicts) ]
438 where
439 dicts = bagToList (dictsToBag solved_dicts)
440
441 emptyInert :: InertSet
442 emptyInert
443 = IS { inert_cans = IC { inert_count = 0
444 , inert_eqs = emptyDVarEnv
445 , inert_dicts = emptyDicts
446 , inert_safehask = emptyDicts
447 , inert_funeqs = emptyFunEqs
448 , inert_irreds = emptyCts }
449 , inert_flat_cache = emptyExactFunEqs
450 , inert_fsks = []
451 , inert_solved_dicts = emptyDictMap }
452
453
454 {- Note [Solved dictionaries]
455 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
456 When we apply a top-level instance declaration, we add the "solved"
457 dictionary to the inert_solved_dicts. In general, we use it to avoid
458 creating a new EvVar when we have a new goal that we have solved in
459 the past.
460
461 But in particular, we can use it to create *recursive* dictionaries.
462 The simplest, degnerate case is
463 instance C [a] => C [a] where ...
464 If we have
465 [W] d1 :: C [x]
466 then we can apply the instance to get
467 d1 = $dfCList d
468 [W] d2 :: C [x]
469 Now 'd1' goes in inert_solved_dicts, and we can solve d2 directly from d1.
470 d1 = $dfCList d
471 d2 = d1
472
473 See Note [Example of recursive dictionaries]
474 Other notes about solved dictionaries
475
476 * See also Note [Do not add superclasses of solved dictionaries]
477
478 * The inert_solved_dicts field is not rewritten by equalities,
479 so it may get out of date.
480
481 * THe inert_solved_dicts are all Wanteds, never givens
482
483 Note [Do not add superclasses of solved dictionaries]
484 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
485 Every member of inert_solved_dicts is the result of applying a dictionary
486 function, NOT of applying superclass selection to anything.
487 Consider
488
489 class Ord a => C a where
490 instance Ord [a] => C [a] where ...
491
492 Suppose we are trying to solve
493 [G] d1 : Ord a
494 [W] d2 : C [a]
495
496 Then we'll use the instance decl to give
497
498 [G] d1 : Ord a Solved: d2 : C [a] = $dfCList d3
499 [W] d3 : Ord [a]
500
501 We must not add d4 : Ord [a] to the 'solved' set (by taking the
502 superclass of d2), otherwise we'll use it to solve d3, without ever
503 using d1, which would be a catastrophe.
504
505 Solution: when extending the solved dictionaries, do not add superclasses.
506 That's why each element of the inert_solved_dicts is the result of applying
507 a dictionary function.
508
509 Note [Example of recursive dictionaries]
510 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
511 --- Example 1
512
513 data D r = ZeroD | SuccD (r (D r));
514
515 instance (Eq (r (D r))) => Eq (D r) where
516 ZeroD == ZeroD = True
517 (SuccD a) == (SuccD b) = a == b
518 _ == _ = False;
519
520 equalDC :: D [] -> D [] -> Bool;
521 equalDC = (==);
522
523 We need to prove (Eq (D [])). Here's how we go:
524
525 [W] d1 : Eq (D [])
526 By instance decl of Eq (D r):
527 [W] d2 : Eq [D []] where d1 = dfEqD d2
528 By instance decl of Eq [a]:
529 [W] d3 : Eq (D []) where d2 = dfEqList d3
530 d1 = dfEqD d2
531 Now this wanted can interact with our "solved" d1 to get:
532 d3 = d1
533
534 -- Example 2:
535 This code arises in the context of "Scrap Your Boilerplate with Class"
536
537 class Sat a
538 class Data ctx a
539 instance Sat (ctx Char) => Data ctx Char -- dfunData1
540 instance (Sat (ctx [a]), Data ctx a) => Data ctx [a] -- dfunData2
541
542 class Data Maybe a => Foo a
543
544 instance Foo t => Sat (Maybe t) -- dfunSat
545
546 instance Data Maybe a => Foo a -- dfunFoo1
547 instance Foo a => Foo [a] -- dfunFoo2
548 instance Foo [Char] -- dfunFoo3
549
550 Consider generating the superclasses of the instance declaration
551 instance Foo a => Foo [a]
552
553 So our problem is this
554 [G] d0 : Foo t
555 [W] d1 : Data Maybe [t] -- Desired superclass
556
557 We may add the given in the inert set, along with its superclasses
558 Inert:
559 [G] d0 : Foo t
560 [G] d01 : Data Maybe t -- Superclass of d0
561 WorkList
562 [W] d1 : Data Maybe [t]
563
564 Solve d1 using instance dfunData2; d1 := dfunData2 d2 d3
565 Inert:
566 [G] d0 : Foo t
567 [G] d01 : Data Maybe t -- Superclass of d0
568 Solved:
569 d1 : Data Maybe [t]
570 WorkList:
571 [W] d2 : Sat (Maybe [t])
572 [W] d3 : Data Maybe t
573
574 Now, we may simplify d2 using dfunSat; d2 := dfunSat d4
575 Inert:
576 [G] d0 : Foo t
577 [G] d01 : Data Maybe t -- Superclass of d0
578 Solved:
579 d1 : Data Maybe [t]
580 d2 : Sat (Maybe [t])
581 WorkList:
582 [W] d3 : Data Maybe t
583 [W] d4 : Foo [t]
584
585 Now, we can just solve d3 from d01; d3 := d01
586 Inert
587 [G] d0 : Foo t
588 [G] d01 : Data Maybe t -- Superclass of d0
589 Solved:
590 d1 : Data Maybe [t]
591 d2 : Sat (Maybe [t])
592 WorkList
593 [W] d4 : Foo [t]
594
595 Now, solve d4 using dfunFoo2; d4 := dfunFoo2 d5
596 Inert
597 [G] d0 : Foo t
598 [G] d01 : Data Maybe t -- Superclass of d0
599 Solved:
600 d1 : Data Maybe [t]
601 d2 : Sat (Maybe [t])
602 d4 : Foo [t]
603 WorkList:
604 [W] d5 : Foo t
605
606 Now, d5 can be solved! d5 := d0
607
608 Result
609 d1 := dfunData2 d2 d3
610 d2 := dfunSat d4
611 d3 := d01
612 d4 := dfunFoo2 d5
613 d5 := d0
614 -}
615
616 {- *********************************************************************
617 * *
618 InertCans: the canonical inerts
619 * *
620 * *
621 ********************************************************************* -}
622
623 data InertCans -- See Note [Detailed InertCans Invariants] for more
624 = IC { inert_eqs :: InertEqs
625 -- See Note [inert_eqs: the inert equalities]
626 -- All CTyEqCans; index is the LHS tyvar
627 -- Domain = skolems and untouchables; a touchable would be unified
628
629 , inert_funeqs :: FunEqMap Ct
630 -- All CFunEqCans; index is the whole family head type.
631 -- All Nominal (that's an invarint of all CFunEqCans)
632 -- LHS is fully rewritten (modulo eqCanRewrite constraints)
633 -- wrt inert_eqs
634 -- Can include all flavours, [G], [W], [WD], [D]
635 -- See Note [Type family equations]
636
637 , inert_dicts :: DictMap Ct
638 -- Dictionaries only
639 -- All fully rewritten (modulo flavour constraints)
640 -- wrt inert_eqs
641
642 , inert_safehask :: DictMap Ct
643 -- Failed dictionary resolution due to Safe Haskell overlapping
644 -- instances restriction. We keep this separate from inert_dicts
645 -- as it doesn't cause compilation failure, just safe inference
646 -- failure.
647 --
648 -- ^ See Note [Safe Haskell Overlapping Instances Implementation]
649 -- in TcSimplify
650
651 , inert_irreds :: Cts
652 -- Irreducible predicates that cannot be made canonical,
653 -- and which don't interact with others (e.g. (c a))
654 -- and insoluble predicates (e.g. Int ~ Bool, or a ~ [a])
655
656 , inert_count :: Int
657 -- Number of Wanted goals in
658 -- inert_eqs, inert_dicts, inert_safehask, inert_irreds
659 -- Does not include insolubles
660 -- When non-zero, keep trying to solve
661 }
662
663 type InertEqs = DTyVarEnv EqualCtList
664 type EqualCtList = [Ct] -- See Note [EqualCtList invariants]
665
666 {- Note [Detailed InertCans Invariants]
667 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
668 The InertCans represents a collection of constraints with the following properties:
669
670 * All canonical
671
672 * No two dictionaries with the same head
673 * No two CIrreds with the same type
674
675 * Family equations inert wrt top-level family axioms
676
677 * Dictionaries have no matching top-level instance
678
679 * Given family or dictionary constraints don't mention touchable
680 unification variables
681
682 * Non-CTyEqCan constraints are fully rewritten with respect
683 to the CTyEqCan equalities (modulo canRewrite of course;
684 eg a wanted cannot rewrite a given)
685
686 * CTyEqCan equalities: see Note [Applying the inert substitution]
687 in TcFlatten
688
689 Note [EqualCtList invariants]
690 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
691 * All are equalities
692 * All these equalities have the same LHS
693 * The list is never empty
694 * No element of the list can rewrite any other
695 * Derived before Wanted
696
697 From the fourth invariant it follows that the list is
698 - A single [G], or
699 - Zero or one [D] or [WD], followd by any number of [W]
700
701 The Wanteds can't rewrite anything which is why we put them last
702
703 Note [Type family equations]
704 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
705 Type-family equations, CFunEqCans, of form (ev : F tys ~ ty),
706 live in three places
707
708 * The work-list, of course
709
710 * The inert_funeqs are un-solved but fully processed, and in
711 the InertCans. They can be [G], [W], [WD], or [D].
712
713 * The inert_flat_cache. This is used when flattening, to get maximal
714 sharing. Everthing in the inert_flat_cache is [G] or [WD]
715
716 It contains lots of things that are still in the work-list.
717 E.g Suppose we have (w1: F (G a) ~ Int), and (w2: H (G a) ~ Int) in the
718 work list. Then we flatten w1, dumping (w3: G a ~ f1) in the work
719 list. Now if we flatten w2 before we get to w3, we still want to
720 share that (G a).
721 Because it contains work-list things, DO NOT use the flat cache to solve
722 a top-level goal. Eg in the above example we don't want to solve w3
723 using w3 itself!
724
725 The CFunEqCan Ownership Invariant:
726
727 * Each [G/W/WD] CFunEqCan has a distinct fsk or fmv
728 It "owns" that fsk/fmv, in the sense that:
729 - reducing a [W/WD] CFunEqCan fills in the fmv
730 - unflattening a [W/WD] CFunEqCan fills in the fmv
731 (in both cases unless an occurs-check would result)
732
733 * In contrast a [D] CFunEqCan does not "own" its fmv:
734 - reducing a [D] CFunEqCan does not fill in the fmv;
735 it just generates an equality
736 - unflattening ignores [D] CFunEqCans altogether
737
738
739 Note [inert_eqs: the inert equalities]
740 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
741 Definition [Can-rewrite relation]
742 A "can-rewrite" relation between flavours, written f1 >= f2, is a
743 binary relation with the following properties
744
745 (R1) >= is transitive
746 (R2) If f1 >= f, and f2 >= f,
747 then either f1 >= f2 or f2 >= f1
748
749 Lemma. If f1 >= f then f1 >= f1
750 Proof. By property (R2), with f1=f2
751
752 Definition [Generalised substitution]
753 A "generalised substitution" S is a set of triples (a -f-> t), where
754 a is a type variable
755 t is a type
756 f is a flavour
757 such that
758 (WF1) if (a -f1-> t1) in S
759 (a -f2-> t2) in S
760 then neither (f1 >= f2) nor (f2 >= f1) hold
761 (WF2) if (a -f-> t) is in S, then t /= a
762
763 Definition [Applying a generalised substitution]
764 If S is a generalised substitution
765 S(f,a) = t, if (a -fs-> t) in S, and fs >= f
766 = a, otherwise
767 Application extends naturally to types S(f,t), modulo roles.
768 See Note [Flavours with roles].
769
770 Theorem: S(f,a) is well defined as a function.
771 Proof: Suppose (a -f1-> t1) and (a -f2-> t2) are both in S,
772 and f1 >= f and f2 >= f
773 Then by (R2) f1 >= f2 or f2 >= f1, which contradicts (WF1)
774
775 Notation: repeated application.
776 S^0(f,t) = t
777 S^(n+1)(f,t) = S(f, S^n(t))
778
779 Definition: inert generalised substitution
780 A generalised substitution S is "inert" iff
781
782 (IG1) there is an n such that
783 for every f,t, S^n(f,t) = S^(n+1)(f,t)
784
785 By (IG1) we define S*(f,t) to be the result of exahaustively
786 applying S(f,_) to t.
787
788 ----------------------------------------------------------------
789 Our main invariant:
790 the inert CTyEqCans should be an inert generalised substitution
791 ----------------------------------------------------------------
792
793 Note that inertness is not the same as idempotence. To apply S to a
794 type, you may have to apply it recursive. But inertness does
795 guarantee that this recursive use will terminate.
796
797 Note [Extending the inert equalities]
798 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
799 Main Theorem [Stability under extension]
800 Suppose we have a "work item"
801 a -fw-> t
802 and an inert generalised substitution S,
803 THEN the extended substitution T = S+(a -fw-> t)
804 is an inert generalised substitution
805 PROVIDED
806 (T1) S(fw,a) = a -- LHS of work-item is a fixpoint of S(fw,_)
807 (T2) S(fw,t) = t -- RHS of work-item is a fixpoint of S(fw,_)
808 (T3) a not in t -- No occurs check in the work item
809
810 AND, for every (b -fs-> s) in S:
811 (K0) not (fw >= fs)
812 Reason: suppose we kick out (a -fs-> s),
813 and add (a -fw-> t) to the inert set.
814 The latter can't rewrite the former,
815 so the kick-out achieved nothing
816
817 OR { (K1) not (a = b)
818 Reason: if fw >= fs, WF1 says we can't have both
819 a -fw-> t and a -fs-> s
820
821 AND (K2): guarantees inertness of the new substitution
822 { (K2a) not (fs >= fs)
823 OR (K2b) fs >= fw
824 OR (K2d) a not in s }
825
826 AND (K3) See Note [K3: completeness of solving]
827 { (K3a) If the role of fs is nominal: s /= a
828 (K3b) If the role of fs is representational:
829 s is not of form (a t1 .. tn) } }
830
831
832 Conditions (T1-T3) are established by the canonicaliser
833 Conditions (K1-K3) are established by TcSMonad.kickOutRewritable
834
835 The idea is that
836 * (T1-2) are guaranteed by exhaustively rewriting the work-item
837 with S(fw,_).
838
839 * T3 is guaranteed by a simple occurs-check on the work item.
840 This is done during canonicalisation, in canEqTyVar;
841 (invariant: a CTyEqCan never has an occurs check).
842
843 * (K1-3) are the "kick-out" criteria. (As stated, they are really the
844 "keep" criteria.) If the current inert S contains a triple that does
845 not satisfy (K1-3), then we remove it from S by "kicking it out",
846 and re-processing it.
847
848 * Note that kicking out is a Bad Thing, because it means we have to
849 re-process a constraint. The less we kick out, the better.
850 TODO: Make sure that kicking out really *is* a Bad Thing. We've assumed
851 this but haven't done the empirical study to check.
852
853 * Assume we have G>=G, G>=W and that's all. Then, when performing
854 a unification we add a new given a -G-> ty. But doing so does NOT require
855 us to kick out an inert wanted that mentions a, because of (K2a). This
856 is a common case, hence good not to kick out.
857
858 * Lemma (L2): if not (fw >= fw), then K0 holds and we kick out nothing
859 Proof: using Definition [Can-rewrite relation], fw can't rewrite anything
860 and so K0 holds. Intuitively, since fw can't rewrite anything,
861 adding it cannot cause any loops
862 This is a common case, because Wanteds cannot rewrite Wanteds.
863 It's used to avoid even looking for constraint to kick out.
864
865 * Lemma (L1): The conditions of the Main Theorem imply that there is no
866 (a -fs-> t) in S, s.t. (fs >= fw).
867 Proof. Suppose the contrary (fs >= fw). Then because of (T1),
868 S(fw,a)=a. But since fs>=fw, S(fw,a) = s, hence s=a. But now we
869 have (a -fs-> a) in S, which contradicts (WF2).
870
871 * The extended substitution satisfies (WF1) and (WF2)
872 - (K1) plus (L1) guarantee that the extended substitution satisfies (WF1).
873 - (T3) guarantees (WF2).
874
875 * (K2) is about inertness. Intuitively, any infinite chain T^0(f,t),
876 T^1(f,t), T^2(f,T).... must pass through the new work item infinitely
877 often, since the substitution without the work item is inert; and must
878 pass through at least one of the triples in S infinitely often.
879
880 - (K2a): if not(fs>=fs) then there is no f that fs can rewrite (fs>=f),
881 and hence this triple never plays a role in application S(f,a).
882 It is always safe to extend S with such a triple.
883
884 (NB: we could strengten K1) in this way too, but see K3.
885
886 - (K2b): If this holds then, by (T2), b is not in t. So applying the
887 work item does not generate any new opportunities for applying S
888
889 - (K2c): If this holds, we can't pass through this triple infinitely
890 often, because if we did then fs>=f, fw>=f, hence by (R2)
891 * either fw>=fs, contradicting K2c
892 * or fs>=fw; so by the argument in K2b we can't have a loop
893
894 - (K2d): if a not in s, we hae no further opportunity to apply the
895 work item, similar to (K2b)
896
897 NB: Dimitrios has a PDF that does this in more detail
898
899 Key lemma to make it watertight.
900 Under the conditions of the Main Theorem,
901 forall f st fw >= f, a is not in S^k(f,t), for any k
902
903 Also, consider roles more carefully. See Note [Flavours with roles]
904
905 Note [K3: completeness of solving]
906 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
907 (K3) is not necessary for the extended substitution
908 to be inert. In fact K1 could be made stronger by saying
909 ... then (not (fw >= fs) or not (fs >= fs))
910 But it's not enough for S to be inert; we also want completeness.
911 That is, we want to be able to solve all soluble wanted equalities.
912 Suppose we have
913
914 work-item b -G-> a
915 inert-item a -W-> b
916
917 Assuming (G >= W) but not (W >= W), this fulfills all the conditions,
918 so we could extend the inerts, thus:
919
920 inert-items b -G-> a
921 a -W-> b
922
923 But if we kicked-out the inert item, we'd get
924
925 work-item a -W-> b
926 inert-item b -G-> a
927
928 Then rewrite the work-item gives us (a -W-> a), which is soluble via Refl.
929 So we add one more clause to the kick-out criteria
930
931 Another way to understand (K3) is that we treat an inert item
932 a -f-> b
933 in the same way as
934 b -f-> a
935 So if we kick out one, we should kick out the other. The orientation
936 is somewhat accidental.
937
938 When considering roles, we also need the second clause (K3b). Consider
939
940 work-item c -G/N-> a
941 inert-item a -W/R-> b c
942
943 The work-item doesn't get rewritten by the inert, because (>=) doesn't hold.
944 But we don't kick out the inert item because not (W/R >= W/R). So we just
945 add the work item. But then, consider if we hit the following:
946
947 work-item b -G/N-> Id
948 inert-items a -W/R-> b c
949 c -G/N-> a
950 where
951 newtype Id x = Id x
952
953 For similar reasons, if we only had (K3a), we wouldn't kick the
954 representational inert out. And then, we'd miss solving the inert, which
955 now reduced to reflexivity.
956
957 The solution here is to kick out representational inerts whenever the
958 tyvar of a work item is "exposed", where exposed means being at the
959 head of the top-level application chain (a t1 .. tn). See
960 TcType.isTyVarHead. This is encoded in (K3b).
961
962 Beware: if we make this test succeed too often, we kick out too much,
963 and the solver might loop. Consider (Trac #14363)
964 work item: [G] a ~R f b
965 inert item: [G] b ~R f a
966 In GHC 8.2 the completeness tests more aggressive, and kicked out
967 the inert item; but no rewriting happened and there was an infinite
968 loop. All we need is to have the tyvar at the head.
969
970 Note [Flavours with roles]
971 ~~~~~~~~~~~~~~~~~~~~~~~~~~
972 The system described in Note [inert_eqs: the inert equalities]
973 discusses an abstract
974 set of flavours. In GHC, flavours have two components: the flavour proper,
975 taken from {Wanted, Derived, Given} and the equality relation (often called
976 role), taken from {NomEq, ReprEq}.
977 When substituting w.r.t. the inert set,
978 as described in Note [inert_eqs: the inert equalities],
979 we must be careful to respect all components of a flavour.
980 For example, if we have
981
982 inert set: a -G/R-> Int
983 b -G/R-> Bool
984
985 type role T nominal representational
986
987 and we wish to compute S(W/R, T a b), the correct answer is T a Bool, NOT
988 T Int Bool. The reason is that T's first parameter has a nominal role, and
989 thus rewriting a to Int in T a b is wrong. Indeed, this non-congruence of
990 substitution means that the proof in Note [The inert equalities] may need
991 to be revisited, but we don't think that the end conclusion is wrong.
992 -}
993
994 instance Outputable InertCans where
995 ppr (IC { inert_eqs = eqs
996 , inert_funeqs = funeqs, inert_dicts = dicts
997 , inert_safehask = safehask, inert_irreds = irreds
998 , inert_count = count })
999 = braces $ vcat
1000 [ ppUnless (isEmptyDVarEnv eqs) $
1001 text "Equalities:"
1002 <+> pprCts (foldDVarEnv (\eqs rest -> listToBag eqs `andCts` rest) emptyCts eqs)
1003 , ppUnless (isEmptyTcAppMap funeqs) $
1004 text "Type-function equalities =" <+> pprCts (funEqsToBag funeqs)
1005 , ppUnless (isEmptyTcAppMap dicts) $
1006 text "Dictionaries =" <+> pprCts (dictsToBag dicts)
1007 , ppUnless (isEmptyTcAppMap safehask) $
1008 text "Safe Haskell unsafe overlap =" <+> pprCts (dictsToBag safehask)
1009 , ppUnless (isEmptyCts irreds) $
1010 text "Irreds =" <+> pprCts irreds
1011 , text "Unsolved goals =" <+> int count
1012 ]
1013
1014 {- *********************************************************************
1015 * *
1016 Shadow constraints and improvement
1017 * *
1018 ************************************************************************
1019
1020 Note [The improvement story and derived shadows]
1021 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1022 Because Wanteds cannot rewrite Wanteds (see Note [Wanteds do not
1023 rewrite Wanteds] in TcRnTypes), we may miss some opportunities for
1024 solving. Here's a classic example (indexed-types/should_fail/T4093a)
1025
1026 Ambiguity check for f: (Foo e ~ Maybe e) => Foo e
1027
1028 We get [G] Foo e ~ Maybe e
1029 [W] Foo e ~ Foo ee -- ee is a unification variable
1030 [W] Foo ee ~ Maybe ee
1031
1032 Flatten: [G] Foo e ~ fsk
1033 [G] fsk ~ Maybe e -- (A)
1034
1035 [W] Foo ee ~ fmv
1036 [W] fmv ~ fsk -- (B) From Foo e ~ Foo ee
1037 [W] fmv ~ Maybe ee
1038
1039 --> rewrite (B) with (A)
1040 [W] Foo ee ~ fmv
1041 [W] fmv ~ Maybe e
1042 [W] fmv ~ Maybe ee
1043
1044 But now we appear to be stuck, since we don't rewrite Wanteds with
1045 Wanteds. This is silly because we can see that ee := e is the
1046 only solution.
1047
1048 The basic plan is
1049 * generate Derived constraints that shadow Wanted constraints
1050 * allow Derived to rewrite Derived
1051 * in order to cause some unifications to take place
1052 * that in turn solve the original Wanteds
1053
1054 The ONLY reason for all these Derived equalities is to tell us how to
1055 unify a variable: that is, what Mark Jones calls "improvement".
1056
1057 The same idea is sometimes also called "saturation"; find all the
1058 equalities that must hold in any solution.
1059
1060 Or, equivalently, you can think of the derived shadows as implementing
1061 the "model": a non-idempotent but no-occurs-check substitution,
1062 reflecting *all* *Nominal* equalities (a ~N ty) that are not
1063 immediately soluble by unification.
1064
1065 More specifically, here's how it works (Oct 16):
1066
1067 * Wanted constraints are born as [WD]; this behaves like a
1068 [W] and a [D] paired together.
1069
1070 * When we are about to add a [WD] to the inert set, if it can
1071 be rewritten by a [D] a ~ ty, then we split it into [W] and [D],
1072 putting the latter into the work list (see maybeEmitShadow).
1073
1074 In the example above, we get to the point where we are stuck:
1075 [WD] Foo ee ~ fmv
1076 [WD] fmv ~ Maybe e
1077 [WD] fmv ~ Maybe ee
1078
1079 But now when [WD] fmv ~ Maybe ee is about to be added, we'll
1080 split it into [W] and [D], since the inert [WD] fmv ~ Maybe e
1081 can rewrite it. Then:
1082 work item: [D] fmv ~ Maybe ee
1083 inert: [W] fmv ~ Maybe ee
1084 [WD] fmv ~ Maybe e -- (C)
1085 [WD] Foo ee ~ fmv
1086
1087 See Note [Splitting WD constraints]. Now the work item is rewritten
1088 by (C) and we soon get ee := e.
1089
1090 Additional notes:
1091
1092 * The derived shadow equalities live in inert_eqs, along with
1093 the Givens and Wanteds; see Note [EqualCtList invariants].
1094
1095 * We make Derived shadows only for Wanteds, not Givens. So we
1096 have only [G], not [GD] and [G] plus splitting. See
1097 Note [Add derived shadows only for Wanteds]
1098
1099 * We also get Derived equalities from functional dependencies
1100 and type-function injectivity; see calls to unifyDerived.
1101
1102 * This splitting business applies to CFunEqCans too; and then
1103 we do apply type-function reductions to the [D] CFunEqCan.
1104 See Note [Reduction for Derived CFunEqCans]
1105
1106 * It's worth having [WD] rather than just [W] and [D] because
1107 * efficiency: silly to process the same thing twice
1108 * inert_funeqs, inert_dicts is a finite map keyed by
1109 the type; it's inconvenient for it to map to TWO constraints
1110
1111 Note [Splitting WD constraints]
1112 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1113 We are about to add a [WD] constraint to the inert set; and we
1114 know that the inert set has fully rewritten it. Should we split
1115 it into [W] and [D], and put the [D] in the work list for further
1116 work?
1117
1118 * CDictCan (C tys) or CFunEqCan (F tys ~ fsk):
1119 Yes if the inert set could rewrite tys to make the class constraint,
1120 or type family, fire. That is, yes if the inert_eqs intersects
1121 with the free vars of tys. For this test we use
1122 (anyRewritableTyVar True) which ignores casts and coercions in tys,
1123 because rewriting the casts or coercions won't make the thing fire
1124 more often.
1125
1126 * CTyEqCan (a ~ ty): Yes if the inert set could rewrite 'a' or 'ty'.
1127 We need to check both 'a' and 'ty' against the inert set:
1128 - Inert set contains [D] a ~ ty2
1129 Then we want to put [D] a ~ ty in the worklist, so we'll
1130 get [D] ty ~ ty2 with consequent good things
1131
1132 - Inert set contains [D] b ~ a, where b is in ty.
1133 We can't just add [WD] a ~ ty[b] to the inert set, because
1134 that breaks the inert-set invariants. If we tried to
1135 canonicalise another [D] constraint mentioning 'a', we'd
1136 get an infinite loop
1137
1138 Moreover we must use (anyRewritableTyVar False) for the RHS,
1139 because even tyvars in the casts and coercions could give
1140 an infinite loop if we don't expose it
1141
1142 * CIrredCan: Yes if the inert set can rewrite the constraint.
1143 We used to think splitting irreds was unnecessary, but
1144 see Note [Splitting Irred WD constraints]
1145
1146 * Others: nothing is gained by splitting.
1147
1148 Note [Splitting Irred WD constraints]
1149 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1150 Splitting Irred constraints can make a difference. Here is the
1151 scenario:
1152
1153 a[sk] :: F v -- F is a type family
1154 beta :: alpha
1155
1156 work item: [WD] a ~ beta
1157
1158 This is heterogeneous, so we try flattening the kinds.
1159
1160 co :: F v ~ fmv
1161 [WD] (a |> co) ~ beta
1162
1163 This is still hetero, so we emit a kind equality and make the work item an
1164 inert Irred.
1165
1166 work item: [D] fmv ~ alpha
1167 inert: [WD] (a |> co) ~ beta (CIrredCan)
1168
1169 Can't make progress on the work item. Add to inert set. This kicks out the
1170 old inert, because a [D] can rewrite a [WD].
1171
1172 work item: [WD] (a |> co) ~ beta
1173 inert: [D] fmv ~ alpha (CTyEqCan)
1174
1175 Can't make progress on this work item either (although GHC tries by
1176 decomposing the cast and reflattening... but that doesn't make a difference),
1177 which is still hetero. Emit a new kind equality and add to inert set. But,
1178 critically, we split the Irred.
1179
1180 work list:
1181 [D] fmv ~ alpha (CTyEqCan)
1182 [D] (a |> co) ~ beta (CIrred) -- this one was split off
1183 inert:
1184 [W] (a |> co) ~ beta
1185 [D] fmv ~ alpha
1186
1187 We quickly solve the first work item, as it's the same as an inert.
1188
1189 work item: [D] (a |> co) ~ beta
1190 inert:
1191 [W] (a |> co) ~ beta
1192 [D] fmv ~ alpha
1193
1194 We decompose the cast, yielding
1195
1196 [D] a ~ beta
1197
1198 We then flatten the kinds. The lhs kind is F v, which flattens to fmv which
1199 then rewrites to alpha.
1200
1201 co' :: F v ~ alpha
1202 [D] (a |> co') ~ beta
1203
1204 Now this equality is homo-kinded. So we swizzle it around to
1205
1206 [D] beta ~ (a |> co')
1207
1208 and set beta := a |> co', and go home happy.
1209
1210 If we don't split the Irreds, we loop. This is all dangerously subtle.
1211
1212 This is triggered by test case typecheck/should_compile/SplitWD.
1213
1214 Note [Examples of how Derived shadows helps completeness]
1215 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1216 Trac #10009, a very nasty example:
1217
1218 f :: (UnF (F b) ~ b) => F b -> ()
1219
1220 g :: forall a. (UnF (F a) ~ a) => a -> ()
1221 g _ = f (undefined :: F a)
1222
1223 For g we get [G] UnF (F a) ~ a
1224 [WD] UnF (F beta) ~ beta
1225 [WD] F a ~ F beta
1226 Flatten:
1227 [G] g1: F a ~ fsk1 fsk1 := F a
1228 [G] g2: UnF fsk1 ~ fsk2 fsk2 := UnF fsk1
1229 [G] g3: fsk2 ~ a
1230
1231 [WD] w1: F beta ~ fmv1
1232 [WD] w2: UnF fmv1 ~ fmv2
1233 [WD] w3: fmv2 ~ beta
1234 [WD] w4: fmv1 ~ fsk1 -- From F a ~ F beta using flat-cache
1235 -- and re-orient to put meta-var on left
1236
1237 Rewrite w2 with w4: [D] d1: UnF fsk1 ~ fmv2
1238 React that with g2: [D] d2: fmv2 ~ fsk2
1239 React that with w3: [D] beta ~ fsk2
1240 and g3: [D] beta ~ a -- Hooray beta := a
1241 And that is enough to solve everything
1242
1243 Note [Add derived shadows only for Wanteds]
1244 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1245 We only add shadows for Wanted constraints. That is, we have
1246 [WD] but not [GD]; and maybeEmitShaodw looks only at [WD]
1247 constraints.
1248
1249 It does just possibly make sense ot add a derived shadow for a
1250 Given. If we created a Derived shadow of a Given, it could be
1251 rewritten by other Deriveds, and that could, conceivably, lead to a
1252 useful unification.
1253
1254 But (a) I have been unable to come up with an example of this
1255 happening
1256 (b) see Trac #12660 for how adding the derived shadows
1257 of a Given led to an infinite loop.
1258 (c) It's unlikely that rewriting derived Givens will lead
1259 to a unification because Givens don't mention touchable
1260 unification variables
1261
1262 For (b) there may be other ways to solve the loop, but simply
1263 reraining from adding derived shadows of Givens is particularly
1264 simple. And it's more efficient too!
1265
1266 Still, here's one possible reason for adding derived shadows
1267 for Givens. Consider
1268 work-item [G] a ~ [b], inerts has [D] b ~ a.
1269 If we added the derived shadow (into the work list)
1270 [D] a ~ [b]
1271 When we process it, we'll rewrite to a ~ [a] and get an
1272 occurs check. Without it we'll miss the occurs check (reporting
1273 inaccessible code); but that's probably OK.
1274
1275 Note [Keep CDictCan shadows as CDictCan]
1276 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1277 Suppose we have
1278 class C a => D a b
1279 and [G] D a b, [G] C a in the inert set. Now we insert
1280 [D] b ~ c. We want to kick out a derived shadow for [D] D a b,
1281 so we can rewrite it with the new constraint, and perhaps get
1282 instance reduction or other consequences.
1283
1284 BUT we do not want to kick out a *non-canonical* (D a b). If we
1285 did, we would do this:
1286 - rewrite it to [D] D a c, with pend_sc = True
1287 - use expandSuperClasses to add C a
1288 - go round again, which solves C a from the givens
1289 This loop goes on for ever and triggers the simpl_loop limit.
1290
1291 Solution: kick out the CDictCan which will have pend_sc = False,
1292 because we've already added its superclasses. So we won't re-add
1293 them. If we forget the pend_sc flag, our cunning scheme for avoiding
1294 generating superclasses repeatedly will fail.
1295
1296 See Trac #11379 for a case of this.
1297
1298 Note [Do not do improvement for WOnly]
1299 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1300 We do improvement between two constraints (e.g. for injectivity
1301 or functional dependencies) only if both are "improvable". And
1302 we improve a constraint wrt the top-level instances only if
1303 it is improvable.
1304
1305 Improvable: [G] [WD] [D}
1306 Not improvable: [W]
1307
1308 Reasons:
1309
1310 * It's less work: fewer pairs to compare
1311
1312 * Every [W] has a shadow [D] so nothing is lost
1313
1314 * Consider [WD] C Int b, where 'b' is a skolem, and
1315 class C a b | a -> b
1316 instance C Int Bool
1317 We'll do a fundep on it and emit [D] b ~ Bool
1318 That will kick out constraint [WD] C Int b
1319 Then we'll split it to [W] C Int b (keep in inert)
1320 and [D] C Int b (in work list)
1321 When processing the latter we'll rewrite it to
1322 [D] C Int Bool
1323 At that point it would be /stupid/ to interact it
1324 with the inert [W] C Int b in the inert set; after all,
1325 it's the very constraint from which the [D] C Int Bool
1326 was split! We can avoid this by not doing improvement
1327 on [W] constraints. This came up in Trac #12860.
1328 -}
1329
1330 maybeEmitShadow :: InertCans -> Ct -> TcS Ct
1331 -- See Note [The improvement story and derived shadows]
1332 maybeEmitShadow ics ct
1333 | let ev = ctEvidence ct
1334 , CtWanted { ctev_pred = pred, ctev_loc = loc
1335 , ctev_nosh = WDeriv } <- ev
1336 , shouldSplitWD (inert_eqs ics) ct
1337 = do { traceTcS "Emit derived shadow" (ppr ct)
1338 ; let derived_ev = CtDerived { ctev_pred = pred
1339 , ctev_loc = loc }
1340 shadow_ct = ct { cc_ev = derived_ev }
1341 -- Te shadow constraint keeps the canonical shape.
1342 -- This just saves work, but is sometimes important;
1343 -- see Note [Keep CDictCan shadows as CDictCan]
1344 ; emitWork [shadow_ct]
1345
1346 ; let ev' = ev { ctev_nosh = WOnly }
1347 ct' = ct { cc_ev = ev' }
1348 -- Record that it now has a shadow
1349 -- This is /the/ place we set the flag to WOnly
1350 ; return ct' }
1351
1352 | otherwise
1353 = return ct
1354
1355 shouldSplitWD :: InertEqs -> Ct -> Bool
1356 -- Precondition: 'ct' is [WD], and is inert
1357 -- True <=> we should split ct ito [W] and [D] because
1358 -- the inert_eqs can make progress on the [D]
1359 -- See Note [Splitting WD constraints]
1360
1361 shouldSplitWD inert_eqs (CFunEqCan { cc_tyargs = tys })
1362 = should_split_match_args inert_eqs tys
1363 -- We don't need to split if the tv is the RHS fsk
1364
1365 shouldSplitWD inert_eqs (CDictCan { cc_tyargs = tys })
1366 = should_split_match_args inert_eqs tys
1367 -- NB True: ignore coercions
1368 -- See Note [Splitting WD constraints]
1369
1370 shouldSplitWD inert_eqs (CTyEqCan { cc_tyvar = tv, cc_rhs = ty
1371 , cc_eq_rel = eq_rel })
1372 = tv `elemDVarEnv` inert_eqs
1373 || anyRewritableTyVar False eq_rel (canRewriteTv inert_eqs) ty
1374 -- NB False: do not ignore casts and coercions
1375 -- See Note [Splitting WD constraints]
1376
1377 shouldSplitWD inert_eqs (CIrredCan { cc_ev = ev })
1378 = anyRewritableTyVar False (ctEvEqRel ev) (canRewriteTv inert_eqs) (ctEvPred ev)
1379
1380 shouldSplitWD _ _ = False -- No point in splitting otherwise
1381
1382 should_split_match_args :: InertEqs -> [TcType] -> Bool
1383 -- True if the inert_eqs can rewrite anything in the argument
1384 -- types, ignoring casts and coercions
1385 should_split_match_args inert_eqs tys
1386 = any (anyRewritableTyVar True NomEq (canRewriteTv inert_eqs)) tys
1387 -- NB True: ignore casts coercions
1388 -- See Note [Splitting WD constraints]
1389
1390 canRewriteTv :: InertEqs -> EqRel -> TyVar -> Bool
1391 canRewriteTv inert_eqs eq_rel tv
1392 | Just (ct : _) <- lookupDVarEnv inert_eqs tv
1393 , CTyEqCan { cc_eq_rel = eq_rel1 } <- ct
1394 = eq_rel1 `eqCanRewrite` eq_rel
1395 | otherwise
1396 = False
1397
1398 isImprovable :: CtEvidence -> Bool
1399 -- See Note [Do not do improvement for WOnly]
1400 isImprovable (CtWanted { ctev_nosh = WOnly }) = False
1401 isImprovable _ = True
1402
1403
1404 {- *********************************************************************
1405 * *
1406 Inert equalities
1407 * *
1408 ********************************************************************* -}
1409
1410 addTyEq :: InertEqs -> TcTyVar -> Ct -> InertEqs
1411 addTyEq old_eqs tv ct
1412 = extendDVarEnv_C add_eq old_eqs tv [ct]
1413 where
1414 add_eq old_eqs _
1415 | isWantedCt ct
1416 , (eq1 : eqs) <- old_eqs
1417 = eq1 : ct : eqs
1418 | otherwise
1419 = ct : old_eqs
1420
1421 foldTyEqs :: (Ct -> b -> b) -> InertEqs -> b -> b
1422 foldTyEqs k eqs z
1423 = foldDVarEnv (\cts z -> foldr k z cts) z eqs
1424
1425 findTyEqs :: InertCans -> TyVar -> EqualCtList
1426 findTyEqs icans tv = lookupDVarEnv (inert_eqs icans) tv `orElse` []
1427
1428 delTyEq :: InertEqs -> TcTyVar -> TcType -> InertEqs
1429 delTyEq m tv t = modifyDVarEnv (filter (not . isThisOne)) m tv
1430 where isThisOne (CTyEqCan { cc_rhs = t1 }) = eqType t t1
1431 isThisOne _ = False
1432
1433 lookupInertTyVar :: InertEqs -> TcTyVar -> Maybe TcType
1434 lookupInertTyVar ieqs tv
1435 = case lookupDVarEnv ieqs tv of
1436 Just (CTyEqCan { cc_rhs = rhs, cc_eq_rel = NomEq } : _ ) -> Just rhs
1437 _ -> Nothing
1438
1439 lookupFlattenTyVar :: InertEqs -> TcTyVar -> TcType
1440 -- See Note [lookupFlattenTyVar]
1441 lookupFlattenTyVar ieqs ftv
1442 = lookupInertTyVar ieqs ftv `orElse` mkTyVarTy ftv
1443
1444 {- Note [lookupFlattenTyVar]
1445 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1446 Suppose we have an injective function F and
1447 inert_funeqs: F t1 ~ fsk1
1448 F t2 ~ fsk2
1449 inert_eqs: fsk1 ~ fsk2
1450
1451 We never rewrite the RHS (cc_fsk) of a CFunEqCan. But we /do/ want to
1452 get the [D] t1 ~ t2 from the injectiveness of F. So we look up the
1453 cc_fsk of CFunEqCans in the inert_eqs when trying to find derived
1454 equalities arising from injectivity.
1455 -}
1456
1457
1458 {- *********************************************************************
1459 * *
1460 Adding an inert
1461 * *
1462 ************************************************************************
1463
1464 Note [Adding an equality to the InertCans]
1465 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1466 When adding an equality to the inerts:
1467
1468 * Split [WD] into [W] and [D] if the inerts can rewrite the latter;
1469 done by maybeEmitShadow.
1470
1471 * Kick out any constraints that can be rewritten by the thing
1472 we are adding. Done by kickOutRewritable.
1473
1474 * Note that unifying a:=ty, is like adding [G] a~ty; just use
1475 kickOutRewritable with Nominal, Given. See kickOutAfterUnification.
1476
1477 Note [Kicking out CFunEqCan for fundeps]
1478 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1479 Consider:
1480 New: [D] fmv1 ~ fmv2
1481 Inert: [W] F alpha ~ fmv1
1482 [W] F beta ~ fmv2
1483
1484 where F is injective. The new (derived) equality certainly can't
1485 rewrite the inerts. But we *must* kick out the first one, to get:
1486
1487 New: [W] F alpha ~ fmv1
1488 Inert: [W] F beta ~ fmv2
1489 [D] fmv1 ~ fmv2
1490
1491 and now improvement will discover [D] alpha ~ beta. This is important;
1492 eg in Trac #9587.
1493
1494 So in kickOutRewritable we look at all the tyvars of the
1495 CFunEqCan, including the fsk.
1496 -}
1497
1498 addInertEq :: Ct -> TcS ()
1499 -- This is a key function, because of the kick-out stuff
1500 -- Precondition: item /is/ canonical
1501 -- See Note [Adding an equality to the InertCans]
1502 addInertEq ct
1503 = do { traceTcS "addInertEq {" $
1504 text "Adding new inert equality:" <+> ppr ct
1505
1506 ; ics <- getInertCans
1507
1508 ; ct@(CTyEqCan { cc_tyvar = tv, cc_ev = ev, cc_eq_rel = eq_rel })
1509 <- maybeEmitShadow ics ct
1510
1511 ; (_, ics1) <- kickOutRewritable (ctEvFlavour ev, eq_rel) tv ics
1512
1513 ; let ics2 = ics1 { inert_eqs = addTyEq (inert_eqs ics1) tv ct
1514 , inert_count = bumpUnsolvedCount ev (inert_count ics1) }
1515 ; setInertCans ics2
1516
1517 ; traceTcS "addInertEq }" $ empty }
1518
1519 --------------
1520 addInertCan :: Ct -> TcS () -- Constraints *other than* equalities
1521 addInertCan ct
1522 = do { traceTcS "insertInertCan {" $
1523 text "Trying to insert new non-eq inert item:" <+> ppr ct
1524
1525 ; ics <- getInertCans
1526 ; ct <- maybeEmitShadow ics ct
1527 ; setInertCans (add_item ics ct)
1528
1529 ; traceTcS "addInertCan }" $ empty }
1530
1531 add_item :: InertCans -> Ct -> InertCans
1532 add_item ics item@(CFunEqCan { cc_fun = tc, cc_tyargs = tys })
1533 = ics { inert_funeqs = insertFunEq (inert_funeqs ics) tc tys item }
1534
1535 add_item ics@(IC { inert_irreds = irreds, inert_count = count })
1536 item@(CIrredCan { cc_ev = ev, cc_insol = insoluble })
1537 = ics { inert_irreds = irreds `Bag.snocBag` item
1538 , inert_count = if insoluble
1539 then count -- inert_count does not include insolubles
1540 else bumpUnsolvedCount ev count }
1541
1542 add_item ics item@(CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys })
1543 = ics { inert_dicts = addDict (inert_dicts ics) cls tys item
1544 , inert_count = bumpUnsolvedCount ev (inert_count ics) }
1545
1546 add_item _ item
1547 = pprPanic "upd_inert set: can't happen! Inserting " $
1548 ppr item -- CTyEqCan is dealt with by addInertEq
1549 -- Can't be CNonCanonical, CHoleCan,
1550 -- because they only land in inert_irreds
1551
1552 bumpUnsolvedCount :: CtEvidence -> Int -> Int
1553 bumpUnsolvedCount ev n | isWanted ev = n+1
1554 | otherwise = n
1555
1556
1557 -----------------------------------------
1558 kickOutRewritable :: CtFlavourRole -- Flavour/role of the equality that
1559 -- is being added to the inert set
1560 -> TcTyVar -- The new equality is tv ~ ty
1561 -> InertCans
1562 -> TcS (Int, InertCans)
1563 kickOutRewritable new_fr new_tv ics
1564 = do { let (kicked_out, ics') = kick_out_rewritable new_fr new_tv ics
1565 n_kicked = workListSize kicked_out
1566
1567 ; unless (n_kicked == 0) $
1568 do { updWorkListTcS (appendWorkList kicked_out)
1569 ; csTraceTcS $
1570 hang (text "Kick out, tv =" <+> ppr new_tv)
1571 2 (vcat [ text "n-kicked =" <+> int n_kicked
1572 , text "kicked_out =" <+> ppr kicked_out
1573 , text "Residual inerts =" <+> ppr ics' ]) }
1574
1575 ; return (n_kicked, ics') }
1576
1577 kick_out_rewritable :: CtFlavourRole -- Flavour/role of the equality that
1578 -- is being added to the inert set
1579 -> TcTyVar -- The new equality is tv ~ ty
1580 -> InertCans
1581 -> (WorkList, InertCans)
1582 -- See Note [kickOutRewritable]
1583 kick_out_rewritable new_fr new_tv ics@(IC { inert_eqs = tv_eqs
1584 , inert_dicts = dictmap
1585 , inert_safehask = safehask
1586 , inert_funeqs = funeqmap
1587 , inert_irreds = irreds
1588 , inert_count = n })
1589 | not (new_fr `eqMayRewriteFR` new_fr)
1590 = (emptyWorkList, ics)
1591 -- If new_fr can't rewrite itself, it can't rewrite
1592 -- anything else, so no need to kick out anything.
1593 -- (This is a common case: wanteds can't rewrite wanteds)
1594 -- Lemma (L2) in Note [Extending the inert equalities]
1595
1596 | otherwise
1597 = (kicked_out, inert_cans_in)
1598 where
1599 inert_cans_in = IC { inert_eqs = tv_eqs_in
1600 , inert_dicts = dicts_in
1601 , inert_safehask = safehask -- ??
1602 , inert_funeqs = feqs_in
1603 , inert_irreds = irs_in
1604 , inert_count = n - workListWantedCount kicked_out }
1605
1606 kicked_out :: WorkList
1607 -- NB: use extendWorkList to ensure that kicked-out equalities get priority
1608 -- See Note [Prioritise equality constraints] (Kick-out).
1609 -- The irreds may include non-canonical (hetero-kinded) equality
1610 -- constraints, which perhaps may have become soluble after new_tv
1611 -- is substituted; ditto the dictionaries, which may include (a~b)
1612 -- or (a~~b) constraints.
1613 kicked_out = foldrBag extendWorkListCt
1614 (emptyWorkList { wl_eqs = tv_eqs_out
1615 , wl_funeqs = feqs_out })
1616 (dicts_out `andCts` irs_out)
1617
1618 (tv_eqs_out, tv_eqs_in) = foldDVarEnv kick_out_eqs ([], emptyDVarEnv) tv_eqs
1619 (feqs_out, feqs_in) = partitionFunEqs kick_out_ct funeqmap
1620 -- See Note [Kicking out CFunEqCan for fundeps]
1621 (dicts_out, dicts_in) = partitionDicts kick_out_ct dictmap
1622 (irs_out, irs_in) = partitionBag kick_out_ct irreds
1623 -- Kick out even insolubles: See Note [Rewrite insolubles]
1624 -- Of course we must kick out irreducibles like (c a), in case
1625 -- we can rewrite 'c' to something more useful
1626
1627 (_, new_role) = new_fr
1628
1629 fr_can_rewrite_ty :: EqRel -> Type -> Bool
1630 fr_can_rewrite_ty role ty = anyRewritableTyVar False role
1631 fr_can_rewrite_tv ty
1632 fr_can_rewrite_tv :: EqRel -> TyVar -> Bool
1633 fr_can_rewrite_tv role tv = new_role `eqCanRewrite` role
1634 && tv == new_tv
1635
1636 fr_may_rewrite :: CtFlavourRole -> Bool
1637 fr_may_rewrite fs = new_fr `eqMayRewriteFR` fs
1638 -- Can the new item rewrite the inert item?
1639
1640 kick_out_ct :: Ct -> Bool
1641 -- Kick it out if the new CTyEqCan can rewrite the inert one
1642 -- See Note [kickOutRewritable]
1643 kick_out_ct ct | let fs@(_,role) = ctFlavourRole ct
1644 = fr_may_rewrite fs
1645 && fr_can_rewrite_ty role (ctPred ct)
1646 -- False: ignore casts and coercions
1647 -- NB: this includes the fsk of a CFunEqCan. It can't
1648 -- actually be rewritten, but we need to kick it out
1649 -- so we get to take advantage of injectivity
1650 -- See Note [Kicking out CFunEqCan for fundeps]
1651
1652 kick_out_eqs :: EqualCtList -> ([Ct], DTyVarEnv EqualCtList)
1653 -> ([Ct], DTyVarEnv EqualCtList)
1654 kick_out_eqs eqs (acc_out, acc_in)
1655 = (eqs_out ++ acc_out, case eqs_in of
1656 [] -> acc_in
1657 (eq1:_) -> extendDVarEnv acc_in (cc_tyvar eq1) eqs_in)
1658 where
1659 (eqs_out, eqs_in) = partition kick_out_eq eqs
1660
1661 -- Implements criteria K1-K3 in Note [Extending the inert equalities]
1662 kick_out_eq (CTyEqCan { cc_tyvar = tv, cc_rhs = rhs_ty
1663 , cc_ev = ev, cc_eq_rel = eq_rel })
1664 | not (fr_may_rewrite fs)
1665 = False -- Keep it in the inert set if the new thing can't rewrite it
1666
1667 -- Below here (fr_may_rewrite fs) is True
1668 | tv == new_tv = True -- (K1)
1669 | kick_out_for_inertness = True
1670 | kick_out_for_completeness = True
1671 | otherwise = False
1672
1673 where
1674 fs = (ctEvFlavour ev, eq_rel)
1675 kick_out_for_inertness
1676 = (fs `eqMayRewriteFR` fs) -- (K2a)
1677 && not (fs `eqMayRewriteFR` new_fr) -- (K2b)
1678 && fr_can_rewrite_ty eq_rel rhs_ty -- (K2d)
1679 -- (K2c) is guaranteed by the first guard of keep_eq
1680
1681 kick_out_for_completeness
1682 = case eq_rel of
1683 NomEq -> rhs_ty `eqType` mkTyVarTy new_tv
1684 ReprEq -> isTyVarHead new_tv rhs_ty
1685
1686 kick_out_eq ct = pprPanic "keep_eq" (ppr ct)
1687
1688 kickOutAfterUnification :: TcTyVar -> TcS Int
1689 kickOutAfterUnification new_tv
1690 = do { ics <- getInertCans
1691 ; (n_kicked, ics2) <- kickOutRewritable (Given,NomEq)
1692 new_tv ics
1693 -- Given because the tv := xi is given; NomEq because
1694 -- only nominal equalities are solved by unification
1695
1696 ; setInertCans ics2
1697 ; return n_kicked }
1698
1699 {- Note [kickOutRewritable]
1700 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1701 See also Note [inert_eqs: the inert equalities].
1702
1703 When we add a new inert equality (a ~N ty) to the inert set,
1704 we must kick out any inert items that could be rewritten by the
1705 new equality, to maintain the inert-set invariants.
1706
1707 - We want to kick out an existing inert constraint if
1708 a) the new constraint can rewrite the inert one
1709 b) 'a' is free in the inert constraint (so that it *will*)
1710 rewrite it if we kick it out.
1711
1712 For (b) we use tyCoVarsOfCt, which returns the type variables /and
1713 the kind variables/ that are directly visible in the type. Hence
1714 we will have exposed all the rewriting we care about to make the
1715 most precise kinds visible for matching classes etc. No need to
1716 kick out constraints that mention type variables whose kinds
1717 contain this variable!
1718
1719 - A Derived equality can kick out [D] constraints in inert_eqs,
1720 inert_dicts, inert_irreds etc.
1721
1722 - We don't kick out constraints from inert_solved_dicts, and
1723 inert_solved_funeqs optimistically. But when we lookup we have to
1724 take the substitution into account
1725
1726
1727 Note [Rewrite insolubles]
1728 ~~~~~~~~~~~~~~~~~~~~~~~~~
1729 Suppose we have an insoluble alpha ~ [alpha], which is insoluble
1730 because an occurs check. And then we unify alpha := [Int]. Then we
1731 really want to rewrite the insoluble to [Int] ~ [[Int]]. Now it can
1732 be decomposed. Otherwise we end up with a "Can't match [Int] ~
1733 [[Int]]" which is true, but a bit confusing because the outer type
1734 constructors match.
1735
1736 Similarly, if we have a CHoleCan, we'd like to rewrite it with any
1737 Givens, to give as informative an error messasge as possible
1738 (Trac #12468, #11325).
1739
1740 Hence:
1741 * In the main simlifier loops in TcSimplify (solveWanteds,
1742 simpl_loop), we feed the insolubles in solveSimpleWanteds,
1743 so that they get rewritten (albeit not solved).
1744
1745 * We kick insolubles out of the inert set, if they can be
1746 rewritten (see TcSMonad.kick_out_rewritable)
1747
1748 * We rewrite those insolubles in TcCanonical.
1749 See Note [Make sure that insolubles are fully rewritten]
1750 -}
1751
1752
1753
1754 --------------
1755 addInertSafehask :: InertCans -> Ct -> InertCans
1756 addInertSafehask ics item@(CDictCan { cc_class = cls, cc_tyargs = tys })
1757 = ics { inert_safehask = addDict (inert_dicts ics) cls tys item }
1758
1759 addInertSafehask _ item
1760 = pprPanic "addInertSafehask: can't happen! Inserting " $ ppr item
1761
1762 insertSafeOverlapFailureTcS :: Ct -> TcS ()
1763 -- See Note [Safe Haskell Overlapping Instances Implementation] in TcSimplify
1764 insertSafeOverlapFailureTcS item
1765 = updInertCans (\ics -> addInertSafehask ics item)
1766
1767 getSafeOverlapFailures :: TcS Cts
1768 -- See Note [Safe Haskell Overlapping Instances Implementation] in TcSimplify
1769 getSafeOverlapFailures
1770 = do { IC { inert_safehask = safehask } <- getInertCans
1771 ; return $ foldDicts consCts safehask emptyCts }
1772
1773 --------------
1774 addSolvedDict :: CtEvidence -> Class -> [Type] -> TcS ()
1775 -- Add a new item in the solved set of the monad
1776 -- See Note [Solved dictionaries]
1777 addSolvedDict item cls tys
1778 | isIPPred (ctEvPred item) -- Never cache "solved" implicit parameters (not sure why!)
1779 = return ()
1780 | otherwise
1781 = do { traceTcS "updSolvedSetTcs:" $ ppr item
1782 ; updInertTcS $ \ ics ->
1783 ics { inert_solved_dicts = addDict (inert_solved_dicts ics) cls tys item } }
1784
1785 getSolvedDicts :: TcS (DictMap CtEvidence)
1786 getSolvedDicts = do { ics <- getTcSInerts; return (inert_solved_dicts ics) }
1787
1788 setSolvedDicts :: DictMap CtEvidence -> TcS ()
1789 setSolvedDicts solved_dicts
1790 = updInertTcS $ \ ics ->
1791 ics { inert_solved_dicts = solved_dicts }
1792
1793
1794 {- *********************************************************************
1795 * *
1796 Other inert-set operations
1797 * *
1798 ********************************************************************* -}
1799
1800 updInertTcS :: (InertSet -> InertSet) -> TcS ()
1801 -- Modify the inert set with the supplied function
1802 updInertTcS upd_fn
1803 = do { is_var <- getTcSInertsRef
1804 ; wrapTcS (do { curr_inert <- TcM.readTcRef is_var
1805 ; TcM.writeTcRef is_var (upd_fn curr_inert) }) }
1806
1807 getInertCans :: TcS InertCans
1808 getInertCans = do { inerts <- getTcSInerts; return (inert_cans inerts) }
1809
1810 setInertCans :: InertCans -> TcS ()
1811 setInertCans ics = updInertTcS $ \ inerts -> inerts { inert_cans = ics }
1812
1813 updRetInertCans :: (InertCans -> (a, InertCans)) -> TcS a
1814 -- Modify the inert set with the supplied function
1815 updRetInertCans upd_fn
1816 = do { is_var <- getTcSInertsRef
1817 ; wrapTcS (do { inerts <- TcM.readTcRef is_var
1818 ; let (res, cans') = upd_fn (inert_cans inerts)
1819 ; TcM.writeTcRef is_var (inerts { inert_cans = cans' })
1820 ; return res }) }
1821
1822 updInertCans :: (InertCans -> InertCans) -> TcS ()
1823 -- Modify the inert set with the supplied function
1824 updInertCans upd_fn
1825 = updInertTcS $ \ inerts -> inerts { inert_cans = upd_fn (inert_cans inerts) }
1826
1827 updInertDicts :: (DictMap Ct -> DictMap Ct) -> TcS ()
1828 -- Modify the inert set with the supplied function
1829 updInertDicts upd_fn
1830 = updInertCans $ \ ics -> ics { inert_dicts = upd_fn (inert_dicts ics) }
1831
1832 updInertSafehask :: (DictMap Ct -> DictMap Ct) -> TcS ()
1833 -- Modify the inert set with the supplied function
1834 updInertSafehask upd_fn
1835 = updInertCans $ \ ics -> ics { inert_safehask = upd_fn (inert_safehask ics) }
1836
1837 updInertFunEqs :: (FunEqMap Ct -> FunEqMap Ct) -> TcS ()
1838 -- Modify the inert set with the supplied function
1839 updInertFunEqs upd_fn
1840 = updInertCans $ \ ics -> ics { inert_funeqs = upd_fn (inert_funeqs ics) }
1841
1842 updInertIrreds :: (Cts -> Cts) -> TcS ()
1843 -- Modify the inert set with the supplied function
1844 updInertIrreds upd_fn
1845 = updInertCans $ \ ics -> ics { inert_irreds = upd_fn (inert_irreds ics) }
1846
1847 getInertEqs :: TcS (DTyVarEnv EqualCtList)
1848 getInertEqs = do { inert <- getInertCans; return (inert_eqs inert) }
1849
1850 getInertInsols :: TcS Cts
1851 -- Returns insoluble equality constraints
1852 -- specifically including Givens
1853 getInertInsols = do { inert <- getInertCans
1854 ; return (filterBag insolubleEqCt (inert_irreds inert)) }
1855
1856 getInertGivens :: TcS [Ct]
1857 -- Returns the Given constraints in the inert set,
1858 -- with type functions *not* unflattened
1859 getInertGivens
1860 = do { inerts <- getInertCans
1861 ; let all_cts = foldDicts (:) (inert_dicts inerts)
1862 $ foldFunEqs (:) (inert_funeqs inerts)
1863 $ concat (dVarEnvElts (inert_eqs inerts))
1864 ; return (filter isGivenCt all_cts) }
1865
1866 getPendingScDicts :: TcS [Ct]
1867 -- Find all inert Given dictionaries whose cc_pend_sc flag is True
1868 -- Set the flag to False in the inert set, and return that Ct
1869 getPendingScDicts = updRetInertCans get_sc_dicts
1870 where
1871 get_sc_dicts ic@(IC { inert_dicts = dicts })
1872 = (sc_pend_dicts, ic')
1873 where
1874 ic' = ic { inert_dicts = foldr add dicts sc_pend_dicts }
1875
1876 sc_pend_dicts :: [Ct]
1877 sc_pend_dicts = foldDicts get_pending dicts []
1878
1879 get_pending :: Ct -> [Ct] -> [Ct] -- Get dicts with cc_pend_sc = True
1880 -- but flipping the flag
1881 get_pending dict dicts
1882 | Just dict' <- isPendingScDict dict = dict' : dicts
1883 | otherwise = dicts
1884
1885 add :: Ct -> DictMap Ct -> DictMap Ct
1886 add ct@(CDictCan { cc_class = cls, cc_tyargs = tys }) dicts
1887 = addDict dicts cls tys ct
1888 add ct _ = pprPanic "getPendingScDicts" (ppr ct)
1889
1890 getUnsolvedInerts :: TcS ( Bag Implication
1891 , Cts -- Tyvar eqs: a ~ ty
1892 , Cts -- Fun eqs: F a ~ ty
1893 , Cts ) -- All others
1894 -- Return all the unsolved [Wanted] or [Derived] constraints
1895 --
1896 -- Post-condition: the returned simple constraints are all fully zonked
1897 -- (because they come from the inert set)
1898 -- the unsolved implics may not be
1899 getUnsolvedInerts
1900 = do { IC { inert_eqs = tv_eqs
1901 , inert_funeqs = fun_eqs
1902 , inert_irreds = irreds
1903 , inert_dicts = idicts
1904 } <- getInertCans
1905
1906 ; let unsolved_tv_eqs = foldTyEqs add_if_unsolved tv_eqs emptyCts
1907 unsolved_fun_eqs = foldFunEqs add_if_wanted fun_eqs emptyCts
1908 unsolved_irreds = Bag.filterBag is_unsolved irreds
1909 unsolved_dicts = foldDicts add_if_unsolved idicts emptyCts
1910 unsolved_others = unsolved_irreds `unionBags` unsolved_dicts
1911
1912 ; implics <- getWorkListImplics
1913
1914 ; traceTcS "getUnsolvedInerts" $
1915 vcat [ text " tv eqs =" <+> ppr unsolved_tv_eqs
1916 , text "fun eqs =" <+> ppr unsolved_fun_eqs
1917 , text "others =" <+> ppr unsolved_others
1918 , text "implics =" <+> ppr implics ]
1919
1920 ; return ( implics, unsolved_tv_eqs, unsolved_fun_eqs, unsolved_others) }
1921 where
1922 add_if_unsolved :: Ct -> Cts -> Cts
1923 add_if_unsolved ct cts | is_unsolved ct = ct `consCts` cts
1924 | otherwise = cts
1925
1926 is_unsolved ct = not (isGivenCt ct) -- Wanted or Derived
1927
1928 -- For CFunEqCans we ignore the Derived ones, and keep
1929 -- only the Wanteds for flattening. The Derived ones
1930 -- share a unification variable with the corresponding
1931 -- Wanted, so we definitely don't want to participate
1932 -- in unflattening
1933 -- See Note [Type family equations]
1934 add_if_wanted ct cts | isWantedCt ct = ct `consCts` cts
1935 | otherwise = cts
1936
1937 isInInertEqs :: DTyVarEnv EqualCtList -> TcTyVar -> TcType -> Bool
1938 -- True if (a ~N ty) is in the inert set, in either Given or Wanted
1939 isInInertEqs eqs tv rhs
1940 = case lookupDVarEnv eqs tv of
1941 Nothing -> False
1942 Just cts -> any (same_pred rhs) cts
1943 where
1944 same_pred rhs ct
1945 | CTyEqCan { cc_rhs = rhs2, cc_eq_rel = eq_rel } <- ct
1946 , NomEq <- eq_rel
1947 , rhs `eqType` rhs2 = True
1948 | otherwise = False
1949
1950 getNoGivenEqs :: TcLevel -- TcLevel of this implication
1951 -> [TcTyVar] -- Skolems of this implication
1952 -> TcS ( Bool -- True <=> definitely no residual given equalities
1953 , Cts ) -- Insoluble equalities arising from givens
1954 -- See Note [When does an implication have given equalities?]
1955 getNoGivenEqs tclvl skol_tvs
1956 = do { inerts@(IC { inert_eqs = ieqs, inert_irreds = irreds })
1957 <- getInertCans
1958 ; let has_given_eqs = foldrBag ((||) . ct_given_here) False irreds
1959 || anyDVarEnv eqs_given_here ieqs
1960 insols = filterBag insolubleEqCt irreds
1961 -- Specifically includes ones that originated in some
1962 -- outer context but were refined to an insoluble by
1963 -- a local equality; so do /not/ add ct_given_here.
1964
1965 ; traceTcS "getNoGivenEqs" $
1966 vcat [ if has_given_eqs then text "May have given equalities"
1967 else text "No given equalities"
1968 , text "Skols:" <+> ppr skol_tvs
1969 , text "Inerts:" <+> ppr inerts
1970 , text "Insols:" <+> ppr insols]
1971 ; return (not has_given_eqs, insols) }
1972 where
1973 eqs_given_here :: EqualCtList -> Bool
1974 eqs_given_here [ct@(CTyEqCan { cc_tyvar = tv })]
1975 -- Givens are always a sigleton
1976 = not (skolem_bound_here tv) && ct_given_here ct
1977 eqs_given_here _ = False
1978
1979 ct_given_here :: Ct -> Bool
1980 -- True for a Given bound by the current implication,
1981 -- i.e. the current level
1982 ct_given_here ct = isGiven ev
1983 && tclvl == ctLocLevel (ctEvLoc ev)
1984 where
1985 ev = ctEvidence ct
1986
1987 skol_tv_set = mkVarSet skol_tvs
1988 skolem_bound_here tv -- See Note [Let-bound skolems]
1989 = case tcTyVarDetails tv of
1990 SkolemTv {} -> tv `elemVarSet` skol_tv_set
1991 _ -> False
1992
1993 -- | Returns Given constraints that might,
1994 -- potentially, match the given pred. This is used when checking to see if a
1995 -- Given might overlap with an instance. See Note [Instance and Given overlap]
1996 -- in TcInteract.
1997 matchableGivens :: CtLoc -> PredType -> InertSet -> Cts
1998 matchableGivens loc_w pred (IS { inert_cans = inert_cans })
1999 = filterBag matchable_given all_relevant_givens
2000 where
2001 -- just look in class constraints and irreds. matchableGivens does get called
2002 -- for ~R constraints, but we don't need to look through equalities, because
2003 -- canonical equalities are used for rewriting. We'll only get caught by
2004 -- non-canonical -- that is, irreducible -- equalities.
2005 all_relevant_givens :: Cts
2006 all_relevant_givens
2007 | Just (clas, _) <- getClassPredTys_maybe pred
2008 = findDictsByClass (inert_dicts inert_cans) clas
2009 `unionBags` inert_irreds inert_cans
2010 | otherwise
2011 = inert_irreds inert_cans
2012
2013 matchable_given :: Ct -> Bool
2014 matchable_given ct
2015 | CtGiven { ctev_loc = loc_g } <- ctev
2016 , Just _ <- tcUnifyTys bind_meta_tv [ctEvPred ctev] [pred]
2017 , not (prohibitedSuperClassSolve loc_g loc_w)
2018 = True
2019
2020 | otherwise
2021 = False
2022 where
2023 ctev = cc_ev ct
2024
2025 bind_meta_tv :: TcTyVar -> BindFlag
2026 -- Any meta tyvar may be unified later, so we treat it as
2027 -- bindable when unifying with givens. That ensures that we
2028 -- conservatively assume that a meta tyvar might get unified with
2029 -- something that matches the 'given', until demonstrated
2030 -- otherwise. More info in Note [Instance and Given overlap]
2031 -- in TcInteract
2032 bind_meta_tv tv | isMetaTyVar tv
2033 , not (isFskTyVar tv) = BindMe
2034 | otherwise = Skolem
2035
2036 prohibitedSuperClassSolve :: CtLoc -> CtLoc -> Bool
2037 -- See Note [Solving superclass constraints] in TcInstDcls
2038 prohibitedSuperClassSolve from_loc solve_loc
2039 | GivenOrigin (InstSC given_size) <- ctLocOrigin from_loc
2040 , ScOrigin wanted_size <- ctLocOrigin solve_loc
2041 = given_size >= wanted_size
2042 | otherwise
2043 = False
2044
2045 {- Note [Unsolved Derived equalities]
2046 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2047 In getUnsolvedInerts, we return a derived equality from the inert_eqs
2048 because it is a candidate for floating out of this implication. We
2049 only float equalities with a meta-tyvar on the left, so we only pull
2050 those out here.
2051
2052 Note [When does an implication have given equalities?]
2053 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2054 Consider an implication
2055 beta => alpha ~ Int
2056 where beta is a unification variable that has already been unified
2057 to () in an outer scope. Then we can float the (alpha ~ Int) out
2058 just fine. So when deciding whether the givens contain an equality,
2059 we should canonicalise first, rather than just looking at the original
2060 givens (Trac #8644).
2061
2062 So we simply look at the inert, canonical Givens and see if there are
2063 any equalities among them, the calculation of has_given_eqs. There
2064 are some wrinkles:
2065
2066 * We must know which ones are bound in *this* implication and which
2067 are bound further out. We can find that out from the TcLevel
2068 of the Given, which is itself recorded in the tcl_tclvl field
2069 of the TcLclEnv stored in the Given (ev_given_here).
2070
2071 What about interactions between inner and outer givens?
2072 - Outer given is rewritten by an inner given, then there must
2073 have been an inner given equality, hence the “given-eq” flag
2074 will be true anyway.
2075
2076 - Inner given rewritten by outer, retains its level (ie. The inner one)
2077
2078 * We must take account of *potential* equalities, like the one above:
2079 beta => ...blah...
2080 If we still don't know what beta is, we conservatively treat it as potentially
2081 becoming an equality. Hence including 'irreds' in the calculation or has_given_eqs.
2082
2083 * When flattening givens, we generate Given equalities like
2084 <F [a]> : F [a] ~ f,
2085 with Refl evidence, and we *don't* want those to count as an equality
2086 in the givens! After all, the entire flattening business is just an
2087 internal matter, and the evidence does not mention any of the 'givens'
2088 of this implication. So we do not treat inert_funeqs as a 'given equality'.
2089
2090 * See Note [Let-bound skolems] for another wrinkle
2091
2092 * We do *not* need to worry about representational equalities, because
2093 these do not affect the ability to float constraints.
2094
2095 Note [Let-bound skolems]
2096 ~~~~~~~~~~~~~~~~~~~~~~~~
2097 If * the inert set contains a canonical Given CTyEqCan (a ~ ty)
2098 and * 'a' is a skolem bound in this very implication, b
2099
2100 then:
2101 a) The Given is pretty much a let-binding, like
2102 f :: (a ~ b->c) => a -> a
2103 Here the equality constraint is like saying
2104 let a = b->c in ...
2105 It is not adding any new, local equality information,
2106 and hence can be ignored by has_given_eqs
2107
2108 b) 'a' will have been completely substituted out in the inert set,
2109 so we can safely discard it. Notably, it doesn't need to be
2110 returned as part of 'fsks'
2111
2112 For an example, see Trac #9211.
2113
2114 See also TcUnify Note [Deeper level on the left] for how we ensure
2115 that the right variable is on the left of the equality when both are
2116 tyvars.
2117 -}
2118
2119 removeInertCts :: [Ct] -> InertCans -> InertCans
2120 -- ^ Remove inert constraints from the 'InertCans', for use when a
2121 -- typechecker plugin wishes to discard a given.
2122 removeInertCts cts icans = foldl' removeInertCt icans cts
2123
2124 removeInertCt :: InertCans -> Ct -> InertCans
2125 removeInertCt is ct =
2126 case ct of
2127
2128 CDictCan { cc_class = cl, cc_tyargs = tys } ->
2129 is { inert_dicts = delDict (inert_dicts is) cl tys }
2130
2131 CFunEqCan { cc_fun = tf, cc_tyargs = tys } ->
2132 is { inert_funeqs = delFunEq (inert_funeqs is) tf tys }
2133
2134 CTyEqCan { cc_tyvar = x, cc_rhs = ty } ->
2135 is { inert_eqs = delTyEq (inert_eqs is) x ty }
2136
2137 CIrredCan {} -> panic "removeInertCt: CIrredEvCan"
2138 CNonCanonical {} -> panic "removeInertCt: CNonCanonical"
2139 CHoleCan {} -> panic "removeInertCt: CHoleCan"
2140
2141
2142 lookupFlatCache :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcType, CtFlavour))
2143 lookupFlatCache fam_tc tys
2144 = do { IS { inert_flat_cache = flat_cache
2145 , inert_cans = IC { inert_funeqs = inert_funeqs } } <- getTcSInerts
2146 ; return (firstJusts [lookup_inerts inert_funeqs,
2147 lookup_flats flat_cache]) }
2148 where
2149 lookup_inerts inert_funeqs
2150 | Just (CFunEqCan { cc_ev = ctev, cc_fsk = fsk, cc_tyargs = xis })
2151 <- findFunEq inert_funeqs fam_tc tys
2152 , tys `eqTypes` xis -- The lookup might find a near-match; see
2153 -- Note [Use loose types in inert set]
2154 = Just (ctEvCoercion ctev, mkTyVarTy fsk, ctEvFlavour ctev)
2155 | otherwise = Nothing
2156
2157 lookup_flats flat_cache = findExactFunEq flat_cache fam_tc tys
2158
2159
2160 lookupInInerts :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence)
2161 -- Is this exact predicate type cached in the solved or canonicals of the InertSet?
2162 lookupInInerts loc pty
2163 | ClassPred cls tys <- classifyPredType pty
2164 = do { inerts <- getTcSInerts
2165 ; return (lookupSolvedDict inerts loc cls tys `mplus`
2166 lookupInertDict (inert_cans inerts) loc cls tys) }
2167 | otherwise -- NB: No caching for equalities, IPs, holes, or errors
2168 = return Nothing
2169
2170 -- | Look up a dictionary inert. NB: the returned 'CtEvidence' might not
2171 -- match the input exactly. Note [Use loose types in inert set].
2172 lookupInertDict :: InertCans -> CtLoc -> Class -> [Type] -> Maybe CtEvidence
2173 lookupInertDict (IC { inert_dicts = dicts }) loc cls tys
2174 = case findDict dicts loc cls tys of
2175 Just ct -> Just (ctEvidence ct)
2176 _ -> Nothing
2177
2178 -- | Look up a solved inert. NB: the returned 'CtEvidence' might not
2179 -- match the input exactly. See Note [Use loose types in inert set].
2180 lookupSolvedDict :: InertSet -> CtLoc -> Class -> [Type] -> Maybe CtEvidence
2181 -- Returns just if exactly this predicate type exists in the solved.
2182 lookupSolvedDict (IS { inert_solved_dicts = solved }) loc cls tys
2183 = case findDict solved loc cls tys of
2184 Just ev -> Just ev
2185 _ -> Nothing
2186
2187 {- *********************************************************************
2188 * *
2189 Irreds
2190 * *
2191 ********************************************************************* -}
2192
2193 foldIrreds :: (Ct -> b -> b) -> Cts -> b -> b
2194 foldIrreds k irreds z = foldrBag k z irreds
2195
2196
2197 {- *********************************************************************
2198 * *
2199 TcAppMap
2200 * *
2201 ************************************************************************
2202
2203 Note [Use loose types in inert set]
2204 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2205 Say we know (Eq (a |> c1)) and we need (Eq (a |> c2)). One is clearly
2206 solvable from the other. So, we do lookup in the inert set using
2207 loose types, which omit the kind-check.
2208
2209 We must be careful when using the result of a lookup because it may
2210 not match the requested info exactly!
2211
2212 -}
2213
2214 type TcAppMap a = UniqDFM (ListMap LooseTypeMap a)
2215 -- Indexed by tycon then the arg types, using "loose" matching, where
2216 -- we don't require kind equality. This allows, for example, (a |> co)
2217 -- to match (a).
2218 -- See Note [Use loose types in inert set]
2219 -- Used for types and classes; hence UniqDFM
2220 -- See Note [foldTM determinism] for why we use UniqDFM here
2221
2222 isEmptyTcAppMap :: TcAppMap a -> Bool
2223 isEmptyTcAppMap m = isNullUDFM m
2224
2225 emptyTcAppMap :: TcAppMap a
2226 emptyTcAppMap = emptyUDFM
2227
2228 findTcApp :: TcAppMap a -> Unique -> [Type] -> Maybe a
2229 findTcApp m u tys = do { tys_map <- lookupUDFM m u
2230 ; lookupTM tys tys_map }
2231
2232 delTcApp :: TcAppMap a -> Unique -> [Type] -> TcAppMap a
2233 delTcApp m cls tys = adjustUDFM (deleteTM tys) m cls
2234
2235 insertTcApp :: TcAppMap a -> Unique -> [Type] -> a -> TcAppMap a
2236 insertTcApp m cls tys ct = alterUDFM alter_tm m cls
2237 where
2238 alter_tm mb_tm = Just (insertTM tys ct (mb_tm `orElse` emptyTM))
2239
2240 -- mapTcApp :: (a->b) -> TcAppMap a -> TcAppMap b
2241 -- mapTcApp f = mapUDFM (mapTM f)
2242
2243 filterTcAppMap :: (Ct -> Bool) -> TcAppMap Ct -> TcAppMap Ct
2244 filterTcAppMap f m
2245 = mapUDFM do_tm m
2246 where
2247 do_tm tm = foldTM insert_mb tm emptyTM
2248 insert_mb ct tm
2249 | f ct = insertTM tys ct tm
2250 | otherwise = tm
2251 where
2252 tys = case ct of
2253 CFunEqCan { cc_tyargs = tys } -> tys
2254 CDictCan { cc_tyargs = tys } -> tys
2255 _ -> pprPanic "filterTcAppMap" (ppr ct)
2256
2257 tcAppMapToBag :: TcAppMap a -> Bag a
2258 tcAppMapToBag m = foldTcAppMap consBag m emptyBag
2259
2260 foldTcAppMap :: (a -> b -> b) -> TcAppMap a -> b -> b
2261 foldTcAppMap k m z = foldUDFM (foldTM k) z m
2262
2263
2264 {- *********************************************************************
2265 * *
2266 DictMap
2267 * *
2268 ********************************************************************* -}
2269
2270
2271 {- Note [Tuples hiding implicit parameters]
2272 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2273 Consider
2274 f,g :: (?x::Int, C a) => a -> a
2275 f v = let ?x = 4 in g v
2276
2277 The call to 'g' gives rise to a Wanted constraint (?x::Int, C a).
2278 We must /not/ solve this from the Given (?x::Int, C a), because of
2279 the intervening binding for (?x::Int). Trac #14218.
2280
2281 We deal with this by arranging that we always fail when looking up a
2282 tuple constraint that hides an implicit parameter. Not that this applies
2283 * both to the inert_dicts (lookupInertDict)
2284 * and to the solved_dicts (looukpSolvedDict)
2285 An alternative would be not to extend these sets with such tuple
2286 constraints, but it seemed more direct to deal with the lookup.
2287
2288 Note [Solving CallStack constraints]
2289 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2290 Suppose f :: HasCallStack => blah. Then
2291
2292 * Each call to 'f' gives rise to
2293 [W] s1 :: IP "callStack" CallStack -- CtOrigin = OccurrenceOf f
2294 with a CtOrigin that says "OccurrenceOf f".
2295 Remember that HasCallStack is just shorthand for
2296 IP "callStack CallStack
2297 See Note [Overview of implicit CallStacks] in TcEvidence
2298
2299 * We cannonicalise such constraints, in TcCanonical.canClassNC, by
2300 pushing the call-site info on the stack, and changing the CtOrigin
2301 to record that has been done.
2302 Bind: s1 = pushCallStack <site-info> s2
2303 [W] s2 :: IP "callStack" CallStack -- CtOrigin = IPOccOrigin
2304
2305 * Then, and only then, we can solve the constraint from an enclosing
2306 Given.
2307
2308 So we must be careful /not/ to solve 's1' from the Givens. Again,
2309 we ensure this by arranging that findDict always misses when looking
2310 up souch constraints.
2311 -}
2312
2313 type DictMap a = TcAppMap a
2314
2315 emptyDictMap :: DictMap a
2316 emptyDictMap = emptyTcAppMap
2317
2318 findDict :: DictMap a -> CtLoc -> Class -> [Type] -> Maybe a
2319 findDict m loc cls tys
2320 | isCTupleClass cls
2321 , any hasIPPred tys -- See Note [Tuples hiding implicit parameters]
2322 = Nothing
2323
2324 | Just {} <- isCallStackPred cls tys
2325 , OccurrenceOf {} <- ctLocOrigin loc
2326 = Nothing -- See Note [Solving CallStack constraints]
2327
2328 | otherwise
2329 = findTcApp m (getUnique cls) tys
2330
2331 findDictsByClass :: DictMap a -> Class -> Bag a
2332 findDictsByClass m cls
2333 | Just tm <- lookupUDFM m cls = foldTM consBag tm emptyBag
2334 | otherwise = emptyBag
2335
2336 delDict :: DictMap a -> Class -> [Type] -> DictMap a
2337 delDict m cls tys = delTcApp m (getUnique cls) tys
2338
2339 addDict :: DictMap a -> Class -> [Type] -> a -> DictMap a
2340 addDict m cls tys item = insertTcApp m (getUnique cls) tys item
2341
2342 addDictsByClass :: DictMap Ct -> Class -> Bag Ct -> DictMap Ct
2343 addDictsByClass m cls items
2344 = addToUDFM m cls (foldrBag add emptyTM items)
2345 where
2346 add ct@(CDictCan { cc_tyargs = tys }) tm = insertTM tys ct tm
2347 add ct _ = pprPanic "addDictsByClass" (ppr ct)
2348
2349 filterDicts :: (Ct -> Bool) -> DictMap Ct -> DictMap Ct
2350 filterDicts f m = filterTcAppMap f m
2351
2352 partitionDicts :: (Ct -> Bool) -> DictMap Ct -> (Bag Ct, DictMap Ct)
2353 partitionDicts f m = foldTcAppMap k m (emptyBag, emptyDicts)
2354 where
2355 k ct (yeses, noes) | f ct = (ct `consBag` yeses, noes)
2356 | otherwise = (yeses, add ct noes)
2357 add ct@(CDictCan { cc_class = cls, cc_tyargs = tys }) m
2358 = addDict m cls tys ct
2359 add ct _ = pprPanic "partitionDicts" (ppr ct)
2360
2361 dictsToBag :: DictMap a -> Bag a
2362 dictsToBag = tcAppMapToBag
2363
2364 foldDicts :: (a -> b -> b) -> DictMap a -> b -> b
2365 foldDicts = foldTcAppMap
2366
2367 emptyDicts :: DictMap a
2368 emptyDicts = emptyTcAppMap
2369
2370
2371 {- *********************************************************************
2372 * *
2373 FunEqMap
2374 * *
2375 ********************************************************************* -}
2376
2377 type FunEqMap a = TcAppMap a -- A map whose key is a (TyCon, [Type]) pair
2378
2379 emptyFunEqs :: TcAppMap a
2380 emptyFunEqs = emptyTcAppMap
2381
2382 findFunEq :: FunEqMap a -> TyCon -> [Type] -> Maybe a
2383 findFunEq m tc tys = findTcApp m (getUnique tc) tys
2384
2385 funEqsToBag :: FunEqMap a -> Bag a
2386 funEqsToBag m = foldTcAppMap consBag m emptyBag
2387
2388 findFunEqsByTyCon :: FunEqMap a -> TyCon -> [a]
2389 -- Get inert function equation constraints that have the given tycon
2390 -- in their head. Not that the constraints remain in the inert set.
2391 -- We use this to check for derived interactions with built-in type-function
2392 -- constructors.
2393 findFunEqsByTyCon m tc
2394 | Just tm <- lookupUDFM m tc = foldTM (:) tm []
2395 | otherwise = []
2396
2397 foldFunEqs :: (a -> b -> b) -> FunEqMap a -> b -> b
2398 foldFunEqs = foldTcAppMap
2399
2400 -- mapFunEqs :: (a -> b) -> FunEqMap a -> FunEqMap b
2401 -- mapFunEqs = mapTcApp
2402
2403 -- filterFunEqs :: (Ct -> Bool) -> FunEqMap Ct -> FunEqMap Ct
2404 -- filterFunEqs = filterTcAppMap
2405
2406 insertFunEq :: FunEqMap a -> TyCon -> [Type] -> a -> FunEqMap a
2407 insertFunEq m tc tys val = insertTcApp m (getUnique tc) tys val
2408
2409 partitionFunEqs :: (Ct -> Bool) -> FunEqMap Ct -> ([Ct], FunEqMap Ct)
2410 -- Optimise for the case where the predicate is false
2411 -- partitionFunEqs is called only from kick-out, and kick-out usually
2412 -- kicks out very few equalities, so we want to optimise for that case
2413 partitionFunEqs f m = (yeses, foldr del m yeses)
2414 where
2415 yeses = foldTcAppMap k m []
2416 k ct yeses | f ct = ct : yeses
2417 | otherwise = yeses
2418 del (CFunEqCan { cc_fun = tc, cc_tyargs = tys }) m
2419 = delFunEq m tc tys
2420 del ct _ = pprPanic "partitionFunEqs" (ppr ct)
2421
2422 delFunEq :: FunEqMap a -> TyCon -> [Type] -> FunEqMap a
2423 delFunEq m tc tys = delTcApp m (getUnique tc) tys
2424
2425 ------------------------------
2426 type ExactFunEqMap a = UniqFM (ListMap TypeMap a)
2427
2428 emptyExactFunEqs :: ExactFunEqMap a
2429 emptyExactFunEqs = emptyUFM
2430
2431 findExactFunEq :: ExactFunEqMap a -> TyCon -> [Type] -> Maybe a
2432 findExactFunEq m tc tys = do { tys_map <- lookupUFM m (getUnique tc)
2433 ; lookupTM tys tys_map }
2434
2435 insertExactFunEq :: ExactFunEqMap a -> TyCon -> [Type] -> a -> ExactFunEqMap a
2436 insertExactFunEq m tc tys val = alterUFM alter_tm m (getUnique tc)
2437 where alter_tm mb_tm = Just (insertTM tys val (mb_tm `orElse` emptyTM))
2438
2439 {-
2440 ************************************************************************
2441 * *
2442 * The TcS solver monad *
2443 * *
2444 ************************************************************************
2445
2446 Note [The TcS monad]
2447 ~~~~~~~~~~~~~~~~~~~~
2448 The TcS monad is a weak form of the main Tc monad
2449
2450 All you can do is
2451 * fail
2452 * allocate new variables
2453 * fill in evidence variables
2454
2455 Filling in a dictionary evidence variable means to create a binding
2456 for it, so TcS carries a mutable location where the binding can be
2457 added. This is initialised from the innermost implication constraint.
2458 -}
2459
2460 data TcSEnv
2461 = TcSEnv {
2462 tcs_ev_binds :: EvBindsVar,
2463
2464 tcs_unified :: IORef Int,
2465 -- The number of unification variables we have filled
2466 -- The important thing is whether it is non-zero
2467
2468 tcs_count :: IORef Int, -- Global step count
2469
2470 tcs_inerts :: IORef InertSet, -- Current inert set
2471
2472 -- The main work-list and the flattening worklist
2473 -- See Note [Work list priorities] and
2474 tcs_worklist :: IORef WorkList -- Current worklist
2475 }
2476
2477 ---------------
2478 newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
2479
2480 instance Functor TcS where
2481 fmap f m = TcS $ fmap f . unTcS m
2482
2483 instance Applicative TcS where
2484 pure x = TcS (\_ -> return x)
2485 (<*>) = ap
2486
2487 instance Monad TcS where
2488 fail = MonadFail.fail
2489 m >>= k = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
2490
2491 instance MonadFail.MonadFail TcS where
2492 fail err = TcS (\_ -> fail err)
2493
2494 instance MonadUnique TcS where
2495 getUniqueSupplyM = wrapTcS getUniqueSupplyM
2496
2497 instance HasModule TcS where
2498 getModule = wrapTcS getModule
2499
2500 instance MonadThings TcS where
2501 lookupThing n = wrapTcS (lookupThing n)
2502
2503 -- Basic functionality
2504 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2505 wrapTcS :: TcM a -> TcS a
2506 -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
2507 -- and TcS is supposed to have limited functionality
2508 wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
2509
2510 wrapErrTcS :: TcM a -> TcS a
2511 -- The thing wrapped should just fail
2512 -- There's no static check; it's up to the user
2513 -- Having a variant for each error message is too painful
2514 wrapErrTcS = wrapTcS
2515
2516 wrapWarnTcS :: TcM a -> TcS a
2517 -- The thing wrapped should just add a warning, or no-op
2518 -- There's no static check; it's up to the user
2519 wrapWarnTcS = wrapTcS
2520
2521 failTcS, panicTcS :: SDoc -> TcS a
2522 warnTcS :: WarningFlag -> SDoc -> TcS ()
2523 addErrTcS :: SDoc -> TcS ()
2524 failTcS = wrapTcS . TcM.failWith
2525 warnTcS flag = wrapTcS . TcM.addWarn (Reason flag)
2526 addErrTcS = wrapTcS . TcM.addErr
2527 panicTcS doc = pprPanic "TcCanonical" doc
2528
2529 traceTcS :: String -> SDoc -> TcS ()
2530 traceTcS herald doc = wrapTcS (TcM.traceTc herald doc)
2531
2532 runTcPluginTcS :: TcPluginM a -> TcS a
2533 runTcPluginTcS m = wrapTcS . runTcPluginM m =<< getTcEvBindsVar
2534
2535 instance HasDynFlags TcS where
2536 getDynFlags = wrapTcS getDynFlags
2537
2538 getGlobalRdrEnvTcS :: TcS GlobalRdrEnv
2539 getGlobalRdrEnvTcS = wrapTcS TcM.getGlobalRdrEnv
2540
2541 bumpStepCountTcS :: TcS ()
2542 bumpStepCountTcS = TcS $ \env -> do { let ref = tcs_count env
2543 ; n <- TcM.readTcRef ref
2544 ; TcM.writeTcRef ref (n+1) }
2545
2546 csTraceTcS :: SDoc -> TcS ()
2547 csTraceTcS doc
2548 = wrapTcS $ csTraceTcM (return doc)
2549
2550 traceFireTcS :: CtEvidence -> SDoc -> TcS ()
2551 -- Dump a rule-firing trace
2552 traceFireTcS ev doc
2553 = TcS $ \env -> csTraceTcM $
2554 do { n <- TcM.readTcRef (tcs_count env)
2555 ; tclvl <- TcM.getTcLevel
2556 ; return (hang (text "Step" <+> int n
2557 <> brackets (text "l:" <> ppr tclvl <> comma <>
2558 text "d:" <> ppr (ctLocDepth (ctEvLoc ev)))
2559 <+> doc <> colon)
2560 4 (ppr ev)) }
2561
2562 csTraceTcM :: TcM SDoc -> TcM ()
2563 -- Constraint-solver tracing, -ddump-cs-trace
2564 csTraceTcM mk_doc
2565 = do { dflags <- getDynFlags
2566 ; when ( dopt Opt_D_dump_cs_trace dflags
2567 || dopt Opt_D_dump_tc_trace dflags )
2568 ( do { msg <- mk_doc
2569 ; TcM.traceTcRn Opt_D_dump_cs_trace msg }) }
2570
2571 runTcS :: TcS a -- What to run
2572 -> TcM (a, EvBindMap)
2573 runTcS tcs
2574 = do { ev_binds_var <- TcM.newTcEvBinds
2575 ; res <- runTcSWithEvBinds ev_binds_var tcs
2576 ; ev_binds <- TcM.getTcEvBindsMap ev_binds_var
2577 ; return (res, ev_binds) }
2578
2579 -- | This variant of 'runTcS' will keep solving, even when only Deriveds
2580 -- are left around. It also doesn't return any evidence, as callers won't
2581 -- need it.
2582 runTcSDeriveds :: TcS a -> TcM a
2583 runTcSDeriveds tcs
2584 = do { ev_binds_var <- TcM.newTcEvBinds
2585 ; runTcSWithEvBinds ev_binds_var tcs }
2586
2587 -- | This can deal only with equality constraints.
2588 runTcSEqualities :: TcS a -> TcM a
2589 runTcSEqualities thing_inside
2590 = do { ev_binds_var <- TcM.newNoTcEvBinds
2591 ; runTcSWithEvBinds ev_binds_var thing_inside }
2592
2593 runTcSWithEvBinds :: EvBindsVar
2594 -> TcS a
2595 -> TcM a
2596 runTcSWithEvBinds ev_binds_var tcs
2597 = do { unified_var <- TcM.newTcRef 0
2598 ; step_count <- TcM.newTcRef 0
2599 ; inert_var <- TcM.newTcRef emptyInert
2600 ; wl_var <- TcM.newTcRef emptyWorkList
2601 ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
2602 , tcs_unified = unified_var
2603 , tcs_count = step_count
2604 , tcs_inerts = inert_var
2605 , tcs_worklist = wl_var }
2606
2607 -- Run the computation
2608 ; res <- unTcS tcs env
2609
2610 ; count <- TcM.readTcRef step_count
2611 ; when (count > 0) $
2612 csTraceTcM $ return (text "Constraint solver steps =" <+> int count)
2613
2614 ; unflattenGivens inert_var
2615
2616 #if defined(DEBUG)
2617 ; ev_binds <- TcM.getTcEvBindsMap ev_binds_var
2618 ; checkForCyclicBinds ev_binds
2619 #endif
2620
2621 ; return res }
2622
2623 ----------------------------
2624 #if defined(DEBUG)
2625 checkForCyclicBinds :: EvBindMap -> TcM ()
2626 checkForCyclicBinds ev_binds_map
2627 | null cycles
2628 = return ()
2629 | null coercion_cycles
2630 = TcM.traceTc "Cycle in evidence binds" $ ppr cycles
2631 | otherwise
2632 = pprPanic "Cycle in coercion bindings" $ ppr coercion_cycles
2633 where
2634 ev_binds = evBindMapBinds ev_binds_map
2635
2636 cycles :: [[EvBind]]
2637 cycles = [c | CyclicSCC c <- stronglyConnCompFromEdgedVerticesUniq edges]
2638
2639 coercion_cycles = [c | c <- cycles, any is_co_bind c]
2640 is_co_bind (EvBind { eb_lhs = b }) = isEqPred (varType b)
2641
2642 edges :: [ Node EvVar EvBind ]
2643 edges = [ DigraphNode bind bndr (nonDetEltsUniqSet (evVarsOfTerm rhs))
2644 | bind@(EvBind { eb_lhs = bndr, eb_rhs = rhs}) <- bagToList ev_binds ]
2645 -- It's OK to use nonDetEltsUFM here as
2646 -- stronglyConnCompFromEdgedVertices is still deterministic even
2647 -- if the edges are in nondeterministic order as explained in
2648 -- Note [Deterministic SCC] in Digraph.
2649 #endif
2650
2651 ----------------------------
2652 setEvBindsTcS :: EvBindsVar -> TcS a -> TcS a
2653 setEvBindsTcS ref (TcS thing_inside)
2654 = TcS $ \ env -> thing_inside (env { tcs_ev_binds = ref })
2655
2656 nestImplicTcS :: EvBindsVar
2657 -> TcLevel -> TcS a
2658 -> TcS a
2659 nestImplicTcS ref inner_tclvl (TcS thing_inside)
2660 = TcS $ \ TcSEnv { tcs_unified = unified_var
2661 , tcs_inerts = old_inert_var
2662 , tcs_count = count
2663 } ->
2664 do { inerts <- TcM.readTcRef old_inert_var
2665 ; let nest_inert = emptyInert { inert_cans = inert_cans inerts
2666 , inert_solved_dicts = inert_solved_dicts inerts }
2667 -- See Note [Do not inherit the flat cache]
2668 ; new_inert_var <- TcM.newTcRef nest_inert
2669 ; new_wl_var <- TcM.newTcRef emptyWorkList
2670 ; let nest_env = TcSEnv { tcs_ev_binds = ref
2671 , tcs_unified = unified_var
2672 , tcs_count = count
2673 , tcs_inerts = new_inert_var
2674 , tcs_worklist = new_wl_var }
2675 ; res <- TcM.setTcLevel inner_tclvl $
2676 thing_inside nest_env
2677
2678 ; unflattenGivens new_inert_var
2679
2680 #if defined(DEBUG)
2681 -- Perform a check that the thing_inside did not cause cycles
2682 ; ev_binds <- TcM.getTcEvBindsMap ref
2683 ; checkForCyclicBinds ev_binds
2684 #endif
2685 ; return res }
2686
2687 {- Note [Do not inherit the flat cache]
2688 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2689 We do not want to inherit the flat cache when processing nested
2690 implications. Consider
2691 a ~ F b, forall c. b~Int => blah
2692 If we have F b ~ fsk in the flat-cache, and we push that into the
2693 nested implication, we might miss that F b can be rewritten to F Int,
2694 and hence perhpas solve it. Moreover, the fsk from outside is
2695 flattened out after solving the outer level, but and we don't
2696 do that flattening recursively.
2697 -}
2698
2699 nestTcS :: TcS a -> TcS a
2700 -- Use the current untouchables, augmenting the current
2701 -- evidence bindings, and solved dictionaries
2702 -- But have no effect on the InertCans, or on the inert_flat_cache
2703 -- (we want to inherit the latter from processing the Givens)
2704 nestTcS (TcS thing_inside)
2705 = TcS $ \ env@(TcSEnv { tcs_inerts = inerts_var }) ->
2706 do { inerts <- TcM.readTcRef inerts_var
2707 ; new_inert_var <- TcM.newTcRef inerts
2708 ; new_wl_var <- TcM.newTcRef emptyWorkList
2709 ; let nest_env = env { tcs_inerts = new_inert_var
2710 , tcs_worklist = new_wl_var }
2711
2712 ; res <- thing_inside nest_env
2713
2714 ; new_inerts <- TcM.readTcRef new_inert_var
2715
2716 -- we want to propogate the safe haskell failures
2717 ; let old_ic = inert_cans inerts
2718 new_ic = inert_cans new_inerts
2719 nxt_ic = old_ic { inert_safehask = inert_safehask new_ic }
2720
2721 ; TcM.writeTcRef inerts_var -- See Note [Propagate the solved dictionaries]
2722 (inerts { inert_solved_dicts = inert_solved_dicts new_inerts
2723 , inert_cans = nxt_ic })
2724
2725 ; return res }
2726
2727 checkConstraintsTcS :: SkolemInfo
2728 -> [TcTyVar] -- Skolems
2729 -> TcS result
2730 -> TcS result
2731 -- Just like TcUnify.checkTvConstraints, but in the TcS monnad,
2732 -- using the work-list to gather the constraints
2733 checkConstraintsTcS skol_info skol_tvs (TcS thing_inside)
2734 = TcS $ \ tcs_env ->
2735 do { new_wl_var <- TcM.newTcRef emptyWorkList
2736 ; let new_tcs_env = tcs_env { tcs_worklist = new_wl_var }
2737
2738 ; (res, new_tclvl) <- TcM.pushTcLevelM $
2739 thing_inside new_tcs_env
2740
2741 ; wl@WL { wl_eqs = eqs } <- TcM.readTcRef new_wl_var
2742 ; ASSERT2( null (wl_funeqs wl) && null (wl_rest wl) &&
2743 null (wl_implics wl), ppr wl )
2744 unless (null eqs) $
2745 do { tcl_env <- TcM.getLclEnv
2746 ; ev_binds_var <- TcM.newNoTcEvBinds
2747 ; let wc = WC { wc_simple = listToCts eqs
2748 , wc_impl = emptyBag }
2749 imp = newImplication { ic_tclvl = new_tclvl
2750 , ic_skols = skol_tvs
2751 , ic_wanted = wc
2752 , ic_binds = ev_binds_var
2753 , ic_env = tcl_env
2754 , ic_info = skol_info }
2755
2756 -- Add the implication to the work-list
2757 ; TcM.updTcRef (tcs_worklist tcs_env)
2758 (extendWorkListImplic (unitBag imp)) }
2759
2760 ; return res }
2761
2762 {-
2763 Note [Propagate the solved dictionaries]
2764 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2765 It's really quite important that nestTcS does not discard the solved
2766 dictionaries from the thing_inside.
2767 Consider
2768 Eq [a]
2769 forall b. empty => Eq [a]
2770 We solve the simple (Eq [a]), under nestTcS, and then turn our attention to
2771 the implications. It's definitely fine to use the solved dictionaries on
2772 the inner implications, and it can make a signficant performance difference
2773 if you do so.
2774 -}
2775
2776 -- Getters and setters of TcEnv fields
2777 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2778
2779 -- Getter of inerts and worklist
2780 getTcSInertsRef :: TcS (IORef InertSet)
2781 getTcSInertsRef = TcS (return . tcs_inerts)
2782
2783 getTcSWorkListRef :: TcS (IORef WorkList)
2784 getTcSWorkListRef = TcS (return . tcs_worklist)
2785
2786 getTcSInerts :: TcS InertSet
2787 getTcSInerts = getTcSInertsRef >>= wrapTcS . (TcM.readTcRef)
2788
2789 setTcSInerts :: InertSet -> TcS ()
2790 setTcSInerts ics = do { r <- getTcSInertsRef; wrapTcS (TcM.writeTcRef r ics) }
2791
2792 getWorkListImplics :: TcS (Bag Implication)
2793 getWorkListImplics
2794 = do { wl_var <- getTcSWorkListRef
2795 ; wl_curr <- wrapTcS (TcM.readTcRef wl_var)
2796 ; return (wl_implics wl_curr) }
2797
2798 updWorkListTcS :: (WorkList -> WorkList) -> TcS ()
2799 updWorkListTcS f
2800 = do { wl_var <- getTcSWorkListRef
2801 ; wrapTcS (TcM.updTcRef wl_var f)}
2802
2803 emitWorkNC :: [CtEvidence] -> TcS ()
2804 emitWorkNC evs
2805 | null evs
2806 = return ()
2807 | otherwise
2808 = emitWork (map mkNonCanonical evs)
2809
2810 emitWork :: [Ct] -> TcS ()
2811 emitWork cts
2812 = do { traceTcS "Emitting fresh work" (vcat (map ppr cts))
2813 ; updWorkListTcS (extendWorkListCts cts) }
2814
2815 newTcRef :: a -> TcS (TcRef a)
2816 newTcRef x = wrapTcS (TcM.newTcRef x)
2817
2818 readTcRef :: TcRef a -> TcS a
2819 readTcRef ref = wrapTcS (TcM.readTcRef ref)
2820
2821 updTcRef :: TcRef a -> (a->a) -> TcS ()
2822 updTcRef ref upd_fn = wrapTcS (TcM.updTcRef ref upd_fn)
2823
2824 getTcEvBindsVar :: TcS EvBindsVar
2825 getTcEvBindsVar = TcS (return . tcs_ev_binds)
2826
2827 getTcLevel :: TcS TcLevel
2828 getTcLevel = wrapTcS TcM.getTcLevel
2829
2830 getTcEvTyCoVars :: EvBindsVar -> TcS TyCoVarSet
2831 getTcEvTyCoVars ev_binds_var
2832 = wrapTcS $ TcM.getTcEvTyCoVars ev_binds_var
2833
2834 getTcEvBindsMap :: EvBindsVar -> TcS EvBindMap
2835 getTcEvBindsMap ev_binds_var
2836 = wrapTcS $ TcM.getTcEvBindsMap ev_binds_var
2837
2838 setTcEvBindsMap :: EvBindsVar -> EvBindMap -> TcS ()
2839 setTcEvBindsMap ev_binds_var binds
2840 = wrapTcS $ TcM.setTcEvBindsMap ev_binds_var binds
2841
2842 unifyTyVar :: TcTyVar -> TcType -> TcS ()
2843 -- Unify a meta-tyvar with a type
2844 -- We keep track of how many unifications have happened in tcs_unified,
2845 --
2846 -- We should never unify the same variable twice!
2847 unifyTyVar tv ty
2848 = ASSERT2( isMetaTyVar tv, ppr tv )
2849 TcS $ \ env ->
2850 do { TcM.traceTc "unifyTyVar" (ppr tv <+> text ":=" <+> ppr ty)
2851 ; TcM.writeMetaTyVar tv ty
2852 ; TcM.updTcRef (tcs_unified env) (+1) }
2853
2854 reportUnifications :: TcS a -> TcS (Int, a)
2855 reportUnifications (TcS thing_inside)
2856 = TcS $ \ env ->
2857 do { inner_unified <- TcM.newTcRef 0
2858 ; res <- thing_inside (env { tcs_unified = inner_unified })
2859 ; n_unifs <- TcM.readTcRef inner_unified
2860 ; TcM.updTcRef (tcs_unified env) (+ n_unifs)
2861 ; return (n_unifs, res) }
2862
2863 getDefaultInfo :: TcS ([Type], (Bool, Bool))
2864 getDefaultInfo = wrapTcS TcM.tcGetDefaultTys
2865
2866 -- Just get some environments needed for instance looking up and matching
2867 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2868
2869 getInstEnvs :: TcS InstEnvs
2870 getInstEnvs = wrapTcS $ TcM.tcGetInstEnvs
2871
2872 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
2873 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
2874
2875 getTopEnv :: TcS HscEnv
2876 getTopEnv = wrapTcS $ TcM.getTopEnv
2877
2878 getGblEnv :: TcS TcGblEnv
2879 getGblEnv = wrapTcS $ TcM.getGblEnv
2880
2881 getLclEnv :: TcS TcLclEnv
2882 getLclEnv = wrapTcS $ TcM.getLclEnv
2883
2884 tcLookupClass :: Name -> TcS Class
2885 tcLookupClass c = wrapTcS $ TcM.tcLookupClass c
2886
2887 tcLookupId :: Name -> TcS Id
2888 tcLookupId n = wrapTcS $ TcM.tcLookupId n
2889
2890 -- Setting names as used (used in the deriving of Coercible evidence)
2891 -- Too hackish to expose it to TcS? In that case somehow extract the used
2892 -- constructors from the result of solveInteract
2893 addUsedGREs :: [GlobalRdrElt] -> TcS ()
2894 addUsedGREs gres = wrapTcS $ TcM.addUsedGREs gres
2895
2896 addUsedGRE :: Bool -> GlobalRdrElt -> TcS ()
2897 addUsedGRE warn_if_deprec gre = wrapTcS $ TcM.addUsedGRE warn_if_deprec gre
2898
2899
2900 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
2901 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2902
2903 checkWellStagedDFun :: PredType -> DFunId -> CtLoc -> TcS ()
2904 checkWellStagedDFun pred dfun_id loc
2905 = wrapTcS $ TcM.setCtLocM loc $
2906 do { use_stage <- TcM.getStage
2907 ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
2908 where
2909 pp_thing = text "instance for" <+> quotes (ppr pred)
2910 bind_lvl = TcM.topIdLvl dfun_id
2911
2912 pprEq :: TcType -> TcType -> SDoc
2913 pprEq ty1 ty2 = pprParendType ty1 <+> char '~' <+> pprParendType ty2
2914
2915 isFilledMetaTyVar_maybe :: TcTyVar -> TcS (Maybe Type)
2916 isFilledMetaTyVar_maybe tv
2917 = case tcTyVarDetails tv of
2918 MetaTv { mtv_ref = ref }
2919 -> do { cts <- wrapTcS (TcM.readTcRef ref)
2920 ; case cts of
2921 Indirect ty -> return (Just ty)
2922 Flexi -> return Nothing }
2923 _ -> return Nothing
2924
2925 isFilledMetaTyVar :: TcTyVar -> TcS Bool
2926 isFilledMetaTyVar tv = wrapTcS (TcM.isFilledMetaTyVar tv)
2927
2928 zonkTyCoVarsAndFV :: TcTyCoVarSet -> TcS TcTyCoVarSet
2929 zonkTyCoVarsAndFV tvs = wrapTcS (TcM.zonkTyCoVarsAndFV tvs)
2930
2931 zonkTyCoVarsAndFVList :: [TcTyCoVar] -> TcS [TcTyCoVar]
2932 zonkTyCoVarsAndFVList tvs = wrapTcS (TcM.zonkTyCoVarsAndFVList tvs)
2933
2934 zonkCo :: Coercion -> TcS Coercion
2935 zonkCo = wrapTcS . TcM.zonkCo
2936
2937 zonkTcType :: TcType -> TcS TcType
2938 zonkTcType ty = wrapTcS (TcM.zonkTcType ty)
2939
2940 zonkTcTypes :: [TcType] -> TcS [TcType]
2941 zonkTcTypes tys = wrapTcS (TcM.zonkTcTypes tys)
2942
2943 zonkTcTyVar :: TcTyVar -> TcS TcType
2944 zonkTcTyVar tv = wrapTcS (TcM.zonkTcTyVar tv)
2945
2946 zonkSimples :: Cts -> TcS Cts
2947 zonkSimples cts = wrapTcS (TcM.zonkSimples cts)
2948
2949 zonkWC :: WantedConstraints -> TcS WantedConstraints
2950 zonkWC wc = wrapTcS (TcM.zonkWC wc)
2951
2952 zonkTcTyCoVarBndr :: TcTyCoVar -> TcS TcTyCoVar
2953 zonkTcTyCoVarBndr tv = wrapTcS (TcM.zonkTcTyCoVarBndr tv)
2954
2955 {- *********************************************************************
2956 * *
2957 * Flatten skolems *
2958 * *
2959 ********************************************************************* -}
2960
2961 newFlattenSkolem :: CtFlavour -> CtLoc
2962 -> TyCon -> [TcType] -- F xis
2963 -> TcS (CtEvidence, Coercion, TcTyVar) -- [G/WD] x:: F xis ~ fsk
2964 newFlattenSkolem flav loc tc xis
2965 = do { stuff@(ev, co, fsk) <- new_skolem
2966 ; let fsk_ty = mkTyVarTy fsk
2967 ; extendFlatCache tc xis (co, fsk_ty, ctEvFlavour ev)
2968 ; return stuff }
2969 where
2970 fam_ty = mkTyConApp tc xis
2971
2972 new_skolem
2973 | Given <- flav
2974 = do { fsk <- wrapTcS (TcM.newFskTyVar fam_ty)
2975
2976 -- Extend the inert_fsks list, for use by unflattenGivens
2977 ; updInertTcS $ \is -> is { inert_fsks = (fsk, fam_ty) : inert_fsks is }
2978
2979 -- Construct the Refl evidence
2980 ; let pred = mkPrimEqPred fam_ty (mkTyVarTy fsk)
2981 co = mkNomReflCo fam_ty
2982 ; ev <- newGivenEvVar loc (pred, evCoercion co)
2983 ; return (ev, co, fsk) }
2984
2985 | otherwise -- Generate a [WD] for both Wanted and Derived
2986 -- See Note [No Derived CFunEqCans]
2987 = do { fmv <- wrapTcS (TcM.newFmvTyVar fam_ty)
2988 ; (ev, hole_co) <- newWantedEq loc Nominal fam_ty (mkTyVarTy fmv)
2989 ; return (ev, hole_co, fmv) }
2990
2991 ----------------------------
2992 unflattenGivens :: IORef InertSet -> TcM ()
2993 -- Unflatten all the fsks created by flattening types in Given
2994 -- constraints. We must be sure to do this, else we end up with
2995 -- flatten-skolems buried in any residual Wanteds
2996 --
2997 -- NB: this is the /only/ way that a fsk (MetaDetails = FlatSkolTv)
2998 -- is filled in. Nothing else does so.
2999 --
3000 -- It's here (rather than in TcFlatten) because the Right Places
3001 -- to call it are in runTcSWithEvBinds/nestImplicTcS, where it
3002 -- is nicely paired with the creation an empty inert_fsks list.
3003 unflattenGivens inert_var
3004 = do { inerts <- TcM.readTcRef inert_var
3005 ; TcM.traceTc "unflattenGivens" (ppr (inert_fsks inerts))
3006 ; mapM_ flatten_one (inert_fsks inerts) }
3007 where
3008 flatten_one (fsk, ty) = TcM.writeMetaTyVar fsk ty
3009
3010 ----------------------------
3011 extendFlatCache :: TyCon -> [Type] -> (TcCoercion, TcType, CtFlavour) -> TcS ()
3012 extendFlatCache tc xi_args stuff@(_, ty, fl)
3013 | isGivenOrWDeriv fl -- Maintain the invariant that inert_flat_cache
3014 -- only has [G] and [WD] CFunEqCans
3015 = do { dflags <- getDynFlags
3016 ; when (gopt Opt_FlatCache dflags) $
3017 do { traceTcS "extendFlatCache" (vcat [ ppr tc <+> ppr xi_args
3018 , ppr fl, ppr ty ])
3019 -- 'co' can be bottom, in the case of derived items
3020 ; updInertTcS $ \ is@(IS { inert_flat_cache = fc }) ->
3021 is { inert_flat_cache = insertExactFunEq fc tc xi_args stuff } } }
3022
3023 | otherwise
3024 = return ()
3025
3026 ----------------------------
3027 unflattenFmv :: TcTyVar -> TcType -> TcS ()
3028 -- Fill a flatten-meta-var, simply by unifying it.
3029 -- This does NOT count as a unification in tcs_unified.
3030 unflattenFmv tv ty
3031 = ASSERT2( isMetaTyVar tv, ppr tv )
3032 TcS $ \ _ ->
3033 do { TcM.traceTc "unflattenFmv" (ppr tv <+> text ":=" <+> ppr ty)
3034 ; TcM.writeMetaTyVar tv ty }
3035
3036 ----------------------------
3037 demoteUnfilledFmv :: TcTyVar -> TcS ()
3038 -- If a flatten-meta-var is still un-filled,
3039 -- turn it into an ordinary meta-var
3040 demoteUnfilledFmv fmv
3041 = wrapTcS $ do { is_filled <- TcM.isFilledMetaTyVar fmv
3042 ; unless is_filled $
3043 do { tv_ty <- TcM.newFlexiTyVarTy (tyVarKind fmv)
3044 ; TcM.writeMetaTyVar fmv tv_ty } }
3045
3046 -----------------------------
3047 dischargeFunEq :: CtEvidence -> TcTyVar -> TcCoercion -> TcType -> TcS ()
3048 -- (dischargeFunEqCan ev tv co ty)
3049 -- Preconditions
3050 -- - ev :: F tys ~ tv is a CFunEqCan
3051 -- - tv is a FlatMetaTv of FlatSkolTv
3052 -- - co :: F tys ~ xi
3053 -- - fmv/fsk `notElem` xi
3054 -- - fmv not filled (for Wanteds)
3055 --
3056 -- Then for [W] or [WD], we actually fill in the fmv:
3057 -- set fmv := xi,
3058 -- set ev := co
3059 -- kick out any inert things that are now rewritable
3060 --
3061 -- For [D], we instead emit an equality that must ultimately hold
3062 -- [D] xi ~ fmv
3063 -- Does not evaluate 'co' if 'ev' is Derived
3064 --
3065 -- For [G], emit this equality
3066 -- [G] (sym ev; co) :: fsk ~ xi
3067
3068 -- See TcFlatten Note [The flattening story],
3069 -- especially "Ownership of fsk/fmv"
3070 dischargeFunEq (CtGiven { ctev_evar = old_evar, ctev_loc = loc }) fsk co xi
3071 = do { new_ev <- newGivenEvVar loc ( new_pred, evCoercion new_co )
3072 ; emitWorkNC [new_ev] }
3073 where
3074 new_pred = mkPrimEqPred (mkTyVarTy fsk) xi
3075 new_co = mkTcSymCo (mkTcCoVarCo old_evar) `mkTcTransCo` co
3076
3077 dischargeFunEq ev@(CtWanted { ctev_dest = dest }) fmv co xi
3078 = ASSERT2( not (fmv `elemVarSet` tyCoVarsOfType xi), ppr ev $$ ppr fmv $$ ppr xi )
3079 do { setWantedEvTerm dest (EvExpr (evCoercion co))
3080 ; unflattenFmv fmv xi
3081 ; n_kicked <- kickOutAfterUnification fmv
3082 ; traceTcS "dischargeFmv" (ppr fmv <+> equals <+> ppr xi $$ pprKicked n_kicked) }
3083
3084 dischargeFunEq (CtDerived { ctev_loc = loc }) fmv _co xi
3085 = emitNewDerivedEq loc Nominal xi (mkTyVarTy fmv)
3086 -- FunEqs are always at Nominal role
3087
3088 pprKicked :: Int -> SDoc
3089 pprKicked 0 = empty
3090 pprKicked n = parens (int n <+> text "kicked out")
3091
3092 {- *********************************************************************
3093 * *
3094 * Instantiation etc.
3095 * *
3096 ********************************************************************* -}
3097
3098 -- Instantiations
3099 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3100
3101 instDFunType :: DFunId -> [DFunInstType] -> TcS ([TcType], TcThetaType)
3102 instDFunType dfun_id inst_tys
3103 = wrapTcS $ TcM.instDFunType dfun_id inst_tys
3104
3105 newFlexiTcSTy :: Kind -> TcS TcType
3106 newFlexiTcSTy knd = wrapTcS (TcM.newFlexiTyVarTy knd)
3107
3108 cloneMetaTyVar :: TcTyVar -> TcS TcTyVar
3109 cloneMetaTyVar tv = wrapTcS (TcM.cloneMetaTyVar tv)
3110
3111 instFlexi :: [TKVar] -> TcS TCvSubst
3112 instFlexi = instFlexiX emptyTCvSubst
3113
3114 instFlexiX :: TCvSubst -> [TKVar] -> TcS TCvSubst
3115 instFlexiX subst tvs
3116 = wrapTcS (foldlM instFlexiHelper subst tvs)
3117
3118 instFlexiHelper :: TCvSubst -> TKVar -> TcM TCvSubst
3119 instFlexiHelper subst tv
3120 = do { uniq <- TcM.newUnique
3121 ; details <- TcM.newMetaDetails TauTv
3122 ; let name = setNameUnique (tyVarName tv) uniq
3123 kind = substTyUnchecked subst (tyVarKind tv)
3124 ty' = mkTyVarTy (mkTcTyVar name kind details)
3125 ; TcM.traceTc "instFlexi" (ppr ty')
3126 ; return (extendTvSubst subst tv ty') }
3127
3128 tcInstType :: ([TyVar] -> TcM (TCvSubst, [TcTyVar]))
3129 -- ^ How to instantiate the type variables
3130 -> Id -- ^ Type to instantiate
3131 -> TcS ([(Name, TcTyVar)], TcThetaType, TcType) -- ^ Result
3132 -- (type vars, preds (incl equalities), rho)
3133 tcInstType inst_tyvars id = wrapTcS (TcM.tcInstType inst_tyvars id)
3134
3135 tcInstSkolTyVarsX :: TCvSubst -> [TyVar] -> TcS (TCvSubst, [TcTyVar])
3136 tcInstSkolTyVarsX subst tvs = wrapTcS $ TcM.tcInstSkolTyVarsX subst tvs
3137
3138 -- Creating and setting evidence variables and CtFlavors
3139 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3140
3141 data MaybeNew = Fresh CtEvidence | Cached EvExpr
3142
3143 isFresh :: MaybeNew -> Bool
3144 isFresh (Fresh {}) = True
3145 isFresh (Cached {}) = False
3146
3147 freshGoals :: [MaybeNew] -> [CtEvidence]
3148 freshGoals mns = [ ctev | Fresh ctev <- mns ]
3149
3150 getEvExpr :: MaybeNew -> EvExpr
3151 getEvExpr (Fresh ctev) = ctEvExpr ctev
3152 getEvExpr (Cached evt) = evt
3153
3154 setEvBind :: EvBind -> TcS ()
3155 setEvBind ev_bind
3156 = do { evb <- getTcEvBindsVar
3157 ; wrapTcS $ TcM.addTcEvBind evb ev_bind }
3158
3159 -- | Mark variables as used filling a coercion hole
3160 useVars :: CoVarSet -> TcS ()
3161 useVars vars
3162 = do { ev_binds_var <- getTcEvBindsVar
3163 ; let ref = ebv_tcvs ev_binds_var
3164 ; wrapTcS $
3165 do { tcvs <- TcM.readTcRef ref
3166 ; let tcvs' = tcvs `unionVarSet` vars
3167 ; TcM.writeTcRef ref tcvs' } }
3168
3169 -- | Equalities only
3170 setWantedEq :: TcEvDest -> Coercion -> TcS ()
3171 setWantedEq (HoleDest hole) co
3172 = do { useVars (coVarsOfCo co)
3173 ; wrapTcS $ TcM.fillCoercionHole hole co }
3174 setWantedEq (EvVarDest ev) _ = pprPanic "setWantedEq" (ppr ev)
3175
3176 -- | Equalities only
3177 setEqIfWanted :: CtEvidence -> Coercion -> TcS ()
3178 setEqIfWanted (CtWanted { ctev_dest = dest }) co = setWantedEq dest co
3179 setEqIfWanted _ _ = return ()
3180
3181 -- | Good for equalities and non-equalities
3182 setWantedEvTerm :: TcEvDest -> EvTerm -> TcS ()
3183 setWantedEvTerm (HoleDest hole) tm
3184 = do { let co = evTermCoercion tm
3185 ; useVars (coVarsOfCo co)
3186 ; wrapTcS $ TcM.fillCoercionHole hole co }
3187 setWantedEvTerm (EvVarDest ev) tm = setWantedEvBind ev tm
3188
3189 setWantedEvBind :: EvVar -> EvTerm -> TcS ()
3190 setWantedEvBind ev_id tm = setEvBind (mkWantedEvBind ev_id tm)
3191
3192 setEvBindIfWanted :: CtEvidence -> EvExpr -> TcS ()
3193 setEvBindIfWanted ev tm
3194 = case ev of
3195 CtWanted { ctev_dest = dest }
3196 -> setWantedEvTerm dest (EvExpr tm)
3197 _ -> return ()
3198
3199 newTcEvBinds :: TcS EvBindsVar
3200 newTcEvBinds = wrapTcS TcM.newTcEvBinds
3201
3202 newNoTcEvBinds :: TcS EvBindsVar
3203 newNoTcEvBinds = wrapTcS TcM.newNoTcEvBinds
3204
3205 newEvVar :: TcPredType -> TcS EvVar
3206 newEvVar pred = wrapTcS (TcM.newEvVar pred)
3207
3208 newGivenEvVar :: CtLoc -> (TcPredType, EvExpr) -> TcS CtEvidence
3209 -- Make a new variable of the given PredType,
3210 -- immediately bind it to the given term
3211 -- and return its CtEvidence
3212 -- See Note [Bind new Givens immediately] in TcRnTypes
3213 newGivenEvVar loc (pred, rhs)
3214 = do { new_ev <- newBoundEvVarId pred rhs
3215 ; return (CtGiven { ctev_pred = pred, ctev_evar = new_ev, ctev_loc = loc }) }
3216
3217 -- | Make a new 'Id' of the given type, bound (in the monad's EvBinds) to the
3218 -- given term
3219 newBoundEvVarId :: TcPredType -> EvExpr -> TcS EvVar
3220 newBoundEvVarId pred rhs
3221 = do { new_ev <- newEvVar pred
3222 ; setEvBind (mkGivenEvBind new_ev rhs)
3223 ; return new_ev }
3224
3225 newGivenEvVars :: CtLoc -> [(TcPredType, EvExpr)] -> TcS [CtEvidence]
3226 newGivenEvVars loc pts = mapM (newGivenEvVar loc) pts
3227
3228 emitNewWantedEq :: CtLoc -> Role -> TcType -> TcType -> TcS Coercion
3229 -- | Emit a new Wanted equality into the work-list
3230 emitNewWantedEq loc role ty1 ty2
3231 | otherwise
3232 = do { (ev, co) <- newWantedEq loc role ty1 ty2
3233 ; updWorkListTcS $
3234 extendWorkListEq (mkNonCanonical ev)
3235 ; return co }
3236
3237 -- | Make a new equality CtEvidence
3238 newWantedEq :: CtLoc -> Role -> TcType -> TcType -> TcS (CtEvidence, Coercion)
3239 newWantedEq loc role ty1 ty2
3240 = do { hole <- wrapTcS $ TcM.newCoercionHole pty
3241 ; traceTcS "Emitting new coercion hole" (ppr hole <+> dcolon <+> ppr pty)
3242 ; return ( CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole
3243 , ctev_nosh = WDeriv
3244 , ctev_loc = loc}
3245 , mkHoleCo hole ) }
3246 where
3247 pty = mkPrimEqPredRole role ty1 ty2
3248
3249 -- no equalities here. Use newWantedEq instead
3250 newWantedEvVarNC :: CtLoc -> TcPredType -> TcS CtEvidence
3251 -- Don't look up in the solved/inerts; we know it's not there
3252 newWantedEvVarNC loc pty
3253 = do { new_ev <- newEvVar pty
3254 ; traceTcS "Emitting new wanted" (ppr new_ev <+> dcolon <+> ppr pty $$
3255 pprCtLoc loc)
3256 ; return (CtWanted { ctev_pred = pty, ctev_dest = EvVarDest new_ev
3257 , ctev_nosh = WDeriv
3258 , ctev_loc = loc })}
3259
3260 newWantedEvVar :: CtLoc -> TcPredType -> TcS MaybeNew
3261 -- For anything except ClassPred, this is the same as newWantedEvVarNC
3262 newWantedEvVar loc pty
3263 = do { mb_ct <- lookupInInerts loc pty
3264 ; case mb_ct of
3265 Just ctev
3266 | not (isDerived ctev)
3267 -> do { traceTcS "newWantedEvVar/cache hit" $ ppr ctev
3268 ; return $ Cached (ctEvExpr ctev) }
3269 _ -> do { ctev <- newWantedEvVarNC loc pty
3270 ; return (Fresh ctev) } }
3271
3272 -- deals with both equalities and non equalities. Tries to look
3273 -- up non-equalities in the cache
3274 newWanted :: CtLoc -> PredType -> TcS MaybeNew
3275 newWanted loc pty
3276 | Just (role, ty1, ty2) <- getEqPredTys_maybe pty
3277 = Fresh . fst <$> newWantedEq loc role ty1 ty2
3278 | otherwise
3279 = newWantedEvVar loc pty
3280
3281 -- deals with both equalities and non equalities. Doesn't do any cache lookups.
3282 newWantedNC :: CtLoc -> PredType -> TcS CtEvidence
3283 newWantedNC loc pty
3284 | Just (role, ty1, ty2) <- getEqPredTys_maybe pty
3285 = fst <$> newWantedEq loc role ty1 ty2
3286 | otherwise
3287 = newWantedEvVarNC loc pty
3288
3289 emitNewDeriveds :: CtLoc -> [TcPredType] -> TcS ()
3290 emitNewDeriveds loc preds
3291 | null preds
3292 = return ()
3293 | otherwise
3294 = do { evs <- mapM (newDerivedNC loc) preds
3295 ; traceTcS "Emitting new deriveds" (ppr evs)
3296 ; updWorkListTcS (extendWorkListDeriveds evs) }
3297
3298 emitNewDerivedEq :: CtLoc -> Role -> TcType -> TcType -> TcS ()
3299 -- Create new equality Derived and put it in the work list
3300 -- There's no caching, no lookupInInerts
3301 emitNewDerivedEq loc role ty1 ty2
3302 = do { ev <- newDerivedNC loc (mkPrimEqPredRole role ty1 ty2)
3303 ; traceTcS "Emitting new derived equality" (ppr ev $$ pprCtLoc loc)
3304 ; updWorkListTcS (extendWorkListEq (mkNonCanonical ev)) }
3305 -- Very important: put in the wl_eqs
3306 -- See Note [Prioritise equalities] (Avoiding fundep iteration)
3307
3308 newDerivedNC :: CtLoc -> TcPredType -> TcS CtEvidence
3309 newDerivedNC loc pred
3310 = do { -- checkReductionDepth loc pred
3311 ; return (CtDerived { ctev_pred = pred, ctev_loc = loc }) }
3312
3313 -- --------- Check done in TcInteract.selectNewWorkItem???? ---------
3314 -- | Checks if the depth of the given location is too much. Fails if
3315 -- it's too big, with an appropriate error message.
3316 checkReductionDepth :: CtLoc -> TcType -- ^ type being reduced
3317 -> TcS ()
3318 checkReductionDepth loc ty
3319 = do { dflags <- getDynFlags
3320 ; when (subGoalDepthExceeded dflags (ctLocDepth loc)) $
3321 wrapErrTcS $
3322 solverDepthErrorTcS loc ty }
3323
3324 matchFam :: TyCon -> [Type] -> TcS (Maybe (Coercion, TcType))
3325 matchFam tycon args = wrapTcS $ matchFamTcM tycon args
3326
3327 matchFamTcM :: TyCon -> [Type] -> TcM (Maybe (Coercion, TcType))
3328 -- Given (F tys) return (ty, co), where co :: F tys ~ ty
3329 matchFamTcM tycon args
3330 = do { fam_envs <- FamInst.tcGetFamInstEnvs
3331 ; let match_fam_result
3332 = reduceTyFamApp_maybe fam_envs Nominal tycon args
3333 ; TcM.traceTc "matchFamTcM" $
3334 vcat [ text "Matching:" <+> ppr (mkTyConApp tycon args)
3335 , ppr_res match_fam_result ]
3336 ; return match_fam_result }
3337 where
3338 ppr_res Nothing = text "Match failed"
3339 ppr_res (Just (co,ty)) = hang (text "Match succeeded:")
3340 2 (vcat [ text "Rewrites to:" <+> ppr ty
3341 , text "Coercion:" <+> ppr co ])
3342
3343 {-
3344 Note [Residual implications]
3345 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3346 The wl_implics in the WorkList are the residual implication
3347 constraints that are generated while solving or canonicalising the
3348 current worklist. Specifically, when canonicalising
3349 (forall a. t1 ~ forall a. t2)
3350 from which we get the implication
3351 (forall a. t1 ~ t2)
3352 See TcSMonad.deferTcSForAllEq
3353 -}