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