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