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