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