Typos in comments [skip ci]
[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.kickOutRewriteable
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 rewriteableTyVars
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_ct insols
1499 -- Kick out even insolubles; see Note [Kick out insolubles]
1500
1501 fr_may_rewrite :: CtFlavourRole -> Bool
1502 fr_may_rewrite fs = new_fr `eqMayRewriteFR` fs
1503 -- Can the new item rewrite the inert item?
1504
1505 kick_out_ct :: Ct -> Bool
1506 -- Kick it out if the new CTyEqCan can rewrite the inert
1507 -- one. See Note [kickOutRewritable]
1508 -- Or if it has no shadow and the shadow
1509 kick_out_ct ct = kick_out_ev (ctEvidence ct)
1510
1511 kick_out_ev :: CtEvidence -> Bool
1512 -- Kick it out if the new CTyEqCan can rewrite the inert
1513 -- one. See Note [kickOutRewritable]
1514 kick_out_ev ev = fr_may_rewrite (ctEvFlavourRole ev)
1515 && new_tv `elemVarSet` rewritableTyVarsOfType (ctEvPred ev)
1516 -- NB: this includes the fsk of a CFunEqCan. It can't
1517 -- actually be rewritten, but we need to kick it out
1518 -- so we get to take advantage of injectivity
1519 -- See Note [Kicking out CFunEqCan for fundeps]
1520
1521 kick_out_eqs :: EqualCtList -> ([Ct], DTyVarEnv EqualCtList)
1522 -> ([Ct], DTyVarEnv EqualCtList)
1523 kick_out_eqs eqs (acc_out, acc_in)
1524 = (eqs_out ++ acc_out, case eqs_in of
1525 [] -> acc_in
1526 (eq1:_) -> extendDVarEnv acc_in (cc_tyvar eq1) eqs_in)
1527 where
1528 (eqs_in, eqs_out) = partition keep_eq eqs
1529
1530 -- Implements criteria K1-K3 in Note [Extending the inert equalities]
1531 keep_eq (CTyEqCan { cc_tyvar = tv, cc_rhs = rhs_ty, cc_ev = ev
1532 , cc_eq_rel = eq_rel })
1533 | tv == new_tv
1534 = not (fr_may_rewrite fs) -- (K1)
1535
1536 | otherwise
1537 = check_k2 && check_k3
1538 where
1539 fs = ctEvFlavourRole ev
1540 check_k2 = not (fs `eqMayRewriteFR` fs) -- (K2a)
1541 || (fs `eqMayRewriteFR` new_fr) -- (K2b)
1542 || not (fr_may_rewrite fs) -- (K2c)
1543 || not (new_tv `elemVarSet` tyCoVarsOfType rhs_ty) -- (K2d)
1544
1545 check_k3
1546 | fr_may_rewrite fs
1547 = case eq_rel of
1548 NomEq -> not (rhs_ty `eqType` mkTyVarTy new_tv)
1549 ReprEq -> not (isTyVarExposed new_tv rhs_ty)
1550
1551 | otherwise
1552 = True
1553
1554 keep_eq ct = pprPanic "keep_eq" (ppr ct)
1555
1556 kickOutAfterUnification :: TcTyVar -> TcS Int
1557 kickOutAfterUnification new_tv
1558 = do { ics <- getInertCans
1559 ; (n_kicked, ics2) <- kickOutRewritable (Given,NomEq)
1560 new_tv ics
1561 -- Given because the tv := xi is given; NomEq because
1562 -- only nominal equalities are solved by unification
1563
1564 ; setInertCans ics2
1565 ; return n_kicked }
1566
1567 {- Note [kickOutRewritable]
1568 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1569 See also Note [inert_eqs: the inert equalities].
1570
1571 When we add a new inert equality (a ~N ty) to the inert set,
1572 we must kick out any inert items that could be rewritten by the
1573 new equality, to maintain the inert-set invariants.
1574
1575 - We want to kick out an existing inert constraint if
1576 a) the new constraint can rewrite the inert one
1577 b) 'a' is free in the inert constraint (so that it *will*)
1578 rewrite it if we kick it out.
1579
1580 For (b) we use tyCoVarsOfCt, which returns the type variables /and
1581 the kind variables/ that are directly visible in the type. Hence
1582 we will have exposed all the rewriting we care about to make the
1583 most precise kinds visible for matching classes etc. No need to
1584 kick out constraints that mention type variables whose kinds
1585 contain this variable!
1586
1587 - A Derived equality can kick out [D] constraints in inert_eqs,
1588 inert_dicts, inert_irreds etc.
1589
1590 - We don't kick out constraints from inert_solved_dicts, and
1591 inert_solved_funeqs optimistically. But when we lookup we have to
1592 take the substitution into account
1593
1594
1595 Note [Kick out insolubles]
1596 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1597 Suppose we have an insoluble alpha ~ [alpha], which is insoluble
1598 because an occurs check. And then we unify alpha := [Int].
1599 Then we really want to rewrite the insoluble to [Int] ~ [[Int]].
1600 Now it can be decomposed. Otherwise we end up with a "Can't match
1601 [Int] ~ [[Int]]" which is true, but a bit confusing because the
1602 outer type constructors match.
1603 -}
1604
1605
1606
1607 --------------
1608 addInertSafehask :: InertCans -> Ct -> InertCans
1609 addInertSafehask ics item@(CDictCan { cc_class = cls, cc_tyargs = tys })
1610 = ics { inert_safehask = addDict (inert_dicts ics) cls tys item }
1611
1612 addInertSafehask _ item
1613 = pprPanic "addInertSafehask: can't happen! Inserting " $ ppr item
1614
1615 insertSafeOverlapFailureTcS :: Ct -> TcS ()
1616 -- See Note [Safe Haskell Overlapping Instances Implementation] in TcSimplify
1617 insertSafeOverlapFailureTcS item
1618 = updInertCans (\ics -> addInertSafehask ics item)
1619
1620 getSafeOverlapFailures :: TcS Cts
1621 -- See Note [Safe Haskell Overlapping Instances Implementation] in TcSimplify
1622 getSafeOverlapFailures
1623 = do { IC { inert_safehask = safehask } <- getInertCans
1624 ; return $ foldDicts consCts safehask emptyCts }
1625
1626 --------------
1627 addSolvedDict :: CtEvidence -> Class -> [Type] -> TcS ()
1628 -- Add a new item in the solved set of the monad
1629 -- See Note [Solved dictionaries]
1630 addSolvedDict item cls tys
1631 | isIPPred (ctEvPred item) -- Never cache "solved" implicit parameters (not sure why!)
1632 = return ()
1633 | otherwise
1634 = do { traceTcS "updSolvedSetTcs:" $ ppr item
1635 ; updInertTcS $ \ ics ->
1636 ics { inert_solved_dicts = addDict (inert_solved_dicts ics) cls tys item } }
1637
1638 {- *********************************************************************
1639 * *
1640 Other inert-set operations
1641 * *
1642 ********************************************************************* -}
1643
1644 updInertTcS :: (InertSet -> InertSet) -> TcS ()
1645 -- Modify the inert set with the supplied function
1646 updInertTcS upd_fn
1647 = do { is_var <- getTcSInertsRef
1648 ; wrapTcS (do { curr_inert <- TcM.readTcRef is_var
1649 ; TcM.writeTcRef is_var (upd_fn curr_inert) }) }
1650
1651 getInertCans :: TcS InertCans
1652 getInertCans = do { inerts <- getTcSInerts; return (inert_cans inerts) }
1653
1654 setInertCans :: InertCans -> TcS ()
1655 setInertCans ics = updInertTcS $ \ inerts -> inerts { inert_cans = ics }
1656
1657 updRetInertCans :: (InertCans -> (a, InertCans)) -> TcS a
1658 -- Modify the inert set with the supplied function
1659 updRetInertCans upd_fn
1660 = do { is_var <- getTcSInertsRef
1661 ; wrapTcS (do { inerts <- TcM.readTcRef is_var
1662 ; let (res, cans') = upd_fn (inert_cans inerts)
1663 ; TcM.writeTcRef is_var (inerts { inert_cans = cans' })
1664 ; return res }) }
1665
1666 updInertCans :: (InertCans -> InertCans) -> TcS ()
1667 -- Modify the inert set with the supplied function
1668 updInertCans upd_fn
1669 = updInertTcS $ \ inerts -> inerts { inert_cans = upd_fn (inert_cans inerts) }
1670
1671 updInertDicts :: (DictMap Ct -> DictMap Ct) -> TcS ()
1672 -- Modify the inert set with the supplied function
1673 updInertDicts upd_fn
1674 = updInertCans $ \ ics -> ics { inert_dicts = upd_fn (inert_dicts ics) }
1675
1676 updInertSafehask :: (DictMap Ct -> DictMap Ct) -> TcS ()
1677 -- Modify the inert set with the supplied function
1678 updInertSafehask upd_fn
1679 = updInertCans $ \ ics -> ics { inert_safehask = upd_fn (inert_safehask ics) }
1680
1681 updInertFunEqs :: (FunEqMap Ct -> FunEqMap Ct) -> TcS ()
1682 -- Modify the inert set with the supplied function
1683 updInertFunEqs upd_fn
1684 = updInertCans $ \ ics -> ics { inert_funeqs = upd_fn (inert_funeqs ics) }
1685
1686 updInertIrreds :: (Cts -> Cts) -> TcS ()
1687 -- Modify the inert set with the supplied function
1688 updInertIrreds upd_fn
1689 = updInertCans $ \ ics -> ics { inert_irreds = upd_fn (inert_irreds ics) }
1690
1691 getInertEqs :: TcS (DTyVarEnv EqualCtList)
1692 getInertEqs = do { inert <- getInertCans; return (inert_eqs inert) }
1693
1694 getInertInsols :: TcS Cts
1695 getInertInsols = do { inert <- getInertCans; return (inert_insols inert) }
1696
1697 getInertGivens :: TcS [Ct]
1698 -- Returns the Given constraints in the inert set,
1699 -- with type functions *not* unflattened
1700 getInertGivens
1701 = do { inerts <- getInertCans
1702 ; let all_cts = foldDicts (:) (inert_dicts inerts)
1703 $ foldFunEqs (:) (inert_funeqs inerts)
1704 $ concat (dVarEnvElts (inert_eqs inerts))
1705 ; return (filter isGivenCt all_cts) }
1706
1707 getPendingScDicts :: TcS [Ct]
1708 -- Find all inert Given dictionaries whose cc_pend_sc flag is True
1709 -- Set the flag to False in the inert set, and return that Ct
1710 getPendingScDicts = updRetInertCans get_sc_dicts
1711 where
1712 get_sc_dicts ic@(IC { inert_dicts = dicts })
1713 = (sc_pend_dicts, ic')
1714 where
1715 ic' = ic { inert_dicts = foldr add dicts sc_pend_dicts }
1716
1717 sc_pend_dicts :: [Ct]
1718 sc_pend_dicts = foldDicts get_pending dicts []
1719
1720 get_pending :: Ct -> [Ct] -> [Ct] -- Get dicts with cc_pend_sc = True
1721 -- but flipping the flag
1722 get_pending dict dicts
1723 | Just dict' <- isPendingScDict dict = dict' : dicts
1724 | otherwise = dicts
1725
1726 add :: Ct -> DictMap Ct -> DictMap Ct
1727 add ct@(CDictCan { cc_class = cls, cc_tyargs = tys }) dicts
1728 = addDict dicts cls tys ct
1729 add ct _ = pprPanic "getPendingScDicts" (ppr ct)
1730
1731 getUnsolvedInerts :: TcS ( Bag Implication
1732 , Cts -- Tyvar eqs: a ~ ty
1733 , Cts -- Fun eqs: F a ~ ty
1734 , Cts -- Insoluble
1735 , Cts ) -- All others
1736 -- Return all the unsolved [Wanted] or [Derived] constraints
1737 --
1738 -- Post-condition: the returned simple constraints are all fully zonked
1739 -- (because they come from the inert set)
1740 -- the unsolved implics may not be
1741 getUnsolvedInerts
1742 = do { IC { inert_eqs = tv_eqs
1743 , inert_funeqs = fun_eqs
1744 , inert_irreds = irreds
1745 , inert_dicts = idicts
1746 , inert_insols = insols
1747 } <- getInertCans
1748
1749 ; let unsolved_tv_eqs = foldTyEqs add_if_unsolved tv_eqs emptyCts
1750 unsolved_fun_eqs = foldFunEqs add_if_wanted fun_eqs emptyCts
1751 unsolved_irreds = Bag.filterBag is_unsolved irreds
1752 unsolved_dicts = foldDicts add_if_unsolved idicts emptyCts
1753 unsolved_others = unsolved_irreds `unionBags` unsolved_dicts
1754 unsolved_insols = filterBag is_unsolved insols
1755
1756 ; implics <- getWorkListImplics
1757
1758 ; traceTcS "getUnsolvedInerts" $
1759 vcat [ text " tv eqs =" <+> ppr unsolved_tv_eqs
1760 , text "fun eqs =" <+> ppr unsolved_fun_eqs
1761 , text "insols =" <+> ppr unsolved_insols
1762 , text "others =" <+> ppr unsolved_others
1763 , text "implics =" <+> ppr implics ]
1764
1765 ; return ( implics, unsolved_tv_eqs, unsolved_fun_eqs
1766 , unsolved_insols, unsolved_others) }
1767 where
1768 add_if_unsolved :: Ct -> Cts -> Cts
1769 add_if_unsolved ct cts | is_unsolved ct = ct `consCts` cts
1770 | otherwise = cts
1771
1772 is_unsolved ct = not (isGivenCt ct) -- Wanted or Derived
1773
1774 -- For CFunEqCans we ignore the Derived ones, and keep
1775 -- only the Wanteds for flattening. The Derived ones
1776 -- share a unification variable with the corresponding
1777 -- Wanted, so we definitely don't want to to participate
1778 -- in unflattening
1779 -- See Note [Type family equations]
1780 add_if_wanted ct cts | isWantedCt ct = ct `consCts` cts
1781 | otherwise = cts
1782
1783 isInInertEqs :: DTyVarEnv EqualCtList -> TcTyVar -> TcType -> Bool
1784 -- True if (a ~N ty) is in the inert set, in either Given or Wanted
1785 isInInertEqs eqs tv rhs
1786 = case lookupDVarEnv eqs tv of
1787 Nothing -> False
1788 Just cts -> any (same_pred rhs) cts
1789 where
1790 same_pred rhs ct
1791 | CTyEqCan { cc_rhs = rhs2, cc_eq_rel = eq_rel } <- ct
1792 , NomEq <- eq_rel
1793 , rhs `eqType` rhs2 = True
1794 | otherwise = False
1795
1796 getNoGivenEqs :: TcLevel -- TcLevel of this implication
1797 -> [TcTyVar] -- Skolems of this implication
1798 -> TcS ( Bool -- True <=> definitely no residual given equalities
1799 , Cts ) -- Insoluble constraints arising from givens
1800 -- See Note [When does an implication have given equalities?]
1801 getNoGivenEqs tclvl skol_tvs
1802 = do { inerts@(IC { inert_eqs = ieqs, inert_irreds = iirreds
1803 , inert_funeqs = funeqs
1804 , inert_insols = insols })
1805 <- getInertCans
1806 ; let local_fsks = foldFunEqs add_fsk funeqs emptyVarSet
1807
1808 has_given_eqs = foldrBag ((||) . ev_given_here . ctEvidence) False
1809 (iirreds `unionBags` insols)
1810 || anyDVarEnv (eqs_given_here local_fsks) ieqs
1811
1812 ; traceTcS "getNoGivenEqs" (vcat [ ppr has_given_eqs, ppr inerts
1813 , ppr insols])
1814 ; return (not has_given_eqs, insols) }
1815 where
1816 eqs_given_here :: VarSet -> EqualCtList -> Bool
1817 eqs_given_here local_fsks [CTyEqCan { cc_tyvar = tv, cc_ev = ev }]
1818 -- Givens are always a sigleton
1819 = not (skolem_bound_here local_fsks tv) && ev_given_here ev
1820 eqs_given_here _ _ = False
1821
1822 ev_given_here :: CtEvidence -> Bool
1823 -- True for a Given bound by the curent implication,
1824 -- i.e. the current level
1825 ev_given_here ev
1826 = isGiven ev
1827 && tclvl == ctLocLevel (ctEvLoc ev)
1828
1829 add_fsk :: Ct -> VarSet -> VarSet
1830 add_fsk ct fsks | CFunEqCan { cc_fsk = tv, cc_ev = ev } <- ct
1831 , isGiven ev = extendVarSet fsks tv
1832 | otherwise = fsks
1833
1834 skol_tv_set = mkVarSet skol_tvs
1835 skolem_bound_here local_fsks tv -- See Note [Let-bound skolems]
1836 = case tcTyVarDetails tv of
1837 SkolemTv {} -> tv `elemVarSet` skol_tv_set
1838 FlatSkol {} -> not (tv `elemVarSet` local_fsks)
1839 _ -> False
1840
1841 -- | Returns Given constraints that might,
1842 -- potentially, match the given pred. This is used when checking to see if a
1843 -- Given might overlap with an instance. See Note [Instance and Given overlap]
1844 -- in TcInteract.
1845 matchableGivens :: CtLoc -> PredType -> InertSet -> Cts
1846 matchableGivens loc_w pred (IS { inert_cans = inert_cans })
1847 = filterBag matchable_given all_relevant_givens
1848 where
1849 -- just look in class constraints and irreds. matchableGivens does get called
1850 -- for ~R constraints, but we don't need to look through equalities, because
1851 -- canonical equalities are used for rewriting. We'll only get caught by
1852 -- non-canonical -- that is, irreducible -- equalities.
1853 all_relevant_givens :: Cts
1854 all_relevant_givens
1855 | Just (clas, _) <- getClassPredTys_maybe pred
1856 = findDictsByClass (inert_dicts inert_cans) clas
1857 `unionBags` inert_irreds inert_cans
1858 | otherwise
1859 = inert_irreds inert_cans
1860
1861 matchable_given :: Ct -> Bool
1862 matchable_given ct
1863 | CtGiven { ctev_loc = loc_g } <- ctev
1864 , Just _ <- tcUnifyTys bind_meta_tv [ctEvPred ctev] [pred]
1865 , not (prohibitedSuperClassSolve loc_g loc_w)
1866 = True
1867
1868 | otherwise
1869 = False
1870 where
1871 ctev = cc_ev ct
1872
1873 bind_meta_tv :: TcTyVar -> BindFlag
1874 -- Any meta tyvar may be unified later, so we treat it as
1875 -- bindable when unifying with givens. That ensures that we
1876 -- conservatively assume that a meta tyvar might get unified with
1877 -- something that matches the 'given', until demonstrated
1878 -- otherwise.
1879 bind_meta_tv tv | isMetaTyVar tv = BindMe
1880 | otherwise = Skolem
1881
1882 prohibitedSuperClassSolve :: CtLoc -> CtLoc -> Bool
1883 -- See Note [Solving superclass constraints] in TcInstDcls
1884 prohibitedSuperClassSolve from_loc solve_loc
1885 | GivenOrigin (InstSC given_size) <- ctLocOrigin from_loc
1886 , ScOrigin wanted_size <- ctLocOrigin solve_loc
1887 = given_size >= wanted_size
1888 | otherwise
1889 = False
1890
1891 {- Note [Unsolved Derived equalities]
1892 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1893 In getUnsolvedInerts, we return a derived equality from the inert_eqs
1894 because it is a candidate for floating out of this implication. We
1895 only float equalities with a meta-tyvar on the left, so we only pull
1896 those out here.
1897
1898 Note [When does an implication have given equalities?]
1899 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1900 Consider an implication
1901 beta => alpha ~ Int
1902 where beta is a unification variable that has already been unified
1903 to () in an outer scope. Then we can float the (alpha ~ Int) out
1904 just fine. So when deciding whether the givens contain an equality,
1905 we should canonicalise first, rather than just looking at the original
1906 givens (Trac #8644).
1907
1908 So we simply look at the inert, canonical Givens and see if there are
1909 any equalities among them, the calculation of has_given_eqs. There
1910 are some wrinkles:
1911
1912 * We must know which ones are bound in *this* implication and which
1913 are bound further out. We can find that out from the TcLevel
1914 of the Given, which is itself recorded in the tcl_tclvl field
1915 of the TcLclEnv stored in the Given (ev_given_here).
1916
1917 What about interactions between inner and outer givens?
1918 - Outer given is rewritten by an inner given, then there must
1919 have been an inner given equality, hence the “given-eq” flag
1920 will be true anyway.
1921
1922 - Inner given rewritten by outer, retains its level (ie. The inner one)
1923
1924 * We must take account of *potential* equalities, like the one above:
1925 beta => ...blah...
1926 If we still don't know what beta is, we conservatively treat it as potentially
1927 becoming an equality. Hence including 'irreds' in the calculation or has_given_eqs.
1928
1929 * When flattening givens, we generate Given equalities like
1930 <F [a]> : F [a] ~ f,
1931 with Refl evidence, and we *don't* want those to count as an equality
1932 in the givens! After all, the entire flattening business is just an
1933 internal matter, and the evidence does not mention any of the 'givens'
1934 of this implication. So we do not treat inert_funeqs as a 'given equality'.
1935
1936 * See Note [Let-bound skolems] for another wrinkle
1937
1938 * We do *not* need to worry about representational equalities, because
1939 these do not affect the ability to float constraints.
1940
1941 Note [Let-bound skolems]
1942 ~~~~~~~~~~~~~~~~~~~~~~~~
1943 If * the inert set contains a canonical Given CTyEqCan (a ~ ty)
1944 and * 'a' is a skolem bound in this very implication, b
1945
1946 then:
1947 a) The Given is pretty much a let-binding, like
1948 f :: (a ~ b->c) => a -> a
1949 Here the equality constraint is like saying
1950 let a = b->c in ...
1951 It is not adding any new, local equality information,
1952 and hence can be ignored by has_given_eqs
1953
1954 b) 'a' will have been completely substituted out in the inert set,
1955 so we can safely discard it. Notably, it doesn't need to be
1956 returned as part of 'fsks'
1957
1958 For an example, see Trac #9211.
1959 -}
1960
1961 removeInertCts :: [Ct] -> InertCans -> InertCans
1962 -- ^ Remove inert constraints from the 'InertCans', for use when a
1963 -- typechecker plugin wishes to discard a given.
1964 removeInertCts cts icans = foldl' removeInertCt icans cts
1965
1966 removeInertCt :: InertCans -> Ct -> InertCans
1967 removeInertCt is ct =
1968 case ct of
1969
1970 CDictCan { cc_class = cl, cc_tyargs = tys } ->
1971 is { inert_dicts = delDict (inert_dicts is) cl tys }
1972
1973 CFunEqCan { cc_fun = tf, cc_tyargs = tys } ->
1974 is { inert_funeqs = delFunEq (inert_funeqs is) tf tys }
1975
1976 CTyEqCan { cc_tyvar = x, cc_rhs = ty } ->
1977 is { inert_eqs = delTyEq (inert_eqs is) x ty }
1978
1979 CIrredEvCan {} -> panic "removeInertCt: CIrredEvCan"
1980 CNonCanonical {} -> panic "removeInertCt: CNonCanonical"
1981 CHoleCan {} -> panic "removeInertCt: CHoleCan"
1982
1983
1984 lookupFlatCache :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcType, CtFlavour))
1985 lookupFlatCache fam_tc tys
1986 = do { IS { inert_flat_cache = flat_cache
1987 , inert_cans = IC { inert_funeqs = inert_funeqs } } <- getTcSInerts
1988 ; return (firstJusts [lookup_inerts inert_funeqs,
1989 lookup_flats flat_cache]) }
1990 where
1991 lookup_inerts inert_funeqs
1992 | Just (CFunEqCan { cc_ev = ctev, cc_fsk = fsk, cc_tyargs = xis })
1993 <- findFunEq inert_funeqs fam_tc tys
1994 , tys `eqTypes` xis -- The lookup might find a near-match; see
1995 -- Note [Use loose types in inert set]
1996 = Just (ctEvCoercion ctev, mkTyVarTy fsk, ctEvFlavour ctev)
1997 | otherwise = Nothing
1998
1999 lookup_flats flat_cache = findExactFunEq flat_cache fam_tc tys
2000
2001
2002 lookupInInerts :: TcPredType -> TcS (Maybe CtEvidence)
2003 -- Is this exact predicate type cached in the solved or canonicals of the InertSet?
2004 lookupInInerts pty
2005 | ClassPred cls tys <- classifyPredType pty
2006 = do { inerts <- getTcSInerts
2007 ; return (lookupSolvedDict inerts cls tys `mplus`
2008 lookupInertDict (inert_cans inerts) cls tys) }
2009 | otherwise -- NB: No caching for equalities, IPs, holes, or errors
2010 = return Nothing
2011
2012 -- | Look up a dictionary inert. NB: the returned 'CtEvidence' might not
2013 -- match the input exactly. Note [Use loose types in inert set].
2014 lookupInertDict :: InertCans -> Class -> [Type] -> Maybe CtEvidence
2015 lookupInertDict (IC { inert_dicts = dicts }) cls tys
2016 = case findDict dicts cls tys of
2017 Just ct -> Just (ctEvidence ct)
2018 _ -> Nothing
2019
2020 -- | Look up a solved inert. NB: the returned 'CtEvidence' might not
2021 -- match the input exactly. See Note [Use loose types in inert set].
2022 lookupSolvedDict :: InertSet -> Class -> [Type] -> Maybe CtEvidence
2023 -- Returns just if exactly this predicate type exists in the solved.
2024 lookupSolvedDict (IS { inert_solved_dicts = solved }) cls tys
2025 = case findDict solved cls tys of
2026 Just ev -> Just ev
2027 _ -> Nothing
2028
2029 {- *********************************************************************
2030 * *
2031 Irreds
2032 * *
2033 ********************************************************************* -}
2034
2035 foldIrreds :: (Ct -> b -> b) -> Cts -> b -> b
2036 foldIrreds k irreds z = foldrBag k z irreds
2037
2038
2039 {- *********************************************************************
2040 * *
2041 TcAppMap
2042 * *
2043 ************************************************************************
2044
2045 Note [Use loose types in inert set]
2046 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2047 Say we know (Eq (a |> c1)) and we need (Eq (a |> c2)). One is clearly
2048 solvable from the other. So, we do lookup in the inert set using
2049 loose types, which omit the kind-check.
2050
2051 We must be careful when using the result of a lookup because it may
2052 not match the requsted info exactly!
2053
2054 -}
2055
2056 type TcAppMap a = UniqDFM (ListMap LooseTypeMap a)
2057 -- Indexed by tycon then the arg types, using "loose" matching, where
2058 -- we don't require kind equality. This allows, for example, (a |> co)
2059 -- to match (a).
2060 -- See Note [Use loose types in inert set]
2061 -- Used for types and classes; hence UniqDFM
2062 -- See Note [foldTM determinism] for why we use UniqDFM here
2063
2064 isEmptyTcAppMap :: TcAppMap a -> Bool
2065 isEmptyTcAppMap m = isNullUDFM m
2066
2067 emptyTcAppMap :: TcAppMap a
2068 emptyTcAppMap = emptyUDFM
2069
2070 findTcApp :: TcAppMap a -> Unique -> [Type] -> Maybe a
2071 findTcApp m u tys = do { tys_map <- lookupUDFM m u
2072 ; lookupTM tys tys_map }
2073
2074 delTcApp :: TcAppMap a -> Unique -> [Type] -> TcAppMap a
2075 delTcApp m cls tys = adjustUDFM (deleteTM tys) m cls
2076
2077 insertTcApp :: TcAppMap a -> Unique -> [Type] -> a -> TcAppMap a
2078 insertTcApp m cls tys ct = alterUDFM alter_tm m cls
2079 where
2080 alter_tm mb_tm = Just (insertTM tys ct (mb_tm `orElse` emptyTM))
2081
2082 -- mapTcApp :: (a->b) -> TcAppMap a -> TcAppMap b
2083 -- mapTcApp f = mapUDFM (mapTM f)
2084
2085 filterTcAppMap :: (Ct -> Bool) -> TcAppMap Ct -> TcAppMap Ct
2086 filterTcAppMap f m
2087 = mapUDFM do_tm m
2088 where
2089 do_tm tm = foldTM insert_mb tm emptyTM
2090 insert_mb ct tm
2091 | f ct = insertTM tys ct tm
2092 | otherwise = tm
2093 where
2094 tys = case ct of
2095 CFunEqCan { cc_tyargs = tys } -> tys
2096 CDictCan { cc_tyargs = tys } -> tys
2097 _ -> pprPanic "filterTcAppMap" (ppr ct)
2098
2099 tcAppMapToBag :: TcAppMap a -> Bag a
2100 tcAppMapToBag m = foldTcAppMap consBag m emptyBag
2101
2102 foldTcAppMap :: (a -> b -> b) -> TcAppMap a -> b -> b
2103 foldTcAppMap k m z = foldUDFM (foldTM k) z m
2104
2105
2106 {- *********************************************************************
2107 * *
2108 DictMap
2109 * *
2110 ********************************************************************* -}
2111
2112 type DictMap a = TcAppMap a
2113
2114 emptyDictMap :: DictMap a
2115 emptyDictMap = emptyTcAppMap
2116
2117 -- sizeDictMap :: DictMap a -> Int
2118 -- sizeDictMap m = foldDicts (\ _ x -> x+1) m 0
2119
2120 findDict :: DictMap a -> Class -> [Type] -> Maybe a
2121 findDict m cls tys = findTcApp m (getUnique cls) tys
2122
2123 findDictsByClass :: DictMap a -> Class -> Bag a
2124 findDictsByClass m cls
2125 | Just tm <- lookupUDFM m cls = foldTM consBag tm emptyBag
2126 | otherwise = emptyBag
2127
2128 delDict :: DictMap a -> Class -> [Type] -> DictMap a
2129 delDict m cls tys = delTcApp m (getUnique cls) tys
2130
2131 addDict :: DictMap a -> Class -> [Type] -> a -> DictMap a
2132 addDict m cls tys item = insertTcApp m (getUnique cls) tys item
2133
2134 addDictsByClass :: DictMap Ct -> Class -> Bag Ct -> DictMap Ct
2135 addDictsByClass m cls items
2136 = addToUDFM m cls (foldrBag add emptyTM items)
2137 where
2138 add ct@(CDictCan { cc_tyargs = tys }) tm = insertTM tys ct tm
2139 add ct _ = pprPanic "addDictsByClass" (ppr ct)
2140
2141 filterDicts :: (Ct -> Bool) -> DictMap Ct -> DictMap Ct
2142 filterDicts f m = filterTcAppMap f m
2143
2144 partitionDicts :: (Ct -> Bool) -> DictMap Ct -> (Bag Ct, DictMap Ct)
2145 partitionDicts f m = foldTcAppMap k m (emptyBag, emptyDicts)
2146 where
2147 k ct (yeses, noes) | f ct = (ct `consBag` yeses, noes)
2148 | otherwise = (yeses, add ct noes)
2149 add ct@(CDictCan { cc_class = cls, cc_tyargs = tys }) m
2150 = addDict m cls tys ct
2151 add ct _ = pprPanic "partitionDicts" (ppr ct)
2152
2153 dictsToBag :: DictMap a -> Bag a
2154 dictsToBag = tcAppMapToBag
2155
2156 foldDicts :: (a -> b -> b) -> DictMap a -> b -> b
2157 foldDicts = foldTcAppMap
2158
2159 emptyDicts :: DictMap a
2160 emptyDicts = emptyTcAppMap
2161
2162
2163 {- *********************************************************************
2164 * *
2165 FunEqMap
2166 * *
2167 ********************************************************************* -}
2168
2169 type FunEqMap a = TcAppMap a -- A map whose key is a (TyCon, [Type]) pair
2170
2171 emptyFunEqs :: TcAppMap a
2172 emptyFunEqs = emptyTcAppMap
2173
2174 findFunEq :: FunEqMap a -> TyCon -> [Type] -> Maybe a
2175 findFunEq m tc tys = findTcApp m (getUnique tc) tys
2176
2177 funEqsToBag :: FunEqMap a -> Bag a
2178 funEqsToBag m = foldTcAppMap consBag m emptyBag
2179
2180 findFunEqsByTyCon :: FunEqMap a -> TyCon -> [a]
2181 -- Get inert function equation constraints that have the given tycon
2182 -- in their head. Not that the constraints remain in the inert set.
2183 -- We use this to check for derived interactions with built-in type-function
2184 -- constructors.
2185 findFunEqsByTyCon m tc
2186 | Just tm <- lookupUDFM m tc = foldTM (:) tm []
2187 | otherwise = []
2188
2189 foldFunEqs :: (a -> b -> b) -> FunEqMap a -> b -> b
2190 foldFunEqs = foldTcAppMap
2191
2192 -- mapFunEqs :: (a -> b) -> FunEqMap a -> FunEqMap b
2193 -- mapFunEqs = mapTcApp
2194
2195 -- filterFunEqs :: (Ct -> Bool) -> FunEqMap Ct -> FunEqMap Ct
2196 -- filterFunEqs = filterTcAppMap
2197
2198 insertFunEq :: FunEqMap a -> TyCon -> [Type] -> a -> FunEqMap a
2199 insertFunEq m tc tys val = insertTcApp m (getUnique tc) tys val
2200
2201 partitionFunEqs :: (Ct -> Bool) -> FunEqMap Ct -> ([Ct], FunEqMap Ct)
2202 -- Optimise for the case where the predicate is false
2203 -- partitionFunEqs is called only from kick-out, and kick-out usually
2204 -- kicks out very few equalities, so we want to optimise for that case
2205 partitionFunEqs f m = (yeses, foldr del m yeses)
2206 where
2207 yeses = foldTcAppMap k m []
2208 k ct yeses | f ct = ct : yeses
2209 | otherwise = yeses
2210 del (CFunEqCan { cc_fun = tc, cc_tyargs = tys }) m
2211 = delFunEq m tc tys
2212 del ct _ = pprPanic "partitionFunEqs" (ppr ct)
2213
2214 delFunEq :: FunEqMap a -> TyCon -> [Type] -> FunEqMap a
2215 delFunEq m tc tys = delTcApp m (getUnique tc) tys
2216
2217 ------------------------------
2218 type ExactFunEqMap a = UniqFM (ListMap TypeMap a)
2219
2220 emptyExactFunEqs :: ExactFunEqMap a
2221 emptyExactFunEqs = emptyUFM
2222
2223 findExactFunEq :: ExactFunEqMap a -> TyCon -> [Type] -> Maybe a
2224 findExactFunEq m tc tys = do { tys_map <- lookupUFM m (getUnique tc)
2225 ; lookupTM tys tys_map }
2226
2227 insertExactFunEq :: ExactFunEqMap a -> TyCon -> [Type] -> a -> ExactFunEqMap a
2228 insertExactFunEq m tc tys val = alterUFM alter_tm m (getUnique tc)
2229 where alter_tm mb_tm = Just (insertTM tys val (mb_tm `orElse` emptyTM))
2230
2231 {-
2232 ************************************************************************
2233 * *
2234 * The TcS solver monad *
2235 * *
2236 ************************************************************************
2237
2238 Note [The TcS monad]
2239 ~~~~~~~~~~~~~~~~~~~~
2240 The TcS monad is a weak form of the main Tc monad
2241
2242 All you can do is
2243 * fail
2244 * allocate new variables
2245 * fill in evidence variables
2246
2247 Filling in a dictionary evidence variable means to create a binding
2248 for it, so TcS carries a mutable location where the binding can be
2249 added. This is initialised from the innermost implication constraint.
2250 -}
2251
2252 data TcSEnv
2253 = TcSEnv {
2254 tcs_ev_binds :: EvBindsVar,
2255
2256 tcs_unified :: IORef Int,
2257 -- The number of unification variables we have filled
2258 -- The important thing is whether it is non-zero
2259
2260 tcs_count :: IORef Int, -- Global step count
2261
2262 tcs_inerts :: IORef InertSet, -- Current inert set
2263
2264 -- The main work-list and the flattening worklist
2265 -- See Note [Work list priorities] and
2266 tcs_worklist :: IORef WorkList -- Current worklist
2267 }
2268
2269 ---------------
2270 newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
2271
2272 instance Functor TcS where
2273 fmap f m = TcS $ fmap f . unTcS m
2274
2275 instance Applicative TcS where
2276 pure x = TcS (\_ -> return x)
2277 (<*>) = ap
2278
2279 instance Monad TcS where
2280 fail err = TcS (\_ -> fail err)
2281 m >>= k = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
2282
2283 #if __GLASGOW_HASKELL__ > 710
2284 instance MonadFail.MonadFail TcS where
2285 fail err = TcS (\_ -> fail err)
2286 #endif
2287
2288 instance MonadUnique TcS where
2289 getUniqueSupplyM = wrapTcS getUniqueSupplyM
2290
2291 -- Basic functionality
2292 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2293 wrapTcS :: TcM a -> TcS a
2294 -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
2295 -- and TcS is supposed to have limited functionality
2296 wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
2297
2298 wrapErrTcS :: TcM a -> TcS a
2299 -- The thing wrapped should just fail
2300 -- There's no static check; it's up to the user
2301 -- Having a variant for each error message is too painful
2302 wrapErrTcS = wrapTcS
2303
2304 wrapWarnTcS :: TcM a -> TcS a
2305 -- The thing wrapped should just add a warning, or no-op
2306 -- There's no static check; it's up to the user
2307 wrapWarnTcS = wrapTcS
2308
2309 failTcS, panicTcS :: SDoc -> TcS a
2310 warnTcS :: WarningFlag -> SDoc -> TcS ()
2311 addErrTcS :: SDoc -> TcS ()
2312 failTcS = wrapTcS . TcM.failWith
2313 warnTcS flag = wrapTcS . TcM.addWarn (Reason flag)
2314 addErrTcS = wrapTcS . TcM.addErr
2315 panicTcS doc = pprPanic "TcCanonical" doc
2316
2317 traceTcS :: String -> SDoc -> TcS ()
2318 traceTcS herald doc = wrapTcS (TcM.traceTc herald doc)
2319
2320 runTcPluginTcS :: TcPluginM a -> TcS a
2321 runTcPluginTcS m = wrapTcS . runTcPluginM m =<< getTcEvBindsVar
2322
2323 instance HasDynFlags TcS where
2324 getDynFlags = wrapTcS getDynFlags
2325
2326 getGlobalRdrEnvTcS :: TcS GlobalRdrEnv
2327 getGlobalRdrEnvTcS = wrapTcS TcM.getGlobalRdrEnv
2328
2329 bumpStepCountTcS :: TcS ()
2330 bumpStepCountTcS = TcS $ \env -> do { let ref = tcs_count env
2331 ; n <- TcM.readTcRef ref
2332 ; TcM.writeTcRef ref (n+1) }
2333
2334 csTraceTcS :: SDoc -> TcS ()
2335 csTraceTcS doc
2336 = wrapTcS $ csTraceTcM (return doc)
2337
2338 traceFireTcS :: CtEvidence -> SDoc -> TcS ()
2339 -- Dump a rule-firing trace
2340 traceFireTcS ev doc
2341 = TcS $ \env -> csTraceTcM $
2342 do { n <- TcM.readTcRef (tcs_count env)
2343 ; tclvl <- TcM.getTcLevel
2344 ; return (hang (text "Step" <+> int n
2345 <> brackets (text "l:" <> ppr tclvl <> comma <>
2346 text "d:" <> ppr (ctLocDepth (ctEvLoc ev)))
2347 <+> doc <> colon)
2348 4 (ppr ev)) }
2349
2350 csTraceTcM :: TcM SDoc -> TcM ()
2351 -- Constraint-solver tracing, -ddump-cs-trace
2352 csTraceTcM mk_doc
2353 = do { dflags <- getDynFlags
2354 ; when ( dopt Opt_D_dump_cs_trace dflags
2355 || dopt Opt_D_dump_tc_trace dflags )
2356 ( do { msg <- mk_doc
2357 ; TcM.traceTcRn Opt_D_dump_cs_trace msg }) }
2358
2359 runTcS :: TcS a -- What to run
2360 -> TcM (a, EvBindMap)
2361 runTcS tcs
2362 = do { ev_binds_var <- TcM.newTcEvBinds
2363 ; res <- runTcSWithEvBinds ev_binds_var tcs
2364 ; ev_binds <- TcM.getTcEvBindsMap ev_binds_var
2365 ; return (res, ev_binds) }
2366
2367 -- | This variant of 'runTcS' will keep solving, even when only Deriveds
2368 -- are left around. It also doesn't return any evidence, as callers won't
2369 -- need it.
2370 runTcSDeriveds :: TcS a -> TcM a
2371 runTcSDeriveds tcs
2372 = do { ev_binds_var <- TcM.newTcEvBinds
2373 ; runTcSWithEvBinds ev_binds_var tcs }
2374
2375 -- | This can deal only with equality constraints.
2376 runTcSEqualities :: TcS a -> TcM a
2377 runTcSEqualities thing_inside
2378 = do { ev_binds_var <- TcM.newTcEvBinds
2379 ; runTcSWithEvBinds ev_binds_var thing_inside }
2380
2381 runTcSWithEvBinds :: EvBindsVar
2382 -> TcS a
2383 -> TcM a
2384 runTcSWithEvBinds ev_binds_var tcs
2385 = do { unified_var <- TcM.newTcRef 0
2386 ; step_count <- TcM.newTcRef 0
2387 ; inert_var <- TcM.newTcRef emptyInert
2388 ; wl_var <- TcM.newTcRef emptyWorkList
2389 ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
2390 , tcs_unified = unified_var
2391 , tcs_count = step_count
2392 , tcs_inerts = inert_var
2393 , tcs_worklist = wl_var }
2394
2395 -- Run the computation
2396 ; res <- unTcS tcs env
2397
2398 ; count <- TcM.readTcRef step_count
2399 ; when (count > 0) $
2400 csTraceTcM $ return (text "Constraint solver steps =" <+> int count)
2401
2402 #ifdef DEBUG
2403 ; ev_binds <- TcM.getTcEvBindsMap ev_binds_var
2404 ; checkForCyclicBinds ev_binds
2405 #endif
2406
2407 ; return res }
2408
2409 #ifdef DEBUG
2410 checkForCyclicBinds :: EvBindMap -> TcM ()
2411 checkForCyclicBinds ev_binds_map
2412 | null cycles
2413 = return ()
2414 | null coercion_cycles
2415 = TcM.traceTc "Cycle in evidence binds" $ ppr cycles
2416 | otherwise
2417 = pprPanic "Cycle in coercion bindings" $ ppr coercion_cycles
2418 where
2419 ev_binds = evBindMapBinds ev_binds_map
2420
2421 cycles :: [[EvBind]]
2422 cycles = [c | CyclicSCC c <- stronglyConnCompFromEdgedVerticesUniq edges]
2423
2424 coercion_cycles = [c | c <- cycles, any is_co_bind c]
2425 is_co_bind (EvBind { eb_lhs = b }) = isEqPred (varType b)
2426
2427 edges :: [(EvBind, EvVar, [EvVar])]
2428 edges = [ (bind, bndr, nonDetEltsUFM (evVarsOfTerm rhs))
2429 | bind@(EvBind { eb_lhs = bndr, eb_rhs = rhs}) <- bagToList ev_binds ]
2430 -- It's OK to use nonDetEltsUFM here as
2431 -- stronglyConnCompFromEdgedVertices is still deterministic even
2432 -- if the edges are in nondeterministic order as explained in
2433 -- Note [Deterministic SCC] in Digraph.
2434 #endif
2435
2436 setEvBindsTcS :: EvBindsVar -> TcS a -> TcS a
2437 setEvBindsTcS ref (TcS thing_inside)
2438 = TcS $ \ env -> thing_inside (env { tcs_ev_binds = ref })
2439
2440 nestImplicTcS :: EvBindsVar
2441 -> TcLevel -> TcS a
2442 -> TcS a
2443 nestImplicTcS ref inner_tclvl (TcS thing_inside)
2444 = TcS $ \ TcSEnv { tcs_unified = unified_var
2445 , tcs_inerts = old_inert_var
2446 , tcs_count = count
2447 } ->
2448 do { inerts <- TcM.readTcRef old_inert_var
2449 ; let nest_inert = inerts { inert_flat_cache = emptyExactFunEqs }
2450 -- See Note [Do not inherit the flat cache]
2451 ; new_inert_var <- TcM.newTcRef nest_inert
2452 ; new_wl_var <- TcM.newTcRef emptyWorkList
2453 ; let nest_env = TcSEnv { tcs_ev_binds = ref
2454 , tcs_unified = unified_var
2455 , tcs_count = count
2456 , tcs_inerts = new_inert_var
2457 , tcs_worklist = new_wl_var }
2458 ; res <- TcM.setTcLevel inner_tclvl $
2459 thing_inside nest_env
2460
2461 #ifdef DEBUG
2462 -- Perform a check that the thing_inside did not cause cycles
2463 ; ev_binds <- TcM.getTcEvBindsMap ref
2464 ; checkForCyclicBinds ev_binds
2465 #endif
2466 ; return res }
2467
2468 {- Note [Do not inherit the flat cache]
2469 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2470 We do not want to inherit the flat cache when processing nested
2471 implications. Consider
2472 a ~ F b, forall c. b~Int => blah
2473 If we have F b ~ fsk in the flat-cache, and we push that into the
2474 nested implication, we might miss that F b can be rewritten to F Int,
2475 and hence perhpas solve it. Moreover, the fsk from outside is
2476 flattened out after solving the outer level, but and we don't
2477 do that flattening recursively.
2478 -}
2479
2480 nestTcS :: TcS a -> TcS a
2481 -- Use the current untouchables, augmenting the current
2482 -- evidence bindings, and solved dictionaries
2483 -- But have no effect on the InertCans, or on the inert_flat_cache
2484 -- (we want to inherit the latter from processing the Givens)
2485 nestTcS (TcS thing_inside)
2486 = TcS $ \ env@(TcSEnv { tcs_inerts = inerts_var }) ->
2487 do { inerts <- TcM.readTcRef inerts_var
2488 ; new_inert_var <- TcM.newTcRef inerts
2489 ; new_wl_var <- TcM.newTcRef emptyWorkList
2490 ; let nest_env = env { tcs_inerts = new_inert_var
2491 , tcs_worklist = new_wl_var }
2492
2493 ; res <- thing_inside nest_env
2494
2495 ; new_inerts <- TcM.readTcRef new_inert_var
2496
2497 -- we want to propogate the safe haskell failures
2498 ; let old_ic = inert_cans inerts
2499 new_ic = inert_cans new_inerts
2500 nxt_ic = old_ic { inert_safehask = inert_safehask new_ic }
2501
2502 ; TcM.writeTcRef inerts_var -- See Note [Propagate the solved dictionaries]
2503 (inerts { inert_solved_dicts = inert_solved_dicts new_inerts
2504 , inert_cans = nxt_ic })
2505
2506 ; return res }
2507
2508 {-
2509 Note [Propagate the solved dictionaries]
2510 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2511 It's really quite important that nestTcS does not discard the solved
2512 dictionaries from the thing_inside.
2513 Consider
2514 Eq [a]
2515 forall b. empty => Eq [a]
2516 We solve the simple (Eq [a]), under nestTcS, and then turn our attention to
2517 the implications. It's definitely fine to use the solved dictionaries on
2518 the inner implications, and it can make a signficant performance difference
2519 if you do so.
2520 -}
2521
2522 -- Getters and setters of TcEnv fields
2523 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2524
2525 -- Getter of inerts and worklist
2526 getTcSInertsRef :: TcS (IORef InertSet)
2527 getTcSInertsRef = TcS (return . tcs_inerts)
2528
2529 getTcSWorkListRef :: TcS (IORef WorkList)
2530 getTcSWorkListRef = TcS (return . tcs_worklist)
2531
2532 getTcSInerts :: TcS InertSet
2533 getTcSInerts = getTcSInertsRef >>= wrapTcS . (TcM.readTcRef)
2534
2535 setTcSInerts :: InertSet -> TcS ()
2536 setTcSInerts ics = do { r <- getTcSInertsRef; wrapTcS (TcM.writeTcRef r ics) }
2537
2538 getWorkListImplics :: TcS (Bag Implication)
2539 getWorkListImplics
2540 = do { wl_var <- getTcSWorkListRef
2541 ; wl_curr <- wrapTcS (TcM.readTcRef wl_var)
2542 ; return (wl_implics wl_curr) }
2543
2544 updWorkListTcS :: (WorkList -> WorkList) -> TcS ()
2545 updWorkListTcS f
2546 = do { wl_var <- getTcSWorkListRef
2547 ; wl_curr <- wrapTcS (TcM.readTcRef wl_var)
2548 ; let new_work = f wl_curr
2549 ; wrapTcS (TcM.writeTcRef wl_var new_work) }
2550
2551 emitWorkNC :: [CtEvidence] -> TcS ()
2552 emitWorkNC evs
2553 | null evs
2554 = return ()
2555 | otherwise
2556 = emitWork (map mkNonCanonical evs)
2557
2558 emitWork :: [Ct] -> TcS ()
2559 emitWork cts
2560 = do { traceTcS "Emitting fresh work" (vcat (map ppr cts))
2561 ; updWorkListTcS (extendWorkListCts cts) }
2562
2563 emitInsoluble :: Ct -> TcS ()
2564 -- Emits a non-canonical constraint that will stand for a frozen error in the inerts.
2565 emitInsoluble ct
2566 = do { traceTcS "Emit insoluble" (ppr ct $$ pprCtLoc (ctLoc ct))
2567 ; updInertTcS add_insol }
2568 where
2569 this_pred = ctPred ct
2570 add_insol is@(IS { inert_cans = ics@(IC { inert_insols = old_insols }) })
2571 | already_there = is
2572 | otherwise = is { inert_cans = ics { inert_insols = old_insols `snocCts` ct } }
2573 where
2574 already_there = not (isWantedCt ct) && anyBag (tcEqType this_pred . ctPred) old_insols
2575 -- See Note [Do not add duplicate derived insolubles]
2576
2577 newTcRef :: a -> TcS (TcRef a)
2578 newTcRef x = wrapTcS (TcM.newTcRef x)
2579
2580 readTcRef :: TcRef a -> TcS a
2581 readTcRef ref = wrapTcS (TcM.readTcRef ref)
2582
2583 updTcRef :: TcRef a -> (a->a) -> TcS ()
2584 updTcRef ref upd_fn = wrapTcS (TcM.updTcRef ref upd_fn)
2585
2586 getTcEvBindsVar :: TcS EvBindsVar
2587 getTcEvBindsVar = TcS (return . tcs_ev_binds)
2588
2589 getTcLevel :: TcS TcLevel
2590 getTcLevel = wrapTcS TcM.getTcLevel
2591
2592 getTcEvBindsAndTCVs :: EvBindsVar -> TcS (EvBindMap, TyCoVarSet)
2593 getTcEvBindsAndTCVs ev_binds_var
2594 = wrapTcS $ do { bnds <- TcM.getTcEvBindsMap ev_binds_var
2595 ; tcvs <- TcM.getTcEvTyCoVars ev_binds_var
2596 ; return (bnds, tcvs) }
2597
2598 getTcEvBindsMap :: TcS EvBindMap
2599 getTcEvBindsMap
2600 = do { ev_binds_var <- getTcEvBindsVar
2601 ; wrapTcS $ TcM.getTcEvBindsMap ev_binds_var }
2602
2603 unifyTyVar :: TcTyVar -> TcType -> TcS ()
2604 -- Unify a meta-tyvar with a type
2605 -- We keep track of how many unifications have happened in tcs_unified,
2606 --
2607 -- We should never unify the same variable twice!
2608 unifyTyVar tv ty
2609 = ASSERT2( isMetaTyVar tv, ppr tv )
2610 TcS $ \ env ->
2611 do { TcM.traceTc "unifyTyVar" (ppr tv <+> text ":=" <+> ppr ty)
2612 ; TcM.writeMetaTyVar tv ty
2613 ; TcM.updTcRef (tcs_unified env) (+1) }
2614
2615 unflattenFmv :: TcTyVar -> TcType -> TcS ()
2616 -- Fill a flatten-meta-var, simply by unifying it.
2617 -- This does NOT count as a unification in tcs_unified.
2618 unflattenFmv tv ty
2619 = ASSERT2( isMetaTyVar tv, ppr tv )
2620 TcS $ \ _ ->
2621 do { TcM.traceTc "unflattenFmv" (ppr tv <+> text ":=" <+> ppr ty)
2622 ; TcM.writeMetaTyVar tv ty }
2623
2624 reportUnifications :: TcS a -> TcS (Int, a)
2625 reportUnifications (TcS thing_inside)
2626 = TcS $ \ env ->
2627 do { inner_unified <- TcM.newTcRef 0
2628 ; res <- thing_inside (env { tcs_unified = inner_unified })
2629 ; n_unifs <- TcM.readTcRef inner_unified
2630 ; TcM.updTcRef (tcs_unified env) (+ n_unifs)
2631 ; return (n_unifs, res) }
2632
2633 getDefaultInfo :: TcS ([Type], (Bool, Bool))
2634 getDefaultInfo = wrapTcS TcM.tcGetDefaultTys
2635
2636 -- Just get some environments needed for instance looking up and matching
2637 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2638
2639 getInstEnvs :: TcS InstEnvs
2640 getInstEnvs = wrapTcS $ TcM.tcGetInstEnvs
2641
2642 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
2643 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
2644
2645 getTopEnv :: TcS HscEnv
2646 getTopEnv = wrapTcS $ TcM.getTopEnv
2647
2648 getGblEnv :: TcS TcGblEnv
2649 getGblEnv = wrapTcS $ TcM.getGblEnv
2650
2651 getLclEnv :: TcS TcLclEnv
2652 getLclEnv = wrapTcS $ TcM.getLclEnv
2653
2654 tcLookupClass :: Name -> TcS Class
2655 tcLookupClass c = wrapTcS $ TcM.tcLookupClass c
2656
2657 -- Setting names as used (used in the deriving of Coercible evidence)
2658 -- Too hackish to expose it to TcS? In that case somehow extract the used
2659 -- constructors from the result of solveInteract
2660 addUsedGREs :: [GlobalRdrElt] -> TcS ()
2661 addUsedGREs gres = wrapTcS $ TcM.addUsedGREs gres
2662
2663 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
2664 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2665
2666 checkWellStagedDFun :: PredType -> DFunId -> CtLoc -> TcS ()
2667 checkWellStagedDFun pred dfun_id loc
2668 = wrapTcS $ TcM.setCtLocM loc $
2669 do { use_stage <- TcM.getStage
2670 ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
2671 where
2672 pp_thing = text "instance for" <+> quotes (ppr pred)
2673 bind_lvl = TcM.topIdLvl dfun_id
2674
2675 pprEq :: TcType -> TcType -> SDoc
2676 pprEq ty1 ty2 = pprParendType ty1 <+> char '~' <+> pprParendType ty2
2677
2678 isTouchableMetaTyVarTcS :: TcTyVar -> TcS Bool
2679 isTouchableMetaTyVarTcS tv
2680 = do { tclvl <- getTcLevel
2681 ; return $ isTouchableMetaTyVar tclvl tv }
2682
2683 isFilledMetaTyVar_maybe :: TcTyVar -> TcS (Maybe Type)
2684 isFilledMetaTyVar_maybe tv
2685 = case tcTyVarDetails tv of
2686 MetaTv { mtv_ref = ref }
2687 -> do { cts <- wrapTcS (TcM.readTcRef ref)
2688 ; case cts of
2689 Indirect ty -> return (Just ty)
2690 Flexi -> return Nothing }
2691 _ -> return Nothing
2692
2693 isFilledMetaTyVar :: TcTyVar -> TcS Bool
2694 isFilledMetaTyVar tv = wrapTcS (TcM.isFilledMetaTyVar tv)
2695
2696 zonkTyCoVarsAndFV :: TcTyCoVarSet -> TcS TcTyCoVarSet
2697 zonkTyCoVarsAndFV tvs = wrapTcS (TcM.zonkTyCoVarsAndFV tvs)
2698
2699 zonkTyCoVarsAndFVList :: [TcTyCoVar] -> TcS [TcTyCoVar]
2700 zonkTyCoVarsAndFVList tvs = wrapTcS (TcM.zonkTyCoVarsAndFVList tvs)
2701
2702 zonkCo :: Coercion -> TcS Coercion
2703 zonkCo = wrapTcS . TcM.zonkCo
2704
2705 zonkTcType :: TcType -> TcS TcType
2706 zonkTcType ty = wrapTcS (TcM.zonkTcType ty)
2707
2708 zonkTcTypes :: [TcType] -> TcS [TcType]
2709 zonkTcTypes tys = wrapTcS (TcM.zonkTcTypes tys)
2710
2711 zonkTcTyVar :: TcTyVar -> TcS TcType
2712 zonkTcTyVar tv = wrapTcS (TcM.zonkTcTyVar tv)
2713
2714 zonkSimples :: Cts -> TcS Cts
2715 zonkSimples cts = wrapTcS (TcM.zonkSimples cts)
2716
2717 zonkWC :: WantedConstraints -> TcS WantedConstraints
2718 zonkWC wc = wrapTcS (TcM.zonkWC wc)
2719
2720 {-
2721 Note [Do not add duplicate derived insolubles]
2722 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2723 In general we *must* add an insoluble (Int ~ Bool) even if there is
2724 one such there already, because they may come from distinct call
2725 sites. Not only do we want an error message for each, but with
2726 -fdefer-type-errors we must generate evidence for each. But for
2727 *derived* insolubles, we only want to report each one once. Why?
2728
2729 (a) A constraint (C r s t) where r -> s, say, may generate the same fundep
2730 equality many times, as the original constraint is successively rewritten.
2731
2732 (b) Ditto the successive iterations of the main solver itself, as it traverses
2733 the constraint tree. See example below.
2734
2735 Also for *given* insolubles we may get repeated errors, as we
2736 repeatedly traverse the constraint tree. These are relatively rare
2737 anyway, so removing duplicates seems ok. (Alternatively we could take
2738 the SrcLoc into account.)
2739
2740 Note that the test does not need to be particularly efficient because
2741 it is only used if the program has a type error anyway.
2742
2743 Example of (b): assume a top-level class and instance declaration:
2744
2745 class D a b | a -> b
2746 instance D [a] [a]
2747
2748 Assume we have started with an implication:
2749
2750 forall c. Eq c => { wc_simple = D [c] c [W] }
2751
2752 which we have simplified to:
2753
2754 forall c. Eq c => { wc_simple = D [c] c [W]
2755 , wc_insols = (c ~ [c]) [D] }
2756
2757 For some reason, e.g. because we floated an equality somewhere else,
2758 we might try to re-solve this implication. If we do not do a
2759 dropDerivedWC, then we will end up trying to solve the following
2760 constraints the second time:
2761
2762 (D [c] c) [W]
2763 (c ~ [c]) [D]
2764
2765 which will result in two Deriveds to end up in the insoluble set:
2766
2767 wc_simple = D [c] c [W]
2768 wc_insols = (c ~ [c]) [D], (c ~ [c]) [D]
2769 -}
2770
2771 -- Flatten skolems
2772 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2773 newFlattenSkolem :: CtFlavour -> CtLoc
2774 -> TyCon -> [TcType] -- F xis
2775 -> TcS (CtEvidence, Coercion, TcTyVar) -- [G/WD] x:: F xis ~ fsk
2776 newFlattenSkolem flav loc tc xis
2777 = do { stuff@(ev, co, fsk) <- new_skolem
2778 ; let fsk_ty = mkTyVarTy fsk
2779 ; extendFlatCache tc xis (co, fsk_ty, ctEvFlavour ev)
2780 ; return stuff }
2781 where
2782 fam_ty = mkTyConApp tc xis
2783
2784 new_skolem
2785 | Given <- flav
2786 = do { fsk <- wrapTcS (TcM.newFskTyVar fam_ty)
2787 ; let co = mkNomReflCo fam_ty
2788 ; ev <- newGivenEvVar loc (mkPrimEqPred fam_ty (mkTyVarTy fsk),
2789 EvCoercion co)
2790 ; return (ev, co, fsk) }
2791
2792 | otherwise -- Generate a [WD] for both Wanted and Derived
2793 -- See Note [No Derived CFunEqCans]
2794 = do { fmv <- wrapTcS (TcM.newFmvTyVar fam_ty)
2795 ; (ev, hole_co) <- newWantedEq loc Nominal fam_ty (mkTyVarTy fmv)
2796 ; return (ev, hole_co, fmv) }
2797
2798 extendFlatCache :: TyCon -> [Type] -> (TcCoercion, TcType, CtFlavour) -> TcS ()
2799 extendFlatCache tc xi_args stuff@(_, ty, fl)
2800 | isGivenOrWDeriv fl -- Maintain the invariant that inert_flat_cache
2801 -- only has [G] and [WD] CFunEqCans
2802 = do { dflags <- getDynFlags
2803 ; when (gopt Opt_FlatCache dflags) $
2804 do { traceTcS "extendFlatCache" (vcat [ ppr tc <+> ppr xi_args
2805 , ppr fl, ppr ty ])
2806 -- 'co' can be bottom, in the case of derived items
2807 ; updInertTcS $ \ is@(IS { inert_flat_cache = fc }) ->
2808 is { inert_flat_cache = insertExactFunEq fc tc xi_args stuff } } }
2809
2810 | otherwise
2811 = return ()
2812
2813 -- Instantiations
2814 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2815
2816 instDFunType :: DFunId -> [DFunInstType] -> TcS ([TcType], TcThetaType)
2817 instDFunType dfun_id inst_tys
2818 = wrapTcS $ TcM.instDFunType dfun_id inst_tys
2819
2820 newFlexiTcSTy :: Kind -> TcS TcType
2821 newFlexiTcSTy knd = wrapTcS (TcM.newFlexiTyVarTy knd)
2822
2823 cloneMetaTyVar :: TcTyVar -> TcS TcTyVar
2824 cloneMetaTyVar tv = wrapTcS (TcM.cloneMetaTyVar tv)
2825
2826 demoteUnfilledFmv :: TcTyVar -> TcS ()
2827 -- If a flatten-meta-var is still un-filled,
2828 -- turn it into an ordinary meta-var
2829 demoteUnfilledFmv fmv
2830 = wrapTcS $ do { is_filled <- TcM.isFilledMetaTyVar fmv
2831 ; unless is_filled $
2832 do { tv_ty <- TcM.newFlexiTyVarTy (tyVarKind fmv)
2833 ; TcM.writeMetaTyVar fmv tv_ty } }
2834
2835 instFlexi :: [TKVar] -> TcS TCvSubst
2836 instFlexi = instFlexiX emptyTCvSubst
2837
2838 instFlexiX :: TCvSubst -> [TKVar] -> TcS TCvSubst
2839 instFlexiX subst tvs
2840 = wrapTcS (foldlM instFlexiHelper subst tvs)
2841
2842 instFlexiHelper :: TCvSubst -> TKVar -> TcM TCvSubst
2843 instFlexiHelper subst tv
2844 = do { uniq <- TcM.newUnique
2845 ; details <- TcM.newMetaDetails TauTv
2846 ; let name = setNameUnique (tyVarName tv) uniq
2847 kind = substTyUnchecked subst (tyVarKind tv)
2848 ty' = mkTyVarTy (mkTcTyVar name kind details)
2849 ; return (extendTvSubst subst tv ty') }
2850
2851
2852 -- Creating and setting evidence variables and CtFlavors
2853 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2854
2855 data MaybeNew = Fresh CtEvidence | Cached EvTerm
2856
2857 isFresh :: MaybeNew -> Bool
2858 isFresh (Fresh {}) = True
2859 isFresh (Cached {}) = False
2860
2861 freshGoals :: [MaybeNew] -> [CtEvidence]
2862 freshGoals mns = [ ctev | Fresh ctev <- mns ]
2863
2864 getEvTerm :: MaybeNew -> EvTerm
2865 getEvTerm (Fresh ctev) = ctEvTerm ctev
2866 getEvTerm (Cached evt) = evt
2867
2868 setEvBind :: EvBind -> TcS ()
2869 setEvBind ev_bind
2870 = do { evb <- getTcEvBindsVar
2871 ; wrapTcS $ TcM.addTcEvBind evb ev_bind }
2872
2873 -- | Mark variables as used filling a coercion hole
2874 useVars :: CoVarSet -> TcS ()
2875 useVars vars
2876 = do { EvBindsVar { ebv_tcvs = ref } <- getTcEvBindsVar
2877 ; wrapTcS $
2878 do { tcvs <- TcM.readTcRef ref
2879 ; let tcvs' = tcvs `unionVarSet` vars
2880 ; TcM.writeTcRef ref tcvs' } }
2881
2882 -- | Equalities only
2883 setWantedEq :: TcEvDest -> Coercion -> TcS ()
2884 setWantedEq (HoleDest hole) co
2885 = do { useVars (coVarsOfCo co)
2886 ; wrapTcS $ TcM.fillCoercionHole hole co }
2887 setWantedEq (EvVarDest ev) _ = pprPanic "setWantedEq" (ppr ev)
2888
2889 -- | Equalities only
2890 setEqIfWanted :: CtEvidence -> Coercion -> TcS ()
2891 setEqIfWanted (CtWanted { ctev_dest = dest }) co = setWantedEq dest co
2892 setEqIfWanted _ _ = return ()
2893
2894 -- | Good for equalities and non-equalities
2895 setWantedEvTerm :: TcEvDest -> EvTerm -> TcS ()
2896 setWantedEvTerm (HoleDest hole) tm
2897 = do { let co = evTermCoercion tm
2898 ; useVars (coVarsOfCo co)
2899 ; wrapTcS $ TcM.fillCoercionHole hole co }
2900 setWantedEvTerm (EvVarDest ev) tm = setWantedEvBind ev tm
2901
2902 setWantedEvBind :: EvVar -> EvTerm -> TcS ()
2903 setWantedEvBind ev_id tm = setEvBind (mkWantedEvBind ev_id tm)
2904
2905 setEvBindIfWanted :: CtEvidence -> EvTerm -> TcS ()
2906 setEvBindIfWanted ev tm
2907 = case ev of
2908 CtWanted { ctev_dest = dest }
2909 -> setWantedEvTerm dest tm
2910 _ -> return ()
2911
2912 newTcEvBinds :: TcS EvBindsVar
2913 newTcEvBinds = wrapTcS TcM.newTcEvBinds
2914
2915 newEvVar :: TcPredType -> TcS EvVar
2916 newEvVar pred = wrapTcS (TcM.newEvVar pred)
2917
2918 newGivenEvVar :: CtLoc -> (TcPredType, EvTerm) -> TcS CtEvidence
2919 -- Make a new variable of the given PredType,
2920 -- immediately bind it to the given term
2921 -- and return its CtEvidence
2922 -- See Note [Bind new Givens immediately] in TcRnTypes
2923 newGivenEvVar loc (pred, rhs)
2924 = do { new_ev <- newBoundEvVarId pred rhs
2925 ; return (CtGiven { ctev_pred = pred, ctev_evar = new_ev, ctev_loc = loc }) }
2926
2927 -- | Make a new 'Id' of the given type, bound (in the monad's EvBinds) to the
2928 -- given term
2929 newBoundEvVarId :: TcPredType -> EvTerm -> TcS EvVar
2930 newBoundEvVarId pred rhs
2931 = do { new_ev <- newEvVar pred
2932 ; setEvBind (mkGivenEvBind new_ev rhs)
2933 ; return new_ev }
2934
2935 newGivenEvVars :: CtLoc -> [(TcPredType, EvTerm)] -> TcS [CtEvidence]
2936 newGivenEvVars loc pts = mapM (newGivenEvVar loc) pts
2937
2938 emitNewWantedEq :: CtLoc -> Role -> TcType -> TcType -> TcS Coercion
2939 -- | Emit a new Wanted equality into the work-list
2940 emitNewWantedEq loc role ty1 ty2
2941 | otherwise
2942 = do { (ev, co) <- newWantedEq loc role ty1 ty2
2943 ; updWorkListTcS $
2944 extendWorkListEq (mkNonCanonical ev)
2945 ; return co }
2946
2947 -- | Make a new equality CtEvidence
2948 newWantedEq :: CtLoc -> Role -> TcType -> TcType -> TcS (CtEvidence, Coercion)
2949 newWantedEq loc role ty1 ty2
2950 = do { hole <- wrapTcS $ TcM.newCoercionHole
2951 ; traceTcS "Emitting new coercion hole" (ppr hole <+> dcolon <+> ppr pty)
2952 ; return ( CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole
2953 , ctev_nosh = WDeriv
2954 , ctev_loc = loc}
2955 , mkHoleCo hole role ty1 ty2 ) }
2956 where
2957 pty = mkPrimEqPredRole role ty1 ty2
2958
2959 -- no equalities here. Use newWantedEq instead
2960 newWantedEvVarNC :: CtLoc -> TcPredType -> TcS CtEvidence
2961 -- Don't look up in the solved/inerts; we know it's not there
2962 newWantedEvVarNC loc pty
2963 = do { new_ev <- newEvVar pty
2964 ; traceTcS "Emitting new wanted" (ppr new_ev <+> dcolon <+> ppr pty $$
2965 pprCtLoc loc)
2966 ; return (CtWanted { ctev_pred = pty, ctev_dest = EvVarDest new_ev
2967 , ctev_nosh = WDeriv
2968 , ctev_loc = loc })}
2969
2970 newWantedEvVar :: CtLoc -> TcPredType -> TcS MaybeNew
2971 -- For anything except ClassPred, this is the same as newWantedEvVarNC
2972 newWantedEvVar loc pty
2973 = do { mb_ct <- lookupInInerts pty
2974 ; case mb_ct of
2975 Just ctev
2976 | not (isDerived ctev)
2977 -> do { traceTcS "newWantedEvVar/cache hit" $ ppr ctev
2978 ; return $ Cached (ctEvTerm ctev) }
2979 _ -> do { ctev <- newWantedEvVarNC loc pty
2980 ; return (Fresh ctev) } }
2981
2982 -- deals with both equalities and non equalities. Tries to look
2983 -- up non-equalities in the cache
2984 newWanted :: CtLoc -> PredType -> TcS MaybeNew
2985 newWanted loc pty
2986 | Just (role, ty1, ty2) <- getEqPredTys_maybe pty
2987 = Fresh . fst <$> newWantedEq loc role ty1 ty2
2988 | otherwise
2989 = newWantedEvVar loc pty
2990
2991 -- deals with both equalities and non equalities. Doesn't do any cache lookups.
2992 newWantedNC :: CtLoc -> PredType -> TcS CtEvidence
2993 newWantedNC loc pty
2994 | Just (role, ty1, ty2) <- getEqPredTys_maybe pty
2995 = fst <$> newWantedEq loc role ty1 ty2
2996 | otherwise
2997 = newWantedEvVarNC loc pty
2998
2999 emitNewDerived :: CtLoc -> TcPredType -> TcS ()
3000 emitNewDerived loc pred
3001 = do { ev <- newDerivedNC loc pred
3002 ; traceTcS "Emitting new derived" (ppr ev)
3003 ; updWorkListTcS (extendWorkListDerived loc ev) }
3004
3005 emitNewDeriveds :: CtLoc -> [TcPredType] -> TcS ()
3006 emitNewDeriveds loc preds
3007 | null preds
3008 = return ()
3009 | otherwise
3010 = do { evs <- mapM (newDerivedNC loc) preds
3011 ; traceTcS "Emitting new deriveds" (ppr evs)
3012 ; updWorkListTcS (extendWorkListDeriveds loc evs) }
3013
3014 emitNewDerivedEq :: CtLoc -> Role -> TcType -> TcType -> TcS ()
3015 -- Create new equality Derived and put it in the work list
3016 -- There's no caching, no lookupInInerts
3017 emitNewDerivedEq loc role ty1 ty2
3018 = do { ev <- newDerivedNC loc (mkPrimEqPredRole role ty1 ty2)
3019 ; traceTcS "Emitting new derived equality" (ppr ev $$ pprCtLoc loc)
3020 ; updWorkListTcS (extendWorkListDerived loc ev) }
3021
3022 newDerivedNC :: CtLoc -> TcPredType -> TcS CtEvidence
3023 newDerivedNC loc pred
3024 = do { -- checkReductionDepth loc pred
3025 ; return (CtDerived { ctev_pred = pred, ctev_loc = loc }) }
3026
3027 -- --------- Check done in TcInteract.selectNewWorkItem???? ---------
3028 -- | Checks if the depth of the given location is too much. Fails if
3029 -- it's too big, with an appropriate error message.
3030 checkReductionDepth :: CtLoc -> TcType -- ^ type being reduced
3031 -> TcS ()
3032 checkReductionDepth loc ty
3033 = do { dflags <- getDynFlags
3034 ; when (subGoalDepthExceeded dflags (ctLocDepth loc)) $
3035 wrapErrTcS $
3036 solverDepthErrorTcS loc ty }
3037
3038 matchFam :: TyCon -> [Type] -> TcS (Maybe (Coercion, TcType))
3039 matchFam tycon args = wrapTcS $ matchFamTcM tycon args
3040
3041 matchFamTcM :: TyCon -> [Type] -> TcM (Maybe (Coercion, TcType))
3042 -- Given (F tys) return (ty, co), where co :: F tys ~ ty
3043 matchFamTcM tycon args
3044 = do { fam_envs <- FamInst.tcGetFamInstEnvs
3045 ; let match_fam_result
3046 = reduceTyFamApp_maybe fam_envs Nominal tycon args
3047 ; TcM.traceTc "matchFamTcM" $
3048 vcat [ text "Matching:" <+> ppr (mkTyConApp tycon args)
3049 , ppr_res match_fam_result ]
3050 ; return match_fam_result }
3051 where
3052 ppr_res Nothing = text "Match failed"
3053 ppr_res (Just (co,ty)) = hang (text "Match succeeded:")
3054 2 (vcat [ text "Rewrites to:" <+> ppr ty
3055 , text "Coercion:" <+> ppr co ])
3056
3057 {-
3058 Note [Residual implications]
3059 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3060 The wl_implics in the WorkList are the residual implication
3061 constraints that are generated while solving or canonicalising the
3062 current worklist. Specifically, when canonicalising
3063 (forall a. t1 ~ forall a. t2)
3064 from which we get the implication
3065 (forall a. t1 ~ t2)
3066 See TcSMonad.deferTcSForAllEq
3067 -}
3068
3069 -- Deferring forall equalities as implications
3070 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3071
3072 deferTcSForAllEq :: Role -- Nominal or Representational
3073 -> CtLoc -- Original wanted equality flavor
3074 -> [Coercion] -- among the kinds of the binders
3075 -> ([TyVarBinder],TcType) -- ForAll tvs1 body1
3076 -> ([TyVarBinder],TcType) -- ForAll tvs2 body2
3077 -> TcS Coercion
3078 deferTcSForAllEq role loc kind_cos (bndrs1,body1) (bndrs2,body2)
3079 = do { let tvs1' = zipWithEqual "deferTcSForAllEq"
3080 mkCastTy (mkTyVarTys tvs1) kind_cos
3081 body2' = substTyWithUnchecked tvs2 tvs1' body2
3082 ; (subst, skol_tvs) <- wrapTcS $ TcM.tcInstSkolTyVars tvs1
3083 ; let phi1 = Type.substTyUnchecked subst body1
3084 phi2 = Type.substTyUnchecked subst body2'
3085 skol_info = UnifyForAllSkol phi1
3086
3087 ; (ctev, hole_co) <- newWantedEq loc role phi1 phi2
3088 ; env <- getLclEnv
3089 ; ev_binds <- newTcEvBinds
3090 -- We have nowhere to put these bindings
3091 -- but TcSimplify.setImplicationStatus
3092 -- checks that we don't actually use them
3093 ; let new_tclvl = pushTcLevel (tcl_tclvl env)
3094 wc = WC { wc_simple = singleCt (mkNonCanonical ctev)
3095 , wc_impl = emptyBag
3096 , wc_insol = emptyCts }
3097 imp = Implic { ic_tclvl = new_tclvl
3098 , ic_skols = skol_tvs
3099 , ic_no_eqs = True
3100 , ic_given = []
3101 , ic_wanted = wc
3102 , ic_status = IC_Unsolved
3103 , ic_binds = ev_binds
3104 , ic_env = env
3105 , ic_needed = emptyVarSet
3106 , ic_info = skol_info }
3107 ; updWorkListTcS (extendWorkListImplic imp)
3108 ; let cobndrs = zip skol_tvs kind_cos
3109 ; return $ mkForAllCos cobndrs hole_co }
3110 where
3111 tvs1 = binderVars bndrs1
3112 tvs2 = binderVars bndrs2