d7c58d502affa8a66a007b0490ac2dfd5849a04b
[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,
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 b _) = isEqVar b
1359
1360 edges :: [(EvBind, EvVar, [EvVar])]
1361 edges = [(bind, bndr, varSetElems (evVarsOfTerm rhs)) | bind@(EvBind bndr rhs) <- bagToList ev_binds]
1362 #endif
1363
1364 nestImplicTcS :: EvBindsVar -> TcLevel -> TcS a -> TcS a
1365 nestImplicTcS ref inner_tclvl (TcS thing_inside)
1366 = TcS $ \ TcSEnv { tcs_unified = unified_var
1367 , tcs_inerts = old_inert_var
1368 , tcs_count = count } ->
1369 do { inerts <- TcM.readTcRef old_inert_var
1370 ; let nest_inert = inerts { inert_flat_cache = emptyFunEqs }
1371 -- See Note [Do not inherit the flat cache]
1372 ; new_inert_var <- TcM.newTcRef nest_inert
1373 ; new_wl_var <- TcM.newTcRef emptyWorkList
1374 ; new_fw_var <- TcM.newTcRef (panic "Flat work list")
1375 ; let nest_env = TcSEnv { tcs_ev_binds = ref
1376 , tcs_unified = unified_var
1377 , tcs_count = count
1378 , tcs_inerts = new_inert_var
1379 , tcs_worklist = new_wl_var
1380 , tcs_flat_work = new_fw_var }
1381 ; res <- TcM.setTcLevel inner_tclvl $
1382 thing_inside nest_env
1383
1384 #ifdef DEBUG
1385 -- Perform a check that the thing_inside did not cause cycles
1386 ; ev_binds <- TcM.getTcEvBinds ref
1387 ; checkForCyclicBinds ev_binds
1388 #endif
1389
1390 ; return res }
1391
1392 recoverTcS :: TcS a -> TcS a -> TcS a
1393 recoverTcS (TcS recovery_code) (TcS thing_inside)
1394 = TcS $ \ env ->
1395 TcM.recoverM (recovery_code env) (thing_inside env)
1396
1397 nestTcS :: TcS a -> TcS a
1398 -- Use the current untouchables, augmenting the current
1399 -- evidence bindings, and solved dictionaries
1400 -- But have no effect on the InertCans, or on the inert_flat_cache
1401 -- (the latter because the thing inside a nestTcS does unflattening)
1402 nestTcS (TcS thing_inside)
1403 = TcS $ \ env@(TcSEnv { tcs_inerts = inerts_var }) ->
1404 do { inerts <- TcM.readTcRef inerts_var
1405 ; new_inert_var <- TcM.newTcRef inerts
1406 ; new_wl_var <- TcM.newTcRef emptyWorkList
1407 ; let nest_env = env { tcs_inerts = new_inert_var
1408 , tcs_worklist = new_wl_var }
1409
1410 ; res <- thing_inside nest_env
1411
1412 ; new_inerts <- TcM.readTcRef new_inert_var
1413 ; TcM.writeTcRef inerts_var -- See Note [Propagate the solved dictionaries]
1414 (inerts { inert_solved_dicts = inert_solved_dicts new_inerts })
1415
1416 ; return res }
1417
1418 tryTcS :: TcS a -> TcS a
1419 -- Like runTcS, but from within the TcS monad
1420 -- Completely fresh inerts and worklist, be careful!
1421 -- Moreover, we will simply throw away all the evidence generated.
1422 tryTcS (TcS thing_inside)
1423 = TcS $ \env ->
1424 do { is_var <- TcM.newTcRef emptyInert
1425 ; unified_var <- TcM.newTcRef False
1426 ; ev_binds_var <- TcM.newTcEvBinds
1427 ; wl_var <- TcM.newTcRef emptyWorkList
1428 ; let nest_env = env { tcs_ev_binds = ev_binds_var
1429 , tcs_unified = unified_var
1430 , tcs_inerts = is_var
1431 , tcs_worklist = wl_var }
1432 ; thing_inside nest_env }
1433
1434 {-
1435 Note [Propagate the solved dictionaries]
1436 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1437 It's really quite important that nestTcS does not discard the solved
1438 dictionaries from the thing_inside.
1439 Consider
1440 Eq [a]
1441 forall b. empty => Eq [a]
1442 We solve the simple (Eq [a]), under nestTcS, and then turn our attention to
1443 the implications. It's definitely fine to use the solved dictionaries on
1444 the inner implications, and it can make a signficant performance difference
1445 if you do so.
1446 -}
1447
1448 -- Getters and setters of TcEnv fields
1449 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1450
1451 -- Getter of inerts and worklist
1452 getTcSInertsRef :: TcS (IORef InertSet)
1453 getTcSInertsRef = TcS (return . tcs_inerts)
1454
1455 getTcSWorkListRef :: TcS (IORef WorkList)
1456 getTcSWorkListRef = TcS (return . tcs_worklist)
1457
1458 getTcSInerts :: TcS InertSet
1459 getTcSInerts = getTcSInertsRef >>= wrapTcS . (TcM.readTcRef)
1460
1461 setTcSInerts :: InertSet -> TcS ()
1462 setTcSInerts ics = do { r <- getTcSInertsRef; wrapTcS (TcM.writeTcRef r ics) }
1463
1464 getWorkListImplics :: TcS (Bag Implication)
1465 getWorkListImplics
1466 = do { wl_var <- getTcSWorkListRef
1467 ; wl_curr <- wrapTcS (TcM.readTcRef wl_var)
1468 ; return (wl_implics wl_curr) }
1469
1470 updWorkListTcS :: (WorkList -> WorkList) -> TcS ()
1471 updWorkListTcS f
1472 = do { wl_var <- getTcSWorkListRef
1473 ; wl_curr <- wrapTcS (TcM.readTcRef wl_var)
1474 ; let new_work = f wl_curr
1475 ; wrapTcS (TcM.writeTcRef wl_var new_work) }
1476
1477 updWorkListTcS_return :: (WorkList -> (a,WorkList)) -> TcS a
1478 -- Process the work list, returning a depleted work list,
1479 -- plus a value extracted from it (typically a work item removed from it)
1480 updWorkListTcS_return f
1481 = do { wl_var <- getTcSWorkListRef
1482 ; wl_curr <- wrapTcS (TcM.readTcRef wl_var)
1483 ; traceTcS "updWorkList" (ppr wl_curr)
1484 ; let (res,new_work) = f wl_curr
1485 ; wrapTcS (TcM.writeTcRef wl_var new_work)
1486 ; return res }
1487
1488 emitWorkNC :: [CtEvidence] -> TcS ()
1489 emitWorkNC evs
1490 | null evs
1491 = return ()
1492 | otherwise
1493 = do { traceTcS "Emitting fresh work" (vcat (map ppr evs))
1494 ; updWorkListTcS (extendWorkListCts (map mkNonCanonical evs)) }
1495
1496 emitInsoluble :: Ct -> TcS ()
1497 -- Emits a non-canonical constraint that will stand for a frozen error in the inerts.
1498 emitInsoluble ct
1499 = do { traceTcS "Emit insoluble" (ppr ct)
1500 ; updInertTcS add_insol }
1501 where
1502 this_pred = ctPred ct
1503 add_insol is@(IS { inert_cans = ics@(IC { inert_insols = old_insols }) })
1504 | already_there = is
1505 | otherwise = is { inert_cans = ics { inert_insols = old_insols `snocCts` ct } }
1506 where
1507 already_there = not (isWantedCt ct) && anyBag (tcEqType this_pred . ctPred) old_insols
1508 -- See Note [Do not add duplicate derived insolubles]
1509
1510 newTcRef :: a -> TcS (TcRef a)
1511 newTcRef x = wrapTcS (TcM.newTcRef x)
1512
1513 readTcRef :: TcRef a -> TcS a
1514 readTcRef ref = wrapTcS (TcM.readTcRef ref)
1515
1516 updTcRef :: TcRef a -> (a->a) -> TcS ()
1517 updTcRef ref upd_fn = wrapTcS (TcM.updTcRef ref upd_fn)
1518
1519 getTcEvBinds :: TcS EvBindsVar
1520 getTcEvBinds = TcS (return . tcs_ev_binds)
1521
1522 getTcLevel :: TcS TcLevel
1523 getTcLevel = wrapTcS TcM.getTcLevel
1524
1525 getTcEvBindsMap :: TcS EvBindMap
1526 getTcEvBindsMap
1527 = do { EvBindsVar ev_ref _ <- getTcEvBinds
1528 ; wrapTcS $ TcM.readTcRef ev_ref }
1529
1530 setWantedTyBind :: TcTyVar -> TcType -> TcS ()
1531 -- Add a type binding
1532 -- We never do this twice!
1533 setWantedTyBind tv ty
1534 | ASSERT2( isMetaTyVar tv, ppr tv )
1535 isFmvTyVar tv
1536 = ASSERT2( isMetaTyVar tv, ppr tv )
1537 wrapTcS (TcM.writeMetaTyVar tv ty)
1538 -- Write directly into the mutable tyvar
1539 -- Flatten meta-vars are born and die locally
1540
1541 | otherwise
1542 = TcS $ \ env ->
1543 do { TcM.traceTc "setWantedTyBind" (ppr tv <+> text ":=" <+> ppr ty)
1544 ; TcM.writeMetaTyVar tv ty
1545 ; TcM.writeTcRef (tcs_unified env) True }
1546
1547 reportUnifications :: TcS a -> TcS (Bool, a)
1548 reportUnifications (TcS thing_inside)
1549 = TcS $ \ env ->
1550 do { inner_unified <- TcM.newTcRef False
1551 ; res <- thing_inside (env { tcs_unified = inner_unified })
1552 ; dirty <- TcM.readTcRef inner_unified
1553 ; return (dirty, res) }
1554
1555 getDefaultInfo :: TcS ([Type], (Bool, Bool))
1556 getDefaultInfo = wrapTcS TcM.tcGetDefaultTys
1557
1558 -- Just get some environments needed for instance looking up and matching
1559 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1560
1561 getInstEnvs :: TcS InstEnvs
1562 getInstEnvs = wrapTcS $ TcM.tcGetInstEnvs
1563
1564 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
1565 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
1566
1567 getTopEnv :: TcS HscEnv
1568 getTopEnv = wrapTcS $ TcM.getTopEnv
1569
1570 getGblEnv :: TcS TcGblEnv
1571 getGblEnv = wrapTcS $ TcM.getGblEnv
1572
1573 -- Setting names as used (used in the deriving of Coercible evidence)
1574 -- Too hackish to expose it to TcS? In that case somehow extract the used
1575 -- constructors from the result of solveInteract
1576 addUsedRdrNamesTcS :: [RdrName] -> TcS ()
1577 addUsedRdrNamesTcS names = wrapTcS $ addUsedRdrNames names
1578
1579 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
1580 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1581
1582 checkWellStagedDFun :: PredType -> DFunId -> CtLoc -> TcS ()
1583 checkWellStagedDFun pred dfun_id loc
1584 = wrapTcS $ TcM.setCtLoc loc $
1585 do { use_stage <- TcM.getStage
1586 ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
1587 where
1588 pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
1589 bind_lvl = TcM.topIdLvl dfun_id
1590
1591 pprEq :: TcType -> TcType -> SDoc
1592 pprEq ty1 ty2 = pprParendType ty1 <+> char '~' <+> pprParendType ty2
1593
1594 isTouchableMetaTyVarTcS :: TcTyVar -> TcS Bool
1595 isTouchableMetaTyVarTcS tv
1596 = do { tclvl <- getTcLevel
1597 ; return $ isTouchableMetaTyVar tclvl tv }
1598
1599 isFilledMetaTyVar_maybe :: TcTyVar -> TcS (Maybe Type)
1600 isFilledMetaTyVar_maybe tv
1601 = ASSERT2( isTcTyVar tv, ppr tv )
1602 case tcTyVarDetails tv of
1603 MetaTv { mtv_ref = ref }
1604 -> do { cts <- wrapTcS (TcM.readTcRef ref)
1605 ; case cts of
1606 Indirect ty -> return (Just ty)
1607 Flexi -> return Nothing }
1608 _ -> return Nothing
1609
1610 isFilledMetaTyVar :: TcTyVar -> TcS Bool
1611 isFilledMetaTyVar tv = wrapTcS (TcM.isFilledMetaTyVar tv)
1612
1613 zonkTyVarsAndFV :: TcTyVarSet -> TcS TcTyVarSet
1614 zonkTyVarsAndFV tvs = wrapTcS (TcM.zonkTyVarsAndFV tvs)
1615
1616 zonkTcType :: TcType -> TcS TcType
1617 zonkTcType ty = wrapTcS (TcM.zonkTcType ty)
1618
1619 zonkTcTyVar :: TcTyVar -> TcS TcType
1620 zonkTcTyVar tv = wrapTcS (TcM.zonkTcTyVar tv)
1621
1622 zonkSimples :: Cts -> TcS Cts
1623 zonkSimples cts = wrapTcS (TcM.zonkSimples cts)
1624
1625 {-
1626 Note [Do not add duplicate derived insolubles]
1627 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1628 In general we *must* add an insoluble (Int ~ Bool) even if there is
1629 one such there already, because they may come from distinct call
1630 sites. Not only do we want an error message for each, but with
1631 -fdefer-type-errors we must generate evidence for each. But for
1632 *derived* insolubles, we only want to report each one once. Why?
1633
1634 (a) A constraint (C r s t) where r -> s, say, may generate the same fundep
1635 equality many times, as the original constraint is sucessively rewritten.
1636
1637 (b) Ditto the successive iterations of the main solver itself, as it traverses
1638 the constraint tree. See example below.
1639
1640 Also for *given* insolubles we may get repeated errors, as we
1641 repeatedly traverse the constraint tree. These are relatively rare
1642 anyway, so removing duplicates seems ok. (Alternatively we could take
1643 the SrcLoc into account.)
1644
1645 Note that the test does not need to be particularly efficient because
1646 it is only used if the program has a type error anyway.
1647
1648 Example of (b): assume a top-level class and instance declaration:
1649
1650 class D a b | a -> b
1651 instance D [a] [a]
1652
1653 Assume we have started with an implication:
1654
1655 forall c. Eq c => { wc_simple = D [c] c [W] }
1656
1657 which we have simplified to:
1658
1659 forall c. Eq c => { wc_simple = D [c] c [W]
1660 , wc_insols = (c ~ [c]) [D] }
1661
1662 For some reason, e.g. because we floated an equality somewhere else,
1663 we might try to re-solve this implication. If we do not do a
1664 dropDerivedWC, then we will end up trying to solve the following
1665 constraints the second time:
1666
1667 (D [c] c) [W]
1668 (c ~ [c]) [D]
1669
1670 which will result in two Deriveds to end up in the insoluble set:
1671
1672 wc_simple = D [c] c [W]
1673 wc_insols = (c ~ [c]) [D], (c ~ [c]) [D]
1674 -}
1675
1676 -- Flatten skolems
1677 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1678 newFlattenSkolem :: CtFlavour -> CtLoc
1679 -> TcType -- F xis
1680 -> TcS (CtEvidence, TcTyVar) -- [W] x:: F xis ~ fsk
1681 newFlattenSkolem Given loc fam_ty
1682 = do { fsk <- wrapTcS $
1683 do { uniq <- TcM.newUnique
1684 ; let name = TcM.mkTcTyVarName uniq (fsLit "fsk")
1685 ; return (mkTcTyVar name (typeKind fam_ty) (FlatSkol fam_ty)) }
1686 ; let ev = CtGiven { ctev_pred = mkTcEqPred fam_ty (mkTyVarTy fsk)
1687 , ctev_evtm = EvCoercion (mkTcNomReflCo fam_ty)
1688 , ctev_loc = loc }
1689 ; return (ev, fsk) }
1690
1691 newFlattenSkolem _ loc fam_ty -- Make a wanted
1692 = do { fuv <- wrapTcS $
1693 do { uniq <- TcM.newUnique
1694 ; ref <- TcM.newMutVar Flexi
1695 ; let details = MetaTv { mtv_info = FlatMetaTv
1696 , mtv_ref = ref
1697 , mtv_tclvl = fskTcLevel }
1698 name = TcM.mkTcTyVarName uniq (fsLit "s")
1699 ; return (mkTcTyVar name (typeKind fam_ty) details) }
1700 ; ev <- newWantedEvVarNC loc (mkTcEqPred fam_ty (mkTyVarTy fuv))
1701 ; return (ev, fuv) }
1702
1703 extendFlatCache :: TyCon -> [Type] -> (TcCoercion, TcType, CtFlavour) -> TcS ()
1704 extendFlatCache tc xi_args stuff
1705 = do { dflags <- getDynFlags
1706 ; when (gopt Opt_FlatCache dflags) $
1707 updInertTcS $ \ is@(IS { inert_flat_cache = fc }) ->
1708 is { inert_flat_cache = insertFunEq fc tc xi_args stuff } }
1709
1710 -- Instantiations
1711 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1712
1713 instDFunType :: DFunId -> [DFunInstType] -> TcS ([TcType], TcThetaType)
1714 instDFunType dfun_id inst_tys
1715 = wrapTcS $ TcM.instDFunType dfun_id inst_tys
1716
1717 newFlexiTcSTy :: Kind -> TcS TcType
1718 newFlexiTcSTy knd = wrapTcS (TcM.newFlexiTyVarTy knd)
1719
1720 cloneMetaTyVar :: TcTyVar -> TcS TcTyVar
1721 cloneMetaTyVar tv = wrapTcS (TcM.cloneMetaTyVar tv)
1722
1723 demoteUnfilledFmv :: TcTyVar -> TcS ()
1724 -- If a flatten-meta-var is still un-filled,
1725 -- turn it into an ordinary meta-var
1726 demoteUnfilledFmv fmv
1727 = wrapTcS $ do { is_filled <- TcM.isFilledMetaTyVar fmv
1728 ; unless is_filled $
1729 do { tv_ty <- TcM.newFlexiTyVarTy (tyVarKind fmv)
1730 ; TcM.writeMetaTyVar fmv tv_ty } }
1731
1732 instFlexiTcS :: [TKVar] -> TcS (TvSubst, [TcType])
1733 instFlexiTcS tvs = wrapTcS (mapAccumLM inst_one emptyTvSubst tvs)
1734 where
1735 inst_one subst tv
1736 = do { ty' <- instFlexiTcSHelper (tyVarName tv)
1737 (substTy subst (tyVarKind tv))
1738 ; return (extendTvSubst subst tv ty', ty') }
1739
1740 instFlexiTcSHelper :: Name -> Kind -> TcM TcType
1741 instFlexiTcSHelper tvname kind
1742 = do { uniq <- TcM.newUnique
1743 ; details <- TcM.newMetaDetails (TauTv False)
1744 ; let name = setNameUnique tvname uniq
1745 ; return (mkTyVarTy (mkTcTyVar name kind details)) }
1746
1747 instFlexiTcSHelperTcS :: Name -> Kind -> TcS TcType
1748 instFlexiTcSHelperTcS n k = wrapTcS (instFlexiTcSHelper n k)
1749
1750
1751 -- Creating and setting evidence variables and CtFlavors
1752 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1753
1754 data Freshness = Fresh | Cached
1755
1756 isFresh :: Freshness -> Bool
1757 isFresh Fresh = True
1758 isFresh Cached = False
1759
1760 freshGoals :: [(CtEvidence, Freshness)] -> [CtEvidence]
1761 freshGoals mns = [ ctev | (ctev, Fresh) <- mns ]
1762
1763 setEvBind :: EvVar -> EvTerm -> TcS ()
1764 setEvBind the_ev tm
1765 = do { tc_evbinds <- getTcEvBinds
1766 ; wrapTcS $ TcM.addTcEvBind tc_evbinds the_ev tm }
1767
1768 newTcEvBinds :: TcS EvBindsVar
1769 newTcEvBinds = wrapTcS TcM.newTcEvBinds
1770
1771 newEvVar :: TcPredType -> TcS EvVar
1772 newEvVar pred = wrapTcS (TcM.newEvVar pred)
1773
1774 newGivenEvVar :: CtLoc -> (TcPredType, EvTerm) -> TcS CtEvidence
1775 -- Make a new variable of the given PredType,
1776 -- immediately bind it to the given term
1777 -- and return its CtEvidence
1778 -- Precondition: this is not a kind equality
1779 -- See Note [Do not create Given kind equalities]
1780 newGivenEvVar loc (pred, rhs)
1781 = ASSERT2( not (isKindEquality pred), ppr pred $$ pprCtOrigin (ctLocOrigin loc) )
1782 do { new_ev <- newEvVar pred
1783 ; setEvBind new_ev rhs
1784 ; return (CtGiven { ctev_pred = pred, ctev_evtm = EvId new_ev, ctev_loc = loc }) }
1785
1786 newGivenEvVars :: CtLoc -> [(TcPredType, EvTerm)] -> TcS [CtEvidence]
1787 -- Like newGivenEvVar, but automatically discard kind equalities
1788 -- See Note [Do not create Given kind equalities]
1789 newGivenEvVars loc pts = mapM (newGivenEvVar loc) (filterOut (isKindEquality . fst) pts)
1790
1791 isKindEquality :: TcPredType -> Bool
1792 -- See Note [Do not create Given kind equalities]
1793 isKindEquality pred = case classifyPredType pred of
1794 EqPred _ t1 _ -> isKind t1
1795 _ -> False
1796
1797 {- Note [Do not create Given kind equalities]
1798 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1799 We do not want to create a Given kind equality like
1800
1801 [G] kv ~ k -- kv is a skolem kind variable
1802 -- Reason we don't yet support non-Refl kind equalities
1803
1804 This showed up in Trac #8566, where we had a data type
1805 data I (u :: U *) (r :: [*]) :: * where
1806 A :: I (AA t as) r -- Existential k
1807 so A has type
1808 A :: forall (u:U *) (r:[*]) Universal
1809 (k:BOX) (t:k) (as:[U *]). Existential
1810 (u ~ AA * k t as) => I u r
1811
1812 There is no direct kind equality, but in a pattern match where 'u' is
1813 instantiated to, say, (AA * kk (t1:kk) as1), we'd decompose to get
1814 k ~ kk, t ~ t1, as ~ as1
1815 This is bad. We "fix" this by simply ignoring the Given kind equality
1816 But the Right Thing is to add kind equalities!
1817
1818 But note (Trac #8705) that we *do* create Given (non-canonical) equalities
1819 with un-equal kinds, e.g.
1820 [G] t1::k1 ~ t2::k2 -- k1 and k2 are un-equal kinds
1821 Reason: k1 or k2 might be unification variables that have already been
1822 unified (at this point we have not canonicalised the types), so we want
1823 to emit this t1~t2 as a (non-canonical) Given in the work-list. If k1/k2
1824 have been unified, we'll find that when we canonicalise it, and the
1825 t1~t2 information may be crucial (Trac #8705 is an example).
1826
1827 If it turns out that k1 and k2 are really un-equal, then it'll end up
1828 as an Irreducible (see Note [Equalities with incompatible kinds] in
1829 TcCanonical), and will do no harm.
1830 -}
1831
1832 newWantedEvVarNC :: CtLoc -> TcPredType -> TcS CtEvidence
1833 -- Don't look up in the solved/inerts; we know it's not there
1834 newWantedEvVarNC loc pty
1835 = do { new_ev <- newEvVar pty
1836 ; return (CtWanted { ctev_pred = pty, ctev_evar = new_ev, ctev_loc = loc })}
1837
1838 newWantedEvVar :: CtLoc -> TcPredType -> TcS (CtEvidence, Freshness)
1839 -- For anything except ClassPred, this is the same as newWantedEvVarNC
1840 newWantedEvVar loc pty
1841 = do { mb_ct <- lookupInInerts loc pty
1842 ; case mb_ct of
1843 Just ctev | not (isDerived ctev)
1844 -> do { traceTcS "newWantedEvVar/cache hit" $ ppr ctev
1845 ; return (ctev, Cached) }
1846 _ -> do { ctev <- newWantedEvVarNC loc pty
1847 ; traceTcS "newWantedEvVar/cache miss" $ ppr ctev
1848 ; return (ctev, Fresh) } }
1849
1850 emitNewDerived :: CtLoc -> TcPredType -> TcS ()
1851 -- Create new Derived and put it in the work list
1852 emitNewDerived loc pred
1853 = do { mb_ev <- newDerived loc pred
1854 ; case mb_ev of
1855 Nothing -> return ()
1856 Just ev -> do { traceTcS "Emitting [D]" (ppr ev)
1857 ; updWorkListTcS (extendWorkListCt (mkNonCanonical ev)) } }
1858
1859 newDerived :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence)
1860 -- Returns Nothing if cached,
1861 -- Just pred if not cached
1862 newDerived loc pred
1863 = do { mb_ct <- lookupInInerts loc pred
1864 ; return (case mb_ct of
1865 Just {} -> Nothing
1866 Nothing -> Just (CtDerived { ctev_pred = pred, ctev_loc = loc })) }
1867
1868
1869 matchFam :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcType))
1870 matchFam tycon args = wrapTcS $ matchFamTcM tycon args
1871
1872 matchFamTcM :: TyCon -> [Type] -> TcM (Maybe (TcCoercion, TcType))
1873 -- Given (F tys) return (ty, co), where co :: F tys ~ ty
1874 matchFamTcM tycon args
1875 = do { fam_envs <- FamInst.tcGetFamInstEnvs
1876 ; return $ fmap (first TcCoercion) $
1877 reduceTyFamApp_maybe fam_envs Nominal tycon args }
1878
1879 {-
1880 Note [Residual implications]
1881 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1882 The wl_implics in the WorkList are the residual implication
1883 constraints that are generated while solving or canonicalising the
1884 current worklist. Specifically, when canonicalising
1885 (forall a. t1 ~ forall a. t2)
1886 from which we get the implication
1887 (forall a. t1 ~ t2)
1888 See TcSMonad.deferTcSForAllEq
1889 -}
1890
1891 -- Deferring forall equalities as implications
1892 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1893
1894 deferTcSForAllEq :: Role -- Nominal or Representational
1895 -> CtLoc -- Original wanted equality flavor
1896 -> ([TyVar],TcType) -- ForAll tvs1 body1
1897 -> ([TyVar],TcType) -- ForAll tvs2 body2
1898 -> TcS EvTerm
1899 -- Some of this functionality is repeated from TcUnify,
1900 -- consider having a single place where we create fresh implications.
1901 deferTcSForAllEq role loc (tvs1,body1) (tvs2,body2)
1902 = do { (subst1, skol_tvs) <- wrapTcS $ TcM.tcInstSkolTyVars tvs1
1903 ; let tys = mkTyVarTys skol_tvs
1904 phi1 = Type.substTy subst1 body1
1905 phi2 = Type.substTy (zipTopTvSubst tvs2 tys) body2
1906 skol_info = UnifyForAllSkol skol_tvs phi1
1907 eq_pred = case role of
1908 Nominal -> mkTcEqPred phi1 phi2
1909 Representational -> mkCoerciblePred phi1 phi2
1910 Phantom -> panic "deferTcSForAllEq Phantom"
1911 ; (ctev, freshness) <- newWantedEvVar loc eq_pred
1912 ; coe_inside <- case freshness of
1913 Cached -> return (ctEvCoercion ctev)
1914 Fresh -> do { ev_binds_var <- newTcEvBinds
1915 ; env <- wrapTcS $ TcM.getLclEnv
1916 ; let ev_binds = TcEvBinds ev_binds_var
1917 new_ct = mkNonCanonical ctev
1918 new_co = ctEvCoercion ctev
1919 new_tclvl = pushTcLevel (tcl_tclvl env)
1920 ; let wc = WC { wc_simple = singleCt new_ct
1921 , wc_impl = emptyBag
1922 , wc_insol = emptyCts }
1923 imp = Implic { ic_tclvl = new_tclvl
1924 , ic_skols = skol_tvs
1925 , ic_no_eqs = True
1926 , ic_given = []
1927 , ic_wanted = wc
1928 , ic_insol = False
1929 , ic_binds = ev_binds_var
1930 , ic_env = env
1931 , ic_info = skol_info }
1932 ; updWorkListTcS (extendWorkListImplic imp)
1933 ; return (TcLetCo ev_binds new_co) }
1934
1935 ; return $ EvCoercion (foldr mkTcForAllCo coe_inside skol_tvs) }
1936