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