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