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