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