never executed always true always false
1
2 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
3
4 {-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
5
6 -- | This module defines types and simple operations over constraints, as used
7 -- in the type-checker and constraint solver.
8 module GHC.Tc.Types.Constraint (
9 -- QCInst
10 QCInst(..), isPendingScInst,
11
12 -- Canonical constraints
13 Xi, Ct(..), Cts,
14 emptyCts, andCts, andManyCts, pprCts,
15 singleCt, listToCts, ctsElts, consCts, snocCts, extendCtsList,
16 isEmptyCts,
17 isPendingScDict, superClassesMightHelp, getPendingWantedScs,
18 isWantedCt, isDerivedCt, isGivenCt,
19 isUserTypeErrorCt, getUserTypeErrorMsg,
20 ctEvidence, ctLoc, setCtLoc, ctPred, ctFlavour, ctEqRel, ctOrigin,
21 ctEvId, mkTcEqPredLikeEv,
22 mkNonCanonical, mkNonCanonicalCt, mkGivens,
23 mkIrredCt,
24 ctEvPred, ctEvLoc, ctEvOrigin, ctEvEqRel,
25 ctEvExpr, ctEvTerm, ctEvCoercion, ctEvEvId,
26 tyCoVarsOfCt, tyCoVarsOfCts,
27 tyCoVarsOfCtList, tyCoVarsOfCtsList,
28
29 CtIrredReason(..), HoleSet, isInsolubleReason,
30
31 CheckTyEqResult, CheckTyEqProblem, cteProblem, cterClearOccursCheck,
32 cteOK, cteImpredicative, cteTypeFamily, cteHoleBlocker,
33 cteInsolubleOccurs, cteSolubleOccurs, cterSetOccursCheckSoluble,
34 cterHasNoProblem, cterHasProblem, cterHasOnlyProblem,
35 cterRemoveProblem, cterHasOccursCheck, cterFromKind,
36
37 CanEqLHS(..), canEqLHS_maybe, canEqLHSKind, canEqLHSType,
38 eqCanEqLHS,
39
40 Hole(..), HoleSort(..), isOutOfScopeHole,
41
42 WantedConstraints(..), insolubleWC, emptyWC, isEmptyWC,
43 isSolvedWC, andWC, unionsWC, mkSimpleWC, mkImplicWC,
44 addInsols, dropMisleading, addSimples, addImplics, addHoles,
45 tyCoVarsOfWC, dropDerivedWC, dropDerivedSimples,
46 tyCoVarsOfWCList, insolubleWantedCt, insolubleEqCt, insolubleCt,
47 isDroppableCt, insolubleImplic,
48 arisesFromGivens,
49
50 Implication(..), implicationPrototype, checkTelescopeSkol,
51 ImplicStatus(..), isInsolubleStatus, isSolvedStatus,
52 HasGivenEqs(..),
53 SubGoalDepth, initialSubGoalDepth, maxSubGoalDepth,
54 bumpSubGoalDepth, subGoalDepthExceeded,
55 CtLoc(..), ctLocSpan, ctLocEnv, ctLocLevel, ctLocOrigin,
56 ctLocTypeOrKind_maybe,
57 ctLocDepth, bumpCtLocDepth, isGivenLoc,
58 setCtLocOrigin, updateCtLocOrigin, setCtLocEnv, setCtLocSpan,
59 pprCtLoc,
60
61 -- CtEvidence
62 CtEvidence(..), TcEvDest(..),
63 mkKindLoc, toKindLoc, mkGivenLoc,
64 isWanted, isGiven, isDerived,
65 ctEvRole,
66
67 wrapType,
68
69 CtFlavour(..), ShadowInfo(..), ctFlavourContainsDerived, ctEvFlavour,
70 CtFlavourRole, ctEvFlavourRole, ctFlavourRole,
71 eqCanRewrite, eqCanRewriteFR, eqMayRewriteFR,
72 eqCanDischargeFR,
73
74 -- Pretty printing
75 pprEvVarTheta,
76 pprEvVars, pprEvVarWithType,
77
78 )
79 where
80
81 import GHC.Prelude
82
83 import {-# SOURCE #-} GHC.Tc.Types ( TcLclEnv, setLclEnvTcLevel, getLclEnvTcLevel
84 , setLclEnvLoc, getLclEnvLoc )
85
86 import GHC.Core.Predicate
87 import GHC.Core.Type
88 import GHC.Core.Coercion
89 import GHC.Core.Class
90 import GHC.Core.TyCon
91 import GHC.Types.Var
92
93 import GHC.Tc.Utils.TcType
94 import GHC.Tc.Types.Evidence
95 import GHC.Tc.Types.Origin
96
97 import GHC.Core
98
99 import GHC.Core.TyCo.Ppr
100 import GHC.Types.Name.Occurrence
101 import GHC.Utils.FV
102 import GHC.Types.Var.Set
103 import GHC.Driver.Session
104 import GHC.Types.Basic
105
106 import GHC.Utils.Outputable
107 import GHC.Types.SrcLoc
108 import GHC.Data.Bag
109 import GHC.Utils.Misc
110 import GHC.Utils.Panic
111
112 import Control.Monad ( msum )
113 import qualified Data.Semigroup ( (<>) )
114
115 -- these are for CheckTyEqResult
116 import Data.Word ( Word8 )
117 import Data.List ( intersperse )
118
119
120
121 {-
122 ************************************************************************
123 * *
124 * Canonical constraints *
125 * *
126 * These are the constraints the low-level simplifier works with *
127 * *
128 ************************************************************************
129
130 Note [CEqCan occurs check]
131 ~~~~~~~~~~~~~~~~~~~~~~~~~~
132 A CEqCan relates a CanEqLHS (a type variable or type family applications) on
133 its left to an arbitrary type on its right. It is used for rewriting.
134 Because it is used for rewriting, it would be disastrous if the RHS
135 were to mention the LHS: this would cause a loop in rewriting.
136
137 We thus perform an occurs-check. There is, of course, some subtlety:
138
139 * For type variables, the occurs-check looks deeply. This is because
140 a CEqCan over a meta-variable is also used to inform unification,
141 in GHC.Tc.Solver.Interact.solveByUnification. If the LHS appears
142 anywhere, at all, in the RHS, unification will create an infinite
143 structure, which is bad.
144
145 * For type family applications, the occurs-check is shallow; it looks
146 only in places where we might rewrite. (Specifically, it does not
147 look in kinds or coercions.) An occurrence of the LHS in, say, an
148 RHS coercion is OK, as we do not rewrite in coercions. No loop to
149 be found.
150
151 You might also worry about the possibility that a type family
152 application LHS doesn't exactly appear in the RHS, but something
153 that reduces to the LHS does. Yet that can't happen: the RHS is
154 already inert, with all type family redexes reduced. So a simple
155 syntactic check is just fine.
156
157 The occurs check is performed in GHC.Tc.Utils.Unify.checkTypeEq
158 and forms condition T3 in Note [Extending the inert equalities]
159 in GHC.Tc.Solver.InertSet.
160
161 -}
162
163 -- | A 'Xi'-type is one that has been fully rewritten with respect
164 -- to the inert set; that is, it has been rewritten by the algorithm
165 -- in GHC.Tc.Solver.Rewrite. (Historical note: 'Xi', for years and years,
166 -- meant that a type was type-family-free. It does *not* mean this
167 -- any more.)
168 type Xi = TcType
169
170 type Cts = Bag Ct
171
172 data Ct
173 -- Atomic canonical constraints
174 = CDictCan { -- e.g. Num ty
175 cc_ev :: CtEvidence, -- See Note [Ct/evidence invariant]
176
177 cc_class :: Class,
178 cc_tyargs :: [Xi], -- cc_tyargs are rewritten w.r.t. inerts, so Xi
179
180 cc_pend_sc :: Bool,
181 -- See Note [The superclass story] in GHC.Tc.Solver.Canonical
182 -- True <=> (a) cc_class has superclasses
183 -- (b) we have not (yet) added those
184 -- superclasses as Givens
185
186 cc_fundeps :: Bool
187 -- See Note [Fundeps with instances] in GHC.Tc.Solver.Interact
188 -- True <=> the class has fundeps, and we have not yet
189 -- compared this constraint with the global
190 -- instances for fundep improvement
191 }
192
193 | CIrredCan { -- These stand for yet-unusable predicates
194 cc_ev :: CtEvidence, -- See Note [Ct/evidence invariant]
195 cc_reason :: CtIrredReason
196
197 -- For the might-be-soluble case, the ctev_pred of the evidence is
198 -- of form (tv xi1 xi2 ... xin) with a tyvar at the head
199 -- or (lhs1 ~ ty2) where the CEqCan kind invariant (TyEq:K) fails
200 -- See Note [CIrredCan constraints]
201
202 -- The definitely-insoluble case is for things like
203 -- Int ~ Bool tycons don't match
204 -- a ~ [a] occurs check
205 }
206
207 | CEqCan { -- CanEqLHS ~ rhs
208 -- Invariants:
209 -- * See Note [inert_eqs: the inert equalities] in GHC.Tc.Solver.InertSet
210 -- * Many are checked in checkTypeEq in GHC.Tc.Utils.Unify
211 -- * (TyEq:OC) lhs does not occur in rhs (occurs check)
212 -- Note [CEqCan occurs check]
213 -- * (TyEq:F) rhs has no foralls
214 -- (this avoids substituting a forall for the tyvar in other types)
215 -- * (TyEq:K) tcTypeKind lhs `tcEqKind` tcTypeKind rhs; Note [Ct kind invariant]
216 -- * (TyEq:N) If the equality is representational, rhs has no top-level newtype
217 -- See Note [No top-level newtypes on RHS of representational equalities]
218 -- in GHC.Tc.Solver.Canonical. (Applies only when constructor of newtype is
219 -- in scope.)
220 -- * (TyEq:TV) If rhs (perhaps under a cast) is also CanEqLHS, then it is oriented
221 -- to give best chance of
222 -- unification happening; eg if rhs is touchable then lhs is too
223 -- Note [TyVar/TyVar orientation] in GHC.Tc.Utils.Unify
224 -- * (TyEq:H) The RHS has no blocking coercion holes. See GHC.Tc.Solver.Canonical
225 -- Note [Equalities with incompatible kinds], wrinkle (2)
226 cc_ev :: CtEvidence, -- See Note [Ct/evidence invariant]
227 cc_lhs :: CanEqLHS,
228 cc_rhs :: Xi, -- See invariants above
229
230 cc_eq_rel :: EqRel -- INVARIANT: cc_eq_rel = ctEvEqRel cc_ev
231 }
232
233 | CNonCanonical { -- See Note [NonCanonical Semantics] in GHC.Tc.Solver.Monad
234 cc_ev :: CtEvidence
235 }
236
237 | CQuantCan QCInst -- A quantified constraint
238 -- NB: I expect to make more of the cases in Ct
239 -- look like this, with the payload in an
240 -- auxiliary type
241
242 -- | A special canonical constraint.
243 --
244 -- When the 'SpecialPred' is 'ConcretePrimPred':
245 --
246 -- - `cc_ev` is Wanted,
247 -- - `cc_xi = ty`, where `ty` cannot be decomposed any further.
248 -- See Note [Canonical Concrete# constraints] in GHC.Tc.Solver.Canonical.
249 | CSpecialCan {
250 cc_ev :: CtEvidence,
251 cc_special_pred :: SpecialPred,
252 cc_xi :: Xi
253 }
254
255 ------------
256 -- | A 'CanEqLHS' is a type that can appear on the left of a canonical
257 -- equality: a type variable or exactly-saturated type family application.
258 data CanEqLHS
259 = TyVarLHS TcTyVar
260 | TyFamLHS TyCon -- ^ of the family
261 [Xi] -- ^ exactly saturating the family
262
263 instance Outputable CanEqLHS where
264 ppr (TyVarLHS tv) = ppr tv
265 ppr (TyFamLHS fam_tc fam_args) = ppr (mkTyConApp fam_tc fam_args)
266
267 ------------
268 data QCInst -- A much simplified version of ClsInst
269 -- See Note [Quantified constraints] in GHC.Tc.Solver.Canonical
270 = QCI { qci_ev :: CtEvidence -- Always of type forall tvs. context => ty
271 -- Always Given
272 , qci_tvs :: [TcTyVar] -- The tvs
273 , qci_pred :: TcPredType -- The ty
274 , qci_pend_sc :: Bool -- Same as cc_pend_sc flag in CDictCan
275 -- Invariant: True => qci_pred is a ClassPred
276 }
277
278 instance Outputable QCInst where
279 ppr (QCI { qci_ev = ev }) = ppr ev
280
281 ------------
282 -- | A hole stores the information needed to report diagnostics
283 -- about holes in terms (unbound identifiers or underscores) or
284 -- in types (also called wildcards, as used in partial type
285 -- signatures). See Note [Holes].
286 data Hole
287 = Hole { hole_sort :: HoleSort -- ^ What flavour of hole is this?
288 , hole_occ :: OccName -- ^ The name of this hole
289 , hole_ty :: TcType -- ^ Type to be printed to the user
290 -- For expression holes: type of expr
291 -- For type holes: the missing type
292 , hole_loc :: CtLoc -- ^ Where hole was written
293 }
294 -- For the hole_loc, we usually only want the TcLclEnv stored within.
295 -- Except when we rewrite, where we need a whole location. And this
296 -- might get reported to the user if reducing type families in a
297 -- hole type loops.
298
299
300 -- | Used to indicate which sort of hole we have.
301 data HoleSort = ExprHole HoleExprRef
302 -- ^ Either an out-of-scope variable or a "true" hole in an
303 -- expression (TypedHoles).
304 -- The HoleExprRef says where to write the
305 -- the erroring expression for -fdefer-type-errors.
306 | TypeHole
307 -- ^ A hole in a type (PartialTypeSignatures)
308 | ConstraintHole
309 -- ^ A hole in a constraint, like @f :: (_, Eq a) => ...
310 -- Differentiated from TypeHole because a ConstraintHole
311 -- is simplified differently. See
312 -- Note [Do not simplify ConstraintHoles] in GHC.Tc.Solver.
313
314 instance Outputable Hole where
315 ppr (Hole { hole_sort = ExprHole ref
316 , hole_occ = occ
317 , hole_ty = ty })
318 = parens $ (braces $ ppr occ <> colon <> ppr ref) <+> dcolon <+> ppr ty
319 ppr (Hole { hole_sort = _other
320 , hole_occ = occ
321 , hole_ty = ty })
322 = braces $ ppr occ <> colon <> ppr ty
323
324 instance Outputable HoleSort where
325 ppr (ExprHole ref) = text "ExprHole:" <+> ppr ref
326 ppr TypeHole = text "TypeHole"
327 ppr ConstraintHole = text "ConstraintHole"
328
329 ------------
330 -- | Used to indicate extra information about why a CIrredCan is irreducible
331 data CtIrredReason
332 = IrredShapeReason
333 -- ^ this constraint has a non-canonical shape (e.g. @c Int@, for a variable @c@)
334
335 | HoleBlockerReason HoleSet
336 -- ^ this constraint is blocked on the coercion hole(s) listed
337 -- See Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Canonical
338 -- Wrinkle (4a). Why store the HoleSet? See Wrinkle (2) of that
339 -- same Note.
340 -- INVARIANT: A HoleBlockerReason constraint is a homogeneous equality whose
341 -- left hand side can fit in a CanEqLHS.
342
343 | NonCanonicalReason CheckTyEqResult
344 -- ^ an equality where some invariant other than (TyEq:H) of 'CEqCan' is not satisfied;
345 -- the 'CheckTyEqResult' states exactly why
346 -- INVARIANT: the 'CheckTyEqResult' has some bit set other than cteHoleBlocker
347
348 | ReprEqReason
349 -- ^ an equality that cannot be decomposed because it is representational.
350 -- Example: @a b ~R# Int@.
351 -- These might still be solved later.
352 -- INVARIANT: The constraint is a representational equality constraint
353
354 | ShapeMismatchReason
355 -- ^ a nominal equality that relates two wholly different types,
356 -- like @Int ~# Bool@ or @a b ~# 3@.
357 -- INVARIANT: The constraint is a nominal equality constraint
358
359 | AbstractTyConReason
360 -- ^ an equality like @T a b c ~ Q d e@ where either @T@ or @Q@
361 -- is an abstract type constructor. See Note [Skolem abstract data]
362 -- in GHC.Core.TyCon.
363 -- INVARIANT: The constraint is an equality constraint between two TyConApps
364
365 instance Outputable CtIrredReason where
366 ppr IrredShapeReason = text "(irred)"
367 ppr (HoleBlockerReason holes) = parens (text "blocked on" <+> ppr holes)
368 ppr (NonCanonicalReason cter) = ppr cter
369 ppr ReprEqReason = text "(repr)"
370 ppr ShapeMismatchReason = text "(shape)"
371 ppr AbstractTyConReason = text "(abstc)"
372
373 -- | Are we sure that more solving will never solve this constraint?
374 isInsolubleReason :: CtIrredReason -> Bool
375 isInsolubleReason IrredShapeReason = False
376 isInsolubleReason (HoleBlockerReason {}) = False
377 isInsolubleReason (NonCanonicalReason cter) = cterIsInsoluble cter
378 isInsolubleReason ReprEqReason = False
379 isInsolubleReason ShapeMismatchReason = True
380 isInsolubleReason AbstractTyConReason = True
381
382 ------------------------------------------------------------------------------
383 --
384 -- CheckTyEqResult, defined here because it is stored in a CtIrredReason
385 --
386 ------------------------------------------------------------------------------
387
388 -- | A set of problems in checking the validity of a type equality.
389 -- See 'checkTypeEq'.
390 newtype CheckTyEqResult = CTER Word8
391
392 -- | No problems in checking the validity of a type equality.
393 cteOK :: CheckTyEqResult
394 cteOK = CTER zeroBits
395
396 -- | Check whether a 'CheckTyEqResult' is marked successful.
397 cterHasNoProblem :: CheckTyEqResult -> Bool
398 cterHasNoProblem (CTER 0) = True
399 cterHasNoProblem _ = False
400
401 -- | An individual problem that might be logged in a 'CheckTyEqResult'
402 newtype CheckTyEqProblem = CTEP Word8
403
404 cteImpredicative, cteTypeFamily, cteHoleBlocker, cteInsolubleOccurs,
405 cteSolubleOccurs :: CheckTyEqProblem
406 cteImpredicative = CTEP (bit 0) -- forall or (=>) encountered
407 cteTypeFamily = CTEP (bit 1) -- type family encountered
408 cteHoleBlocker = CTEP (bit 2) -- blocking coercion hole
409 -- See Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Canonical
410 cteInsolubleOccurs = CTEP (bit 3) -- occurs-check
411 cteSolubleOccurs = CTEP (bit 4) -- occurs-check under a type function or in a coercion
412 -- must be one bit to the left of cteInsolubleOccurs
413 -- See also Note [Insoluble occurs check] in GHC.Tc.Errors
414
415 cteProblem :: CheckTyEqProblem -> CheckTyEqResult
416 cteProblem (CTEP mask) = CTER mask
417
418 occurs_mask :: Word8
419 occurs_mask = insoluble_mask .|. soluble_mask
420 where
421 CTEP insoluble_mask = cteInsolubleOccurs
422 CTEP soluble_mask = cteSolubleOccurs
423
424 -- | Check whether a 'CheckTyEqResult' has a 'CheckTyEqProblem'
425 cterHasProblem :: CheckTyEqResult -> CheckTyEqProblem -> Bool
426 CTER bits `cterHasProblem` CTEP mask = (bits .&. mask) /= 0
427
428 -- | Check whether a 'CheckTyEqResult' has one 'CheckTyEqProblem' and no other
429 cterHasOnlyProblem :: CheckTyEqResult -> CheckTyEqProblem -> Bool
430 CTER bits `cterHasOnlyProblem` CTEP mask = bits == mask
431
432 cterRemoveProblem :: CheckTyEqResult -> CheckTyEqProblem -> CheckTyEqResult
433 cterRemoveProblem (CTER bits) (CTEP mask) = CTER (bits .&. complement mask)
434
435 cterHasOccursCheck :: CheckTyEqResult -> Bool
436 cterHasOccursCheck (CTER bits) = (bits .&. occurs_mask) /= 0
437
438 cterClearOccursCheck :: CheckTyEqResult -> CheckTyEqResult
439 cterClearOccursCheck (CTER bits) = CTER (bits .&. complement occurs_mask)
440
441 -- | Mark a 'CheckTyEqResult' as not having an insoluble occurs-check: any occurs
442 -- check under a type family or in a representation equality is soluble.
443 cterSetOccursCheckSoluble :: CheckTyEqResult -> CheckTyEqResult
444 cterSetOccursCheckSoluble (CTER bits)
445 = CTER $ ((bits .&. insoluble_mask) `shift` 1) .|. (bits .&. complement insoluble_mask)
446 where
447 CTEP insoluble_mask = cteInsolubleOccurs
448
449 -- | Retain only information about occurs-check failures, because only that
450 -- matters after recurring into a kind.
451 cterFromKind :: CheckTyEqResult -> CheckTyEqResult
452 cterFromKind (CTER bits)
453 = CTER (bits .&. occurs_mask)
454
455 cterIsInsoluble :: CheckTyEqResult -> Bool
456 cterIsInsoluble (CTER bits) = (bits .&. mask) /= 0
457 where
458 mask = impredicative_mask .|. insoluble_occurs_mask
459
460 CTEP impredicative_mask = cteImpredicative
461 CTEP insoluble_occurs_mask = cteInsolubleOccurs
462
463 instance Semigroup CheckTyEqResult where
464 CTER bits1 <> CTER bits2 = CTER (bits1 .|. bits2)
465 instance Monoid CheckTyEqResult where
466 mempty = cteOK
467
468 instance Outputable CheckTyEqResult where
469 ppr cter | cterHasNoProblem cter = text "cteOK"
470 | otherwise
471 = parens $ fcat $ intersperse vbar $ set_bits
472 where
473 all_bits = [ (cteImpredicative, "cteImpredicative")
474 , (cteTypeFamily, "cteTypeFamily")
475 , (cteHoleBlocker, "cteHoleBlocker")
476 , (cteInsolubleOccurs, "cteInsolubleOccurs")
477 , (cteSolubleOccurs, "cteSolubleOccurs") ]
478 set_bits = [ text str
479 | (bitmask, str) <- all_bits
480 , cter `cterHasProblem` bitmask ]
481
482 {- Note [CIrredCan constraints]
483 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
484 CIrredCan constraints are used for constraints that are "stuck"
485 - we can't solve them (yet)
486 - we can't use them to solve other constraints
487 - but they may become soluble if we substitute for some
488 of the type variables in the constraint
489
490 Example 1: (c Int), where c :: * -> Constraint. We can't do anything
491 with this yet, but if later c := Num, *then* we can solve it
492
493 Example 2: a ~ b, where a :: *, b :: k, where k is a kind variable
494 We don't want to use this to substitute 'b' for 'a', in case
495 'k' is subsequently unified with (say) *->*, because then
496 we'd have ill-kinded types floating about. Rather we want
497 to defer using the equality altogether until 'k' get resolved.
498
499 Note [Ct/evidence invariant]
500 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
501 If ct :: Ct, then extra fields of 'ct' cache precisely the ctev_pred field
502 of (cc_ev ct), and is fully rewritten wrt the substitution. Eg for CDictCan,
503 ctev_pred (cc_ev ct) = (cc_class ct) (cc_tyargs ct)
504 This holds by construction; look at the unique place where CDictCan is
505 built (in GHC.Tc.Solver.Canonical).
506
507 In contrast, the type of the evidence *term* (ctev_dest / ctev_evar) in
508 the evidence may *not* be fully zonked; we are careful not to look at it
509 during constraint solving. See Note [Evidence field of CtEvidence].
510
511 Note [Ct kind invariant]
512 ~~~~~~~~~~~~~~~~~~~~~~~~
513 CEqCan requires that the kind of the lhs matches the kind
514 of the rhs. This is necessary because these constraints are used for substitutions
515 during solving. If the kinds differed, then the substitution would take a well-kinded
516 type to an ill-kinded one.
517
518 Note [Holes]
519 ~~~~~~~~~~~~
520 This Note explains how GHC tracks *holes*.
521
522 A hole represents one of two conditions:
523 - A missing bit of an expression. Example: foo x = x + _
524 - A missing bit of a type. Example: bar :: Int -> _
525
526 What these have in common is that both cause GHC to emit a diagnostic to the
527 user describing the bit that is left out.
528
529 When a hole is encountered, a new entry of type Hole is added to the ambient
530 WantedConstraints. The type (hole_ty) of the hole is then simplified during
531 solving (with respect to any Givens in surrounding implications). It is
532 reported with all the other errors in GHC.Tc.Errors.
533
534 For expression holes, the user has the option of deferring errors until runtime
535 with -fdefer-type-errors. In this case, the hole actually has evidence: this
536 evidence is an erroring expression that prints an error and crashes at runtime.
537 The ExprHole variant of holes stores an IORef EvTerm that will contain this evidence;
538 during constraint generation, this IORef was stored in the HsUnboundVar extension
539 field by the type checker. The desugarer simply dereferences to get the CoreExpr.
540
541 Prior to fixing #17812, we used to invent an Id to hold the erroring
542 expression, and then bind it during type-checking. But this does not support
543 representation-polymorphic out-of-scope identifiers. See
544 typecheck/should_compile/T17812. We thus use the mutable-CoreExpr approach
545 described above.
546
547 You might think that the type in the HoleExprRef is the same as the type of the
548 hole. However, because the hole type (hole_ty) is rewritten with respect to
549 givens, this might not be the case. That is, the hole_ty is always (~) to the
550 type of the HoleExprRef, but they might not be `eqType`. We need the type of the generated
551 evidence to match what is expected in the context of the hole, and so we must
552 store these types separately.
553
554 Type-level holes have no evidence at all.
555 -}
556
557 mkNonCanonical :: CtEvidence -> Ct
558 mkNonCanonical ev = CNonCanonical { cc_ev = ev }
559
560 mkNonCanonicalCt :: Ct -> Ct
561 mkNonCanonicalCt ct = CNonCanonical { cc_ev = cc_ev ct }
562
563 mkIrredCt :: CtIrredReason -> CtEvidence -> Ct
564 mkIrredCt reason ev = CIrredCan { cc_ev = ev, cc_reason = reason }
565
566 mkGivens :: CtLoc -> [EvId] -> [Ct]
567 mkGivens loc ev_ids
568 = map mk ev_ids
569 where
570 mk ev_id = mkNonCanonical (CtGiven { ctev_evar = ev_id
571 , ctev_pred = evVarPred ev_id
572 , ctev_loc = loc })
573
574 ctEvidence :: Ct -> CtEvidence
575 ctEvidence (CQuantCan (QCI { qci_ev = ev })) = ev
576 ctEvidence ct = cc_ev ct
577
578 ctLoc :: Ct -> CtLoc
579 ctLoc = ctEvLoc . ctEvidence
580
581 setCtLoc :: Ct -> CtLoc -> Ct
582 setCtLoc ct loc = ct { cc_ev = (cc_ev ct) { ctev_loc = loc } }
583
584 ctOrigin :: Ct -> CtOrigin
585 ctOrigin = ctLocOrigin . ctLoc
586
587 ctPred :: Ct -> PredType
588 -- See Note [Ct/evidence invariant]
589 ctPred ct = ctEvPred (ctEvidence ct)
590
591 ctEvId :: Ct -> EvVar
592 -- The evidence Id for this Ct
593 ctEvId ct = ctEvEvId (ctEvidence ct)
594
595 -- | Makes a new equality predicate with the same role as the given
596 -- evidence.
597 mkTcEqPredLikeEv :: CtEvidence -> TcType -> TcType -> TcType
598 mkTcEqPredLikeEv ev
599 = case predTypeEqRel pred of
600 NomEq -> mkPrimEqPred
601 ReprEq -> mkReprPrimEqPred
602 where
603 pred = ctEvPred ev
604
605 -- | Get the flavour of the given 'Ct'
606 ctFlavour :: Ct -> CtFlavour
607 ctFlavour = ctEvFlavour . ctEvidence
608
609 -- | Get the equality relation for the given 'Ct'
610 ctEqRel :: Ct -> EqRel
611 ctEqRel = ctEvEqRel . ctEvidence
612
613 instance Outputable Ct where
614 ppr ct = ppr (ctEvidence ct) <+> parens pp_sort
615 where
616 pp_sort = case ct of
617 CEqCan {} -> text "CEqCan"
618 CNonCanonical {} -> text "CNonCanonical"
619 CDictCan { cc_pend_sc = psc, cc_fundeps = fds }
620 | psc, fds -> text "CDictCan(psc,fds)"
621 | psc, not fds -> text "CDictCan(psc)"
622 | not psc, fds -> text "CDictCan(fds)"
623 | otherwise -> text "CDictCan"
624 CIrredCan { cc_reason = reason } -> text "CIrredCan" <> ppr reason
625 CQuantCan (QCI { qci_pend_sc = pend_sc })
626 | pend_sc -> text "CQuantCan(psc)"
627 | otherwise -> text "CQuantCan"
628 CSpecialCan { cc_special_pred = special_pred } ->
629 text "CSpecialCan" <> parens (ppr special_pred)
630
631 -----------------------------------
632 -- | Is a type a canonical LHS? That is, is it a tyvar or an exactly-saturated
633 -- type family application?
634 -- Does not look through type synonyms.
635 canEqLHS_maybe :: Xi -> Maybe CanEqLHS
636 canEqLHS_maybe xi
637 | Just tv <- tcGetTyVar_maybe xi
638 = Just $ TyVarLHS tv
639
640 | Just (tc, args) <- tcSplitTyConApp_maybe xi
641 , isTypeFamilyTyCon tc
642 , args `lengthIs` tyConArity tc
643 = Just $ TyFamLHS tc args
644
645 | otherwise
646 = Nothing
647
648 -- | Convert a 'CanEqLHS' back into a 'Type'
649 canEqLHSType :: CanEqLHS -> TcType
650 canEqLHSType (TyVarLHS tv) = mkTyVarTy tv
651 canEqLHSType (TyFamLHS fam_tc fam_args) = mkTyConApp fam_tc fam_args
652
653 -- | Retrieve the kind of a 'CanEqLHS'
654 canEqLHSKind :: CanEqLHS -> TcKind
655 canEqLHSKind (TyVarLHS tv) = tyVarKind tv
656 canEqLHSKind (TyFamLHS fam_tc fam_args) = piResultTys (tyConKind fam_tc) fam_args
657
658 -- | Are two 'CanEqLHS's equal?
659 eqCanEqLHS :: CanEqLHS -> CanEqLHS -> Bool
660 eqCanEqLHS (TyVarLHS tv1) (TyVarLHS tv2) = tv1 == tv2
661 eqCanEqLHS (TyFamLHS fam_tc1 fam_args1) (TyFamLHS fam_tc2 fam_args2)
662 = tcEqTyConApps fam_tc1 fam_args1 fam_tc2 fam_args2
663 eqCanEqLHS _ _ = False
664
665 {-
666 ************************************************************************
667 * *
668 Simple functions over evidence variables
669 * *
670 ************************************************************************
671 -}
672
673 ---------------- Getting free tyvars -------------------------
674
675 -- | Returns free variables of constraints as a non-deterministic set
676 tyCoVarsOfCt :: Ct -> TcTyCoVarSet
677 tyCoVarsOfCt = fvVarSet . tyCoFVsOfCt
678
679 -- | Returns free variables of constraints as a deterministically ordered.
680 -- list. See Note [Deterministic FV] in "GHC.Utils.FV".
681 tyCoVarsOfCtList :: Ct -> [TcTyCoVar]
682 tyCoVarsOfCtList = fvVarList . tyCoFVsOfCt
683
684 -- | Returns free variables of constraints as a composable FV computation.
685 -- See Note [Deterministic FV] in "GHC.Utils.FV".
686 tyCoFVsOfCt :: Ct -> FV
687 tyCoFVsOfCt ct = tyCoFVsOfType (ctPred ct)
688 -- This must consult only the ctPred, so that it gets *tidied* fvs if the
689 -- constraint has been tidied. Tidying a constraint does not tidy the
690 -- fields of the Ct, only the predicate in the CtEvidence.
691
692 -- | Returns free variables of a bag of constraints as a non-deterministic
693 -- set. See Note [Deterministic FV] in "GHC.Utils.FV".
694 tyCoVarsOfCts :: Cts -> TcTyCoVarSet
695 tyCoVarsOfCts = fvVarSet . tyCoFVsOfCts
696
697 -- | Returns free variables of a bag of constraints as a deterministically
698 -- ordered list. See Note [Deterministic FV] in "GHC.Utils.FV".
699 tyCoVarsOfCtsList :: Cts -> [TcTyCoVar]
700 tyCoVarsOfCtsList = fvVarList . tyCoFVsOfCts
701
702 -- | Returns free variables of a bag of constraints as a composable FV
703 -- computation. See Note [Deterministic FV] in "GHC.Utils.FV".
704 tyCoFVsOfCts :: Cts -> FV
705 tyCoFVsOfCts = foldr (unionFV . tyCoFVsOfCt) emptyFV
706
707 -- | Returns free variables of WantedConstraints as a non-deterministic
708 -- set. See Note [Deterministic FV] in "GHC.Utils.FV".
709 tyCoVarsOfWC :: WantedConstraints -> TyCoVarSet
710 -- Only called on *zonked* things
711 tyCoVarsOfWC = fvVarSet . tyCoFVsOfWC
712
713 -- | Returns free variables of WantedConstraints as a deterministically
714 -- ordered list. See Note [Deterministic FV] in "GHC.Utils.FV".
715 tyCoVarsOfWCList :: WantedConstraints -> [TyCoVar]
716 -- Only called on *zonked* things
717 tyCoVarsOfWCList = fvVarList . tyCoFVsOfWC
718
719 -- | Returns free variables of WantedConstraints as a composable FV
720 -- computation. See Note [Deterministic FV] in "GHC.Utils.FV".
721 tyCoFVsOfWC :: WantedConstraints -> FV
722 -- Only called on *zonked* things
723 tyCoFVsOfWC (WC { wc_simple = simple, wc_impl = implic, wc_holes = holes })
724 = tyCoFVsOfCts simple `unionFV`
725 tyCoFVsOfBag tyCoFVsOfImplic implic `unionFV`
726 tyCoFVsOfBag tyCoFVsOfHole holes
727
728 -- | Returns free variables of Implication as a composable FV computation.
729 -- See Note [Deterministic FV] in "GHC.Utils.FV".
730 tyCoFVsOfImplic :: Implication -> FV
731 -- Only called on *zonked* things
732 tyCoFVsOfImplic (Implic { ic_skols = skols
733 , ic_given = givens
734 , ic_wanted = wanted })
735 | isEmptyWC wanted
736 = emptyFV
737 | otherwise
738 = tyCoFVsVarBndrs skols $
739 tyCoFVsVarBndrs givens $
740 tyCoFVsOfWC wanted
741
742 tyCoFVsOfHole :: Hole -> FV
743 tyCoFVsOfHole (Hole { hole_ty = ty }) = tyCoFVsOfType ty
744
745 tyCoFVsOfBag :: (a -> FV) -> Bag a -> FV
746 tyCoFVsOfBag tvs_of = foldr (unionFV . tvs_of) emptyFV
747
748 ---------------------------
749 dropDerivedWC :: WantedConstraints -> WantedConstraints
750 -- See Note [Dropping derived constraints]
751 dropDerivedWC wc@(WC { wc_simple = simples })
752 = wc { wc_simple = dropDerivedSimples simples }
753 -- The wc_impl implications are already (recursively) filtered
754
755 --------------------------
756 dropDerivedSimples :: Cts -> Cts
757 -- Drop all Derived constraints, but make [W] back into [WD],
758 -- so that if we re-simplify these constraints we will get all
759 -- the right derived constraints re-generated. Forgetting this
760 -- step led to #12936
761 dropDerivedSimples simples = mapMaybeBag dropDerivedCt simples
762
763 dropDerivedCt :: Ct -> Maybe Ct
764 dropDerivedCt ct
765 = case ctEvFlavour ev of
766 Wanted WOnly -> Just (ct' { cc_ev = ev_wd })
767 Wanted _ -> Just ct'
768 _ | isDroppableCt ct -> Nothing
769 | otherwise -> Just ct
770 where
771 ev = ctEvidence ct
772 ev_wd = ev { ctev_nosh = WDeriv }
773 ct' = setPendingScDict ct -- See Note [Resetting cc_pend_sc]
774
775 {- Note [Resetting cc_pend_sc]
776 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
777 When we discard Derived constraints, in dropDerivedSimples, we must
778 set the cc_pend_sc flag to True, so that if we re-process this
779 CDictCan we will re-generate its derived superclasses. Otherwise
780 we might miss some fundeps. #13662 showed this up.
781
782 See Note [The superclass story] in GHC.Tc.Solver.Canonical.
783 -}
784
785 isDroppableCt :: Ct -> Bool
786 isDroppableCt ct
787 = isDerived ev && not keep_deriv
788 -- Drop only derived constraints, and then only if they
789 -- obey Note [Dropping derived constraints]
790 where
791 ev = ctEvidence ct
792 loc = ctEvLoc ev
793 orig = ctLocOrigin loc
794
795 keep_deriv
796 = case ct of
797 CIrredCan { cc_reason = reason } | isInsolubleReason reason -> keep_eq True
798 _ -> keep_eq False
799
800 keep_eq definitely_insoluble
801 | isGivenOrigin orig -- Arising only from givens
802 = definitely_insoluble -- Keep only definitely insoluble
803 | otherwise
804 = case orig of
805 -- See Note [Dropping derived constraints]
806 -- For fundeps, drop wanted/wanted interactions
807 FunDepOrigin2 {} -> True -- Top-level/Wanted
808 FunDepOrigin1 _ orig1 _ _ orig2 _
809 | g1 || g2 -> True -- Given/Wanted errors: keep all
810 | otherwise -> False -- Wanted/Wanted errors: discard
811 where
812 g1 = isGivenOrigin orig1
813 g2 = isGivenOrigin orig2
814
815 _ -> False
816
817 arisesFromGivens :: Ct -> Bool
818 arisesFromGivens ct
819 = case ctEvidence ct of
820 CtGiven {} -> True
821 CtWanted {} -> False
822 CtDerived { ctev_loc = loc } -> isGivenLoc loc
823
824 isGivenLoc :: CtLoc -> Bool
825 isGivenLoc loc = isGivenOrigin (ctLocOrigin loc)
826
827 {- Note [Dropping derived constraints]
828 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
829 In general we discard derived constraints at the end of constraint solving;
830 see dropDerivedWC. For example
831
832 * Superclasses: if we have an unsolved [W] (Ord a), we don't want to
833 complain about an unsolved [D] (Eq a) as well.
834
835 * If we have [W] a ~ Int, [W] a ~ Bool, improvement will generate
836 [D] Int ~ Bool, and we don't want to report that because it's
837 incomprehensible. That is why we don't rewrite wanteds with wanteds!
838
839 * We might float out some Wanteds from an implication, leaving behind
840 their insoluble Deriveds. For example:
841
842 forall a[2]. [W] alpha[1] ~ Int
843 [W] alpha[1] ~ Bool
844 [D] Int ~ Bool
845
846 The Derived is insoluble, but we very much want to drop it when floating
847 out.
848
849 But (tiresomely) we do keep *some* Derived constraints:
850
851 * Type holes are derived constraints, because they have no evidence
852 and we want to keep them, so we get the error report
853
854 * We keep most derived equalities arising from functional dependencies
855 - Given/Given interactions (subset of FunDepOrigin1):
856 The definitely-insoluble ones reflect unreachable code.
857
858 Others not-definitely-insoluble ones like [D] a ~ Int do not
859 reflect unreachable code; indeed if fundeps generated proofs, it'd
860 be a useful equality. See #14763. So we discard them.
861
862 - Given/Wanted interacGiven or Wanted interacting with an
863 instance declaration (FunDepOrigin2)
864
865 - Given/Wanted interactions (FunDepOrigin1); see #9612
866
867 - But for Wanted/Wanted interactions we do /not/ want to report an
868 error (#13506). Consider [W] C Int Int, [W] C Int Bool, with
869 a fundep on class C. We don't want to report an insoluble Int~Bool;
870 c.f. "wanteds do not rewrite wanteds".
871
872 To distinguish these cases we use the CtOrigin.
873
874 NB: we keep *all* derived insolubles under some circumstances:
875
876 * They are looked at by simplifyInfer, to decide whether to
877 generalise. Example: [W] a ~ Int, [W] a ~ Bool
878 We get [D] Int ~ Bool, and indeed the constraints are insoluble,
879 and we want simplifyInfer to see that, even though we don't
880 ultimately want to generate an (inexplicable) error message from it
881
882
883 ************************************************************************
884 * *
885 CtEvidence
886 The "flavor" of a canonical constraint
887 * *
888 ************************************************************************
889 -}
890
891 isWantedCt :: Ct -> Bool
892 isWantedCt = isWanted . ctEvidence
893
894 isGivenCt :: Ct -> Bool
895 isGivenCt = isGiven . ctEvidence
896
897 isDerivedCt :: Ct -> Bool
898 isDerivedCt = isDerived . ctEvidence
899
900 {- Note [Custom type errors in constraints]
901 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
902
903 When GHC reports a type-error about an unsolved-constraint, we check
904 to see if the constraint contains any custom-type errors, and if so
905 we report them. Here are some examples of constraints containing type
906 errors:
907
908 TypeError msg -- The actual constraint is a type error
909
910 TypError msg ~ Int -- Some type was supposed to be Int, but ended up
911 -- being a type error instead
912
913 Eq (TypeError msg) -- A class constraint is stuck due to a type error
914
915 F (TypeError msg) ~ a -- A type function failed to evaluate due to a type err
916
917 It is also possible to have constraints where the type error is nested deeper,
918 for example see #11990, and also:
919
920 Eq (F (TypeError msg)) -- Here the type error is nested under a type-function
921 -- call, which failed to evaluate because of it,
922 -- and so the `Eq` constraint was unsolved.
923 -- This may happen when one function calls another
924 -- and the called function produced a custom type error.
925 -}
926
927 -- | A constraint is considered to be a custom type error, if it contains
928 -- custom type errors anywhere in it.
929 -- See Note [Custom type errors in constraints]
930 getUserTypeErrorMsg :: Ct -> Maybe Type
931 getUserTypeErrorMsg ct = findUserTypeError (ctPred ct)
932 where
933 findUserTypeError t = msum ( userTypeError_maybe t
934 : map findUserTypeError (subTys t)
935 )
936
937 subTys t = case splitAppTys t of
938 (t,[]) ->
939 case splitTyConApp_maybe t of
940 Nothing -> []
941 Just (_,ts) -> ts
942 (t,ts) -> t : ts
943
944
945
946
947 isUserTypeErrorCt :: Ct -> Bool
948 isUserTypeErrorCt ct = case getUserTypeErrorMsg ct of
949 Just _ -> True
950 _ -> False
951
952 isPendingScDict :: Ct -> Maybe Ct
953 -- Says whether this is a CDictCan with cc_pend_sc is True,
954 -- AND if so flips the flag
955 isPendingScDict ct@(CDictCan { cc_pend_sc = True })
956 = Just (ct { cc_pend_sc = False })
957 isPendingScDict _ = Nothing
958
959 isPendingScInst :: QCInst -> Maybe QCInst
960 -- Same as isPendingScDict, but for QCInsts
961 isPendingScInst qci@(QCI { qci_pend_sc = True })
962 = Just (qci { qci_pend_sc = False })
963 isPendingScInst _ = Nothing
964
965 setPendingScDict :: Ct -> Ct
966 -- Set the cc_pend_sc flag to True
967 setPendingScDict ct@(CDictCan { cc_pend_sc = False })
968 = ct { cc_pend_sc = True }
969 setPendingScDict ct = ct
970
971 superClassesMightHelp :: WantedConstraints -> Bool
972 -- ^ True if taking superclasses of givens, or of wanteds (to perhaps
973 -- expose more equalities or functional dependencies) might help to
974 -- solve this constraint. See Note [When superclasses help]
975 superClassesMightHelp (WC { wc_simple = simples, wc_impl = implics })
976 = anyBag might_help_ct simples || anyBag might_help_implic implics
977 where
978 might_help_implic ic
979 | IC_Unsolved <- ic_status ic = superClassesMightHelp (ic_wanted ic)
980 | otherwise = False
981
982 might_help_ct ct = isWantedCt ct && not (is_ip ct)
983
984 is_ip (CDictCan { cc_class = cls }) = isIPClass cls
985 is_ip _ = False
986
987 getPendingWantedScs :: Cts -> ([Ct], Cts)
988 getPendingWantedScs simples
989 = mapAccumBagL get [] simples
990 where
991 get acc ct | Just ct' <- isPendingScDict ct
992 = (ct':acc, ct')
993 | otherwise
994 = (acc, ct)
995
996 {- Note [When superclasses help]
997 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
998 First read Note [The superclass story] in GHC.Tc.Solver.Canonical.
999
1000 We expand superclasses and iterate only if there is at unsolved wanted
1001 for which expansion of superclasses (e.g. from given constraints)
1002 might actually help. The function superClassesMightHelp tells if
1003 doing this superclass expansion might help solve this constraint.
1004 Note that
1005
1006 * We look inside implications; maybe it'll help to expand the Givens
1007 at level 2 to help solve an unsolved Wanted buried inside an
1008 implication. E.g.
1009 forall a. Ord a => forall b. [W] Eq a
1010
1011 * Superclasses help only for Wanted constraints. Derived constraints
1012 are not really "unsolved" and we certainly don't want them to
1013 trigger superclass expansion. This was a good part of the loop
1014 in #11523
1015
1016 * Even for Wanted constraints, we say "no" for implicit parameters.
1017 we have [W] ?x::ty, expanding superclasses won't help:
1018 - Superclasses can't be implicit parameters
1019 - If we have a [G] ?x:ty2, then we'll have another unsolved
1020 [D] ty ~ ty2 (from the functional dependency)
1021 which will trigger superclass expansion.
1022
1023 It's a bit of a special case, but it's easy to do. The runtime cost
1024 is low because the unsolved set is usually empty anyway (errors
1025 aside), and the first non-implicit-parameter will terminate the search.
1026
1027 The special case is worth it (#11480, comment:2) because it
1028 applies to CallStack constraints, which aren't type errors. If we have
1029 f :: (C a) => blah
1030 f x = ...undefined...
1031 we'll get a CallStack constraint. If that's the only unsolved
1032 constraint it'll eventually be solved by defaulting. So we don't
1033 want to emit warnings about hitting the simplifier's iteration
1034 limit. A CallStack constraint really isn't an unsolved
1035 constraint; it can always be solved by defaulting.
1036 -}
1037
1038 singleCt :: Ct -> Cts
1039 singleCt = unitBag
1040
1041 andCts :: Cts -> Cts -> Cts
1042 andCts = unionBags
1043
1044 listToCts :: [Ct] -> Cts
1045 listToCts = listToBag
1046
1047 ctsElts :: Cts -> [Ct]
1048 ctsElts = bagToList
1049
1050 consCts :: Ct -> Cts -> Cts
1051 consCts = consBag
1052
1053 snocCts :: Cts -> Ct -> Cts
1054 snocCts = snocBag
1055
1056 extendCtsList :: Cts -> [Ct] -> Cts
1057 extendCtsList cts xs | null xs = cts
1058 | otherwise = cts `unionBags` listToBag xs
1059
1060 andManyCts :: [Cts] -> Cts
1061 andManyCts = unionManyBags
1062
1063 emptyCts :: Cts
1064 emptyCts = emptyBag
1065
1066 isEmptyCts :: Cts -> Bool
1067 isEmptyCts = isEmptyBag
1068
1069 pprCts :: Cts -> SDoc
1070 pprCts cts = vcat (map ppr (bagToList cts))
1071
1072 {-
1073 ************************************************************************
1074 * *
1075 Wanted constraints
1076 These are forced to be in GHC.Tc.Types because
1077 TcLclEnv mentions WantedConstraints
1078 WantedConstraint mentions CtLoc
1079 CtLoc mentions ErrCtxt
1080 ErrCtxt mentions TcM
1081 * *
1082 v%************************************************************************
1083 -}
1084
1085 data WantedConstraints
1086 = WC { wc_simple :: Cts -- Unsolved constraints, all wanted
1087 , wc_impl :: Bag Implication
1088 , wc_holes :: Bag Hole
1089 }
1090
1091 emptyWC :: WantedConstraints
1092 emptyWC = WC { wc_simple = emptyBag
1093 , wc_impl = emptyBag
1094 , wc_holes = emptyBag }
1095
1096 mkSimpleWC :: [CtEvidence] -> WantedConstraints
1097 mkSimpleWC cts
1098 = emptyWC { wc_simple = listToBag (map mkNonCanonical cts) }
1099
1100 mkImplicWC :: Bag Implication -> WantedConstraints
1101 mkImplicWC implic
1102 = emptyWC { wc_impl = implic }
1103
1104 isEmptyWC :: WantedConstraints -> Bool
1105 isEmptyWC (WC { wc_simple = f, wc_impl = i, wc_holes = holes })
1106 = isEmptyBag f && isEmptyBag i && isEmptyBag holes
1107
1108 -- | Checks whether a the given wanted constraints are solved, i.e.
1109 -- that there are no simple constraints left and all the implications
1110 -- are solved.
1111 isSolvedWC :: WantedConstraints -> Bool
1112 isSolvedWC WC {wc_simple = wc_simple, wc_impl = wc_impl, wc_holes = holes} =
1113 isEmptyBag wc_simple && allBag (isSolvedStatus . ic_status) wc_impl && isEmptyBag holes
1114
1115 andWC :: WantedConstraints -> WantedConstraints -> WantedConstraints
1116 andWC (WC { wc_simple = f1, wc_impl = i1, wc_holes = h1 })
1117 (WC { wc_simple = f2, wc_impl = i2, wc_holes = h2 })
1118 = WC { wc_simple = f1 `unionBags` f2
1119 , wc_impl = i1 `unionBags` i2
1120 , wc_holes = h1 `unionBags` h2 }
1121
1122 unionsWC :: [WantedConstraints] -> WantedConstraints
1123 unionsWC = foldr andWC emptyWC
1124
1125 addSimples :: WantedConstraints -> Bag Ct -> WantedConstraints
1126 addSimples wc cts
1127 = wc { wc_simple = wc_simple wc `unionBags` cts }
1128 -- Consider: Put the new constraints at the front, so they get solved first
1129
1130 addImplics :: WantedConstraints -> Bag Implication -> WantedConstraints
1131 addImplics wc implic = wc { wc_impl = wc_impl wc `unionBags` implic }
1132
1133 addInsols :: WantedConstraints -> Bag Ct -> WantedConstraints
1134 addInsols wc cts
1135 = wc { wc_simple = wc_simple wc `unionBags` cts }
1136
1137 addHoles :: WantedConstraints -> Bag Hole -> WantedConstraints
1138 addHoles wc holes
1139 = wc { wc_holes = holes `unionBags` wc_holes wc }
1140
1141 dropMisleading :: WantedConstraints -> WantedConstraints
1142 -- Drop misleading constraints; really just class constraints
1143 -- See Note [Constraints and errors] in GHC.Tc.Utils.Monad
1144 -- for why this function is so strange, treating the 'simples'
1145 -- and the implications differently. Sigh.
1146 dropMisleading (WC { wc_simple = simples, wc_impl = implics, wc_holes = holes })
1147 = WC { wc_simple = filterBag insolubleWantedCt simples
1148 , wc_impl = mapBag drop_implic implics
1149 , wc_holes = filterBag isOutOfScopeHole holes }
1150 where
1151 drop_implic implic
1152 = implic { ic_wanted = drop_wanted (ic_wanted implic) }
1153 drop_wanted (WC { wc_simple = simples, wc_impl = implics, wc_holes = holes })
1154 = WC { wc_simple = filterBag keep_ct simples
1155 , wc_impl = mapBag drop_implic implics
1156 , wc_holes = filterBag isOutOfScopeHole holes }
1157
1158 keep_ct ct = case classifyPredType (ctPred ct) of
1159 ClassPred {} -> False
1160 _ -> True
1161
1162 isSolvedStatus :: ImplicStatus -> Bool
1163 isSolvedStatus (IC_Solved {}) = True
1164 isSolvedStatus _ = False
1165
1166 isInsolubleStatus :: ImplicStatus -> Bool
1167 isInsolubleStatus IC_Insoluble = True
1168 isInsolubleStatus IC_BadTelescope = True
1169 isInsolubleStatus _ = False
1170
1171 insolubleImplic :: Implication -> Bool
1172 insolubleImplic ic = isInsolubleStatus (ic_status ic)
1173
1174 insolubleWC :: WantedConstraints -> Bool
1175 insolubleWC (WC { wc_impl = implics, wc_simple = simples, wc_holes = holes })
1176 = anyBag insolubleWantedCt simples
1177 || anyBag insolubleImplic implics
1178 || anyBag isOutOfScopeHole holes -- See Note [Insoluble holes]
1179
1180 insolubleWantedCt :: Ct -> Bool
1181 -- Definitely insoluble, in particular /excluding/ type-hole constraints
1182 -- Namely:
1183 -- a) an insoluble constraint as per 'insolubleCt', i.e. either
1184 -- - an insoluble equality constraint (e.g. Int ~ Bool), or
1185 -- - a custom type error constraint, TypeError msg :: Constraint
1186 -- b) that does not arise from a Given
1187 --
1188 -- See Note [Given insolubles].
1189 insolubleWantedCt ct = insolubleCt ct && not (arisesFromGivens ct)
1190
1191 insolubleEqCt :: Ct -> Bool
1192 -- Returns True of /equality/ constraints
1193 -- that are /definitely/ insoluble
1194 -- It won't detect some definite errors like
1195 -- F a ~ T (F a)
1196 -- where F is a type family, which actually has an occurs check
1197 --
1198 -- The function is tuned for application /after/ constraint solving
1199 -- i.e. assuming canonicalisation has been done
1200 -- E.g. It'll reply True for a ~ [a]
1201 -- but False for [a] ~ a
1202 -- and
1203 -- True for Int ~ F a Int
1204 -- but False for Maybe Int ~ F a Int Int
1205 -- (where F is an arity-1 type function)
1206 insolubleEqCt (CIrredCan { cc_reason = reason }) = isInsolubleReason reason
1207 insolubleEqCt _ = False
1208
1209 -- | Returns True of equality constraints that are definitely insoluble,
1210 -- as well as TypeError constraints.
1211 -- Can return 'True' for Given constraints, unlike 'insolubleWantedCt'.
1212 --
1213 -- This function is critical for accurate pattern-match overlap warnings.
1214 -- See Note [Pattern match warnings with insoluble Givens] in GHC.Tc.Solver
1215 --
1216 -- Note that this does not traverse through the constraint to find
1217 -- nested custom type errors: it only detects @TypeError msg :: Constraint@,
1218 -- and not e.g. @Eq (TypeError msg)@.
1219 insolubleCt :: Ct -> Bool
1220 insolubleCt ct
1221 | Just _ <- userTypeError_maybe (ctPred ct)
1222 -- Don't use 'isUserTypeErrorCt' here, as that function is too eager:
1223 -- the TypeError might appear inside a type family application
1224 -- which might later reduce, but we only want to return 'True'
1225 -- for constraints that are definitely insoluble.
1226 --
1227 -- Test case: T11503, with the 'Assert' type family:
1228 --
1229 -- > type Assert :: Bool -> Constraint -> Constraint
1230 -- > type family Assert check errMsg where
1231 -- > Assert 'True _errMsg = ()
1232 -- > Assert _check errMsg = errMsg
1233 = True
1234 | otherwise
1235 = insolubleEqCt ct
1236
1237 -- | Does this hole represent an "out of scope" error?
1238 -- See Note [Insoluble holes]
1239 isOutOfScopeHole :: Hole -> Bool
1240 isOutOfScopeHole (Hole { hole_occ = occ }) = not (startsWithUnderscore occ)
1241
1242 instance Outputable WantedConstraints where
1243 ppr (WC {wc_simple = s, wc_impl = i, wc_holes = h})
1244 = text "WC" <+> braces (vcat
1245 [ ppr_bag (text "wc_simple") s
1246 , ppr_bag (text "wc_impl") i
1247 , ppr_bag (text "wc_holes") h ])
1248
1249 ppr_bag :: Outputable a => SDoc -> Bag a -> SDoc
1250 ppr_bag doc bag
1251 | isEmptyBag bag = empty
1252 | otherwise = hang (doc <+> equals)
1253 2 (foldr (($$) . ppr) empty bag)
1254
1255 {- Note [Given insolubles]
1256 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1257 Consider (#14325, comment:)
1258 class (a~b) => C a b
1259
1260 foo :: C a c => a -> c
1261 foo x = x
1262
1263 hm3 :: C (f b) b => b -> f b
1264 hm3 x = foo x
1265
1266 In the RHS of hm3, from the [G] C (f b) b we get the insoluble
1267 [G] f b ~# b. Then we also get an unsolved [W] C b (f b).
1268 Residual implication looks like
1269 forall b. C (f b) b => [G] f b ~# b
1270 [W] C f (f b)
1271
1272 We do /not/ want to set the implication status to IC_Insoluble,
1273 because that'll suppress reports of [W] C b (f b). But we
1274 may not report the insoluble [G] f b ~# b either (see Note [Given errors]
1275 in GHC.Tc.Errors), so we may fail to report anything at all! Yikes.
1276
1277 The same applies to Derived constraints that /arise from/ Givens.
1278 E.g. f :: (C Int [a]) => blah
1279 where a fundep means we get
1280 [D] Int ~ [a]
1281 By the same reasoning we must not suppress other errors (#15767)
1282
1283 Bottom line: insolubleWC (called in GHC.Tc.Solver.setImplicationStatus)
1284 should ignore givens even if they are insoluble.
1285
1286 Note [Insoluble holes]
1287 ~~~~~~~~~~~~~~~~~~~~~~
1288 Hole constraints that ARE NOT treated as truly insoluble:
1289 a) type holes, arising from PartialTypeSignatures,
1290 b) "true" expression holes arising from TypedHoles
1291
1292 An "expression hole" or "type hole" isn't really an error
1293 at all; it's a report saying "_ :: Int" here. But an out-of-scope
1294 variable masquerading as expression holes IS treated as truly
1295 insoluble, so that it trumps other errors during error reporting.
1296 Yuk!
1297
1298 ************************************************************************
1299 * *
1300 Implication constraints
1301 * *
1302 ************************************************************************
1303 -}
1304
1305 data Implication
1306 = Implic { -- Invariants for a tree of implications:
1307 -- see TcType Note [TcLevel invariants]
1308
1309 ic_tclvl :: TcLevel, -- TcLevel of unification variables
1310 -- allocated /inside/ this implication
1311
1312 ic_skols :: [TcTyVar], -- Introduced skolems
1313 ic_info :: SkolemInfo, -- See Note [Skolems in an implication]
1314 -- See Note [Shadowing in a constraint]
1315
1316 ic_given :: [EvVar], -- Given evidence variables
1317 -- (order does not matter)
1318 -- See Invariant (GivenInv) in GHC.Tc.Utils.TcType
1319
1320 ic_given_eqs :: HasGivenEqs, -- Are there Given equalities here?
1321
1322 ic_warn_inaccessible :: Bool,
1323 -- True <=> -Winaccessible-code is enabled
1324 -- at construction. See
1325 -- Note [Avoid -Winaccessible-code when deriving]
1326 -- in GHC.Tc.TyCl.Instance
1327
1328 ic_env :: TcLclEnv,
1329 -- Records the TcLClEnv at the time of creation.
1330 --
1331 -- The TcLclEnv gives the source location
1332 -- and error context for the implication, and
1333 -- hence for all the given evidence variables.
1334
1335 ic_wanted :: WantedConstraints, -- The wanteds
1336 -- See Invariang (WantedInf) in GHC.Tc.Utils.TcType
1337
1338 ic_binds :: EvBindsVar, -- Points to the place to fill in the
1339 -- abstraction and bindings.
1340
1341 -- The ic_need fields keep track of which Given evidence
1342 -- is used by this implication or its children
1343 -- NB: including stuff used by nested implications that have since
1344 -- been discarded
1345 -- See Note [Needed evidence variables]
1346 ic_need_inner :: VarSet, -- Includes all used Given evidence
1347 ic_need_outer :: VarSet, -- Includes only the free Given evidence
1348 -- i.e. ic_need_inner after deleting
1349 -- (a) givens (b) binders of ic_binds
1350
1351 ic_status :: ImplicStatus
1352 }
1353
1354 implicationPrototype :: Implication
1355 implicationPrototype
1356 = Implic { -- These fields must be initialised
1357 ic_tclvl = panic "newImplic:tclvl"
1358 , ic_binds = panic "newImplic:binds"
1359 , ic_info = panic "newImplic:info"
1360 , ic_env = panic "newImplic:env"
1361 , ic_warn_inaccessible = panic "newImplic:warn_inaccessible"
1362
1363 -- The rest have sensible default values
1364 , ic_skols = []
1365 , ic_given = []
1366 , ic_wanted = emptyWC
1367 , ic_given_eqs = MaybeGivenEqs
1368 , ic_status = IC_Unsolved
1369 , ic_need_inner = emptyVarSet
1370 , ic_need_outer = emptyVarSet }
1371
1372 data ImplicStatus
1373 = IC_Solved -- All wanteds in the tree are solved, all the way down
1374 { ics_dead :: [EvVar] } -- Subset of ic_given that are not needed
1375 -- See Note [Tracking redundant constraints] in GHC.Tc.Solver
1376
1377 | IC_Insoluble -- At least one insoluble constraint in the tree
1378
1379 | IC_BadTelescope -- Solved, but the skolems in the telescope are out of
1380 -- dependency order. See Note [Checking telescopes]
1381
1382 | IC_Unsolved -- Neither of the above; might go either way
1383
1384 data HasGivenEqs -- See Note [HasGivenEqs]
1385 = NoGivenEqs -- Definitely no given equalities,
1386 -- except by Note [Let-bound skolems] in GHC.Tc.Solver.InertSet
1387 | LocalGivenEqs -- Might have Given equalities, but only ones that affect only
1388 -- local skolems e.g. forall a b. (a ~ F b) => ...
1389 | MaybeGivenEqs -- Might have any kind of Given equalities; no floating out
1390 -- is possible.
1391 deriving Eq
1392
1393 {- Note [HasGivenEqs]
1394 ~~~~~~~~~~~~~~~~~~~~~
1395 The GivenEqs data type describes the Given constraints of an implication constraint:
1396
1397 * NoGivenEqs: definitely no Given equalities, except perhaps let-bound skolems
1398 which don't count: see Note [Let-bound skolems] in GHC.Tc.Solver.InertSet
1399 Examples: forall a. Eq a => ...
1400 forall a. (Show a, Num a) => ...
1401 forall a. a ~ Either Int Bool => ... -- Let-bound skolem
1402
1403 * LocalGivenEqs: definitely no Given equalities that would affect principal
1404 types. But may have equalities that affect only skolems of this implication
1405 (and hence do not affect princial types)
1406 Examples: forall a. F a ~ Int => ...
1407 forall a b. F a ~ G b => ...
1408
1409 * MaybeGivenEqs: may have Given equalities that would affect principal
1410 types
1411 Examples: forall. (a ~ b) => ...
1412 forall a. F a ~ b => ...
1413 forall a. c a => ... -- The 'c' might be instantiated to (b ~)
1414 forall a. C a b => ....
1415 where class x~y => C a b
1416 so there is an equality in the superclass of a Given
1417
1418 The HasGivenEqs classifications affect two things:
1419
1420 * Suppressing redundant givens during error reporting; see GHC.Tc.Errors
1421 Note [Suppress redundant givens during error reporting]
1422
1423 * Floating in approximateWC.
1424
1425 Specifically, here's how it goes:
1426
1427 Stops floating | Suppresses Givens in errors
1428 in approximateWC |
1429 -----------------------------------------------
1430 NoGivenEqs NO | YES
1431 LocalGivenEqs NO | NO
1432 MaybeGivenEqs YES | NO
1433 -}
1434
1435 instance Outputable Implication where
1436 ppr (Implic { ic_tclvl = tclvl, ic_skols = skols
1437 , ic_given = given, ic_given_eqs = given_eqs
1438 , ic_wanted = wanted, ic_status = status
1439 , ic_binds = binds
1440 , ic_need_inner = need_in, ic_need_outer = need_out
1441 , ic_info = info })
1442 = hang (text "Implic" <+> lbrace)
1443 2 (sep [ text "TcLevel =" <+> ppr tclvl
1444 , text "Skolems =" <+> pprTyVars skols
1445 , text "Given-eqs =" <+> ppr given_eqs
1446 , text "Status =" <+> ppr status
1447 , hang (text "Given =") 2 (pprEvVars given)
1448 , hang (text "Wanted =") 2 (ppr wanted)
1449 , text "Binds =" <+> ppr binds
1450 , whenPprDebug (text "Needed inner =" <+> ppr need_in)
1451 , whenPprDebug (text "Needed outer =" <+> ppr need_out)
1452 , pprSkolInfo info ] <+> rbrace)
1453
1454 instance Outputable ImplicStatus where
1455 ppr IC_Insoluble = text "Insoluble"
1456 ppr IC_BadTelescope = text "Bad telescope"
1457 ppr IC_Unsolved = text "Unsolved"
1458 ppr (IC_Solved { ics_dead = dead })
1459 = text "Solved" <+> (braces (text "Dead givens =" <+> ppr dead))
1460
1461 checkTelescopeSkol :: SkolemInfo -> Bool
1462 -- See Note [Checking telescopes]
1463 checkTelescopeSkol (ForAllSkol {}) = True
1464 checkTelescopeSkol _ = False
1465
1466 instance Outputable HasGivenEqs where
1467 ppr NoGivenEqs = text "NoGivenEqs"
1468 ppr LocalGivenEqs = text "LocalGivenEqs"
1469 ppr MaybeGivenEqs = text "MaybeGivenEqs"
1470
1471 -- Used in GHC.Tc.Solver.Monad.getHasGivenEqs
1472 instance Semigroup HasGivenEqs where
1473 NoGivenEqs <> other = other
1474 other <> NoGivenEqs = other
1475
1476 MaybeGivenEqs <> _other = MaybeGivenEqs
1477 _other <> MaybeGivenEqs = MaybeGivenEqs
1478
1479 LocalGivenEqs <> LocalGivenEqs = LocalGivenEqs
1480
1481 -- Used in GHC.Tc.Solver.Monad.getHasGivenEqs
1482 instance Monoid HasGivenEqs where
1483 mempty = NoGivenEqs
1484
1485 {- Note [Checking telescopes]
1486 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1487 When kind-checking a /user-written/ type, we might have a "bad telescope"
1488 like this one:
1489 data SameKind :: forall k. k -> k -> Type
1490 type Foo :: forall a k (b :: k). SameKind a b -> Type
1491
1492 The kind of 'a' mentions 'k' which is bound after 'a'. Oops.
1493
1494 One approach to doing this would be to bring each of a, k, and b into
1495 scope, one at a time, creating a separate implication constraint for
1496 each one, and bumping the TcLevel. This would work, because the kind
1497 of, say, a would be untouchable when k is in scope (and the constraint
1498 couldn't float out because k blocks it). However, it leads to terrible
1499 error messages, complaining about skolem escape. While it is indeed a
1500 problem of skolem escape, we can do better.
1501
1502 Instead, our approach is to bring the block of variables into scope
1503 all at once, creating one implication constraint for the lot:
1504
1505 * We make a single implication constraint when kind-checking
1506 the 'forall' in Foo's kind, something like
1507 forall a k (b::k). { wanted constraints }
1508
1509 * Having solved {wanted}, before discarding the now-solved implication,
1510 the constraint solver checks the dependency order of the skolem
1511 variables (ic_skols). This is done in setImplicationStatus.
1512
1513 * This check is only necessary if the implication was born from a
1514 'forall' in a user-written signature (the HsForAllTy case in
1515 GHC.Tc.Gen.HsType. If, say, it comes from checking a pattern match
1516 that binds existentials, where the type of the data constructor is
1517 known to be valid (it in tcConPat), no need for the check.
1518
1519 So the check is done /if and only if/ ic_info is ForAllSkol.
1520
1521 * If ic_info is (ForAllSkol dt dvs), the dvs::SDoc displays the
1522 original, user-written type variables.
1523
1524 * Be careful /NOT/ to discard an implication with a ForAllSkol
1525 ic_info, even if ic_wanted is empty. We must give the
1526 constraint solver a chance to make that bad-telescope test! Hence
1527 the extra guard in emitResidualTvConstraint; see #16247
1528
1529 * Don't mix up inferred and explicit variables in the same implication
1530 constraint. E.g.
1531 foo :: forall a kx (b :: kx). SameKind a b
1532 We want an implication
1533 Implic { ic_skol = [(a::kx), kx, (b::kx)], ... }
1534 but GHC will attempt to quantify over kx, since it is free in (a::kx),
1535 and it's hopelessly confusing to report an error about quantified
1536 variables kx (a::kx) kx (b::kx).
1537 Instead, the outer quantification over kx should be in a separate
1538 implication. TL;DR: an explicit forall should generate an implication
1539 quantified only over those explicitly quantified variables.
1540
1541 Note [Needed evidence variables]
1542 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1543 Th ic_need_evs field holds the free vars of ic_binds, and all the
1544 ic_binds in nested implications.
1545
1546 * Main purpose: if one of the ic_givens is not mentioned in here, it
1547 is redundant.
1548
1549 * solveImplication may drop an implication altogether if it has no
1550 remaining 'wanteds'. But we still track the free vars of its
1551 evidence binds, even though it has now disappeared.
1552
1553 Note [Shadowing in a constraint]
1554 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1555 We assume NO SHADOWING in a constraint. Specifically
1556 * The unification variables are all implicitly quantified at top
1557 level, and are all unique
1558 * The skolem variables bound in ic_skols are all freah when the
1559 implication is created.
1560 So we can safely substitute. For example, if we have
1561 forall a. a~Int => ...(forall b. ...a...)...
1562 we can push the (a~Int) constraint inwards in the "givens" without
1563 worrying that 'b' might clash.
1564
1565 Note [Skolems in an implication]
1566 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1567 The skolems in an implication are used:
1568
1569 * When considering floating a constraint outside the implication in
1570 GHC.Tc.Solver.floatEqualities or GHC.Tc.Solver.approximateImplications
1571 For this, we can treat ic_skols as a set.
1572
1573 * When checking that a /user-specified/ forall (ic_info = ForAllSkol tvs)
1574 has its variables in the correct order; see Note [Checking telescopes].
1575 Only for these implications does ic_skols need to be a list.
1576
1577 Nota bene: Although ic_skols is a list, it is not necessarily
1578 in dependency order:
1579 - In the ic_info=ForAllSkol case, the user might have written them
1580 in the wrong order
1581 - In the case of a type signature like
1582 f :: [a] -> [b]
1583 the renamer gathers the implicit "outer" forall'd variables {a,b}, but
1584 does not know what order to put them in. The type checker can sort them
1585 into dependency order, but only after solving all the kind constraints;
1586 and to do that it's convenient to create the Implication!
1587
1588 So we accept that ic_skols may be out of order. Think of it as a set or
1589 (in the case of ic_info=ForAllSkol, a list in user-specified, and possibly
1590 wrong, order.
1591
1592 Note [Insoluble constraints]
1593 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1594 Some of the errors that we get during canonicalization are best
1595 reported when all constraints have been simplified as much as
1596 possible. For instance, assume that during simplification the
1597 following constraints arise:
1598
1599 [Wanted] F alpha ~ uf1
1600 [Wanted] beta ~ uf1 beta
1601
1602 When canonicalizing the wanted (beta ~ uf1 beta), if we eagerly fail
1603 we will simply see a message:
1604 'Can't construct the infinite type beta ~ uf1 beta'
1605 and the user has no idea what the uf1 variable is.
1606
1607 Instead our plan is that we will NOT fail immediately, but:
1608 (1) Record the "frozen" error in the ic_insols field
1609 (2) Isolate the offending constraint from the rest of the inerts
1610 (3) Keep on simplifying/canonicalizing
1611
1612 At the end, we will hopefully have substituted uf1 := F alpha, and we
1613 will be able to report a more informative error:
1614 'Can't construct the infinite type beta ~ F alpha beta'
1615
1616 Insoluble constraints *do* include Derived constraints. For example,
1617 a functional dependency might give rise to [D] Int ~ Bool, and we must
1618 report that. If insolubles did not contain Deriveds, reportErrors would
1619 never see it.
1620
1621
1622 ************************************************************************
1623 * *
1624 Pretty printing
1625 * *
1626 ************************************************************************
1627 -}
1628
1629 pprEvVars :: [EvVar] -> SDoc -- Print with their types
1630 pprEvVars ev_vars = vcat (map pprEvVarWithType ev_vars)
1631
1632 pprEvVarTheta :: [EvVar] -> SDoc
1633 pprEvVarTheta ev_vars = pprTheta (map evVarPred ev_vars)
1634
1635 pprEvVarWithType :: EvVar -> SDoc
1636 pprEvVarWithType v = ppr v <+> dcolon <+> pprType (evVarPred v)
1637
1638
1639
1640 wrapType :: Type -> [TyVar] -> [PredType] -> Type
1641 wrapType ty skols givens = mkSpecForAllTys skols $ mkPhiTy givens ty
1642
1643
1644 {-
1645 ************************************************************************
1646 * *
1647 CtEvidence
1648 * *
1649 ************************************************************************
1650
1651 Note [Evidence field of CtEvidence]
1652 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1653 During constraint solving we never look at the type of ctev_evar/ctev_dest;
1654 instead we look at the ctev_pred field. The evtm/evar field
1655 may be un-zonked.
1656
1657 Note [Bind new Givens immediately]
1658 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1659 For Givens we make new EvVars and bind them immediately. Two main reasons:
1660 * Gain sharing. E.g. suppose we start with g :: C a b, where
1661 class D a => C a b
1662 class (E a, F a) => D a
1663 If we generate all g's superclasses as separate EvTerms we might
1664 get selD1 (selC1 g) :: E a
1665 selD2 (selC1 g) :: F a
1666 selC1 g :: D a
1667 which we could do more economically as:
1668 g1 :: D a = selC1 g
1669 g2 :: E a = selD1 g1
1670 g3 :: F a = selD2 g1
1671
1672 * For *coercion* evidence we *must* bind each given:
1673 class (a~b) => C a b where ....
1674 f :: C a b => ....
1675 Then in f's Givens we have g:(C a b) and the superclass sc(g,0):a~b.
1676 But that superclass selector can't (yet) appear in a coercion
1677 (see evTermCoercion), so the easy thing is to bind it to an Id.
1678
1679 So a Given has EvVar inside it rather than (as previously) an EvTerm.
1680
1681 -}
1682
1683 -- | A place for type-checking evidence to go after it is generated.
1684 -- Wanted equalities are always HoleDest; other wanteds are always
1685 -- EvVarDest.
1686 data TcEvDest
1687 = EvVarDest EvVar -- ^ bind this var to the evidence
1688 -- EvVarDest is always used for non-type-equalities
1689 -- e.g. class constraints
1690
1691 | HoleDest CoercionHole -- ^ fill in this hole with the evidence
1692 -- HoleDest is always used for type-equalities
1693 -- See Note [Coercion holes] in GHC.Core.TyCo.Rep
1694
1695 data CtEvidence
1696 = CtGiven -- Truly given, not depending on subgoals
1697 { ctev_pred :: TcPredType -- See Note [Ct/evidence invariant]
1698 , ctev_evar :: EvVar -- See Note [Evidence field of CtEvidence]
1699 , ctev_loc :: CtLoc }
1700
1701
1702 | CtWanted -- Wanted goal
1703 { ctev_pred :: TcPredType -- See Note [Ct/evidence invariant]
1704 , ctev_dest :: TcEvDest
1705 , ctev_nosh :: ShadowInfo -- See Note [Constraint flavours]
1706 , ctev_loc :: CtLoc }
1707
1708 | CtDerived -- A goal that we don't really have to solve and can't
1709 -- immediately rewrite anything other than a derived
1710 -- (there's no evidence!) but if we do manage to solve
1711 -- it may help in solving other goals.
1712 { ctev_pred :: TcPredType
1713 , ctev_loc :: CtLoc }
1714
1715 ctEvPred :: CtEvidence -> TcPredType
1716 -- The predicate of a flavor
1717 ctEvPred = ctev_pred
1718
1719 ctEvLoc :: CtEvidence -> CtLoc
1720 ctEvLoc = ctev_loc
1721
1722 ctEvOrigin :: CtEvidence -> CtOrigin
1723 ctEvOrigin = ctLocOrigin . ctEvLoc
1724
1725 -- | Get the equality relation relevant for a 'CtEvidence'
1726 ctEvEqRel :: CtEvidence -> EqRel
1727 ctEvEqRel = predTypeEqRel . ctEvPred
1728
1729 -- | Get the role relevant for a 'CtEvidence'
1730 ctEvRole :: CtEvidence -> Role
1731 ctEvRole = eqRelRole . ctEvEqRel
1732
1733 ctEvTerm :: CtEvidence -> EvTerm
1734 ctEvTerm ev = EvExpr (ctEvExpr ev)
1735
1736 ctEvExpr :: CtEvidence -> EvExpr
1737 ctEvExpr ev@(CtWanted { ctev_dest = HoleDest _ })
1738 = Coercion $ ctEvCoercion ev
1739 ctEvExpr ev = evId (ctEvEvId ev)
1740
1741 ctEvCoercion :: HasDebugCallStack => CtEvidence -> TcCoercion
1742 ctEvCoercion (CtGiven { ctev_evar = ev_id })
1743 = mkTcCoVarCo ev_id
1744 ctEvCoercion (CtWanted { ctev_dest = dest })
1745 | HoleDest hole <- dest
1746 = -- ctEvCoercion is only called on type equalities
1747 -- and they always have HoleDests
1748 mkHoleCo hole
1749 ctEvCoercion ev
1750 = pprPanic "ctEvCoercion" (ppr ev)
1751
1752 ctEvEvId :: CtEvidence -> EvVar
1753 ctEvEvId (CtWanted { ctev_dest = EvVarDest ev }) = ev
1754 ctEvEvId (CtWanted { ctev_dest = HoleDest h }) = coHoleCoVar h
1755 ctEvEvId (CtGiven { ctev_evar = ev }) = ev
1756 ctEvEvId ctev@(CtDerived {}) = pprPanic "ctEvId:" (ppr ctev)
1757
1758 instance Outputable TcEvDest where
1759 ppr (HoleDest h) = text "hole" <> ppr h
1760 ppr (EvVarDest ev) = ppr ev
1761
1762 instance Outputable CtEvidence where
1763 ppr ev = ppr (ctEvFlavour ev)
1764 <+> pp_ev <+> braces (ppr (ctl_depth (ctEvLoc ev)))
1765 -- Show the sub-goal depth too
1766 <> dcolon <+> ppr (ctEvPred ev)
1767 where
1768 pp_ev = case ev of
1769 CtGiven { ctev_evar = v } -> ppr v
1770 CtWanted {ctev_dest = d } -> ppr d
1771 CtDerived {} -> text "_"
1772
1773 isWanted :: CtEvidence -> Bool
1774 isWanted (CtWanted {}) = True
1775 isWanted _ = False
1776
1777 isGiven :: CtEvidence -> Bool
1778 isGiven (CtGiven {}) = True
1779 isGiven _ = False
1780
1781 isDerived :: CtEvidence -> Bool
1782 isDerived (CtDerived {}) = True
1783 isDerived _ = False
1784
1785 {-
1786 %************************************************************************
1787 %* *
1788 CtFlavour
1789 %* *
1790 %************************************************************************
1791
1792 Note [Constraint flavours]
1793 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1794 Constraints come in four flavours:
1795
1796 * [G] Given: we have evidence
1797
1798 * [W] Wanted WOnly: we want evidence
1799
1800 * [D] Derived: any solution must satisfy this constraint, but
1801 we don't need evidence for it. Examples include:
1802 - superclasses of [W] class constraints
1803 - equalities arising from functional dependencies
1804 or injectivity
1805
1806 * [WD] Wanted WDeriv: a single constraint that represents
1807 both [W] and [D]
1808 We keep them paired as one both for efficiency
1809
1810 The ctev_nosh field of a Wanted distinguishes between [W] and [WD]
1811
1812 Wanted constraints are born as [WD], but are split into [W] and its
1813 "shadow" [D] in GHC.Tc.Solver.Monad.maybeEmitShadow.
1814
1815 See Note [The improvement story and derived shadows] in GHC.Tc.Solver.Monad
1816 -}
1817
1818 data CtFlavour -- See Note [Constraint flavours]
1819 = Given
1820 | Wanted ShadowInfo
1821 | Derived
1822 deriving Eq
1823
1824 data ShadowInfo
1825 = WDeriv -- [WD] This Wanted constraint has no Derived shadow,
1826 -- so it behaves like a pair of a Wanted and a Derived
1827 | WOnly -- [W] It has a separate derived shadow
1828 -- See Note [The improvement story and derived shadows] in GHC.Tc.Solver.Monad
1829 deriving( Eq )
1830
1831 instance Outputable CtFlavour where
1832 ppr Given = text "[G]"
1833 ppr (Wanted WDeriv) = text "[WD]"
1834 ppr (Wanted WOnly) = text "[W]"
1835 ppr Derived = text "[D]"
1836
1837 -- | Does this 'CtFlavour' subsumed 'Derived'? True of @[WD]@ and @[D]@.
1838 ctFlavourContainsDerived :: CtFlavour -> Bool
1839 ctFlavourContainsDerived (Wanted WDeriv) = True
1840 ctFlavourContainsDerived Derived = True
1841 ctFlavourContainsDerived _ = False
1842
1843 ctEvFlavour :: CtEvidence -> CtFlavour
1844 ctEvFlavour (CtWanted { ctev_nosh = nosh }) = Wanted nosh
1845 ctEvFlavour (CtGiven {}) = Given
1846 ctEvFlavour (CtDerived {}) = Derived
1847
1848 -- | Whether or not one 'Ct' can rewrite another is determined by its
1849 -- flavour and its equality relation. See also
1850 -- Note [Flavours with roles] in GHC.Tc.Solver.InertSet
1851 type CtFlavourRole = (CtFlavour, EqRel)
1852
1853 -- | Extract the flavour, role, and boxity from a 'CtEvidence'
1854 ctEvFlavourRole :: CtEvidence -> CtFlavourRole
1855 ctEvFlavourRole ev = (ctEvFlavour ev, ctEvEqRel ev)
1856
1857 -- | Extract the flavour and role from a 'Ct'
1858 ctFlavourRole :: Ct -> CtFlavourRole
1859 -- Uses short-cuts to role for special cases
1860 ctFlavourRole (CDictCan { cc_ev = ev })
1861 = (ctEvFlavour ev, NomEq)
1862 ctFlavourRole (CEqCan { cc_ev = ev, cc_eq_rel = eq_rel })
1863 = (ctEvFlavour ev, eq_rel)
1864 ctFlavourRole ct
1865 = ctEvFlavourRole (ctEvidence ct)
1866
1867 {- Note [eqCanRewrite]
1868 ~~~~~~~~~~~~~~~~~~~~~~
1869 (eqCanRewrite ct1 ct2) holds if the constraint ct1 (a CEqCan of form
1870 lhs ~ ty) can be used to rewrite ct2. It must satisfy the properties of
1871 a can-rewrite relation, see Definition [Can-rewrite relation] in
1872 GHC.Tc.Solver.Monad.
1873
1874 With the solver handling Coercible constraints like equality constraints,
1875 the rewrite conditions must take role into account, never allowing
1876 a representational equality to rewrite a nominal one.
1877
1878 Note [Wanteds do not rewrite Wanteds]
1879 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1880 We don't allow Wanteds to rewrite Wanteds, because that can give rise
1881 to very confusing type error messages. A good example is #8450.
1882 Here's another
1883 f :: a -> Bool
1884 f x = ( [x,'c'], [x,True] ) `seq` True
1885 Here we get
1886 [W] a ~ Char
1887 [W] a ~ Bool
1888 but we do not want to complain about Bool ~ Char!
1889
1890 Note [Deriveds do rewrite Deriveds]
1891 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1892 However we DO allow Deriveds to rewrite Deriveds, because that's how
1893 improvement works; see Note [The improvement story] in GHC.Tc.Solver.Interact.
1894
1895 However, for now at least I'm only letting (Derived,NomEq) rewrite
1896 (Derived,NomEq) and not doing anything for ReprEq. If we have
1897 eqCanRewriteFR (Derived, NomEq) (Derived, _) = True
1898 then we lose property R2 of Definition [Can-rewrite relation]
1899 in GHC.Tc.Solver.Monad
1900 R2. If f1 >= f, and f2 >= f,
1901 then either f1 >= f2 or f2 >= f1
1902 Consider f1 = (Given, ReprEq)
1903 f2 = (Derived, NomEq)
1904 f = (Derived, ReprEq)
1905
1906 I thought maybe we could never get Derived ReprEq constraints, but
1907 we can; straight from the Wanteds during improvement. And from a Derived
1908 ReprEq we could conceivably get a Derived NomEq improvement (by decomposing
1909 a type constructor with Nomninal role), and hence unify.
1910
1911 This restriction that (Derived, NomEq) cannot rewrite (Derived, ReprEq) bites,
1912 in an obscure scenario:
1913
1914 data T a
1915 type role T nominal
1916
1917 type family F a
1918
1919 g :: forall b a. (F a ~ T a, Coercible (F a) (T b)) => ()
1920 g = ()
1921
1922 f :: forall a. (F a ~ T a) => ()
1923 f = g @a
1924
1925 The problem is in the body of f. We have
1926
1927 [G] F a ~N T a
1928 [WD] F alpha ~N T alpha
1929 [WD] F alpha ~R T a
1930
1931 The Wanteds aren't of use, so let's just look at Deriveds:
1932
1933 [G] F a ~N T a
1934 [D] F alpha ~N T alpha
1935 [D] F alpha ~R T a
1936
1937 As written, this makes no progress, and GHC errors. But, if we
1938 allowed D/N to rewrite D/R, the first D could rewrite the second:
1939
1940 [G] F a ~N T a
1941 [D] F alpha ~N T alpha
1942 [D] T alpha ~R T a
1943
1944 Now we decompose the second D to get
1945
1946 [D] alpha ~N a
1947
1948 noting the role annotation on T. This causes (alpha := a), and then
1949 everything else unlocks.
1950
1951 What to do? We could "decompose" nominal equalities into nominal-only
1952 ("NO") equalities and representational ones, where a NO equality rewrites
1953 only nominals. That is, when considering whether [D] F alpha ~N T alpha
1954 should rewrite [D] F alpha ~R T a, we could require splitting the first D
1955 into [D] F alpha ~NO T alpha, [D] F alpha ~R T alpha. Then, we use the R
1956 half of the split to rewrite the second D, and off we go. This splitting
1957 would allow the split-off R equality to be rewritten by other equalities,
1958 thus avoiding the problem in Note [Why R2?] in GHC.Tc.Solver.InertSet.
1959
1960 This infelicity is #19665 and tested in typecheck/should_compile/T19665
1961 (marked as expect_broken).
1962
1963 -}
1964
1965 eqCanRewrite :: EqRel -> EqRel -> Bool
1966 eqCanRewrite NomEq _ = True
1967 eqCanRewrite ReprEq ReprEq = True
1968 eqCanRewrite ReprEq NomEq = False
1969
1970 eqCanRewriteFR :: CtFlavourRole -> CtFlavourRole -> Bool
1971 -- Can fr1 actually rewrite fr2?
1972 -- Very important function!
1973 -- See Note [eqCanRewrite]
1974 -- See Note [Wanteds do not rewrite Wanteds]
1975 -- See Note [Deriveds do rewrite Deriveds]
1976 eqCanRewriteFR (Given, r1) (_, r2) = eqCanRewrite r1 r2
1977 eqCanRewriteFR (Wanted WDeriv, NomEq) (Derived, NomEq) = True
1978 eqCanRewriteFR (Derived, NomEq) (Derived, NomEq) = True
1979 eqCanRewriteFR _ _ = False
1980
1981 eqMayRewriteFR :: CtFlavourRole -> CtFlavourRole -> Bool
1982 -- Is it /possible/ that fr1 can rewrite fr2?
1983 -- This is used when deciding which inerts to kick out,
1984 -- at which time a [WD] inert may be split into [W] and [D]
1985 eqMayRewriteFR (Wanted WDeriv, NomEq) (Wanted WDeriv, NomEq) = True
1986 eqMayRewriteFR (Derived, NomEq) (Wanted WDeriv, NomEq) = True
1987 eqMayRewriteFR fr1 fr2 = eqCanRewriteFR fr1 fr2
1988
1989 {- Note [eqCanDischarge]
1990 ~~~~~~~~~~~~~~~~~~~~~~~~
1991 Suppose we have two identical CEqCan equality constraints
1992 (i.e. both LHS and RHS are the same)
1993 (x1:lhs~t) `eqCanDischarge` (xs:lhs~t)
1994 Can we just drop x2 in favour of x1?
1995
1996 Answer: yes if eqCanDischarge is true.
1997
1998 Note that we do /not/ allow Wanted to discharge Derived.
1999 We must keep both. Why? Because the Derived may rewrite
2000 other Deriveds in the model whereas the Wanted cannot.
2001
2002 However a Wanted can certainly discharge an identical Wanted. So
2003 eqCanDischarge does /not/ define a can-rewrite relation in the
2004 sense of Definition [Can-rewrite relation] in GHC.Tc.Solver.Monad.
2005
2006 We /do/ say that a [W] can discharge a [WD]. In evidence terms it
2007 certainly can, and the /caller/ arranges that the otherwise-lost [D]
2008 is spat out as a new Derived. -}
2009
2010 eqCanDischargeFR :: CtFlavourRole -> CtFlavourRole -> Bool
2011 -- See Note [eqCanDischarge]
2012 eqCanDischargeFR (f1,r1) (f2, r2) = eqCanRewrite r1 r2
2013 && eqCanDischargeF f1 f2
2014
2015 eqCanDischargeF :: CtFlavour -> CtFlavour -> Bool
2016 eqCanDischargeF Given _ = True
2017 eqCanDischargeF (Wanted _) (Wanted _) = True
2018 eqCanDischargeF (Wanted WDeriv) Derived = True
2019 eqCanDischargeF Derived Derived = True
2020 eqCanDischargeF _ _ = False
2021
2022
2023 {-
2024 ************************************************************************
2025 * *
2026 SubGoalDepth
2027 * *
2028 ************************************************************************
2029
2030 Note [SubGoalDepth]
2031 ~~~~~~~~~~~~~~~~~~~
2032 The 'SubGoalDepth' takes care of stopping the constraint solver from looping.
2033
2034 The counter starts at zero and increases. It includes dictionary constraints,
2035 equality simplification, and type family reduction. (Why combine these? Because
2036 it's actually quite easy to mistake one for another, in sufficiently involved
2037 scenarios, like ConstraintKinds.)
2038
2039 The flag -freduction-depth=n fixes the maximium level.
2040
2041 * The counter includes the depth of type class instance declarations. Example:
2042 [W] d{7} : Eq [Int]
2043 That is d's dictionary-constraint depth is 7. If we use the instance
2044 $dfEqList :: Eq a => Eq [a]
2045 to simplify it, we get
2046 d{7} = $dfEqList d'{8}
2047 where d'{8} : Eq Int, and d' has depth 8.
2048
2049 For civilised (decidable) instance declarations, each increase of
2050 depth removes a type constructor from the type, so the depth never
2051 gets big; i.e. is bounded by the structural depth of the type.
2052
2053 * The counter also increments when resolving
2054 equalities involving type functions. Example:
2055 Assume we have a wanted at depth 7:
2056 [W] d{7} : F () ~ a
2057 If there is a type function equation "F () = Int", this would be rewritten to
2058 [W] d{8} : Int ~ a
2059 and remembered as having depth 8.
2060
2061 Again, without UndecidableInstances, this counter is bounded, but without it
2062 can resolve things ad infinitum. Hence there is a maximum level.
2063
2064 * Lastly, every time an equality is rewritten, the counter increases. Again,
2065 rewriting an equality constraint normally makes progress, but it's possible
2066 the "progress" is just the reduction of an infinitely-reducing type family.
2067 Hence we need to track the rewrites.
2068
2069 When compiling a program requires a greater depth, then GHC recommends turning
2070 off this check entirely by setting -freduction-depth=0. This is because the
2071 exact number that works is highly variable, and is likely to change even between
2072 minor releases. Because this check is solely to prevent infinite compilation
2073 times, it seems safe to disable it when a user has ascertained that their program
2074 doesn't loop at the type level.
2075
2076 -}
2077
2078 -- | See Note [SubGoalDepth]
2079 newtype SubGoalDepth = SubGoalDepth Int
2080 deriving (Eq, Ord, Outputable)
2081
2082 initialSubGoalDepth :: SubGoalDepth
2083 initialSubGoalDepth = SubGoalDepth 0
2084
2085 bumpSubGoalDepth :: SubGoalDepth -> SubGoalDepth
2086 bumpSubGoalDepth (SubGoalDepth n) = SubGoalDepth (n + 1)
2087
2088 maxSubGoalDepth :: SubGoalDepth -> SubGoalDepth -> SubGoalDepth
2089 maxSubGoalDepth (SubGoalDepth n) (SubGoalDepth m) = SubGoalDepth (n `max` m)
2090
2091 subGoalDepthExceeded :: DynFlags -> SubGoalDepth -> Bool
2092 subGoalDepthExceeded dflags (SubGoalDepth d)
2093 = mkIntWithInf d > reductionDepth dflags
2094
2095 {-
2096 ************************************************************************
2097 * *
2098 CtLoc
2099 * *
2100 ************************************************************************
2101
2102 The 'CtLoc' gives information about where a constraint came from.
2103 This is important for decent error message reporting because
2104 dictionaries don't appear in the original source code.
2105 type will evolve...
2106
2107 -}
2108
2109 data CtLoc = CtLoc { ctl_origin :: CtOrigin
2110 , ctl_env :: TcLclEnv
2111 , ctl_t_or_k :: Maybe TypeOrKind -- OK if we're not sure
2112 , ctl_depth :: !SubGoalDepth }
2113
2114 -- The TcLclEnv includes particularly
2115 -- source location: tcl_loc :: RealSrcSpan
2116 -- context: tcl_ctxt :: [ErrCtxt]
2117 -- binder stack: tcl_bndrs :: TcBinderStack
2118 -- level: tcl_tclvl :: TcLevel
2119
2120 mkKindLoc :: TcType -> TcType -- original *types* being compared
2121 -> CtLoc -> CtLoc
2122 mkKindLoc s1 s2 loc = setCtLocOrigin (toKindLoc loc)
2123 (KindEqOrigin s1 s2 (ctLocOrigin loc)
2124 (ctLocTypeOrKind_maybe loc))
2125
2126 -- | Take a CtLoc and moves it to the kind level
2127 toKindLoc :: CtLoc -> CtLoc
2128 toKindLoc loc = loc { ctl_t_or_k = Just KindLevel }
2129
2130 mkGivenLoc :: TcLevel -> SkolemInfo -> TcLclEnv -> CtLoc
2131 mkGivenLoc tclvl skol_info env
2132 = CtLoc { ctl_origin = GivenOrigin skol_info
2133 , ctl_env = setLclEnvTcLevel env tclvl
2134 , ctl_t_or_k = Nothing -- this only matters for error msgs
2135 , ctl_depth = initialSubGoalDepth }
2136
2137 ctLocEnv :: CtLoc -> TcLclEnv
2138 ctLocEnv = ctl_env
2139
2140 ctLocLevel :: CtLoc -> TcLevel
2141 ctLocLevel loc = getLclEnvTcLevel (ctLocEnv loc)
2142
2143 ctLocDepth :: CtLoc -> SubGoalDepth
2144 ctLocDepth = ctl_depth
2145
2146 ctLocOrigin :: CtLoc -> CtOrigin
2147 ctLocOrigin = ctl_origin
2148
2149 ctLocSpan :: CtLoc -> RealSrcSpan
2150 ctLocSpan (CtLoc { ctl_env = lcl}) = getLclEnvLoc lcl
2151
2152 ctLocTypeOrKind_maybe :: CtLoc -> Maybe TypeOrKind
2153 ctLocTypeOrKind_maybe = ctl_t_or_k
2154
2155 setCtLocSpan :: CtLoc -> RealSrcSpan -> CtLoc
2156 setCtLocSpan ctl@(CtLoc { ctl_env = lcl }) loc = setCtLocEnv ctl (setLclEnvLoc lcl loc)
2157
2158 bumpCtLocDepth :: CtLoc -> CtLoc
2159 bumpCtLocDepth loc@(CtLoc { ctl_depth = d }) = loc { ctl_depth = bumpSubGoalDepth d }
2160
2161 setCtLocOrigin :: CtLoc -> CtOrigin -> CtLoc
2162 setCtLocOrigin ctl orig = ctl { ctl_origin = orig }
2163
2164 updateCtLocOrigin :: CtLoc -> (CtOrigin -> CtOrigin) -> CtLoc
2165 updateCtLocOrigin ctl@(CtLoc { ctl_origin = orig }) upd
2166 = ctl { ctl_origin = upd orig }
2167
2168 setCtLocEnv :: CtLoc -> TcLclEnv -> CtLoc
2169 setCtLocEnv ctl env = ctl { ctl_env = env }
2170
2171 pprCtLoc :: CtLoc -> SDoc
2172 -- "arising from ... at ..."
2173 -- Not an instance of Outputable because of the "arising from" prefix
2174 pprCtLoc (CtLoc { ctl_origin = o, ctl_env = lcl})
2175 = sep [ pprCtOrigin o
2176 , text "at" <+> ppr (getLclEnvLoc lcl)]