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