Newtype CoreMap and TypeMap so their keys are user-friendly.
[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,
9 extendWorkListCts, appendWorkList, selectWorkItem,
10 workListSize,
11 updWorkListTcS, updWorkListTcS_return,
12 runFlatten, emitFlatWork,
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 setWantedTyBind, reportUnifications,
30 setEvBind, setWantedEvBind, setEvBindIfWanted,
31 newEvVar, newGivenEvVar, newGivenEvVars,
32 newDerived, emitNewDerived,
33
34 getInstEnvs, getFamInstEnvs, -- Getting the environments
35 getTopEnv, getGblEnv, getTcEvBinds, getTcLevel,
36 getTcEvBindsMap,
37
38 -- Inerts
39 InertSet(..), InertCans(..),
40 updInertTcS, updInertCans, updInertDicts, updInertIrreds,
41 getNoGivenEqs, setInertCans, getInertEqs, getInertCans,
42 emptyInert, getTcSInerts, setTcSInerts,
43 getUnsolvedInerts, checkAllSolved,
44 splitInertCans, removeInertCts,
45 prepareInertsForImplications,
46 addInertCan, insertInertItemTcS, insertFunEq,
47 emitInsoluble, emitWorkNC,
48 EqualCtList,
49
50 -- Inert CDictCans
51 lookupInertDict, findDictsByClass, addDict, addDictsByClass, delDict, partitionDicts,
52
53 -- Inert CTyEqCans
54 findTyEqs,
55
56 -- Inert solved dictionaries
57 addSolvedDict, lookupSolvedDict,
58
59 -- The flattening cache
60 lookupFlatCache, extendFlatCache, newFlattenSkolem, -- Flatten skolems
61
62 -- Inert CFunEqCans
63 updInertFunEqs, findFunEq, sizeFunEqMap,
64 findFunEqsByTyCon, findFunEqs, partitionFunEqs,
65
66 instDFunType, -- Instantiation
67
68 -- MetaTyVars
69 newFlexiTcSTy, instFlexiTcS, instFlexiTcSHelperTcS,
70 cloneMetaTyVar, demoteUnfilledFmv,
71
72 TcLevel, isTouchableMetaTyVarTcS,
73 isFilledMetaTyVar_maybe, isFilledMetaTyVar,
74 zonkTyVarsAndFV, zonkTcType, zonkTcTyVar, zonkSimples,
75
76 -- References
77 newTcRef, readTcRef, updTcRef,
78
79 -- Misc
80 getDefaultInfo, getDynFlags, getGlobalRdrEnvTcS,
81 matchFam, matchFamTcM,
82 checkWellStagedDFun,
83 pprEq -- Smaller utils, re-exported from TcM
84 -- TODO (DV): these are only really used in the
85 -- instance matcher in TcSimplify. I am wondering
86 -- if the whole instance matcher simply belongs
87 -- here
88 ) where
89
90 #include "HsVersions.h"
91
92 import HscTypes
93
94 import qualified Inst as TcM
95 import InstEnv
96 import FamInst
97 import FamInstEnv
98
99 import qualified TcRnMonad as TcM
100 import qualified TcMType as TcM
101 import qualified TcEnv as TcM
102 ( checkWellStaged, topIdLvl, tcGetDefaultTys )
103 import Kind
104 import TcType
105 import DynFlags
106 import Type
107
108 import TcEvidence
109 import Class
110 import TyCon
111
112 import Name
113 import RdrName (RdrName, GlobalRdrEnv)
114 import RnEnv (addUsedRdrNames)
115 import Var
116 import VarEnv
117 import VarSet
118 import Outputable
119 import Bag
120 import UniqSupply
121
122 import FastString
123 import Util
124 import TcRnTypes
125
126 import Unique
127 import UniqFM
128 import Maybes ( orElse, firstJusts )
129
130 import TrieMap
131 import Control.Arrow ( first )
132 import Control.Monad( ap, when, unless, MonadPlus(..) )
133 import MonadUtils
134 import Data.IORef
135 import Data.List ( partition, foldl' )
136
137 #ifdef DEBUG
138 import Digraph
139 #endif
140
141 {-
142 ************************************************************************
143 * *
144 * Worklists *
145 * Canonical and non-canonical constraints that the simplifier has to *
146 * work on. Including their simplification depths. *
147 * *
148 * *
149 ************************************************************************
150
151 Note [WorkList priorities]
152 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
153 A WorkList contains canonical and non-canonical items (of all flavors).
154 Notice that each Ct now has a simplification depth. We may
155 consider using this depth for prioritization as well in the future.
156
157 As a simple form of priority queue, our worklist separates out
158 equalities (wl_eqs) from the rest of the canonical constraints,
159 so that it's easier to deal with them first, but the separation
160 is not strictly necessary. Notice that non-canonical constraints
161 are also parts of the worklist.
162
163 Note [The flattening work list]
164 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
165 The "flattening work list", held in the tcs_flat_work field of TcSEnv,
166 is a list of CFunEqCans generated during flattening. The key idea
167 is this. Consider flattening (Eq (F (G Int) (H Bool)):
168 * The flattener recursively calls itself on sub-terms before building
169 the main term, so it will encounter the terms in order
170 G Int
171 H Bool
172 F (G Int) (H Bool)
173 flattening to sub-goals
174 w1: G Int ~ fuv0
175 w2: H Bool ~ fuv1
176 w3: F fuv0 fuv1 ~ fuv2
177
178 * Processing w3 first is BAD, because we can't reduce i t,so it'll
179 get put into the inert set, and later kicked out when w1, w2 are
180 solved. In Trac #9872 this led to inert sets containing hundreds
181 of suspended calls.
182
183 * So we want to process w1, w2 first.
184
185 * So you might think that we should just use a FIFO deque for the work-list,
186 so that putting adding goals in order w1,w2,w3 would mean we processed
187 w1 first.
188
189 * BUT suppose we have 'type instance G Int = H Char'. Then processing
190 w1 leads to a new goal
191 w4: H Char ~ fuv0
192 We do NOT want to put that on the far end of a deque! Instead we want
193 to put it at the *front* of the work-list so that we continue to work
194 on it.
195
196 So the work-list structure is this:
197
198 * The wl_funeqs is a LIFO stack; we push new goals (such as w4) on
199 top (extendWorkListFunEq), and take new work from the top
200 (selectWorkItem).
201
202 * When flattening, emitFlatWork pushes new flattening goals (like
203 w1,w2,w3) onto the flattening work list, tcs_flat_work, another
204 push-down stack.
205
206 * When we finish flattening, we *reverse* the tcs_flat_work stack
207 onto the wl_funeqs stack (which brings w1 to the top).
208
209 The function runFlatten initialised the tcs_flat_work stack, and reverses
210 it onto wl_fun_eqs at the end.
211
212 -}
213
214 -- See Note [WorkList priorities]
215 data WorkList
216 = WL { wl_eqs :: [Ct]
217 , wl_funeqs :: [Ct] -- LIFO stack of goals
218 , wl_rest :: [Ct]
219 , wl_implics :: Bag Implication -- See Note [Residual implications]
220 }
221
222 appendWorkList :: WorkList -> WorkList -> WorkList
223 appendWorkList
224 (WL { wl_eqs = eqs1, wl_funeqs = funeqs1, wl_rest = rest1, wl_implics = implics1 })
225 (WL { wl_eqs = eqs2, wl_funeqs = funeqs2, wl_rest = rest2, wl_implics = implics2 })
226 = WL { wl_eqs = eqs1 ++ eqs2
227 , wl_funeqs = funeqs1 ++ funeqs2
228 , wl_rest = rest1 ++ rest2
229 , wl_implics = implics1 `unionBags` implics2 }
230
231
232 workListSize :: WorkList -> Int
233 workListSize (WL { wl_eqs = eqs, wl_funeqs = funeqs, wl_rest = rest })
234 = length eqs + length funeqs + length rest
235
236 extendWorkListEq :: Ct -> WorkList -> WorkList
237 extendWorkListEq ct wl
238 = wl { wl_eqs = ct : wl_eqs wl }
239
240 extendWorkListFunEq :: Ct -> WorkList -> WorkList
241 extendWorkListFunEq ct wl
242 = wl { wl_funeqs = ct : wl_funeqs wl }
243
244 extendWorkListNonEq :: Ct -> WorkList -> WorkList
245 -- Extension by non equality
246 extendWorkListNonEq ct wl
247 = wl { wl_rest = ct : wl_rest wl }
248
249 extendWorkListImplic :: Implication -> WorkList -> WorkList
250 extendWorkListImplic implic wl
251 = wl { wl_implics = implic `consBag` wl_implics wl }
252
253 extendWorkListCt :: Ct -> WorkList -> WorkList
254 -- Agnostic
255 extendWorkListCt ct wl
256 = case classifyPredType (ctPred ct) of
257 EqPred NomEq ty1 _
258 | Just (tc,_) <- tcSplitTyConApp_maybe ty1
259 , isTypeFamilyTyCon tc
260 -> extendWorkListFunEq ct wl
261 EqPred {}
262 -> extendWorkListEq ct wl
263
264 _ -> extendWorkListNonEq ct wl
265
266 extendWorkListCts :: [Ct] -> WorkList -> WorkList
267 -- Agnostic
268 extendWorkListCts cts wl = foldr extendWorkListCt wl cts
269
270 isEmptyWorkList :: WorkList -> Bool
271 isEmptyWorkList (WL { wl_eqs = eqs, wl_funeqs = funeqs
272 , wl_rest = rest, wl_implics = implics })
273 = null eqs && null rest && null funeqs && isEmptyBag implics
274
275 emptyWorkList :: WorkList
276 emptyWorkList = WL { wl_eqs = [], wl_rest = []
277 , wl_funeqs = [], wl_implics = emptyBag }
278
279 selectWorkItem :: WorkList -> (Maybe Ct, WorkList)
280 selectWorkItem wl@(WL { wl_eqs = eqs, wl_funeqs = feqs, wl_rest = rest })
281 = case (eqs,feqs,rest) of
282 (ct:cts,_,_) -> (Just ct, wl { wl_eqs = cts })
283 (_,ct:fes,_) -> (Just ct, wl { wl_funeqs = fes })
284 (_,_,ct:cts) -> (Just ct, wl { wl_rest = cts })
285 (_,_,_) -> (Nothing,wl)
286
287 -- Pretty printing
288 instance Outputable WorkList where
289 ppr (WL { wl_eqs = eqs, wl_funeqs = feqs
290 , wl_rest = rest, wl_implics = implics })
291 = text "WL" <+> (braces $
292 vcat [ ppUnless (null eqs) $
293 ptext (sLit "Eqs =") <+> vcat (map ppr eqs)
294 , ppUnless (null feqs) $
295 ptext (sLit "Funeqs =") <+> vcat (map ppr feqs)
296 , ppUnless (null rest) $
297 ptext (sLit "Non-eqs =") <+> vcat (map ppr rest)
298 , ppUnless (isEmptyBag implics) $
299 ptext (sLit "Implics =") <+> vcat (map ppr (bagToList implics))
300 ])
301
302 emitFlatWork :: Ct -> TcS ()
303 -- See Note [The flattening work list]
304 emitFlatWork ct
305 = TcS $ \env ->
306 do { let flat_ref = tcs_flat_work env
307 ; TcM.updTcRef flat_ref (ct :) }
308
309 runFlatten :: TcS a -> TcS a
310 -- Run thing_inside (which does flattening), and put all
311 -- the work it generates onto the main work list
312 -- See Note [The flattening work list]
313 runFlatten (TcS thing_inside)
314 = TcS $ \env ->
315 do { let flat_ref = tcs_flat_work env
316 ; old_flats <- TcM.updTcRefX flat_ref (\_ -> [])
317 ; res <- thing_inside env
318 ; new_flats <- TcM.updTcRefX flat_ref (\_ -> old_flats)
319 ; TcM.updTcRef (tcs_worklist env) (add_flats new_flats)
320 ; return res }
321 where
322 add_flats new_flats wl
323 = wl { wl_funeqs = add_funeqs new_flats (wl_funeqs wl) }
324
325 add_funeqs [] wl = wl
326 add_funeqs (f:fs) wl = add_funeqs fs (f:wl)
327 -- add_funeqs fs ws = reverse fs ++ ws
328 -- e.g. add_funeqs [f1,f2,f3] [w1,w2,w3,w4]
329 -- = [f3,f2,f1,w1,w2,w3,w4]
330
331 {-
332 ************************************************************************
333 * *
334 * Inert Sets *
335 * *
336 * *
337 ************************************************************************
338
339 Note [Detailed InertCans Invariants]
340 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
341 The InertCans represents a collection of constraints with the following properties:
342
343 * All canonical
344
345 * No two dictionaries with the same head
346 * No two CIrreds with the same type
347
348 * Family equations inert wrt top-level family axioms
349
350 * Dictionaries have no matching top-level instance
351
352 * Given family or dictionary constraints don't mention touchable
353 unification variables
354
355 * Non-CTyEqCan constraints are fully rewritten with respect
356 to the CTyEqCan equalities (modulo canRewrite of course;
357 eg a wanted cannot rewrite a given)
358
359 * CTyEqCan equalities: see Note [Applying the inert substitution]
360 in TcFlatten
361
362 Note [Type family equations]
363 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
364 Type-family equations, of form (ev : F tys ~ ty), live in three places
365
366 * The work-list, of course
367
368 * The inert_flat_cache. This is used when flattening, to get maximal
369 sharing. It contains lots of things that are still in the work-list.
370 E.g Suppose we have (w1: F (G a) ~ Int), and (w2: H (G a) ~ Int) in the
371 work list. Then we flatten w1, dumping (w3: G a ~ f1) in the work
372 list. Now if we flatten w2 before we get to w3, we still want to
373 share that (G a).
374
375 Because it contains work-list things, DO NOT use the flat cache to solve
376 a top-level goal. Eg in the above example we don't want to solve w3
377 using w3 itself!
378
379 * The inert_funeqs are un-solved but fully processed and in the InertCans.
380
381 Note [Solved dictionaries]
382 ~~~~~~~~~~~~~~~~~~~~~~~~~~
383 When we apply a top-level instance declararation, we add the "solved"
384 dictionary to the inert_solved_dicts. In general, we use it to avoid
385 creating a new EvVar when we have a new goal that we have solved in
386 the past.
387
388 But in particular, we can use it to create *recursive* dicationaries.
389 The simplest, degnerate case is
390 instance C [a] => C [a] where ...
391 If we have
392 [W] d1 :: C [x]
393 then we can apply the instance to get
394 d1 = $dfCList d
395 [W] d2 :: C [x]
396 Now 'd1' goes in inert_solved_dicts, and we can solve d2 directly from d1.
397 d1 = $dfCList d
398 d2 = d1
399
400 See Note [Example of recursive dictionaries]
401 Other notes about solved dictionaries
402
403 * See also Note [Do not add superclasses of solved dictionaries]
404
405 * The inert_solved_dicts field is not rewritten by equalities, so it may
406 get out of date.
407
408 Note [Do not add superclasses of solved dictionaries]
409 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
410 Every member of inert_solved_dicts is the result of applying a dictionary
411 function, NOT of applying superclass selection to anything.
412 Consider
413
414 class Ord a => C a where
415 instance Ord [a] => C [a] where ...
416
417 Suppose we are trying to solve
418 [G] d1 : Ord a
419 [W] d2 : C [a]
420
421 Then we'll use the instance decl to give
422
423 [G] d1 : Ord a Solved: d2 : C [a] = $dfCList d3
424 [W] d3 : Ord [a]
425
426 We must not add d4 : Ord [a] to the 'solved' set (by taking the
427 superclass of d2), otherwise we'll use it to solve d3, without ever
428 using d1, which would be a catastrophe.
429
430 Solution: when extending the solved dictionaries, do not add superclasses.
431 That's why each element of the inert_solved_dicts is the result of applying
432 a dictionary function.
433
434 Note [Example of recursive dictionaries]
435 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
436 --- Example 1
437
438 data D r = ZeroD | SuccD (r (D r));
439
440 instance (Eq (r (D r))) => Eq (D r) where
441 ZeroD == ZeroD = True
442 (SuccD a) == (SuccD b) = a == b
443 _ == _ = False;
444
445 equalDC :: D [] -> D [] -> Bool;
446 equalDC = (==);
447
448 We need to prove (Eq (D [])). Here's how we go:
449
450 [W] d1 : Eq (D [])
451 By instance decl of Eq (D r):
452 [W] d2 : Eq [D []] where d1 = dfEqD d2
453 By instance decl of Eq [a]:
454 [W] d3 : Eq (D []) where d2 = dfEqList d3
455 d1 = dfEqD d2
456 Now this wanted can interact with our "solved" d1 to get:
457 d3 = d1
458
459 -- Example 2:
460 This code arises in the context of "Scrap Your Boilerplate with Class"
461
462 class Sat a
463 class Data ctx a
464 instance Sat (ctx Char) => Data ctx Char -- dfunData1
465 instance (Sat (ctx [a]), Data ctx a) => Data ctx [a] -- dfunData2
466
467 class Data Maybe a => Foo a
468
469 instance Foo t => Sat (Maybe t) -- dfunSat
470
471 instance Data Maybe a => Foo a -- dfunFoo1
472 instance Foo a => Foo [a] -- dfunFoo2
473 instance Foo [Char] -- dfunFoo3
474
475 Consider generating the superclasses of the instance declaration
476 instance Foo a => Foo [a]
477
478 So our problem is this
479 [G] d0 : Foo t
480 [W] d1 : Data Maybe [t] -- Desired superclass
481
482 We may add the given in the inert set, along with its superclasses
483 Inert:
484 [G] d0 : Foo t
485 [G] d01 : Data Maybe t -- Superclass of d0
486 WorkList
487 [W] d1 : Data Maybe [t]
488
489 Solve d1 using instance dfunData2; d1 := dfunData2 d2 d3
490 Inert:
491 [G] d0 : Foo t
492 [G] d01 : Data Maybe t -- Superclass of d0
493 Solved:
494 d1 : Data Maybe [t]
495 WorkList:
496 [W] d2 : Sat (Maybe [t])
497 [W] d3 : Data Maybe t
498
499 Now, we may simplify d2 using dfunSat; d2 := dfunSat d4
500 Inert:
501 [G] d0 : Foo t
502 [G] d01 : Data Maybe t -- Superclass of d0
503 Solved:
504 d1 : Data Maybe [t]
505 d2 : Sat (Maybe [t])
506 WorkList:
507 [W] d3 : Data Maybe t
508 [W] d4 : Foo [t]
509
510 Now, we can just solve d3 from d01; d3 := d01
511 Inert
512 [G] d0 : Foo t
513 [G] d01 : Data Maybe t -- Superclass of d0
514 Solved:
515 d1 : Data Maybe [t]
516 d2 : Sat (Maybe [t])
517 WorkList
518 [W] d4 : Foo [t]
519
520 Now, solve d4 using dfunFoo2; d4 := dfunFoo2 d5
521 Inert
522 [G] d0 : Foo t
523 [G] d01 : Data Maybe t -- Superclass of d0
524 Solved:
525 d1 : Data Maybe [t]
526 d2 : Sat (Maybe [t])
527 d4 : Foo [t]
528 WorkList:
529 [W] d5 : Foo t
530
531 Now, d5 can be solved! d5 := d0
532
533 Result
534 d1 := dfunData2 d2 d3
535 d2 := dfunSat d4
536 d3 := d01
537 d4 := dfunFoo2 d5
538 d5 := d0
539 -}
540
541 -- All Given (fully known) or Wanted or Derived
542 -- See Note [Detailed InertCans Invariants] for more
543 data InertCans
544 = IC { inert_eqs :: TyVarEnv EqualCtList
545 -- All CTyEqCans with NomEq; index is the LHS tyvar
546
547 , inert_funeqs :: FunEqMap Ct
548 -- All CFunEqCans; index is the whole family head type.
549
550 , inert_dicts :: DictMap Ct
551 -- Dictionaries only, index is the class
552 -- NB: index is /not/ the whole type because FD reactions
553 -- need to match the class but not necessarily the whole type.
554
555 , inert_irreds :: Cts
556 -- Irreducible predicates
557
558 , inert_insols :: Cts
559 -- Frozen errors (as non-canonicals)
560 }
561
562 type EqualCtList = [Ct]
563 {-
564 Note [EqualCtList invariants]
565 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
566 * All are equalities
567 * All these equalities have the same LHS
568 * The list is never empty
569 * No element of the list can rewrite any other
570
571 From the fourth invariant it follows that the list is
572 - A single Given, or
573 - Any number of Wanteds and/or Deriveds
574 -}
575
576 -- The Inert Set
577 data InertSet
578 = IS { inert_cans :: InertCans
579 -- Canonical Given, Wanted, Derived (no Solved)
580 -- Sometimes called "the inert set"
581
582 , inert_flat_cache :: FunEqMap (TcCoercion, TcType, CtFlavour)
583 -- See Note [Type family equations]
584 -- If F tys :-> (co, ty, ev),
585 -- then co :: F tys ~ ty
586 --
587 -- Just a hash-cons cache for use when flattening only
588 -- These include entirely un-processed goals, so don't use
589 -- them to solve a top-level goal, else you may end up solving
590 -- (w:F ty ~ a) by setting w:=w! We just use the flat-cache
591 -- when allocating a new flatten-skolem.
592 -- Not necessarily inert wrt top-level equations (or inert_cans)
593
594 , inert_solved_dicts :: DictMap CtEvidence
595 -- Of form ev :: C t1 .. tn
596 -- See Note [Solved dictionaries]
597 -- and Note [Do not add superclasses of solved dictionaries]
598 }
599
600 instance Outputable InertCans where
601 ppr ics = vcat [ ptext (sLit "Equalities:")
602 <+> pprCts (foldVarEnv (\eqs rest -> listToBag eqs `andCts` rest)
603 emptyCts (inert_eqs ics))
604 , ptext (sLit "Type-function equalities:")
605 <+> pprCts (funEqsToBag (inert_funeqs ics))
606 , ptext (sLit "Dictionaries:")
607 <+> pprCts (dictsToBag (inert_dicts ics))
608 , ptext (sLit "Irreds:")
609 <+> pprCts (inert_irreds ics)
610 , text "Insolubles =" <+> -- Clearly print frozen errors
611 braces (vcat (map ppr (Bag.bagToList $ inert_insols ics)))
612 ]
613
614 instance Outputable InertSet where
615 ppr is = vcat [ ppr $ inert_cans is
616 , text "Solved dicts" <+> vcat (map ppr (bagToList (dictsToBag (inert_solved_dicts is)))) ]
617
618 emptyInert :: InertSet
619 emptyInert
620 = IS { inert_cans = IC { inert_eqs = emptyVarEnv
621 , inert_dicts = emptyDicts
622 , inert_funeqs = emptyFunEqs
623 , inert_irreds = emptyCts
624 , inert_insols = emptyCts
625 }
626 , inert_flat_cache = emptyFunEqs
627 , inert_solved_dicts = emptyDictMap }
628
629 ---------------
630 addInertCan :: InertCans -> Ct -> InertCans
631 -- Precondition: item /is/ canonical
632 addInertCan ics item@(CTyEqCan {})
633 = ics { inert_eqs = add_eq (inert_eqs ics) item }
634 where
635 add_eq :: TyVarEnv EqualCtList -> Ct -> TyVarEnv EqualCtList
636 add_eq old_list it
637 = extendVarEnv_C (\old_eqs _new_eqs -> it : old_eqs)
638 old_list (cc_tyvar it) [it]
639
640 addInertCan ics item@(CFunEqCan { cc_fun = tc, cc_tyargs = tys })
641 = ics { inert_funeqs = insertFunEq (inert_funeqs ics) tc tys item }
642
643 addInertCan ics item@(CIrredEvCan {})
644 = ics { inert_irreds = inert_irreds ics `Bag.snocBag` item }
645 -- The 'False' is because the irreducible constraint might later instantiate
646 -- to an equality.
647 -- But since we try to simplify first, if there's a constraint function FC with
648 -- type instance FC Int = Show
649 -- we'll reduce a constraint (FC Int a) to Show a, and never add an inert irreducible
650
651 addInertCan ics item@(CDictCan { cc_class = cls, cc_tyargs = tys })
652 = ics { inert_dicts = addDict (inert_dicts ics) cls tys item }
653
654 addInertCan _ item
655 = pprPanic "upd_inert set: can't happen! Inserting " $
656 ppr item -- Can't be CNonCanonical, CHoleCan,
657 -- because they only land in inert_insols
658
659 --------------
660 insertInertItemTcS :: Ct -> TcS ()
661 -- Add a new item in the inerts of the monad
662 insertInertItemTcS item
663 = do { traceTcS "insertInertItemTcS {" $
664 text "Trying to insert new inert item:" <+> ppr item
665
666 ; updInertCans (\ics -> addInertCan ics item)
667
668 ; traceTcS "insertInertItemTcS }" $ empty }
669
670 addSolvedDict :: CtEvidence -> Class -> [Type] -> TcS ()
671 -- Add a new item in the solved set of the monad
672 -- See Note [Solved dictionaries]
673 addSolvedDict item cls tys
674 | isIPPred (ctEvPred item) -- Never cache "solved" implicit parameters (not sure why!)
675 = return ()
676 | otherwise
677 = do { traceTcS "updSolvedSetTcs:" $ ppr item
678 ; updInertTcS $ \ ics ->
679 ics { inert_solved_dicts = addDict (inert_solved_dicts ics) cls tys item } }
680
681 updInertTcS :: (InertSet -> InertSet) -> TcS ()
682 -- Modify the inert set with the supplied function
683 updInertTcS upd_fn
684 = do { is_var <- getTcSInertsRef
685 ; wrapTcS (do { curr_inert <- TcM.readTcRef is_var
686 ; TcM.writeTcRef is_var (upd_fn curr_inert) }) }
687
688 getInertCans :: TcS InertCans
689 getInertCans = do { inerts <- getTcSInerts; return (inert_cans inerts) }
690
691 setInertCans :: InertCans -> TcS ()
692 setInertCans ics = updInertTcS $ \ inerts -> inerts { inert_cans = ics }
693
694 updInertCans :: (InertCans -> InertCans) -> TcS ()
695 -- Modify the inert set with the supplied function
696 updInertCans upd_fn
697 = updInertTcS $ \ inerts -> inerts { inert_cans = upd_fn (inert_cans inerts) }
698
699 updInertDicts :: (DictMap Ct -> DictMap Ct) -> TcS ()
700 -- Modify the inert set with the supplied function
701 updInertDicts upd_fn
702 = updInertCans $ \ ics -> ics { inert_dicts = upd_fn (inert_dicts ics) }
703
704 updInertFunEqs :: (FunEqMap Ct -> FunEqMap Ct) -> TcS ()
705 -- Modify the inert set with the supplied function
706 updInertFunEqs upd_fn
707 = updInertCans $ \ ics -> ics { inert_funeqs = upd_fn (inert_funeqs ics) }
708
709 updInertIrreds :: (Cts -> Cts) -> TcS ()
710 -- Modify the inert set with the supplied function
711 updInertIrreds upd_fn
712 = updInertCans $ \ ics -> ics { inert_irreds = upd_fn (inert_irreds ics) }
713
714
715 prepareInertsForImplications :: InertSet -> (InertSet)
716 -- See Note [Preparing inert set for implications]
717 prepareInertsForImplications is@(IS { inert_cans = cans })
718 = is { inert_cans = getGivens cans
719 , inert_flat_cache = emptyFunEqs } -- See Note [Do not inherit the flat cache]
720 where
721 getGivens (IC { inert_eqs = eqs
722 , inert_irreds = irreds
723 , inert_funeqs = funeqs
724 , inert_dicts = dicts })
725 = IC { inert_eqs = filterVarEnv is_given_ecl eqs
726 , inert_funeqs = filterFunEqs isGivenCt funeqs
727 , inert_irreds = Bag.filterBag isGivenCt irreds
728 , inert_dicts = filterDicts isGivenCt dicts
729 , inert_insols = emptyCts }
730
731 is_given_ecl :: EqualCtList -> Bool
732 is_given_ecl (ct:rest) | isGivenCt ct = ASSERT( null rest ) True
733 is_given_ecl _ = False
734
735 {-
736 Note [Do not inherit the flat cache]
737 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
738 We do not want to inherit the flat cache when processing nested
739 implications. Consider
740 a ~ F b, forall c. b~Int => blah
741 If we have F b ~ fsk in the flat-cache, and we push that into the
742 nested implication, we might miss that F b can be rewritten to F Int,
743 and hence perhpas solve it. Moreover, the fsk from outside is
744 flattened out after solving the outer level, but and we don't
745 do that flattening recursively.
746
747 Note [Preparing inert set for implications]
748 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
749 Before solving the nested implications, we trim the inert set,
750 retaining only Givens. These givens can be used when solving
751 the inner implications.
752
753 There might be cases where interactions between wanteds at different levels
754 could help to solve a constraint. For example
755
756 class C a b | a -> b
757 (C Int alpha), (forall d. C d blah => C Int a)
758
759 If we pushed the (C Int alpha) inwards, as a given, it can produce a
760 fundep (alpha~a) and this can float out again and be used to fix
761 alpha. (In general we can't float class constraints out just in case
762 (C d blah) might help to solve (C Int a).) But we ignore this possiblity.
763
764 For Derived constraints we don't have evidence, so we do not turn
765 them into Givens. There can *be* deriving CFunEqCans; see Trac #8129.
766 -}
767
768 getInertEqs :: TcS (TyVarEnv EqualCtList)
769 getInertEqs
770 = do { inert <- getTcSInerts
771 ; return (inert_eqs (inert_cans inert)) }
772
773 getUnsolvedInerts :: TcS ( Bag Implication
774 , Cts -- Tyvar eqs: a ~ ty
775 , Cts -- Fun eqs: F a ~ ty
776 , Cts -- Insoluble
777 , Cts ) -- All others
778 getUnsolvedInerts
779 = do { IC { inert_eqs = tv_eqs
780 , inert_funeqs = fun_eqs
781 , inert_irreds = irreds, inert_dicts = idicts
782 , inert_insols = insols } <- getInertCans
783
784 ; let unsolved_tv_eqs = foldVarEnv (\cts rest ->
785 foldr add_if_unsolved rest cts)
786 emptyCts tv_eqs
787 unsolved_fun_eqs = foldFunEqs add_if_unsolved fun_eqs emptyCts
788 unsolved_irreds = Bag.filterBag is_unsolved irreds
789 unsolved_dicts = foldDicts add_if_unsolved idicts emptyCts
790
791 others = unsolved_irreds `unionBags` unsolved_dicts
792
793 ; implics <- getWorkListImplics
794
795 ; return ( implics, unsolved_tv_eqs, unsolved_fun_eqs, insols, others) }
796 -- Keep even the given insolubles
797 -- so that we can report dead GADT pattern match branches
798 where
799 add_if_unsolved :: Ct -> Cts -> Cts
800 add_if_unsolved ct cts | is_unsolved ct = ct `consCts` cts
801 | otherwise = cts
802
803 is_unsolved ct = not (isGivenCt ct) -- Wanted or Derived
804
805 getNoGivenEqs :: TcLevel -- TcLevel of this implication
806 -> [TcTyVar] -- Skolems of this implication
807 -> TcS Bool -- True <=> definitely no residual given equalities
808 -- See Note [When does an implication have given equalities?]
809 getNoGivenEqs tclvl skol_tvs
810 = do { inerts@(IC { inert_eqs = ieqs, inert_irreds = iirreds, inert_funeqs = funeqs })
811 <- getInertCans
812 ; let local_fsks = foldFunEqs add_fsk funeqs emptyVarSet
813
814 has_given_eqs = foldrBag ((||) . ev_given_here . ctEvidence) False iirreds
815 || foldVarEnv ((||) . eqs_given_here local_fsks) False ieqs
816
817 ; traceTcS "getNoGivenEqs" (vcat [ppr has_given_eqs, ppr inerts])
818 ; return (not has_given_eqs) }
819 where
820 eqs_given_here :: VarSet -> EqualCtList -> Bool
821 eqs_given_here local_fsks [CTyEqCan { cc_tyvar = tv, cc_ev = ev }]
822 -- Givens are always a sigleton
823 = not (skolem_bound_here local_fsks tv) && ev_given_here ev
824 eqs_given_here _ _ = False
825
826 ev_given_here :: CtEvidence -> Bool
827 -- True for a Given bound by the curent implication,
828 -- i.e. the current level
829 ev_given_here ev
830 = isGiven ev
831 && tclvl == ctLocLevel (ctEvLoc ev)
832
833 add_fsk :: Ct -> VarSet -> VarSet
834 add_fsk ct fsks | CFunEqCan { cc_fsk = tv, cc_ev = ev } <- ct
835 , isGiven ev = extendVarSet fsks tv
836 | otherwise = fsks
837
838 skol_tv_set = mkVarSet skol_tvs
839 skolem_bound_here local_fsks tv -- See Note [Let-bound skolems]
840 = case tcTyVarDetails tv of
841 SkolemTv {} -> tv `elemVarSet` skol_tv_set
842 FlatSkol {} -> not (tv `elemVarSet` local_fsks)
843 _ -> False
844
845 {-
846 Note [When does an implication have given equalities?]
847 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
848 Consider an implication
849 beta => alpha ~ Int
850 where beta is a unification variable that has already been unified
851 to () in an outer scope. Then we can float the (alpha ~ Int) out
852 just fine. So when deciding whether the givens contain an equality,
853 we should canonicalise first, rather than just looking at the original
854 givens (Trac #8644).
855
856 So we simply look at the inert, canonical Givens and see if there are
857 any equalities among them, the calculation of has_given_eqs. There
858 are some wrinkles:
859
860 * We must know which ones are bound in *this* implication and which
861 are bound further out. We can find that out from the TcLevel
862 of the Given, which is itself recorded in the tcl_tclvl field
863 of the TcLclEnv stored in the Given (ev_given_here).
864
865 What about interactions between inner and outer givens?
866 - Outer given is rewritten by an inner given, then there must
867 have been an inner given equality, hence the “given-eq” flag
868 will be true anyway.
869
870 - Inner given rewritten by outer, retains its level (ie. The inner one)
871
872 * We must take account of *potential* equalities, like the one above:
873 beta => ...blah...
874 If we still don't know what beta is, we conservatively treat it as potentially
875 becoming an equality. Hence including 'irreds' in the calculation or has_given_eqs.
876
877 * When flattening givens, we generate Given equalities like
878 <F [a]> : F [a] ~ f,
879 with Refl evidence, and we *don't* want those to count as an equality
880 in the givens! After all, the entire flattening business is just an
881 internal matter, and the evidence does not mention any of the 'givens'
882 of this implication. So we do not treat inert_funeqs as a 'given equality'.
883
884 * See Note [Let-bound skolems] for another wrinkle
885
886 * We do *not* need to worry about representational equalities, because
887 these do not affect the ability to float constraints.
888
889 Note [Let-bound skolems]
890 ~~~~~~~~~~~~~~~~~~~~~~~~
891 If * the inert set contains a canonical Given CTyEqCan (a ~ ty)
892 and * 'a' is a skolem bound in this very implication, b
893
894 then:
895 a) The Given is pretty much a let-binding, like
896 f :: (a ~ b->c) => a -> a
897 Here the equality constraint is like saying
898 let a = b->c in ...
899 It is not adding any new, local equality information,
900 and hence can be ignored by has_given_eqs
901
902 b) 'a' will have been completely substituted out in the inert set,
903 so we can safely discard it. Notably, it doesn't need to be
904 returned as part of 'fsks'
905
906 For an example, see Trac #9211.
907 -}
908
909 splitInertCans :: InertCans -> ([Ct], [Ct], [Ct])
910 -- ^ Extract the (given, derived, wanted) inert constraints
911 splitInertCans iCans = (given,derived,wanted)
912 where
913 allCts = foldDicts (:) (inert_dicts iCans)
914 $ foldFunEqs (:) (inert_funeqs iCans)
915 $ concat (varEnvElts (inert_eqs iCans))
916
917 (derived,other) = partition isDerivedCt allCts
918 (wanted,given) = partition isWantedCt other
919
920 removeInertCts :: [Ct] -> InertCans -> InertCans
921 -- ^ Remove inert constraints from the 'InertCans', for use when a
922 -- typechecker plugin wishes to discard a given.
923 removeInertCts cts icans = foldl' removeInertCt icans cts
924
925 removeInertCt :: InertCans -> Ct -> InertCans
926 removeInertCt is ct =
927 case ct of
928
929 CDictCan { cc_class = cl, cc_tyargs = tys } ->
930 is { inert_dicts = delDict (inert_dicts is) cl tys }
931
932 CFunEqCan { cc_fun = tf, cc_tyargs = tys } ->
933 is { inert_funeqs = delFunEq (inert_funeqs is) tf tys }
934
935 CTyEqCan { cc_tyvar = x, cc_rhs = ty } ->
936 is { inert_eqs = delTyEq (inert_eqs is) x ty }
937
938 CIrredEvCan {} -> panic "removeInertCt: CIrredEvCan"
939 CNonCanonical {} -> panic "removeInertCt: CNonCanonical"
940 CHoleCan {} -> panic "removeInertCt: CHoleCan"
941
942
943 checkAllSolved :: TcS Bool
944 -- True if there are no unsolved wanteds
945 -- Ignore Derived for this purpose, unless in insolubles
946 checkAllSolved
947 = do { is <- getTcSInerts
948
949 ; let icans = inert_cans is
950 unsolved_irreds = Bag.anyBag isWantedCt (inert_irreds icans)
951 unsolved_dicts = foldDicts ((||) . isWantedCt)
952 (inert_dicts icans) False
953 unsolved_funeqs = foldFunEqs ((||) . isWantedCt)
954 (inert_funeqs icans) False
955 unsolved_eqs = foldVarEnv ((||) . any isWantedCt) False
956 (inert_eqs icans)
957
958 ; return (not (unsolved_eqs || unsolved_irreds
959 || unsolved_dicts || unsolved_funeqs
960 || not (isEmptyBag (inert_insols icans)))) }
961
962 lookupFlatCache :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcType, CtFlavour))
963 lookupFlatCache fam_tc tys
964 = do { IS { inert_flat_cache = flat_cache
965 , inert_cans = IC { inert_funeqs = inert_funeqs } } <- getTcSInerts
966 ; return (firstJusts [lookup_inerts inert_funeqs,
967 lookup_flats flat_cache]) }
968 where
969 lookup_inerts inert_funeqs
970 | Just (CFunEqCan { cc_ev = ctev, cc_fsk = fsk })
971 <- findFunEqs inert_funeqs fam_tc tys
972 = Just (ctEvCoercion ctev, mkTyVarTy fsk, ctEvFlavour ctev)
973 | otherwise = Nothing
974
975 lookup_flats flat_cache = findFunEq flat_cache fam_tc tys
976
977
978 lookupInInerts :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence)
979 -- Is this exact predicate type cached in the solved or canonicals of the InertSet?
980 lookupInInerts loc pty
981 | ClassPred cls tys <- classifyPredType pty
982 = do { inerts <- getTcSInerts
983 ; return (lookupSolvedDict inerts loc cls tys `mplus`
984 lookupInertDict (inert_cans inerts) loc cls tys) }
985 | otherwise -- NB: No caching for equalities, IPs, holes, or errors
986 = return Nothing
987
988 lookupInertDict :: InertCans -> CtLoc -> Class -> [Type] -> Maybe CtEvidence
989 lookupInertDict (IC { inert_dicts = dicts }) loc cls tys
990 = case findDict dicts cls tys of
991 Just ct | let ev = ctEvidence ct
992 , ctEvCheckDepth cls loc ev
993 -> Just ev
994 _ -> Nothing
995
996 lookupSolvedDict :: InertSet -> CtLoc -> Class -> [Type] -> Maybe CtEvidence
997 -- Returns just if exactly this predicate type exists in the solved.
998 lookupSolvedDict (IS { inert_solved_dicts = solved }) loc cls tys
999 = case findDict solved cls tys of
1000 Just ev | ctEvCheckDepth cls loc ev -> Just ev
1001 _ -> Nothing
1002
1003 {-
1004 ************************************************************************
1005 * *
1006 TyEqMap
1007 * *
1008 ************************************************************************
1009 -}
1010
1011 type TyEqMap a = TyVarEnv a
1012
1013 findTyEqs :: InertCans -> TyVar -> EqualCtList
1014 findTyEqs icans tv = lookupVarEnv (inert_eqs icans) tv `orElse` []
1015
1016 delTyEq :: TyEqMap EqualCtList -> TcTyVar -> TcType -> TyEqMap EqualCtList
1017 delTyEq m tv t = modifyVarEnv (filter (not . isThisOne)) m tv
1018 where isThisOne (CTyEqCan { cc_rhs = t1 }) = eqType t t1
1019 isThisOne _ = False
1020
1021 {-
1022 ************************************************************************
1023 * *
1024 TcAppMap, DictMap, FunEqMap
1025 * *
1026 ************************************************************************
1027 -}
1028
1029 type TcAppMap a = UniqFM (ListMap TypeMap a)
1030 -- Indexed by tycon then the arg types
1031 -- Used for types and classes; hence UniqFM
1032
1033 emptyTcAppMap :: TcAppMap a
1034 emptyTcAppMap = emptyUFM
1035
1036 findTcApp :: TcAppMap a -> Unique -> [Type] -> Maybe a
1037 findTcApp m u tys = do { tys_map <- lookupUFM m u
1038 ; lookupTM tys tys_map }
1039
1040 delTcApp :: TcAppMap a -> Unique -> [Type] -> TcAppMap a
1041 delTcApp m cls tys = adjustUFM (deleteTM tys) m cls
1042
1043 insertTcApp :: TcAppMap a -> Unique -> [Type] -> a -> TcAppMap a
1044 insertTcApp m cls tys ct = alterUFM alter_tm m cls
1045 where
1046 alter_tm mb_tm = Just (insertTM tys ct (mb_tm `orElse` emptyTM))
1047
1048 -- mapTcApp :: (a->b) -> TcAppMap a -> TcAppMap b
1049 -- mapTcApp f = mapUFM (mapTM f)
1050
1051 filterTcAppMap :: (Ct -> Bool) -> TcAppMap Ct -> TcAppMap Ct
1052 filterTcAppMap f m
1053 = mapUFM do_tm m
1054 where
1055 do_tm tm = foldTM insert_mb tm emptyTM
1056 insert_mb ct tm
1057 | f ct = insertTM tys ct tm
1058 | otherwise = tm
1059 where
1060 tys = case ct of
1061 CFunEqCan { cc_tyargs = tys } -> tys
1062 CDictCan { cc_tyargs = tys } -> tys
1063 _ -> pprPanic "filterTcAppMap" (ppr ct)
1064
1065 tcAppMapToBag :: TcAppMap a -> Bag a
1066 tcAppMapToBag m = foldTcAppMap consBag m emptyBag
1067
1068 foldTcAppMap :: (a -> b -> b) -> TcAppMap a -> b -> b
1069 foldTcAppMap k m z = foldUFM (foldTM k) z m
1070
1071 -------------------------
1072 type DictMap a = TcAppMap a
1073
1074 emptyDictMap :: DictMap a
1075 emptyDictMap = emptyTcAppMap
1076
1077 -- sizeDictMap :: DictMap a -> Int
1078 -- sizeDictMap m = foldDicts (\ _ x -> x+1) m 0
1079
1080 findDict :: DictMap a -> Class -> [Type] -> Maybe a
1081 findDict m cls tys = findTcApp m (getUnique cls) tys
1082
1083 findDictsByClass :: DictMap a -> Class -> Bag a
1084 findDictsByClass m cls
1085 | Just tm <- lookupUFM m cls = foldTM consBag tm emptyBag
1086 | otherwise = emptyBag
1087
1088 delDict :: DictMap a -> Class -> [Type] -> DictMap a
1089 delDict m cls tys = delTcApp m (getUnique cls) tys
1090
1091 addDict :: DictMap a -> Class -> [Type] -> a -> DictMap a
1092 addDict m cls tys item = insertTcApp m (getUnique cls) tys item
1093
1094 addDictsByClass :: DictMap Ct -> Class -> Bag Ct -> DictMap Ct
1095 addDictsByClass m cls items
1096 = addToUFM m cls (foldrBag add emptyTM items)
1097 where
1098 add ct@(CDictCan { cc_tyargs = tys }) tm = insertTM tys ct tm
1099 add ct _ = pprPanic "addDictsByClass" (ppr ct)
1100
1101 filterDicts :: (Ct -> Bool) -> DictMap Ct -> DictMap Ct
1102 filterDicts f m = filterTcAppMap f m
1103
1104 partitionDicts :: (Ct -> Bool) -> DictMap Ct -> (Bag Ct, DictMap Ct)
1105 partitionDicts f m = foldTcAppMap k m (emptyBag, emptyDicts)
1106 where
1107 k ct (yeses, noes) | f ct = (ct `consBag` yeses, noes)
1108 | otherwise = (yeses, add ct noes)
1109 add ct@(CDictCan { cc_class = cls, cc_tyargs = tys }) m
1110 = addDict m cls tys ct
1111 add ct _ = pprPanic "partitionDicts" (ppr ct)
1112
1113 dictsToBag :: DictMap a -> Bag a
1114 dictsToBag = tcAppMapToBag
1115
1116 foldDicts :: (a -> b -> b) -> DictMap a -> b -> b
1117 foldDicts = foldTcAppMap
1118
1119 emptyDicts :: DictMap a
1120 emptyDicts = emptyTcAppMap
1121
1122 ------------------------
1123 type FunEqMap a = TcAppMap a -- A map whose key is a (TyCon, [Type]) pair
1124
1125 emptyFunEqs :: TcAppMap a
1126 emptyFunEqs = emptyTcAppMap
1127
1128 sizeFunEqMap :: FunEqMap a -> Int
1129 sizeFunEqMap m = foldFunEqs (\ _ x -> x+1) m 0
1130
1131 findFunEq :: FunEqMap a -> TyCon -> [Type] -> Maybe a
1132 findFunEq m tc tys = findTcApp m (getUnique tc) tys
1133
1134 findFunEqs :: FunEqMap a -> TyCon -> [Type] -> Maybe a
1135 findFunEqs m tc tys = findTcApp m (getUnique tc) tys
1136
1137 funEqsToBag :: FunEqMap a -> Bag a
1138 funEqsToBag m = foldTcAppMap consBag m emptyBag
1139
1140 findFunEqsByTyCon :: FunEqMap a -> TyCon -> [a]
1141 -- Get inert function equation constraints that have the given tycon
1142 -- in their head. Not that the constraints remain in the inert set.
1143 -- We use this to check for derived interactions with built-in type-function
1144 -- constructors.
1145 findFunEqsByTyCon m tc
1146 | Just tm <- lookupUFM m tc = foldTM (:) tm []
1147 | otherwise = []
1148
1149 foldFunEqs :: (a -> b -> b) -> FunEqMap a -> b -> b
1150 foldFunEqs = foldTcAppMap
1151
1152 -- mapFunEqs :: (a -> b) -> FunEqMap a -> FunEqMap b
1153 -- mapFunEqs = mapTcApp
1154
1155 filterFunEqs :: (Ct -> Bool) -> FunEqMap Ct -> FunEqMap Ct
1156 filterFunEqs = filterTcAppMap
1157
1158 insertFunEq :: FunEqMap a -> TyCon -> [Type] -> a -> FunEqMap a
1159 insertFunEq m tc tys val = insertTcApp m (getUnique tc) tys val
1160
1161 -- insertFunEqCt :: FunEqMap Ct -> Ct -> FunEqMap Ct
1162 -- insertFunEqCt m ct@(CFunEqCan { cc_fun = tc, cc_tyargs = tys })
1163 -- = insertFunEq m tc tys ct
1164 -- insertFunEqCt _ ct = pprPanic "insertFunEqCt" (ppr ct)
1165
1166 partitionFunEqs :: (Ct -> Bool) -> FunEqMap Ct -> ([Ct], FunEqMap Ct)
1167 -- Optimise for the case where the predicate is false
1168 -- partitionFunEqs is called only from kick-out, and kick-out usually
1169 -- kicks out very few equalities, so we want to optimise for that case
1170 partitionFunEqs f m = (yeses, foldr del m yeses)
1171 where
1172 yeses = foldTcAppMap k m []
1173 k ct yeses | f ct = ct : yeses
1174 | otherwise = yeses
1175 del (CFunEqCan { cc_fun = tc, cc_tyargs = tys }) m
1176 = delFunEq m tc tys
1177 del ct _ = pprPanic "partitionFunEqs" (ppr ct)
1178
1179 delFunEq :: FunEqMap a -> TyCon -> [Type] -> FunEqMap a
1180 delFunEq m tc tys = delTcApp m (getUnique tc) tys
1181
1182 {-
1183 ************************************************************************
1184 * *
1185 * The TcS solver monad *
1186 * *
1187 ************************************************************************
1188
1189 Note [The TcS monad]
1190 ~~~~~~~~~~~~~~~~~~~~
1191 The TcS monad is a weak form of the main Tc monad
1192
1193 All you can do is
1194 * fail
1195 * allocate new variables
1196 * fill in evidence variables
1197
1198 Filling in a dictionary evidence variable means to create a binding
1199 for it, so TcS carries a mutable location where the binding can be
1200 added. This is initialised from the innermost implication constraint.
1201 -}
1202
1203 data TcSEnv
1204 = TcSEnv {
1205 tcs_ev_binds :: EvBindsVar,
1206
1207 tcs_unified :: IORef Bool,
1208 -- The "dirty-flag" Bool is set True when
1209 -- we unify a unification variable
1210
1211 tcs_count :: IORef Int, -- Global step count
1212
1213 tcs_inerts :: IORef InertSet, -- Current inert set
1214
1215 -- The main work-list and the flattening worklist
1216 -- See Note [Work list priorities] and
1217 -- Note [The flattening work list]
1218 tcs_worklist :: IORef WorkList, -- Current worklist
1219 tcs_flat_work :: IORef [Ct] -- Flattening worklist
1220 }
1221
1222 ---------------
1223 newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
1224
1225 instance Functor TcS where
1226 fmap f m = TcS $ fmap f . unTcS m
1227
1228 instance Applicative TcS where
1229 pure = return
1230 (<*>) = ap
1231
1232 instance Monad TcS where
1233 return x = TcS (\_ -> return x)
1234 fail err = TcS (\_ -> fail err)
1235 m >>= k = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
1236
1237 instance MonadUnique TcS where
1238 getUniqueSupplyM = wrapTcS getUniqueSupplyM
1239
1240 -- Basic functionality
1241 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1242 wrapTcS :: TcM a -> TcS a
1243 -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
1244 -- and TcS is supposed to have limited functionality
1245 wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
1246
1247 wrapErrTcS :: TcM a -> TcS a
1248 -- The thing wrapped should just fail
1249 -- There's no static check; it's up to the user
1250 -- Having a variant for each error message is too painful
1251 wrapErrTcS = wrapTcS
1252
1253 wrapWarnTcS :: TcM a -> TcS a
1254 -- The thing wrapped should just add a warning, or no-op
1255 -- There's no static check; it's up to the user
1256 wrapWarnTcS = wrapTcS
1257
1258 failTcS, panicTcS :: SDoc -> TcS a
1259 failTcS = wrapTcS . TcM.failWith
1260 panicTcS doc = pprPanic "TcCanonical" doc
1261
1262 traceTcS :: String -> SDoc -> TcS ()
1263 traceTcS herald doc = wrapTcS (TcM.traceTc herald doc)
1264
1265 runTcPluginTcS :: TcPluginM a -> TcS a
1266 runTcPluginTcS = wrapTcS . runTcPluginM
1267
1268 instance HasDynFlags TcS where
1269 getDynFlags = wrapTcS getDynFlags
1270
1271 getGlobalRdrEnvTcS :: TcS GlobalRdrEnv
1272 getGlobalRdrEnvTcS = wrapTcS TcM.getGlobalRdrEnv
1273
1274 bumpStepCountTcS :: TcS ()
1275 bumpStepCountTcS = TcS $ \env -> do { let ref = tcs_count env
1276 ; n <- TcM.readTcRef ref
1277 ; TcM.writeTcRef ref (n+1) }
1278
1279 csTraceTcS :: SDoc -> TcS ()
1280 csTraceTcS doc
1281 = wrapTcS $ csTraceTcM 1 (return doc)
1282
1283 traceFireTcS :: CtEvidence -> SDoc -> TcS ()
1284 -- Dump a rule-firing trace
1285 traceFireTcS ev doc
1286 = TcS $ \env -> csTraceTcM 1 $
1287 do { n <- TcM.readTcRef (tcs_count env)
1288 ; tclvl <- TcM.getTcLevel
1289 ; return (hang (int n <> brackets (ptext (sLit "U:") <> ppr tclvl
1290 <> ppr (ctLocDepth (ctEvLoc ev)))
1291 <+> doc <> colon)
1292 4 (ppr ev)) }
1293
1294 csTraceTcM :: Int -> TcM SDoc -> TcM ()
1295 -- Constraint-solver tracing, -ddump-cs-trace
1296 csTraceTcM trace_level mk_doc
1297 = do { dflags <- getDynFlags
1298 ; when ( (dopt Opt_D_dump_cs_trace dflags || dopt Opt_D_dump_tc_trace dflags)
1299 && trace_level <= traceLevel dflags ) $
1300 do { msg <- mk_doc
1301 ; TcM.traceTcRn Opt_D_dump_cs_trace msg } }
1302
1303 runTcS :: TcS a -- What to run
1304 -> TcM (a, Bag EvBind)
1305 runTcS tcs
1306 = do { ev_binds_var <- TcM.newTcEvBinds
1307 ; res <- runTcSWithEvBinds ev_binds_var tcs
1308 ; ev_binds <- TcM.getTcEvBinds ev_binds_var
1309 ; return (res, ev_binds) }
1310
1311 runTcSWithEvBinds :: EvBindsVar
1312 -> TcS a
1313 -> TcM a
1314 runTcSWithEvBinds ev_binds_var tcs
1315 = do { unified_var <- TcM.newTcRef False
1316 ; step_count <- TcM.newTcRef 0
1317 ; inert_var <- TcM.newTcRef is
1318 ; wl_var <- TcM.newTcRef emptyWorkList
1319 ; fw_var <- TcM.newTcRef (panic "Flat work list")
1320
1321 ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
1322 , tcs_unified = unified_var
1323 , tcs_count = step_count
1324 , tcs_inerts = inert_var
1325 , tcs_worklist = wl_var
1326 , tcs_flat_work = fw_var }
1327
1328 -- Run the computation
1329 ; res <- unTcS tcs env
1330
1331 ; count <- TcM.readTcRef step_count
1332 ; when (count > 0) $
1333 csTraceTcM 0 $ return (ptext (sLit "Constraint solver steps =") <+> int count)
1334
1335 #ifdef DEBUG
1336 ; ev_binds <- TcM.getTcEvBinds ev_binds_var
1337 ; checkForCyclicBinds ev_binds
1338 #endif
1339
1340 ; return res }
1341 where
1342 is = emptyInert
1343
1344 #ifdef DEBUG
1345 checkForCyclicBinds :: Bag EvBind -> TcM ()
1346 checkForCyclicBinds ev_binds
1347 | null cycles
1348 = return ()
1349 | null coercion_cycles
1350 = TcM.traceTc "Cycle in evidence binds" $ ppr cycles
1351 | otherwise
1352 = pprPanic "Cycle in coercion bindings" $ ppr coercion_cycles
1353 where
1354 cycles :: [[EvBind]]
1355 cycles = [c | CyclicSCC c <- stronglyConnCompFromEdgedVertices edges]
1356
1357 coercion_cycles = [c | c <- cycles, any is_co_bind c]
1358 is_co_bind (EvBind { eb_lhs = b }) = isEqVar b
1359
1360 edges :: [(EvBind, EvVar, [EvVar])]
1361 edges = [(bind, bndr, varSetElems (evVarsOfTerm rhs))
1362 | bind@(EvBind { eb_lhs = bndr, eb_rhs = rhs }) <- bagToList ev_binds]
1363 #endif
1364
1365 nestImplicTcS :: EvBindsVar -> TcLevel -> TcS a -> TcS a
1366 nestImplicTcS ref inner_tclvl (TcS thing_inside)
1367 = TcS $ \ TcSEnv { tcs_unified = unified_var
1368 , tcs_inerts = old_inert_var
1369 , tcs_count = count } ->
1370 do { inerts <- TcM.readTcRef old_inert_var
1371 ; let nest_inert = inerts { inert_flat_cache = emptyFunEqs }
1372 -- See Note [Do not inherit the flat cache]
1373 ; new_inert_var <- TcM.newTcRef nest_inert
1374 ; new_wl_var <- TcM.newTcRef emptyWorkList
1375 ; new_fw_var <- TcM.newTcRef (panic "Flat work list")
1376 ; let nest_env = TcSEnv { tcs_ev_binds = ref
1377 , tcs_unified = unified_var
1378 , tcs_count = count
1379 , tcs_inerts = new_inert_var
1380 , tcs_worklist = new_wl_var
1381 , tcs_flat_work = new_fw_var }
1382 ; res <- TcM.setTcLevel inner_tclvl $
1383 thing_inside nest_env
1384
1385 #ifdef DEBUG
1386 -- Perform a check that the thing_inside did not cause cycles
1387 ; ev_binds <- TcM.getTcEvBinds ref
1388 ; checkForCyclicBinds ev_binds
1389 #endif
1390
1391 ; return res }
1392
1393 recoverTcS :: TcS a -> TcS a -> TcS a
1394 recoverTcS (TcS recovery_code) (TcS thing_inside)
1395 = TcS $ \ env ->
1396 TcM.recoverM (recovery_code env) (thing_inside env)
1397
1398 nestTcS :: TcS a -> TcS a
1399 -- Use the current untouchables, augmenting the current
1400 -- evidence bindings, and solved dictionaries
1401 -- But have no effect on the InertCans, or on the inert_flat_cache
1402 -- (the latter because the thing inside a nestTcS does unflattening)
1403 nestTcS (TcS thing_inside)
1404 = TcS $ \ env@(TcSEnv { tcs_inerts = inerts_var }) ->
1405 do { inerts <- TcM.readTcRef inerts_var
1406 ; new_inert_var <- TcM.newTcRef inerts
1407 ; new_wl_var <- TcM.newTcRef emptyWorkList
1408 ; let nest_env = env { tcs_inerts = new_inert_var
1409 , tcs_worklist = new_wl_var }
1410
1411 ; res <- thing_inside nest_env
1412
1413 ; new_inerts <- TcM.readTcRef new_inert_var
1414 ; TcM.writeTcRef inerts_var -- See Note [Propagate the solved dictionaries]
1415 (inerts { inert_solved_dicts = inert_solved_dicts new_inerts })
1416
1417 ; return res }
1418
1419 tryTcS :: TcS a -> TcS a
1420 -- Like runTcS, but from within the TcS monad
1421 -- Completely fresh inerts and worklist, be careful!
1422 -- Moreover, we will simply throw away all the evidence generated.
1423 tryTcS (TcS thing_inside)
1424 = TcS $ \env ->
1425 do { is_var <- TcM.newTcRef emptyInert
1426 ; unified_var <- TcM.newTcRef False
1427 ; ev_binds_var <- TcM.newTcEvBinds
1428 ; wl_var <- TcM.newTcRef emptyWorkList
1429 ; let nest_env = env { tcs_ev_binds = ev_binds_var
1430 , tcs_unified = unified_var
1431 , tcs_inerts = is_var
1432 , tcs_worklist = wl_var }
1433 ; thing_inside nest_env }
1434
1435 {-
1436 Note [Propagate the solved dictionaries]
1437 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1438 It's really quite important that nestTcS does not discard the solved
1439 dictionaries from the thing_inside.
1440 Consider
1441 Eq [a]
1442 forall b. empty => Eq [a]
1443 We solve the simple (Eq [a]), under nestTcS, and then turn our attention to
1444 the implications. It's definitely fine to use the solved dictionaries on
1445 the inner implications, and it can make a signficant performance difference
1446 if you do so.
1447 -}
1448
1449 -- Getters and setters of TcEnv fields
1450 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1451
1452 -- Getter of inerts and worklist
1453 getTcSInertsRef :: TcS (IORef InertSet)
1454 getTcSInertsRef = TcS (return . tcs_inerts)
1455
1456 getTcSWorkListRef :: TcS (IORef WorkList)
1457 getTcSWorkListRef = TcS (return . tcs_worklist)
1458
1459 getTcSInerts :: TcS InertSet
1460 getTcSInerts = getTcSInertsRef >>= wrapTcS . (TcM.readTcRef)
1461
1462 setTcSInerts :: InertSet -> TcS ()
1463 setTcSInerts ics = do { r <- getTcSInertsRef; wrapTcS (TcM.writeTcRef r ics) }
1464
1465 getWorkListImplics :: TcS (Bag Implication)
1466 getWorkListImplics
1467 = do { wl_var <- getTcSWorkListRef
1468 ; wl_curr <- wrapTcS (TcM.readTcRef wl_var)
1469 ; return (wl_implics wl_curr) }
1470
1471 updWorkListTcS :: (WorkList -> WorkList) -> TcS ()
1472 updWorkListTcS f
1473 = do { wl_var <- getTcSWorkListRef
1474 ; wl_curr <- wrapTcS (TcM.readTcRef wl_var)
1475 ; let new_work = f wl_curr
1476 ; wrapTcS (TcM.writeTcRef wl_var new_work) }
1477
1478 updWorkListTcS_return :: (WorkList -> (a,WorkList)) -> TcS a
1479 -- Process the work list, returning a depleted work list,
1480 -- plus a value extracted from it (typically a work item removed from it)
1481 updWorkListTcS_return f
1482 = do { wl_var <- getTcSWorkListRef
1483 ; wl_curr <- wrapTcS (TcM.readTcRef wl_var)
1484 ; traceTcS "updWorkList" (ppr wl_curr)
1485 ; let (res,new_work) = f wl_curr
1486 ; wrapTcS (TcM.writeTcRef wl_var new_work)
1487 ; return res }
1488
1489 emitWorkNC :: [CtEvidence] -> TcS ()
1490 emitWorkNC evs
1491 | null evs
1492 = return ()
1493 | otherwise
1494 = do { traceTcS "Emitting fresh work" (vcat (map ppr evs))
1495 ; updWorkListTcS (extendWorkListCts (map mkNonCanonical evs)) }
1496
1497 emitInsoluble :: Ct -> TcS ()
1498 -- Emits a non-canonical constraint that will stand for a frozen error in the inerts.
1499 emitInsoluble ct
1500 = do { traceTcS "Emit insoluble" (ppr ct)
1501 ; updInertTcS add_insol }
1502 where
1503 this_pred = ctPred ct
1504 add_insol is@(IS { inert_cans = ics@(IC { inert_insols = old_insols }) })
1505 | already_there = is
1506 | otherwise = is { inert_cans = ics { inert_insols = old_insols `snocCts` ct } }
1507 where
1508 already_there = not (isWantedCt ct) && anyBag (tcEqType this_pred . ctPred) old_insols
1509 -- See Note [Do not add duplicate derived insolubles]
1510
1511 newTcRef :: a -> TcS (TcRef a)
1512 newTcRef x = wrapTcS (TcM.newTcRef x)
1513
1514 readTcRef :: TcRef a -> TcS a
1515 readTcRef ref = wrapTcS (TcM.readTcRef ref)
1516
1517 updTcRef :: TcRef a -> (a->a) -> TcS ()
1518 updTcRef ref upd_fn = wrapTcS (TcM.updTcRef ref upd_fn)
1519
1520 getTcEvBinds :: TcS EvBindsVar
1521 getTcEvBinds = TcS (return . tcs_ev_binds)
1522
1523 getTcLevel :: TcS TcLevel
1524 getTcLevel = wrapTcS TcM.getTcLevel
1525
1526 getTcEvBindsMap :: TcS EvBindMap
1527 getTcEvBindsMap
1528 = do { EvBindsVar ev_ref _ <- getTcEvBinds
1529 ; wrapTcS $ TcM.readTcRef ev_ref }
1530
1531 setWantedTyBind :: TcTyVar -> TcType -> TcS ()
1532 -- Add a type binding
1533 -- We never do this twice!
1534 setWantedTyBind tv ty
1535 | ASSERT2( isMetaTyVar tv, ppr tv )
1536 isFmvTyVar tv
1537 = ASSERT2( isMetaTyVar tv, ppr tv )
1538 wrapTcS (TcM.writeMetaTyVar tv ty)
1539 -- Write directly into the mutable tyvar
1540 -- Flatten meta-vars are born and die locally
1541
1542 | otherwise
1543 = TcS $ \ env ->
1544 do { TcM.traceTc "setWantedTyBind" (ppr tv <+> text ":=" <+> ppr ty)
1545 ; TcM.writeMetaTyVar tv ty
1546 ; TcM.writeTcRef (tcs_unified env) True }
1547
1548 reportUnifications :: TcS a -> TcS (Bool, a)
1549 reportUnifications (TcS thing_inside)
1550 = TcS $ \ env ->
1551 do { inner_unified <- TcM.newTcRef False
1552 ; res <- thing_inside (env { tcs_unified = inner_unified })
1553 ; dirty <- TcM.readTcRef inner_unified
1554 ; return (dirty, res) }
1555
1556 getDefaultInfo :: TcS ([Type], (Bool, Bool))
1557 getDefaultInfo = wrapTcS TcM.tcGetDefaultTys
1558
1559 -- Just get some environments needed for instance looking up and matching
1560 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1561
1562 getInstEnvs :: TcS InstEnvs
1563 getInstEnvs = wrapTcS $ TcM.tcGetInstEnvs
1564
1565 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
1566 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
1567
1568 getTopEnv :: TcS HscEnv
1569 getTopEnv = wrapTcS $ TcM.getTopEnv
1570
1571 getGblEnv :: TcS TcGblEnv
1572 getGblEnv = wrapTcS $ TcM.getGblEnv
1573
1574 -- Setting names as used (used in the deriving of Coercible evidence)
1575 -- Too hackish to expose it to TcS? In that case somehow extract the used
1576 -- constructors from the result of solveInteract
1577 addUsedRdrNamesTcS :: [RdrName] -> TcS ()
1578 addUsedRdrNamesTcS names = wrapTcS $ addUsedRdrNames names
1579
1580 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
1581 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1582
1583 checkWellStagedDFun :: PredType -> DFunId -> CtLoc -> TcS ()
1584 checkWellStagedDFun pred dfun_id loc
1585 = wrapTcS $ TcM.setCtLoc loc $
1586 do { use_stage <- TcM.getStage
1587 ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
1588 where
1589 pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
1590 bind_lvl = TcM.topIdLvl dfun_id
1591
1592 pprEq :: TcType -> TcType -> SDoc
1593 pprEq ty1 ty2 = pprParendType ty1 <+> char '~' <+> pprParendType ty2
1594
1595 isTouchableMetaTyVarTcS :: TcTyVar -> TcS Bool
1596 isTouchableMetaTyVarTcS tv
1597 = do { tclvl <- getTcLevel
1598 ; return $ isTouchableMetaTyVar tclvl tv }
1599
1600 isFilledMetaTyVar_maybe :: TcTyVar -> TcS (Maybe Type)
1601 isFilledMetaTyVar_maybe tv
1602 = ASSERT2( isTcTyVar tv, ppr tv )
1603 case tcTyVarDetails tv of
1604 MetaTv { mtv_ref = ref }
1605 -> do { cts <- wrapTcS (TcM.readTcRef ref)
1606 ; case cts of
1607 Indirect ty -> return (Just ty)
1608 Flexi -> return Nothing }
1609 _ -> return Nothing
1610
1611 isFilledMetaTyVar :: TcTyVar -> TcS Bool
1612 isFilledMetaTyVar tv = wrapTcS (TcM.isFilledMetaTyVar tv)
1613
1614 zonkTyVarsAndFV :: TcTyVarSet -> TcS TcTyVarSet
1615 zonkTyVarsAndFV tvs = wrapTcS (TcM.zonkTyVarsAndFV tvs)
1616
1617 zonkTcType :: TcType -> TcS TcType
1618 zonkTcType ty = wrapTcS (TcM.zonkTcType ty)
1619
1620 zonkTcTyVar :: TcTyVar -> TcS TcType
1621 zonkTcTyVar tv = wrapTcS (TcM.zonkTcTyVar tv)
1622
1623 zonkSimples :: Cts -> TcS Cts
1624 zonkSimples cts = wrapTcS (TcM.zonkSimples cts)
1625
1626 {-
1627 Note [Do not add duplicate derived insolubles]
1628 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1629 In general we *must* add an insoluble (Int ~ Bool) even if there is
1630 one such there already, because they may come from distinct call
1631 sites. Not only do we want an error message for each, but with
1632 -fdefer-type-errors we must generate evidence for each. But for
1633 *derived* insolubles, we only want to report each one once. Why?
1634
1635 (a) A constraint (C r s t) where r -> s, say, may generate the same fundep
1636 equality many times, as the original constraint is sucessively rewritten.
1637
1638 (b) Ditto the successive iterations of the main solver itself, as it traverses
1639 the constraint tree. See example below.
1640
1641 Also for *given* insolubles we may get repeated errors, as we
1642 repeatedly traverse the constraint tree. These are relatively rare
1643 anyway, so removing duplicates seems ok. (Alternatively we could take
1644 the SrcLoc into account.)
1645
1646 Note that the test does not need to be particularly efficient because
1647 it is only used if the program has a type error anyway.
1648
1649 Example of (b): assume a top-level class and instance declaration:
1650
1651 class D a b | a -> b
1652 instance D [a] [a]
1653
1654 Assume we have started with an implication:
1655
1656 forall c. Eq c => { wc_simple = D [c] c [W] }
1657
1658 which we have simplified to:
1659
1660 forall c. Eq c => { wc_simple = D [c] c [W]
1661 , wc_insols = (c ~ [c]) [D] }
1662
1663 For some reason, e.g. because we floated an equality somewhere else,
1664 we might try to re-solve this implication. If we do not do a
1665 dropDerivedWC, then we will end up trying to solve the following
1666 constraints the second time:
1667
1668 (D [c] c) [W]
1669 (c ~ [c]) [D]
1670
1671 which will result in two Deriveds to end up in the insoluble set:
1672
1673 wc_simple = D [c] c [W]
1674 wc_insols = (c ~ [c]) [D], (c ~ [c]) [D]
1675 -}
1676
1677 -- Flatten skolems
1678 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1679 newFlattenSkolem :: CtFlavour -> CtLoc
1680 -> TcType -- F xis
1681 -> TcS (CtEvidence, TcTyVar) -- [W] x:: F xis ~ fsk
1682 newFlattenSkolem Given loc fam_ty
1683 = do { fsk <- wrapTcS $
1684 do { uniq <- TcM.newUnique
1685 ; let name = TcM.mkTcTyVarName uniq (fsLit "fsk")
1686 ; return (mkTcTyVar name (typeKind fam_ty) (FlatSkol fam_ty)) }
1687 ; let ev = CtGiven { ctev_pred = mkTcEqPred fam_ty (mkTyVarTy fsk)
1688 , ctev_evtm = EvCoercion (mkTcNomReflCo fam_ty)
1689 , ctev_loc = loc }
1690 ; return (ev, fsk) }
1691
1692 newFlattenSkolem _ loc fam_ty -- Make a wanted
1693 = do { fuv <- wrapTcS $
1694 do { uniq <- TcM.newUnique
1695 ; ref <- TcM.newMutVar Flexi
1696 ; let details = MetaTv { mtv_info = FlatMetaTv
1697 , mtv_ref = ref
1698 , mtv_tclvl = fskTcLevel }
1699 name = TcM.mkTcTyVarName uniq (fsLit "s")
1700 ; return (mkTcTyVar name (typeKind fam_ty) details) }
1701 ; ev <- newWantedEvVarNC loc (mkTcEqPred fam_ty (mkTyVarTy fuv))
1702 ; return (ev, fuv) }
1703
1704 extendFlatCache :: TyCon -> [Type] -> (TcCoercion, TcType, CtFlavour) -> TcS ()
1705 extendFlatCache tc xi_args stuff
1706 = do { dflags <- getDynFlags
1707 ; when (gopt Opt_FlatCache dflags) $
1708 updInertTcS $ \ is@(IS { inert_flat_cache = fc }) ->
1709 is { inert_flat_cache = insertFunEq fc tc xi_args stuff } }
1710
1711 -- Instantiations
1712 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1713
1714 instDFunType :: DFunId -> [DFunInstType] -> TcS ([TcType], TcThetaType)
1715 instDFunType dfun_id inst_tys
1716 = wrapTcS $ TcM.instDFunType dfun_id inst_tys
1717
1718 newFlexiTcSTy :: Kind -> TcS TcType
1719 newFlexiTcSTy knd = wrapTcS (TcM.newFlexiTyVarTy knd)
1720
1721 cloneMetaTyVar :: TcTyVar -> TcS TcTyVar
1722 cloneMetaTyVar tv = wrapTcS (TcM.cloneMetaTyVar tv)
1723
1724 demoteUnfilledFmv :: TcTyVar -> TcS ()
1725 -- If a flatten-meta-var is still un-filled,
1726 -- turn it into an ordinary meta-var
1727 demoteUnfilledFmv fmv
1728 = wrapTcS $ do { is_filled <- TcM.isFilledMetaTyVar fmv
1729 ; unless is_filled $
1730 do { tv_ty <- TcM.newFlexiTyVarTy (tyVarKind fmv)
1731 ; TcM.writeMetaTyVar fmv tv_ty } }
1732
1733 instFlexiTcS :: [TKVar] -> TcS (TvSubst, [TcType])
1734 instFlexiTcS tvs = wrapTcS (mapAccumLM inst_one emptyTvSubst tvs)
1735 where
1736 inst_one subst tv
1737 = do { ty' <- instFlexiTcSHelper (tyVarName tv)
1738 (substTy subst (tyVarKind tv))
1739 ; return (extendTvSubst subst tv ty', ty') }
1740
1741 instFlexiTcSHelper :: Name -> Kind -> TcM TcType
1742 instFlexiTcSHelper tvname kind
1743 = do { uniq <- TcM.newUnique
1744 ; details <- TcM.newMetaDetails (TauTv False)
1745 ; let name = setNameUnique tvname uniq
1746 ; return (mkTyVarTy (mkTcTyVar name kind details)) }
1747
1748 instFlexiTcSHelperTcS :: Name -> Kind -> TcS TcType
1749 instFlexiTcSHelperTcS n k = wrapTcS (instFlexiTcSHelper n k)
1750
1751
1752 -- Creating and setting evidence variables and CtFlavors
1753 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1754
1755 data Freshness = Fresh | Cached
1756
1757 isFresh :: Freshness -> Bool
1758 isFresh Fresh = True
1759 isFresh Cached = False
1760
1761 freshGoals :: [(CtEvidence, Freshness)] -> [CtEvidence]
1762 freshGoals mns = [ ctev | (ctev, Fresh) <- mns ]
1763
1764 setEvBind :: EvBind -> TcS ()
1765 setEvBind ev_bind
1766 = do { tc_evbinds <- getTcEvBinds
1767 ; wrapTcS $ TcM.addTcEvBind tc_evbinds ev_bind }
1768
1769 setWantedEvBind :: EvVar -> EvTerm -> TcS ()
1770 setWantedEvBind ev_id tm = setEvBind (mkWantedEvBind ev_id tm)
1771
1772 setEvBindIfWanted :: CtEvidence -> EvTerm -> TcS ()
1773 setEvBindIfWanted ev tm
1774 = case ev of
1775 CtWanted { ctev_evar = ev_id } -> setWantedEvBind ev_id tm
1776 _ -> return ()
1777
1778 newTcEvBinds :: TcS EvBindsVar
1779 newTcEvBinds = wrapTcS TcM.newTcEvBinds
1780
1781 newEvVar :: TcPredType -> TcS EvVar
1782 newEvVar pred = wrapTcS (TcM.newEvVar pred)
1783
1784 newGivenEvVar :: CtLoc -> (TcPredType, EvTerm) -> TcS CtEvidence
1785 -- Make a new variable of the given PredType,
1786 -- immediately bind it to the given term
1787 -- and return its CtEvidence
1788 -- Precondition: this is not a kind equality
1789 -- See Note [Do not create Given kind equalities]
1790 newGivenEvVar loc (pred, rhs)
1791 = ASSERT2( not (isKindEquality pred), ppr pred $$ pprCtOrigin (ctLocOrigin loc) )
1792 do { new_ev <- newEvVar pred
1793 ; setEvBind (mkGivenEvBind new_ev rhs)
1794 ; return (CtGiven { ctev_pred = pred, ctev_evtm = EvId new_ev, ctev_loc = loc }) }
1795
1796 newGivenEvVars :: CtLoc -> [(TcPredType, EvTerm)] -> TcS [CtEvidence]
1797 -- Like newGivenEvVar, but automatically discard kind equalities
1798 -- See Note [Do not create Given kind equalities]
1799 newGivenEvVars loc pts = mapM (newGivenEvVar loc) (filterOut (isKindEquality . fst) pts)
1800
1801 isKindEquality :: TcPredType -> Bool
1802 -- See Note [Do not create Given kind equalities]
1803 isKindEquality pred = case classifyPredType pred of
1804 EqPred _ t1 _ -> isKind t1
1805 _ -> False
1806
1807 {- Note [Do not create Given kind equalities]
1808 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1809 We do not want to create a Given kind equality like
1810
1811 [G] kv ~ k -- kv is a skolem kind variable
1812 -- Reason we don't yet support non-Refl kind equalities
1813
1814 This showed up in Trac #8566, where we had a data type
1815 data I (u :: U *) (r :: [*]) :: * where
1816 A :: I (AA t as) r -- Existential k
1817 so A has type
1818 A :: forall (u:U *) (r:[*]) Universal
1819 (k:BOX) (t:k) (as:[U *]). Existential
1820 (u ~ AA * k t as) => I u r
1821
1822 There is no direct kind equality, but in a pattern match where 'u' is
1823 instantiated to, say, (AA * kk (t1:kk) as1), we'd decompose to get
1824 k ~ kk, t ~ t1, as ~ as1
1825 This is bad. We "fix" this by simply ignoring the Given kind equality
1826 But the Right Thing is to add kind equalities!
1827
1828 But note (Trac #8705) that we *do* create Given (non-canonical) equalities
1829 with un-equal kinds, e.g.
1830 [G] t1::k1 ~ t2::k2 -- k1 and k2 are un-equal kinds
1831 Reason: k1 or k2 might be unification variables that have already been
1832 unified (at this point we have not canonicalised the types), so we want
1833 to emit this t1~t2 as a (non-canonical) Given in the work-list. If k1/k2
1834 have been unified, we'll find that when we canonicalise it, and the
1835 t1~t2 information may be crucial (Trac #8705 is an example).
1836
1837 If it turns out that k1 and k2 are really un-equal, then it'll end up
1838 as an Irreducible (see Note [Equalities with incompatible kinds] in
1839 TcCanonical), and will do no harm.
1840 -}
1841
1842 newWantedEvVarNC :: CtLoc -> TcPredType -> TcS CtEvidence
1843 -- Don't look up in the solved/inerts; we know it's not there
1844 newWantedEvVarNC loc pty
1845 = do { new_ev <- newEvVar pty
1846 ; return (CtWanted { ctev_pred = pty, ctev_evar = new_ev, ctev_loc = loc })}
1847
1848 newWantedEvVar :: CtLoc -> TcPredType -> TcS (CtEvidence, Freshness)
1849 -- For anything except ClassPred, this is the same as newWantedEvVarNC
1850 newWantedEvVar loc pty
1851 = do { mb_ct <- lookupInInerts loc pty
1852 ; case mb_ct of
1853 Just ctev | not (isDerived ctev)
1854 -> do { traceTcS "newWantedEvVar/cache hit" $ ppr ctev
1855 ; return (ctev, Cached) }
1856 _ -> do { ctev <- newWantedEvVarNC loc pty
1857 ; traceTcS "newWantedEvVar/cache miss" $ ppr ctev
1858 ; return (ctev, Fresh) } }
1859
1860 emitNewDerived :: CtLoc -> TcPredType -> TcS ()
1861 -- Create new Derived and put it in the work list
1862 emitNewDerived loc pred
1863 = do { mb_ev <- newDerived loc pred
1864 ; case mb_ev of
1865 Nothing -> return ()
1866 Just ev -> do { traceTcS "Emitting [D]" (ppr ev)
1867 ; updWorkListTcS (extendWorkListCt (mkNonCanonical ev)) } }
1868
1869 newDerived :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence)
1870 -- Returns Nothing if cached,
1871 -- Just pred if not cached
1872 newDerived loc pred
1873 = do { mb_ct <- lookupInInerts loc pred
1874 ; return (case mb_ct of
1875 Just {} -> Nothing
1876 Nothing -> Just (CtDerived { ctev_pred = pred, ctev_loc = loc })) }
1877
1878
1879 matchFam :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcType))
1880 matchFam tycon args = wrapTcS $ matchFamTcM tycon args
1881
1882 matchFamTcM :: TyCon -> [Type] -> TcM (Maybe (TcCoercion, TcType))
1883 -- Given (F tys) return (ty, co), where co :: F tys ~ ty
1884 matchFamTcM tycon args
1885 = do { fam_envs <- FamInst.tcGetFamInstEnvs
1886 ; return $ fmap (first TcCoercion) $
1887 reduceTyFamApp_maybe fam_envs Nominal tycon args }
1888
1889 {-
1890 Note [Residual implications]
1891 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1892 The wl_implics in the WorkList are the residual implication
1893 constraints that are generated while solving or canonicalising the
1894 current worklist. Specifically, when canonicalising
1895 (forall a. t1 ~ forall a. t2)
1896 from which we get the implication
1897 (forall a. t1 ~ t2)
1898 See TcSMonad.deferTcSForAllEq
1899 -}
1900
1901 -- Deferring forall equalities as implications
1902 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1903
1904 deferTcSForAllEq :: Role -- Nominal or Representational
1905 -> CtLoc -- Original wanted equality flavor
1906 -> ([TyVar],TcType) -- ForAll tvs1 body1
1907 -> ([TyVar],TcType) -- ForAll tvs2 body2
1908 -> TcS EvTerm
1909 -- Some of this functionality is repeated from TcUnify,
1910 -- consider having a single place where we create fresh implications.
1911 deferTcSForAllEq role loc (tvs1,body1) (tvs2,body2)
1912 = do { (subst1, skol_tvs) <- wrapTcS $ TcM.tcInstSkolTyVars tvs1
1913 ; let tys = mkTyVarTys skol_tvs
1914 phi1 = Type.substTy subst1 body1
1915 phi2 = Type.substTy (zipTopTvSubst tvs2 tys) body2
1916 skol_info = UnifyForAllSkol skol_tvs phi1
1917 eq_pred = case role of
1918 Nominal -> mkTcEqPred phi1 phi2
1919 Representational -> mkCoerciblePred phi1 phi2
1920 Phantom -> panic "deferTcSForAllEq Phantom"
1921 ; (ctev, freshness) <- newWantedEvVar loc eq_pred
1922 ; coe_inside <- case freshness of
1923 Cached -> return (ctEvCoercion ctev)
1924 Fresh -> do { ev_binds_var <- newTcEvBinds
1925 ; env <- wrapTcS $ TcM.getLclEnv
1926 ; let ev_binds = TcEvBinds ev_binds_var
1927 new_ct = mkNonCanonical ctev
1928 new_co = ctEvCoercion ctev
1929 new_tclvl = pushTcLevel (tcl_tclvl env)
1930 ; let wc = WC { wc_simple = singleCt new_ct
1931 , wc_impl = emptyBag
1932 , wc_insol = emptyCts }
1933 imp = Implic { ic_tclvl = new_tclvl
1934 , ic_skols = skol_tvs
1935 , ic_no_eqs = True
1936 , ic_given = []
1937 , ic_wanted = wc
1938 , ic_status = IC_Unsolved
1939 , ic_binds = ev_binds_var
1940 , ic_env = env
1941 , ic_info = skol_info }
1942 ; updWorkListTcS (extendWorkListImplic imp)
1943 ; return (TcLetCo ev_binds new_co) }
1944
1945 ; return $ EvCoercion (foldr mkTcForAllCo coe_inside skol_tvs) }
1946