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