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