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