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