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