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