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