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