never executed always true always false
1 {-# LANGUAGE CPP #-}
2 {-# LANGUAGE DeriveFunctor #-}
3 {-# LANGUAGE DerivingStrategies #-}
4 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
5 {-# LANGUAGE MultiWayIf #-}
6 {-# LANGUAGE ScopedTypeVariables #-}
7 {-# LANGUAGE TypeFamilies #-}
8 {-# LANGUAGE ViewPatterns #-}
9
10 {-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
11
12 -- | Monadic definitions for the constraint solver
13 module GHC.Tc.Solver.Monad (
14
15 -- The TcS monad
16 TcS, runTcS, runTcSDeriveds, runTcSDerivedsEarlyAbort, runTcSWithEvBinds,
17 runTcSInerts, failTcS, warnTcS, addErrTcS, wrapTcS, runTcSEqualities,
18 nestTcS, nestImplicTcS, setEvBindsTcS,
19 emitImplicationTcS, emitTvImplicationTcS,
20
21 selectNextWorkItem,
22 getWorkList,
23 updWorkListTcS,
24 pushLevelNoWorkList,
25
26 runTcPluginTcS, addUsedGRE, addUsedGREs, keepAlive,
27 matchGlobalInst, TcM.ClsInstResult(..),
28
29 QCInst(..),
30
31 -- Tracing etc
32 panicTcS, traceTcS,
33 traceFireTcS, bumpStepCountTcS, csTraceTcS,
34 wrapErrTcS, wrapWarnTcS,
35 resetUnificationFlag, setUnificationFlag,
36
37 -- Evidence creation and transformation
38 MaybeNew(..), freshGoals, isFresh, getEvExpr,
39
40 newTcEvBinds, newNoTcEvBinds,
41 newWantedEq, newWantedEq_SI, emitNewWantedEq,
42 newWanted, newWanted_SI, newWantedEvVar,
43 newWantedNC, newWantedEvVarNC,
44 newDerivedNC,
45 newBoundEvVarId,
46 unifyTyVar, reportUnifications, touchabilityTest, TouchabilityTestResult(..),
47 setEvBind, setWantedEq,
48 setWantedEvTerm, setEvBindIfWanted,
49 newEvVar, newGivenEvVar, newGivenEvVars,
50 emitNewDeriveds, emitNewDerivedEq,
51 checkReductionDepth,
52 getSolvedDicts, setSolvedDicts,
53
54 getInstEnvs, getFamInstEnvs, -- Getting the environments
55 getTopEnv, getGblEnv, getLclEnv,
56 getTcEvBindsVar, getTcLevel,
57 getTcEvTyCoVars, getTcEvBindsMap, setTcEvBindsMap,
58 tcLookupClass, tcLookupId,
59
60 -- Inerts
61 updInertTcS, updInertCans, updInertDicts, updInertIrreds,
62 getHasGivenEqs, setInertCans,
63 getInertEqs, getInertCans, getInertGivens,
64 getInertInsols, getInnermostGivenEqLevel,
65 getTcSInerts, setTcSInerts,
66 getUnsolvedInerts,
67 removeInertCts, getPendingGivenScs,
68 addInertCan, insertFunEq, addInertForAll,
69 emitWorkNC, emitWork,
70 isImprovable,
71 lookupInertDict,
72
73 -- The Model
74 kickOutAfterUnification,
75
76 -- Inert Safe Haskell safe-overlap failures
77 addInertSafehask, insertSafeOverlapFailureTcS, updInertSafehask,
78 getSafeOverlapFailures,
79
80 -- Inert solved dictionaries
81 addSolvedDict, lookupSolvedDict,
82
83 -- Irreds
84 foldIrreds,
85
86 -- The family application cache
87 lookupFamAppInert, lookupFamAppCache, extendFamAppCache,
88 pprKicked,
89
90 instDFunType, -- Instantiation
91
92 -- MetaTyVars
93 newFlexiTcSTy, instFlexi, instFlexiX,
94 cloneMetaTyVar,
95 tcInstSkolTyVarsX,
96
97 TcLevel,
98 isFilledMetaTyVar_maybe, isFilledMetaTyVar,
99 zonkTyCoVarsAndFV, zonkTcType, zonkTcTypes, zonkTcTyVar, zonkCo,
100 zonkTyCoVarsAndFVList,
101 zonkSimples, zonkWC,
102 zonkTyCoVarKind,
103
104 -- References
105 newTcRef, readTcRef, writeTcRef, updTcRef,
106
107 -- Misc
108 getDefaultInfo, getDynFlags, getGlobalRdrEnvTcS,
109 matchFam, matchFamTcM,
110 checkWellStagedDFun,
111 pprEq, -- Smaller utils, re-exported from TcM
112 -- TODO (DV): these are only really used in the
113 -- instance matcher in GHC.Tc.Solver. I am wondering
114 -- if the whole instance matcher simply belongs
115 -- here
116
117 breakTyVarCycle_maybe, rewriterView
118 ) where
119
120 import GHC.Prelude
121
122 import GHC.Driver.Env
123
124 import qualified GHC.Tc.Utils.Instantiate as TcM
125 import GHC.Core.InstEnv
126 import GHC.Tc.Instance.Family as FamInst
127 import GHC.Core.FamInstEnv
128
129 import qualified GHC.Tc.Utils.Monad as TcM
130 import qualified GHC.Tc.Utils.TcMType as TcM
131 import qualified GHC.Tc.Instance.Class as TcM( matchGlobalInst, ClsInstResult(..) )
132 import qualified GHC.Tc.Utils.Env as TcM
133 ( checkWellStaged, tcGetDefaultTys, tcLookupClass, tcLookupId, topIdLvl )
134 import GHC.Tc.Instance.Class( InstanceWhat(..), safeOverlap, instanceReturnsDictCon )
135 import GHC.Tc.Utils.TcType
136 import GHC.Driver.Session
137 import GHC.Core.Type
138 import qualified GHC.Core.TyCo.Rep as Rep -- this needs to be used only very locally
139 import GHC.Core.Coercion
140 import GHC.Core.Reduction
141
142 import GHC.Tc.Solver.Types
143 import GHC.Tc.Solver.InertSet
144
145 import GHC.Tc.Types.Evidence
146 import GHC.Core.Class
147 import GHC.Core.TyCon
148 import GHC.Tc.Errors ( solverDepthErrorTcS )
149 import GHC.Tc.Errors.Types
150
151 import GHC.Types.Name
152 import GHC.Types.TyThing
153 import GHC.Unit.Module ( HasModule, getModule )
154 import GHC.Types.Name.Reader ( GlobalRdrEnv, GlobalRdrElt )
155 import qualified GHC.Rename.Env as TcM
156 import GHC.Types.Var
157 import GHC.Types.Var.Env
158 import GHC.Types.Var.Set
159 import GHC.Utils.Outputable
160 import GHC.Utils.Panic
161 import GHC.Utils.Logger
162 import GHC.Utils.Misc (HasDebugCallStack)
163 import GHC.Data.Bag as Bag
164 import GHC.Types.Unique.Supply
165 import GHC.Tc.Types
166 import GHC.Tc.Types.Origin
167 import GHC.Tc.Types.Constraint
168 import GHC.Tc.Utils.Unify
169 import GHC.Core.Predicate
170
171 import GHC.Types.Unique.Set
172
173 import Control.Monad
174 import GHC.Utils.Monad
175 import Data.IORef
176 import GHC.Exts (oneShot)
177 import Data.List ( mapAccumL, partition )
178 import Data.List.NonEmpty ( NonEmpty(..) )
179
180 #if defined(DEBUG)
181 import GHC.Data.Graph.Directed
182 #endif
183
184 {- *********************************************************************
185 * *
186 Shadow constraints and improvement
187 * *
188 ************************************************************************
189
190 Note [The improvement story and derived shadows]
191 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
192 Because Wanteds cannot rewrite Wanteds (see Note [Wanteds do not
193 rewrite Wanteds] in GHC.Tc.Types.Constraint), we may miss some opportunities for
194 solving. Here's a classic example (indexed-types/should_fail/T4093a)
195
196 Ambiguity check for f: (Foo e ~ Maybe e) => Foo e
197
198 We get [G] Foo e ~ Maybe e (CEqCan)
199 [W] Foo ee ~ Foo e (CEqCan) -- ee is a unification variable
200 [W] Foo ee ~ Maybe ee (CEqCan)
201
202 The first Wanted gets rewritten to
203
204 [W] Foo ee ~ Maybe e
205
206 But now we appear to be stuck, since we don't rewrite Wanteds with
207 Wanteds. This is silly because we can see that ee := e is the
208 only solution.
209
210 The basic plan is
211 * generate Derived constraints that shadow Wanted constraints
212 * allow Derived to rewrite Derived
213 * in order to cause some unifications to take place
214 * that in turn solve the original Wanteds
215
216 The ONLY reason for all these Derived equalities is to tell us how to
217 unify a variable: that is, what Mark Jones calls "improvement".
218
219 The same idea is sometimes also called "saturation"; find all the
220 equalities that must hold in any solution.
221
222 Or, equivalently, you can think of the derived shadows as implementing
223 the "model": a non-idempotent but no-occurs-check substitution,
224 reflecting *all* *Nominal* equalities (a ~N ty) that are not
225 immediately soluble by unification.
226
227 More specifically, here's how it works (Oct 16):
228
229 * Wanted constraints are born as [WD]; this behaves like a
230 [W] and a [D] paired together.
231
232 * When we are about to add a [WD] to the inert set, if it can
233 be rewritten by a [D] a ~ ty, then we split it into [W] and [D],
234 putting the latter into the work list (see maybeEmitShadow).
235
236 In the example above, we get to the point where we are stuck:
237 [WD] Foo ee ~ Foo e
238 [WD] Foo ee ~ Maybe ee
239
240 But now when [WD] Foo ee ~ Maybe ee is about to be added, we'll
241 split it into [W] and [D], since the inert [WD] Foo ee ~ Foo e
242 can rewrite it. Then:
243 work item: [D] Foo ee ~ Maybe ee
244 inert: [W] Foo ee ~ Maybe ee
245 [WD] Foo ee ~ Maybe e
246
247 See Note [Splitting WD constraints]. Now the work item is rewritten
248 by the [WD] and we soon get ee := e.
249
250 Additional notes:
251
252 * The derived shadow equalities live in inert_eqs, along with
253 the Givens and Wanteds; see Note [EqualCtList invariants]
254 in GHC.Tc.Solver.Types.
255
256 * We make Derived shadows only for Wanteds, not Givens. So we
257 have only [G], not [GD] and [G] plus splitting. See
258 Note [Add derived shadows only for Wanteds]
259
260 * We also get Derived equalities from functional dependencies
261 and type-function injectivity; see calls to unifyDerived.
262
263 * It's worth having [WD] rather than just [W] and [D] because
264 * efficiency: silly to process the same thing twice
265 * inert_dicts is a finite map keyed by
266 the type; it's inconvenient for it to map to TWO constraints
267
268 Another example requiring Deriveds is in
269 Note [Put touchable variables on the left] in GHC.Tc.Solver.Canonical.
270
271 Note [Splitting WD constraints]
272 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
273 We are about to add a [WD] constraint to the inert set; and we
274 know that the inert set has fully rewritten it. Should we split
275 it into [W] and [D], and put the [D] in the work list for further
276 work?
277
278 * CDictCan (C tys):
279 Yes if the inert set could rewrite tys to make the class constraint,
280 or type family, fire. That is, yes if the inert_eqs intersects
281 with the free vars of tys. For this test we use
282 (anyRewritableTyVar True) which ignores casts and coercions in tys,
283 because rewriting the casts or coercions won't make the thing fire
284 more often.
285
286 * CEqCan (lhs ~ ty): Yes if the inert set could rewrite 'lhs' or 'ty'.
287 We need to check both 'lhs' and 'ty' against the inert set:
288 - Inert set contains [D] a ~ ty2
289 Then we want to put [D] a ~ ty in the worklist, so we'll
290 get [D] ty ~ ty2 with consequent good things
291
292 - Inert set contains [D] b ~ a, where b is in ty.
293 We can't just add [WD] a ~ ty[b] to the inert set, because
294 that breaks the inert-set invariants. If we tried to
295 canonicalise another [D] constraint mentioning 'a', we'd
296 get an infinite loop
297
298 Moreover we must use (anyRewritableTyVar False) for the RHS,
299 because even tyvars in the casts and coercions could give
300 an infinite loop if we don't expose it
301
302 * CIrredCan: Yes if the inert set can rewrite the constraint.
303 We used to think splitting irreds was unnecessary, but
304 see Note [Splitting Irred WD constraints]
305
306 * Others: nothing is gained by splitting.
307
308 Note [Splitting Irred WD constraints]
309 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
310 Splitting Irred constraints can make a difference. Here is the
311 scenario:
312
313 a[sk] :: F v -- F is a type family
314 beta :: alpha
315
316 work item: [WD] a ~ beta
317
318 This is heterogeneous, so we emit a kind equality and make the work item an
319 inert Irred.
320
321 work item: [D] F v ~ alpha
322 inert: [WD] (a |> co) ~ beta (CIrredCan)
323
324 Can't make progress on the work item. Add to inert set. This kicks out the
325 old inert, because a [D] can rewrite a [WD].
326
327 work item: [WD] (a |> co) ~ beta
328 inert: [D] F v ~ alpha (CEqCan)
329
330 Can't make progress on this work item either (although GHC tries by
331 decomposing the cast and rewriting... but that doesn't make a difference),
332 which is still hetero. Emit a new kind equality and add to inert set. But,
333 critically, we split the Irred.
334
335 work list:
336 [D] F v ~ alpha (CEqCan)
337 [D] (a |> co) ~ beta (CIrred) -- this one was split off
338 inert:
339 [W] (a |> co) ~ beta
340 [D] F v ~ alpha
341
342 We quickly solve the first work item, as it's the same as an inert.
343
344 work item: [D] (a |> co) ~ beta
345 inert:
346 [W] (a |> co) ~ beta
347 [D] F v ~ alpha
348
349 We decompose the cast, yielding
350
351 [D] a ~ beta
352
353 We then rewrite the kinds. The lhs kind is F v, which flattens to alpha.
354
355 co' :: F v ~ alpha
356 [D] (a |> co') ~ beta
357
358 Now this equality is homo-kinded. So we swizzle it around to
359
360 [D] beta ~ (a |> co')
361
362 and set beta := a |> co', and go home happy.
363
364 If we don't split the Irreds, we loop. This is all dangerously subtle.
365
366 This is triggered by test case typecheck/should_compile/SplitWD.
367
368 Note [Add derived shadows only for Wanteds]
369 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
370 We only add shadows for Wanted constraints. That is, we have
371 [WD] but not [GD]; and maybeEmitShaodw looks only at [WD]
372 constraints.
373
374 It does just possibly make sense ot add a derived shadow for a
375 Given. If we created a Derived shadow of a Given, it could be
376 rewritten by other Deriveds, and that could, conceivably, lead to a
377 useful unification.
378
379 But (a) I have been unable to come up with an example of this
380 happening
381 (b) see #12660 for how adding the derived shadows
382 of a Given led to an infinite loop.
383 (c) It's unlikely that rewriting derived Givens will lead
384 to a unification because Givens don't mention touchable
385 unification variables
386
387 For (b) there may be other ways to solve the loop, but simply
388 reraining from adding derived shadows of Givens is particularly
389 simple. And it's more efficient too!
390
391 Still, here's one possible reason for adding derived shadows
392 for Givens. Consider
393 work-item [G] a ~ [b], inerts has [D] b ~ a.
394 If we added the derived shadow (into the work list)
395 [D] a ~ [b]
396 When we process it, we'll rewrite to a ~ [a] and get an
397 occurs check. Without it we'll miss the occurs check (reporting
398 inaccessible code); but that's probably OK.
399
400 Note [Keep CDictCan shadows as CDictCan]
401 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
402 Suppose we have
403 class C a => D a b
404 and [G] D a b, [G] C a in the inert set. Now we insert
405 [D] b ~ c. We want to kick out a derived shadow for [D] D a b,
406 so we can rewrite it with the new constraint, and perhaps get
407 instance reduction or other consequences.
408
409 BUT we do not want to kick out a *non-canonical* (D a b). If we
410 did, we would do this:
411 - rewrite it to [D] D a c, with pend_sc = True
412 - use expandSuperClasses to add C a
413 - go round again, which solves C a from the givens
414 This loop goes on for ever and triggers the simpl_loop limit.
415
416 Solution: kick out the CDictCan which will have pend_sc = False,
417 because we've already added its superclasses. So we won't re-add
418 them. If we forget the pend_sc flag, our cunning scheme for avoiding
419 generating superclasses repeatedly will fail.
420
421 See #11379 for a case of this.
422
423 Note [Do not do improvement for WOnly]
424 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
425 We do improvement between two constraints (e.g. for injectivity
426 or functional dependencies) only if both are "improvable". And
427 we improve a constraint wrt the top-level instances only if
428 it is improvable.
429
430 Improvable: [G] [WD] [D}
431 Not improvable: [W]
432
433 Reasons:
434
435 * It's less work: fewer pairs to compare
436
437 * Every [W] has a shadow [D] so nothing is lost
438
439 * Consider [WD] C Int b, where 'b' is a skolem, and
440 class C a b | a -> b
441 instance C Int Bool
442 We'll do a fundep on it and emit [D] b ~ Bool
443 That will kick out constraint [WD] C Int b
444 Then we'll split it to [W] C Int b (keep in inert)
445 and [D] C Int b (in work list)
446 When processing the latter we'll rewrite it to
447 [D] C Int Bool
448 At that point it would be /stupid/ to interact it
449 with the inert [W] C Int b in the inert set; after all,
450 it's the very constraint from which the [D] C Int Bool
451 was split! We can avoid this by not doing improvement
452 on [W] constraints. This came up in #12860.
453 -}
454
455 maybeEmitShadow :: InertCans -> Ct -> TcS Ct
456 -- See Note [The improvement story and derived shadows]
457 maybeEmitShadow ics ct
458 | let ev = ctEvidence ct
459 , CtWanted { ctev_pred = pred, ctev_loc = loc
460 , ctev_nosh = WDeriv } <- ev
461 , shouldSplitWD (inert_eqs ics) (inert_funeqs ics) ct
462 = do { traceTcS "Emit derived shadow" (ppr ct)
463 ; let derived_ev = CtDerived { ctev_pred = pred
464 , ctev_loc = loc }
465 shadow_ct = ct { cc_ev = derived_ev }
466 -- Te shadow constraint keeps the canonical shape.
467 -- This just saves work, but is sometimes important;
468 -- see Note [Keep CDictCan shadows as CDictCan]
469 ; emitWork [shadow_ct]
470
471 ; let ev' = ev { ctev_nosh = WOnly }
472 ct' = ct { cc_ev = ev' }
473 -- Record that it now has a shadow
474 -- This is /the/ place we set the flag to WOnly
475 ; return ct' }
476
477 | otherwise
478 = return ct
479
480 shouldSplitWD :: InertEqs -> FunEqMap EqualCtList -> Ct -> Bool
481 -- Precondition: 'ct' is [WD], and is inert
482 -- True <=> we should split ct ito [W] and [D] because
483 -- the inert_eqs can make progress on the [D]
484 -- See Note [Splitting WD constraints]
485
486 shouldSplitWD inert_eqs fun_eqs (CDictCan { cc_tyargs = tys })
487 = should_split_match_args inert_eqs fun_eqs tys
488 -- NB True: ignore coercions
489 -- See Note [Splitting WD constraints]
490
491 shouldSplitWD inert_eqs fun_eqs (CEqCan { cc_lhs = TyVarLHS tv, cc_rhs = ty
492 , cc_eq_rel = eq_rel })
493 = tv `elemDVarEnv` inert_eqs
494 || anyRewritableCanEqLHS eq_rel (canRewriteTv inert_eqs) (canRewriteTyFam fun_eqs) ty
495 -- NB False: do not ignore casts and coercions
496 -- See Note [Splitting WD constraints]
497
498 shouldSplitWD inert_eqs fun_eqs (CEqCan { cc_ev = ev, cc_eq_rel = eq_rel })
499 = anyRewritableCanEqLHS eq_rel (canRewriteTv inert_eqs) (canRewriteTyFam fun_eqs)
500 (ctEvPred ev)
501
502 shouldSplitWD inert_eqs fun_eqs (CIrredCan { cc_ev = ev })
503 = anyRewritableCanEqLHS (ctEvEqRel ev) (canRewriteTv inert_eqs)
504 (canRewriteTyFam fun_eqs) (ctEvPred ev)
505
506 shouldSplitWD _ _ _ = False -- No point in splitting otherwise
507
508 should_split_match_args :: InertEqs -> FunEqMap EqualCtList -> [TcType] -> Bool
509 -- True if the inert_eqs can rewrite anything in the argument types
510 should_split_match_args inert_eqs fun_eqs tys
511 = any (anyRewritableCanEqLHS NomEq (canRewriteTv inert_eqs) (canRewriteTyFam fun_eqs)) tys
512 -- See Note [Splitting WD constraints]
513
514 canRewriteTv :: InertEqs -> EqRel -> TyVar -> Bool
515 canRewriteTv inert_eqs eq_rel tv
516 | Just (EqualCtList (ct :| _)) <- lookupDVarEnv inert_eqs tv
517 , CEqCan { cc_eq_rel = eq_rel1 } <- ct
518 = eq_rel1 `eqCanRewrite` eq_rel
519 | otherwise
520 = False
521
522 canRewriteTyFam :: FunEqMap EqualCtList -> EqRel -> TyCon -> [Type] -> Bool
523 canRewriteTyFam fun_eqs eq_rel tf args
524 | Just (EqualCtList (ct :| _)) <- findFunEq fun_eqs tf args
525 , CEqCan { cc_eq_rel = eq_rel1 } <- ct
526 = eq_rel1 `eqCanRewrite` eq_rel
527 | otherwise
528 = False
529
530 isImprovable :: CtEvidence -> Bool
531 -- See Note [Do not do improvement for WOnly]
532 isImprovable (CtWanted { ctev_nosh = WOnly }) = False
533 isImprovable _ = True
534
535
536 {- *********************************************************************
537 * *
538 Inert instances: inert_insts
539 * *
540 ********************************************************************* -}
541
542 addInertForAll :: QCInst -> TcS ()
543 -- Add a local Given instance, typically arising from a type signature
544 addInertForAll new_qci
545 = do { ics <- getInertCans
546 ; ics1 <- add_qci ics
547
548 -- Update given equalities. C.f updateGivenEqs
549 ; tclvl <- getTcLevel
550 ; let pred = qci_pred new_qci
551 not_equality = isClassPred pred && not (isEqPred pred)
552 -- True <=> definitely not an equality
553 -- A qci_pred like (f a) might be an equality
554
555 ics2 | not_equality = ics1
556 | otherwise = ics1 { inert_given_eq_lvl = tclvl
557 , inert_given_eqs = True }
558
559 ; setInertCans ics2 }
560 where
561 add_qci :: InertCans -> TcS InertCans
562 -- See Note [Do not add duplicate quantified instances]
563 add_qci ics@(IC { inert_insts = qcis })
564 | any same_qci qcis
565 = do { traceTcS "skipping duplicate quantified instance" (ppr new_qci)
566 ; return ics }
567
568 | otherwise
569 = do { traceTcS "adding new inert quantified instance" (ppr new_qci)
570 ; return (ics { inert_insts = new_qci : qcis }) }
571
572 same_qci old_qci = tcEqType (ctEvPred (qci_ev old_qci))
573 (ctEvPred (qci_ev new_qci))
574
575 {- Note [Do not add duplicate quantified instances]
576 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
577 Consider this (#15244):
578
579 f :: (C g, D g) => ....
580 class S g => C g where ...
581 class S g => D g where ...
582 class (forall a. Eq a => Eq (g a)) => S g where ...
583
584 Then in f's RHS there are two identical quantified constraints
585 available, one via the superclasses of C and one via the superclasses
586 of D. The two are identical, and it seems wrong to reject the program
587 because of that. But without doing duplicate-elimination we will have
588 two matching QCInsts when we try to solve constraints arising from f's
589 RHS.
590
591 The simplest thing is simply to eliminate duplicates, which we do here.
592 -}
593
594 {- *********************************************************************
595 * *
596 Adding an inert
597 * *
598 ************************************************************************
599
600 Note [Adding an equality to the InertCans]
601 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
602 When adding an equality to the inerts:
603
604 * Split [WD] into [W] and [D] if the inerts can rewrite the latter;
605 done by maybeEmitShadow.
606
607 * Kick out any constraints that can be rewritten by the thing
608 we are adding. Done by kickOutRewritable.
609
610 * Note that unifying a:=ty, is like adding [G] a~ty; just use
611 kickOutRewritable with Nominal, Given. See kickOutAfterUnification.
612 -}
613
614 addInertCan :: Ct -> TcS ()
615 -- Precondition: item /is/ canonical
616 -- See Note [Adding an equality to the InertCans]
617 addInertCan ct =
618 do { traceTcS "addInertCan {" $
619 text "Trying to insert new inert item:" <+> ppr ct
620 ; mkTcS (\TcSEnv{tcs_abort_on_insoluble=abort_flag} ->
621 when (abort_flag && insolubleEqCt ct) TcM.failM)
622 ; ics <- getInertCans
623 ; ct <- maybeEmitShadow ics ct
624 ; ics <- maybeKickOut ics ct
625 ; tclvl <- getTcLevel
626 ; setInertCans (addInertItem tclvl ics ct)
627
628 ; traceTcS "addInertCan }" $ empty }
629
630 maybeKickOut :: InertCans -> Ct -> TcS InertCans
631 -- For a CEqCan, kick out any inert that can be rewritten by the CEqCan
632 maybeKickOut ics ct
633 | CEqCan { cc_lhs = lhs, cc_ev = ev, cc_eq_rel = eq_rel } <- ct
634 = do { (_, ics') <- kickOutRewritable (ctEvFlavour ev, eq_rel) lhs ics
635 ; return ics' }
636 | otherwise
637 = return ics
638
639 -----------------------------------------
640 kickOutRewritable :: CtFlavourRole -- Flavour/role of the equality that
641 -- is being added to the inert set
642 -> CanEqLHS -- The new equality is lhs ~ ty
643 -> InertCans
644 -> TcS (Int, InertCans)
645 kickOutRewritable new_fr new_lhs ics
646 = do { let (kicked_out, ics') = kickOutRewritableLHS new_fr new_lhs ics
647 n_kicked = workListSize kicked_out
648
649 ; unless (n_kicked == 0) $
650 do { updWorkListTcS (appendWorkList kicked_out)
651
652 -- The famapp-cache contains Given evidence from the inert set.
653 -- If we're kicking out Givens, we need to remove this evidence
654 -- from the cache, too.
655 ; let kicked_given_ev_vars =
656 [ ev_var | ct <- wl_eqs kicked_out
657 , CtGiven { ctev_evar = ev_var } <- [ctEvidence ct] ]
658 ; when (new_fr `eqCanRewriteFR` (Given, NomEq) &&
659 -- if this isn't true, no use looking through the constraints
660 not (null kicked_given_ev_vars)) $
661 do { traceTcS "Given(s) have been kicked out; drop from famapp-cache"
662 (ppr kicked_given_ev_vars)
663 ; dropFromFamAppCache (mkVarSet kicked_given_ev_vars) }
664
665 ; csTraceTcS $
666 hang (text "Kick out, lhs =" <+> ppr new_lhs)
667 2 (vcat [ text "n-kicked =" <+> int n_kicked
668 , text "kicked_out =" <+> ppr kicked_out
669 , text "Residual inerts =" <+> ppr ics' ]) }
670
671 ; return (n_kicked, ics') }
672
673 kickOutAfterUnification :: TcTyVar -> TcS Int
674 kickOutAfterUnification new_tv
675 = do { ics <- getInertCans
676 ; (n_kicked, ics2) <- kickOutRewritable (Given,NomEq)
677 (TyVarLHS new_tv) ics
678 -- Given because the tv := xi is given; NomEq because
679 -- only nominal equalities are solved by unification
680
681 ; setInertCans ics2
682 ; return n_kicked }
683
684 -- See Wrinkle (2) in Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Canonical
685 kickOutAfterFillingCoercionHole :: CoercionHole -> Coercion -> TcS ()
686 kickOutAfterFillingCoercionHole hole filled_co
687 = do { ics <- getInertCans
688 ; let (kicked_out, ics') = kick_out ics
689 n_kicked = workListSize kicked_out
690
691 ; unless (n_kicked == 0) $
692 do { updWorkListTcS (appendWorkList kicked_out)
693 ; csTraceTcS $
694 hang (text "Kick out, hole =" <+> ppr hole)
695 2 (vcat [ text "n-kicked =" <+> int n_kicked
696 , text "kicked_out =" <+> ppr kicked_out
697 , text "Residual inerts =" <+> ppr ics' ]) }
698
699 ; setInertCans ics' }
700 where
701 holes_of_co = coercionHolesOfCo filled_co
702
703 kick_out :: InertCans -> (WorkList, InertCans)
704 kick_out ics@(IC { inert_blocked = blocked })
705 = let (to_kick, to_keep) = partitionBagWith kick_ct blocked
706
707 kicked_out = extendWorkListCts (bagToList to_kick) emptyWorkList
708 ics' = ics { inert_blocked = to_keep }
709 in
710 (kicked_out, ics')
711
712 kick_ct :: Ct -> Either Ct Ct
713 -- Left: kick out; Right: keep. But even if we keep, we may need
714 -- to update the set of blocking holes
715 kick_ct ct@(CIrredCan { cc_reason = HoleBlockerReason holes })
716 | hole `elementOfUniqSet` holes
717 = let new_holes = holes `delOneFromUniqSet` hole
718 `unionUniqSets` holes_of_co
719 updated_ct = ct { cc_reason = HoleBlockerReason new_holes }
720 in
721 if isEmptyUniqSet new_holes
722 then Left updated_ct
723 else Right updated_ct
724
725 | otherwise
726 = Right ct
727
728 kick_ct other = pprPanic "kickOutAfterFillingCoercionHole" (ppr other)
729
730 --------------
731 addInertSafehask :: InertCans -> Ct -> InertCans
732 addInertSafehask ics item@(CDictCan { cc_class = cls, cc_tyargs = tys })
733 = ics { inert_safehask = addDictCt (inert_dicts ics) (classTyCon cls) tys item }
734
735 addInertSafehask _ item
736 = pprPanic "addInertSafehask: can't happen! Inserting " $ ppr item
737
738 insertSafeOverlapFailureTcS :: InstanceWhat -> Ct -> TcS ()
739 -- See Note [Safe Haskell Overlapping Instances Implementation] in GHC.Tc.Solver
740 insertSafeOverlapFailureTcS what item
741 | safeOverlap what = return ()
742 | otherwise = updInertCans (\ics -> addInertSafehask ics item)
743
744 getSafeOverlapFailures :: TcS Cts
745 -- See Note [Safe Haskell Overlapping Instances Implementation] in GHC.Tc.Solver
746 getSafeOverlapFailures
747 = do { IC { inert_safehask = safehask } <- getInertCans
748 ; return $ foldDicts consCts safehask emptyCts }
749
750 --------------
751 addSolvedDict :: InstanceWhat -> CtEvidence -> Class -> [Type] -> TcS ()
752 -- Conditionally add a new item in the solved set of the monad
753 -- See Note [Solved dictionaries] in GHC.Tc.Solver.InertSet
754 addSolvedDict what item cls tys
755 | isWanted item
756 , instanceReturnsDictCon what
757 = do { traceTcS "updSolvedSetTcs:" $ ppr item
758 ; updInertTcS $ \ ics ->
759 ics { inert_solved_dicts = addDict (inert_solved_dicts ics) cls tys item } }
760 | otherwise
761 = return ()
762
763 getSolvedDicts :: TcS (DictMap CtEvidence)
764 getSolvedDicts = do { ics <- getTcSInerts; return (inert_solved_dicts ics) }
765
766 setSolvedDicts :: DictMap CtEvidence -> TcS ()
767 setSolvedDicts solved_dicts
768 = updInertTcS $ \ ics ->
769 ics { inert_solved_dicts = solved_dicts }
770
771 {- *********************************************************************
772 * *
773 Other inert-set operations
774 * *
775 ********************************************************************* -}
776
777 updInertTcS :: (InertSet -> InertSet) -> TcS ()
778 -- Modify the inert set with the supplied function
779 updInertTcS upd_fn
780 = do { is_var <- getTcSInertsRef
781 ; wrapTcS (do { curr_inert <- TcM.readTcRef is_var
782 ; TcM.writeTcRef is_var (upd_fn curr_inert) }) }
783
784 getInertCans :: TcS InertCans
785 getInertCans = do { inerts <- getTcSInerts; return (inert_cans inerts) }
786
787 setInertCans :: InertCans -> TcS ()
788 setInertCans ics = updInertTcS $ \ inerts -> inerts { inert_cans = ics }
789
790 updRetInertCans :: (InertCans -> (a, InertCans)) -> TcS a
791 -- Modify the inert set with the supplied function
792 updRetInertCans upd_fn
793 = do { is_var <- getTcSInertsRef
794 ; wrapTcS (do { inerts <- TcM.readTcRef is_var
795 ; let (res, cans') = upd_fn (inert_cans inerts)
796 ; TcM.writeTcRef is_var (inerts { inert_cans = cans' })
797 ; return res }) }
798
799 updInertCans :: (InertCans -> InertCans) -> TcS ()
800 -- Modify the inert set with the supplied function
801 updInertCans upd_fn
802 = updInertTcS $ \ inerts -> inerts { inert_cans = upd_fn (inert_cans inerts) }
803
804 updInertDicts :: (DictMap Ct -> DictMap Ct) -> TcS ()
805 -- Modify the inert set with the supplied function
806 updInertDicts upd_fn
807 = updInertCans $ \ ics -> ics { inert_dicts = upd_fn (inert_dicts ics) }
808
809 updInertSafehask :: (DictMap Ct -> DictMap Ct) -> TcS ()
810 -- Modify the inert set with the supplied function
811 updInertSafehask upd_fn
812 = updInertCans $ \ ics -> ics { inert_safehask = upd_fn (inert_safehask ics) }
813
814 updInertIrreds :: (Cts -> Cts) -> TcS ()
815 -- Modify the inert set with the supplied function
816 updInertIrreds upd_fn
817 = updInertCans $ \ ics -> ics { inert_irreds = upd_fn (inert_irreds ics) }
818
819 getInertEqs :: TcS (DTyVarEnv EqualCtList)
820 getInertEqs = do { inert <- getInertCans; return (inert_eqs inert) }
821
822 getInnermostGivenEqLevel :: TcS TcLevel
823 getInnermostGivenEqLevel = do { inert <- getInertCans
824 ; return (inert_given_eq_lvl inert) }
825
826 getInertInsols :: TcS Cts
827 -- Returns insoluble equality constraints and TypeError constraints,
828 -- specifically including Givens.
829 --
830 -- Note that this function only inspects irreducible constraints;
831 -- a DictCan constraint such as 'Eq (TypeError msg)' is not
832 -- considered to be an insoluble constraint by this function.
833 --
834 -- See Note [Pattern match warnings with insoluble Givens] in GHC.Tc.Solver.
835 getInertInsols = do { inert <- getInertCans
836 ; return $ filterBag insolubleCt (inert_irreds inert) }
837
838 getInertGivens :: TcS [Ct]
839 -- Returns the Given constraints in the inert set
840 getInertGivens
841 = do { inerts <- getInertCans
842 ; let all_cts = foldDicts (:) (inert_dicts inerts)
843 $ foldFunEqs (\ecl out -> equalCtListToList ecl ++ out)
844 (inert_funeqs inerts)
845 $ concatMap equalCtListToList (dVarEnvElts (inert_eqs inerts))
846 ; return (filter isGivenCt all_cts) }
847
848 getPendingGivenScs :: TcS [Ct]
849 -- Find all inert Given dictionaries, or quantified constraints,
850 -- whose cc_pend_sc flag is True
851 -- and that belong to the current level
852 -- Set their cc_pend_sc flag to False in the inert set, and return that Ct
853 getPendingGivenScs = do { lvl <- getTcLevel
854 ; updRetInertCans (get_sc_pending lvl) }
855
856 get_sc_pending :: TcLevel -> InertCans -> ([Ct], InertCans)
857 get_sc_pending this_lvl ic@(IC { inert_dicts = dicts, inert_insts = insts })
858 = assertPpr (all isGivenCt sc_pending) (ppr sc_pending)
859 -- When getPendingScDics is called,
860 -- there are never any Wanteds in the inert set
861 (sc_pending, ic { inert_dicts = dicts', inert_insts = insts' })
862 where
863 sc_pending = sc_pend_insts ++ sc_pend_dicts
864
865 sc_pend_dicts = foldDicts get_pending dicts []
866 dicts' = foldr add dicts sc_pend_dicts
867
868 (sc_pend_insts, insts') = mapAccumL get_pending_inst [] insts
869
870 get_pending :: Ct -> [Ct] -> [Ct] -- Get dicts with cc_pend_sc = True
871 -- but flipping the flag
872 get_pending dict dicts
873 | Just dict' <- isPendingScDict dict
874 , belongs_to_this_level (ctEvidence dict)
875 = dict' : dicts
876 | otherwise
877 = dicts
878
879 add :: Ct -> DictMap Ct -> DictMap Ct
880 add ct@(CDictCan { cc_class = cls, cc_tyargs = tys }) dicts
881 = addDictCt dicts (classTyCon cls) tys ct
882 add ct _ = pprPanic "getPendingScDicts" (ppr ct)
883
884 get_pending_inst :: [Ct] -> QCInst -> ([Ct], QCInst)
885 get_pending_inst cts qci@(QCI { qci_ev = ev })
886 | Just qci' <- isPendingScInst qci
887 , belongs_to_this_level ev
888 = (CQuantCan qci' : cts, qci')
889 | otherwise
890 = (cts, qci)
891
892 belongs_to_this_level ev = ctLocLevel (ctEvLoc ev) == this_lvl
893 -- We only want Givens from this level; see (3a) in
894 -- Note [The superclass story] in GHC.Tc.Solver.Canonical
895
896 getUnsolvedInerts :: TcS ( Bag Implication
897 , Cts ) -- All simple constraints
898 -- Return all the unsolved [Wanted] or [Derived] constraints
899 --
900 -- Post-condition: the returned simple constraints are all fully zonked
901 -- (because they come from the inert set)
902 -- the unsolved implics may not be
903 getUnsolvedInerts
904 = do { IC { inert_eqs = tv_eqs
905 , inert_funeqs = fun_eqs
906 , inert_irreds = irreds
907 , inert_blocked = blocked
908 , inert_dicts = idicts
909 } <- getInertCans
910
911 ; let unsolved_tv_eqs = foldTyEqs add_if_unsolved tv_eqs emptyCts
912 unsolved_fun_eqs = foldFunEqs add_if_unsolveds fun_eqs emptyCts
913 unsolved_irreds = Bag.filterBag is_unsolved irreds
914 unsolved_blocked = blocked -- all blocked equalities are W/D
915 unsolved_dicts = foldDicts add_if_unsolved idicts emptyCts
916 unsolved_others = unionManyBags [ unsolved_irreds
917 , unsolved_dicts
918 , unsolved_blocked ]
919
920 ; implics <- getWorkListImplics
921
922 ; traceTcS "getUnsolvedInerts" $
923 vcat [ text " tv eqs =" <+> ppr unsolved_tv_eqs
924 , text "fun eqs =" <+> ppr unsolved_fun_eqs
925 , text "others =" <+> ppr unsolved_others
926 , text "implics =" <+> ppr implics ]
927
928 ; return ( implics, unsolved_tv_eqs `unionBags`
929 unsolved_fun_eqs `unionBags`
930 unsolved_others) }
931 where
932 add_if_unsolved :: Ct -> Cts -> Cts
933 add_if_unsolved ct cts | is_unsolved ct = ct `consCts` cts
934 | otherwise = cts
935
936 add_if_unsolveds :: EqualCtList -> Cts -> Cts
937 add_if_unsolveds new_cts old_cts = foldr add_if_unsolved old_cts
938 (equalCtListToList new_cts)
939
940 is_unsolved ct = not (isGivenCt ct) -- Wanted or Derived
941
942 getHasGivenEqs :: TcLevel -- TcLevel of this implication
943 -> TcS ( HasGivenEqs -- are there Given equalities?
944 , Cts ) -- Insoluble equalities arising from givens
945 -- See Note [Tracking Given equalities] in GHC.Tc.Solver.InertSet
946 getHasGivenEqs tclvl
947 = do { inerts@(IC { inert_irreds = irreds
948 , inert_given_eqs = given_eqs
949 , inert_given_eq_lvl = ge_lvl })
950 <- getInertCans
951 ; let insols = filterBag insolubleEqCt irreds
952 -- Specifically includes ones that originated in some
953 -- outer context but were refined to an insoluble by
954 -- a local equality; so do /not/ add ct_given_here.
955
956 -- See Note [HasGivenEqs] in GHC.Tc.Types.Constraint, and
957 -- Note [Tracking Given equalities] in GHC.Tc.Solver.InertSet
958 has_ge | ge_lvl == tclvl = MaybeGivenEqs
959 | given_eqs = LocalGivenEqs
960 | otherwise = NoGivenEqs
961
962 ; traceTcS "getHasGivenEqs" $
963 vcat [ text "given_eqs:" <+> ppr given_eqs
964 , text "ge_lvl:" <+> ppr ge_lvl
965 , text "ambient level:" <+> ppr tclvl
966 , text "Inerts:" <+> ppr inerts
967 , text "Insols:" <+> ppr insols]
968 ; return (has_ge, insols) }
969
970 {- Note [Unsolved Derived equalities]
971 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
972 In getUnsolvedInerts, we return a derived equality from the inert_eqs
973 because it is a candidate for floating out of this implication. We
974 only float equalities with a meta-tyvar on the left, so we only pull
975 those out here.
976
977 Note [What might equal later?]
978 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
979 We must determine whether a Given might later equal a Wanted. We
980 definitely need to account for the possibility that any metavariable
981 might be arbitrarily instantiated. Yet we do *not* want
982 to allow skolems in to be instantiated, as we've already rewritten
983 with respect to any Givens. (We're solving a Wanted here, and so
984 all Givens have already been processed.)
985
986 This is best understood by example.
987
988 1. C alpha ~? C Int
989
990 That given certainly might match later.
991
992 2. C a ~? C Int
993
994 No. No new givens are going to arise that will get the `a` to rewrite
995 to Int.
996
997 3. C alpha[tv] ~? C Int
998
999 That alpha[tv] is a TyVarTv, unifiable only with other type variables.
1000 It cannot equal later.
1001
1002 4. C (F alpha) ~? C Int
1003
1004 Sure -- that can equal later, if we learn something useful about alpha.
1005
1006 5. C (F alpha[tv]) ~? C Int
1007
1008 This, too, might equal later. Perhaps we have [G] F b ~ Int elsewhere.
1009 Or maybe we have C (F alpha[tv] beta[tv]), these unify with each other,
1010 and F x x = Int. Remember: returning True doesn't commit ourselves to
1011 anything.
1012
1013 6. C (F a) ~? C a
1014
1015 No, this won't match later. If we could rewrite (F a) or a, we would
1016 have by now.
1017
1018 7. C (Maybe alpha) ~? C alpha
1019
1020 We say this cannot equal later, because it would require
1021 alpha := Maybe (Maybe (Maybe ...)). While such a type can be contrived,
1022 we choose not to worry about it. See Note [Infinitary substitution in lookup]
1023 in GHC.Core.InstEnv. Getting this wrong let to #19107, tested in
1024 typecheck/should_compile/T19107.
1025
1026 8. C cbv ~? C Int
1027 where cbv = F a
1028
1029 The cbv is a cycle-breaker var which stands for F a. See
1030 Note [Type variable cycles] in GHC.Tc.Solver.Canonical.
1031 This is just like case 6, and we say "no". Saying "no" here is
1032 essential in getting the parser to type-check, with its use of DisambECP.
1033
1034 9. C cbv ~? C Int
1035 where cbv = F alpha
1036
1037 Here, we might indeed equal later. Distinguishing between
1038 this case and Example 8 is why we need the InertSet in mightEqualLater.
1039
1040 10. C (F alpha, Int) ~? C (Bool, F alpha)
1041
1042 This cannot equal later, because F a would have to equal both Bool and
1043 Int.
1044
1045 To deal with type family applications, we use the Core flattener. See
1046 Note [Flattening type-family applications when matching instances] in GHC.Core.Unify.
1047 The Core flattener replaces all type family applications with
1048 fresh variables. The next question: should we allow these fresh
1049 variables in the domain of a unifying substitution?
1050
1051 A type family application that mentions only skolems (example 6) is settled:
1052 any skolems would have been rewritten w.r.t. Givens by now. These type family
1053 applications match only themselves. A type family application that mentions
1054 metavariables, on the other hand, can match anything. So, if the original type
1055 family application contains a metavariable, we use BindMe to tell the unifier
1056 to allow it in the substitution. On the other hand, a type family application
1057 with only skolems is considered rigid.
1058
1059 This treatment fixes #18910 and is tested in
1060 typecheck/should_compile/InstanceGivenOverlap{,2}
1061 -}
1062
1063 removeInertCts :: [Ct] -> InertCans -> InertCans
1064 -- ^ Remove inert constraints from the 'InertCans', for use when a
1065 -- typechecker plugin wishes to discard a given.
1066 removeInertCts cts icans = foldl' removeInertCt icans cts
1067
1068 removeInertCt :: InertCans -> Ct -> InertCans
1069 removeInertCt is ct =
1070 case ct of
1071
1072 CDictCan { cc_class = cl, cc_tyargs = tys } ->
1073 is { inert_dicts = delDict (inert_dicts is) cl tys }
1074
1075 CEqCan { cc_lhs = lhs, cc_rhs = rhs } -> delEq is lhs rhs
1076
1077 CQuantCan {} -> panic "removeInertCt: CQuantCan"
1078 CIrredCan {} -> panic "removeInertCt: CIrredEvCan"
1079 CNonCanonical {} -> panic "removeInertCt: CNonCanonical"
1080 CSpecialCan _ special_pred _ ->
1081 pprPanic "removeInertCt" (ppr "CSpecialCan" <+> parens (ppr special_pred))
1082
1083 -- | Looks up a family application in the inerts.
1084 lookupFamAppInert :: TyCon -> [Type] -> TcS (Maybe (Reduction, CtFlavourRole))
1085 lookupFamAppInert fam_tc tys
1086 = do { IS { inert_cans = IC { inert_funeqs = inert_funeqs } } <- getTcSInerts
1087 ; return (lookup_inerts inert_funeqs) }
1088 where
1089 lookup_inerts inert_funeqs
1090 | Just (EqualCtList (CEqCan { cc_ev = ctev, cc_rhs = rhs } :| _))
1091 <- findFunEq inert_funeqs fam_tc tys
1092 = Just (mkReduction (ctEvCoercion ctev) rhs
1093 ,ctEvFlavourRole ctev)
1094 | otherwise = Nothing
1095
1096 lookupInInerts :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence)
1097 -- Is this exact predicate type cached in the solved or canonicals of the InertSet?
1098 lookupInInerts loc pty
1099 | ClassPred cls tys <- classifyPredType pty
1100 = do { inerts <- getTcSInerts
1101 ; return (lookupSolvedDict inerts loc cls tys `mplus`
1102 fmap ctEvidence (lookupInertDict (inert_cans inerts) loc cls tys)) }
1103 | otherwise -- NB: No caching for equalities, IPs, holes, or errors
1104 = return Nothing
1105
1106 -- | Look up a dictionary inert.
1107 lookupInertDict :: InertCans -> CtLoc -> Class -> [Type] -> Maybe Ct
1108 lookupInertDict (IC { inert_dicts = dicts }) loc cls tys
1109 = case findDict dicts loc cls tys of
1110 Just ct -> Just ct
1111 _ -> Nothing
1112
1113 -- | Look up a solved inert.
1114 lookupSolvedDict :: InertSet -> CtLoc -> Class -> [Type] -> Maybe CtEvidence
1115 -- Returns just if exactly this predicate type exists in the solved.
1116 lookupSolvedDict (IS { inert_solved_dicts = solved }) loc cls tys
1117 = case findDict solved loc cls tys of
1118 Just ev -> Just ev
1119 _ -> Nothing
1120
1121 ---------------------------
1122 lookupFamAppCache :: TyCon -> [Type] -> TcS (Maybe Reduction)
1123 lookupFamAppCache fam_tc tys
1124 = do { IS { inert_famapp_cache = famapp_cache } <- getTcSInerts
1125 ; case findFunEq famapp_cache fam_tc tys of
1126 result@(Just redn) ->
1127 do { traceTcS "famapp_cache hit" (vcat [ ppr (mkTyConApp fam_tc tys)
1128 , ppr redn ])
1129 ; return result }
1130 Nothing -> return Nothing }
1131
1132 extendFamAppCache :: TyCon -> [Type] -> Reduction -> TcS ()
1133 -- NB: co :: rhs ~ F tys, to match expectations of rewriter
1134 extendFamAppCache tc xi_args stuff@(Reduction _ ty)
1135 = do { dflags <- getDynFlags
1136 ; when (gopt Opt_FamAppCache dflags) $
1137 do { traceTcS "extendFamAppCache" (vcat [ ppr tc <+> ppr xi_args
1138 , ppr ty ])
1139 -- 'co' can be bottom, in the case of derived items
1140 ; updInertTcS $ \ is@(IS { inert_famapp_cache = fc }) ->
1141 is { inert_famapp_cache = insertFunEq fc tc xi_args stuff } } }
1142
1143 -- Remove entries from the cache whose evidence mentions variables in the
1144 -- supplied set
1145 dropFromFamAppCache :: VarSet -> TcS ()
1146 dropFromFamAppCache varset
1147 = do { inerts@(IS { inert_famapp_cache = famapp_cache }) <- getTcSInerts
1148 ; let filtered = filterTcAppMap check famapp_cache
1149 ; setTcSInerts $ inerts { inert_famapp_cache = filtered } }
1150 where
1151 check :: Reduction -> Bool
1152 check redn
1153 = not (anyFreeVarsOfCo (`elemVarSet` varset) $ reductionCoercion redn)
1154
1155 {- *********************************************************************
1156 * *
1157 Irreds
1158 * *
1159 ********************************************************************* -}
1160
1161 foldIrreds :: (Ct -> b -> b) -> Cts -> b -> b
1162 foldIrreds k irreds z = foldr k z irreds
1163
1164 {-
1165 ************************************************************************
1166 * *
1167 * The TcS solver monad *
1168 * *
1169 ************************************************************************
1170
1171 Note [The TcS monad]
1172 ~~~~~~~~~~~~~~~~~~~~
1173 The TcS monad is a weak form of the main Tc monad
1174
1175 All you can do is
1176 * fail
1177 * allocate new variables
1178 * fill in evidence variables
1179
1180 Filling in a dictionary evidence variable means to create a binding
1181 for it, so TcS carries a mutable location where the binding can be
1182 added. This is initialised from the innermost implication constraint.
1183 -}
1184
1185 data TcSEnv
1186 = TcSEnv {
1187 tcs_ev_binds :: EvBindsVar,
1188
1189 tcs_unified :: IORef Int,
1190 -- The number of unification variables we have filled
1191 -- The important thing is whether it is non-zero
1192
1193 tcs_unif_lvl :: IORef (Maybe TcLevel),
1194 -- The Unification Level Flag
1195 -- Outermost level at which we have unified a meta tyvar
1196 -- Starts at Nothing, then (Just i), then (Just j) where j<i
1197 -- See Note [The Unification Level Flag]
1198
1199 tcs_count :: IORef Int, -- Global step count
1200
1201 tcs_inerts :: IORef InertSet, -- Current inert set
1202
1203 -- Whether to throw an exception if we come across an insoluble constraint.
1204 -- Used to fail-fast when checking for hole-fits. See Note [Speeding up
1205 -- valid hole-fits].
1206 tcs_abort_on_insoluble :: Bool,
1207
1208 -- See Note [WorkList priorities] in GHC.Tc.Solver.InertSet
1209 tcs_worklist :: IORef WorkList -- Current worklist
1210 }
1211
1212 ---------------
1213 newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a } deriving (Functor)
1214
1215 -- | Smart constructor for 'TcS', as describe in Note [The one-shot state
1216 -- monad trick] in "GHC.Utils.Monad".
1217 mkTcS :: (TcSEnv -> TcM a) -> TcS a
1218 mkTcS f = TcS (oneShot f)
1219
1220 instance Applicative TcS where
1221 pure x = mkTcS $ \_ -> return x
1222 (<*>) = ap
1223
1224 instance Monad TcS where
1225 m >>= k = mkTcS $ \ebs -> do
1226 unTcS m ebs >>= (\r -> unTcS (k r) ebs)
1227
1228 instance MonadFail TcS where
1229 fail err = mkTcS $ \_ -> fail err
1230
1231 instance MonadUnique TcS where
1232 getUniqueSupplyM = wrapTcS getUniqueSupplyM
1233
1234 instance HasModule TcS where
1235 getModule = wrapTcS getModule
1236
1237 instance MonadThings TcS where
1238 lookupThing n = wrapTcS (lookupThing n)
1239
1240 -- Basic functionality
1241 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1242 wrapTcS :: TcM a -> TcS a
1243 -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
1244 -- and TcS is supposed to have limited functionality
1245 wrapTcS action = mkTcS $ \_env -> action -- a TcM action will not use the TcEvBinds
1246
1247 wrapErrTcS :: TcM a -> TcS a
1248 -- The thing wrapped should just fail
1249 -- There's no static check; it's up to the user
1250 -- Having a variant for each error message is too painful
1251 wrapErrTcS = wrapTcS
1252
1253 wrapWarnTcS :: TcM a -> TcS a
1254 -- The thing wrapped should just add a warning, or no-op
1255 -- There's no static check; it's up to the user
1256 wrapWarnTcS = wrapTcS
1257
1258 panicTcS :: SDoc -> TcS a
1259 failTcS :: TcRnMessage -> TcS a
1260 warnTcS, addErrTcS :: TcRnMessage -> TcS ()
1261 failTcS = wrapTcS . TcM.failWith
1262 warnTcS msg = wrapTcS (TcM.addDiagnostic msg)
1263 addErrTcS = wrapTcS . TcM.addErr
1264 panicTcS doc = pprPanic "GHC.Tc.Solver.Canonical" doc
1265
1266 traceTcS :: String -> SDoc -> TcS ()
1267 traceTcS herald doc = wrapTcS (TcM.traceTc herald doc)
1268 {-# INLINE traceTcS #-} -- see Note [INLINE conditional tracing utilities]
1269
1270 runTcPluginTcS :: TcPluginM a -> TcS a
1271 runTcPluginTcS = wrapTcS . runTcPluginM
1272
1273 instance HasDynFlags TcS where
1274 getDynFlags = wrapTcS getDynFlags
1275
1276 getGlobalRdrEnvTcS :: TcS GlobalRdrEnv
1277 getGlobalRdrEnvTcS = wrapTcS TcM.getGlobalRdrEnv
1278
1279 bumpStepCountTcS :: TcS ()
1280 bumpStepCountTcS = mkTcS $ \env ->
1281 do { let ref = tcs_count env
1282 ; n <- TcM.readTcRef ref
1283 ; TcM.writeTcRef ref (n+1) }
1284
1285 csTraceTcS :: SDoc -> TcS ()
1286 csTraceTcS doc
1287 = wrapTcS $ csTraceTcM (return doc)
1288 {-# INLINE csTraceTcS #-} -- see Note [INLINE conditional tracing utilities]
1289
1290 traceFireTcS :: CtEvidence -> SDoc -> TcS ()
1291 -- Dump a rule-firing trace
1292 traceFireTcS ev doc
1293 = mkTcS $ \env -> csTraceTcM $
1294 do { n <- TcM.readTcRef (tcs_count env)
1295 ; tclvl <- TcM.getTcLevel
1296 ; return (hang (text "Step" <+> int n
1297 <> brackets (text "l:" <> ppr tclvl <> comma <>
1298 text "d:" <> ppr (ctLocDepth (ctEvLoc ev)))
1299 <+> doc <> colon)
1300 4 (ppr ev)) }
1301 {-# INLINE traceFireTcS #-} -- see Note [INLINE conditional tracing utilities]
1302
1303 csTraceTcM :: TcM SDoc -> TcM ()
1304 -- Constraint-solver tracing, -ddump-cs-trace
1305 csTraceTcM mk_doc
1306 = do { logger <- getLogger
1307 ; when ( logHasDumpFlag logger Opt_D_dump_cs_trace
1308 || logHasDumpFlag logger Opt_D_dump_tc_trace)
1309 ( do { msg <- mk_doc
1310 ; TcM.dumpTcRn False
1311 Opt_D_dump_cs_trace
1312 "" FormatText
1313 msg }) }
1314 {-# INLINE csTraceTcM #-} -- see Note [INLINE conditional tracing utilities]
1315
1316 runTcS :: TcS a -- What to run
1317 -> TcM (a, EvBindMap)
1318 runTcS tcs
1319 = do { ev_binds_var <- TcM.newTcEvBinds
1320 ; res <- runTcSWithEvBinds ev_binds_var tcs
1321 ; ev_binds <- TcM.getTcEvBindsMap ev_binds_var
1322 ; return (res, ev_binds) }
1323
1324 -- | This variant of 'runTcS' will keep solving, even when only Deriveds
1325 -- are left around. It also doesn't return any evidence, as callers won't
1326 -- need it.
1327 runTcSDeriveds :: TcS a -> TcM a
1328 runTcSDeriveds tcs
1329 = do { ev_binds_var <- TcM.newTcEvBinds
1330 ; runTcSWithEvBinds ev_binds_var tcs }
1331
1332
1333 -- | This variant of 'runTcSDeriveds' will immediatley fail upon encountering an
1334 -- insoluble ct. See Note [Speeding up valid-hole fits]
1335 runTcSDerivedsEarlyAbort :: TcS a -> TcM a
1336 runTcSDerivedsEarlyAbort tcs
1337 = do { ev_binds_var <- TcM.newTcEvBinds
1338 ; runTcSWithEvBinds' True True ev_binds_var tcs }
1339
1340 -- | This can deal only with equality constraints.
1341 runTcSEqualities :: TcS a -> TcM a
1342 runTcSEqualities thing_inside
1343 = do { ev_binds_var <- TcM.newNoTcEvBinds
1344 ; runTcSWithEvBinds ev_binds_var thing_inside }
1345
1346 -- | A variant of 'runTcS' that takes and returns an 'InertSet' for
1347 -- later resumption of the 'TcS' session.
1348 runTcSInerts :: InertSet -> TcS a -> TcM (a, InertSet)
1349 runTcSInerts inerts tcs = do
1350 ev_binds_var <- TcM.newTcEvBinds
1351 runTcSWithEvBinds' False False ev_binds_var $ do
1352 setTcSInerts inerts
1353 a <- tcs
1354 new_inerts <- getTcSInerts
1355 return (a, new_inerts)
1356
1357 runTcSWithEvBinds :: EvBindsVar
1358 -> TcS a
1359 -> TcM a
1360 runTcSWithEvBinds = runTcSWithEvBinds' True False
1361
1362 runTcSWithEvBinds' :: Bool -- ^ Restore type variable cycles afterwards?
1363 -- Don't if you want to reuse the InertSet.
1364 -- See also Note [Type variable cycles]
1365 -- in GHC.Tc.Solver.Canonical
1366 -> Bool
1367 -> EvBindsVar
1368 -> TcS a
1369 -> TcM a
1370 runTcSWithEvBinds' restore_cycles abort_on_insoluble ev_binds_var tcs
1371 = do { unified_var <- TcM.newTcRef 0
1372 ; step_count <- TcM.newTcRef 0
1373 ; inert_var <- TcM.newTcRef emptyInert
1374 ; wl_var <- TcM.newTcRef emptyWorkList
1375 ; unif_lvl_var <- TcM.newTcRef Nothing
1376 ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
1377 , tcs_unified = unified_var
1378 , tcs_unif_lvl = unif_lvl_var
1379 , tcs_count = step_count
1380 , tcs_inerts = inert_var
1381 , tcs_abort_on_insoluble = abort_on_insoluble
1382 , tcs_worklist = wl_var }
1383
1384 -- Run the computation
1385 ; res <- unTcS tcs env
1386
1387 ; count <- TcM.readTcRef step_count
1388 ; when (count > 0) $
1389 csTraceTcM $ return (text "Constraint solver steps =" <+> int count)
1390
1391 ; when restore_cycles $
1392 do { inert_set <- TcM.readTcRef inert_var
1393 ; restoreTyVarCycles inert_set }
1394
1395 #if defined(DEBUG)
1396 ; ev_binds <- TcM.getTcEvBindsMap ev_binds_var
1397 ; checkForCyclicBinds ev_binds
1398 #endif
1399
1400 ; return res }
1401
1402 ----------------------------
1403 #if defined(DEBUG)
1404 checkForCyclicBinds :: EvBindMap -> TcM ()
1405 checkForCyclicBinds ev_binds_map
1406 | null cycles
1407 = return ()
1408 | null coercion_cycles
1409 = TcM.traceTc "Cycle in evidence binds" $ ppr cycles
1410 | otherwise
1411 = pprPanic "Cycle in coercion bindings" $ ppr coercion_cycles
1412 where
1413 ev_binds = evBindMapBinds ev_binds_map
1414
1415 cycles :: [[EvBind]]
1416 cycles = [c | CyclicSCC c <- stronglyConnCompFromEdgedVerticesUniq edges]
1417
1418 coercion_cycles = [c | c <- cycles, any is_co_bind c]
1419 is_co_bind (EvBind { eb_lhs = b }) = isEqPrimPred (varType b)
1420
1421 edges :: [ Node EvVar EvBind ]
1422 edges = [ DigraphNode bind bndr (nonDetEltsUniqSet (evVarsOfTerm rhs))
1423 | bind@(EvBind { eb_lhs = bndr, eb_rhs = rhs}) <- bagToList ev_binds ]
1424 -- It's OK to use nonDetEltsUFM here as
1425 -- stronglyConnCompFromEdgedVertices is still deterministic even
1426 -- if the edges are in nondeterministic order as explained in
1427 -- Note [Deterministic SCC] in GHC.Data.Graph.Directed.
1428 #endif
1429
1430 ----------------------------
1431 setEvBindsTcS :: EvBindsVar -> TcS a -> TcS a
1432 setEvBindsTcS ref (TcS thing_inside)
1433 = TcS $ \ env -> thing_inside (env { tcs_ev_binds = ref })
1434
1435 nestImplicTcS :: EvBindsVar
1436 -> TcLevel -> TcS a
1437 -> TcS a
1438 nestImplicTcS ref inner_tclvl (TcS thing_inside)
1439 = TcS $ \ TcSEnv { tcs_unified = unified_var
1440 , tcs_inerts = old_inert_var
1441 , tcs_count = count
1442 , tcs_unif_lvl = unif_lvl
1443 , tcs_abort_on_insoluble = abort_on_insoluble
1444 } ->
1445 do { inerts <- TcM.readTcRef old_inert_var
1446 ; let nest_inert = inerts { inert_cycle_breakers = []
1447 , inert_cans = (inert_cans inerts)
1448 { inert_given_eqs = False } }
1449 -- All other InertSet fields are inherited
1450 ; new_inert_var <- TcM.newTcRef nest_inert
1451 ; new_wl_var <- TcM.newTcRef emptyWorkList
1452 ; let nest_env = TcSEnv { tcs_count = count -- Inherited
1453 , tcs_unif_lvl = unif_lvl -- Inherited
1454 , tcs_ev_binds = ref
1455 , tcs_unified = unified_var
1456 , tcs_inerts = new_inert_var
1457 , tcs_abort_on_insoluble = abort_on_insoluble
1458 , tcs_worklist = new_wl_var }
1459 ; res <- TcM.setTcLevel inner_tclvl $
1460 thing_inside nest_env
1461
1462 ; out_inert_set <- TcM.readTcRef new_inert_var
1463 ; restoreTyVarCycles out_inert_set
1464
1465 #if defined(DEBUG)
1466 -- Perform a check that the thing_inside did not cause cycles
1467 ; ev_binds <- TcM.getTcEvBindsMap ref
1468 ; checkForCyclicBinds ev_binds
1469 #endif
1470 ; return res }
1471
1472 nestTcS :: TcS a -> TcS a
1473 -- Use the current untouchables, augmenting the current
1474 -- evidence bindings, and solved dictionaries
1475 -- But have no effect on the InertCans, or on the inert_famapp_cache
1476 -- (we want to inherit the latter from processing the Givens)
1477 nestTcS (TcS thing_inside)
1478 = TcS $ \ env@(TcSEnv { tcs_inerts = inerts_var }) ->
1479 do { inerts <- TcM.readTcRef inerts_var
1480 ; new_inert_var <- TcM.newTcRef inerts
1481 ; new_wl_var <- TcM.newTcRef emptyWorkList
1482 ; let nest_env = env { tcs_inerts = new_inert_var
1483 , tcs_worklist = new_wl_var }
1484
1485 ; res <- thing_inside nest_env
1486
1487 ; new_inerts <- TcM.readTcRef new_inert_var
1488
1489 -- we want to propagate the safe haskell failures
1490 ; let old_ic = inert_cans inerts
1491 new_ic = inert_cans new_inerts
1492 nxt_ic = old_ic { inert_safehask = inert_safehask new_ic }
1493
1494 ; TcM.writeTcRef inerts_var -- See Note [Propagate the solved dictionaries]
1495 (inerts { inert_solved_dicts = inert_solved_dicts new_inerts
1496 , inert_cans = nxt_ic })
1497
1498 ; return res }
1499
1500 emitImplicationTcS :: TcLevel -> SkolemInfo
1501 -> [TcTyVar] -- Skolems
1502 -> [EvVar] -- Givens
1503 -> Cts -- Wanteds
1504 -> TcS TcEvBinds
1505 -- Add an implication to the TcS monad work-list
1506 emitImplicationTcS new_tclvl skol_info skol_tvs givens wanteds
1507 = do { let wc = emptyWC { wc_simple = wanteds }
1508 ; imp <- wrapTcS $
1509 do { ev_binds_var <- TcM.newTcEvBinds
1510 ; imp <- TcM.newImplication
1511 ; return (imp { ic_tclvl = new_tclvl
1512 , ic_skols = skol_tvs
1513 , ic_given = givens
1514 , ic_wanted = wc
1515 , ic_binds = ev_binds_var
1516 , ic_info = skol_info }) }
1517
1518 ; emitImplication imp
1519 ; return (TcEvBinds (ic_binds imp)) }
1520
1521 emitTvImplicationTcS :: TcLevel -> SkolemInfo
1522 -> [TcTyVar] -- Skolems
1523 -> Cts -- Wanteds
1524 -> TcS ()
1525 -- Just like emitImplicationTcS but no givens and no bindings
1526 emitTvImplicationTcS new_tclvl skol_info skol_tvs wanteds
1527 = do { let wc = emptyWC { wc_simple = wanteds }
1528 ; imp <- wrapTcS $
1529 do { ev_binds_var <- TcM.newNoTcEvBinds
1530 ; imp <- TcM.newImplication
1531 ; return (imp { ic_tclvl = new_tclvl
1532 , ic_skols = skol_tvs
1533 , ic_wanted = wc
1534 , ic_binds = ev_binds_var
1535 , ic_info = skol_info }) }
1536
1537 ; emitImplication imp }
1538
1539
1540 {- Note [Propagate the solved dictionaries]
1541 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1542 It's really quite important that nestTcS does not discard the solved
1543 dictionaries from the thing_inside.
1544 Consider
1545 Eq [a]
1546 forall b. empty => Eq [a]
1547 We solve the simple (Eq [a]), under nestTcS, and then turn our attention to
1548 the implications. It's definitely fine to use the solved dictionaries on
1549 the inner implications, and it can make a significant performance difference
1550 if you do so.
1551 -}
1552
1553 -- Getters and setters of GHC.Tc.Utils.Env fields
1554 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1555
1556 -- Getter of inerts and worklist
1557 getTcSInertsRef :: TcS (IORef InertSet)
1558 getTcSInertsRef = TcS (return . tcs_inerts)
1559
1560 getTcSWorkListRef :: TcS (IORef WorkList)
1561 getTcSWorkListRef = TcS (return . tcs_worklist)
1562
1563 getTcSInerts :: TcS InertSet
1564 getTcSInerts = getTcSInertsRef >>= readTcRef
1565
1566 setTcSInerts :: InertSet -> TcS ()
1567 setTcSInerts ics = do { r <- getTcSInertsRef; writeTcRef r ics }
1568
1569 getWorkListImplics :: TcS (Bag Implication)
1570 getWorkListImplics
1571 = do { wl_var <- getTcSWorkListRef
1572 ; wl_curr <- readTcRef wl_var
1573 ; return (wl_implics wl_curr) }
1574
1575 pushLevelNoWorkList :: SDoc -> TcS a -> TcS (TcLevel, a)
1576 -- Push the level and run thing_inside
1577 -- However, thing_inside should not generate any work items
1578 #if defined(DEBUG)
1579 pushLevelNoWorkList err_doc (TcS thing_inside)
1580 = TcS (\env -> TcM.pushTcLevelM $
1581 thing_inside (env { tcs_worklist = wl_panic })
1582 )
1583 where
1584 wl_panic = pprPanic "GHC.Tc.Solver.Monad.buildImplication" err_doc
1585 -- This panic checks that the thing-inside
1586 -- does not emit any work-list constraints
1587 #else
1588 pushLevelNoWorkList _ (TcS thing_inside)
1589 = TcS (\env -> TcM.pushTcLevelM (thing_inside env)) -- Don't check
1590 #endif
1591
1592 updWorkListTcS :: (WorkList -> WorkList) -> TcS ()
1593 updWorkListTcS f
1594 = do { wl_var <- getTcSWorkListRef
1595 ; updTcRef wl_var f }
1596
1597 emitWorkNC :: [CtEvidence] -> TcS ()
1598 emitWorkNC evs
1599 | null evs
1600 = return ()
1601 | otherwise
1602 = emitWork (map mkNonCanonical evs)
1603
1604 emitWork :: [Ct] -> TcS ()
1605 emitWork [] = return () -- avoid printing, among other work
1606 emitWork cts
1607 = do { traceTcS "Emitting fresh work" (vcat (map ppr cts))
1608 ; updWorkListTcS (extendWorkListCts cts) }
1609
1610 emitImplication :: Implication -> TcS ()
1611 emitImplication implic
1612 = updWorkListTcS (extendWorkListImplic implic)
1613
1614 newTcRef :: a -> TcS (TcRef a)
1615 newTcRef x = wrapTcS (TcM.newTcRef x)
1616
1617 readTcRef :: TcRef a -> TcS a
1618 readTcRef ref = wrapTcS (TcM.readTcRef ref)
1619
1620 writeTcRef :: TcRef a -> a -> TcS ()
1621 writeTcRef ref val = wrapTcS (TcM.writeTcRef ref val)
1622
1623 updTcRef :: TcRef a -> (a->a) -> TcS ()
1624 updTcRef ref upd_fn = wrapTcS (TcM.updTcRef ref upd_fn)
1625
1626 getTcEvBindsVar :: TcS EvBindsVar
1627 getTcEvBindsVar = TcS (return . tcs_ev_binds)
1628
1629 getTcLevel :: TcS TcLevel
1630 getTcLevel = wrapTcS TcM.getTcLevel
1631
1632 getTcEvTyCoVars :: EvBindsVar -> TcS TyCoVarSet
1633 getTcEvTyCoVars ev_binds_var
1634 = wrapTcS $ TcM.getTcEvTyCoVars ev_binds_var
1635
1636 getTcEvBindsMap :: EvBindsVar -> TcS EvBindMap
1637 getTcEvBindsMap ev_binds_var
1638 = wrapTcS $ TcM.getTcEvBindsMap ev_binds_var
1639
1640 setTcEvBindsMap :: EvBindsVar -> EvBindMap -> TcS ()
1641 setTcEvBindsMap ev_binds_var binds
1642 = wrapTcS $ TcM.setTcEvBindsMap ev_binds_var binds
1643
1644 unifyTyVar :: TcTyVar -> TcType -> TcS ()
1645 -- Unify a meta-tyvar with a type
1646 -- We keep track of how many unifications have happened in tcs_unified,
1647 --
1648 -- We should never unify the same variable twice!
1649 unifyTyVar tv ty
1650 = assertPpr (isMetaTyVar tv) (ppr tv) $
1651 TcS $ \ env ->
1652 do { TcM.traceTc "unifyTyVar" (ppr tv <+> text ":=" <+> ppr ty)
1653 ; TcM.writeMetaTyVar tv ty
1654 ; TcM.updTcRef (tcs_unified env) (+1) }
1655
1656 reportUnifications :: TcS a -> TcS (Int, a)
1657 reportUnifications (TcS thing_inside)
1658 = TcS $ \ env ->
1659 do { inner_unified <- TcM.newTcRef 0
1660 ; res <- thing_inside (env { tcs_unified = inner_unified })
1661 ; n_unifs <- TcM.readTcRef inner_unified
1662 ; TcM.updTcRef (tcs_unified env) (+ n_unifs)
1663 ; return (n_unifs, res) }
1664
1665 data TouchabilityTestResult
1666 -- See Note [Solve by unification] in GHC.Tc.Solver.Interact
1667 -- which points out that having TouchableSameLevel is just an optimisation;
1668 -- we could manage with TouchableOuterLevel alone (suitably renamed)
1669 = TouchableSameLevel
1670 | TouchableOuterLevel [TcTyVar] -- Promote these
1671 TcLevel -- ..to this level
1672 | Untouchable
1673
1674 instance Outputable TouchabilityTestResult where
1675 ppr TouchableSameLevel = text "TouchableSameLevel"
1676 ppr (TouchableOuterLevel tvs lvl) = text "TouchableOuterLevel" <> parens (ppr lvl <+> ppr tvs)
1677 ppr Untouchable = text "Untouchable"
1678
1679 touchabilityTest :: CtFlavour -> TcTyVar -> TcType -> TcS TouchabilityTestResult
1680 -- This is the key test for untouchability:
1681 -- See Note [Unification preconditions] in GHC.Tc.Utils.Unify
1682 -- and Note [Solve by unification] in GHC.Tc.Solver.Interact
1683 touchabilityTest flav tv1 rhs
1684 | flav /= Given -- See Note [Do not unify Givens]
1685 , MetaTv { mtv_tclvl = tv_lvl, mtv_info = info } <- tcTyVarDetails tv1
1686 , canSolveByUnification info rhs
1687 = do { ambient_lvl <- getTcLevel
1688 ; given_eq_lvl <- getInnermostGivenEqLevel
1689
1690 ; if | tv_lvl `sameDepthAs` ambient_lvl
1691 -> return TouchableSameLevel
1692
1693 | tv_lvl `deeperThanOrSame` given_eq_lvl -- No intervening given equalities
1694 , all (does_not_escape tv_lvl) free_skols -- No skolem escapes
1695 -> return (TouchableOuterLevel free_metas tv_lvl)
1696
1697 | otherwise
1698 -> return Untouchable }
1699 | otherwise
1700 = return Untouchable
1701 where
1702 (free_metas, free_skols) = partition isPromotableMetaTyVar $
1703 nonDetEltsUniqSet $
1704 tyCoVarsOfType rhs
1705
1706 does_not_escape tv_lvl fv
1707 | isTyVar fv = tv_lvl `deeperThanOrSame` tcTyVarLevel fv
1708 | otherwise = True
1709 -- Coercion variables are not an escape risk
1710 -- If an implication binds a coercion variable, it'll have equalities,
1711 -- so the "intervening given equalities" test above will catch it
1712 -- Coercion holes get filled with coercions, so again no problem.
1713
1714 {- Note [Do not unify Givens]
1715 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1716 Consider this GADT match
1717 data T a where
1718 T1 :: T Int
1719 ...
1720
1721 f x = case x of
1722 T1 -> True
1723 ...
1724
1725 So we get f :: T alpha[1] -> beta[1]
1726 x :: T alpha[1]
1727 and from the T1 branch we get the implication
1728 forall[2] (alpha[1] ~ Int) => beta[1] ~ Bool
1729
1730 Now, clearly we don't want to unify alpha:=Int! Yet at the moment we
1731 process [G] alpha[1] ~ Int, we don't have any given-equalities in the
1732 inert set, and hence there are no given equalities to make alpha untouchable.
1733
1734 NB: if it were alpha[2] ~ Int, this argument wouldn't hold. But that
1735 never happens: invariant (GivenInv) in Note [TcLevel invariants]
1736 in GHC.Tc.Utils.TcType.
1737
1738 Simple solution: never unify in Givens!
1739 -}
1740
1741 getDefaultInfo :: TcS ([Type], (Bool, Bool))
1742 getDefaultInfo = wrapTcS TcM.tcGetDefaultTys
1743
1744 getWorkList :: TcS WorkList
1745 getWorkList = do { wl_var <- getTcSWorkListRef
1746 ; wrapTcS (TcM.readTcRef wl_var) }
1747
1748 selectNextWorkItem :: TcS (Maybe Ct)
1749 -- Pick which work item to do next
1750 -- See Note [Prioritise equalities]
1751 selectNextWorkItem
1752 = do { wl_var <- getTcSWorkListRef
1753 ; wl <- readTcRef wl_var
1754 ; case selectWorkItem wl of {
1755 Nothing -> return Nothing ;
1756 Just (ct, new_wl) ->
1757 do { -- checkReductionDepth (ctLoc ct) (ctPred ct)
1758 -- This is done by GHC.Tc.Solver.Interact.chooseInstance
1759 ; writeTcRef wl_var new_wl
1760 ; return (Just ct) } } }
1761
1762 -- Just get some environments needed for instance looking up and matching
1763 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1764
1765 getInstEnvs :: TcS InstEnvs
1766 getInstEnvs = wrapTcS $ TcM.tcGetInstEnvs
1767
1768 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv)
1769 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
1770
1771 getTopEnv :: TcS HscEnv
1772 getTopEnv = wrapTcS $ TcM.getTopEnv
1773
1774 getGblEnv :: TcS TcGblEnv
1775 getGblEnv = wrapTcS $ TcM.getGblEnv
1776
1777 getLclEnv :: TcS TcLclEnv
1778 getLclEnv = wrapTcS $ TcM.getLclEnv
1779
1780 tcLookupClass :: Name -> TcS Class
1781 tcLookupClass c = wrapTcS $ TcM.tcLookupClass c
1782
1783 tcLookupId :: Name -> TcS Id
1784 tcLookupId n = wrapTcS $ TcM.tcLookupId n
1785
1786 -- Setting names as used (used in the deriving of Coercible evidence)
1787 -- Too hackish to expose it to TcS? In that case somehow extract the used
1788 -- constructors from the result of solveInteract
1789 addUsedGREs :: [GlobalRdrElt] -> TcS ()
1790 addUsedGREs gres = wrapTcS $ TcM.addUsedGREs gres
1791
1792 addUsedGRE :: Bool -> GlobalRdrElt -> TcS ()
1793 addUsedGRE warn_if_deprec gre = wrapTcS $ TcM.addUsedGRE warn_if_deprec gre
1794
1795 keepAlive :: Name -> TcS ()
1796 keepAlive = wrapTcS . TcM.keepAlive
1797
1798 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
1799 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1800
1801 checkWellStagedDFun :: CtLoc -> InstanceWhat -> PredType -> TcS ()
1802 -- Check that we do not try to use an instance before it is available. E.g.
1803 -- instance Eq T where ...
1804 -- f x = $( ... (\(p::T) -> p == p)... )
1805 -- Here we can't use the equality function from the instance in the splice
1806
1807 checkWellStagedDFun loc what pred
1808 | TopLevInstance { iw_dfun_id = dfun_id } <- what
1809 , let bind_lvl = TcM.topIdLvl dfun_id
1810 , bind_lvl > impLevel
1811 = wrapTcS $ TcM.setCtLocM loc $
1812 do { use_stage <- TcM.getStage
1813 ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
1814
1815 | otherwise
1816 = return () -- Fast path for common case
1817 where
1818 pp_thing = text "instance for" <+> quotes (ppr pred)
1819
1820 pprEq :: TcType -> TcType -> SDoc
1821 pprEq ty1 ty2 = pprParendType ty1 <+> char '~' <+> pprParendType ty2
1822
1823 isFilledMetaTyVar_maybe :: TcTyVar -> TcS (Maybe Type)
1824 isFilledMetaTyVar_maybe tv = wrapTcS (TcM.isFilledMetaTyVar_maybe tv)
1825
1826 isFilledMetaTyVar :: TcTyVar -> TcS Bool
1827 isFilledMetaTyVar tv = wrapTcS (TcM.isFilledMetaTyVar tv)
1828
1829 zonkTyCoVarsAndFV :: TcTyCoVarSet -> TcS TcTyCoVarSet
1830 zonkTyCoVarsAndFV tvs = wrapTcS (TcM.zonkTyCoVarsAndFV tvs)
1831
1832 zonkTyCoVarsAndFVList :: [TcTyCoVar] -> TcS [TcTyCoVar]
1833 zonkTyCoVarsAndFVList tvs = wrapTcS (TcM.zonkTyCoVarsAndFVList tvs)
1834
1835 zonkCo :: Coercion -> TcS Coercion
1836 zonkCo = wrapTcS . TcM.zonkCo
1837
1838 zonkTcType :: TcType -> TcS TcType
1839 zonkTcType ty = wrapTcS (TcM.zonkTcType ty)
1840
1841 zonkTcTypes :: [TcType] -> TcS [TcType]
1842 zonkTcTypes tys = wrapTcS (TcM.zonkTcTypes tys)
1843
1844 zonkTcTyVar :: TcTyVar -> TcS TcType
1845 zonkTcTyVar tv = wrapTcS (TcM.zonkTcTyVar tv)
1846
1847 zonkSimples :: Cts -> TcS Cts
1848 zonkSimples cts = wrapTcS (TcM.zonkSimples cts)
1849
1850 zonkWC :: WantedConstraints -> TcS WantedConstraints
1851 zonkWC wc = wrapTcS (TcM.zonkWC wc)
1852
1853 zonkTyCoVarKind :: TcTyCoVar -> TcS TcTyCoVar
1854 zonkTyCoVarKind tv = wrapTcS (TcM.zonkTyCoVarKind tv)
1855
1856 ----------------------------
1857 pprKicked :: Int -> SDoc
1858 pprKicked 0 = empty
1859 pprKicked n = parens (int n <+> text "kicked out")
1860
1861 {- *********************************************************************
1862 * *
1863 * The Unification Level Flag *
1864 * *
1865 ********************************************************************* -}
1866
1867 {- Note [The Unification Level Flag]
1868 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1869 Consider a deep tree of implication constraints
1870 forall[1] a. -- Outer-implic
1871 C alpha[1] -- Simple
1872 forall[2] c. ....(C alpha[1]).... -- Implic-1
1873 forall[2] b. ....(alpha[1] ~ Int).... -- Implic-2
1874
1875 The (C alpha) is insoluble until we know alpha. We solve alpha
1876 by unifying alpha:=Int somewhere deep inside Implic-2. But then we
1877 must try to solve the Outer-implic all over again. This time we can
1878 solve (C alpha) both in Outer-implic, and nested inside Implic-1.
1879
1880 When should we iterate solving a level-n implication?
1881 Answer: if any unification of a tyvar at level n takes place
1882 in the ic_implics of that implication.
1883
1884 * What if a unification takes place at level n-1? Then don't iterate
1885 level n, because we'll iterate level n-1, and that will in turn iterate
1886 level n.
1887
1888 * What if a unification takes place at level n, in the ic_simples of
1889 level n? No need to track this, because the kick-out mechanism deals
1890 with it. (We can't drop kick-out in favour of iteration, because kick-out
1891 works for skolem-equalities, not just unifications.)
1892
1893 So the monad-global Unification Level Flag, kept in tcs_unif_lvl keeps
1894 track of
1895 - Whether any unifications at all have taken place (Nothing => no unifications)
1896 - If so, what is the outermost level that has seen a unification (Just lvl)
1897
1898 The iteration done in the simplify_loop/maybe_simplify_again loop in GHC.Tc.Solver.
1899
1900 It helpful not to iterate unless there is a chance of progress. #8474 is
1901 an example:
1902
1903 * There's a deeply-nested chain of implication constraints.
1904 ?x:alpha => ?y1:beta1 => ... ?yn:betan => [W] ?x:Int
1905
1906 * From the innermost one we get a [D] alpha[1] ~ Int,
1907 so we can unify.
1908
1909 * It's better not to iterate the inner implications, but go all the
1910 way out to level 1 before iterating -- because iterating level 1
1911 will iterate the inner levels anyway.
1912
1913 (In the olden days when we "floated" thse Derived constraints, this was
1914 much, much more important -- we got exponential behaviour, as each iteration
1915 produced the same Derived constraint.)
1916 -}
1917
1918
1919 resetUnificationFlag :: TcS Bool
1920 -- We are at ambient level i
1921 -- If the unification flag = Just i, reset it to Nothing and return True
1922 -- Otherwise leave it unchanged and return False
1923 resetUnificationFlag
1924 = TcS $ \env ->
1925 do { let ref = tcs_unif_lvl env
1926 ; ambient_lvl <- TcM.getTcLevel
1927 ; mb_lvl <- TcM.readTcRef ref
1928 ; TcM.traceTc "resetUnificationFlag" $
1929 vcat [ text "ambient:" <+> ppr ambient_lvl
1930 , text "unif_lvl:" <+> ppr mb_lvl ]
1931 ; case mb_lvl of
1932 Nothing -> return False
1933 Just unif_lvl | ambient_lvl `strictlyDeeperThan` unif_lvl
1934 -> return False
1935 | otherwise
1936 -> do { TcM.writeTcRef ref Nothing
1937 ; return True } }
1938
1939 setUnificationFlag :: TcLevel -> TcS ()
1940 -- (setUnificationFlag i) sets the unification level to (Just i)
1941 -- unless it already is (Just j) where j <= i
1942 setUnificationFlag lvl
1943 = TcS $ \env ->
1944 do { let ref = tcs_unif_lvl env
1945 ; mb_lvl <- TcM.readTcRef ref
1946 ; case mb_lvl of
1947 Just unif_lvl | lvl `deeperThanOrSame` unif_lvl
1948 -> return ()
1949 _ -> TcM.writeTcRef ref (Just lvl) }
1950
1951
1952 {- *********************************************************************
1953 * *
1954 * Instantiation etc.
1955 * *
1956 ********************************************************************* -}
1957
1958 -- Instantiations
1959 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1960
1961 instDFunType :: DFunId -> [DFunInstType] -> TcS ([TcType], TcThetaType)
1962 instDFunType dfun_id inst_tys
1963 = wrapTcS $ TcM.instDFunType dfun_id inst_tys
1964
1965 newFlexiTcSTy :: Kind -> TcS TcType
1966 newFlexiTcSTy knd = wrapTcS (TcM.newFlexiTyVarTy knd)
1967
1968 cloneMetaTyVar :: TcTyVar -> TcS TcTyVar
1969 cloneMetaTyVar tv = wrapTcS (TcM.cloneMetaTyVar tv)
1970
1971 instFlexi :: [TKVar] -> TcS TCvSubst
1972 instFlexi = instFlexiX emptyTCvSubst
1973
1974 instFlexiX :: TCvSubst -> [TKVar] -> TcS TCvSubst
1975 instFlexiX subst tvs
1976 = wrapTcS (foldlM instFlexiHelper subst tvs)
1977
1978 instFlexiHelper :: TCvSubst -> TKVar -> TcM TCvSubst
1979 instFlexiHelper subst tv
1980 = do { uniq <- TcM.newUnique
1981 ; details <- TcM.newMetaDetails TauTv
1982 ; let name = setNameUnique (tyVarName tv) uniq
1983 kind = substTyUnchecked subst (tyVarKind tv)
1984 ty' = mkTyVarTy (mkTcTyVar name kind details)
1985 ; TcM.traceTc "instFlexi" (ppr ty')
1986 ; return (extendTvSubst subst tv ty') }
1987
1988 matchGlobalInst :: DynFlags
1989 -> Bool -- True <=> caller is the short-cut solver
1990 -- See Note [Shortcut solving: overlap]
1991 -> Class -> [Type] -> TcS TcM.ClsInstResult
1992 matchGlobalInst dflags short_cut cls tys
1993 = wrapTcS (TcM.matchGlobalInst dflags short_cut cls tys)
1994
1995 tcInstSkolTyVarsX :: TCvSubst -> [TyVar] -> TcS (TCvSubst, [TcTyVar])
1996 tcInstSkolTyVarsX subst tvs = wrapTcS $ TcM.tcInstSkolTyVarsX subst tvs
1997
1998 -- Creating and setting evidence variables and CtFlavors
1999 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2000
2001 data MaybeNew = Fresh CtEvidence | Cached EvExpr
2002
2003 isFresh :: MaybeNew -> Bool
2004 isFresh (Fresh {}) = True
2005 isFresh (Cached {}) = False
2006
2007 freshGoals :: [MaybeNew] -> [CtEvidence]
2008 freshGoals mns = [ ctev | Fresh ctev <- mns ]
2009
2010 getEvExpr :: MaybeNew -> EvExpr
2011 getEvExpr (Fresh ctev) = ctEvExpr ctev
2012 getEvExpr (Cached evt) = evt
2013
2014 setEvBind :: EvBind -> TcS ()
2015 setEvBind ev_bind
2016 = do { evb <- getTcEvBindsVar
2017 ; wrapTcS $ TcM.addTcEvBind evb ev_bind }
2018
2019 -- | Mark variables as used filling a coercion hole
2020 useVars :: CoVarSet -> TcS ()
2021 useVars co_vars
2022 = do { ev_binds_var <- getTcEvBindsVar
2023 ; let ref = ebv_tcvs ev_binds_var
2024 ; wrapTcS $
2025 do { tcvs <- TcM.readTcRef ref
2026 ; let tcvs' = tcvs `unionVarSet` co_vars
2027 ; TcM.writeTcRef ref tcvs' } }
2028
2029 -- | Equalities only
2030 setWantedEq :: HasDebugCallStack => TcEvDest -> Coercion -> TcS ()
2031 setWantedEq (HoleDest hole) co
2032 = do { useVars (coVarsOfCo co)
2033 ; fillCoercionHole hole co }
2034 setWantedEq (EvVarDest ev) _ = pprPanic "setWantedEq" (ppr ev)
2035
2036 -- | Good for both equalities and non-equalities
2037 setWantedEvTerm :: TcEvDest -> EvTerm -> TcS ()
2038 setWantedEvTerm (HoleDest hole) tm
2039 | Just co <- evTermCoercion_maybe tm
2040 = do { useVars (coVarsOfCo co)
2041 ; fillCoercionHole hole co }
2042 | otherwise
2043 = -- See Note [Yukky eq_sel for a HoleDest]
2044 do { let co_var = coHoleCoVar hole
2045 ; setEvBind (mkWantedEvBind co_var tm)
2046 ; fillCoercionHole hole (mkTcCoVarCo co_var) }
2047
2048 setWantedEvTerm (EvVarDest ev_id) tm
2049 = setEvBind (mkWantedEvBind ev_id tm)
2050
2051 {- Note [Yukky eq_sel for a HoleDest]
2052 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2053 How can it be that a Wanted with HoleDest gets evidence that isn't
2054 just a coercion? i.e. evTermCoercion_maybe returns Nothing.
2055
2056 Consider [G] forall a. blah => a ~ T
2057 [W] S ~# T
2058
2059 Then doTopReactEqPred carefully looks up the (boxed) constraint (S ~
2060 T) in the quantified constraints, and wraps the (boxed) evidence it
2061 gets back in an eq_sel to extract the unboxed (S ~# T). We can't put
2062 that term into a coercion, so we add a value binding
2063 h = eq_sel (...)
2064 and the coercion variable h to fill the coercion hole.
2065 We even re-use the CoHole's Id for this binding!
2066
2067 Yuk!
2068 -}
2069
2070 fillCoercionHole :: CoercionHole -> Coercion -> TcS ()
2071 fillCoercionHole hole co
2072 = do { wrapTcS $ TcM.fillCoercionHole hole co
2073 ; kickOutAfterFillingCoercionHole hole co }
2074
2075 setEvBindIfWanted :: CtEvidence -> EvTerm -> TcS ()
2076 setEvBindIfWanted ev tm
2077 = case ev of
2078 CtWanted { ctev_dest = dest } -> setWantedEvTerm dest tm
2079 _ -> return ()
2080
2081 newTcEvBinds :: TcS EvBindsVar
2082 newTcEvBinds = wrapTcS TcM.newTcEvBinds
2083
2084 newNoTcEvBinds :: TcS EvBindsVar
2085 newNoTcEvBinds = wrapTcS TcM.newNoTcEvBinds
2086
2087 newEvVar :: TcPredType -> TcS EvVar
2088 newEvVar pred = wrapTcS (TcM.newEvVar pred)
2089
2090 newGivenEvVar :: CtLoc -> (TcPredType, EvTerm) -> TcS CtEvidence
2091 -- Make a new variable of the given PredType,
2092 -- immediately bind it to the given term
2093 -- and return its CtEvidence
2094 -- See Note [Bind new Givens immediately] in GHC.Tc.Types.Constraint
2095 newGivenEvVar loc (pred, rhs)
2096 = do { new_ev <- newBoundEvVarId pred rhs
2097 ; return (CtGiven { ctev_pred = pred, ctev_evar = new_ev, ctev_loc = loc }) }
2098
2099 -- | Make a new 'Id' of the given type, bound (in the monad's EvBinds) to the
2100 -- given term
2101 newBoundEvVarId :: TcPredType -> EvTerm -> TcS EvVar
2102 newBoundEvVarId pred rhs
2103 = do { new_ev <- newEvVar pred
2104 ; setEvBind (mkGivenEvBind new_ev rhs)
2105 ; return new_ev }
2106
2107 newGivenEvVars :: CtLoc -> [(TcPredType, EvTerm)] -> TcS [CtEvidence]
2108 newGivenEvVars loc pts = mapM (newGivenEvVar loc) pts
2109
2110 emitNewWantedEq :: CtLoc -> Role -> TcType -> TcType -> TcS Coercion
2111 -- | Emit a new Wanted equality into the work-list
2112 emitNewWantedEq loc role ty1 ty2
2113 = do { (ev, co) <- newWantedEq loc role ty1 ty2
2114 ; updWorkListTcS (extendWorkListEq (mkNonCanonical ev))
2115 ; return co }
2116
2117 -- | Make a new equality CtEvidence
2118 newWantedEq :: CtLoc -> Role -> TcType -> TcType
2119 -> TcS (CtEvidence, Coercion)
2120 newWantedEq = newWantedEq_SI WDeriv
2121
2122 newWantedEq_SI :: ShadowInfo -> CtLoc -> Role
2123 -> TcType -> TcType
2124 -> TcS (CtEvidence, Coercion)
2125 newWantedEq_SI si loc role ty1 ty2
2126 = do { hole <- wrapTcS $ TcM.newCoercionHole pty
2127 ; traceTcS "Emitting new coercion hole" (ppr hole <+> dcolon <+> ppr pty)
2128 ; return ( CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole
2129 , ctev_nosh = si
2130 , ctev_loc = loc}
2131 , mkHoleCo hole ) }
2132 where
2133 pty = mkPrimEqPredRole role ty1 ty2
2134
2135 -- no equalities here. Use newWantedEq instead
2136 newWantedEvVarNC :: CtLoc -> TcPredType -> TcS CtEvidence
2137 newWantedEvVarNC = newWantedEvVarNC_SI WDeriv
2138
2139 newWantedEvVarNC_SI :: ShadowInfo -> CtLoc -> TcPredType -> TcS CtEvidence
2140 -- Don't look up in the solved/inerts; we know it's not there
2141 newWantedEvVarNC_SI si loc pty
2142 = do { new_ev <- newEvVar pty
2143 ; traceTcS "Emitting new wanted" (ppr new_ev <+> dcolon <+> ppr pty $$
2144 pprCtLoc loc)
2145 ; return (CtWanted { ctev_pred = pty, ctev_dest = EvVarDest new_ev
2146 , ctev_nosh = si
2147 , ctev_loc = loc })}
2148
2149 newWantedEvVar :: CtLoc -> TcPredType -> TcS MaybeNew
2150 newWantedEvVar = newWantedEvVar_SI WDeriv
2151
2152 newWantedEvVar_SI :: ShadowInfo -> CtLoc -> TcPredType -> TcS MaybeNew
2153 -- For anything except ClassPred, this is the same as newWantedEvVarNC
2154 newWantedEvVar_SI si loc pty
2155 = do { mb_ct <- lookupInInerts loc pty
2156 ; case mb_ct of
2157 Just ctev
2158 | not (isDerived ctev)
2159 -> do { traceTcS "newWantedEvVar/cache hit" $ ppr ctev
2160 ; return $ Cached (ctEvExpr ctev) }
2161 _ -> do { ctev <- newWantedEvVarNC_SI si loc pty
2162 ; return (Fresh ctev) } }
2163
2164 newWanted :: CtLoc -> PredType -> TcS MaybeNew
2165 -- Deals with both equalities and non equalities. Tries to look
2166 -- up non-equalities in the cache
2167 newWanted = newWanted_SI WDeriv
2168
2169 newWanted_SI :: ShadowInfo -> CtLoc -> PredType -> TcS MaybeNew
2170 newWanted_SI si loc pty
2171 | Just (role, ty1, ty2) <- getEqPredTys_maybe pty
2172 = Fresh . fst <$> newWantedEq_SI si loc role ty1 ty2
2173 | otherwise
2174 = newWantedEvVar_SI si loc pty
2175
2176 -- deals with both equalities and non equalities. Doesn't do any cache lookups.
2177 newWantedNC :: CtLoc -> PredType -> TcS CtEvidence
2178 newWantedNC loc pty
2179 | Just (role, ty1, ty2) <- getEqPredTys_maybe pty
2180 = fst <$> newWantedEq loc role ty1 ty2
2181 | otherwise
2182 = newWantedEvVarNC loc pty
2183
2184 emitNewDeriveds :: CtLoc -> [TcPredType] -> TcS ()
2185 emitNewDeriveds loc preds
2186 | null preds
2187 = return ()
2188 | otherwise
2189 = do { evs <- mapM (newDerivedNC loc) preds
2190 ; traceTcS "Emitting new deriveds" (ppr evs)
2191 ; updWorkListTcS (extendWorkListDeriveds evs) }
2192
2193 emitNewDerivedEq :: CtLoc -> Role -> TcType -> TcType -> TcS ()
2194 -- Create new equality Derived and put it in the work list
2195 -- There's no caching, no lookupInInerts
2196 emitNewDerivedEq loc role ty1 ty2
2197 = do { ev <- newDerivedNC loc (mkPrimEqPredRole role ty1 ty2)
2198 ; traceTcS "Emitting new derived equality" (ppr ev $$ pprCtLoc loc)
2199 ; updWorkListTcS (extendWorkListEq (mkNonCanonical ev)) }
2200 -- Very important: put in the wl_eqs
2201 -- See Note [Prioritise equalities] in GHC.Tc.Solver.InertSet
2202 -- (Avoiding fundep iteration)
2203
2204 newDerivedNC :: CtLoc -> TcPredType -> TcS CtEvidence
2205 newDerivedNC loc pred
2206 = return $ CtDerived { ctev_pred = pred, ctev_loc = loc }
2207
2208 -- --------- Check done in GHC.Tc.Solver.Interact.selectNewWorkItem???? ---------
2209 -- | Checks if the depth of the given location is too much. Fails if
2210 -- it's too big, with an appropriate error message.
2211 checkReductionDepth :: CtLoc -> TcType -- ^ type being reduced
2212 -> TcS ()
2213 checkReductionDepth loc ty
2214 = do { dflags <- getDynFlags
2215 ; when (subGoalDepthExceeded dflags (ctLocDepth loc)) $
2216 wrapErrTcS $
2217 solverDepthErrorTcS loc ty }
2218
2219 matchFam :: TyCon -> [Type] -> TcS (Maybe ReductionN)
2220 matchFam tycon args = wrapTcS $ matchFamTcM tycon args
2221
2222 matchFamTcM :: TyCon -> [Type] -> TcM (Maybe ReductionN)
2223 -- Given (F tys) return (ty, co), where co :: F tys ~N ty
2224 matchFamTcM tycon args
2225 = do { fam_envs <- FamInst.tcGetFamInstEnvs
2226 ; let match_fam_result
2227 = reduceTyFamApp_maybe fam_envs Nominal tycon args
2228 ; TcM.traceTc "matchFamTcM" $
2229 vcat [ text "Matching:" <+> ppr (mkTyConApp tycon args)
2230 , ppr_res match_fam_result ]
2231 ; return match_fam_result }
2232 where
2233 ppr_res Nothing = text "Match failed"
2234 ppr_res (Just (Reduction co ty))
2235 = hang (text "Match succeeded:")
2236 2 (vcat [ text "Rewrites to:" <+> ppr ty
2237 , text "Coercion:" <+> ppr co ])
2238
2239 {-
2240 ************************************************************************
2241 * *
2242 Breaking type variable cycles
2243 * *
2244 ************************************************************************
2245 -}
2246
2247 -- | Conditionally replace all type family applications in the RHS with fresh
2248 -- variables, emitting givens that relate the type family application to the
2249 -- variable. See Note [Type variable cycles] in GHC.Tc.Solver.Canonical.
2250 -- This only works under conditions as described in the Note; otherwise, returns
2251 -- Nothing.
2252 breakTyVarCycle_maybe :: CtEvidence
2253 -> CheckTyEqResult -- result of checkTypeEq
2254 -> CanEqLHS
2255 -> TcType -- RHS
2256 -> TcS (Maybe (TcTyVar, ReductionN))
2257 -- new RHS that doesn't have any type families
2258 -- TcTyVar is the LHS tv; convenient for the caller
2259 breakTyVarCycle_maybe (ctLocOrigin . ctEvLoc -> CycleBreakerOrigin _) _ _ _
2260 -- see Detail (7) of Note
2261 = return Nothing
2262
2263 breakTyVarCycle_maybe ev cte_result (TyVarLHS lhs_tv) rhs
2264 | NomEq <- eq_rel
2265
2266 , cte_result `cterHasOnlyProblem` cteSolubleOccurs
2267 -- only do this if the only problem is a soluble occurs-check
2268 -- See Detail (8) of the Note.
2269
2270 = do { should_break <- final_check
2271 ; if should_break then do { redn <- go rhs
2272 ; return (Just (lhs_tv, redn)) }
2273 else return Nothing }
2274 where
2275 flavour = ctEvFlavour ev
2276 eq_rel = ctEvEqRel ev
2277
2278 final_check
2279 | Given <- flavour
2280 = return True
2281 | ctFlavourContainsDerived flavour
2282 = do { result <- touchabilityTest Derived lhs_tv rhs
2283 ; return $ case result of
2284 Untouchable -> False
2285 _ -> True }
2286 | otherwise
2287 = return False
2288
2289 -- This could be considerably more efficient. See Detail (5) of Note.
2290 go :: TcType -> TcS ReductionN
2291 go ty | Just ty' <- rewriterView ty = go ty'
2292 go (Rep.TyConApp tc tys)
2293 | isTypeFamilyTyCon tc -- worried about whether this type family is not actually
2294 -- causing trouble? See Detail (5) of Note.
2295 = do { let (fun_args, extra_args) = splitAt (tyConArity tc) tys
2296 fun_app = mkTyConApp tc fun_args
2297 fun_app_kind = tcTypeKind fun_app
2298 ; fun_redn <- emit_work fun_app_kind fun_app
2299 ; arg_redns <- unzipRedns <$> mapM go extra_args
2300 ; return $ mkAppRedns fun_redn arg_redns }
2301 -- Worried that this substitution will change kinds?
2302 -- See Detail (3) of Note
2303
2304 | otherwise
2305 = do { arg_redns <- unzipRedns <$> mapM go tys
2306 ; return $ mkTyConAppRedn Nominal tc arg_redns }
2307
2308 go (Rep.AppTy ty1 ty2)
2309 = mkAppRedn <$> go ty1 <*> go ty2
2310 go (Rep.FunTy vis w arg res)
2311 = mkFunRedn Nominal vis <$> go w <*> go arg <*> go res
2312 go (Rep.CastTy ty cast_co)
2313 = mkCastRedn1 Nominal ty cast_co <$> go ty
2314 go ty@(Rep.TyVarTy {}) = skip ty
2315 go ty@(Rep.LitTy {}) = skip ty
2316 go ty@(Rep.ForAllTy {}) = skip ty -- See Detail (1) of Note
2317 go ty@(Rep.CoercionTy {}) = skip ty -- See Detail (2) of Note
2318
2319 skip ty = return $ mkReflRedn Nominal ty
2320
2321 emit_work :: TcKind -- of the function application
2322 -> TcType -- original function application
2323 -> TcS ReductionN -- rewritten type (the fresh tyvar)
2324 emit_work fun_app_kind fun_app = case flavour of
2325 Given ->
2326 do { new_tv <- wrapTcS (TcM.newCycleBreakerTyVar fun_app_kind)
2327 ; let new_ty = mkTyVarTy new_tv
2328 given_pred = mkHeteroPrimEqPred fun_app_kind fun_app_kind
2329 fun_app new_ty
2330 given_term = evCoercion $ mkNomReflCo new_ty -- See Detail (4) of Note
2331 ; new_given <- newGivenEvVar new_loc (given_pred, given_term)
2332 ; traceTcS "breakTyVarCycle replacing type family in Given" (ppr new_given)
2333 ; emitWorkNC [new_given]
2334 ; updInertTcS $ \is ->
2335 is { inert_cycle_breakers = (new_tv, fun_app) :
2336 inert_cycle_breakers is }
2337 ; return $ mkReflRedn Nominal new_ty }
2338 -- Why reflexive? See Detail (4) of the Note
2339
2340 _derived_or_wd ->
2341 do { new_tv <- wrapTcS (TcM.newFlexiTyVar fun_app_kind)
2342 ; let new_ty = mkTyVarTy new_tv
2343 ; co <- emitNewWantedEq new_loc Nominal new_ty fun_app
2344 ; return $ mkReduction (mkSymCo co) new_ty }
2345
2346 -- See Detail (7) of the Note
2347 new_loc = updateCtLocOrigin (ctEvLoc ev) CycleBreakerOrigin
2348
2349 -- does not fit scenario from Note
2350 breakTyVarCycle_maybe _ _ _ _ = return Nothing
2351
2352 -- | Fill in CycleBreakerTvs with the variables they stand for.
2353 -- See Note [Type variable cycles] in GHC.Tc.Solver.Canonical.
2354 restoreTyVarCycles :: InertSet -> TcM ()
2355 restoreTyVarCycles is
2356 = forM_ (inert_cycle_breakers is) $ \ (cycle_breaker_tv, orig_ty) ->
2357 TcM.writeMetaTyVar cycle_breaker_tv orig_ty
2358
2359 -- Unwrap a type synonym only when either:
2360 -- The type synonym is forgetful, or
2361 -- the type synonym mentions a type family in its expansion
2362 -- See Note [Rewriting synonyms] in GHC.Tc.Solver.Rewrite.
2363 rewriterView :: TcType -> Maybe TcType
2364 rewriterView ty@(Rep.TyConApp tc _)
2365 | isForgetfulSynTyCon tc || (isTypeSynonymTyCon tc && not (isFamFreeTyCon tc))
2366 = tcView ty
2367 rewriterView _other = Nothing