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