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