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