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