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