Remove derived CFunEqCans after solving givens
[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,
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, takeGivenInsolubles,
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 takeGivenInsolubles :: TcS Cts
1478 -- See Note [The inert set after solving Givens]
1479 takeGivenInsolubles
1480 = updRetInertCans $ \ cans ->
1481 ( inert_insols cans
1482 , cans { inert_insols = emptyBag
1483 , inert_funeqs = filterFunEqs isGivenCt (inert_funeqs cans) } )
1484
1485 {- Note [The inert set after solving Givens]
1486 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1487 After solving the Givens we take two things out of the inert set
1488
1489 a) The insolubles; we return these to report inaccessible code
1490 We return these separately. We don't want to leave them in
1491 the inert set, lest we onfuse them with insolubles arising from
1492 solving wanteds
1493
1494 b) Any Derived CFunEqCans. Derived CTyEqCans are in the
1495 inert_model and do no harm. In contrast, Derived CFunEqCans
1496 get mixed up with the Wanteds later and confuse the
1497 post-solve-wanted unflattening (Trac #10507).
1498 E.g. From [G] 1 <= m, [G] m <= n
1499 We get [D] 1 <= n, and we must remove it!
1500 Otherwise we unflatten it more then once, and assign
1501 to its fmv more than once...disaster.
1502 It's ok to remove them because they turned ont not to
1503 yield an insoluble, and hence have now done their work.
1504 -}
1505
1506 updRetInertCans :: (InertCans -> (a, InertCans)) -> TcS a
1507 -- Modify the inert set with the supplied function
1508 updRetInertCans upd_fn
1509 = do { is_var <- getTcSInertsRef
1510 ; wrapTcS (do { inerts <- TcM.readTcRef is_var
1511 ; let (res, cans') = upd_fn (inert_cans inerts)
1512 ; TcM.writeTcRef is_var (inerts { inert_cans = cans' })
1513 ; return res }) }
1514
1515 updInertCans :: (InertCans -> InertCans) -> TcS ()
1516 -- Modify the inert set with the supplied function
1517 updInertCans upd_fn
1518 = updInertTcS $ \ inerts -> inerts { inert_cans = upd_fn (inert_cans inerts) }
1519
1520 updInertDicts :: (DictMap Ct -> DictMap Ct) -> TcS ()
1521 -- Modify the inert set with the supplied function
1522 updInertDicts upd_fn
1523 = updInertCans $ \ ics -> ics { inert_dicts = upd_fn (inert_dicts ics) }
1524
1525 updInertSafehask :: (DictMap Ct -> DictMap Ct) -> TcS ()
1526 -- Modify the inert set with the supplied function
1527 updInertSafehask upd_fn
1528 = updInertCans $ \ ics -> ics { inert_safehask = upd_fn (inert_safehask ics) }
1529
1530 updInertFunEqs :: (FunEqMap Ct -> FunEqMap Ct) -> TcS ()
1531 -- Modify the inert set with the supplied function
1532 updInertFunEqs upd_fn
1533 = updInertCans $ \ ics -> ics { inert_funeqs = upd_fn (inert_funeqs ics) }
1534
1535 updInertIrreds :: (Cts -> Cts) -> TcS ()
1536 -- Modify the inert set with the supplied function
1537 updInertIrreds upd_fn
1538 = updInertCans $ \ ics -> ics { inert_irreds = upd_fn (inert_irreds ics) }
1539
1540
1541 getInertEqs :: TcS (TyVarEnv EqualCtList)
1542 getInertEqs = do { inert <- getInertCans; return (inert_eqs inert) }
1543
1544 getInertModel :: TcS InertModel
1545 getInertModel = do { inert <- getInertCans; return (inert_model inert) }
1546
1547 getInertGivens :: TcS [Ct]
1548 -- Returns the Given constraints in the inert set,
1549 -- with type functions *not* unflattened
1550 getInertGivens
1551 = do { inerts <- getInertCans
1552 ; let all_cts = foldDicts (:) (inert_dicts inerts)
1553 $ foldFunEqs (:) (inert_funeqs inerts)
1554 $ concat (varEnvElts (inert_eqs inerts))
1555 ; return (filter isGivenCt all_cts) }
1556
1557 getUnsolvedInerts :: TcS ( Bag Implication
1558 , Cts -- Tyvar eqs: a ~ ty
1559 , Cts -- Fun eqs: F a ~ ty
1560 , Cts -- Insoluble
1561 , Cts ) -- All others
1562 -- Post-condition: the returned simple constraints are all fully zonked
1563 -- (because they come from the inert set)
1564 -- the unsolved implics may not be
1565 getUnsolvedInerts
1566 = do { IC { inert_eqs = tv_eqs
1567 , inert_funeqs = fun_eqs
1568 , inert_irreds = irreds
1569 , inert_dicts = idicts
1570 , inert_insols = insols
1571 , inert_model = model } <- getInertCans
1572
1573 ; let der_tv_eqs = foldVarEnv (add_der tv_eqs) emptyCts model -- Want to float these
1574 unsolved_tv_eqs = foldTyEqs add_if_unsolved tv_eqs der_tv_eqs
1575 unsolved_fun_eqs = foldFunEqs add_if_unsolved fun_eqs emptyCts
1576 unsolved_irreds = Bag.filterBag is_unsolved irreds
1577 unsolved_dicts = foldDicts add_if_unsolved idicts emptyCts
1578 others = unsolved_irreds `unionBags` unsolved_dicts
1579
1580 ; implics <- getWorkListImplics
1581
1582 ; traceTcS "getUnsolvedInerts" $
1583 vcat [ text " tv eqs =" <+> ppr unsolved_tv_eqs
1584 , text "fun eqs =" <+> ppr unsolved_fun_eqs
1585 , text "insols =" <+> ppr insols
1586 , text "others =" <+> ppr others
1587 , text "implics =" <+> ppr implics ]
1588
1589 ; return ( implics, unsolved_tv_eqs, unsolved_fun_eqs, insols, others) }
1590 -- Keep even the given insolubles
1591 -- so that we can report dead GADT pattern match branches
1592 where
1593 add_der tv_eqs ct cts
1594 | CTyEqCan { cc_tyvar = tv, cc_rhs = rhs } <- ct
1595 , not (isInInertEqs tv_eqs tv rhs) = ct `consBag` cts
1596 | otherwise = cts
1597 add_if_unsolved :: Ct -> Cts -> Cts
1598 add_if_unsolved ct cts | is_unsolved ct = ct `consCts` cts
1599 | otherwise = cts
1600
1601 is_unsolved ct = not (isGivenCt ct) -- Wanted or Derived
1602
1603 isInInertEqs :: TyVarEnv EqualCtList -> TcTyVar -> TcType -> Bool
1604 -- True if (a ~N ty) is in the inert set, in either Given or Wanted
1605 isInInertEqs eqs tv rhs
1606 = case lookupVarEnv eqs tv of
1607 Nothing -> False
1608 Just cts -> any (same_pred rhs) cts
1609 where
1610 same_pred rhs ct
1611 | CTyEqCan { cc_rhs = rhs2, cc_eq_rel = eq_rel } <- ct
1612 , NomEq <- eq_rel
1613 , rhs `eqType` rhs2 = True
1614 | otherwise = False
1615
1616 getNoGivenEqs :: TcLevel -- TcLevel of this implication
1617 -> [TcTyVar] -- Skolems of this implication
1618 -> TcS Bool -- True <=> definitely no residual given equalities
1619 -- See Note [When does an implication have given equalities?]
1620 getNoGivenEqs tclvl skol_tvs
1621 = do { inerts@(IC { inert_eqs = ieqs, inert_irreds = iirreds, inert_funeqs = funeqs })
1622 <- getInertCans
1623 ; let local_fsks = foldFunEqs add_fsk funeqs emptyVarSet
1624
1625 has_given_eqs = foldrBag ((||) . ev_given_here . ctEvidence) False iirreds
1626 || foldVarEnv ((||) . eqs_given_here local_fsks) False ieqs
1627
1628 ; traceTcS "getNoGivenEqs" (vcat [ppr has_given_eqs, ppr inerts])
1629 ; return (not has_given_eqs) }
1630 where
1631 eqs_given_here :: VarSet -> EqualCtList -> Bool
1632 eqs_given_here local_fsks [CTyEqCan { cc_tyvar = tv, cc_ev = ev }]
1633 -- Givens are always a sigleton
1634 = not (skolem_bound_here local_fsks tv) && ev_given_here ev
1635 eqs_given_here _ _ = False
1636
1637 ev_given_here :: CtEvidence -> Bool
1638 -- True for a Given bound by the curent implication,
1639 -- i.e. the current level
1640 ev_given_here ev
1641 = isGiven ev
1642 && tclvl == ctLocLevel (ctEvLoc ev)
1643
1644 add_fsk :: Ct -> VarSet -> VarSet
1645 add_fsk ct fsks | CFunEqCan { cc_fsk = tv, cc_ev = ev } <- ct
1646 , isGiven ev = extendVarSet fsks tv
1647 | otherwise = fsks
1648
1649 skol_tv_set = mkVarSet skol_tvs
1650 skolem_bound_here local_fsks tv -- See Note [Let-bound skolems]
1651 = case tcTyVarDetails tv of
1652 SkolemTv {} -> tv `elemVarSet` skol_tv_set
1653 FlatSkol {} -> not (tv `elemVarSet` local_fsks)
1654 _ -> False
1655
1656 {-
1657 Note [When does an implication have given equalities?]
1658 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1659 Consider an implication
1660 beta => alpha ~ Int
1661 where beta is a unification variable that has already been unified
1662 to () in an outer scope. Then we can float the (alpha ~ Int) out
1663 just fine. So when deciding whether the givens contain an equality,
1664 we should canonicalise first, rather than just looking at the original
1665 givens (Trac #8644).
1666
1667 So we simply look at the inert, canonical Givens and see if there are
1668 any equalities among them, the calculation of has_given_eqs. There
1669 are some wrinkles:
1670
1671 * We must know which ones are bound in *this* implication and which
1672 are bound further out. We can find that out from the TcLevel
1673 of the Given, which is itself recorded in the tcl_tclvl field
1674 of the TcLclEnv stored in the Given (ev_given_here).
1675
1676 What about interactions between inner and outer givens?
1677 - Outer given is rewritten by an inner given, then there must
1678 have been an inner given equality, hence the “given-eq” flag
1679 will be true anyway.
1680
1681 - Inner given rewritten by outer, retains its level (ie. The inner one)
1682
1683 * We must take account of *potential* equalities, like the one above:
1684 beta => ...blah...
1685 If we still don't know what beta is, we conservatively treat it as potentially
1686 becoming an equality. Hence including 'irreds' in the calculation or has_given_eqs.
1687
1688 * When flattening givens, we generate Given equalities like
1689 <F [a]> : F [a] ~ f,
1690 with Refl evidence, and we *don't* want those to count as an equality
1691 in the givens! After all, the entire flattening business is just an
1692 internal matter, and the evidence does not mention any of the 'givens'
1693 of this implication. So we do not treat inert_funeqs as a 'given equality'.
1694
1695 * See Note [Let-bound skolems] for another wrinkle
1696
1697 * We do *not* need to worry about representational equalities, because
1698 these do not affect the ability to float constraints.
1699
1700 Note [Let-bound skolems]
1701 ~~~~~~~~~~~~~~~~~~~~~~~~
1702 If * the inert set contains a canonical Given CTyEqCan (a ~ ty)
1703 and * 'a' is a skolem bound in this very implication, b
1704
1705 then:
1706 a) The Given is pretty much a let-binding, like
1707 f :: (a ~ b->c) => a -> a
1708 Here the equality constraint is like saying
1709 let a = b->c in ...
1710 It is not adding any new, local equality information,
1711 and hence can be ignored by has_given_eqs
1712
1713 b) 'a' will have been completely substituted out in the inert set,
1714 so we can safely discard it. Notably, it doesn't need to be
1715 returned as part of 'fsks'
1716
1717 For an example, see Trac #9211.
1718 -}
1719
1720 removeInertCts :: [Ct] -> InertCans -> InertCans
1721 -- ^ Remove inert constraints from the 'InertCans', for use when a
1722 -- typechecker plugin wishes to discard a given.
1723 removeInertCts cts icans = foldl' removeInertCt icans cts
1724
1725 removeInertCt :: InertCans -> Ct -> InertCans
1726 removeInertCt is ct =
1727 case ct of
1728
1729 CDictCan { cc_class = cl, cc_tyargs = tys } ->
1730 is { inert_dicts = delDict (inert_dicts is) cl tys }
1731
1732 CFunEqCan { cc_fun = tf, cc_tyargs = tys } ->
1733 is { inert_funeqs = delFunEq (inert_funeqs is) tf tys }
1734
1735 CTyEqCan { cc_tyvar = x, cc_rhs = ty } ->
1736 is { inert_eqs = delTyEq (inert_eqs is) x ty }
1737
1738 CIrredEvCan {} -> panic "removeInertCt: CIrredEvCan"
1739 CNonCanonical {} -> panic "removeInertCt: CNonCanonical"
1740 CHoleCan {} -> panic "removeInertCt: CHoleCan"
1741
1742
1743 lookupFlatCache :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcType, CtFlavour))
1744 lookupFlatCache fam_tc tys
1745 = do { IS { inert_flat_cache = flat_cache
1746 , inert_cans = IC { inert_funeqs = inert_funeqs } } <- getTcSInerts
1747 ; return (firstJusts [lookup_inerts inert_funeqs,
1748 lookup_flats flat_cache]) }
1749 where
1750 lookup_inerts inert_funeqs
1751 | Just (CFunEqCan { cc_ev = ctev, cc_fsk = fsk })
1752 <- findFunEqs inert_funeqs fam_tc tys
1753 = Just (ctEvCoercion ctev, mkTyVarTy fsk, ctEvFlavour ctev)
1754 | otherwise = Nothing
1755
1756 lookup_flats flat_cache = findFunEq flat_cache fam_tc tys
1757
1758
1759 lookupInInerts :: TcPredType -> TcS (Maybe CtEvidence)
1760 -- Is this exact predicate type cached in the solved or canonicals of the InertSet?
1761 lookupInInerts pty
1762 | ClassPred cls tys <- classifyPredType pty
1763 = do { inerts <- getTcSInerts
1764 ; return (lookupSolvedDict inerts cls tys `mplus`
1765 lookupInertDict (inert_cans inerts) cls tys) }
1766 | otherwise -- NB: No caching for equalities, IPs, holes, or errors
1767 = return Nothing
1768
1769 lookupInertDict :: InertCans -> Class -> [Type] -> Maybe CtEvidence
1770 lookupInertDict (IC { inert_dicts = dicts }) cls tys
1771 = case findDict dicts cls tys of
1772 Just ct -> Just (ctEvidence ct)
1773 _ -> Nothing
1774
1775 lookupSolvedDict :: InertSet -> Class -> [Type] -> Maybe CtEvidence
1776 -- Returns just if exactly this predicate type exists in the solved.
1777 lookupSolvedDict (IS { inert_solved_dicts = solved }) cls tys
1778 = case findDict solved cls tys of
1779 Just ev -> Just ev
1780 _ -> Nothing
1781
1782
1783 {- *********************************************************************
1784 * *
1785 Irreds
1786 * *
1787 ********************************************************************* -}
1788
1789 foldIrreds :: (Ct -> b -> b) -> Cts -> b -> b
1790 foldIrreds k irreds z = foldrBag k z irreds
1791
1792
1793 {- *********************************************************************
1794 * *
1795 Type equalities
1796 * *
1797 ********************************************************************* -}
1798
1799 type EqualCtList = [Ct]
1800
1801 {- Note [EqualCtList invariants]
1802 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1803 * All are equalities
1804 * All these equalities have the same LHS
1805 * The list is never empty
1806 * No element of the list can rewrite any other
1807
1808 From the fourth invariant it follows that the list is
1809 - A single Given, or
1810 - Any number of Wanteds and/or Deriveds
1811 -}
1812
1813 addTyEq :: TyVarEnv EqualCtList -> TcTyVar -> Ct -> TyVarEnv EqualCtList
1814 addTyEq old_list tv it = extendVarEnv_C (\old_eqs _new_eqs -> it : old_eqs)
1815 old_list tv [it]
1816
1817 foldTyEqs :: (Ct -> b -> b) -> TyVarEnv EqualCtList -> b -> b
1818 foldTyEqs k eqs z
1819 = foldVarEnv (\cts z -> foldr k z cts) z eqs
1820
1821 findTyEqs :: InertCans -> TyVar -> EqualCtList
1822 findTyEqs icans tv = lookupVarEnv (inert_eqs icans) tv `orElse` []
1823
1824 delTyEq :: TyVarEnv EqualCtList -> TcTyVar -> TcType -> TyVarEnv EqualCtList
1825 delTyEq m tv t = modifyVarEnv (filter (not . isThisOne)) m tv
1826 where isThisOne (CTyEqCan { cc_rhs = t1 }) = eqType t t1
1827 isThisOne _ = False
1828
1829 {- *********************************************************************
1830 * *
1831 TcAppMap
1832 * *
1833 ********************************************************************* -}
1834
1835 type TcAppMap a = UniqFM (ListMap TypeMap a)
1836 -- Indexed by tycon then the arg types
1837 -- Used for types and classes; hence UniqFM
1838
1839 isEmptyTcAppMap :: TcAppMap a -> Bool
1840 isEmptyTcAppMap m = isNullUFM m
1841
1842 emptyTcAppMap :: TcAppMap a
1843 emptyTcAppMap = emptyUFM
1844
1845 findTcApp :: TcAppMap a -> Unique -> [Type] -> Maybe a
1846 findTcApp m u tys = do { tys_map <- lookupUFM m u
1847 ; lookupTM tys tys_map }
1848
1849 delTcApp :: TcAppMap a -> Unique -> [Type] -> TcAppMap a
1850 delTcApp m cls tys = adjustUFM (deleteTM tys) m cls
1851
1852 insertTcApp :: TcAppMap a -> Unique -> [Type] -> a -> TcAppMap a
1853 insertTcApp m cls tys ct = alterUFM alter_tm m cls
1854 where
1855 alter_tm mb_tm = Just (insertTM tys ct (mb_tm `orElse` emptyTM))
1856
1857 -- mapTcApp :: (a->b) -> TcAppMap a -> TcAppMap b
1858 -- mapTcApp f = mapUFM (mapTM f)
1859
1860 filterTcAppMap :: (Ct -> Bool) -> TcAppMap Ct -> TcAppMap Ct
1861 filterTcAppMap f m
1862 = mapUFM do_tm m
1863 where
1864 do_tm tm = foldTM insert_mb tm emptyTM
1865 insert_mb ct tm
1866 | f ct = insertTM tys ct tm
1867 | otherwise = tm
1868 where
1869 tys = case ct of
1870 CFunEqCan { cc_tyargs = tys } -> tys
1871 CDictCan { cc_tyargs = tys } -> tys
1872 _ -> pprPanic "filterTcAppMap" (ppr ct)
1873
1874 tcAppMapToBag :: TcAppMap a -> Bag a
1875 tcAppMapToBag m = foldTcAppMap consBag m emptyBag
1876
1877 foldTcAppMap :: (a -> b -> b) -> TcAppMap a -> b -> b
1878 foldTcAppMap k m z = foldUFM (foldTM k) z m
1879
1880
1881 {- *********************************************************************
1882 * *
1883 DictMap
1884 * *
1885 ********************************************************************* -}
1886
1887 type DictMap a = TcAppMap a
1888
1889 emptyDictMap :: DictMap a
1890 emptyDictMap = emptyTcAppMap
1891
1892 -- sizeDictMap :: DictMap a -> Int
1893 -- sizeDictMap m = foldDicts (\ _ x -> x+1) m 0
1894
1895 findDict :: DictMap a -> Class -> [Type] -> Maybe a
1896 findDict m cls tys = findTcApp m (getUnique cls) tys
1897
1898 findDictsByClass :: DictMap a -> Class -> Bag a
1899 findDictsByClass m cls
1900 | Just tm <- lookupUFM m cls = foldTM consBag tm emptyBag
1901 | otherwise = emptyBag
1902
1903 delDict :: DictMap a -> Class -> [Type] -> DictMap a
1904 delDict m cls tys = delTcApp m (getUnique cls) tys
1905
1906 addDict :: DictMap a -> Class -> [Type] -> a -> DictMap a
1907 addDict m cls tys item = insertTcApp m (getUnique cls) tys item
1908
1909 addDictsByClass :: DictMap Ct -> Class -> Bag Ct -> DictMap Ct
1910 addDictsByClass m cls items
1911 = addToUFM m cls (foldrBag add emptyTM items)
1912 where
1913 add ct@(CDictCan { cc_tyargs = tys }) tm = insertTM tys ct tm
1914 add ct _ = pprPanic "addDictsByClass" (ppr ct)
1915
1916 filterDicts :: (Ct -> Bool) -> DictMap Ct -> DictMap Ct
1917 filterDicts f m = filterTcAppMap f m
1918
1919 partitionDicts :: (Ct -> Bool) -> DictMap Ct -> (Bag Ct, DictMap Ct)
1920 partitionDicts f m = foldTcAppMap k m (emptyBag, emptyDicts)
1921 where
1922 k ct (yeses, noes) | f ct = (ct `consBag` yeses, noes)
1923 | otherwise = (yeses, add ct noes)
1924 add ct@(CDictCan { cc_class = cls, cc_tyargs = tys }) m
1925 = addDict m cls tys ct
1926 add ct _ = pprPanic "partitionDicts" (ppr ct)
1927
1928 dictsToBag :: DictMap a -> Bag a
1929 dictsToBag = tcAppMapToBag
1930
1931 foldDicts :: (a -> b -> b) -> DictMap a -> b -> b
1932 foldDicts = foldTcAppMap
1933
1934 emptyDicts :: DictMap a
1935 emptyDicts = emptyTcAppMap
1936
1937
1938 {- *********************************************************************
1939 * *
1940 FunEqMap
1941 * *
1942 ********************************************************************* -}
1943
1944 type FunEqMap a = TcAppMap a -- A map whose key is a (TyCon, [Type]) pair
1945
1946 emptyFunEqs :: TcAppMap a
1947 emptyFunEqs = emptyTcAppMap
1948
1949 sizeFunEqMap :: FunEqMap a -> Int
1950 sizeFunEqMap m = foldFunEqs (\ _ x -> x+1) m 0
1951
1952 findFunEq :: FunEqMap a -> TyCon -> [Type] -> Maybe a
1953 findFunEq m tc tys = findTcApp m (getUnique tc) tys
1954
1955 findFunEqs :: FunEqMap a -> TyCon -> [Type] -> Maybe a
1956 findFunEqs m tc tys = findTcApp m (getUnique tc) tys
1957
1958 funEqsToBag :: FunEqMap a -> Bag a
1959 funEqsToBag m = foldTcAppMap consBag m emptyBag
1960
1961 findFunEqsByTyCon :: FunEqMap a -> TyCon -> [a]
1962 -- Get inert function equation constraints that have the given tycon
1963 -- in their head. Not that the constraints remain in the inert set.
1964 -- We use this to check for derived interactions with built-in type-function
1965 -- constructors.
1966 findFunEqsByTyCon m tc
1967 | Just tm <- lookupUFM m tc = foldTM (:) tm []
1968 | otherwise = []
1969
1970 foldFunEqs :: (a -> b -> b) -> FunEqMap a -> b -> b
1971 foldFunEqs = foldTcAppMap
1972
1973 -- mapFunEqs :: (a -> b) -> FunEqMap a -> FunEqMap b
1974 -- mapFunEqs = mapTcApp
1975
1976 filterFunEqs :: (Ct -> Bool) -> FunEqMap Ct -> FunEqMap Ct
1977 filterFunEqs = filterTcAppMap
1978
1979 insertFunEq :: FunEqMap a -> TyCon -> [Type] -> a -> FunEqMap a
1980 insertFunEq m tc tys val = insertTcApp m (getUnique tc) tys val
1981
1982 -- insertFunEqCt :: FunEqMap Ct -> Ct -> FunEqMap Ct
1983 -- insertFunEqCt m ct@(CFunEqCan { cc_fun = tc, cc_tyargs = tys })
1984 -- = insertFunEq m tc tys ct
1985 -- insertFunEqCt _ ct = pprPanic "insertFunEqCt" (ppr ct)
1986
1987 partitionFunEqs :: (Ct -> Bool) -> FunEqMap Ct -> ([Ct], FunEqMap Ct)
1988 -- Optimise for the case where the predicate is false
1989 -- partitionFunEqs is called only from kick-out, and kick-out usually
1990 -- kicks out very few equalities, so we want to optimise for that case
1991 partitionFunEqs f m = (yeses, foldr del m yeses)
1992 where
1993 yeses = foldTcAppMap k m []
1994 k ct yeses | f ct = ct : yeses
1995 | otherwise = yeses
1996 del (CFunEqCan { cc_fun = tc, cc_tyargs = tys }) m
1997 = delFunEq m tc tys
1998 del ct _ = pprPanic "partitionFunEqs" (ppr ct)
1999
2000 delFunEq :: FunEqMap a -> TyCon -> [Type] -> FunEqMap a
2001 delFunEq m tc tys = delTcApp m (getUnique tc) tys
2002
2003 {-
2004 ************************************************************************
2005 * *
2006 * The TcS solver monad *
2007 * *
2008 ************************************************************************
2009
2010 Note [The TcS monad]
2011 ~~~~~~~~~~~~~~~~~~~~
2012 The TcS monad is a weak form of the main Tc monad
2013
2014 All you can do is
2015 * fail
2016 * allocate new variables
2017 * fill in evidence variables
2018
2019 Filling in a dictionary evidence variable means to create a binding
2020 for it, so TcS carries a mutable location where the binding can be
2021 added. This is initialised from the innermost implication constraint.
2022 -}
2023
2024 data TcSEnv
2025 = TcSEnv {
2026 tcs_ev_binds :: EvBindsVar,
2027
2028 tcs_unified :: IORef Int,
2029 -- The number of unification variables we have filled
2030 -- The important thing is whether it is non-zero
2031
2032 tcs_count :: IORef Int, -- Global step count
2033
2034 tcs_inerts :: IORef InertSet, -- Current inert set
2035
2036 -- The main work-list and the flattening worklist
2037 -- See Note [Work list priorities] and
2038 tcs_worklist :: IORef WorkList -- Current worklist
2039 }
2040
2041 ---------------
2042 newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
2043
2044 instance Functor TcS where
2045 fmap f m = TcS $ fmap f . unTcS m
2046
2047 instance Applicative TcS where
2048 pure = return
2049 (<*>) = ap
2050
2051 instance Monad TcS where
2052 return x = TcS (\_ -> return x)
2053 fail err = TcS (\_ -> fail err)
2054 m >>= k = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
2055
2056 instance MonadUnique TcS where
2057 getUniqueSupplyM = wrapTcS getUniqueSupplyM
2058
2059 -- Basic functionality
2060 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2061 wrapTcS :: TcM a -> TcS a
2062 -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
2063 -- and TcS is supposed to have limited functionality
2064 wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
2065
2066 wrapErrTcS :: TcM a -> TcS a
2067 -- The thing wrapped should just fail
2068 -- There's no static check; it's up to the user
2069 -- Having a variant for each error message is too painful
2070 wrapErrTcS = wrapTcS
2071
2072 wrapWarnTcS :: TcM a -> TcS a
2073 -- The thing wrapped should just add a warning, or no-op
2074 -- There's no static check; it's up to the user
2075 wrapWarnTcS = wrapTcS
2076
2077 failTcS, panicTcS :: SDoc -> TcS a
2078 failTcS = wrapTcS . TcM.failWith
2079 panicTcS doc = pprPanic "TcCanonical" doc
2080
2081 traceTcS :: String -> SDoc -> TcS ()
2082 traceTcS herald doc = wrapTcS (TcM.traceTc herald doc)
2083
2084 runTcPluginTcS :: TcPluginM a -> TcS a
2085 runTcPluginTcS m = wrapTcS . runTcPluginM m . Just =<< getTcEvBinds
2086
2087 instance HasDynFlags TcS where
2088 getDynFlags = wrapTcS getDynFlags
2089
2090 getGlobalRdrEnvTcS :: TcS GlobalRdrEnv
2091 getGlobalRdrEnvTcS = wrapTcS TcM.getGlobalRdrEnv
2092
2093 bumpStepCountTcS :: TcS ()
2094 bumpStepCountTcS = TcS $ \env -> do { let ref = tcs_count env
2095 ; n <- TcM.readTcRef ref
2096 ; TcM.writeTcRef ref (n+1) }
2097
2098 csTraceTcS :: SDoc -> TcS ()
2099 csTraceTcS doc
2100 = wrapTcS $ csTraceTcM 1 (return doc)
2101
2102 traceFireTcS :: CtEvidence -> SDoc -> TcS ()
2103 -- Dump a rule-firing trace
2104 traceFireTcS ev doc
2105 = TcS $ \env -> csTraceTcM 1 $
2106 do { n <- TcM.readTcRef (tcs_count env)
2107 ; tclvl <- TcM.getTcLevel
2108 ; return (hang (int n <> brackets (ptext (sLit "U:") <> ppr tclvl
2109 <> ppr (ctLocDepth (ctEvLoc ev)))
2110 <+> doc <> colon)
2111 4 (ppr ev)) }
2112
2113 csTraceTcM :: Int -> TcM SDoc -> TcM ()
2114 -- Constraint-solver tracing, -ddump-cs-trace
2115 csTraceTcM trace_level mk_doc
2116 = do { dflags <- getDynFlags
2117 ; when ( (dopt Opt_D_dump_cs_trace dflags || dopt Opt_D_dump_tc_trace dflags)
2118 && trace_level <= traceLevel dflags ) $
2119 do { msg <- mk_doc
2120 ; TcM.traceTcRn Opt_D_dump_cs_trace msg } }
2121
2122 runTcS :: TcS a -- What to run
2123 -> TcM (a, Bag EvBind)
2124 runTcS tcs
2125 = do { ev_binds_var <- TcM.newTcEvBinds
2126 ; res <- runTcSWithEvBinds ev_binds_var tcs
2127 ; ev_binds <- TcM.getTcEvBinds ev_binds_var
2128 ; return (res, ev_binds) }
2129
2130 runTcSWithEvBinds :: EvBindsVar
2131 -> TcS a
2132 -> TcM a
2133 runTcSWithEvBinds ev_binds_var tcs
2134 = do { unified_var <- TcM.newTcRef 0
2135 ; step_count <- TcM.newTcRef 0
2136 ; inert_var <- TcM.newTcRef is
2137 ; wl_var <- TcM.newTcRef emptyWorkList
2138
2139 ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
2140 , tcs_unified = unified_var
2141 , tcs_count = step_count
2142 , tcs_inerts = inert_var
2143 , tcs_worklist = wl_var }
2144
2145 -- Run the computation
2146 ; res <- unTcS tcs env
2147
2148 ; count <- TcM.readTcRef step_count
2149 ; when (count > 0) $
2150 csTraceTcM 0 $ return (ptext (sLit "Constraint solver steps =") <+> int count)
2151
2152 #ifdef DEBUG
2153 ; ev_binds <- TcM.getTcEvBinds ev_binds_var
2154 ; checkForCyclicBinds ev_binds
2155 #endif
2156
2157 ; return res }
2158 where
2159 is = emptyInert
2160
2161 #ifdef DEBUG
2162 checkForCyclicBinds :: Bag EvBind -> TcM ()
2163 checkForCyclicBinds ev_binds
2164 | null cycles
2165 = return ()
2166 | null coercion_cycles
2167 = TcM.traceTc "Cycle in evidence binds" $ ppr cycles
2168 | otherwise
2169 = pprPanic "Cycle in coercion bindings" $ ppr coercion_cycles
2170 where
2171 cycles :: [[EvBind]]
2172 cycles = [c | CyclicSCC c <- stronglyConnCompFromEdgedVertices edges]
2173
2174 coercion_cycles = [c | c <- cycles, any is_co_bind c]
2175 is_co_bind (EvBind { eb_lhs = b }) = isEqVar b
2176
2177 edges :: [(EvBind, EvVar, [EvVar])]
2178 edges = [(bind, bndr, varSetElems (evVarsOfTerm rhs))
2179 | bind@(EvBind { eb_lhs = bndr, eb_rhs = rhs }) <- bagToList ev_binds]
2180 #endif
2181
2182 nestImplicTcS :: EvBindsVar -> TcLevel -> TcS a -> TcS a
2183 nestImplicTcS ref inner_tclvl (TcS thing_inside)
2184 = TcS $ \ TcSEnv { tcs_unified = unified_var
2185 , tcs_inerts = old_inert_var
2186 , tcs_count = count } ->
2187 do { inerts <- TcM.readTcRef old_inert_var
2188 ; let nest_inert = inerts { inert_flat_cache = emptyFunEqs }
2189 -- See Note [Do not inherit the flat cache]
2190 ; new_inert_var <- TcM.newTcRef nest_inert
2191 ; new_wl_var <- TcM.newTcRef emptyWorkList
2192 ; let nest_env = TcSEnv { tcs_ev_binds = ref
2193 , tcs_unified = unified_var
2194 , tcs_count = count
2195 , tcs_inerts = new_inert_var
2196 , tcs_worklist = new_wl_var }
2197 ; res <- TcM.setTcLevel inner_tclvl $
2198 thing_inside nest_env
2199
2200 #ifdef DEBUG
2201 -- Perform a check that the thing_inside did not cause cycles
2202 ; ev_binds <- TcM.getTcEvBinds ref
2203 ; checkForCyclicBinds ev_binds
2204 #endif
2205
2206 ; return res }
2207
2208 {- Note [Do not inherit the flat cache]
2209 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2210 We do not want to inherit the flat cache when processing nested
2211 implications. Consider
2212 a ~ F b, forall c. b~Int => blah
2213 If we have F b ~ fsk in the flat-cache, and we push that into the
2214 nested implication, we might miss that F b can be rewritten to F Int,
2215 and hence perhpas solve it. Moreover, the fsk from outside is
2216 flattened out after solving the outer level, but and we don't
2217 do that flattening recursively.
2218 -}
2219
2220
2221 recoverTcS :: TcS a -> TcS a -> TcS a
2222 recoverTcS (TcS recovery_code) (TcS thing_inside)
2223 = TcS $ \ env ->
2224 TcM.recoverM (recovery_code env) (thing_inside env)
2225
2226 nestTcS :: TcS a -> TcS a
2227 -- Use the current untouchables, augmenting the current
2228 -- evidence bindings, and solved dictionaries
2229 -- But have no effect on the InertCans, or on the inert_flat_cache
2230 -- (the latter because the thing inside a nestTcS does unflattening)
2231 nestTcS (TcS thing_inside)
2232 = TcS $ \ env@(TcSEnv { tcs_inerts = inerts_var }) ->
2233 do { inerts <- TcM.readTcRef inerts_var
2234 ; new_inert_var <- TcM.newTcRef inerts
2235 ; new_wl_var <- TcM.newTcRef emptyWorkList
2236 ; let nest_env = env { tcs_inerts = new_inert_var
2237 , tcs_worklist = new_wl_var }
2238
2239 ; res <- thing_inside nest_env
2240
2241 ; new_inerts <- TcM.readTcRef new_inert_var
2242
2243 -- we want to propogate the safe haskell failures
2244 ; let old_ic = inert_cans inerts
2245 new_ic = inert_cans new_inerts
2246 nxt_ic = old_ic { inert_safehask = inert_safehask new_ic }
2247
2248 ; TcM.writeTcRef inerts_var -- See Note [Propagate the solved dictionaries]
2249 (inerts { inert_solved_dicts = inert_solved_dicts new_inerts
2250 , inert_cans = nxt_ic })
2251
2252 ; return res }
2253
2254 tryTcS :: TcS a -> TcS a
2255 -- Like runTcS, but from within the TcS monad
2256 -- Completely fresh inerts and worklist, be careful!
2257 -- Moreover, we will simply throw away all the evidence generated.
2258 tryTcS (TcS thing_inside)
2259 = TcS $ \env ->
2260 do { is_var <- TcM.newTcRef emptyInert
2261 ; unified_var <- TcM.newTcRef 0
2262 ; ev_binds_var <- TcM.newTcEvBinds
2263 ; wl_var <- TcM.newTcRef emptyWorkList
2264 ; let nest_env = env { tcs_ev_binds = ev_binds_var
2265 , tcs_unified = unified_var
2266 , tcs_inerts = is_var
2267 , tcs_worklist = wl_var }
2268 ; thing_inside nest_env }
2269
2270 {-
2271 Note [Propagate the solved dictionaries]
2272 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2273 It's really quite important that nestTcS does not discard the solved
2274 dictionaries from the thing_inside.
2275 Consider
2276 Eq [a]
2277 forall b. empty => Eq [a]
2278 We solve the simple (Eq [a]), under nestTcS, and then turn our attention to
2279 the implications. It's definitely fine to use the solved dictionaries on
2280 the inner implications, and it can make a signficant performance difference
2281 if you do so.
2282 -}
2283
2284 -- Getters and setters of TcEnv fields
2285 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2286
2287 -- Getter of inerts and worklist
2288 getTcSInertsRef :: TcS (IORef InertSet)
2289 getTcSInertsRef = TcS (return . tcs_inerts)
2290
2291 getTcSWorkListRef :: TcS (IORef WorkList)
2292 getTcSWorkListRef = TcS (return . tcs_worklist)
2293
2294 getTcSInerts :: TcS InertSet
2295 getTcSInerts = getTcSInertsRef >>= wrapTcS . (TcM.readTcRef)
2296
2297 setTcSInerts :: InertSet -> TcS ()
2298 setTcSInerts ics = do { r <- getTcSInertsRef; wrapTcS (TcM.writeTcRef r ics) }
2299
2300 getWorkListImplics :: TcS (Bag Implication)
2301 getWorkListImplics
2302 = do { wl_var <- getTcSWorkListRef
2303 ; wl_curr <- wrapTcS (TcM.readTcRef wl_var)
2304 ; return (wl_implics wl_curr) }
2305
2306 updWorkListTcS :: (WorkList -> WorkList) -> TcS ()
2307 updWorkListTcS f
2308 = do { wl_var <- getTcSWorkListRef
2309 ; wl_curr <- wrapTcS (TcM.readTcRef wl_var)
2310 ; let new_work = f wl_curr
2311 ; wrapTcS (TcM.writeTcRef wl_var new_work) }
2312
2313 emitWorkNC :: [CtEvidence] -> TcS ()
2314 emitWorkNC evs
2315 | null evs
2316 = return ()
2317 | otherwise
2318 = do { traceTcS "Emitting fresh work" (vcat (map ppr evs))
2319 ; updWorkListTcS (extendWorkListCts (map mkNonCanonical evs)) }
2320
2321 emitWorkCt :: Ct -> TcS ()
2322 emitWorkCt ct
2323 = do { traceTcS "Emitting fresh (canonical) work" (ppr ct)
2324 ; updWorkListTcS (extendWorkListCt ct) }
2325
2326 emitInsoluble :: Ct -> TcS ()
2327 -- Emits a non-canonical constraint that will stand for a frozen error in the inerts.
2328 emitInsoluble ct
2329 = do { traceTcS "Emit insoluble" (ppr ct)
2330 ; updInertTcS add_insol }
2331 where
2332 this_pred = ctPred ct
2333 add_insol is@(IS { inert_cans = ics@(IC { inert_insols = old_insols }) })
2334 | already_there = is
2335 | otherwise = is { inert_cans = ics { inert_insols = old_insols `snocCts` ct } }
2336 where
2337 already_there = not (isWantedCt ct) && anyBag (tcEqType this_pred . ctPred) old_insols
2338 -- See Note [Do not add duplicate derived insolubles]
2339
2340 newTcRef :: a -> TcS (TcRef a)
2341 newTcRef x = wrapTcS (TcM.newTcRef x)
2342
2343 readTcRef :: TcRef a -> TcS a
2344 readTcRef ref = wrapTcS (TcM.readTcRef ref)
2345
2346 updTcRef :: TcRef a -> (a->a) -> TcS ()
2347 updTcRef ref upd_fn = wrapTcS (TcM.updTcRef ref upd_fn)
2348
2349 getTcEvBinds :: TcS EvBindsVar
2350 getTcEvBinds = TcS (return . tcs_ev_binds)
2351
2352 getTcLevel :: TcS TcLevel
2353 getTcLevel = wrapTcS TcM.getTcLevel
2354
2355 getTcEvBindsMap :: TcS EvBindMap
2356 getTcEvBindsMap
2357 = do { EvBindsVar ev_ref _ <- getTcEvBinds
2358 ; wrapTcS $ TcM.readTcRef ev_ref }
2359
2360 unifyTyVar :: TcTyVar -> TcType -> TcS ()
2361 -- Unify a meta-tyvar with a type
2362 -- We keep track of how many unifications have happened in tcs_unified,
2363 --
2364 -- We should never unify the same variable twice!
2365 unifyTyVar tv ty
2366 = ASSERT2( isMetaTyVar tv, ppr tv )
2367 TcS $ \ env ->
2368 do { TcM.traceTc "unifyTyVar" (ppr tv <+> text ":=" <+> ppr ty)
2369 ; TcM.writeMetaTyVar tv ty
2370 ; TcM.updTcRef (tcs_unified env) (+ 1) }
2371
2372 unflattenFmv :: TcTyVar -> TcType -> TcS ()
2373 -- Fill a flatten-meta-var, simply by unifying it.
2374 -- This does NOT count as a unification in tcs_unified.
2375 unflattenFmv tv ty
2376 = ASSERT2( isMetaTyVar tv, ppr tv )
2377 TcS $ \ _ ->
2378 do { TcM.traceTc "unflattenFmv" (ppr tv <+> text ":=" <+> ppr ty)
2379 ; TcM.writeMetaTyVar tv ty }
2380
2381 reportUnifications :: TcS a -> TcS (Int, a)
2382 reportUnifications (TcS thing_inside)
2383 = TcS $ \ env ->
2384 do { inner_unified <- TcM.newTcRef 0
2385 ; res <- thing_inside (env { tcs_unified = inner_unified })
2386 ; n_unifs <- TcM.readTcRef inner_unified
2387 ; TcM.updTcRef (tcs_unified env) (+ n_unifs) -- Inner unifications affect
2388 ; return (n_unifs, res) } -- the outer scope too
2389
2390 getDefaultInfo :: TcS ([Type], (Bool, Bool))
2391 getDefaultInfo = wrapTcS TcM.tcGetDefaultTys
2392
2393 -- Just get some environments needed for instance looking up and matching
2394 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2395
2396 getInstEnvs :: TcS InstEnvs
2397 getInstEnvs = wrapTcS $ TcM.tcGetInstEnvs
2398
2399 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
2400 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
2401
2402 getTopEnv :: TcS HscEnv
2403 getTopEnv = wrapTcS $ TcM.getTopEnv
2404
2405 getGblEnv :: TcS TcGblEnv
2406 getGblEnv = wrapTcS $ TcM.getGblEnv
2407
2408 -- Setting names as used (used in the deriving of Coercible evidence)
2409 -- Too hackish to expose it to TcS? In that case somehow extract the used
2410 -- constructors from the result of solveInteract
2411 addUsedRdrNamesTcS :: [RdrName] -> TcS ()
2412 addUsedRdrNamesTcS names = wrapTcS $ addUsedRdrNames names
2413
2414 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
2415 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2416
2417 checkWellStagedDFun :: PredType -> DFunId -> CtLoc -> TcS ()
2418 checkWellStagedDFun pred dfun_id loc
2419 = wrapTcS $ TcM.setCtLoc loc $
2420 do { use_stage <- TcM.getStage
2421 ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
2422 where
2423 pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
2424 bind_lvl = TcM.topIdLvl dfun_id
2425
2426 pprEq :: TcType -> TcType -> SDoc
2427 pprEq ty1 ty2 = pprParendType ty1 <+> char '~' <+> pprParendType ty2
2428
2429 isTouchableMetaTyVarTcS :: TcTyVar -> TcS Bool
2430 isTouchableMetaTyVarTcS tv
2431 = do { tclvl <- getTcLevel
2432 ; return $ isTouchableMetaTyVar tclvl tv }
2433
2434 isFilledMetaTyVar_maybe :: TcTyVar -> TcS (Maybe Type)
2435 isFilledMetaTyVar_maybe tv
2436 = ASSERT2( isTcTyVar tv, ppr tv )
2437 case tcTyVarDetails tv of
2438 MetaTv { mtv_ref = ref }
2439 -> do { cts <- wrapTcS (TcM.readTcRef ref)
2440 ; case cts of
2441 Indirect ty -> return (Just ty)
2442 Flexi -> return Nothing }
2443 _ -> return Nothing
2444
2445 isFilledMetaTyVar :: TcTyVar -> TcS Bool
2446 isFilledMetaTyVar tv = wrapTcS (TcM.isFilledMetaTyVar tv)
2447
2448 zonkTyVarsAndFV :: TcTyVarSet -> TcS TcTyVarSet
2449 zonkTyVarsAndFV tvs = wrapTcS (TcM.zonkTyVarsAndFV tvs)
2450
2451 zonkTcType :: TcType -> TcS TcType
2452 zonkTcType ty = wrapTcS (TcM.zonkTcType ty)
2453
2454 zonkTcTypes :: [TcType] -> TcS [TcType]
2455 zonkTcTypes tys = wrapTcS (TcM.zonkTcTypes tys)
2456
2457 zonkTcTyVar :: TcTyVar -> TcS TcType
2458 zonkTcTyVar tv = wrapTcS (TcM.zonkTcTyVar tv)
2459
2460 zonkSimples :: Cts -> TcS Cts
2461 zonkSimples cts = wrapTcS (TcM.zonkSimples cts)
2462
2463 zonkWC :: WantedConstraints -> TcS WantedConstraints
2464 zonkWC wc = wrapTcS (TcM.zonkWC wc)
2465
2466 {-
2467 Note [Do not add duplicate derived insolubles]
2468 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2469 In general we *must* add an insoluble (Int ~ Bool) even if there is
2470 one such there already, because they may come from distinct call
2471 sites. Not only do we want an error message for each, but with
2472 -fdefer-type-errors we must generate evidence for each. But for
2473 *derived* insolubles, we only want to report each one once. Why?
2474
2475 (a) A constraint (C r s t) where r -> s, say, may generate the same fundep
2476 equality many times, as the original constraint is sucessively rewritten.
2477
2478 (b) Ditto the successive iterations of the main solver itself, as it traverses
2479 the constraint tree. See example below.
2480
2481 Also for *given* insolubles we may get repeated errors, as we
2482 repeatedly traverse the constraint tree. These are relatively rare
2483 anyway, so removing duplicates seems ok. (Alternatively we could take
2484 the SrcLoc into account.)
2485
2486 Note that the test does not need to be particularly efficient because
2487 it is only used if the program has a type error anyway.
2488
2489 Example of (b): assume a top-level class and instance declaration:
2490
2491 class D a b | a -> b
2492 instance D [a] [a]
2493
2494 Assume we have started with an implication:
2495
2496 forall c. Eq c => { wc_simple = D [c] c [W] }
2497
2498 which we have simplified to:
2499
2500 forall c. Eq c => { wc_simple = D [c] c [W]
2501 , wc_insols = (c ~ [c]) [D] }
2502
2503 For some reason, e.g. because we floated an equality somewhere else,
2504 we might try to re-solve this implication. If we do not do a
2505 dropDerivedWC, then we will end up trying to solve the following
2506 constraints the second time:
2507
2508 (D [c] c) [W]
2509 (c ~ [c]) [D]
2510
2511 which will result in two Deriveds to end up in the insoluble set:
2512
2513 wc_simple = D [c] c [W]
2514 wc_insols = (c ~ [c]) [D], (c ~ [c]) [D]
2515 -}
2516
2517 -- Flatten skolems
2518 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2519 newFlattenSkolem :: CtFlavour -> CtLoc
2520 -> TcType -- F xis
2521 -> TcS (CtEvidence, TcTyVar) -- [W] x:: F xis ~ fsk
2522 newFlattenSkolem Given loc fam_ty
2523 = do { fsk <- newFsk fam_ty
2524 ; ev <- newGivenEvVar loc (mkTcEqPred fam_ty (mkTyVarTy fsk),
2525 EvCoercion (mkTcNomReflCo fam_ty))
2526 ; return (ev, fsk) }
2527
2528 newFlattenSkolem Wanted loc fam_ty
2529 = do { fmv <- newFmv fam_ty
2530 ; ev <- newWantedEvVarNC loc (mkTcEqPred fam_ty (mkTyVarTy fmv))
2531 ; return (ev, fmv) }
2532
2533 newFlattenSkolem Derived loc fam_ty
2534 = do { fmv <- newFmv fam_ty
2535 ; ev <- newDerivedNC loc (mkTcEqPred fam_ty (mkTyVarTy fmv))
2536 ; return (ev, fmv) }
2537
2538 newFsk, newFmv :: TcType -> TcS TcTyVar
2539 newFsk fam_ty
2540 = wrapTcS $ do { uniq <- TcM.newUnique
2541 ; let name = TcM.mkTcTyVarName uniq (fsLit "fsk")
2542 ; return (mkTcTyVar name (typeKind fam_ty) (FlatSkol fam_ty)) }
2543
2544 newFmv fam_ty
2545 = wrapTcS $ do { uniq <- TcM.newUnique
2546 ; ref <- TcM.newMutVar Flexi
2547 ; cur_lvl <- TcM.getTcLevel
2548 ; let details = MetaTv { mtv_info = FlatMetaTv
2549 , mtv_ref = ref
2550 , mtv_tclvl = fmvTcLevel cur_lvl }
2551 name = TcM.mkTcTyVarName uniq (fsLit "s")
2552 ; return (mkTcTyVar name (typeKind fam_ty) details) }
2553
2554 extendFlatCache :: TyCon -> [Type] -> (TcCoercion, TcType, CtFlavour) -> TcS ()
2555 extendFlatCache tc xi_args stuff
2556 = do { dflags <- getDynFlags
2557 ; when (gopt Opt_FlatCache dflags) $
2558 updInertTcS $ \ is@(IS { inert_flat_cache = fc }) ->
2559 is { inert_flat_cache = insertFunEq fc tc xi_args stuff } }
2560
2561 -- Instantiations
2562 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2563
2564 instDFunType :: DFunId -> [DFunInstType] -> TcS ([TcType], TcThetaType)
2565 instDFunType dfun_id inst_tys
2566 = wrapTcS $ TcM.instDFunType dfun_id inst_tys
2567
2568 newFlexiTcSTy :: Kind -> TcS TcType
2569 newFlexiTcSTy knd = wrapTcS (TcM.newFlexiTyVarTy knd)
2570
2571 cloneMetaTyVar :: TcTyVar -> TcS TcTyVar
2572 cloneMetaTyVar tv = wrapTcS (TcM.cloneMetaTyVar tv)
2573
2574 demoteUnfilledFmv :: TcTyVar -> TcS ()
2575 -- If a flatten-meta-var is still un-filled,
2576 -- turn it into an ordinary meta-var
2577 demoteUnfilledFmv fmv
2578 = wrapTcS $ do { is_filled <- TcM.isFilledMetaTyVar fmv
2579 ; unless is_filled $
2580 do { tv_ty <- TcM.newFlexiTyVarTy (tyVarKind fmv)
2581 ; TcM.writeMetaTyVar fmv tv_ty } }
2582
2583 instFlexiTcS :: [TKVar] -> TcS (TvSubst, [TcType])
2584 instFlexiTcS tvs = wrapTcS (mapAccumLM inst_one emptyTvSubst tvs)
2585 where
2586 inst_one subst tv
2587 = do { ty' <- instFlexiTcSHelper (tyVarName tv)
2588 (substTy subst (tyVarKind tv))
2589 ; return (extendTvSubst subst tv ty', ty') }
2590
2591 instFlexiTcSHelper :: Name -> Kind -> TcM TcType
2592 instFlexiTcSHelper tvname kind
2593 = do { uniq <- TcM.newUnique
2594 ; details <- TcM.newMetaDetails (TauTv False)
2595 ; let name = setNameUnique tvname uniq
2596 ; return (mkTyVarTy (mkTcTyVar name kind details)) }
2597
2598 instFlexiTcSHelperTcS :: Name -> Kind -> TcS TcType
2599 instFlexiTcSHelperTcS n k = wrapTcS (instFlexiTcSHelper n k)
2600
2601
2602 -- Creating and setting evidence variables and CtFlavors
2603 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2604
2605 data Freshness = Fresh | Cached
2606
2607 isFresh :: Freshness -> Bool
2608 isFresh Fresh = True
2609 isFresh Cached = False
2610
2611 freshGoals :: [(CtEvidence, Freshness)] -> [CtEvidence]
2612 freshGoals mns = [ ctev | (ctev, Fresh) <- mns ]
2613
2614 setEvBind :: EvBind -> TcS ()
2615 setEvBind ev_bind
2616 = do { tc_evbinds <- getTcEvBinds
2617 ; wrapTcS $ TcM.addTcEvBind tc_evbinds ev_bind }
2618
2619 setWantedEvBind :: EvVar -> EvTerm -> TcS ()
2620 setWantedEvBind ev_id tm = setEvBind (mkWantedEvBind ev_id tm)
2621
2622 setEvBindIfWanted :: CtEvidence -> EvTerm -> TcS ()
2623 setEvBindIfWanted ev tm
2624 = case ev of
2625 CtWanted { ctev_evar = ev_id } -> setWantedEvBind ev_id tm
2626 _ -> return ()
2627
2628 newTcEvBinds :: TcS EvBindsVar
2629 newTcEvBinds = wrapTcS TcM.newTcEvBinds
2630
2631 newEvVar :: TcPredType -> TcS EvVar
2632 newEvVar pred = wrapTcS (TcM.newEvVar pred)
2633
2634 newGivenEvVar :: CtLoc -> (TcPredType, EvTerm) -> TcS CtEvidence
2635 -- Make a new variable of the given PredType,
2636 -- immediately bind it to the given term
2637 -- and return its CtEvidence
2638 -- See Note [Bind new Givens immediately] in TcRnTypes
2639 -- Precondition: this is not a kind equality
2640 -- See Note [Do not create Given kind equalities]
2641 newGivenEvVar loc (pred, rhs)
2642 = ASSERT2( not (isKindEquality pred), ppr pred $$ pprCtOrigin (ctLocOrigin loc) )
2643 do { -- checkReductionDepth loc pred
2644 ; new_ev <- newEvVar pred
2645 ; setEvBind (mkGivenEvBind new_ev rhs)
2646 ; return (CtGiven { ctev_pred = pred, ctev_evar = new_ev, ctev_loc = loc }) }
2647
2648 newGivenEvVars :: CtLoc -> [(TcPredType, EvTerm)] -> TcS [CtEvidence]
2649 -- Like newGivenEvVar, but automatically discard kind equalities
2650 -- See Note [Do not create Given kind equalities]
2651 newGivenEvVars loc pts = mapM (newGivenEvVar loc) (filterOut (isKindEquality . fst) pts)
2652
2653 isKindEquality :: TcPredType -> Bool
2654 -- See Note [Do not create Given kind equalities]
2655 isKindEquality pred = case classifyPredType pred of
2656 EqPred _ t1 _ -> isKind t1
2657 _ -> False
2658
2659 {- Note [Do not create Given kind equalities]
2660 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2661 We do not want to create a Given kind equality like
2662
2663 [G] kv ~ k -- kv is a skolem kind variable
2664 -- Reason we don't yet support non-Refl kind equalities
2665
2666 This showed up in Trac #8566, where we had a data type
2667 data I (u :: U *) (r :: [*]) :: * where
2668 A :: I (AA t as) r -- Existential k
2669 so A has type
2670 A :: forall (u:U *) (r:[*]) Universal
2671 (k:BOX) (t:k) (as:[U *]). Existential
2672 (u ~ AA * k t as) => I u r
2673
2674 There is no direct kind equality, but in a pattern match where 'u' is
2675 instantiated to, say, (AA * kk (t1:kk) as1), we'd decompose to get
2676 k ~ kk, t ~ t1, as ~ as1
2677 This is bad. We "fix" this by simply ignoring the Given kind equality
2678 But the Right Thing is to add kind equalities!
2679
2680 But note (Trac #8705) that we *do* create Given (non-canonical) equalities
2681 with un-equal kinds, e.g.
2682 [G] t1::k1 ~ t2::k2 -- k1 and k2 are un-equal kinds
2683 Reason: k1 or k2 might be unification variables that have already been
2684 unified (at this point we have not canonicalised the types), so we want
2685 to emit this t1~t2 as a (non-canonical) Given in the work-list. If k1/k2
2686 have been unified, we'll find that when we canonicalise it, and the
2687 t1~t2 information may be crucial (Trac #8705 is an example).
2688
2689 If it turns out that k1 and k2 are really un-equal, then it'll end up
2690 as an Irreducible (see Note [Equalities with incompatible kinds] in
2691 TcCanonical), and will do no harm.
2692 -}
2693
2694 newWantedEvVarNC :: CtLoc -> TcPredType -> TcS CtEvidence
2695 -- Don't look up in the solved/inerts; we know it's not there
2696 newWantedEvVarNC loc pty
2697 = do { -- checkReductionDepth loc pty
2698 ; new_ev <- newEvVar pty
2699 ; return (CtWanted { ctev_pred = pty, ctev_evar = new_ev, ctev_loc = loc })}
2700
2701 newWantedEvVar :: CtLoc -> TcPredType -> TcS (CtEvidence, Freshness)
2702 -- For anything except ClassPred, this is the same as newWantedEvVarNC
2703 newWantedEvVar loc pty
2704 = do { mb_ct <- lookupInInerts pty
2705 ; case mb_ct of
2706 Just ctev | not (isDerived ctev)
2707 -> do { traceTcS "newWantedEvVar/cache hit" $ ppr ctev
2708 ; return (ctev, Cached) }
2709 _ -> do { ctev <- newWantedEvVarNC loc pty
2710 ; traceTcS "newWantedEvVar/cache miss" $ ppr ctev
2711 ; return (ctev, Fresh) } }
2712
2713 emitNewDerived :: CtLoc -> TcPredType -> TcS ()
2714 emitNewDerived loc pred
2715 = do { ev <- newDerivedNC loc pred
2716 ; traceTcS "Emitting new derived" (ppr ev)
2717 ; updWorkListTcS (extendWorkListDerived loc ev) }
2718
2719 emitNewDeriveds :: CtLoc -> [TcPredType] -> TcS ()
2720 emitNewDeriveds loc preds
2721 | null preds
2722 = return ()
2723 | otherwise
2724 = do { evs <- mapM (newDerivedNC loc) preds
2725 ; traceTcS "Emitting new deriveds" (ppr evs)
2726 ; updWorkListTcS (extendWorkListDeriveds loc evs) }
2727
2728 emitNewDerivedEq :: CtLoc -> TcPredType -> TcS ()
2729 -- Create new equality Derived and put it in the work list
2730 -- There's no caching, no lookupInInerts
2731 emitNewDerivedEq loc pred
2732 = do { ev <- newDerivedNC loc pred
2733 ; traceTcS "Emitting new derived equality" (ppr ev)
2734 ; updWorkListTcS (extendWorkListDerived loc ev) }
2735
2736 newDerivedNC :: CtLoc -> TcPredType -> TcS CtEvidence
2737 newDerivedNC loc pred
2738 = do { -- checkReductionDepth loc pred
2739 ; return (CtDerived { ctev_pred = pred, ctev_loc = loc }) }
2740
2741 -- --------- Check done in TcInteract.selectNewWorkItem???? ---------
2742 -- | Checks if the depth of the given location is too much. Fails if
2743 -- it's too big, with an appropriate error message.
2744 checkReductionDepth :: CtLoc -> TcType -- ^ type being reduced
2745 -> TcS ()
2746 checkReductionDepth loc ty
2747 = do { dflags <- getDynFlags
2748 ; when (subGoalDepthExceeded dflags (ctLocDepth loc)) $
2749 wrapErrTcS $
2750 solverDepthErrorTcS loc ty }
2751
2752 matchFam :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcType))
2753 matchFam tycon args = wrapTcS $ matchFamTcM tycon args
2754
2755 matchFamTcM :: TyCon -> [Type] -> TcM (Maybe (TcCoercion, TcType))
2756 -- Given (F tys) return (ty, co), where co :: F tys ~ ty
2757 matchFamTcM tycon args
2758 = do { fam_envs <- FamInst.tcGetFamInstEnvs
2759 ; return $ fmap (first TcCoercion) $
2760 reduceTyFamApp_maybe fam_envs Nominal tycon args }
2761
2762 {-
2763 Note [Residual implications]
2764 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2765 The wl_implics in the WorkList are the residual implication
2766 constraints that are generated while solving or canonicalising the
2767 current worklist. Specifically, when canonicalising
2768 (forall a. t1 ~ forall a. t2)
2769 from which we get the implication
2770 (forall a. t1 ~ t2)
2771 See TcSMonad.deferTcSForAllEq
2772 -}
2773
2774 -- Deferring forall equalities as implications
2775 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2776
2777 deferTcSForAllEq :: Role -- Nominal or Representational
2778 -> CtLoc -- Original wanted equality flavor
2779 -> ([TyVar],TcType) -- ForAll tvs1 body1
2780 -> ([TyVar],TcType) -- ForAll tvs2 body2
2781 -> TcS EvTerm
2782 -- Some of this functionality is repeated from TcUnify,
2783 -- consider having a single place where we create fresh implications.
2784 deferTcSForAllEq role loc (tvs1,body1) (tvs2,body2)
2785 = do { (subst1, skol_tvs) <- wrapTcS $ TcM.tcInstSkolTyVars tvs1
2786 ; let tys = mkTyVarTys skol_tvs
2787 phi1 = Type.substTy subst1 body1
2788 phi2 = Type.substTy (zipTopTvSubst tvs2 tys) body2
2789 skol_info = UnifyForAllSkol skol_tvs phi1
2790 eq_pred = case role of
2791 Nominal -> mkTcEqPred phi1 phi2
2792 Representational -> mkCoerciblePred phi1 phi2
2793 Phantom -> panic "deferTcSForAllEq Phantom"
2794 ; (ctev, freshness) <- newWantedEvVar loc eq_pred
2795 ; coe_inside <- case freshness of
2796 Cached -> return (ctEvCoercion ctev)
2797 Fresh -> do { ev_binds_var <- newTcEvBinds
2798 ; env <- wrapTcS $ TcM.getLclEnv
2799 ; let ev_binds = TcEvBinds ev_binds_var
2800 new_ct = mkNonCanonical ctev
2801 new_co = ctEvCoercion ctev
2802 new_tclvl = pushTcLevel (tcl_tclvl env)
2803 ; let wc = WC { wc_simple = singleCt new_ct
2804 , wc_impl = emptyBag
2805 , wc_insol = emptyCts }
2806 imp = Implic { ic_tclvl = new_tclvl
2807 , ic_skols = skol_tvs
2808 , ic_no_eqs = True
2809 , ic_given = []
2810 , ic_wanted = wc
2811 , ic_status = IC_Unsolved
2812 , ic_binds = ev_binds_var
2813 , ic_env = env
2814 , ic_info = skol_info }
2815 ; updWorkListTcS (extendWorkListImplic imp)
2816 ; return (TcLetCo ev_binds new_co) }
2817
2818 ; return $ EvCoercion (foldr mkTcForAllCo coe_inside skol_tvs) }
2819