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