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