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