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