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