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