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