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