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