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