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