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