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