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