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