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