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