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