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