be28deb2ca12e469bf7f28cf769f398e53259e89
[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 setWantedTyBind, 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,
41 emptyInert, getTcSInerts, setTcSInerts,
42 getUnsolvedInerts, checkAllSolved,
43 splitInertCans, 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,
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 ( partition, 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 updInertCans :: (InertCans -> InertCans) -> TcS ()
617 -- Modify the inert set with the supplied function
618 updInertCans upd_fn
619 = updInertTcS $ \ inerts -> inerts { inert_cans = upd_fn (inert_cans inerts) }
620
621 updInertDicts :: (DictMap Ct -> DictMap Ct) -> TcS ()
622 -- Modify the inert set with the supplied function
623 updInertDicts upd_fn
624 = updInertCans $ \ ics -> ics { inert_dicts = upd_fn (inert_dicts ics) }
625
626 updInertFunEqs :: (FunEqMap Ct -> FunEqMap Ct) -> TcS ()
627 -- Modify the inert set with the supplied function
628 updInertFunEqs upd_fn
629 = updInertCans $ \ ics -> ics { inert_funeqs = upd_fn (inert_funeqs ics) }
630
631 updInertIrreds :: (Cts -> Cts) -> TcS ()
632 -- Modify the inert set with the supplied function
633 updInertIrreds upd_fn
634 = updInertCans $ \ ics -> ics { inert_irreds = upd_fn (inert_irreds ics) }
635
636
637 prepareInertsForImplications :: InertSet -> (InertSet)
638 -- See Note [Preparing inert set for implications]
639 prepareInertsForImplications is@(IS { inert_cans = cans })
640 = is { inert_cans = getGivens cans
641 , inert_flat_cache = emptyFunEqs } -- See Note [Do not inherit the flat cache]
642 where
643 getGivens (IC { inert_eqs = eqs
644 , inert_irreds = irreds
645 , inert_funeqs = funeqs
646 , inert_dicts = dicts })
647 = IC { inert_eqs = filterVarEnv is_given_ecl eqs
648 , inert_funeqs = filterFunEqs isGivenCt funeqs
649 , inert_irreds = Bag.filterBag isGivenCt irreds
650 , inert_dicts = filterDicts isGivenCt dicts
651 , inert_insols = emptyCts }
652
653 is_given_ecl :: EqualCtList -> Bool
654 is_given_ecl (ct:rest) | isGivenCt ct = ASSERT( null rest ) True
655 is_given_ecl _ = False
656
657 {-
658 Note [Do not inherit the flat cache]
659 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
660 We do not want to inherit the flat cache when processing nested
661 implications. Consider
662 a ~ F b, forall c. b~Int => blah
663 If we have F b ~ fsk in the flat-cache, and we push that into the
664 nested implication, we might miss that F b can be rewritten to F Int,
665 and hence perhpas solve it. Moreover, the fsk from outside is
666 flattened out after solving the outer level, but and we don't
667 do that flattening recursively.
668
669 Note [Preparing inert set for implications]
670 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
671 Before solving the nested implications, we trim the inert set,
672 retaining only Givens. These givens can be used when solving
673 the inner implications.
674
675 There might be cases where interactions between wanteds at different levels
676 could help to solve a constraint. For example
677
678 class C a b | a -> b
679 (C Int alpha), (forall d. C d blah => C Int a)
680
681 If we pushed the (C Int alpha) inwards, as a given, it can produce a
682 fundep (alpha~a) and this can float out again and be used to fix
683 alpha. (In general we can't float class constraints out just in case
684 (C d blah) might help to solve (C Int a).) But we ignore this possiblity.
685
686 For Derived constraints we don't have evidence, so we do not turn
687 them into Givens. There can *be* deriving CFunEqCans; see Trac #8129.
688 -}
689
690 getInertEqs :: TcS (TyVarEnv EqualCtList)
691 getInertEqs
692 = do { inert <- getTcSInerts
693 ; return (inert_eqs (inert_cans inert)) }
694
695 getUnsolvedInerts :: TcS ( Bag Implication
696 , Cts -- Tyvar eqs: a ~ ty
697 , Cts -- Fun eqs: F a ~ ty
698 , Cts -- Insoluble
699 , Cts ) -- All others
700 getUnsolvedInerts
701 = do { IC { inert_eqs = tv_eqs
702 , inert_funeqs = fun_eqs
703 , inert_irreds = irreds, inert_dicts = idicts
704 , inert_insols = insols } <- getInertCans
705
706 ; let unsolved_tv_eqs = foldVarEnv (\cts rest ->
707 foldr add_if_unsolved rest cts)
708 emptyCts tv_eqs
709 unsolved_fun_eqs = foldFunEqs add_if_unsolved fun_eqs emptyCts
710 unsolved_irreds = Bag.filterBag is_unsolved irreds
711 unsolved_dicts = foldDicts add_if_unsolved idicts emptyCts
712
713 others = unsolved_irreds `unionBags` unsolved_dicts
714
715 ; implics <- getWorkListImplics
716
717 ; return ( implics, unsolved_tv_eqs, unsolved_fun_eqs, insols, others) }
718 -- Keep even the given insolubles
719 -- so that we can report dead GADT pattern match branches
720 where
721 add_if_unsolved :: Ct -> Cts -> Cts
722 add_if_unsolved ct cts | is_unsolved ct = ct `consCts` cts
723 | otherwise = cts
724
725 is_unsolved ct = not (isGivenCt ct) -- Wanted or Derived
726
727 getNoGivenEqs :: TcLevel -- TcLevel of this implication
728 -> [TcTyVar] -- Skolems of this implication
729 -> TcS Bool -- True <=> definitely no residual given equalities
730 -- See Note [When does an implication have given equalities?]
731 getNoGivenEqs tclvl skol_tvs
732 = do { inerts@(IC { inert_eqs = ieqs, inert_irreds = iirreds, inert_funeqs = funeqs })
733 <- getInertCans
734 ; let local_fsks = foldFunEqs add_fsk funeqs emptyVarSet
735
736 has_given_eqs = foldrBag ((||) . ev_given_here . ctEvidence) False iirreds
737 || foldVarEnv ((||) . eqs_given_here local_fsks) False ieqs
738
739 ; traceTcS "getNoGivenEqs" (vcat [ppr has_given_eqs, ppr inerts])
740 ; return (not has_given_eqs) }
741 where
742 eqs_given_here :: VarSet -> EqualCtList -> Bool
743 eqs_given_here local_fsks [CTyEqCan { cc_tyvar = tv, cc_ev = ev }]
744 -- Givens are always a sigleton
745 = not (skolem_bound_here local_fsks tv) && ev_given_here ev
746 eqs_given_here _ _ = False
747
748 ev_given_here :: CtEvidence -> Bool
749 -- True for a Given bound by the curent implication,
750 -- i.e. the current level
751 ev_given_here ev
752 = isGiven ev
753 && tclvl == ctLocLevel (ctEvLoc ev)
754
755 add_fsk :: Ct -> VarSet -> VarSet
756 add_fsk ct fsks | CFunEqCan { cc_fsk = tv, cc_ev = ev } <- ct
757 , isGiven ev = extendVarSet fsks tv
758 | otherwise = fsks
759
760 skol_tv_set = mkVarSet skol_tvs
761 skolem_bound_here local_fsks tv -- See Note [Let-bound skolems]
762 = case tcTyVarDetails tv of
763 SkolemTv {} -> tv `elemVarSet` skol_tv_set
764 FlatSkol {} -> not (tv `elemVarSet` local_fsks)
765 _ -> False
766
767 {-
768 Note [When does an implication have given equalities?]
769 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
770 Consider an implication
771 beta => alpha ~ Int
772 where beta is a unification variable that has already been unified
773 to () in an outer scope. Then we can float the (alpha ~ Int) out
774 just fine. So when deciding whether the givens contain an equality,
775 we should canonicalise first, rather than just looking at the original
776 givens (Trac #8644).
777
778 So we simply look at the inert, canonical Givens and see if there are
779 any equalities among them, the calculation of has_given_eqs. There
780 are some wrinkles:
781
782 * We must know which ones are bound in *this* implication and which
783 are bound further out. We can find that out from the TcLevel
784 of the Given, which is itself recorded in the tcl_tclvl field
785 of the TcLclEnv stored in the Given (ev_given_here).
786
787 What about interactions between inner and outer givens?
788 - Outer given is rewritten by an inner given, then there must
789 have been an inner given equality, hence the “given-eq” flag
790 will be true anyway.
791
792 - Inner given rewritten by outer, retains its level (ie. The inner one)
793
794 * We must take account of *potential* equalities, like the one above:
795 beta => ...blah...
796 If we still don't know what beta is, we conservatively treat it as potentially
797 becoming an equality. Hence including 'irreds' in the calculation or has_given_eqs.
798
799 * When flattening givens, we generate Given equalities like
800 <F [a]> : F [a] ~ f,
801 with Refl evidence, and we *don't* want those to count as an equality
802 in the givens! After all, the entire flattening business is just an
803 internal matter, and the evidence does not mention any of the 'givens'
804 of this implication. So we do not treat inert_funeqs as a 'given equality'.
805
806 * See Note [Let-bound skolems] for another wrinkle
807
808 * We do *not* need to worry about representational equalities, because
809 these do not affect the ability to float constraints.
810
811 Note [Let-bound skolems]
812 ~~~~~~~~~~~~~~~~~~~~~~~~
813 If * the inert set contains a canonical Given CTyEqCan (a ~ ty)
814 and * 'a' is a skolem bound in this very implication, b
815
816 then:
817 a) The Given is pretty much a let-binding, like
818 f :: (a ~ b->c) => a -> a
819 Here the equality constraint is like saying
820 let a = b->c in ...
821 It is not adding any new, local equality information,
822 and hence can be ignored by has_given_eqs
823
824 b) 'a' will have been completely substituted out in the inert set,
825 so we can safely discard it. Notably, it doesn't need to be
826 returned as part of 'fsks'
827
828 For an example, see Trac #9211.
829 -}
830
831 splitInertCans :: InertCans -> ([Ct], [Ct], [Ct])
832 -- ^ Extract the (given, derived, wanted) inert constraints
833 splitInertCans iCans = (given,derived,wanted)
834 where
835 allCts = foldDicts (:) (inert_dicts iCans)
836 $ foldFunEqs (:) (inert_funeqs iCans)
837 $ concat (varEnvElts (inert_eqs iCans))
838
839 (derived,other) = partition isDerivedCt allCts
840 (wanted,given) = partition isWantedCt other
841
842 removeInertCts :: [Ct] -> InertCans -> InertCans
843 -- ^ Remove inert constraints from the 'InertCans', for use when a
844 -- typechecker plugin wishes to discard a given.
845 removeInertCts cts icans = foldl' removeInertCt icans cts
846
847 removeInertCt :: InertCans -> Ct -> InertCans
848 removeInertCt is ct =
849 case ct of
850
851 CDictCan { cc_class = cl, cc_tyargs = tys } ->
852 is { inert_dicts = delDict (inert_dicts is) cl tys }
853
854 CFunEqCan { cc_fun = tf, cc_tyargs = tys } ->
855 is { inert_funeqs = delFunEq (inert_funeqs is) tf tys }
856
857 CTyEqCan { cc_tyvar = x, cc_rhs = ty } ->
858 is { inert_eqs = delTyEq (inert_eqs is) x ty }
859
860 CIrredEvCan {} -> panic "removeInertCt: CIrredEvCan"
861 CNonCanonical {} -> panic "removeInertCt: CNonCanonical"
862 CHoleCan {} -> panic "removeInertCt: CHoleCan"
863
864
865 checkAllSolved :: TcS Bool
866 -- True if there are no unsolved wanteds
867 -- Ignore Derived for this purpose, unless in insolubles
868 checkAllSolved
869 = do { is <- getTcSInerts
870
871 ; let icans = inert_cans is
872 unsolved_irreds = Bag.anyBag isWantedCt (inert_irreds icans)
873 unsolved_dicts = foldDicts ((||) . isWantedCt)
874 (inert_dicts icans) False
875 unsolved_funeqs = foldFunEqs ((||) . isWantedCt)
876 (inert_funeqs icans) False
877 unsolved_eqs = foldVarEnv ((||) . any isWantedCt) False
878 (inert_eqs icans)
879
880 ; return (not (unsolved_eqs || unsolved_irreds
881 || unsolved_dicts || unsolved_funeqs
882 || not (isEmptyBag (inert_insols icans)))) }
883
884 lookupFlatCache :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcType, CtFlavour))
885 lookupFlatCache fam_tc tys
886 = do { IS { inert_flat_cache = flat_cache
887 , inert_cans = IC { inert_funeqs = inert_funeqs } } <- getTcSInerts
888 ; return (firstJusts [lookup_inerts inert_funeqs,
889 lookup_flats flat_cache]) }
890 where
891 lookup_inerts inert_funeqs
892 | Just (CFunEqCan { cc_ev = ctev, cc_fsk = fsk })
893 <- findFunEqs inert_funeqs fam_tc tys
894 = Just (ctEvCoercion ctev, mkTyVarTy fsk, ctEvFlavour ctev)
895 | otherwise = Nothing
896
897 lookup_flats flat_cache = findFunEq flat_cache fam_tc tys
898
899
900 lookupInInerts :: TcPredType -> TcS (Maybe CtEvidence)
901 -- Is this exact predicate type cached in the solved or canonicals of the InertSet?
902 lookupInInerts pty
903 | ClassPred cls tys <- classifyPredType pty
904 = do { inerts <- getTcSInerts
905 ; return (lookupSolvedDict inerts cls tys `mplus`
906 lookupInertDict (inert_cans inerts) cls tys) }
907 | otherwise -- NB: No caching for equalities, IPs, holes, or errors
908 = return Nothing
909
910 lookupInertDict :: InertCans -> Class -> [Type] -> Maybe CtEvidence
911 lookupInertDict (IC { inert_dicts = dicts }) cls tys
912 = case findDict dicts cls tys of
913 Just ct -> Just (ctEvidence ct)
914 _ -> Nothing
915
916 lookupSolvedDict :: InertSet -> Class -> [Type] -> Maybe CtEvidence
917 -- Returns just if exactly this predicate type exists in the solved.
918 lookupSolvedDict (IS { inert_solved_dicts = solved }) cls tys
919 = case findDict solved cls tys of
920 Just ev -> Just ev
921 _ -> Nothing
922
923 {-
924 ************************************************************************
925 * *
926 TyEqMap
927 * *
928 ************************************************************************
929 -}
930
931 type TyEqMap a = TyVarEnv a
932
933 findTyEqs :: InertCans -> TyVar -> EqualCtList
934 findTyEqs icans tv = lookupVarEnv (inert_eqs icans) tv `orElse` []
935
936 delTyEq :: TyEqMap EqualCtList -> TcTyVar -> TcType -> TyEqMap EqualCtList
937 delTyEq m tv t = modifyVarEnv (filter (not . isThisOne)) m tv
938 where isThisOne (CTyEqCan { cc_rhs = t1 }) = eqType t t1
939 isThisOne _ = False
940
941 {-
942 ************************************************************************
943 * *
944 TcAppMap, DictMap, FunEqMap
945 * *
946 ************************************************************************
947 -}
948
949 type TcAppMap a = UniqFM (ListMap TypeMap a)
950 -- Indexed by tycon then the arg types
951 -- Used for types and classes; hence UniqFM
952
953 emptyTcAppMap :: TcAppMap a
954 emptyTcAppMap = emptyUFM
955
956 findTcApp :: TcAppMap a -> Unique -> [Type] -> Maybe a
957 findTcApp m u tys = do { tys_map <- lookupUFM m u
958 ; lookupTM tys tys_map }
959
960 delTcApp :: TcAppMap a -> Unique -> [Type] -> TcAppMap a
961 delTcApp m cls tys = adjustUFM (deleteTM tys) m cls
962
963 insertTcApp :: TcAppMap a -> Unique -> [Type] -> a -> TcAppMap a
964 insertTcApp m cls tys ct = alterUFM alter_tm m cls
965 where
966 alter_tm mb_tm = Just (insertTM tys ct (mb_tm `orElse` emptyTM))
967
968 -- mapTcApp :: (a->b) -> TcAppMap a -> TcAppMap b
969 -- mapTcApp f = mapUFM (mapTM f)
970
971 filterTcAppMap :: (Ct -> Bool) -> TcAppMap Ct -> TcAppMap Ct
972 filterTcAppMap f m
973 = mapUFM do_tm m
974 where
975 do_tm tm = foldTM insert_mb tm emptyTM
976 insert_mb ct tm
977 | f ct = insertTM tys ct tm
978 | otherwise = tm
979 where
980 tys = case ct of
981 CFunEqCan { cc_tyargs = tys } -> tys
982 CDictCan { cc_tyargs = tys } -> tys
983 _ -> pprPanic "filterTcAppMap" (ppr ct)
984
985 tcAppMapToBag :: TcAppMap a -> Bag a
986 tcAppMapToBag m = foldTcAppMap consBag m emptyBag
987
988 foldTcAppMap :: (a -> b -> b) -> TcAppMap a -> b -> b
989 foldTcAppMap k m z = foldUFM (foldTM k) z m
990
991 -------------------------
992 type DictMap a = TcAppMap a
993
994 emptyDictMap :: DictMap a
995 emptyDictMap = emptyTcAppMap
996
997 -- sizeDictMap :: DictMap a -> Int
998 -- sizeDictMap m = foldDicts (\ _ x -> x+1) m 0
999
1000 findDict :: DictMap a -> Class -> [Type] -> Maybe a
1001 findDict m cls tys = findTcApp m (getUnique cls) tys
1002
1003 findDictsByClass :: DictMap a -> Class -> Bag a
1004 findDictsByClass m cls
1005 | Just tm <- lookupUFM m cls = foldTM consBag tm emptyBag
1006 | otherwise = emptyBag
1007
1008 delDict :: DictMap a -> Class -> [Type] -> DictMap a
1009 delDict m cls tys = delTcApp m (getUnique cls) tys
1010
1011 addDict :: DictMap a -> Class -> [Type] -> a -> DictMap a
1012 addDict m cls tys item = insertTcApp m (getUnique cls) tys item
1013
1014 addDictsByClass :: DictMap Ct -> Class -> Bag Ct -> DictMap Ct
1015 addDictsByClass m cls items
1016 = addToUFM m cls (foldrBag add emptyTM items)
1017 where
1018 add ct@(CDictCan { cc_tyargs = tys }) tm = insertTM tys ct tm
1019 add ct _ = pprPanic "addDictsByClass" (ppr ct)
1020
1021 filterDicts :: (Ct -> Bool) -> DictMap Ct -> DictMap Ct
1022 filterDicts f m = filterTcAppMap f m
1023
1024 partitionDicts :: (Ct -> Bool) -> DictMap Ct -> (Bag Ct, DictMap Ct)
1025 partitionDicts f m = foldTcAppMap k m (emptyBag, emptyDicts)
1026 where
1027 k ct (yeses, noes) | f ct = (ct `consBag` yeses, noes)
1028 | otherwise = (yeses, add ct noes)
1029 add ct@(CDictCan { cc_class = cls, cc_tyargs = tys }) m
1030 = addDict m cls tys ct
1031 add ct _ = pprPanic "partitionDicts" (ppr ct)
1032
1033 dictsToBag :: DictMap a -> Bag a
1034 dictsToBag = tcAppMapToBag
1035
1036 foldDicts :: (a -> b -> b) -> DictMap a -> b -> b
1037 foldDicts = foldTcAppMap
1038
1039 emptyDicts :: DictMap a
1040 emptyDicts = emptyTcAppMap
1041
1042 ------------------------
1043 type FunEqMap a = TcAppMap a -- A map whose key is a (TyCon, [Type]) pair
1044
1045 emptyFunEqs :: TcAppMap a
1046 emptyFunEqs = emptyTcAppMap
1047
1048 sizeFunEqMap :: FunEqMap a -> Int
1049 sizeFunEqMap m = foldFunEqs (\ _ x -> x+1) m 0
1050
1051 findFunEq :: FunEqMap a -> TyCon -> [Type] -> Maybe a
1052 findFunEq m tc tys = findTcApp m (getUnique tc) tys
1053
1054 findFunEqs :: FunEqMap a -> TyCon -> [Type] -> Maybe a
1055 findFunEqs m tc tys = findTcApp m (getUnique tc) tys
1056
1057 funEqsToBag :: FunEqMap a -> Bag a
1058 funEqsToBag m = foldTcAppMap consBag m emptyBag
1059
1060 findFunEqsByTyCon :: FunEqMap a -> TyCon -> [a]
1061 -- Get inert function equation constraints that have the given tycon
1062 -- in their head. Not that the constraints remain in the inert set.
1063 -- We use this to check for derived interactions with built-in type-function
1064 -- constructors.
1065 findFunEqsByTyCon m tc
1066 | Just tm <- lookupUFM m tc = foldTM (:) tm []
1067 | otherwise = []
1068
1069 foldFunEqs :: (a -> b -> b) -> FunEqMap a -> b -> b
1070 foldFunEqs = foldTcAppMap
1071
1072 -- mapFunEqs :: (a -> b) -> FunEqMap a -> FunEqMap b
1073 -- mapFunEqs = mapTcApp
1074
1075 filterFunEqs :: (Ct -> Bool) -> FunEqMap Ct -> FunEqMap Ct
1076 filterFunEqs = filterTcAppMap
1077
1078 insertFunEq :: FunEqMap a -> TyCon -> [Type] -> a -> FunEqMap a
1079 insertFunEq m tc tys val = insertTcApp m (getUnique tc) tys val
1080
1081 -- insertFunEqCt :: FunEqMap Ct -> Ct -> FunEqMap Ct
1082 -- insertFunEqCt m ct@(CFunEqCan { cc_fun = tc, cc_tyargs = tys })
1083 -- = insertFunEq m tc tys ct
1084 -- insertFunEqCt _ ct = pprPanic "insertFunEqCt" (ppr ct)
1085
1086 partitionFunEqs :: (Ct -> Bool) -> FunEqMap Ct -> ([Ct], FunEqMap Ct)
1087 -- Optimise for the case where the predicate is false
1088 -- partitionFunEqs is called only from kick-out, and kick-out usually
1089 -- kicks out very few equalities, so we want to optimise for that case
1090 partitionFunEqs f m = (yeses, foldr del m yeses)
1091 where
1092 yeses = foldTcAppMap k m []
1093 k ct yeses | f ct = ct : yeses
1094 | otherwise = yeses
1095 del (CFunEqCan { cc_fun = tc, cc_tyargs = tys }) m
1096 = delFunEq m tc tys
1097 del ct _ = pprPanic "partitionFunEqs" (ppr ct)
1098
1099 delFunEq :: FunEqMap a -> TyCon -> [Type] -> FunEqMap a
1100 delFunEq m tc tys = delTcApp m (getUnique tc) tys
1101
1102 {-
1103 ************************************************************************
1104 * *
1105 * The TcS solver monad *
1106 * *
1107 ************************************************************************
1108
1109 Note [The TcS monad]
1110 ~~~~~~~~~~~~~~~~~~~~
1111 The TcS monad is a weak form of the main Tc monad
1112
1113 All you can do is
1114 * fail
1115 * allocate new variables
1116 * fill in evidence variables
1117
1118 Filling in a dictionary evidence variable means to create a binding
1119 for it, so TcS carries a mutable location where the binding can be
1120 added. This is initialised from the innermost implication constraint.
1121 -}
1122
1123 data TcSEnv
1124 = TcSEnv {
1125 tcs_ev_binds :: EvBindsVar,
1126
1127 tcs_unified :: IORef Bool,
1128 -- The "dirty-flag" Bool is set True when
1129 -- we unify a unification variable
1130
1131 tcs_count :: IORef Int, -- Global step count
1132
1133 tcs_inerts :: IORef InertSet, -- Current inert set
1134
1135 -- The main work-list and the flattening worklist
1136 -- See Note [Work list priorities] and
1137 tcs_worklist :: IORef WorkList -- Current worklist
1138 }
1139
1140 ---------------
1141 newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
1142
1143 instance Functor TcS where
1144 fmap f m = TcS $ fmap f . unTcS m
1145
1146 instance Applicative TcS where
1147 pure = return
1148 (<*>) = ap
1149
1150 instance Monad TcS where
1151 return x = TcS (\_ -> return x)
1152 fail err = TcS (\_ -> fail err)
1153 m >>= k = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
1154
1155 instance MonadUnique TcS where
1156 getUniqueSupplyM = wrapTcS getUniqueSupplyM
1157
1158 -- Basic functionality
1159 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1160 wrapTcS :: TcM a -> TcS a
1161 -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
1162 -- and TcS is supposed to have limited functionality
1163 wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
1164
1165 wrapErrTcS :: TcM a -> TcS a
1166 -- The thing wrapped should just fail
1167 -- There's no static check; it's up to the user
1168 -- Having a variant for each error message is too painful
1169 wrapErrTcS = wrapTcS
1170
1171 wrapWarnTcS :: TcM a -> TcS a
1172 -- The thing wrapped should just add a warning, or no-op
1173 -- There's no static check; it's up to the user
1174 wrapWarnTcS = wrapTcS
1175
1176 failTcS, panicTcS :: SDoc -> TcS a
1177 failTcS = wrapTcS . TcM.failWith
1178 panicTcS doc = pprPanic "TcCanonical" doc
1179
1180 traceTcS :: String -> SDoc -> TcS ()
1181 traceTcS herald doc = wrapTcS (TcM.traceTc herald doc)
1182
1183 runTcPluginTcS :: TcPluginM a -> TcS a
1184 runTcPluginTcS = wrapTcS . runTcPluginM
1185
1186 instance HasDynFlags TcS where
1187 getDynFlags = wrapTcS getDynFlags
1188
1189 getGlobalRdrEnvTcS :: TcS GlobalRdrEnv
1190 getGlobalRdrEnvTcS = wrapTcS TcM.getGlobalRdrEnv
1191
1192 bumpStepCountTcS :: TcS ()
1193 bumpStepCountTcS = TcS $ \env -> do { let ref = tcs_count env
1194 ; n <- TcM.readTcRef ref
1195 ; TcM.writeTcRef ref (n+1) }
1196
1197 csTraceTcS :: SDoc -> TcS ()
1198 csTraceTcS doc
1199 = wrapTcS $ csTraceTcM 1 (return doc)
1200
1201 traceFireTcS :: CtEvidence -> SDoc -> TcS ()
1202 -- Dump a rule-firing trace
1203 traceFireTcS ev doc
1204 = TcS $ \env -> csTraceTcM 1 $
1205 do { n <- TcM.readTcRef (tcs_count env)
1206 ; tclvl <- TcM.getTcLevel
1207 ; return (hang (int n <> brackets (ptext (sLit "U:") <> ppr tclvl
1208 <> ppr (ctLocDepth (ctEvLoc ev)))
1209 <+> doc <> colon)
1210 4 (ppr ev)) }
1211
1212 csTraceTcM :: Int -> TcM SDoc -> TcM ()
1213 -- Constraint-solver tracing, -ddump-cs-trace
1214 csTraceTcM trace_level mk_doc
1215 = do { dflags <- getDynFlags
1216 ; when ( (dopt Opt_D_dump_cs_trace dflags || dopt Opt_D_dump_tc_trace dflags)
1217 && trace_level <= traceLevel dflags ) $
1218 do { msg <- mk_doc
1219 ; TcM.traceTcRn Opt_D_dump_cs_trace msg } }
1220
1221 runTcS :: TcS a -- What to run
1222 -> TcM (a, Bag EvBind)
1223 runTcS tcs
1224 = do { ev_binds_var <- TcM.newTcEvBinds
1225 ; res <- runTcSWithEvBinds ev_binds_var tcs
1226 ; ev_binds <- TcM.getTcEvBinds ev_binds_var
1227 ; return (res, ev_binds) }
1228
1229 runTcSWithEvBinds :: EvBindsVar
1230 -> TcS a
1231 -> TcM a
1232 runTcSWithEvBinds ev_binds_var tcs
1233 = do { unified_var <- TcM.newTcRef False
1234 ; step_count <- TcM.newTcRef 0
1235 ; inert_var <- TcM.newTcRef is
1236 ; wl_var <- TcM.newTcRef emptyWorkList
1237
1238 ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
1239 , tcs_unified = unified_var
1240 , tcs_count = step_count
1241 , tcs_inerts = inert_var
1242 , tcs_worklist = wl_var }
1243
1244 -- Run the computation
1245 ; res <- unTcS tcs env
1246
1247 ; count <- TcM.readTcRef step_count
1248 ; when (count > 0) $
1249 csTraceTcM 0 $ return (ptext (sLit "Constraint solver steps =") <+> int count)
1250
1251 #ifdef DEBUG
1252 ; ev_binds <- TcM.getTcEvBinds ev_binds_var
1253 ; checkForCyclicBinds ev_binds
1254 #endif
1255
1256 ; return res }
1257 where
1258 is = emptyInert
1259
1260 #ifdef DEBUG
1261 checkForCyclicBinds :: Bag EvBind -> TcM ()
1262 checkForCyclicBinds ev_binds
1263 | null cycles
1264 = return ()
1265 | null coercion_cycles
1266 = TcM.traceTc "Cycle in evidence binds" $ ppr cycles
1267 | otherwise
1268 = pprPanic "Cycle in coercion bindings" $ ppr coercion_cycles
1269 where
1270 cycles :: [[EvBind]]
1271 cycles = [c | CyclicSCC c <- stronglyConnCompFromEdgedVertices edges]
1272
1273 coercion_cycles = [c | c <- cycles, any is_co_bind c]
1274 is_co_bind (EvBind { eb_lhs = b }) = isEqVar b
1275
1276 edges :: [(EvBind, EvVar, [EvVar])]
1277 edges = [(bind, bndr, varSetElems (evVarsOfTerm rhs))
1278 | bind@(EvBind { eb_lhs = bndr, eb_rhs = rhs }) <- bagToList ev_binds]
1279 #endif
1280
1281 nestImplicTcS :: EvBindsVar -> TcLevel -> TcS a -> TcS a
1282 nestImplicTcS ref inner_tclvl (TcS thing_inside)
1283 = TcS $ \ TcSEnv { tcs_unified = unified_var
1284 , tcs_inerts = old_inert_var
1285 , tcs_count = count } ->
1286 do { inerts <- TcM.readTcRef old_inert_var
1287 ; let nest_inert = inerts { inert_flat_cache = emptyFunEqs }
1288 -- See Note [Do not inherit the flat cache]
1289 ; new_inert_var <- TcM.newTcRef nest_inert
1290 ; new_wl_var <- TcM.newTcRef emptyWorkList
1291 ; let nest_env = TcSEnv { tcs_ev_binds = ref
1292 , tcs_unified = unified_var
1293 , tcs_count = count
1294 , tcs_inerts = new_inert_var
1295 , tcs_worklist = new_wl_var }
1296 ; res <- TcM.setTcLevel inner_tclvl $
1297 thing_inside nest_env
1298
1299 #ifdef DEBUG
1300 -- Perform a check that the thing_inside did not cause cycles
1301 ; ev_binds <- TcM.getTcEvBinds ref
1302 ; checkForCyclicBinds ev_binds
1303 #endif
1304
1305 ; return res }
1306
1307 recoverTcS :: TcS a -> TcS a -> TcS a
1308 recoverTcS (TcS recovery_code) (TcS thing_inside)
1309 = TcS $ \ env ->
1310 TcM.recoverM (recovery_code env) (thing_inside env)
1311
1312 nestTcS :: TcS a -> TcS a
1313 -- Use the current untouchables, augmenting the current
1314 -- evidence bindings, and solved dictionaries
1315 -- But have no effect on the InertCans, or on the inert_flat_cache
1316 -- (the latter because the thing inside a nestTcS does unflattening)
1317 nestTcS (TcS thing_inside)
1318 = TcS $ \ env@(TcSEnv { tcs_inerts = inerts_var }) ->
1319 do { inerts <- TcM.readTcRef inerts_var
1320 ; new_inert_var <- TcM.newTcRef inerts
1321 ; new_wl_var <- TcM.newTcRef emptyWorkList
1322 ; let nest_env = env { tcs_inerts = new_inert_var
1323 , tcs_worklist = new_wl_var }
1324
1325 ; res <- thing_inside nest_env
1326
1327 ; new_inerts <- TcM.readTcRef new_inert_var
1328 ; TcM.writeTcRef inerts_var -- See Note [Propagate the solved dictionaries]
1329 (inerts { inert_solved_dicts = inert_solved_dicts new_inerts })
1330
1331 ; return res }
1332
1333 tryTcS :: TcS a -> TcS a
1334 -- Like runTcS, but from within the TcS monad
1335 -- Completely fresh inerts and worklist, be careful!
1336 -- Moreover, we will simply throw away all the evidence generated.
1337 tryTcS (TcS thing_inside)
1338 = TcS $ \env ->
1339 do { is_var <- TcM.newTcRef emptyInert
1340 ; unified_var <- TcM.newTcRef False
1341 ; ev_binds_var <- TcM.newTcEvBinds
1342 ; wl_var <- TcM.newTcRef emptyWorkList
1343 ; let nest_env = env { tcs_ev_binds = ev_binds_var
1344 , tcs_unified = unified_var
1345 , tcs_inerts = is_var
1346 , tcs_worklist = wl_var }
1347 ; thing_inside nest_env }
1348
1349 {-
1350 Note [Propagate the solved dictionaries]
1351 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1352 It's really quite important that nestTcS does not discard the solved
1353 dictionaries from the thing_inside.
1354 Consider
1355 Eq [a]
1356 forall b. empty => Eq [a]
1357 We solve the simple (Eq [a]), under nestTcS, and then turn our attention to
1358 the implications. It's definitely fine to use the solved dictionaries on
1359 the inner implications, and it can make a signficant performance difference
1360 if you do so.
1361 -}
1362
1363 -- Getters and setters of TcEnv fields
1364 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1365
1366 -- Getter of inerts and worklist
1367 getTcSInertsRef :: TcS (IORef InertSet)
1368 getTcSInertsRef = TcS (return . tcs_inerts)
1369
1370 getTcSWorkListRef :: TcS (IORef WorkList)
1371 getTcSWorkListRef = TcS (return . tcs_worklist)
1372
1373 getTcSInerts :: TcS InertSet
1374 getTcSInerts = getTcSInertsRef >>= wrapTcS . (TcM.readTcRef)
1375
1376 setTcSInerts :: InertSet -> TcS ()
1377 setTcSInerts ics = do { r <- getTcSInertsRef; wrapTcS (TcM.writeTcRef r ics) }
1378
1379 getWorkListImplics :: TcS (Bag Implication)
1380 getWorkListImplics
1381 = do { wl_var <- getTcSWorkListRef
1382 ; wl_curr <- wrapTcS (TcM.readTcRef wl_var)
1383 ; return (wl_implics wl_curr) }
1384
1385 updWorkListTcS :: (WorkList -> WorkList) -> TcS ()
1386 updWorkListTcS f
1387 = do { wl_var <- getTcSWorkListRef
1388 ; wl_curr <- wrapTcS (TcM.readTcRef wl_var)
1389 ; let new_work = f wl_curr
1390 ; wrapTcS (TcM.writeTcRef wl_var new_work) }
1391
1392 updWorkListTcS_return :: (WorkList -> (a,WorkList)) -> TcS a
1393 -- Process the work list, returning a depleted work list,
1394 -- plus a value extracted from it (typically a work item removed from it)
1395 updWorkListTcS_return f
1396 = do { wl_var <- getTcSWorkListRef
1397 ; wl_curr <- wrapTcS (TcM.readTcRef wl_var)
1398 ; traceTcS "updWorkList" (ppr wl_curr)
1399 ; let (res,new_work) = f wl_curr
1400 ; wrapTcS (TcM.writeTcRef wl_var new_work)
1401 ; return res }
1402
1403 emitWorkNC :: [CtEvidence] -> TcS ()
1404 emitWorkNC evs
1405 | null evs
1406 = return ()
1407 | otherwise
1408 = do { traceTcS "Emitting fresh work" (vcat (map ppr evs))
1409 ; updWorkListTcS (extendWorkListCts (map mkNonCanonical evs)) }
1410
1411 emitWorkCt :: Ct -> TcS ()
1412 emitWorkCt ct
1413 = do { traceTcS "Emitting fresh (canonical) work" (ppr ct)
1414 ; updWorkListTcS (extendWorkListCt ct) }
1415
1416 emitInsoluble :: Ct -> TcS ()
1417 -- Emits a non-canonical constraint that will stand for a frozen error in the inerts.
1418 emitInsoluble ct
1419 = do { traceTcS "Emit insoluble" (ppr ct)
1420 ; updInertTcS add_insol }
1421 where
1422 this_pred = ctPred ct
1423 add_insol is@(IS { inert_cans = ics@(IC { inert_insols = old_insols }) })
1424 | already_there = is
1425 | otherwise = is { inert_cans = ics { inert_insols = old_insols `snocCts` ct } }
1426 where
1427 already_there = not (isWantedCt ct) && anyBag (tcEqType this_pred . ctPred) old_insols
1428 -- See Note [Do not add duplicate derived insolubles]
1429
1430 newTcRef :: a -> TcS (TcRef a)
1431 newTcRef x = wrapTcS (TcM.newTcRef x)
1432
1433 readTcRef :: TcRef a -> TcS a
1434 readTcRef ref = wrapTcS (TcM.readTcRef ref)
1435
1436 updTcRef :: TcRef a -> (a->a) -> TcS ()
1437 updTcRef ref upd_fn = wrapTcS (TcM.updTcRef ref upd_fn)
1438
1439 getTcEvBinds :: TcS EvBindsVar
1440 getTcEvBinds = TcS (return . tcs_ev_binds)
1441
1442 getTcLevel :: TcS TcLevel
1443 getTcLevel = wrapTcS TcM.getTcLevel
1444
1445 getTcEvBindsMap :: TcS EvBindMap
1446 getTcEvBindsMap
1447 = do { EvBindsVar ev_ref _ <- getTcEvBinds
1448 ; wrapTcS $ TcM.readTcRef ev_ref }
1449
1450 setWantedTyBind :: TcTyVar -> TcType -> TcS ()
1451 -- Add a type binding
1452 -- We never do this twice!
1453 setWantedTyBind tv ty
1454 | ASSERT2( isMetaTyVar tv, ppr tv )
1455 isFmvTyVar tv
1456 = ASSERT2( isMetaTyVar tv, ppr tv )
1457 wrapTcS (TcM.writeMetaTyVar tv ty)
1458 -- Write directly into the mutable tyvar
1459 -- Flatten meta-vars are born and die locally
1460
1461 | otherwise
1462 = TcS $ \ env ->
1463 do { TcM.traceTc "setWantedTyBind" (ppr tv <+> text ":=" <+> ppr ty)
1464 ; TcM.writeMetaTyVar tv ty
1465 ; TcM.writeTcRef (tcs_unified env) True }
1466
1467 reportUnifications :: TcS a -> TcS (Bool, a)
1468 reportUnifications (TcS thing_inside)
1469 = TcS $ \ env ->
1470 do { inner_unified <- TcM.newTcRef False
1471 ; res <- thing_inside (env { tcs_unified = inner_unified })
1472 ; dirty <- TcM.readTcRef inner_unified
1473 ; return (dirty, res) }
1474
1475 getDefaultInfo :: TcS ([Type], (Bool, Bool))
1476 getDefaultInfo = wrapTcS TcM.tcGetDefaultTys
1477
1478 -- Just get some environments needed for instance looking up and matching
1479 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1480
1481 getInstEnvs :: TcS InstEnvs
1482 getInstEnvs = wrapTcS $ TcM.tcGetInstEnvs
1483
1484 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
1485 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
1486
1487 getTopEnv :: TcS HscEnv
1488 getTopEnv = wrapTcS $ TcM.getTopEnv
1489
1490 getGblEnv :: TcS TcGblEnv
1491 getGblEnv = wrapTcS $ TcM.getGblEnv
1492
1493 -- Setting names as used (used in the deriving of Coercible evidence)
1494 -- Too hackish to expose it to TcS? In that case somehow extract the used
1495 -- constructors from the result of solveInteract
1496 addUsedRdrNamesTcS :: [RdrName] -> TcS ()
1497 addUsedRdrNamesTcS names = wrapTcS $ addUsedRdrNames names
1498
1499 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
1500 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1501
1502 checkWellStagedDFun :: PredType -> DFunId -> CtLoc -> TcS ()
1503 checkWellStagedDFun pred dfun_id loc
1504 = wrapTcS $ TcM.setCtLoc loc $
1505 do { use_stage <- TcM.getStage
1506 ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
1507 where
1508 pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
1509 bind_lvl = TcM.topIdLvl dfun_id
1510
1511 pprEq :: TcType -> TcType -> SDoc
1512 pprEq ty1 ty2 = pprParendType ty1 <+> char '~' <+> pprParendType ty2
1513
1514 isTouchableMetaTyVarTcS :: TcTyVar -> TcS Bool
1515 isTouchableMetaTyVarTcS tv
1516 = do { tclvl <- getTcLevel
1517 ; return $ isTouchableMetaTyVar tclvl tv }
1518
1519 isFilledMetaTyVar_maybe :: TcTyVar -> TcS (Maybe Type)
1520 isFilledMetaTyVar_maybe tv
1521 = ASSERT2( isTcTyVar tv, ppr tv )
1522 case tcTyVarDetails tv of
1523 MetaTv { mtv_ref = ref }
1524 -> do { cts <- wrapTcS (TcM.readTcRef ref)
1525 ; case cts of
1526 Indirect ty -> return (Just ty)
1527 Flexi -> return Nothing }
1528 _ -> return Nothing
1529
1530 isFilledMetaTyVar :: TcTyVar -> TcS Bool
1531 isFilledMetaTyVar tv = wrapTcS (TcM.isFilledMetaTyVar tv)
1532
1533 zonkTyVarsAndFV :: TcTyVarSet -> TcS TcTyVarSet
1534 zonkTyVarsAndFV tvs = wrapTcS (TcM.zonkTyVarsAndFV tvs)
1535
1536 zonkTcType :: TcType -> TcS TcType
1537 zonkTcType ty = wrapTcS (TcM.zonkTcType ty)
1538
1539 zonkTcTyVar :: TcTyVar -> TcS TcType
1540 zonkTcTyVar tv = wrapTcS (TcM.zonkTcTyVar tv)
1541
1542 zonkSimples :: Cts -> TcS Cts
1543 zonkSimples cts = wrapTcS (TcM.zonkSimples cts)
1544
1545 {-
1546 Note [Do not add duplicate derived insolubles]
1547 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1548 In general we *must* add an insoluble (Int ~ Bool) even if there is
1549 one such there already, because they may come from distinct call
1550 sites. Not only do we want an error message for each, but with
1551 -fdefer-type-errors we must generate evidence for each. But for
1552 *derived* insolubles, we only want to report each one once. Why?
1553
1554 (a) A constraint (C r s t) where r -> s, say, may generate the same fundep
1555 equality many times, as the original constraint is sucessively rewritten.
1556
1557 (b) Ditto the successive iterations of the main solver itself, as it traverses
1558 the constraint tree. See example below.
1559
1560 Also for *given* insolubles we may get repeated errors, as we
1561 repeatedly traverse the constraint tree. These are relatively rare
1562 anyway, so removing duplicates seems ok. (Alternatively we could take
1563 the SrcLoc into account.)
1564
1565 Note that the test does not need to be particularly efficient because
1566 it is only used if the program has a type error anyway.
1567
1568 Example of (b): assume a top-level class and instance declaration:
1569
1570 class D a b | a -> b
1571 instance D [a] [a]
1572
1573 Assume we have started with an implication:
1574
1575 forall c. Eq c => { wc_simple = D [c] c [W] }
1576
1577 which we have simplified to:
1578
1579 forall c. Eq c => { wc_simple = D [c] c [W]
1580 , wc_insols = (c ~ [c]) [D] }
1581
1582 For some reason, e.g. because we floated an equality somewhere else,
1583 we might try to re-solve this implication. If we do not do a
1584 dropDerivedWC, then we will end up trying to solve the following
1585 constraints the second time:
1586
1587 (D [c] c) [W]
1588 (c ~ [c]) [D]
1589
1590 which will result in two Deriveds to end up in the insoluble set:
1591
1592 wc_simple = D [c] c [W]
1593 wc_insols = (c ~ [c]) [D], (c ~ [c]) [D]
1594 -}
1595
1596 -- Flatten skolems
1597 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1598 newFlattenSkolem :: CtFlavour -> CtLoc
1599 -> TcType -- F xis
1600 -> TcS (CtEvidence, TcTyVar) -- [W] x:: F xis ~ fsk
1601 newFlattenSkolem Given loc fam_ty
1602 = do { checkReductionDepth loc fam_ty
1603 ; fsk <- wrapTcS $
1604 do { uniq <- TcM.newUnique
1605 ; let name = TcM.mkTcTyVarName uniq (fsLit "fsk")
1606 ; return (mkTcTyVar name (typeKind fam_ty) (FlatSkol fam_ty)) }
1607 ; ev <- newGivenEvVar loc (mkTcEqPred fam_ty (mkTyVarTy fsk),
1608 EvCoercion (mkTcNomReflCo fam_ty))
1609 ; return (ev, fsk) }
1610
1611 newFlattenSkolem _ loc fam_ty -- Make a wanted
1612 = do { checkReductionDepth loc fam_ty
1613 ; fuv <- wrapTcS $
1614 do { uniq <- TcM.newUnique
1615 ; ref <- TcM.newMutVar Flexi
1616 ; let details = MetaTv { mtv_info = FlatMetaTv
1617 , mtv_ref = ref
1618 , mtv_tclvl = fskTcLevel }
1619 name = TcM.mkTcTyVarName uniq (fsLit "s")
1620 ; return (mkTcTyVar name (typeKind fam_ty) details) }
1621 ; ev <- newWantedEvVarNC loc (mkTcEqPred fam_ty (mkTyVarTy fuv))
1622 ; return (ev, fuv) }
1623
1624 extendFlatCache :: TyCon -> [Type] -> (TcCoercion, TcType, CtFlavour) -> TcS ()
1625 extendFlatCache tc xi_args stuff
1626 = do { dflags <- getDynFlags
1627 ; when (gopt Opt_FlatCache dflags) $
1628 updInertTcS $ \ is@(IS { inert_flat_cache = fc }) ->
1629 is { inert_flat_cache = insertFunEq fc tc xi_args stuff } }
1630
1631 -- Instantiations
1632 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1633
1634 instDFunType :: DFunId -> [DFunInstType] -> TcS ([TcType], TcThetaType)
1635 instDFunType dfun_id inst_tys
1636 = wrapTcS $ TcM.instDFunType dfun_id inst_tys
1637
1638 newFlexiTcSTy :: Kind -> TcS TcType
1639 newFlexiTcSTy knd = wrapTcS (TcM.newFlexiTyVarTy knd)
1640
1641 cloneMetaTyVar :: TcTyVar -> TcS TcTyVar
1642 cloneMetaTyVar tv = wrapTcS (TcM.cloneMetaTyVar tv)
1643
1644 demoteUnfilledFmv :: TcTyVar -> TcS ()
1645 -- If a flatten-meta-var is still un-filled,
1646 -- turn it into an ordinary meta-var
1647 demoteUnfilledFmv fmv
1648 = wrapTcS $ do { is_filled <- TcM.isFilledMetaTyVar fmv
1649 ; unless is_filled $
1650 do { tv_ty <- TcM.newFlexiTyVarTy (tyVarKind fmv)
1651 ; TcM.writeMetaTyVar fmv tv_ty } }
1652
1653 instFlexiTcS :: [TKVar] -> TcS (TvSubst, [TcType])
1654 instFlexiTcS tvs = wrapTcS (mapAccumLM inst_one emptyTvSubst tvs)
1655 where
1656 inst_one subst tv
1657 = do { ty' <- instFlexiTcSHelper (tyVarName tv)
1658 (substTy subst (tyVarKind tv))
1659 ; return (extendTvSubst subst tv ty', ty') }
1660
1661 instFlexiTcSHelper :: Name -> Kind -> TcM TcType
1662 instFlexiTcSHelper tvname kind
1663 = do { uniq <- TcM.newUnique
1664 ; details <- TcM.newMetaDetails (TauTv False)
1665 ; let name = setNameUnique tvname uniq
1666 ; return (mkTyVarTy (mkTcTyVar name kind details)) }
1667
1668 instFlexiTcSHelperTcS :: Name -> Kind -> TcS TcType
1669 instFlexiTcSHelperTcS n k = wrapTcS (instFlexiTcSHelper n k)
1670
1671
1672 -- Creating and setting evidence variables and CtFlavors
1673 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1674
1675 data Freshness = Fresh | Cached
1676
1677 isFresh :: Freshness -> Bool
1678 isFresh Fresh = True
1679 isFresh Cached = False
1680
1681 freshGoals :: [(CtEvidence, Freshness)] -> [CtEvidence]
1682 freshGoals mns = [ ctev | (ctev, Fresh) <- mns ]
1683
1684 setEvBind :: EvBind -> TcS ()
1685 setEvBind ev_bind
1686 = do { tc_evbinds <- getTcEvBinds
1687 ; wrapTcS $ TcM.addTcEvBind tc_evbinds ev_bind }
1688
1689 setWantedEvBind :: EvVar -> EvTerm -> TcS ()
1690 setWantedEvBind ev_id tm = setEvBind (mkWantedEvBind ev_id tm)
1691
1692 setEvBindIfWanted :: CtEvidence -> EvTerm -> TcS ()
1693 setEvBindIfWanted ev tm
1694 = case ev of
1695 CtWanted { ctev_evar = ev_id } -> setWantedEvBind ev_id tm
1696 _ -> return ()
1697
1698 newTcEvBinds :: TcS EvBindsVar
1699 newTcEvBinds = wrapTcS TcM.newTcEvBinds
1700
1701 newEvVar :: TcPredType -> TcS EvVar
1702 newEvVar pred = wrapTcS (TcM.newEvVar pred)
1703
1704 newGivenEvVar :: CtLoc -> (TcPredType, EvTerm) -> TcS CtEvidence
1705 -- Make a new variable of the given PredType,
1706 -- immediately bind it to the given term
1707 -- and return its CtEvidence
1708 -- See Note [Bind new Givens immediately] in TcRnTypes
1709 -- Precondition: this is not a kind equality
1710 -- See Note [Do not create Given kind equalities]
1711 newGivenEvVar loc (pred, rhs)
1712 = ASSERT2( not (isKindEquality pred), ppr pred $$ pprCtOrigin (ctLocOrigin loc) )
1713 do { checkReductionDepth loc pred
1714 ; new_ev <- newEvVar pred
1715 ; setEvBind (mkGivenEvBind new_ev rhs)
1716 ; return (CtGiven { ctev_pred = pred, ctev_evar = new_ev, ctev_loc = loc }) }
1717
1718 newGivenEvVars :: CtLoc -> [(TcPredType, EvTerm)] -> TcS [CtEvidence]
1719 -- Like newGivenEvVar, but automatically discard kind equalities
1720 -- See Note [Do not create Given kind equalities]
1721 newGivenEvVars loc pts = mapM (newGivenEvVar loc) (filterOut (isKindEquality . fst) pts)
1722
1723 isKindEquality :: TcPredType -> Bool
1724 -- See Note [Do not create Given kind equalities]
1725 isKindEquality pred = case classifyPredType pred of
1726 EqPred _ t1 _ -> isKind t1
1727 _ -> False
1728
1729 {- Note [Do not create Given kind equalities]
1730 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1731 We do not want to create a Given kind equality like
1732
1733 [G] kv ~ k -- kv is a skolem kind variable
1734 -- Reason we don't yet support non-Refl kind equalities
1735
1736 This showed up in Trac #8566, where we had a data type
1737 data I (u :: U *) (r :: [*]) :: * where
1738 A :: I (AA t as) r -- Existential k
1739 so A has type
1740 A :: forall (u:U *) (r:[*]) Universal
1741 (k:BOX) (t:k) (as:[U *]). Existential
1742 (u ~ AA * k t as) => I u r
1743
1744 There is no direct kind equality, but in a pattern match where 'u' is
1745 instantiated to, say, (AA * kk (t1:kk) as1), we'd decompose to get
1746 k ~ kk, t ~ t1, as ~ as1
1747 This is bad. We "fix" this by simply ignoring the Given kind equality
1748 But the Right Thing is to add kind equalities!
1749
1750 But note (Trac #8705) that we *do* create Given (non-canonical) equalities
1751 with un-equal kinds, e.g.
1752 [G] t1::k1 ~ t2::k2 -- k1 and k2 are un-equal kinds
1753 Reason: k1 or k2 might be unification variables that have already been
1754 unified (at this point we have not canonicalised the types), so we want
1755 to emit this t1~t2 as a (non-canonical) Given in the work-list. If k1/k2
1756 have been unified, we'll find that when we canonicalise it, and the
1757 t1~t2 information may be crucial (Trac #8705 is an example).
1758
1759 If it turns out that k1 and k2 are really un-equal, then it'll end up
1760 as an Irreducible (see Note [Equalities with incompatible kinds] in
1761 TcCanonical), and will do no harm.
1762 -}
1763
1764 newWantedEvVarNC :: CtLoc -> TcPredType -> TcS CtEvidence
1765 -- Don't look up in the solved/inerts; we know it's not there
1766 newWantedEvVarNC loc pty
1767 = do { checkReductionDepth loc pty
1768 ; new_ev <- newEvVar pty
1769 ; return (CtWanted { ctev_pred = pty, ctev_evar = new_ev, ctev_loc = loc })}
1770
1771 newWantedEvVar :: CtLoc -> TcPredType -> TcS (CtEvidence, Freshness)
1772 -- For anything except ClassPred, this is the same as newWantedEvVarNC
1773 newWantedEvVar loc pty
1774 = do { mb_ct <- lookupInInerts pty
1775 ; case mb_ct of
1776 Just ctev | not (isDerived ctev)
1777 -> do { traceTcS "newWantedEvVar/cache hit" $ ppr ctev
1778 ; return (ctev, Cached) }
1779 _ -> do { ctev <- newWantedEvVarNC loc pty
1780 ; traceTcS "newWantedEvVar/cache miss" $ ppr ctev
1781 ; return (ctev, Fresh) } }
1782
1783 emitNewDerived :: CtLoc -> TcPredType -> TcS ()
1784 -- Create new Derived and put it in the work list
1785 emitNewDerived loc pred
1786 = do { mb_ev <- newDerived loc pred
1787 ; case mb_ev of
1788 Nothing -> return ()
1789 Just ev -> do { traceTcS "Emitting [D]" (ppr ev)
1790 ; updWorkListTcS (extendWorkListCt (mkNonCanonical ev)) } }
1791
1792 newDerived :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence)
1793 -- Returns Nothing if cached,
1794 -- Just pred if not cached
1795 newDerived loc pred
1796 = do { checkReductionDepth loc pred
1797 ; mb_ct <- lookupInInerts pred
1798 ; return (case mb_ct of
1799 Just {} -> Nothing
1800 Nothing -> Just (CtDerived { ctev_pred = pred, ctev_loc = loc })) }
1801
1802 -- | Checks if the depth of the given location is too much. Fails if
1803 -- it's too big, with an appropriate error message.
1804 checkReductionDepth :: CtLoc -> TcType -- ^ type being reduced
1805 -> TcS ()
1806 checkReductionDepth loc ty
1807 = do { dflags <- getDynFlags
1808 ; when (subGoalDepthExceeded dflags (ctLocDepth loc)) $
1809 wrapErrTcS $
1810 solverDepthErrorTcS loc ty }
1811
1812 matchFam :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcType))
1813 matchFam tycon args = wrapTcS $ matchFamTcM tycon args
1814
1815 matchFamTcM :: TyCon -> [Type] -> TcM (Maybe (TcCoercion, TcType))
1816 -- Given (F tys) return (ty, co), where co :: F tys ~ ty
1817 matchFamTcM tycon args
1818 = do { fam_envs <- FamInst.tcGetFamInstEnvs
1819 ; return $ fmap (first TcCoercion) $
1820 reduceTyFamApp_maybe fam_envs Nominal tycon args }
1821
1822 {-
1823 Note [Residual implications]
1824 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1825 The wl_implics in the WorkList are the residual implication
1826 constraints that are generated while solving or canonicalising the
1827 current worklist. Specifically, when canonicalising
1828 (forall a. t1 ~ forall a. t2)
1829 from which we get the implication
1830 (forall a. t1 ~ t2)
1831 See TcSMonad.deferTcSForAllEq
1832 -}
1833
1834 -- Deferring forall equalities as implications
1835 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1836
1837 deferTcSForAllEq :: Role -- Nominal or Representational
1838 -> CtLoc -- Original wanted equality flavor
1839 -> ([TyVar],TcType) -- ForAll tvs1 body1
1840 -> ([TyVar],TcType) -- ForAll tvs2 body2
1841 -> TcS EvTerm
1842 -- Some of this functionality is repeated from TcUnify,
1843 -- consider having a single place where we create fresh implications.
1844 deferTcSForAllEq role loc (tvs1,body1) (tvs2,body2)
1845 = do { (subst1, skol_tvs) <- wrapTcS $ TcM.tcInstSkolTyVars tvs1
1846 ; let tys = mkTyVarTys skol_tvs
1847 phi1 = Type.substTy subst1 body1
1848 phi2 = Type.substTy (zipTopTvSubst tvs2 tys) body2
1849 skol_info = UnifyForAllSkol skol_tvs phi1
1850 eq_pred = case role of
1851 Nominal -> mkTcEqPred phi1 phi2
1852 Representational -> mkCoerciblePred phi1 phi2
1853 Phantom -> panic "deferTcSForAllEq Phantom"
1854 ; (ctev, freshness) <- newWantedEvVar loc eq_pred
1855 ; coe_inside <- case freshness of
1856 Cached -> return (ctEvCoercion ctev)
1857 Fresh -> do { ev_binds_var <- newTcEvBinds
1858 ; env <- wrapTcS $ TcM.getLclEnv
1859 ; let ev_binds = TcEvBinds ev_binds_var
1860 new_ct = mkNonCanonical ctev
1861 new_co = ctEvCoercion ctev
1862 new_tclvl = pushTcLevel (tcl_tclvl env)
1863 ; let wc = WC { wc_simple = singleCt new_ct
1864 , wc_impl = emptyBag
1865 , wc_insol = emptyCts }
1866 imp = Implic { ic_tclvl = new_tclvl
1867 , ic_skols = skol_tvs
1868 , ic_no_eqs = True
1869 , ic_given = []
1870 , ic_wanted = wc
1871 , ic_status = IC_Unsolved
1872 , ic_binds = ev_binds_var
1873 , ic_env = env
1874 , ic_info = skol_info }
1875 ; updWorkListTcS (extendWorkListImplic imp)
1876 ; return (TcLetCo ev_binds new_co) }
1877
1878 ; return $ EvCoercion (foldr mkTcForAllCo coe_inside skol_tvs) }
1879