fb09fdd9234f96b59cabfcbb9fc6b9aaa079f063
[ghc.git] / compiler / typecheck / TcRnTypes.hs
1 {-
2 (c) The University of Glasgow 2006-2012
3 (c) The GRASP Project, Glasgow University, 1992-2002
4
5
6 Various types used during typechecking, please see TcRnMonad as well for
7 operations on these types. You probably want to import it, instead of this
8 module.
9
10 All the monads exported here are built on top of the same IOEnv monad. The
11 monad functions like a Reader monad in the way it passes the environment
12 around. This is done to allow the environment to be manipulated in a stack
13 like fashion when entering expressions... etc.
14
15 For state that is global and should be returned at the end (e.g not part
16 of the stack mechanism), you should use a TcRef (= IORef) to store them.
17 -}
18
19 {-# LANGUAGE CPP, ExistentialQuantification, GeneralizedNewtypeDeriving,
20 ViewPatterns #-}
21
22 module TcRnTypes(
23 TcRnIf, TcRn, TcM, RnM, IfM, IfL, IfG, -- The monad is opaque outside this module
24 TcRef,
25
26 -- The environment types
27 Env(..),
28 TcGblEnv(..), TcLclEnv(..),
29 IfGblEnv(..), IfLclEnv(..),
30 tcVisibleOrphanMods,
31
32 -- Frontend types (shouldn't really be here)
33 FrontendResult(..),
34
35 -- Renamer types
36 ErrCtxt, RecFieldEnv,
37 ImportAvails(..), emptyImportAvails, plusImportAvails,
38 WhereFrom(..), mkModDeps, modDepsElts,
39
40 -- Typechecker types
41 TcTypeEnv, TcBinderStack, TcBinder(..),
42 TcTyThing(..), PromotionErr(..),
43 IdBindingInfo(..), ClosedTypeId, RhsNames,
44 IsGroupClosed(..),
45 SelfBootInfo(..),
46 pprTcTyThingCategory, pprPECategory, CompleteMatch(..),
47
48 -- Desugaring types
49 DsM, DsLclEnv(..), DsGblEnv(..),
50 DsMetaEnv, DsMetaVal(..), CompleteMatchMap,
51 mkCompleteMatchMap, extendCompleteMatchMap,
52
53 -- Template Haskell
54 ThStage(..), SpliceType(..), PendingStuff(..),
55 topStage, topAnnStage, topSpliceStage,
56 ThLevel, impLevel, outerLevel, thLevel,
57 ForeignSrcLang(..),
58
59 -- Arrows
60 ArrowCtxt(..),
61
62 -- TcSigInfo
63 TcSigFun, TcSigInfo(..), TcIdSigInfo(..),
64 TcIdSigInst(..), TcPatSynInfo(..),
65 isPartialSig, hasCompleteSig,
66
67 -- Canonical constraints
68 Xi, Ct(..), Cts, emptyCts, andCts, andManyCts, pprCts,
69 singleCt, listToCts, ctsElts, consCts, snocCts, extendCtsList,
70 isEmptyCts, isCTyEqCan, isCFunEqCan,
71 isPendingScDict, superClassesMightHelp,
72 isCDictCan_Maybe, isCFunEqCan_maybe,
73 isCNonCanonical, isWantedCt, isDerivedCt,
74 isGivenCt, isHoleCt, isOutOfScopeCt, isExprHoleCt, isTypeHoleCt,
75 isUserTypeErrorCt, getUserTypeErrorMsg,
76 ctEvidence, ctLoc, setCtLoc, ctPred, ctFlavour, ctEqRel, ctOrigin,
77 ctEvId, mkTcEqPredLikeEv,
78 mkNonCanonical, mkNonCanonicalCt, mkGivens,
79 mkIrredCt, mkInsolubleCt,
80 ctEvPred, ctEvLoc, ctEvOrigin, ctEvEqRel,
81 ctEvExpr, ctEvCoercion, ctEvEvId,
82 tyCoVarsOfCt, tyCoVarsOfCts,
83 tyCoVarsOfCtList, tyCoVarsOfCtsList,
84
85 WantedConstraints(..), insolubleWC, emptyWC, isEmptyWC,
86 isSolvedWC, andWC, unionsWC, mkSimpleWC, mkImplicWC,
87 addInsols, insolublesOnly, addSimples, addImplics,
88 tyCoVarsOfWC, dropDerivedWC, dropDerivedSimples,
89 tyCoVarsOfWCList, insolubleWantedCt, insolubleEqCt,
90 isDroppableCt, insolubleImplic,
91 arisesFromGivens,
92
93 Implication(..), newImplication,
94 ImplicStatus(..), isInsolubleStatus, isSolvedStatus,
95 SubGoalDepth, initialSubGoalDepth, maxSubGoalDepth,
96 bumpSubGoalDepth, subGoalDepthExceeded,
97 CtLoc(..), ctLocSpan, ctLocEnv, ctLocLevel, ctLocOrigin,
98 ctLocTypeOrKind_maybe,
99 ctLocDepth, bumpCtLocDepth, isGivenLoc,
100 setCtLocOrigin, updateCtLocOrigin, setCtLocEnv, setCtLocSpan,
101 CtOrigin(..), exprCtOrigin, lexprCtOrigin, matchesCtOrigin, grhssCtOrigin,
102 isVisibleOrigin, toInvisibleOrigin,
103 TypeOrKind(..), isTypeLevel, isKindLevel,
104 pprCtOrigin, pprCtLoc,
105 pushErrCtxt, pushErrCtxtSameOrigin,
106
107
108 SkolemInfo(..), pprSigSkolInfo, pprSkolInfo,
109
110 CtEvidence(..), TcEvDest(..),
111 mkKindLoc, toKindLoc, mkGivenLoc,
112 isWanted, isGiven, isDerived, isGivenOrWDeriv,
113 ctEvRole,
114
115 wrapType, wrapTypeWithImplication,
116 removeBindingShadowing,
117
118 -- Constraint solver plugins
119 TcPlugin(..), TcPluginResult(..), TcPluginSolver,
120 TcPluginM, runTcPluginM, unsafeTcPluginTcM,
121 getEvBindsTcPluginM,
122
123 CtFlavour(..), ShadowInfo(..), ctEvFlavour,
124 CtFlavourRole, ctEvFlavourRole, ctFlavourRole,
125 eqCanRewrite, eqCanRewriteFR, eqMayRewriteFR,
126 eqCanDischargeFR,
127 funEqCanDischarge, funEqCanDischargeF,
128
129 -- Pretty printing
130 pprEvVarTheta,
131 pprEvVars, pprEvVarWithType,
132
133 -- Misc other types
134 TcId, TcIdSet,
135 Hole(..), holeOcc,
136 NameShape(..),
137
138 -- Role annotations
139 RoleAnnotEnv, emptyRoleAnnotEnv, mkRoleAnnotEnv,
140 lookupRoleAnnot, getRoleAnnots,
141
142 ) where
143
144 #include "HsVersions.h"
145
146 import GhcPrelude
147
148 import HsSyn
149 import CoreSyn
150 import HscTypes
151 import TcEvidence
152 import Type
153 import Class ( Class )
154 import TyCon ( TyCon, TyConFlavour, tyConKind )
155 import TyCoRep ( CoercionHole(..), coHoleCoVar )
156 import Coercion ( Coercion, mkHoleCo )
157 import ConLike ( ConLike(..) )
158 import DataCon ( DataCon, dataConUserType, dataConOrigArgTys )
159 import PatSyn ( PatSyn, pprPatSynType )
160 import Id ( idType, idName )
161 import FieldLabel ( FieldLabel )
162 import TcType
163 import Annotations
164 import InstEnv
165 import FamInstEnv
166 import PmExpr
167 import IOEnv
168 import RdrName
169 import Name
170 import NameEnv
171 import NameSet
172 import Avail
173 import Var
174 import FV
175 import VarEnv
176 import Module
177 import SrcLoc
178 import VarSet
179 import ErrUtils
180 import UniqFM
181 import UniqSupply
182 import BasicTypes
183 import Bag
184 import DynFlags
185 import Outputable
186 import ListSetOps
187 import FastString
188 import qualified GHC.LanguageExtensions as LangExt
189 import Fingerprint
190 import Util
191 import PrelNames ( isUnboundName )
192 import CostCentreState
193
194 import Control.Monad (ap, liftM, msum)
195 import qualified Control.Monad.Fail as MonadFail
196 import Data.Set ( Set )
197 import qualified Data.Set as S
198
199 import Data.List ( sort )
200 import Data.Map ( Map )
201 import Data.Dynamic ( Dynamic )
202 import Data.Typeable ( TypeRep )
203 import Data.Maybe ( mapMaybe )
204 import GHCi.Message
205 import GHCi.RemoteTypes
206
207 import qualified Language.Haskell.TH as TH
208
209 -- | A 'NameShape' is a substitution on 'Name's that can be used
210 -- to refine the identities of a hole while we are renaming interfaces
211 -- (see 'RnModIface'). Specifically, a 'NameShape' for
212 -- 'ns_module_name' @A@, defines a mapping from @{A.T}@
213 -- (for some 'OccName' @T@) to some arbitrary other 'Name'.
214 --
215 -- The most intruiging thing about a 'NameShape', however, is
216 -- how it's constructed. A 'NameShape' is *implied* by the
217 -- exported 'AvailInfo's of the implementor of an interface:
218 -- if an implementor of signature @<H>@ exports @M.T@, you implicitly
219 -- define a substitution from @{H.T}@ to @M.T@. So a 'NameShape'
220 -- is computed from the list of 'AvailInfo's that are exported
221 -- by the implementation of a module, or successively merged
222 -- together by the export lists of signatures which are joining
223 -- together.
224 --
225 -- It's not the most obvious way to go about doing this, but it
226 -- does seem to work!
227 --
228 -- NB: Can't boot this and put it in NameShape because then we
229 -- start pulling in too many DynFlags things.
230 data NameShape = NameShape {
231 ns_mod_name :: ModuleName,
232 ns_exports :: [AvailInfo],
233 ns_map :: OccEnv Name
234 }
235
236
237 {-
238 ************************************************************************
239 * *
240 Standard monad definition for TcRn
241 All the combinators for the monad can be found in TcRnMonad
242 * *
243 ************************************************************************
244
245 The monad itself has to be defined here, because it is mentioned by ErrCtxt
246 -}
247
248 type TcRnIf a b = IOEnv (Env a b)
249 type TcRn = TcRnIf TcGblEnv TcLclEnv -- Type inference
250 type IfM lcl = TcRnIf IfGblEnv lcl -- Iface stuff
251 type IfG = IfM () -- Top level
252 type IfL = IfM IfLclEnv -- Nested
253 type DsM = TcRnIf DsGblEnv DsLclEnv -- Desugaring
254
255 -- TcRn is the type-checking and renaming monad: the main monad that
256 -- most type-checking takes place in. The global environment is
257 -- 'TcGblEnv', which tracks all of the top-level type-checking
258 -- information we've accumulated while checking a module, while the
259 -- local environment is 'TcLclEnv', which tracks local information as
260 -- we move inside expressions.
261
262 -- | Historical "renaming monad" (now it's just 'TcRn').
263 type RnM = TcRn
264
265 -- | Historical "type-checking monad" (now it's just 'TcRn').
266 type TcM = TcRn
267
268 -- We 'stack' these envs through the Reader like monad infrastructure
269 -- as we move into an expression (although the change is focused in
270 -- the lcl type).
271 data Env gbl lcl
272 = Env {
273 env_top :: !HscEnv, -- Top-level stuff that never changes
274 -- Includes all info about imported things
275 -- BangPattern is to fix leak, see #15111
276
277 env_us :: {-# UNPACK #-} !(IORef UniqSupply),
278 -- Unique supply for local variables
279
280 env_gbl :: gbl, -- Info about things defined at the top level
281 -- of the module being compiled
282
283 env_lcl :: lcl -- Nested stuff; changes as we go into
284 }
285
286 instance ContainsDynFlags (Env gbl lcl) where
287 extractDynFlags env = hsc_dflags (env_top env)
288
289 instance ContainsModule gbl => ContainsModule (Env gbl lcl) where
290 extractModule env = extractModule (env_gbl env)
291
292
293 {-
294 ************************************************************************
295 * *
296 The interface environments
297 Used when dealing with IfaceDecls
298 * *
299 ************************************************************************
300 -}
301
302 data IfGblEnv
303 = IfGblEnv {
304 -- Some information about where this environment came from;
305 -- useful for debugging.
306 if_doc :: SDoc,
307 -- The type environment for the module being compiled,
308 -- in case the interface refers back to it via a reference that
309 -- was originally a hi-boot file.
310 -- We need the module name so we can test when it's appropriate
311 -- to look in this env.
312 -- See Note [Tying the knot] in TcIface
313 if_rec_types :: Maybe (Module, IfG TypeEnv)
314 -- Allows a read effect, so it can be in a mutable
315 -- variable; c.f. handling the external package type env
316 -- Nothing => interactive stuff, no loops possible
317 }
318
319 data IfLclEnv
320 = IfLclEnv {
321 -- The module for the current IfaceDecl
322 -- So if we see f = \x -> x
323 -- it means M.f = \x -> x, where M is the if_mod
324 -- NB: This is a semantic module, see
325 -- Note [Identity versus semantic module]
326 if_mod :: Module,
327
328 -- Whether or not the IfaceDecl came from a boot
329 -- file or not; we'll use this to choose between
330 -- NoUnfolding and BootUnfolding
331 if_boot :: Bool,
332
333 -- The field is used only for error reporting
334 -- if (say) there's a Lint error in it
335 if_loc :: SDoc,
336 -- Where the interface came from:
337 -- .hi file, or GHCi state, or ext core
338 -- plus which bit is currently being examined
339
340 if_nsubst :: Maybe NameShape,
341
342 -- This field is used to make sure "implicit" declarations
343 -- (anything that cannot be exported in mi_exports) get
344 -- wired up correctly in typecheckIfacesForMerging. Most
345 -- of the time it's @Nothing@. See Note [Resolving never-exported Names in TcIface]
346 -- in TcIface.
347 if_implicits_env :: Maybe TypeEnv,
348
349 if_tv_env :: FastStringEnv TyVar, -- Nested tyvar bindings
350 if_id_env :: FastStringEnv Id -- Nested id binding
351 }
352
353 {-
354 ************************************************************************
355 * *
356 Desugarer monad
357 * *
358 ************************************************************************
359
360 Now the mondo monad magic (yes, @DsM@ is a silly name)---carry around
361 a @UniqueSupply@ and some annotations, which
362 presumably include source-file location information:
363 -}
364
365 data DsGblEnv
366 = DsGblEnv
367 { ds_mod :: Module -- For SCC profiling
368 , ds_fam_inst_env :: FamInstEnv -- Like tcg_fam_inst_env
369 , ds_unqual :: PrintUnqualified
370 , ds_msgs :: IORef Messages -- Warning messages
371 , ds_if_env :: (IfGblEnv, IfLclEnv) -- Used for looking up global,
372 -- possibly-imported things
373 , ds_complete_matches :: CompleteMatchMap
374 -- Additional complete pattern matches
375 , ds_cc_st :: IORef CostCentreState
376 -- Tracking indices for cost centre annotations
377 }
378
379 instance ContainsModule DsGblEnv where
380 extractModule = ds_mod
381
382 data DsLclEnv = DsLclEnv {
383 dsl_meta :: DsMetaEnv, -- Template Haskell bindings
384 dsl_loc :: RealSrcSpan, -- To put in pattern-matching error msgs
385 dsl_dicts :: Bag EvVar, -- Constraints from GADT pattern-matching
386 dsl_tm_cs :: Bag SimpleEq,
387 dsl_pm_iter :: IORef Int -- no iterations for pmcheck
388 }
389
390 -- Inside [| |] brackets, the desugarer looks
391 -- up variables in the DsMetaEnv
392 type DsMetaEnv = NameEnv DsMetaVal
393
394 data DsMetaVal
395 = DsBound Id -- Bound by a pattern inside the [| |].
396 -- Will be dynamically alpha renamed.
397 -- The Id has type THSyntax.Var
398
399 | DsSplice (HsExpr GhcTc) -- These bindings are introduced by
400 -- the PendingSplices on a HsBracketOut
401
402
403 {-
404 ************************************************************************
405 * *
406 Global typechecker environment
407 * *
408 ************************************************************************
409 -}
410
411 -- | 'FrontendResult' describes the result of running the
412 -- frontend of a Haskell module. Usually, you'll get
413 -- a 'FrontendTypecheck', since running the frontend involves
414 -- typechecking a program, but for an hs-boot merge you'll
415 -- just get a ModIface, since no actual typechecking occurred.
416 --
417 -- This data type really should be in HscTypes, but it needs
418 -- to have a TcGblEnv which is only defined here.
419 data FrontendResult
420 = FrontendTypecheck TcGblEnv
421
422 -- Note [Identity versus semantic module]
423 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
424 -- When typechecking an hsig file, it is convenient to keep track
425 -- of two different "this module" identifiers:
426 --
427 -- - The IDENTITY module is simply thisPackage + the module
428 -- name; i.e. it uniquely *identifies* the interface file
429 -- we're compiling. For example, p[A=<A>]:A is an
430 -- identity module identifying the requirement named A
431 -- from library p.
432 --
433 -- - The SEMANTIC module, which is the actual module that
434 -- this signature is intended to represent (e.g. if
435 -- we have a identity module p[A=base:Data.IORef]:A,
436 -- then the semantic module is base:Data.IORef)
437 --
438 -- Which one should you use?
439 --
440 -- - In the desugarer and later phases of compilation,
441 -- identity and semantic modules coincide, since we never compile
442 -- signatures (we just generate blank object files for
443 -- hsig files.)
444 --
445 -- A corrolary of this is that the following invariant holds at any point
446 -- past desugaring,
447 --
448 -- if I have a Module, this_mod, in hand representing the module
449 -- currently being compiled,
450 -- then moduleUnitId this_mod == thisPackage dflags
451 --
452 -- - For any code involving Names, we want semantic modules.
453 -- See lookupIfaceTop in IfaceEnv, mkIface and addFingerprints
454 -- in MkIface, and tcLookupGlobal in TcEnv
455 --
456 -- - When reading interfaces, we want the identity module to
457 -- identify the specific interface we want (such interfaces
458 -- should never be loaded into the EPS). However, if a
459 -- hole module <A> is requested, we look for A.hi
460 -- in the home library we are compiling. (See LoadIface.)
461 -- Similarly, in RnNames we check for self-imports using
462 -- identity modules, to allow signatures to import their implementor.
463 --
464 -- - For recompilation avoidance, you want the identity module,
465 -- since that will actually say the specific interface you
466 -- want to track (and recompile if it changes)
467
468 -- | 'TcGblEnv' describes the top-level of the module at the
469 -- point at which the typechecker is finished work.
470 -- It is this structure that is handed on to the desugarer
471 -- For state that needs to be updated during the typechecking
472 -- phase and returned at end, use a 'TcRef' (= 'IORef').
473 data TcGblEnv
474 = TcGblEnv {
475 tcg_mod :: Module, -- ^ Module being compiled
476 tcg_semantic_mod :: Module, -- ^ If a signature, the backing module
477 -- See also Note [Identity versus semantic module]
478 tcg_src :: HscSource,
479 -- ^ What kind of module (regular Haskell, hs-boot, hsig)
480
481 tcg_rdr_env :: GlobalRdrEnv, -- ^ Top level envt; used during renaming
482 tcg_default :: Maybe [Type],
483 -- ^ Types used for defaulting. @Nothing@ => no @default@ decl
484
485 tcg_fix_env :: FixityEnv, -- ^ Just for things in this module
486 tcg_field_env :: RecFieldEnv, -- ^ Just for things in this module
487 -- See Note [The interactive package] in HscTypes
488
489 tcg_type_env :: TypeEnv,
490 -- ^ Global type env for the module we are compiling now. All
491 -- TyCons and Classes (for this module) end up in here right away,
492 -- along with their derived constructors, selectors.
493 --
494 -- (Ids defined in this module start in the local envt, though they
495 -- move to the global envt during zonking)
496 --
497 -- NB: for what "things in this module" means, see
498 -- Note [The interactive package] in HscTypes
499
500 tcg_type_env_var :: TcRef TypeEnv,
501 -- Used only to initialise the interface-file
502 -- typechecker in initIfaceTcRn, so that it can see stuff
503 -- bound in this module when dealing with hi-boot recursions
504 -- Updated at intervals (e.g. after dealing with types and classes)
505
506 tcg_inst_env :: !InstEnv,
507 -- ^ Instance envt for all /home-package/ modules;
508 -- Includes the dfuns in tcg_insts
509 -- NB. BangPattern is to fix a leak, see #15111
510 tcg_fam_inst_env :: !FamInstEnv, -- ^ Ditto for family instances
511 -- NB. BangPattern is to fix a leak, see #15111
512 tcg_ann_env :: AnnEnv, -- ^ And for annotations
513
514 -- Now a bunch of things about this module that are simply
515 -- accumulated, but never consulted until the end.
516 -- Nevertheless, it's convenient to accumulate them along
517 -- with the rest of the info from this module.
518 tcg_exports :: [AvailInfo], -- ^ What is exported
519 tcg_imports :: ImportAvails,
520 -- ^ Information about what was imported from where, including
521 -- things bound in this module. Also store Safe Haskell info
522 -- here about transitive trusted package requirements.
523 --
524 -- There are not many uses of this field, so you can grep for
525 -- all them.
526 --
527 -- The ImportAvails records information about the following
528 -- things:
529 --
530 -- 1. All of the modules you directly imported (tcRnImports)
531 -- 2. The orphans (only!) of all imported modules in a GHCi
532 -- session (runTcInteractive)
533 -- 3. The module that instantiated a signature
534 -- 4. Each of the signatures that merged in
535 --
536 -- It is used in the following ways:
537 -- - imp_orphs is used to determine what orphan modules should be
538 -- visible in the context (tcVisibleOrphanMods)
539 -- - imp_finsts is used to determine what family instances should
540 -- be visible (tcExtendLocalFamInstEnv)
541 -- - To resolve the meaning of the export list of a module
542 -- (tcRnExports)
543 -- - imp_mods is used to compute usage info (mkIfaceTc, deSugar)
544 -- - imp_trust_own_pkg is used for Safe Haskell in interfaces
545 -- (mkIfaceTc, as well as in HscMain)
546 -- - To create the Dependencies field in interface (mkDependencies)
547
548 tcg_dus :: DefUses, -- ^ What is defined in this module and what is used.
549 tcg_used_gres :: TcRef [GlobalRdrElt], -- ^ Records occurrences of imported entities
550 -- See Note [Tracking unused binding and imports]
551
552 tcg_keep :: TcRef NameSet,
553 -- ^ Locally-defined top-level names to keep alive.
554 --
555 -- "Keep alive" means give them an Exported flag, so that the
556 -- simplifier does not discard them as dead code, and so that they
557 -- are exposed in the interface file (but not to export to the
558 -- user).
559 --
560 -- Some things, like dict-fun Ids and default-method Ids are "born"
561 -- with the Exported flag on, for exactly the above reason, but some
562 -- we only discover as we go. Specifically:
563 --
564 -- * The to/from functions for generic data types
565 --
566 -- * Top-level variables appearing free in the RHS of an orphan
567 -- rule
568 --
569 -- * Top-level variables appearing free in a TH bracket
570
571 tcg_th_used :: TcRef Bool,
572 -- ^ @True@ <=> Template Haskell syntax used.
573 --
574 -- We need this so that we can generate a dependency on the
575 -- Template Haskell package, because the desugarer is going
576 -- to emit loads of references to TH symbols. The reference
577 -- is implicit rather than explicit, so we have to zap a
578 -- mutable variable.
579
580 tcg_th_splice_used :: TcRef Bool,
581 -- ^ @True@ <=> A Template Haskell splice was used.
582 --
583 -- Splices disable recompilation avoidance (see #481)
584
585 tcg_th_top_level_locs :: TcRef (Set RealSrcSpan),
586 -- ^ Locations of the top-level splices; used for providing details on
587 -- scope in error messages for out-of-scope variables
588
589 tcg_dfun_n :: TcRef OccSet,
590 -- ^ Allows us to choose unique DFun names.
591
592 tcg_merged :: [(Module, Fingerprint)],
593 -- ^ The requirements we merged with; we always have to recompile
594 -- if any of these changed.
595
596 -- The next fields accumulate the payload of the module
597 -- The binds, rules and foreign-decl fields are collected
598 -- initially in un-zonked form and are finally zonked in tcRnSrcDecls
599
600 tcg_rn_exports :: Maybe [(Located (IE GhcRn), Avails)],
601 -- Nothing <=> no explicit export list
602 -- Is always Nothing if we don't want to retain renamed
603 -- exports.
604 -- If present contains each renamed export list item
605 -- together with its exported names.
606
607 tcg_rn_imports :: [LImportDecl GhcRn],
608 -- Keep the renamed imports regardless. They are not
609 -- voluminous and are needed if you want to report unused imports
610
611 tcg_rn_decls :: Maybe (HsGroup GhcRn),
612 -- ^ Renamed decls, maybe. @Nothing@ <=> Don't retain renamed
613 -- decls.
614
615 tcg_dependent_files :: TcRef [FilePath], -- ^ dependencies from addDependentFile
616
617 tcg_th_topdecls :: TcRef [LHsDecl GhcPs],
618 -- ^ Top-level declarations from addTopDecls
619
620 tcg_th_foreign_files :: TcRef [(ForeignSrcLang, FilePath)],
621 -- ^ Foreign files emitted from TH.
622
623 tcg_th_topnames :: TcRef NameSet,
624 -- ^ Exact names bound in top-level declarations in tcg_th_topdecls
625
626 tcg_th_modfinalizers :: TcRef [TcM ()],
627 -- ^ Template Haskell module finalizers.
628 --
629 -- They are computations in the @TcM@ monad rather than @Q@ because we
630 -- set them to use particular local environments.
631
632 tcg_th_coreplugins :: TcRef [String],
633 -- ^ Core plugins added by Template Haskell code.
634
635 tcg_th_state :: TcRef (Map TypeRep Dynamic),
636 tcg_th_remote_state :: TcRef (Maybe (ForeignRef (IORef QState))),
637 -- ^ Template Haskell state
638
639 tcg_ev_binds :: Bag EvBind, -- Top-level evidence bindings
640
641 -- Things defined in this module, or (in GHCi)
642 -- in the declarations for a single GHCi command.
643 -- For the latter, see Note [The interactive package] in HscTypes
644 tcg_tr_module :: Maybe Id, -- Id for $trModule :: GHC.Types.Module
645 -- for which every module has a top-level defn
646 -- except in GHCi in which case we have Nothing
647 tcg_binds :: LHsBinds GhcTc, -- Value bindings in this module
648 tcg_sigs :: NameSet, -- ...Top-level names that *lack* a signature
649 tcg_imp_specs :: [LTcSpecPrag], -- ...SPECIALISE prags for imported Ids
650 tcg_warns :: Warnings, -- ...Warnings and deprecations
651 tcg_anns :: [Annotation], -- ...Annotations
652 tcg_tcs :: [TyCon], -- ...TyCons and Classes
653 tcg_insts :: [ClsInst], -- ...Instances
654 tcg_fam_insts :: [FamInst], -- ...Family instances
655 tcg_rules :: [LRuleDecl GhcTc], -- ...Rules
656 tcg_fords :: [LForeignDecl GhcTc], -- ...Foreign import & exports
657 tcg_patsyns :: [PatSyn], -- ...Pattern synonyms
658
659 tcg_doc_hdr :: Maybe LHsDocString, -- ^ Maybe Haddock header docs
660 tcg_hpc :: !AnyHpcUsage, -- ^ @True@ if any part of the
661 -- prog uses hpc instrumentation.
662 -- NB. BangPattern is to fix a leak, see #15111
663
664 tcg_self_boot :: SelfBootInfo, -- ^ Whether this module has a
665 -- corresponding hi-boot file
666
667 tcg_main :: Maybe Name, -- ^ The Name of the main
668 -- function, if this module is
669 -- the main module.
670
671 tcg_safeInfer :: TcRef (Bool, WarningMessages),
672 -- ^ Has the typechecker inferred this module as -XSafe (Safe Haskell)
673 -- See Note [Safe Haskell Overlapping Instances Implementation],
674 -- although this is used for more than just that failure case.
675
676 tcg_tc_plugins :: [TcPluginSolver],
677 -- ^ A list of user-defined plugins for the constraint solver.
678
679 tcg_top_loc :: RealSrcSpan,
680 -- ^ The RealSrcSpan this module came from
681
682 tcg_static_wc :: TcRef WantedConstraints,
683 -- ^ Wanted constraints of static forms.
684 -- See Note [Constraints in static forms].
685 tcg_complete_matches :: [CompleteMatch],
686
687 -- ^ Tracking indices for cost centre annotations
688 tcg_cc_st :: TcRef CostCentreState
689 }
690
691 -- NB: topModIdentity, not topModSemantic!
692 -- Definition sites of orphan identities will be identity modules, not semantic
693 -- modules.
694
695 -- Note [Constraints in static forms]
696 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
697 --
698 -- When a static form produces constraints like
699 --
700 -- f :: StaticPtr (Bool -> String)
701 -- f = static show
702 --
703 -- we collect them in tcg_static_wc and resolve them at the end
704 -- of type checking. They need to be resolved separately because
705 -- we don't want to resolve them in the context of the enclosing
706 -- expression. Consider
707 --
708 -- g :: Show a => StaticPtr (a -> String)
709 -- g = static show
710 --
711 -- If the @Show a0@ constraint that the body of the static form produces was
712 -- resolved in the context of the enclosing expression, then the body of the
713 -- static form wouldn't be closed because the Show dictionary would come from
714 -- g's context instead of coming from the top level.
715
716 tcVisibleOrphanMods :: TcGblEnv -> ModuleSet
717 tcVisibleOrphanMods tcg_env
718 = mkModuleSet (tcg_mod tcg_env : imp_orphs (tcg_imports tcg_env))
719
720 instance ContainsModule TcGblEnv where
721 extractModule env = tcg_semantic_mod env
722
723 type RecFieldEnv = NameEnv [FieldLabel]
724 -- Maps a constructor name *in this module*
725 -- to the fields for that constructor.
726 -- This is used when dealing with ".." notation in record
727 -- construction and pattern matching.
728 -- The FieldEnv deals *only* with constructors defined in *this*
729 -- module. For imported modules, we get the same info from the
730 -- TypeEnv
731
732 data SelfBootInfo
733 = NoSelfBoot -- No corresponding hi-boot file
734 | SelfBoot
735 { sb_mds :: ModDetails -- There was a hi-boot file,
736 , sb_tcs :: NameSet } -- defining these TyCons,
737 -- What is sb_tcs used for? See Note [Extra dependencies from .hs-boot files]
738 -- in RnSource
739
740
741 {- Note [Tracking unused binding and imports]
742 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
743 We gather two sorts of usage information
744
745 * tcg_dus (defs/uses)
746 Records *defined* Names (local, top-level)
747 and *used* Names (local or imported)
748
749 Used (a) to report "defined but not used"
750 (see RnNames.reportUnusedNames)
751 (b) to generate version-tracking usage info in interface
752 files (see MkIface.mkUsedNames)
753 This usage info is mainly gathered by the renamer's
754 gathering of free-variables
755
756 * tcg_used_gres
757 Used only to report unused import declarations
758
759 Records each *occurrence* an *imported* (not locally-defined) entity.
760 The occurrence is recorded by keeping a GlobalRdrElt for it.
761 These is not the GRE that is in the GlobalRdrEnv; rather it
762 is recorded *after* the filtering done by pickGREs. So it reflect
763 /how that occurrence is in scope/. See Note [GRE filtering] in
764 RdrName.
765
766
767 ************************************************************************
768 * *
769 The local typechecker environment
770 * *
771 ************************************************************************
772
773 Note [The Global-Env/Local-Env story]
774 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
775 During type checking, we keep in the tcg_type_env
776 * All types and classes
777 * All Ids derived from types and classes (constructors, selectors)
778
779 At the end of type checking, we zonk the local bindings,
780 and as we do so we add to the tcg_type_env
781 * Locally defined top-level Ids
782
783 Why? Because they are now Ids not TcIds. This final GlobalEnv is
784 a) fed back (via the knot) to typechecking the
785 unfoldings of interface signatures
786 b) used in the ModDetails of this module
787 -}
788
789 data TcLclEnv -- Changes as we move inside an expression
790 -- Discarded after typecheck/rename; not passed on to desugarer
791 = TcLclEnv {
792 tcl_loc :: RealSrcSpan, -- Source span
793 tcl_ctxt :: [ErrCtxt], -- Error context, innermost on top
794 tcl_tclvl :: TcLevel, -- Birthplace for new unification variables
795
796 tcl_th_ctxt :: ThStage, -- Template Haskell context
797 tcl_th_bndrs :: ThBindEnv, -- and binder info
798 -- The ThBindEnv records the TH binding level of in-scope Names
799 -- defined in this module (not imported)
800 -- We can't put this info in the TypeEnv because it's needed
801 -- (and extended) in the renamer, for untyed splices
802
803 tcl_arrow_ctxt :: ArrowCtxt, -- Arrow-notation context
804
805 tcl_rdr :: LocalRdrEnv, -- Local name envt
806 -- Maintained during renaming, of course, but also during
807 -- type checking, solely so that when renaming a Template-Haskell
808 -- splice we have the right environment for the renamer.
809 --
810 -- Does *not* include global name envt; may shadow it
811 -- Includes both ordinary variables and type variables;
812 -- they are kept distinct because tyvar have a different
813 -- occurrence constructor (Name.TvOcc)
814 -- We still need the unsullied global name env so that
815 -- we can look up record field names
816
817 tcl_env :: TcTypeEnv, -- The local type environment:
818 -- Ids and TyVars defined in this module
819
820 tcl_bndrs :: TcBinderStack, -- Used for reporting relevant bindings,
821 -- and for tidying types
822
823 tcl_tyvars :: TcRef TcTyVarSet, -- The "global tyvars"
824 -- Namely, the in-scope TyVars bound in tcl_env,
825 -- plus the tyvars mentioned in the types of Ids bound
826 -- in tcl_lenv.
827 -- Why mutable? see notes with tcGetGlobalTyCoVars
828
829 tcl_lie :: TcRef WantedConstraints, -- Place to accumulate type constraints
830 tcl_errs :: TcRef Messages -- Place to accumulate errors
831 }
832
833 type ErrCtxt = (Bool, TidyEnv -> TcM (TidyEnv, MsgDoc))
834 -- Monadic so that we have a chance
835 -- to deal with bound type variables just before error
836 -- message construction
837
838 -- Bool: True <=> this is a landmark context; do not
839 -- discard it when trimming for display
840
841 type TcTypeEnv = NameEnv TcTyThing
842
843 type ThBindEnv = NameEnv (TopLevelFlag, ThLevel)
844 -- Domain = all Ids bound in this module (ie not imported)
845 -- The TopLevelFlag tells if the binding is syntactically top level.
846 -- We need to know this, because the cross-stage persistence story allows
847 -- cross-stage at arbitrary types if the Id is bound at top level.
848 --
849 -- Nota bene: a ThLevel of 'outerLevel' is *not* the same as being
850 -- bound at top level! See Note [Template Haskell levels] in TcSplice
851
852 {- Note [Given Insts]
853 ~~~~~~~~~~~~~~~~~~
854 Because of GADTs, we have to pass inwards the Insts provided by type signatures
855 and existential contexts. Consider
856 data T a where { T1 :: b -> b -> T [b] }
857 f :: Eq a => T a -> Bool
858 f (T1 x y) = [x]==[y]
859
860 The constructor T1 binds an existential variable 'b', and we need Eq [b].
861 Well, we have it, because Eq a refines to Eq [b], but we can only spot that if we
862 pass it inwards.
863
864 -}
865
866 -- | Type alias for 'IORef'; the convention is we'll use this for mutable
867 -- bits of data in 'TcGblEnv' which are updated during typechecking and
868 -- returned at the end.
869 type TcRef a = IORef a
870 -- ToDo: when should I refer to it as a 'TcId' instead of an 'Id'?
871 type TcId = Id
872 type TcIdSet = IdSet
873
874 ---------------------------
875 -- The TcBinderStack
876 ---------------------------
877
878 type TcBinderStack = [TcBinder]
879 -- This is a stack of locally-bound ids and tyvars,
880 -- innermost on top
881 -- Used only in error reporting (relevantBindings in TcError),
882 -- and in tidying
883 -- We can't use the tcl_env type environment, because it doesn't
884 -- keep track of the nesting order
885
886 data TcBinder
887 = TcIdBndr
888 TcId
889 TopLevelFlag -- Tells whether the binding is syntactically top-level
890 -- (The monomorphic Ids for a recursive group count
891 -- as not-top-level for this purpose.)
892
893 | TcIdBndr_ExpType -- Variant that allows the type to be specified as
894 -- an ExpType
895 Name
896 ExpType
897 TopLevelFlag
898
899 | TcTvBndr -- e.g. case x of P (y::a) -> blah
900 Name -- We bind the lexical name "a" to the type of y,
901 TyVar -- which might be an utterly different (perhaps
902 -- existential) tyvar
903
904 instance Outputable TcBinder where
905 ppr (TcIdBndr id top_lvl) = ppr id <> brackets (ppr top_lvl)
906 ppr (TcIdBndr_ExpType id _ top_lvl) = ppr id <> brackets (ppr top_lvl)
907 ppr (TcTvBndr name tv) = ppr name <+> ppr tv
908
909 instance HasOccName TcBinder where
910 occName (TcIdBndr id _) = occName (idName id)
911 occName (TcIdBndr_ExpType name _ _) = occName name
912 occName (TcTvBndr name _) = occName name
913
914 -- fixes #12177
915 -- Builds up a list of bindings whose OccName has not been seen before
916 -- i.e., If ys = removeBindingShadowing xs
917 -- then
918 -- - ys is obtained from xs by deleting some elements
919 -- - ys has no duplicate OccNames
920 -- - The first duplicated OccName in xs is retained in ys
921 -- Overloaded so that it can be used for both GlobalRdrElt in typed-hole
922 -- substitutions and TcBinder when looking for relevant bindings.
923 removeBindingShadowing :: HasOccName a => [a] -> [a]
924 removeBindingShadowing bindings = reverse $ fst $ foldl
925 (\(bindingAcc, seenNames) binding ->
926 if occName binding `elemOccSet` seenNames -- if we've seen it
927 then (bindingAcc, seenNames) -- skip it
928 else (binding:bindingAcc, extendOccSet seenNames (occName binding)))
929 ([], emptyOccSet) bindings
930
931 ---------------------------
932 -- Template Haskell stages and levels
933 ---------------------------
934
935 data SpliceType = Typed | Untyped
936
937 data ThStage -- See Note [Template Haskell state diagram] in TcSplice
938 = Splice SpliceType -- Inside a top-level splice
939 -- This code will be run *at compile time*;
940 -- the result replaces the splice
941 -- Binding level = 0
942
943 | RunSplice (TcRef [ForeignRef (TH.Q ())])
944 -- Set when running a splice, i.e. NOT when renaming or typechecking the
945 -- Haskell code for the splice. See Note [RunSplice ThLevel].
946 --
947 -- Contains a list of mod finalizers collected while executing the splice.
948 --
949 -- 'addModFinalizer' inserts finalizers here, and from here they are taken
950 -- to construct an @HsSpliced@ annotation for untyped splices. See Note
951 -- [Delaying modFinalizers in untyped splices] in "RnSplice".
952 --
953 -- For typed splices, the typechecker takes finalizers from here and
954 -- inserts them in the list of finalizers in the global environment.
955 --
956 -- See Note [Collecting modFinalizers in typed splices] in "TcSplice".
957
958 | Comp -- Ordinary Haskell code
959 -- Binding level = 1
960
961 | Brack -- Inside brackets
962 ThStage -- Enclosing stage
963 PendingStuff
964
965 data PendingStuff
966 = RnPendingUntyped -- Renaming the inside of an *untyped* bracket
967 (TcRef [PendingRnSplice]) -- Pending splices in here
968
969 | RnPendingTyped -- Renaming the inside of a *typed* bracket
970
971 | TcPending -- Typechecking the inside of a typed bracket
972 (TcRef [PendingTcSplice]) -- Accumulate pending splices here
973 (TcRef WantedConstraints) -- and type constraints here
974
975 topStage, topAnnStage, topSpliceStage :: ThStage
976 topStage = Comp
977 topAnnStage = Splice Untyped
978 topSpliceStage = Splice Untyped
979
980 instance Outputable ThStage where
981 ppr (Splice _) = text "Splice"
982 ppr (RunSplice _) = text "RunSplice"
983 ppr Comp = text "Comp"
984 ppr (Brack s _) = text "Brack" <> parens (ppr s)
985
986 type ThLevel = Int
987 -- NB: see Note [Template Haskell levels] in TcSplice
988 -- Incremented when going inside a bracket,
989 -- decremented when going inside a splice
990 -- NB: ThLevel is one greater than the 'n' in Fig 2 of the
991 -- original "Template meta-programming for Haskell" paper
992
993 impLevel, outerLevel :: ThLevel
994 impLevel = 0 -- Imported things; they can be used inside a top level splice
995 outerLevel = 1 -- Things defined outside brackets
996
997 thLevel :: ThStage -> ThLevel
998 thLevel (Splice _) = 0
999 thLevel (RunSplice _) =
1000 -- See Note [RunSplice ThLevel].
1001 panic "thLevel: called when running a splice"
1002 thLevel Comp = 1
1003 thLevel (Brack s _) = thLevel s + 1
1004
1005 {- Node [RunSplice ThLevel]
1006 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1007 The 'RunSplice' stage is set when executing a splice, and only when running a
1008 splice. In particular it is not set when the splice is renamed or typechecked.
1009
1010 'RunSplice' is needed to provide a reference where 'addModFinalizer' can insert
1011 the finalizer (see Note [Delaying modFinalizers in untyped splices]), and
1012 'addModFinalizer' runs when doing Q things. Therefore, It doesn't make sense to
1013 set 'RunSplice' when renaming or typechecking the splice, where 'Splice', 'Brak'
1014 or 'Comp' are used instead.
1015
1016 -}
1017
1018 ---------------------------
1019 -- Arrow-notation context
1020 ---------------------------
1021
1022 {- Note [Escaping the arrow scope]
1023 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1024 In arrow notation, a variable bound by a proc (or enclosed let/kappa)
1025 is not in scope to the left of an arrow tail (-<) or the head of (|..|).
1026 For example
1027
1028 proc x -> (e1 -< e2)
1029
1030 Here, x is not in scope in e1, but it is in scope in e2. This can get
1031 a bit complicated:
1032
1033 let x = 3 in
1034 proc y -> (proc z -> e1) -< e2
1035
1036 Here, x and z are in scope in e1, but y is not.
1037
1038 We implement this by
1039 recording the environment when passing a proc (using newArrowScope),
1040 and returning to that (using escapeArrowScope) on the left of -< and the
1041 head of (|..|).
1042
1043 All this can be dealt with by the *renamer*. But the type checker needs
1044 to be involved too. Example (arrowfail001)
1045 class Foo a where foo :: a -> ()
1046 data Bar = forall a. Foo a => Bar a
1047 get :: Bar -> ()
1048 get = proc x -> case x of Bar a -> foo -< a
1049 Here the call of 'foo' gives rise to a (Foo a) constraint that should not
1050 be captured by the pattern match on 'Bar'. Rather it should join the
1051 constraints from further out. So we must capture the constraint bag
1052 from further out in the ArrowCtxt that we push inwards.
1053 -}
1054
1055 data ArrowCtxt -- Note [Escaping the arrow scope]
1056 = NoArrowCtxt
1057 | ArrowCtxt LocalRdrEnv (TcRef WantedConstraints)
1058
1059
1060 ---------------------------
1061 -- TcTyThing
1062 ---------------------------
1063
1064 -- | A typecheckable thing available in a local context. Could be
1065 -- 'AGlobal' 'TyThing', but also lexically scoped variables, etc.
1066 -- See 'TcEnv' for how to retrieve a 'TyThing' given a 'Name'.
1067 data TcTyThing
1068 = AGlobal TyThing -- Used only in the return type of a lookup
1069
1070 | ATcId -- Ids defined in this module; may not be fully zonked
1071 { tct_id :: TcId
1072 , tct_info :: IdBindingInfo -- See Note [Meaning of IdBindingInfo]
1073 }
1074
1075 | ATyVar Name TcTyVar -- The type variable to which the lexically scoped type
1076 -- variable is bound. We only need the Name
1077 -- for error-message purposes; it is the corresponding
1078 -- Name in the domain of the envt
1079
1080 | ATcTyCon TyCon -- Used temporarily, during kind checking, for the
1081 -- tycons and clases in this recursive group
1082 -- The TyCon is always a TcTyCon. Its kind
1083 -- can be a mono-kind or a poly-kind; in TcTyClsDcls see
1084 -- Note [Type checking recursive type and class declarations]
1085
1086 | APromotionErr PromotionErr
1087
1088 data PromotionErr
1089 = TyConPE -- TyCon used in a kind before we are ready
1090 -- data T :: T -> * where ...
1091 | ClassPE -- Ditto Class
1092
1093 | FamDataConPE -- Data constructor for a data family
1094 -- See Note [AFamDataCon: not promoting data family constructors]
1095 -- in TcEnv.
1096 | PatSynPE -- Pattern synonyms
1097 -- See Note [Don't promote pattern synonyms] in TcEnv
1098
1099 | PatSynExPE -- Pattern synonym existential type variable
1100 -- See Note [Pattern synonym existentials do not scope] in TcPatSyn
1101
1102 | RecDataConPE -- Data constructor in a recursive loop
1103 -- See Note [Recursion and promoting data constructors] in TcTyClsDecls
1104 | NoDataKindsTC -- -XDataKinds not enabled (for a tycon)
1105 | NoDataKindsDC -- -XDataKinds not enabled (for a datacon)
1106 | NoTypeInTypeTC -- -XTypeInType not enabled (for a tycon)
1107 | NoTypeInTypeDC -- -XTypeInType not enabled (for a datacon)
1108
1109 instance Outputable TcTyThing where -- Debugging only
1110 ppr (AGlobal g) = ppr g
1111 ppr elt@(ATcId {}) = text "Identifier" <>
1112 brackets (ppr (tct_id elt) <> dcolon
1113 <> ppr (varType (tct_id elt)) <> comma
1114 <+> ppr (tct_info elt))
1115 ppr (ATyVar n tv) = text "Type variable" <+> quotes (ppr n) <+> equals <+> ppr tv
1116 <+> dcolon <+> ppr (varType tv)
1117 ppr (ATcTyCon tc) = text "ATcTyCon" <+> ppr tc <+> dcolon <+> ppr (tyConKind tc)
1118 ppr (APromotionErr err) = text "APromotionErr" <+> ppr err
1119
1120 -- | IdBindingInfo describes how an Id is bound.
1121 --
1122 -- It is used for the following purposes:
1123 -- a) for static forms in TcExpr.checkClosedInStaticForm and
1124 -- b) to figure out when a nested binding can be generalised,
1125 -- in TcBinds.decideGeneralisationPlan.
1126 --
1127 data IdBindingInfo -- See Note [Meaning of IdBindingInfo and ClosedTypeId]
1128 = NotLetBound
1129 | ClosedLet
1130 | NonClosedLet
1131 RhsNames -- Used for (static e) checks only
1132 ClosedTypeId -- Used for generalisation checks
1133 -- and for (static e) checks
1134
1135 -- | IsGroupClosed describes a group of mutually-recursive bindings
1136 data IsGroupClosed
1137 = IsGroupClosed
1138 (NameEnv RhsNames) -- Free var info for the RHS of each binding in the goup
1139 -- Used only for (static e) checks
1140
1141 ClosedTypeId -- True <=> all the free vars of the group are
1142 -- imported or ClosedLet or
1143 -- NonClosedLet with ClosedTypeId=True.
1144 -- In particular, no tyvars, no NotLetBound
1145
1146 type RhsNames = NameSet -- Names of variables, mentioned on the RHS of
1147 -- a definition, that are not Global or ClosedLet
1148
1149 type ClosedTypeId = Bool
1150 -- See Note [Meaning of IdBindingInfo and ClosedTypeId]
1151
1152 {- Note [Meaning of IdBindingInfo]
1153 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1154 NotLetBound means that
1155 the Id is not let-bound (e.g. it is bound in a
1156 lambda-abstraction or in a case pattern)
1157
1158 ClosedLet means that
1159 - The Id is let-bound,
1160 - Any free term variables are also Global or ClosedLet
1161 - Its type has no free variables (NB: a top-level binding subject
1162 to the MR might have free vars in its type)
1163 These ClosedLets can definitely be floated to top level; and we
1164 may need to do so for static forms.
1165
1166 Property: ClosedLet
1167 is equivalent to
1168 NonClosedLet emptyNameSet True
1169
1170 (NonClosedLet (fvs::RhsNames) (cl::ClosedTypeId)) means that
1171 - The Id is let-bound
1172
1173 - The fvs::RhsNames contains the free names of the RHS,
1174 excluding Global and ClosedLet ones.
1175
1176 - For the ClosedTypeId field see Note [Bindings with closed types]
1177
1178 For (static e) to be valid, we need for every 'x' free in 'e',
1179 that x's binding is floatable to the top level. Specifically:
1180 * x's RhsNames must be empty
1181 * x's type has no free variables
1182 See Note [Grand plan for static forms] in StaticPtrTable.hs.
1183 This test is made in TcExpr.checkClosedInStaticForm.
1184 Actually knowing x's RhsNames (rather than just its emptiness
1185 or otherwise) is just so we can produce better error messages
1186
1187 Note [Bindings with closed types: ClosedTypeId]
1188 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1189 Consider
1190
1191 f x = let g ys = map not ys
1192 in ...
1193
1194 Can we generalise 'g' under the OutsideIn algorithm? Yes,
1195 because all g's free variables are top-level; that is they themselves
1196 have no free type variables, and it is the type variables in the
1197 environment that makes things tricky for OutsideIn generalisation.
1198
1199 Here's the invariant:
1200 If an Id has ClosedTypeId=True (in its IdBindingInfo), then
1201 the Id's type is /definitely/ closed (has no free type variables).
1202 Specifically,
1203 a) The Id's acutal type is closed (has no free tyvars)
1204 b) Either the Id has a (closed) user-supplied type signature
1205 or all its free variables are Global/ClosedLet
1206 or NonClosedLet with ClosedTypeId=True.
1207 In particular, none are NotLetBound.
1208
1209 Why is (b) needed? Consider
1210 \x. (x :: Int, let y = x+1 in ...)
1211 Initially x::alpha. If we happen to typecheck the 'let' before the
1212 (x::Int), y's type will have a free tyvar; but if the other way round
1213 it won't. So we treat any let-bound variable with a free
1214 non-let-bound variable as not ClosedTypeId, regardless of what the
1215 free vars of its type actually are.
1216
1217 But if it has a signature, all is well:
1218 \x. ...(let { y::Int; y = x+1 } in
1219 let { v = y+2 } in ...)...
1220 Here the signature on 'v' makes 'y' a ClosedTypeId, so we can
1221 generalise 'v'.
1222
1223 Note that:
1224
1225 * A top-level binding may not have ClosedTypeId=True, if it suffers
1226 from the MR
1227
1228 * A nested binding may be closed (eg 'g' in the example we started
1229 with). Indeed, that's the point; whether a function is defined at
1230 top level or nested is orthogonal to the question of whether or
1231 not it is closed.
1232
1233 * A binding may be non-closed because it mentions a lexically scoped
1234 *type variable* Eg
1235 f :: forall a. blah
1236 f x = let g y = ...(y::a)...
1237
1238 Under OutsideIn we are free to generalise an Id all of whose free
1239 variables have ClosedTypeId=True (or imported). This is an extension
1240 compared to the JFP paper on OutsideIn, which used "top-level" as a
1241 proxy for "closed". (It's not a good proxy anyway -- the MR can make
1242 a top-level binding with a free type variable.)
1243 -}
1244
1245 instance Outputable IdBindingInfo where
1246 ppr NotLetBound = text "NotLetBound"
1247 ppr ClosedLet = text "TopLevelLet"
1248 ppr (NonClosedLet fvs closed_type) =
1249 text "TopLevelLet" <+> ppr fvs <+> ppr closed_type
1250
1251 instance Outputable PromotionErr where
1252 ppr ClassPE = text "ClassPE"
1253 ppr TyConPE = text "TyConPE"
1254 ppr PatSynPE = text "PatSynPE"
1255 ppr PatSynExPE = text "PatSynExPE"
1256 ppr FamDataConPE = text "FamDataConPE"
1257 ppr RecDataConPE = text "RecDataConPE"
1258 ppr NoDataKindsTC = text "NoDataKindsTC"
1259 ppr NoDataKindsDC = text "NoDataKindsDC"
1260 ppr NoTypeInTypeTC = text "NoTypeInTypeTC"
1261 ppr NoTypeInTypeDC = text "NoTypeInTypeDC"
1262
1263 pprTcTyThingCategory :: TcTyThing -> SDoc
1264 pprTcTyThingCategory (AGlobal thing) = pprTyThingCategory thing
1265 pprTcTyThingCategory (ATyVar {}) = text "Type variable"
1266 pprTcTyThingCategory (ATcId {}) = text "Local identifier"
1267 pprTcTyThingCategory (ATcTyCon {}) = text "Local tycon"
1268 pprTcTyThingCategory (APromotionErr pe) = pprPECategory pe
1269
1270 pprPECategory :: PromotionErr -> SDoc
1271 pprPECategory ClassPE = text "Class"
1272 pprPECategory TyConPE = text "Type constructor"
1273 pprPECategory PatSynPE = text "Pattern synonym"
1274 pprPECategory PatSynExPE = text "Pattern synonym existential"
1275 pprPECategory FamDataConPE = text "Data constructor"
1276 pprPECategory RecDataConPE = text "Data constructor"
1277 pprPECategory NoDataKindsTC = text "Type constructor"
1278 pprPECategory NoDataKindsDC = text "Data constructor"
1279 pprPECategory NoTypeInTypeTC = text "Type constructor"
1280 pprPECategory NoTypeInTypeDC = text "Data constructor"
1281
1282 {-
1283 ************************************************************************
1284 * *
1285 Operations over ImportAvails
1286 * *
1287 ************************************************************************
1288 -}
1289
1290 -- | 'ImportAvails' summarises what was imported from where, irrespective of
1291 -- whether the imported things are actually used or not. It is used:
1292 --
1293 -- * when processing the export list,
1294 --
1295 -- * when constructing usage info for the interface file,
1296 --
1297 -- * to identify the list of directly imported modules for initialisation
1298 -- purposes and for optimised overlap checking of family instances,
1299 --
1300 -- * when figuring out what things are really unused
1301 --
1302 data ImportAvails
1303 = ImportAvails {
1304 imp_mods :: ImportedMods,
1305 -- = ModuleEnv [ImportedModsVal],
1306 -- ^ Domain is all directly-imported modules
1307 --
1308 -- See the documentation on ImportedModsVal in HscTypes for the
1309 -- meaning of the fields.
1310 --
1311 -- We need a full ModuleEnv rather than a ModuleNameEnv here,
1312 -- because we might be importing modules of the same name from
1313 -- different packages. (currently not the case, but might be in the
1314 -- future).
1315
1316 imp_dep_mods :: ModuleNameEnv (ModuleName, IsBootInterface),
1317 -- ^ Home-package modules needed by the module being compiled
1318 --
1319 -- It doesn't matter whether any of these dependencies
1320 -- are actually /used/ when compiling the module; they
1321 -- are listed if they are below it at all. For
1322 -- example, suppose M imports A which imports X. Then
1323 -- compiling M might not need to consult X.hi, but X
1324 -- is still listed in M's dependencies.
1325
1326 imp_dep_pkgs :: Set InstalledUnitId,
1327 -- ^ Packages needed by the module being compiled, whether directly,
1328 -- or via other modules in this package, or via modules imported
1329 -- from other packages.
1330
1331 imp_trust_pkgs :: Set InstalledUnitId,
1332 -- ^ This is strictly a subset of imp_dep_pkgs and records the
1333 -- packages the current module needs to trust for Safe Haskell
1334 -- compilation to succeed. A package is required to be trusted if
1335 -- we are dependent on a trustworthy module in that package.
1336 -- While perhaps making imp_dep_pkgs a tuple of (UnitId, Bool)
1337 -- where True for the bool indicates the package is required to be
1338 -- trusted is the more logical design, doing so complicates a lot
1339 -- of code not concerned with Safe Haskell.
1340 -- See Note [RnNames . Tracking Trust Transitively]
1341
1342 imp_trust_own_pkg :: Bool,
1343 -- ^ Do we require that our own package is trusted?
1344 -- This is to handle efficiently the case where a Safe module imports
1345 -- a Trustworthy module that resides in the same package as it.
1346 -- See Note [RnNames . Trust Own Package]
1347
1348 imp_orphs :: [Module],
1349 -- ^ Orphan modules below us in the import tree (and maybe including
1350 -- us for imported modules)
1351
1352 imp_finsts :: [Module]
1353 -- ^ Family instance modules below us in the import tree (and maybe
1354 -- including us for imported modules)
1355 }
1356
1357 mkModDeps :: [(ModuleName, IsBootInterface)]
1358 -> ModuleNameEnv (ModuleName, IsBootInterface)
1359 mkModDeps deps = foldl add emptyUFM deps
1360 where
1361 add env elt@(m,_) = addToUFM env m elt
1362
1363 modDepsElts
1364 :: ModuleNameEnv (ModuleName, IsBootInterface)
1365 -> [(ModuleName, IsBootInterface)]
1366 modDepsElts = sort . nonDetEltsUFM
1367 -- It's OK to use nonDetEltsUFM here because sorting by module names
1368 -- restores determinism
1369
1370 emptyImportAvails :: ImportAvails
1371 emptyImportAvails = ImportAvails { imp_mods = emptyModuleEnv,
1372 imp_dep_mods = emptyUFM,
1373 imp_dep_pkgs = S.empty,
1374 imp_trust_pkgs = S.empty,
1375 imp_trust_own_pkg = False,
1376 imp_orphs = [],
1377 imp_finsts = [] }
1378
1379 -- | Union two ImportAvails
1380 --
1381 -- This function is a key part of Import handling, basically
1382 -- for each import we create a separate ImportAvails structure
1383 -- and then union them all together with this function.
1384 plusImportAvails :: ImportAvails -> ImportAvails -> ImportAvails
1385 plusImportAvails
1386 (ImportAvails { imp_mods = mods1,
1387 imp_dep_mods = dmods1, imp_dep_pkgs = dpkgs1,
1388 imp_trust_pkgs = tpkgs1, imp_trust_own_pkg = tself1,
1389 imp_orphs = orphs1, imp_finsts = finsts1 })
1390 (ImportAvails { imp_mods = mods2,
1391 imp_dep_mods = dmods2, imp_dep_pkgs = dpkgs2,
1392 imp_trust_pkgs = tpkgs2, imp_trust_own_pkg = tself2,
1393 imp_orphs = orphs2, imp_finsts = finsts2 })
1394 = ImportAvails { imp_mods = plusModuleEnv_C (++) mods1 mods2,
1395 imp_dep_mods = plusUFM_C plus_mod_dep dmods1 dmods2,
1396 imp_dep_pkgs = dpkgs1 `S.union` dpkgs2,
1397 imp_trust_pkgs = tpkgs1 `S.union` tpkgs2,
1398 imp_trust_own_pkg = tself1 || tself2,
1399 imp_orphs = orphs1 `unionLists` orphs2,
1400 imp_finsts = finsts1 `unionLists` finsts2 }
1401 where
1402 plus_mod_dep r1@(m1, boot1) r2@(m2, boot2)
1403 | ASSERT2( m1 == m2, (ppr m1 <+> ppr m2) $$ (ppr boot1 <+> ppr boot2) )
1404 boot1 = r2
1405 | otherwise = r1
1406 -- If either side can "see" a non-hi-boot interface, use that
1407 -- Reusing existing tuples saves 10% of allocations on test
1408 -- perf/compiler/MultiLayerModules
1409
1410 {-
1411 ************************************************************************
1412 * *
1413 \subsection{Where from}
1414 * *
1415 ************************************************************************
1416
1417 The @WhereFrom@ type controls where the renamer looks for an interface file
1418 -}
1419
1420 data WhereFrom
1421 = ImportByUser IsBootInterface -- Ordinary user import (perhaps {-# SOURCE #-})
1422 | ImportBySystem -- Non user import.
1423 | ImportByPlugin -- Importing a plugin;
1424 -- See Note [Care with plugin imports] in LoadIface
1425
1426 instance Outputable WhereFrom where
1427 ppr (ImportByUser is_boot) | is_boot = text "{- SOURCE -}"
1428 | otherwise = empty
1429 ppr ImportBySystem = text "{- SYSTEM -}"
1430 ppr ImportByPlugin = text "{- PLUGIN -}"
1431
1432
1433 {- *********************************************************************
1434 * *
1435 Type signatures
1436 * *
1437 ********************************************************************* -}
1438
1439 -- These data types need to be here only because
1440 -- TcSimplify uses them, and TcSimplify is fairly
1441 -- low down in the module hierarchy
1442
1443 type TcSigFun = Name -> Maybe TcSigInfo
1444
1445 data TcSigInfo = TcIdSig TcIdSigInfo
1446 | TcPatSynSig TcPatSynInfo
1447
1448 data TcIdSigInfo -- See Note [Complete and partial type signatures]
1449 = CompleteSig -- A complete signature with no wildcards,
1450 -- so the complete polymorphic type is known.
1451 { sig_bndr :: TcId -- The polymorphic Id with that type
1452
1453 , sig_ctxt :: UserTypeCtxt -- In the case of type-class default methods,
1454 -- the Name in the FunSigCtxt is not the same
1455 -- as the TcId; the former is 'op', while the
1456 -- latter is '$dmop' or some such
1457
1458 , sig_loc :: SrcSpan -- Location of the type signature
1459 }
1460
1461 | PartialSig -- A partial type signature (i.e. includes one or more
1462 -- wildcards). In this case it doesn't make sense to give
1463 -- the polymorphic Id, because we are going to /infer/ its
1464 -- type, so we can't make the polymorphic Id ab-initio
1465 { psig_name :: Name -- Name of the function; used when report wildcards
1466 , psig_hs_ty :: LHsSigWcType GhcRn -- The original partial signature in
1467 -- HsSyn form
1468 , sig_ctxt :: UserTypeCtxt
1469 , sig_loc :: SrcSpan -- Location of the type signature
1470 }
1471
1472
1473 {- Note [Complete and partial type signatures]
1474 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1475 A type signature is partial when it contains one or more wildcards
1476 (= type holes). The wildcard can either be:
1477 * A (type) wildcard occurring in sig_theta or sig_tau. These are
1478 stored in sig_wcs.
1479 f :: Bool -> _
1480 g :: Eq _a => _a -> _a -> Bool
1481 * Or an extra-constraints wildcard, stored in sig_cts:
1482 h :: (Num a, _) => a -> a
1483
1484 A type signature is a complete type signature when there are no
1485 wildcards in the type signature, i.e. iff sig_wcs is empty and
1486 sig_extra_cts is Nothing.
1487 -}
1488
1489 data TcIdSigInst
1490 = TISI { sig_inst_sig :: TcIdSigInfo
1491
1492 , sig_inst_skols :: [(Name, TcTyVar)]
1493 -- Instantiated type and kind variables, SigTvs
1494 -- The Name is the Name that the renamer chose;
1495 -- but the TcTyVar may come from instantiating
1496 -- the type and hence have a different unique.
1497 -- No need to keep track of whether they are truly lexically
1498 -- scoped because the renamer has named them uniquely
1499 -- See Note [Binding scoped type variables] in TcSigs
1500
1501 , sig_inst_theta :: TcThetaType
1502 -- Instantiated theta. In the case of a
1503 -- PartialSig, sig_theta does not include
1504 -- the extra-constraints wildcard
1505
1506 , sig_inst_tau :: TcSigmaType -- Instantiated tau
1507 -- See Note [sig_inst_tau may be polymorphic]
1508
1509 -- Relevant for partial signature only
1510 , sig_inst_wcs :: [(Name, TcTyVar)]
1511 -- Like sig_inst_skols, but for wildcards. The named
1512 -- wildcards scope over the binding, and hence their
1513 -- Names may appear in type signatures in the binding
1514
1515 , sig_inst_wcx :: Maybe TcType
1516 -- Extra-constraints wildcard to fill in, if any
1517 -- If this exists, it is surely of the form (meta_tv |> co)
1518 -- (where the co might be reflexive). This is filled in
1519 -- only from the return value of TcHsType.tcWildCardOcc
1520 }
1521
1522 {- Note [sig_inst_tau may be polymorphic]
1523 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1524 Note that "sig_inst_tau" might actually be a polymorphic type,
1525 if the original function had a signature like
1526 forall a. Eq a => forall b. Ord b => ....
1527 But that's ok: tcMatchesFun (called by tcRhs) can deal with that
1528 It happens, too! See Note [Polymorphic methods] in TcClassDcl.
1529
1530 Note [Wildcards in partial signatures]
1531 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1532 The wildcards in psig_wcs may stand for a type mentioning
1533 the universally-quantified tyvars of psig_ty
1534
1535 E.g. f :: forall a. _ -> a
1536 f x = x
1537 We get sig_inst_skols = [a]
1538 sig_inst_tau = _22 -> a
1539 sig_inst_wcs = [_22]
1540 and _22 in the end is unified with the type 'a'
1541
1542 Moreover the kind of a wildcard in sig_inst_wcs may mention
1543 the universally-quantified tyvars sig_inst_skols
1544 e.g. f :: t a -> t _
1545 Here we get
1546 sig_inst_skols = [k:*, (t::k ->*), (a::k)]
1547 sig_inst_tau = t a -> t _22
1548 sig_inst_wcs = [ _22::k ]
1549 -}
1550
1551 data TcPatSynInfo
1552 = TPSI {
1553 patsig_name :: Name,
1554 patsig_implicit_bndrs :: [TyVarBinder], -- Implicitly-bound kind vars (Inferred) and
1555 -- implicitly-bound type vars (Specified)
1556 -- See Note [The pattern-synonym signature splitting rule] in TcSigs
1557 patsig_univ_bndrs :: [TyVar], -- Bound by explicit user forall
1558 patsig_req :: TcThetaType,
1559 patsig_ex_bndrs :: [TyVar], -- Bound by explicit user forall
1560 patsig_prov :: TcThetaType,
1561 patsig_body_ty :: TcSigmaType
1562 }
1563
1564 instance Outputable TcSigInfo where
1565 ppr (TcIdSig idsi) = ppr idsi
1566 ppr (TcPatSynSig tpsi) = text "TcPatSynInfo" <+> ppr tpsi
1567
1568 instance Outputable TcIdSigInfo where
1569 ppr (CompleteSig { sig_bndr = bndr })
1570 = ppr bndr <+> dcolon <+> ppr (idType bndr)
1571 ppr (PartialSig { psig_name = name, psig_hs_ty = hs_ty })
1572 = text "psig" <+> ppr name <+> dcolon <+> ppr hs_ty
1573
1574 instance Outputable TcIdSigInst where
1575 ppr (TISI { sig_inst_sig = sig, sig_inst_skols = skols
1576 , sig_inst_theta = theta, sig_inst_tau = tau })
1577 = hang (ppr sig) 2 (vcat [ ppr skols, ppr theta <+> darrow <+> ppr tau ])
1578
1579 instance Outputable TcPatSynInfo where
1580 ppr (TPSI{ patsig_name = name}) = ppr name
1581
1582 isPartialSig :: TcIdSigInst -> Bool
1583 isPartialSig (TISI { sig_inst_sig = PartialSig {} }) = True
1584 isPartialSig _ = False
1585
1586 -- | No signature or a partial signature
1587 hasCompleteSig :: TcSigFun -> Name -> Bool
1588 hasCompleteSig sig_fn name
1589 = case sig_fn name of
1590 Just (TcIdSig (CompleteSig {})) -> True
1591 _ -> False
1592
1593
1594 {-
1595 ************************************************************************
1596 * *
1597 * Canonical constraints *
1598 * *
1599 * These are the constraints the low-level simplifier works with *
1600 * *
1601 ************************************************************************
1602 -}
1603
1604 -- The syntax of xi (ΞΎ) types:
1605 -- xi ::= a | T xis | xis -> xis | ... | forall a. tau
1606 -- Two important notes:
1607 -- (i) No type families, unless we are under a ForAll
1608 -- (ii) Note that xi types can contain unexpanded type synonyms;
1609 -- however, the (transitive) expansions of those type synonyms
1610 -- will not contain any type functions, unless we are under a ForAll.
1611 -- We enforce the structure of Xi types when we flatten (TcCanonical)
1612
1613 type Xi = Type -- In many comments, "xi" ranges over Xi
1614
1615 type Cts = Bag Ct
1616
1617 data Ct
1618 -- Atomic canonical constraints
1619 = CDictCan { -- e.g. Num xi
1620 cc_ev :: CtEvidence, -- See Note [Ct/evidence invariant]
1621
1622 cc_class :: Class,
1623 cc_tyargs :: [Xi], -- cc_tyargs are function-free, hence Xi
1624
1625 cc_pend_sc :: Bool -- See Note [The superclass story] in TcCanonical
1626 -- True <=> (a) cc_class has superclasses
1627 -- (b) we have not (yet) added those
1628 -- superclasses as Givens
1629 }
1630
1631 | CIrredCan { -- These stand for yet-unusable predicates
1632 cc_ev :: CtEvidence, -- See Note [Ct/evidence invariant]
1633 cc_insol :: Bool -- True <=> definitely an error, can never be solved
1634 -- False <=> might be soluble
1635
1636 -- For the might-be-soluble case, the ctev_pred of the evidence is
1637 -- of form (tv xi1 xi2 ... xin) with a tyvar at the head
1638 -- or (tv1 ~ ty2) where the CTyEqCan kind invariant fails
1639 -- or (F tys ~ ty) where the CFunEqCan kind invariant fails
1640 -- See Note [CIrredCan constraints]
1641
1642 -- The definitely-insoluble case is for things like
1643 -- Int ~ Bool tycons don't match
1644 -- a ~ [a] occurs check
1645 }
1646
1647 | CTyEqCan { -- tv ~ rhs
1648 -- Invariants:
1649 -- * See Note [Applying the inert substitution] in TcFlatten
1650 -- * tv not in tvs(rhs) (occurs check)
1651 -- * If tv is a TauTv, then rhs has no foralls
1652 -- (this avoids substituting a forall for the tyvar in other types)
1653 -- * typeKind ty `tcEqKind` typeKind tv; Note [Ct kind invariant]
1654 -- * rhs may have at most one top-level cast
1655 -- * rhs (perhaps under the one cast) is not necessarily function-free,
1656 -- but it has no top-level function.
1657 -- E.g. a ~ [F b] is fine
1658 -- but a ~ F b is not
1659 -- * If the equality is representational, rhs has no top-level newtype
1660 -- See Note [No top-level newtypes on RHS of representational
1661 -- equalities] in TcCanonical
1662 -- * If rhs (perhaps under the cast) is also a tv, then it is oriented
1663 -- to give best chance of
1664 -- unification happening; eg if rhs is touchable then lhs is too
1665 cc_ev :: CtEvidence, -- See Note [Ct/evidence invariant]
1666 cc_tyvar :: TcTyVar,
1667 cc_rhs :: TcType, -- Not necessarily function-free (hence not Xi)
1668 -- See invariants above
1669
1670 cc_eq_rel :: EqRel -- INVARIANT: cc_eq_rel = ctEvEqRel cc_ev
1671 }
1672
1673 | CFunEqCan { -- F xis ~ fsk
1674 -- Invariants:
1675 -- * isTypeFamilyTyCon cc_fun
1676 -- * typeKind (F xis) = tyVarKind fsk; Note [Ct kind invariant]
1677 -- * always Nominal role
1678 cc_ev :: CtEvidence, -- See Note [Ct/evidence invariant]
1679 cc_fun :: TyCon, -- A type function
1680
1681 cc_tyargs :: [Xi], -- cc_tyargs are function-free (hence Xi)
1682 -- Either under-saturated or exactly saturated
1683 -- *never* over-saturated (because if so
1684 -- we should have decomposed)
1685
1686 cc_fsk :: TcTyVar -- [G] always a FlatSkolTv
1687 -- [W], [WD], or [D] always a FlatMetaTv
1688 -- See Note [The flattening story] in TcFlatten
1689 }
1690
1691 | CNonCanonical { -- See Note [NonCanonical Semantics] in TcSMonad
1692 cc_ev :: CtEvidence
1693 }
1694
1695 | CHoleCan { -- See Note [Hole constraints]
1696 -- Treated as an "insoluble" constraint
1697 -- See Note [Insoluble constraints]
1698 cc_ev :: CtEvidence,
1699 cc_hole :: Hole
1700 }
1701
1702 -- | An expression or type hole
1703 data Hole = ExprHole UnboundVar
1704 -- ^ Either an out-of-scope variable or a "true" hole in an
1705 -- expression (TypedHoles)
1706 | TypeHole OccName
1707 -- ^ A hole in a type (PartialTypeSignatures)
1708
1709 instance Outputable Hole where
1710 ppr (ExprHole ub) = ppr ub
1711 ppr (TypeHole occ) = text "TypeHole" <> parens (ppr occ)
1712
1713 holeOcc :: Hole -> OccName
1714 holeOcc (ExprHole uv) = unboundVarOcc uv
1715 holeOcc (TypeHole occ) = occ
1716
1717 {- Note [Hole constraints]
1718 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1719 CHoleCan constraints are used for two kinds of holes,
1720 distinguished by cc_hole:
1721
1722 * For holes in expressions (including variables not in scope)
1723 e.g. f x = g _ x
1724
1725 * For holes in type signatures
1726 e.g. f :: _ -> _
1727 f x = [x,True]
1728
1729 Note [CIrredCan constraints]
1730 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1731 CIrredCan constraints are used for constraints that are "stuck"
1732 - we can't solve them (yet)
1733 - we can't use them to solve other constraints
1734 - but they may become soluble if we substitute for some
1735 of the type variables in the constraint
1736
1737 Example 1: (c Int), where c :: * -> Constraint. We can't do anything
1738 with this yet, but if later c := Num, *then* we can solve it
1739
1740 Example 2: a ~ b, where a :: *, b :: k, where k is a kind variable
1741 We don't want to use this to substitute 'b' for 'a', in case
1742 'k' is subequently unifed with (say) *->*, because then
1743 we'd have ill-kinded types floating about. Rather we want
1744 to defer using the equality altogether until 'k' get resolved.
1745
1746 Note [Ct/evidence invariant]
1747 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1748 If ct :: Ct, then extra fields of 'ct' cache precisely the ctev_pred field
1749 of (cc_ev ct), and is fully rewritten wrt the substitution. Eg for CDictCan,
1750 ctev_pred (cc_ev ct) = (cc_class ct) (cc_tyargs ct)
1751 This holds by construction; look at the unique place where CDictCan is
1752 built (in TcCanonical).
1753
1754 In contrast, the type of the evidence *term* (ctev_dest / ctev_evar) in
1755 the evidence may *not* be fully zonked; we are careful not to look at it
1756 during constraint solving. See Note [Evidence field of CtEvidence].
1757
1758 Note [Ct kind invariant]
1759 ~~~~~~~~~~~~~~~~~~~~~~~~
1760 CTyEqCan and CFunEqCan both require that the kind of the lhs matches the kind
1761 of the rhs. This is necessary because both constraints are used for substitutions
1762 during solving. If the kinds differed, then the substitution would take a well-kinded
1763 type to an ill-kinded one.
1764
1765 -}
1766
1767 mkNonCanonical :: CtEvidence -> Ct
1768 mkNonCanonical ev = CNonCanonical { cc_ev = ev }
1769
1770 mkNonCanonicalCt :: Ct -> Ct
1771 mkNonCanonicalCt ct = CNonCanonical { cc_ev = cc_ev ct }
1772
1773 mkIrredCt :: CtEvidence -> Ct
1774 mkIrredCt ev = CIrredCan { cc_ev = ev, cc_insol = False }
1775
1776 mkInsolubleCt :: CtEvidence -> Ct
1777 mkInsolubleCt ev = CIrredCan { cc_ev = ev, cc_insol = True }
1778
1779 mkGivens :: CtLoc -> [EvId] -> [Ct]
1780 mkGivens loc ev_ids
1781 = map mk ev_ids
1782 where
1783 mk ev_id = mkNonCanonical (CtGiven { ctev_evar = ev_id
1784 , ctev_pred = evVarPred ev_id
1785 , ctev_loc = loc })
1786
1787 ctEvidence :: Ct -> CtEvidence
1788 ctEvidence = cc_ev
1789
1790 ctLoc :: Ct -> CtLoc
1791 ctLoc = ctEvLoc . ctEvidence
1792
1793 setCtLoc :: Ct -> CtLoc -> Ct
1794 setCtLoc ct loc = ct { cc_ev = (cc_ev ct) { ctev_loc = loc } }
1795
1796 ctOrigin :: Ct -> CtOrigin
1797 ctOrigin = ctLocOrigin . ctLoc
1798
1799 ctPred :: Ct -> PredType
1800 -- See Note [Ct/evidence invariant]
1801 ctPred ct = ctEvPred (cc_ev ct)
1802
1803 ctEvId :: Ct -> EvVar
1804 -- The evidence Id for this Ct
1805 ctEvId ct = ctEvEvId (ctEvidence ct)
1806
1807 -- | Makes a new equality predicate with the same role as the given
1808 -- evidence.
1809 mkTcEqPredLikeEv :: CtEvidence -> TcType -> TcType -> TcType
1810 mkTcEqPredLikeEv ev
1811 = case predTypeEqRel pred of
1812 NomEq -> mkPrimEqPred
1813 ReprEq -> mkReprPrimEqPred
1814 where
1815 pred = ctEvPred ev
1816
1817 -- | Get the flavour of the given 'Ct'
1818 ctFlavour :: Ct -> CtFlavour
1819 ctFlavour = ctEvFlavour . ctEvidence
1820
1821 -- | Get the equality relation for the given 'Ct'
1822 ctEqRel :: Ct -> EqRel
1823 ctEqRel = ctEvEqRel . ctEvidence
1824
1825 instance Outputable Ct where
1826 ppr ct = ppr (cc_ev ct) <+> parens pp_sort
1827 where
1828 pp_sort = case ct of
1829 CTyEqCan {} -> text "CTyEqCan"
1830 CFunEqCan {} -> text "CFunEqCan"
1831 CNonCanonical {} -> text "CNonCanonical"
1832 CDictCan { cc_pend_sc = pend_sc }
1833 | pend_sc -> text "CDictCan(psc)"
1834 | otherwise -> text "CDictCan"
1835 CIrredCan { cc_insol = insol }
1836 | insol -> text "CIrredCan(insol)"
1837 | otherwise -> text "CIrredCan(sol)"
1838 CHoleCan { cc_hole = hole } -> text "CHoleCan:" <+> ppr hole
1839
1840 {-
1841 ************************************************************************
1842 * *
1843 Simple functions over evidence variables
1844 * *
1845 ************************************************************************
1846 -}
1847
1848 ---------------- Getting free tyvars -------------------------
1849
1850 -- | Returns free variables of constraints as a non-deterministic set
1851 tyCoVarsOfCt :: Ct -> TcTyCoVarSet
1852 tyCoVarsOfCt = fvVarSet . tyCoFVsOfCt
1853
1854 -- | Returns free variables of constraints as a deterministically ordered.
1855 -- list. See Note [Deterministic FV] in FV.
1856 tyCoVarsOfCtList :: Ct -> [TcTyCoVar]
1857 tyCoVarsOfCtList = fvVarList . tyCoFVsOfCt
1858
1859 -- | Returns free variables of constraints as a composable FV computation.
1860 -- See Note [Deterministic FV] in FV.
1861 tyCoFVsOfCt :: Ct -> FV
1862 tyCoFVsOfCt (CTyEqCan { cc_tyvar = tv, cc_rhs = xi })
1863 = tyCoFVsOfType xi `unionFV` FV.unitFV tv
1864 `unionFV` tyCoFVsOfType (tyVarKind tv)
1865 tyCoFVsOfCt (CFunEqCan { cc_tyargs = tys, cc_fsk = fsk })
1866 = tyCoFVsOfTypes tys `unionFV` FV.unitFV fsk
1867 `unionFV` tyCoFVsOfType (tyVarKind fsk)
1868 tyCoFVsOfCt (CDictCan { cc_tyargs = tys }) = tyCoFVsOfTypes tys
1869 tyCoFVsOfCt (CIrredCan { cc_ev = ev }) = tyCoFVsOfType (ctEvPred ev)
1870 tyCoFVsOfCt (CHoleCan { cc_ev = ev }) = tyCoFVsOfType (ctEvPred ev)
1871 tyCoFVsOfCt (CNonCanonical { cc_ev = ev }) = tyCoFVsOfType (ctEvPred ev)
1872
1873 -- | Returns free variables of a bag of constraints as a non-deterministic
1874 -- set. See Note [Deterministic FV] in FV.
1875 tyCoVarsOfCts :: Cts -> TcTyCoVarSet
1876 tyCoVarsOfCts = fvVarSet . tyCoFVsOfCts
1877
1878 -- | Returns free variables of a bag of constraints as a deterministically
1879 -- odered list. See Note [Deterministic FV] in FV.
1880 tyCoVarsOfCtsList :: Cts -> [TcTyCoVar]
1881 tyCoVarsOfCtsList = fvVarList . tyCoFVsOfCts
1882
1883 -- | Returns free variables of a bag of constraints as a composable FV
1884 -- computation. See Note [Deterministic FV] in FV.
1885 tyCoFVsOfCts :: Cts -> FV
1886 tyCoFVsOfCts = foldrBag (unionFV . tyCoFVsOfCt) emptyFV
1887
1888 -- | Returns free variables of WantedConstraints as a non-deterministic
1889 -- set. See Note [Deterministic FV] in FV.
1890 tyCoVarsOfWC :: WantedConstraints -> TyCoVarSet
1891 -- Only called on *zonked* things, hence no need to worry about flatten-skolems
1892 tyCoVarsOfWC = fvVarSet . tyCoFVsOfWC
1893
1894 -- | Returns free variables of WantedConstraints as a deterministically
1895 -- ordered list. See Note [Deterministic FV] in FV.
1896 tyCoVarsOfWCList :: WantedConstraints -> [TyCoVar]
1897 -- Only called on *zonked* things, hence no need to worry about flatten-skolems
1898 tyCoVarsOfWCList = fvVarList . tyCoFVsOfWC
1899
1900 -- | Returns free variables of WantedConstraints as a composable FV
1901 -- computation. See Note [Deterministic FV] in FV.
1902 tyCoFVsOfWC :: WantedConstraints -> FV
1903 -- Only called on *zonked* things, hence no need to worry about flatten-skolems
1904 tyCoFVsOfWC (WC { wc_simple = simple, wc_impl = implic })
1905 = tyCoFVsOfCts simple `unionFV`
1906 tyCoFVsOfBag tyCoFVsOfImplic implic
1907
1908 -- | Returns free variables of Implication as a composable FV computation.
1909 -- See Note [Deterministic FV] in FV.
1910 tyCoFVsOfImplic :: Implication -> FV
1911 -- Only called on *zonked* things, hence no need to worry about flatten-skolems
1912 tyCoFVsOfImplic (Implic { ic_skols = skols
1913 , ic_given = givens
1914 , ic_wanted = wanted })
1915 = FV.delFVs (mkVarSet skols `unionVarSet` mkVarSet givens)
1916 (tyCoFVsOfWC wanted `unionFV` tyCoFVsOfTypes (map evVarPred givens))
1917
1918 tyCoFVsOfBag :: (a -> FV) -> Bag a -> FV
1919 tyCoFVsOfBag tvs_of = foldrBag (unionFV . tvs_of) emptyFV
1920
1921 ---------------------------
1922 dropDerivedWC :: WantedConstraints -> WantedConstraints
1923 -- See Note [Dropping derived constraints]
1924 dropDerivedWC wc@(WC { wc_simple = simples })
1925 = wc { wc_simple = dropDerivedSimples simples }
1926 -- The wc_impl implications are already (recursively) filtered
1927
1928 --------------------------
1929 dropDerivedSimples :: Cts -> Cts
1930 -- Drop all Derived constraints, but make [W] back into [WD],
1931 -- so that if we re-simplify these constraints we will get all
1932 -- the right derived constraints re-generated. Forgetting this
1933 -- step led to #12936
1934 dropDerivedSimples simples = mapMaybeBag dropDerivedCt simples
1935
1936 dropDerivedCt :: Ct -> Maybe Ct
1937 dropDerivedCt ct
1938 = case ctEvFlavour ev of
1939 Wanted WOnly -> Just (ct' { cc_ev = ev_wd })
1940 Wanted _ -> Just ct'
1941 _ | isDroppableCt ct -> Nothing
1942 | otherwise -> Just ct
1943 where
1944 ev = ctEvidence ct
1945 ev_wd = ev { ctev_nosh = WDeriv }
1946 ct' = setPendingScDict ct -- See Note [Resetting cc_pend_sc]
1947
1948 {- Note [Resetting cc_pend_sc]
1949 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1950 When we discard Derived constraints, in dropDerivedSimples, we must
1951 set the cc_pend_sc flag to True, so that if we re-process this
1952 CDictCan we will re-generate its derived superclasses. Otherwise
1953 we might miss some fundeps. Trac #13662 showed this up.
1954
1955 See Note [The superclass story] in TcCanonical.
1956 -}
1957
1958 isDroppableCt :: Ct -> Bool
1959 isDroppableCt ct
1960 = isDerived ev && not keep_deriv
1961 -- Drop only derived constraints, and then only if they
1962 -- obey Note [Dropping derived constraints]
1963 where
1964 ev = ctEvidence ct
1965 loc = ctEvLoc ev
1966 orig = ctLocOrigin loc
1967
1968 keep_deriv
1969 = case ct of
1970 CHoleCan {} -> True
1971 CIrredCan { cc_insol = insoluble }
1972 -> keep_eq insoluble
1973 _ -> keep_eq False
1974
1975 keep_eq definitely_insoluble
1976 | isGivenOrigin orig -- Arising only from givens
1977 = definitely_insoluble -- Keep only definitely insoluble
1978 | otherwise
1979 = case orig of
1980 KindEqOrigin {} -> True -- See Note [Dropping derived constraints]
1981
1982 -- See Note [Dropping derived constraints]
1983 -- For fundeps, drop wanted/wanted interactions
1984 FunDepOrigin2 {} -> True -- Top-level/Wanted
1985 FunDepOrigin1 _ loc1 _ loc2
1986 | g1 || g2 -> True -- Given/Wanted errors: keep all
1987 | otherwise -> False -- Wanted/Wanted errors: discard
1988 where
1989 g1 = isGivenLoc loc1
1990 g2 = isGivenLoc loc2
1991
1992 _ -> False
1993
1994 arisesFromGivens :: Ct -> Bool
1995 arisesFromGivens ct
1996 = case ctEvidence ct of
1997 CtGiven {} -> True
1998 CtWanted {} -> False
1999 CtDerived { ctev_loc = loc } -> isGivenLoc loc
2000
2001 isGivenLoc :: CtLoc -> Bool
2002 isGivenLoc loc = isGivenOrigin (ctLocOrigin loc)
2003
2004 isGivenOrigin :: CtOrigin -> Bool
2005 isGivenOrigin (GivenOrigin {}) = True
2006 isGivenOrigin (FunDepOrigin1 _ l1 _ l2) = isGivenLoc l1 && isGivenLoc l2
2007 isGivenOrigin (FunDepOrigin2 _ o1 _ _) = isGivenOrigin o1
2008 isGivenOrigin _ = False
2009
2010 {- Note [Dropping derived constraints]
2011 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2012 In general we discard derived constraints at the end of constraint solving;
2013 see dropDerivedWC. For example
2014
2015 * Superclasses: if we have an unsolved [W] (Ord a), we don't want to
2016 complain about an unsolved [D] (Eq a) as well.
2017
2018 * If we have [W] a ~ Int, [W] a ~ Bool, improvement will generate
2019 [D] Int ~ Bool, and we don't want to report that because it's
2020 incomprehensible. That is why we don't rewrite wanteds with wanteds!
2021
2022 But (tiresomely) we do keep *some* Derived constraints:
2023
2024 * Type holes are derived constraints, because they have no evidence
2025 and we want to keep them, so we get the error report
2026
2027 * Insoluble kind equalities (e.g. [D] * ~ (* -> *)), with
2028 KindEqOrigin, may arise from a type equality a ~ Int#, say. See
2029 Note [Equalities with incompatible kinds] in TcCanonical.
2030 These need to be kept because the kind equalities might have different
2031 source locations and hence different error messages.
2032 E.g., test case dependent/should_fail/T11471
2033
2034 * We keep most derived equalities arising from functional dependencies
2035 - Given/Given interactions (subset of FunDepOrigin1):
2036 The definitely-insoluble ones reflect unreachable code.
2037
2038 Others not-definitely-insoluble ones like [D] a ~ Int do not
2039 reflect unreachable code; indeed if fundeps generated proofs, it'd
2040 be a useful equality. See Trac #14763. So we discard them.
2041
2042 - Given/Wanted interacGiven or Wanted interacting with an
2043 instance declaration (FunDepOrigin2)
2044
2045 - Given/Wanted interactions (FunDepOrigin1); see Trac #9612
2046
2047 - But for Wanted/Wanted interactions we do /not/ want to report an
2048 error (Trac #13506). Consider [W] C Int Int, [W] C Int Bool, with
2049 a fundep on class C. We don't want to report an insoluble Int~Bool;
2050 c.f. "wanteds do not rewrite wanteds".
2051
2052 To distinguish these cases we use the CtOrigin.
2053
2054 NB: we keep *all* derived insolubles under some circumstances:
2055
2056 * They are looked at by simplifyInfer, to decide whether to
2057 generalise. Example: [W] a ~ Int, [W] a ~ Bool
2058 We get [D] Int ~ Bool, and indeed the constraints are insoluble,
2059 and we want simplifyInfer to see that, even though we don't
2060 ultimately want to generate an (inexplicable) error message from it
2061
2062
2063 ************************************************************************
2064 * *
2065 CtEvidence
2066 The "flavor" of a canonical constraint
2067 * *
2068 ************************************************************************
2069 -}
2070
2071 isWantedCt :: Ct -> Bool
2072 isWantedCt = isWanted . cc_ev
2073
2074 isGivenCt :: Ct -> Bool
2075 isGivenCt = isGiven . cc_ev
2076
2077 isDerivedCt :: Ct -> Bool
2078 isDerivedCt = isDerived . cc_ev
2079
2080 isCTyEqCan :: Ct -> Bool
2081 isCTyEqCan (CTyEqCan {}) = True
2082 isCTyEqCan (CFunEqCan {}) = False
2083 isCTyEqCan _ = False
2084
2085 isCDictCan_Maybe :: Ct -> Maybe Class
2086 isCDictCan_Maybe (CDictCan {cc_class = cls }) = Just cls
2087 isCDictCan_Maybe _ = Nothing
2088
2089 isCFunEqCan_maybe :: Ct -> Maybe (TyCon, [Type])
2090 isCFunEqCan_maybe (CFunEqCan { cc_fun = tc, cc_tyargs = xis }) = Just (tc, xis)
2091 isCFunEqCan_maybe _ = Nothing
2092
2093 isCFunEqCan :: Ct -> Bool
2094 isCFunEqCan (CFunEqCan {}) = True
2095 isCFunEqCan _ = False
2096
2097 isCNonCanonical :: Ct -> Bool
2098 isCNonCanonical (CNonCanonical {}) = True
2099 isCNonCanonical _ = False
2100
2101 isHoleCt:: Ct -> Bool
2102 isHoleCt (CHoleCan {}) = True
2103 isHoleCt _ = False
2104
2105 isOutOfScopeCt :: Ct -> Bool
2106 -- We treat expression holes representing out-of-scope variables a bit
2107 -- differently when it comes to error reporting
2108 isOutOfScopeCt (CHoleCan { cc_hole = ExprHole (OutOfScope {}) }) = True
2109 isOutOfScopeCt _ = False
2110
2111 isExprHoleCt :: Ct -> Bool
2112 isExprHoleCt (CHoleCan { cc_hole = ExprHole {} }) = True
2113 isExprHoleCt _ = False
2114
2115 isTypeHoleCt :: Ct -> Bool
2116 isTypeHoleCt (CHoleCan { cc_hole = TypeHole {} }) = True
2117 isTypeHoleCt _ = False
2118
2119
2120 {- Note [Custom type errors in constraints]
2121 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2122
2123 When GHC reports a type-error about an unsolved-constraint, we check
2124 to see if the constraint contains any custom-type errors, and if so
2125 we report them. Here are some examples of constraints containing type
2126 errors:
2127
2128 TypeError msg -- The actual constraint is a type error
2129
2130 TypError msg ~ Int -- Some type was supposed to be Int, but ended up
2131 -- being a type error instead
2132
2133 Eq (TypeError msg) -- A class constraint is stuck due to a type error
2134
2135 F (TypeError msg) ~ a -- A type function failed to evaluate due to a type err
2136
2137 It is also possible to have constraints where the type error is nested deeper,
2138 for example see #11990, and also:
2139
2140 Eq (F (TypeError msg)) -- Here the type error is nested under a type-function
2141 -- call, which failed to evaluate because of it,
2142 -- and so the `Eq` constraint was unsolved.
2143 -- This may happen when one function calls another
2144 -- and the called function produced a custom type error.
2145 -}
2146
2147 -- | A constraint is considered to be a custom type error, if it contains
2148 -- custom type errors anywhere in it.
2149 -- See Note [Custom type errors in constraints]
2150 getUserTypeErrorMsg :: Ct -> Maybe Type
2151 getUserTypeErrorMsg ct = findUserTypeError (ctPred ct)
2152 where
2153 findUserTypeError t = msum ( userTypeError_maybe t
2154 : map findUserTypeError (subTys t)
2155 )
2156
2157 subTys t = case splitAppTys t of
2158 (t,[]) ->
2159 case splitTyConApp_maybe t of
2160 Nothing -> []
2161 Just (_,ts) -> ts
2162 (t,ts) -> t : ts
2163
2164
2165
2166
2167 isUserTypeErrorCt :: Ct -> Bool
2168 isUserTypeErrorCt ct = case getUserTypeErrorMsg ct of
2169 Just _ -> True
2170 _ -> False
2171
2172 isPendingScDict :: Ct -> Maybe Ct
2173 -- Says whether cc_pend_sc is True, AND if so flips the flag
2174 isPendingScDict ct@(CDictCan { cc_pend_sc = True })
2175 = Just (ct { cc_pend_sc = False })
2176 isPendingScDict _ = Nothing
2177
2178 setPendingScDict :: Ct -> Ct
2179 -- Set the cc_pend_sc flag to True
2180 setPendingScDict ct@(CDictCan { cc_pend_sc = False })
2181 = ct { cc_pend_sc = True }
2182 setPendingScDict ct = ct
2183
2184 superClassesMightHelp :: Ct -> Bool
2185 -- ^ True if taking superclasses of givens, or of wanteds (to perhaps
2186 -- expose more equalities or functional dependencies) might help to
2187 -- solve this constraint. See Note [When superclasses help]
2188 superClassesMightHelp ct
2189 = isWantedCt ct && not (is_ip ct)
2190 where
2191 is_ip (CDictCan { cc_class = cls }) = isIPClass cls
2192 is_ip _ = False
2193
2194 {- Note [When superclasses help]
2195 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2196 First read Note [The superclass story] in TcCanonical.
2197
2198 We expand superclasses and iterate only if there is at unsolved wanted
2199 for which expansion of superclasses (e.g. from given constraints)
2200 might actually help. The function superClassesMightHelp tells if
2201 doing this superclass expansion might help solve this constraint.
2202 Note that
2203
2204 * Superclasses help only for Wanted constraints. Derived constraints
2205 are not really "unsolved" and we certainly don't want them to
2206 trigger superclass expansion. This was a good part of the loop
2207 in Trac #11523
2208
2209 * Even for Wanted constraints, we say "no" for implicit parameters.
2210 we have [W] ?x::ty, expanding superclasses won't help:
2211 - Superclasses can't be implicit parameters
2212 - If we have a [G] ?x:ty2, then we'll have another unsolved
2213 [D] ty ~ ty2 (from the functional dependency)
2214 which will trigger superclass expansion.
2215
2216 It's a bit of a special case, but it's easy to do. The runtime cost
2217 is low because the unsolved set is usually empty anyway (errors
2218 aside), and the first non-imlicit-parameter will terminate the search.
2219
2220 The special case is worth it (Trac #11480, comment:2) because it
2221 applies to CallStack constraints, which aren't type errors. If we have
2222 f :: (C a) => blah
2223 f x = ...undefined...
2224 we'll get a CallStack constraint. If that's the only unsolved
2225 constraint it'll eventually be solved by defaulting. So we don't
2226 want to emit warnings about hitting the simplifier's iteration
2227 limit. A CallStack constraint really isn't an unsolved
2228 constraint; it can always be solved by defaulting.
2229 -}
2230
2231 singleCt :: Ct -> Cts
2232 singleCt = unitBag
2233
2234 andCts :: Cts -> Cts -> Cts
2235 andCts = unionBags
2236
2237 listToCts :: [Ct] -> Cts
2238 listToCts = listToBag
2239
2240 ctsElts :: Cts -> [Ct]
2241 ctsElts = bagToList
2242
2243 consCts :: Ct -> Cts -> Cts
2244 consCts = consBag
2245
2246 snocCts :: Cts -> Ct -> Cts
2247 snocCts = snocBag
2248
2249 extendCtsList :: Cts -> [Ct] -> Cts
2250 extendCtsList cts xs | null xs = cts
2251 | otherwise = cts `unionBags` listToBag xs
2252
2253 andManyCts :: [Cts] -> Cts
2254 andManyCts = unionManyBags
2255
2256 emptyCts :: Cts
2257 emptyCts = emptyBag
2258
2259 isEmptyCts :: Cts -> Bool
2260 isEmptyCts = isEmptyBag
2261
2262 pprCts :: Cts -> SDoc
2263 pprCts cts = vcat (map ppr (bagToList cts))
2264
2265 {-
2266 ************************************************************************
2267 * *
2268 Wanted constraints
2269 These are forced to be in TcRnTypes because
2270 TcLclEnv mentions WantedConstraints
2271 WantedConstraint mentions CtLoc
2272 CtLoc mentions ErrCtxt
2273 ErrCtxt mentions TcM
2274 * *
2275 v%************************************************************************
2276 -}
2277
2278 data WantedConstraints
2279 = WC { wc_simple :: Cts -- Unsolved constraints, all wanted
2280 , wc_impl :: Bag Implication
2281 }
2282
2283 emptyWC :: WantedConstraints
2284 emptyWC = WC { wc_simple = emptyBag, wc_impl = emptyBag }
2285
2286 mkSimpleWC :: [CtEvidence] -> WantedConstraints
2287 mkSimpleWC cts
2288 = WC { wc_simple = listToBag (map mkNonCanonical cts)
2289 , wc_impl = emptyBag }
2290
2291 mkImplicWC :: Bag Implication -> WantedConstraints
2292 mkImplicWC implic
2293 = WC { wc_simple = emptyBag, wc_impl = implic }
2294
2295 isEmptyWC :: WantedConstraints -> Bool
2296 isEmptyWC (WC { wc_simple = f, wc_impl = i })
2297 = isEmptyBag f && isEmptyBag i
2298
2299
2300 -- | Checks whether a the given wanted constraints are solved, i.e.
2301 -- that there are no simple constraints left and all the implications
2302 -- are solved.
2303 isSolvedWC :: WantedConstraints -> Bool
2304 isSolvedWC WC {wc_simple = wc_simple, wc_impl = wc_impl} =
2305 isEmptyBag wc_simple && allBag (isSolvedStatus . ic_status) wc_impl
2306
2307 andWC :: WantedConstraints -> WantedConstraints -> WantedConstraints
2308 andWC (WC { wc_simple = f1, wc_impl = i1 })
2309 (WC { wc_simple = f2, wc_impl = i2 })
2310 = WC { wc_simple = f1 `unionBags` f2
2311 , wc_impl = i1 `unionBags` i2 }
2312
2313 unionsWC :: [WantedConstraints] -> WantedConstraints
2314 unionsWC = foldr andWC emptyWC
2315
2316 addSimples :: WantedConstraints -> Bag Ct -> WantedConstraints
2317 addSimples wc cts
2318 = wc { wc_simple = wc_simple wc `unionBags` cts }
2319 -- Consider: Put the new constraints at the front, so they get solved first
2320
2321 addImplics :: WantedConstraints -> Bag Implication -> WantedConstraints
2322 addImplics wc implic = wc { wc_impl = wc_impl wc `unionBags` implic }
2323
2324 addInsols :: WantedConstraints -> Bag Ct -> WantedConstraints
2325 addInsols wc cts
2326 = wc { wc_simple = wc_simple wc `unionBags` cts }
2327
2328 insolublesOnly :: WantedConstraints -> WantedConstraints
2329 -- Keep only the definitely-insoluble constraints
2330 insolublesOnly (WC { wc_simple = simples, wc_impl = implics })
2331 = WC { wc_simple = filterBag insolubleWantedCt simples
2332 , wc_impl = mapBag implic_insols_only implics }
2333 where
2334 implic_insols_only implic
2335 = implic { ic_wanted = insolublesOnly (ic_wanted implic) }
2336
2337 isSolvedStatus :: ImplicStatus -> Bool
2338 isSolvedStatus (IC_Solved {}) = True
2339 isSolvedStatus _ = False
2340
2341 isInsolubleStatus :: ImplicStatus -> Bool
2342 isInsolubleStatus IC_Insoluble = True
2343 isInsolubleStatus IC_BadTelescope = True
2344 isInsolubleStatus _ = False
2345
2346 insolubleImplic :: Implication -> Bool
2347 insolubleImplic ic = isInsolubleStatus (ic_status ic)
2348
2349 insolubleWC :: WantedConstraints -> Bool
2350 insolubleWC (WC { wc_impl = implics, wc_simple = simples })
2351 = anyBag insolubleWantedCt simples
2352 || anyBag insolubleImplic implics
2353
2354 insolubleWantedCt :: Ct -> Bool
2355 -- Definitely insoluble, in particular /excluding/ type-hole constraints
2356 insolubleWantedCt ct
2357 | isGivenCt ct = False -- See Note [Given insolubles]
2358 | isHoleCt ct = isOutOfScopeCt ct -- See Note [Insoluble holes]
2359 | insolubleEqCt ct = True
2360 | otherwise = False
2361
2362 insolubleEqCt :: Ct -> Bool
2363 -- Returns True of /equality/ constraints
2364 -- that are /definitely/ insoluble
2365 -- It won't detect some definite errors like
2366 -- F a ~ T (F a)
2367 -- where F is a type family, which actually has an occurs check
2368 --
2369 -- The function is tuned for application /after/ constraint solving
2370 -- i.e. assuming canonicalisation has been done
2371 -- E.g. It'll reply True for a ~ [a]
2372 -- but False for [a] ~ a
2373 -- and
2374 -- True for Int ~ F a Int
2375 -- but False for Maybe Int ~ F a Int Int
2376 -- (where F is an arity-1 type function)
2377 insolubleEqCt (CIrredCan { cc_insol = insol }) = insol
2378 insolubleEqCt _ = False
2379
2380 instance Outputable WantedConstraints where
2381 ppr (WC {wc_simple = s, wc_impl = i})
2382 = text "WC" <+> braces (vcat
2383 [ ppr_bag (text "wc_simple") s
2384 , ppr_bag (text "wc_impl") i ])
2385
2386 ppr_bag :: Outputable a => SDoc -> Bag a -> SDoc
2387 ppr_bag doc bag
2388 | isEmptyBag bag = empty
2389 | otherwise = hang (doc <+> equals)
2390 2 (foldrBag (($$) . ppr) empty bag)
2391
2392 {- Note [Given insolubles]
2393 ~~~~~~~~~~~~~~~~~~~~~~~~~~
2394 Consider (Trac #14325, comment:)
2395 class (a~b) => C a b
2396
2397 foo :: C a c => a -> c
2398 foo x = x
2399
2400 hm3 :: C (f b) b => b -> f b
2401 hm3 x = foo x
2402
2403 In the RHS of hm3, from the [G] C (f b) b we get the insoluble
2404 [G] f b ~# b. Then we also get an unsolved [W] C b (f b).
2405 Residual implication looks like
2406 forall b. C (f b) b => [G] f b ~# b
2407 [W] C f (f b)
2408
2409 We do /not/ want to set the implication status to IC_Insoluble,
2410 because that'll suppress reports of [W] C b (f b). But we
2411 may not report the insoluble [G] f b ~# b either (see Note [Given errors]
2412 in TcErrors), so we may fail to report anything at all! Yikes.
2413
2414 Bottom line: insolubleWC (called in TcSimplify.setImplicationStatus)
2415 should ignore givens even if they are insoluble.
2416
2417 Note [Insoluble holes]
2418 ~~~~~~~~~~~~~~~~~~~~~~
2419 Hole constraints that ARE NOT treated as truly insoluble:
2420 a) type holes, arising from PartialTypeSignatures,
2421 b) "true" expression holes arising from TypedHoles
2422
2423 An "expression hole" or "type hole" constraint isn't really an error
2424 at all; it's a report saying "_ :: Int" here. But an out-of-scope
2425 variable masquerading as expression holes IS treated as truly
2426 insoluble, so that it trumps other errors during error reporting.
2427 Yuk!
2428
2429 ************************************************************************
2430 * *
2431 Implication constraints
2432 * *
2433 ************************************************************************
2434 -}
2435
2436 data Implication
2437 = Implic { -- Invariants for a tree of implications:
2438 -- see TcType Note [TcLevel and untouchable type variables]
2439
2440 ic_tclvl :: TcLevel, -- TcLevel of unification variables
2441 -- allocated /inside/ this implication
2442
2443 ic_skols :: [TcTyVar], -- Introduced skolems
2444 ic_info :: SkolemInfo, -- See Note [Skolems in an implication]
2445 -- See Note [Shadowing in a constraint]
2446 ic_telescope :: Maybe SDoc, -- User-written telescope, if there is one
2447 -- The list of skolems is order-checked
2448 -- if and only if this is a Just.
2449 -- See Note [Keeping scoped variables in order: Explicit]
2450 -- in TcHsType
2451
2452 ic_given :: [EvVar], -- Given evidence variables
2453 -- (order does not matter)
2454 -- See Invariant (GivenInv) in TcType
2455
2456 ic_no_eqs :: Bool, -- True <=> ic_givens have no equalities, for sure
2457 -- False <=> ic_givens might have equalities
2458
2459 ic_env :: TcLclEnv, -- Gives the source location and error context
2460 -- for the implication, and hence for all the
2461 -- given evidence variables
2462
2463 ic_wanted :: WantedConstraints, -- The wanteds
2464 -- See Invariang (WantedInf) in TcType
2465
2466 ic_binds :: EvBindsVar, -- Points to the place to fill in the
2467 -- abstraction and bindings.
2468
2469 -- The ic_need fields keep track of which Given evidence
2470 -- is used by this implication or its children
2471 -- NB: including stuff used by nested implications that have since
2472 -- been discarded
2473 ic_need_inner :: VarSet, -- Includes all used Given evidence
2474 ic_need_outer :: VarSet, -- Includes only the free Given evidence
2475 -- i.e. ic_need_inner after deleting
2476 -- (a) givens (b) binders of ic_binds
2477
2478 ic_status :: ImplicStatus
2479 }
2480
2481 newImplication :: Implication
2482 newImplication
2483 = Implic { -- These fields must be initialisad
2484 ic_tclvl = panic "newImplic:tclvl"
2485 , ic_binds = panic "newImplic:binds"
2486 , ic_info = panic "newImplic:info"
2487 , ic_env = panic "newImplic:env"
2488
2489 -- The rest have sensible default values
2490 , ic_skols = []
2491 , ic_telescope = Nothing
2492 , ic_given = []
2493 , ic_wanted = emptyWC
2494 , ic_no_eqs = False
2495 , ic_status = IC_Unsolved
2496 , ic_need_inner = emptyVarSet
2497 , ic_need_outer = emptyVarSet }
2498
2499 data ImplicStatus
2500 = IC_Solved -- All wanteds in the tree are solved, all the way down
2501 { ics_dead :: [EvVar] } -- Subset of ic_given that are not needed
2502 -- See Note [Tracking redundant constraints] in TcSimplify
2503
2504 | IC_Insoluble -- At least one insoluble constraint in the tree
2505
2506 | IC_BadTelescope -- solved, but the skolems in the telescope are out of
2507 -- dependency order
2508
2509 | IC_Unsolved -- Neither of the above; might go either way
2510
2511 instance Outputable Implication where
2512 ppr (Implic { ic_tclvl = tclvl, ic_skols = skols
2513 , ic_given = given, ic_no_eqs = no_eqs
2514 , ic_wanted = wanted, ic_status = status
2515 , ic_binds = binds
2516 -- , ic_need_inner = need_in, ic_need_outer = need_out
2517 , ic_info = info })
2518 = hang (text "Implic" <+> lbrace)
2519 2 (sep [ text "TcLevel =" <+> ppr tclvl
2520 , text "Skolems =" <+> pprTyVars skols
2521 , text "No-eqs =" <+> ppr no_eqs
2522 , text "Status =" <+> ppr status
2523 , hang (text "Given =") 2 (pprEvVars given)
2524 , hang (text "Wanted =") 2 (ppr wanted)
2525 , text "Binds =" <+> ppr binds
2526 -- , text "Needed inner =" <+> ppr need_in
2527 -- , text "Needed outer =" <+> ppr need_out
2528 , pprSkolInfo info ] <+> rbrace)
2529
2530 instance Outputable ImplicStatus where
2531 ppr IC_Insoluble = text "Insoluble"
2532 ppr IC_BadTelescope = text "Bad telescope"
2533 ppr IC_Unsolved = text "Unsolved"
2534 ppr (IC_Solved { ics_dead = dead })
2535 = text "Solved" <+> (braces (text "Dead givens =" <+> ppr dead))
2536
2537 {-
2538 Note [Needed evidence variables]
2539 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2540 Th ic_need_evs field holds the free vars of ic_binds, and all the
2541 ic_binds in nested implications.
2542
2543 * Main purpose: if one of the ic_givens is not mentioned in here, it
2544 is redundant.
2545
2546 * solveImplication may drop an implication altogether if it has no
2547 remaining 'wanteds'. But we still track the free vars of its
2548 evidence binds, even though it has now disappeared.
2549
2550 Note [Shadowing in a constraint]
2551 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2552 We assume NO SHADOWING in a constraint. Specifically
2553 * The unification variables are all implicitly quantified at top
2554 level, and are all unique
2555 * The skolem variables bound in ic_skols are all freah when the
2556 implication is created.
2557 So we can safely substitute. For example, if we have
2558 forall a. a~Int => ...(forall b. ...a...)...
2559 we can push the (a~Int) constraint inwards in the "givens" without
2560 worrying that 'b' might clash.
2561
2562 Note [Skolems in an implication]
2563 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2564 The skolems in an implication are not there to perform a skolem escape
2565 check. That happens because all the environment variables are in the
2566 untouchables, and therefore cannot be unified with anything at all,
2567 let alone the skolems.
2568
2569 Instead, ic_skols is used only when considering floating a constraint
2570 outside the implication in TcSimplify.floatEqualities or
2571 TcSimplify.approximateImplications
2572
2573 Note [Insoluble constraints]
2574 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2575 Some of the errors that we get during canonicalization are best
2576 reported when all constraints have been simplified as much as
2577 possible. For instance, assume that during simplification the
2578 following constraints arise:
2579
2580 [Wanted] F alpha ~ uf1
2581 [Wanted] beta ~ uf1 beta
2582
2583 When canonicalizing the wanted (beta ~ uf1 beta), if we eagerly fail
2584 we will simply see a message:
2585 'Can't construct the infinite type beta ~ uf1 beta'
2586 and the user has no idea what the uf1 variable is.
2587
2588 Instead our plan is that we will NOT fail immediately, but:
2589 (1) Record the "frozen" error in the ic_insols field
2590 (2) Isolate the offending constraint from the rest of the inerts
2591 (3) Keep on simplifying/canonicalizing
2592
2593 At the end, we will hopefully have substituted uf1 := F alpha, and we
2594 will be able to report a more informative error:
2595 'Can't construct the infinite type beta ~ F alpha beta'
2596
2597 Insoluble constraints *do* include Derived constraints. For example,
2598 a functional dependency might give rise to [D] Int ~ Bool, and we must
2599 report that. If insolubles did not contain Deriveds, reportErrors would
2600 never see it.
2601
2602
2603 ************************************************************************
2604 * *
2605 Pretty printing
2606 * *
2607 ************************************************************************
2608 -}
2609
2610 pprEvVars :: [EvVar] -> SDoc -- Print with their types
2611 pprEvVars ev_vars = vcat (map pprEvVarWithType ev_vars)
2612
2613 pprEvVarTheta :: [EvVar] -> SDoc
2614 pprEvVarTheta ev_vars = pprTheta (map evVarPred ev_vars)
2615
2616 pprEvVarWithType :: EvVar -> SDoc
2617 pprEvVarWithType v = ppr v <+> dcolon <+> pprType (evVarPred v)
2618
2619
2620
2621 -- | Wraps the given type with the constraints (via ic_given) in the given
2622 -- implication, according to the variables mentioned (via ic_skols)
2623 -- in the implication, but taking care to only wrap those variables
2624 -- that are mentioned in the type or the implication.
2625 wrapTypeWithImplication :: Type -> Implication -> Type
2626 wrapTypeWithImplication ty impl = wrapType ty mentioned_skols givens
2627 where givens = map idType $ ic_given impl
2628 skols = ic_skols impl
2629 freeVars = fvVarSet $ tyCoFVsOfTypes (ty:givens)
2630 mentioned_skols = filter (`elemVarSet` freeVars) skols
2631
2632 wrapType :: Type -> [TyVar] -> [PredType] -> Type
2633 wrapType ty skols givens = mkSpecForAllTys skols $ mkFunTys givens ty
2634
2635
2636 {-
2637 ************************************************************************
2638 * *
2639 CtEvidence
2640 * *
2641 ************************************************************************
2642
2643 Note [Evidence field of CtEvidence]
2644 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2645 During constraint solving we never look at the type of ctev_evar/ctev_dest;
2646 instead we look at the ctev_pred field. The evtm/evar field
2647 may be un-zonked.
2648
2649 Note [Bind new Givens immediately]
2650 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2651 For Givens we make new EvVars and bind them immediately. Two main reasons:
2652 * Gain sharing. E.g. suppose we start with g :: C a b, where
2653 class D a => C a b
2654 class (E a, F a) => D a
2655 If we generate all g's superclasses as separate EvTerms we might
2656 get selD1 (selC1 g) :: E a
2657 selD2 (selC1 g) :: F a
2658 selC1 g :: D a
2659 which we could do more economically as:
2660 g1 :: D a = selC1 g
2661 g2 :: E a = selD1 g1
2662 g3 :: F a = selD2 g1
2663
2664 * For *coercion* evidence we *must* bind each given:
2665 class (a~b) => C a b where ....
2666 f :: C a b => ....
2667 Then in f's Givens we have g:(C a b) and the superclass sc(g,0):a~b.
2668 But that superclass selector can't (yet) appear in a coercion
2669 (see evTermCoercion), so the easy thing is to bind it to an Id.
2670
2671 So a Given has EvVar inside it rather than (as previously) an EvTerm.
2672
2673 -}
2674
2675 -- | A place for type-checking evidence to go after it is generated.
2676 -- Wanted equalities are always HoleDest; other wanteds are always
2677 -- EvVarDest.
2678 data TcEvDest
2679 = EvVarDest EvVar -- ^ bind this var to the evidence
2680 -- EvVarDest is always used for non-type-equalities
2681 -- e.g. class constraints
2682
2683 | HoleDest CoercionHole -- ^ fill in this hole with the evidence
2684 -- HoleDest is always used for type-equalities
2685 -- See Note [Coercion holes] in TyCoRep
2686
2687 data CtEvidence
2688 = CtGiven -- Truly given, not depending on subgoals
2689 { ctev_pred :: TcPredType -- See Note [Ct/evidence invariant]
2690 , ctev_evar :: EvVar -- See Note [Evidence field of CtEvidence]
2691 , ctev_loc :: CtLoc }
2692
2693
2694 | CtWanted -- Wanted goal
2695 { ctev_pred :: TcPredType -- See Note [Ct/evidence invariant]
2696 , ctev_dest :: TcEvDest
2697 , ctev_nosh :: ShadowInfo -- See Note [Constraint flavours]
2698 , ctev_loc :: CtLoc }
2699
2700 | CtDerived -- A goal that we don't really have to solve and can't
2701 -- immediately rewrite anything other than a derived
2702 -- (there's no evidence!) but if we do manage to solve
2703 -- it may help in solving other goals.
2704 { ctev_pred :: TcPredType
2705 , ctev_loc :: CtLoc }
2706
2707 ctEvPred :: CtEvidence -> TcPredType
2708 -- The predicate of a flavor
2709 ctEvPred = ctev_pred
2710
2711 ctEvLoc :: CtEvidence -> CtLoc
2712 ctEvLoc = ctev_loc
2713
2714 ctEvOrigin :: CtEvidence -> CtOrigin
2715 ctEvOrigin = ctLocOrigin . ctEvLoc
2716
2717 -- | Get the equality relation relevant for a 'CtEvidence'
2718 ctEvEqRel :: CtEvidence -> EqRel
2719 ctEvEqRel = predTypeEqRel . ctEvPred
2720
2721 -- | Get the role relevant for a 'CtEvidence'
2722 ctEvRole :: CtEvidence -> Role
2723 ctEvRole = eqRelRole . ctEvEqRel
2724
2725 ctEvExpr :: CtEvidence -> EvExpr
2726 ctEvExpr ev@(CtWanted { ctev_dest = HoleDest _ }) = evCoercion $ ctEvCoercion ev
2727 ctEvExpr ev = evId (ctEvEvId ev)
2728
2729 ctEvCoercion :: CtEvidence -> Coercion
2730 ctEvCoercion (CtGiven { ctev_evar = ev_id })
2731 = mkTcCoVarCo ev_id
2732 ctEvCoercion (CtWanted { ctev_dest = dest })
2733 | HoleDest hole <- dest
2734 = -- ctEvCoercion is only called on type equalities
2735 -- and they always have HoleDests
2736 mkHoleCo hole
2737 ctEvCoercion ev
2738 = pprPanic "ctEvCoercion" (ppr ev)
2739
2740 ctEvEvId :: CtEvidence -> EvVar
2741 ctEvEvId (CtWanted { ctev_dest = EvVarDest ev }) = ev
2742 ctEvEvId (CtWanted { ctev_dest = HoleDest h }) = coHoleCoVar h
2743 ctEvEvId (CtGiven { ctev_evar = ev }) = ev
2744 ctEvEvId ctev@(CtDerived {}) = pprPanic "ctEvId:" (ppr ctev)
2745
2746 instance Outputable TcEvDest where
2747 ppr (HoleDest h) = text "hole" <> ppr h
2748 ppr (EvVarDest ev) = ppr ev
2749
2750 instance Outputable CtEvidence where
2751 ppr ev = ppr (ctEvFlavour ev)
2752 <+> pp_ev
2753 <+> braces (ppr (ctl_depth (ctEvLoc ev))) <> dcolon
2754 -- Show the sub-goal depth too
2755 <+> ppr (ctEvPred ev)
2756 where
2757 pp_ev = case ev of
2758 CtGiven { ctev_evar = v } -> ppr v
2759 CtWanted {ctev_dest = d } -> ppr d
2760 CtDerived {} -> text "_"
2761
2762 isWanted :: CtEvidence -> Bool
2763 isWanted (CtWanted {}) = True
2764 isWanted _ = False
2765
2766 isGiven :: CtEvidence -> Bool
2767 isGiven (CtGiven {}) = True
2768 isGiven _ = False
2769
2770 isDerived :: CtEvidence -> Bool
2771 isDerived (CtDerived {}) = True
2772 isDerived _ = False
2773
2774 {-
2775 %************************************************************************
2776 %* *
2777 CtFlavour
2778 %* *
2779 %************************************************************************
2780
2781 Note [Constraint flavours]
2782 ~~~~~~~~~~~~~~~~~~~~~~~~~~
2783 Constraints come in four flavours:
2784
2785 * [G] Given: we have evidence
2786
2787 * [W] Wanted WOnly: we want evidence
2788
2789 * [D] Derived: any solution must satisfy this constraint, but
2790 we don't need evidence for it. Examples include:
2791 - superclasses of [W] class constraints
2792 - equalities arising from functional dependencies
2793 or injectivity
2794
2795 * [WD] Wanted WDeriv: a single constraint that represents
2796 both [W] and [D]
2797 We keep them paired as one both for efficiency, and because
2798 when we have a finite map F tys -> CFunEqCan, it's inconvenient
2799 to have two CFunEqCans in the range
2800
2801 The ctev_nosh field of a Wanted distinguishes between [W] and [WD]
2802
2803 Wanted constraints are born as [WD], but are split into [W] and its
2804 "shadow" [D] in TcSMonad.maybeEmitShadow.
2805
2806 See Note [The improvement story and derived shadows] in TcSMonad
2807 -}
2808
2809 data CtFlavour -- See Note [Constraint flavours]
2810 = Given
2811 | Wanted ShadowInfo
2812 | Derived
2813 deriving Eq
2814
2815 data ShadowInfo
2816 = WDeriv -- [WD] This Wanted constraint has no Derived shadow,
2817 -- so it behaves like a pair of a Wanted and a Derived
2818 | WOnly -- [W] It has a separate derived shadow
2819 -- See Note [Derived shadows]
2820 deriving( Eq )
2821
2822 isGivenOrWDeriv :: CtFlavour -> Bool
2823 isGivenOrWDeriv Given = True
2824 isGivenOrWDeriv (Wanted WDeriv) = True
2825 isGivenOrWDeriv _ = False
2826
2827 instance Outputable CtFlavour where
2828 ppr Given = text "[G]"
2829 ppr (Wanted WDeriv) = text "[WD]"
2830 ppr (Wanted WOnly) = text "[W]"
2831 ppr Derived = text "[D]"
2832
2833 ctEvFlavour :: CtEvidence -> CtFlavour
2834 ctEvFlavour (CtWanted { ctev_nosh = nosh }) = Wanted nosh
2835 ctEvFlavour (CtGiven {}) = Given
2836 ctEvFlavour (CtDerived {}) = Derived
2837
2838 -- | Whether or not one 'Ct' can rewrite another is determined by its
2839 -- flavour and its equality relation. See also
2840 -- Note [Flavours with roles] in TcSMonad
2841 type CtFlavourRole = (CtFlavour, EqRel)
2842
2843 -- | Extract the flavour, role, and boxity from a 'CtEvidence'
2844 ctEvFlavourRole :: CtEvidence -> CtFlavourRole
2845 ctEvFlavourRole ev = (ctEvFlavour ev, ctEvEqRel ev)
2846
2847 -- | Extract the flavour and role from a 'Ct'
2848 ctFlavourRole :: Ct -> CtFlavourRole
2849 -- Uses short-cuts to role for special cases
2850 ctFlavourRole (CDictCan { cc_ev = ev })
2851 = (ctEvFlavour ev, NomEq)
2852 ctFlavourRole (CTyEqCan { cc_ev = ev, cc_eq_rel = eq_rel })
2853 = (ctEvFlavour ev, eq_rel)
2854 ctFlavourRole (CFunEqCan { cc_ev = ev })
2855 = (ctEvFlavour ev, NomEq)
2856 ctFlavourRole (CHoleCan { cc_ev = ev })
2857 = (ctEvFlavour ev, NomEq)
2858 ctFlavourRole ct
2859 = ctEvFlavourRole (cc_ev ct)
2860
2861 {- Note [eqCanRewrite]
2862 ~~~~~~~~~~~~~~~~~~~~~~
2863 (eqCanRewrite ct1 ct2) holds if the constraint ct1 (a CTyEqCan of form
2864 tv ~ ty) can be used to rewrite ct2. It must satisfy the properties of
2865 a can-rewrite relation, see Definition [Can-rewrite relation] in
2866 TcSMonad.
2867
2868 With the solver handling Coercible constraints like equality constraints,
2869 the rewrite conditions must take role into account, never allowing
2870 a representational equality to rewrite a nominal one.
2871
2872 Note [Wanteds do not rewrite Wanteds]
2873 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2874 We don't allow Wanteds to rewrite Wanteds, because that can give rise
2875 to very confusing type error messages. A good example is Trac #8450.
2876 Here's another
2877 f :: a -> Bool
2878 f x = ( [x,'c'], [x,True] ) `seq` True
2879 Here we get
2880 [W] a ~ Char
2881 [W] a ~ Bool
2882 but we do not want to complain about Bool ~ Char!
2883
2884 Note [Deriveds do rewrite Deriveds]
2885 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2886 However we DO allow Deriveds to rewrite Deriveds, because that's how
2887 improvement works; see Note [The improvement story] in TcInteract.
2888
2889 However, for now at least I'm only letting (Derived,NomEq) rewrite
2890 (Derived,NomEq) and not doing anything for ReprEq. If we have
2891 eqCanRewriteFR (Derived, NomEq) (Derived, _) = True
2892 then we lose property R2 of Definition [Can-rewrite relation]
2893 in TcSMonad
2894 R2. If f1 >= f, and f2 >= f,
2895 then either f1 >= f2 or f2 >= f1
2896 Consider f1 = (Given, ReprEq)
2897 f2 = (Derived, NomEq)
2898 f = (Derived, ReprEq)
2899
2900 I thought maybe we could never get Derived ReprEq constraints, but
2901 we can; straight from the Wanteds during improvement. And from a Derived
2902 ReprEq we could conceivably get a Derived NomEq improvement (by decomposing
2903 a type constructor with Nomninal role), and hence unify.
2904 -}
2905
2906 eqCanRewrite :: EqRel -> EqRel -> Bool
2907 eqCanRewrite NomEq _ = True
2908 eqCanRewrite ReprEq ReprEq = True
2909 eqCanRewrite ReprEq NomEq = False
2910
2911 eqCanRewriteFR :: CtFlavourRole -> CtFlavourRole -> Bool
2912 -- Can fr1 actually rewrite fr2?
2913 -- Very important function!
2914 -- See Note [eqCanRewrite]
2915 -- See Note [Wanteds do not rewrite Wanteds]
2916 -- See Note [Deriveds do rewrite Deriveds]
2917 eqCanRewriteFR (Given, r1) (_, r2) = eqCanRewrite r1 r2
2918 eqCanRewriteFR (Wanted WDeriv, NomEq) (Derived, NomEq) = True
2919 eqCanRewriteFR (Derived, NomEq) (Derived, NomEq) = True
2920 eqCanRewriteFR _ _ = False
2921
2922 eqMayRewriteFR :: CtFlavourRole -> CtFlavourRole -> Bool
2923 -- Is it /possible/ that fr1 can rewrite fr2?
2924 -- This is used when deciding which inerts to kick out,
2925 -- at which time a [WD] inert may be split into [W] and [D]
2926 eqMayRewriteFR (Wanted WDeriv, NomEq) (Wanted WDeriv, NomEq) = True
2927 eqMayRewriteFR (Derived, NomEq) (Wanted WDeriv, NomEq) = True
2928 eqMayRewriteFR fr1 fr2 = eqCanRewriteFR fr1 fr2
2929
2930 -----------------
2931 {- Note [funEqCanDischarge]
2932 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
2933 Suppose we have two CFunEqCans with the same LHS:
2934 (x1:F ts ~ f1) `funEqCanDischarge` (x2:F ts ~ f2)
2935 Can we drop x2 in favour of x1, either unifying
2936 f2 (if it's a flatten meta-var) or adding a new Given
2937 (f1 ~ f2), if x2 is a Given?
2938
2939 Answer: yes if funEqCanDischarge is true.
2940 -}
2941
2942 funEqCanDischarge
2943 :: CtEvidence -> CtEvidence
2944 -> ( SwapFlag -- NotSwapped => lhs can discharge rhs
2945 -- Swapped => rhs can discharge lhs
2946 , Bool) -- True <=> upgrade non-discharded one
2947 -- from [W] to [WD]
2948 -- See Note [funEqCanDischarge]
2949 funEqCanDischarge ev1 ev2
2950 = ASSERT2( ctEvEqRel ev1 == NomEq, ppr ev1 )
2951 ASSERT2( ctEvEqRel ev2 == NomEq, ppr ev2 )
2952 -- CFunEqCans are all Nominal, hence asserts
2953 funEqCanDischargeF (ctEvFlavour ev1) (ctEvFlavour ev2)
2954
2955 funEqCanDischargeF :: CtFlavour -> CtFlavour -> (SwapFlag, Bool)
2956 funEqCanDischargeF Given _ = (NotSwapped, False)
2957 funEqCanDischargeF _ Given = (IsSwapped, False)
2958 funEqCanDischargeF (Wanted WDeriv) _ = (NotSwapped, False)
2959 funEqCanDischargeF _ (Wanted WDeriv) = (IsSwapped, True)
2960 funEqCanDischargeF (Wanted WOnly) (Wanted WOnly) = (NotSwapped, False)
2961 funEqCanDischargeF (Wanted WOnly) Derived = (NotSwapped, True)
2962 funEqCanDischargeF Derived (Wanted WOnly) = (IsSwapped, True)
2963 funEqCanDischargeF Derived Derived = (NotSwapped, False)
2964
2965
2966 {- Note [eqCanDischarge]
2967 ~~~~~~~~~~~~~~~~~~~~~~~~
2968 Suppose we have two identical CTyEqCan equality constraints
2969 (i.e. both LHS and RHS are the same)
2970 (x1:a~t) `eqCanDischarge` (xs:a~t)
2971 Can we just drop x2 in favour of x1?
2972
2973 Answer: yes if eqCanDischarge is true.
2974
2975 Note that we do /not/ allow Wanted to discharge Derived.
2976 We must keep both. Why? Because the Derived may rewrite
2977 other Deriveds in the model whereas the Wanted cannot.
2978
2979 However a Wanted can certainly discharge an identical Wanted. So
2980 eqCanDischarge does /not/ define a can-rewrite relation in the
2981 sense of Definition [Can-rewrite relation] in TcSMonad.
2982
2983 We /do/ say that a [W] can discharge a [WD]. In evidence terms it
2984 certainly can, and the /caller/ arranges that the otherwise-lost [D]
2985 is spat out as a new Derived. -}
2986
2987 eqCanDischargeFR :: CtFlavourRole -> CtFlavourRole -> Bool
2988 -- See Note [eqCanDischarge]
2989 eqCanDischargeFR (f1,r1) (f2, r2) = eqCanRewrite r1 r2
2990 && eqCanDischargeF f1 f2
2991
2992 eqCanDischargeF :: CtFlavour -> CtFlavour -> Bool
2993 eqCanDischargeF Given _ = True
2994 eqCanDischargeF (Wanted _) (Wanted _) = True
2995 eqCanDischargeF (Wanted WDeriv) Derived = True
2996 eqCanDischargeF Derived Derived = True
2997 eqCanDischargeF _ _ = False
2998
2999
3000 {-
3001 ************************************************************************
3002 * *
3003 SubGoalDepth
3004 * *
3005 ************************************************************************
3006
3007 Note [SubGoalDepth]
3008 ~~~~~~~~~~~~~~~~~~~
3009 The 'SubGoalDepth' takes care of stopping the constraint solver from looping.
3010
3011 The counter starts at zero and increases. It includes dictionary constraints,
3012 equality simplification, and type family reduction. (Why combine these? Because
3013 it's actually quite easy to mistake one for another, in sufficiently involved
3014 scenarios, like ConstraintKinds.)
3015
3016 The flag -fcontext-stack=n (not very well named!) fixes the maximium
3017 level.
3018
3019 * The counter includes the depth of type class instance declarations. Example:
3020 [W] d{7} : Eq [Int]
3021 That is d's dictionary-constraint depth is 7. If we use the instance
3022 $dfEqList :: Eq a => Eq [a]
3023 to simplify it, we get
3024 d{7} = $dfEqList d'{8}
3025 where d'{8} : Eq Int, and d' has depth 8.
3026
3027 For civilised (decidable) instance declarations, each increase of
3028 depth removes a type constructor from the type, so the depth never
3029 gets big; i.e. is bounded by the structural depth of the type.
3030
3031 * The counter also increments when resolving
3032 equalities involving type functions. Example:
3033 Assume we have a wanted at depth 7:
3034 [W] d{7} : F () ~ a
3035 If there is a type function equation "F () = Int", this would be rewritten to
3036 [W] d{8} : Int ~ a
3037 and remembered as having depth 8.
3038
3039 Again, without UndecidableInstances, this counter is bounded, but without it
3040 can resolve things ad infinitum. Hence there is a maximum level.
3041
3042 * Lastly, every time an equality is rewritten, the counter increases. Again,
3043 rewriting an equality constraint normally makes progress, but it's possible
3044 the "progress" is just the reduction of an infinitely-reducing type family.
3045 Hence we need to track the rewrites.
3046
3047 When compiling a program requires a greater depth, then GHC recommends turning
3048 off this check entirely by setting -freduction-depth=0. This is because the
3049 exact number that works is highly variable, and is likely to change even between
3050 minor releases. Because this check is solely to prevent infinite compilation
3051 times, it seems safe to disable it when a user has ascertained that their program
3052 doesn't loop at the type level.
3053
3054 -}
3055
3056 -- | See Note [SubGoalDepth]
3057 newtype SubGoalDepth = SubGoalDepth Int
3058 deriving (Eq, Ord, Outputable)
3059
3060 initialSubGoalDepth :: SubGoalDepth
3061 initialSubGoalDepth = SubGoalDepth 0
3062
3063 bumpSubGoalDepth :: SubGoalDepth -> SubGoalDepth
3064 bumpSubGoalDepth (SubGoalDepth n) = SubGoalDepth (n + 1)
3065
3066 maxSubGoalDepth :: SubGoalDepth -> SubGoalDepth -> SubGoalDepth
3067 maxSubGoalDepth (SubGoalDepth n) (SubGoalDepth m) = SubGoalDepth (n `max` m)
3068
3069 subGoalDepthExceeded :: DynFlags -> SubGoalDepth -> Bool
3070 subGoalDepthExceeded dflags (SubGoalDepth d)
3071 = mkIntWithInf d > reductionDepth dflags
3072
3073 {-
3074 ************************************************************************
3075 * *
3076 CtLoc
3077 * *
3078 ************************************************************************
3079
3080 The 'CtLoc' gives information about where a constraint came from.
3081 This is important for decent error message reporting because
3082 dictionaries don't appear in the original source code.
3083 type will evolve...
3084
3085 -}
3086
3087 data CtLoc = CtLoc { ctl_origin :: CtOrigin
3088 , ctl_env :: TcLclEnv
3089 , ctl_t_or_k :: Maybe TypeOrKind -- OK if we're not sure
3090 , ctl_depth :: !SubGoalDepth }
3091
3092 -- The TcLclEnv includes particularly
3093 -- source location: tcl_loc :: RealSrcSpan
3094 -- context: tcl_ctxt :: [ErrCtxt]
3095 -- binder stack: tcl_bndrs :: TcBinderStack
3096 -- level: tcl_tclvl :: TcLevel
3097
3098 mkKindLoc :: TcType -> TcType -- original *types* being compared
3099 -> CtLoc -> CtLoc
3100 mkKindLoc s1 s2 loc = setCtLocOrigin (toKindLoc loc)
3101 (KindEqOrigin s1 (Just s2) (ctLocOrigin loc)
3102 (ctLocTypeOrKind_maybe loc))
3103
3104 -- | Take a CtLoc and moves it to the kind level
3105 toKindLoc :: CtLoc -> CtLoc
3106 toKindLoc loc = loc { ctl_t_or_k = Just KindLevel }
3107
3108 mkGivenLoc :: TcLevel -> SkolemInfo -> TcLclEnv -> CtLoc
3109 mkGivenLoc tclvl skol_info env
3110 = CtLoc { ctl_origin = GivenOrigin skol_info
3111 , ctl_env = env { tcl_tclvl = tclvl }
3112 , ctl_t_or_k = Nothing -- this only matters for error msgs
3113 , ctl_depth = initialSubGoalDepth }
3114
3115 ctLocEnv :: CtLoc -> TcLclEnv
3116 ctLocEnv = ctl_env
3117
3118 ctLocLevel :: CtLoc -> TcLevel
3119 ctLocLevel loc = tcl_tclvl (ctLocEnv loc)
3120
3121 ctLocDepth :: CtLoc -> SubGoalDepth
3122 ctLocDepth = ctl_depth
3123
3124 ctLocOrigin :: CtLoc -> CtOrigin
3125 ctLocOrigin = ctl_origin
3126
3127 ctLocSpan :: CtLoc -> RealSrcSpan
3128 ctLocSpan (CtLoc { ctl_env = lcl}) = tcl_loc lcl
3129
3130 ctLocTypeOrKind_maybe :: CtLoc -> Maybe TypeOrKind
3131 ctLocTypeOrKind_maybe = ctl_t_or_k
3132
3133 setCtLocSpan :: CtLoc -> RealSrcSpan -> CtLoc
3134 setCtLocSpan ctl@(CtLoc { ctl_env = lcl }) loc = setCtLocEnv ctl (lcl { tcl_loc = loc })
3135
3136 bumpCtLocDepth :: CtLoc -> CtLoc
3137 bumpCtLocDepth loc@(CtLoc { ctl_depth = d }) = loc { ctl_depth = bumpSubGoalDepth d }
3138
3139 setCtLocOrigin :: CtLoc -> CtOrigin -> CtLoc
3140 setCtLocOrigin ctl orig = ctl { ctl_origin = orig }
3141
3142 updateCtLocOrigin :: CtLoc -> (CtOrigin -> CtOrigin) -> CtLoc
3143 updateCtLocOrigin ctl@(CtLoc { ctl_origin = orig }) upd
3144 = ctl { ctl_origin = upd orig }
3145
3146 setCtLocEnv :: CtLoc -> TcLclEnv -> CtLoc
3147 setCtLocEnv ctl env = ctl { ctl_env = env }
3148
3149 pushErrCtxt :: CtOrigin -> ErrCtxt -> CtLoc -> CtLoc
3150 pushErrCtxt o err loc@(CtLoc { ctl_env = lcl })
3151 = loc { ctl_origin = o, ctl_env = lcl { tcl_ctxt = err : tcl_ctxt lcl } }
3152
3153 pushErrCtxtSameOrigin :: ErrCtxt -> CtLoc -> CtLoc
3154 -- Just add information w/o updating the origin!
3155 pushErrCtxtSameOrigin err loc@(CtLoc { ctl_env = lcl })
3156 = loc { ctl_env = lcl { tcl_ctxt = err : tcl_ctxt lcl } }
3157
3158 {-
3159 ************************************************************************
3160 * *
3161 SkolemInfo
3162 * *
3163 ************************************************************************
3164 -}
3165
3166 -- SkolemInfo gives the origin of *given* constraints
3167 -- a) type variables are skolemised
3168 -- b) an implication constraint is generated
3169 data SkolemInfo
3170 = SigSkol -- A skolem that is created by instantiating
3171 -- a programmer-supplied type signature
3172 -- Location of the binding site is on the TyVar
3173 -- See Note [SigSkol SkolemInfo]
3174 UserTypeCtxt -- What sort of signature
3175 TcType -- Original type signature (before skolemisation)
3176 [(Name,TcTyVar)] -- Maps the original name of the skolemised tyvar
3177 -- to its instantiated version
3178
3179 | SigTypeSkol UserTypeCtxt
3180 -- like SigSkol, but when we're kind-checking the *type*
3181 -- hence, we have less info
3182
3183 | ForAllSkol SDoc -- Bound by a user-written "forall".
3184
3185 | DerivSkol Type -- Bound by a 'deriving' clause;
3186 -- the type is the instance we are trying to derive
3187
3188 | InstSkol -- Bound at an instance decl
3189 | InstSC TypeSize -- A "given" constraint obtained by superclass selection.
3190 -- If (C ty1 .. tyn) is the largest class from
3191 -- which we made a superclass selection in the chain,
3192 -- then TypeSize = sizeTypes [ty1, .., tyn]
3193 -- See Note [Solving superclass constraints] in TcInstDcls
3194
3195 | FamInstSkol -- Bound at a family instance decl
3196 | PatSkol -- An existential type variable bound by a pattern for
3197 ConLike -- a data constructor with an existential type.
3198 (HsMatchContext Name)
3199 -- e.g. data T = forall a. Eq a => MkT a
3200 -- f (MkT x) = ...
3201 -- The pattern MkT x will allocate an existential type
3202 -- variable for 'a'.
3203
3204 | ArrowSkol -- An arrow form (see TcArrows)
3205
3206 | IPSkol [HsIPName] -- Binding site of an implicit parameter
3207
3208 | RuleSkol RuleName -- The LHS of a RULE
3209
3210 | InferSkol [(Name,TcType)]
3211 -- We have inferred a type for these (mutually-recursivive)
3212 -- polymorphic Ids, and are now checking that their RHS
3213 -- constraints are satisfied.
3214
3215 | BracketSkol -- Template Haskell bracket
3216
3217 | UnifyForAllSkol -- We are unifying two for-all types
3218 TcType -- The instantiated type *inside* the forall
3219
3220 | TyConSkol TyConFlavour Name -- bound in a type declaration of the given flavour
3221
3222 | DataConSkol Name -- bound as an existential in a Haskell98 datacon decl or
3223 -- as any variable in a GADT datacon decl
3224
3225 | ReifySkol -- Bound during Template Haskell reification
3226
3227 | UnkSkol -- Unhelpful info (until I improve it)
3228
3229 instance Outputable SkolemInfo where
3230 ppr = pprSkolInfo
3231
3232 pprSkolInfo :: SkolemInfo -> SDoc
3233 -- Complete the sentence "is a rigid type variable bound by..."
3234 pprSkolInfo (SigSkol cx ty _) = pprSigSkolInfo cx ty
3235 pprSkolInfo (SigTypeSkol cx) = pprUserTypeCtxt cx
3236 pprSkolInfo (ForAllSkol doc) = quotes doc
3237 pprSkolInfo (IPSkol ips) = text "the implicit-parameter binding" <> plural ips <+> text "for"
3238 <+> pprWithCommas ppr ips
3239 pprSkolInfo (DerivSkol pred) = text "the deriving clause for" <+> quotes (ppr pred)
3240 pprSkolInfo InstSkol = text "the instance declaration"
3241 pprSkolInfo (InstSC n) = text "the instance declaration" <> whenPprDebug (parens (ppr n))
3242 pprSkolInfo FamInstSkol = text "a family instance declaration"
3243 pprSkolInfo BracketSkol = text "a Template Haskell bracket"
3244 pprSkolInfo (RuleSkol name) = text "the RULE" <+> pprRuleName name
3245 pprSkolInfo ArrowSkol = text "an arrow form"
3246 pprSkolInfo (PatSkol cl mc) = sep [ pprPatSkolInfo cl
3247 , text "in" <+> pprMatchContext mc ]
3248 pprSkolInfo (InferSkol ids) = hang (text "the inferred type" <> plural ids <+> text "of")
3249 2 (vcat [ ppr name <+> dcolon <+> ppr ty
3250 | (name,ty) <- ids ])
3251 pprSkolInfo (UnifyForAllSkol ty) = text "the type" <+> ppr ty
3252 pprSkolInfo (TyConSkol flav name) = text "the" <+> ppr flav <+> text "declaration for" <+> quotes (ppr name)
3253 pprSkolInfo (DataConSkol name)= text "the data constructor" <+> quotes (ppr name)
3254 pprSkolInfo ReifySkol = text "the type being reified"
3255
3256 -- UnkSkol
3257 -- For type variables the others are dealt with by pprSkolTvBinding.
3258 -- For Insts, these cases should not happen
3259 pprSkolInfo UnkSkol = WARN( True, text "pprSkolInfo: UnkSkol" ) text "UnkSkol"
3260
3261 pprSigSkolInfo :: UserTypeCtxt -> TcType -> SDoc
3262 -- The type is already tidied
3263 pprSigSkolInfo ctxt ty
3264 = case ctxt of
3265 FunSigCtxt f _ -> vcat [ text "the type signature for:"
3266 , nest 2 (pprPrefixOcc f <+> dcolon <+> ppr ty) ]
3267 PatSynCtxt {} -> pprUserTypeCtxt ctxt -- See Note [Skolem info for pattern synonyms]
3268 _ -> vcat [ pprUserTypeCtxt ctxt <> colon
3269 , nest 2 (ppr ty) ]
3270
3271 pprPatSkolInfo :: ConLike -> SDoc
3272 pprPatSkolInfo (RealDataCon dc)
3273 = sep [ text "a pattern with constructor:"
3274 , nest 2 $ ppr dc <+> dcolon
3275 <+> pprType (dataConUserType dc) <> comma ]
3276 -- pprType prints forall's regardless of -fprint-explicit-foralls
3277 -- which is what we want here, since we might be saying
3278 -- type variable 't' is bound by ...
3279
3280 pprPatSkolInfo (PatSynCon ps)
3281 = sep [ text "a pattern with pattern synonym:"
3282 , nest 2 $ ppr ps <+> dcolon
3283 <+> pprPatSynType ps <> comma ]
3284
3285 {- Note [Skolem info for pattern synonyms]
3286 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3287 For pattern synonym SkolemInfo we have
3288 SigSkol (PatSynCtxt p) ty _
3289 but the type 'ty' is not very helpful. The full pattern-synonym type
3290 has the provided and required pieces, which it is inconvenient to
3291 record and display here. So we simply don't display the type at all,
3292 contenting outselves with just the name of the pattern synonym, which
3293 is fine. We could do more, but it doesn't seem worth it.
3294
3295 Note [SigSkol SkolemInfo]
3296 ~~~~~~~~~~~~~~~~~~~~~~~~~
3297 Suppose we (deeply) skolemise a type
3298 f :: forall a. a -> forall b. b -> a
3299 Then we'll instantiate [a :-> a', b :-> b'], and with the instantiated
3300 a' -> b' -> a.
3301 But when, in an error message, we report that "b is a rigid type
3302 variable bound by the type signature for f", we want to show the foralls
3303 in the right place. So we proceed as follows:
3304
3305 * In SigSkol we record
3306 - the original signature forall a. a -> forall b. b -> a
3307 - the instantiation mapping [a :-> a', b :-> b']
3308
3309 * Then when tidying in TcMType.tidySkolemInfo, we first tidy a' to
3310 whatever it tidies to, say a''; and then we walk over the type
3311 replacing the binder a by the tidied version a'', to give
3312 forall a''. a'' -> forall b''. b'' -> a''
3313 We need to do this under function arrows, to match what deeplySkolemise
3314 does.
3315
3316 * Typically a'' will have a nice pretty name like "a", but the point is
3317 that the foral-bound variables of the signature we report line up with
3318 the instantiated skolems lying around in other types.
3319
3320
3321 ************************************************************************
3322 * *
3323 CtOrigin
3324 * *
3325 ************************************************************************
3326 -}
3327
3328 data CtOrigin
3329 = GivenOrigin SkolemInfo
3330
3331 -- All the others are for *wanted* constraints
3332 | OccurrenceOf Name -- Occurrence of an overloaded identifier
3333 | OccurrenceOfRecSel RdrName -- Occurrence of a record selector
3334 | AppOrigin -- An application of some kind
3335
3336 | SpecPragOrigin UserTypeCtxt -- Specialisation pragma for
3337 -- function or instance
3338
3339 | TypeEqOrigin { uo_actual :: TcType
3340 , uo_expected :: TcType
3341 , uo_thing :: Maybe SDoc
3342 -- ^ The thing that has type "actual"
3343 , uo_visible :: Bool
3344 -- ^ Is at least one of the three elements above visible?
3345 -- (Errors from the polymorphic subsumption check are considered
3346 -- visible.) Only used for prioritizing error messages.
3347 }
3348
3349 | KindEqOrigin -- See Note [Equalities with incompatible kinds] in TcCanonical.
3350 TcType (Maybe TcType) -- A kind equality arising from unifying these two types
3351 CtOrigin -- originally arising from this
3352 (Maybe TypeOrKind) -- the level of the eq this arises from
3353
3354 | IPOccOrigin HsIPName -- Occurrence of an implicit parameter
3355 | OverLabelOrigin FastString -- Occurrence of an overloaded label
3356
3357 | LiteralOrigin (HsOverLit GhcRn) -- Occurrence of a literal
3358 | NegateOrigin -- Occurrence of syntactic negation
3359
3360 | ArithSeqOrigin (ArithSeqInfo GhcRn) -- [x..], [x..y] etc
3361 | SectionOrigin
3362 | TupleOrigin -- (..,..)
3363 | ExprSigOrigin -- e :: ty
3364 | PatSigOrigin -- p :: ty
3365 | PatOrigin -- Instantiating a polytyped pattern at a constructor
3366 | ProvCtxtOrigin -- The "provided" context of a pattern synonym signature
3367 (PatSynBind GhcRn GhcRn) -- Information about the pattern synonym, in
3368 -- particular the name and the right-hand side
3369 | RecordUpdOrigin
3370 | ViewPatOrigin
3371
3372 | ScOrigin TypeSize -- Typechecking superclasses of an instance declaration
3373 -- If the instance head is C ty1 .. tyn
3374 -- then TypeSize = sizeTypes [ty1, .., tyn]
3375 -- See Note [Solving superclass constraints] in TcInstDcls
3376
3377 | DerivClauseOrigin -- Typechecking a deriving clause (as opposed to
3378 -- standalone deriving).
3379 | DerivOriginDC DataCon Int Bool
3380 -- Checking constraints arising from this data con and field index. The
3381 -- Bool argument in DerivOriginDC and DerivOriginCoerce is True if
3382 -- standalong deriving (with a wildcard constraint) is being used. This
3383 -- is used to inform error messages on how to recommended fixes (e.g., if
3384 -- the argument is True, then don't recommend "use standalone deriving",
3385 -- but rather "fill in the wildcard constraint yourself").
3386 -- See Note [Inferring the instance context] in TcDerivInfer
3387 | DerivOriginCoerce Id Type Type Bool
3388 -- DerivOriginCoerce id ty1 ty2: Trying to coerce class method `id` from
3389 -- `ty1` to `ty2`.
3390 | StandAloneDerivOrigin -- Typechecking stand-alone deriving. Useful for
3391 -- constraints coming from a wildcard constraint,
3392 -- e.g., deriving instance _ => Eq (Foo a)
3393 -- See Note [Inferring the instance context]
3394 -- in TcDerivInfer
3395 | DefaultOrigin -- Typechecking a default decl
3396 | DoOrigin -- Arising from a do expression
3397 | DoPatOrigin (LPat GhcRn) -- Arising from a failable pattern in
3398 -- a do expression
3399 | MCompOrigin -- Arising from a monad comprehension
3400 | MCompPatOrigin (LPat GhcRn) -- Arising from a failable pattern in a
3401 -- monad comprehension
3402 | IfOrigin -- Arising from an if statement
3403 | ProcOrigin -- Arising from a proc expression
3404 | AnnOrigin -- An annotation
3405
3406 | FunDepOrigin1 -- A functional dependency from combining
3407 PredType CtLoc -- This constraint arising from ...
3408 PredType CtLoc -- and this constraint arising from ...
3409
3410 | FunDepOrigin2 -- A functional dependency from combining
3411 PredType CtOrigin -- This constraint arising from ...
3412 PredType SrcSpan -- and this top-level instance
3413 -- We only need a CtOrigin on the first, because the location
3414 -- is pinned on the entire error message
3415
3416 | HoleOrigin
3417 | UnboundOccurrenceOf OccName
3418 | ListOrigin -- An overloaded list
3419 | StaticOrigin -- A static form
3420 | FailablePattern (LPat GhcTcId) -- A failable pattern in do-notation for the
3421 -- MonadFail Proposal (MFP). Obsolete when
3422 -- actual desugaring to MonadFail.fail is
3423 -- live.
3424 | Shouldn'tHappenOrigin String
3425 -- the user should never see this one,
3426 -- unless ImpredicativeTypes is on, where all
3427 -- bets are off
3428 | InstProvidedOrigin Module ClsInst
3429 -- Skolem variable arose when we were testing if an instance
3430 -- is solvable or not.
3431
3432 -- | Flag to see whether we're type-checking terms or kind-checking types
3433 data TypeOrKind = TypeLevel | KindLevel
3434 deriving Eq
3435
3436 instance Outputable TypeOrKind where
3437 ppr TypeLevel = text "TypeLevel"
3438 ppr KindLevel = text "KindLevel"
3439
3440 isTypeLevel :: TypeOrKind -> Bool
3441 isTypeLevel TypeLevel = True
3442 isTypeLevel KindLevel = False
3443
3444 isKindLevel :: TypeOrKind -> Bool
3445 isKindLevel TypeLevel = False
3446 isKindLevel KindLevel = True
3447
3448 -- An origin is visible if the place where the constraint arises is manifest
3449 -- in user code. Currently, all origins are visible except for invisible
3450 -- TypeEqOrigins. This is used when choosing which error of
3451 -- several to report
3452 isVisibleOrigin :: CtOrigin -> Bool
3453 isVisibleOrigin (TypeEqOrigin { uo_visible = vis }) = vis
3454 isVisibleOrigin (KindEqOrigin _ _ sub_orig _) = isVisibleOrigin sub_orig
3455 isVisibleOrigin _ = True
3456
3457 -- Converts a visible origin to an invisible one, if possible. Currently,
3458 -- this works only for TypeEqOrigin
3459 toInvisibleOrigin :: CtOrigin -> CtOrigin
3460 toInvisibleOrigin orig@(TypeEqOrigin {}) = orig { uo_visible = False }
3461 toInvisibleOrigin orig = orig
3462
3463 instance Outputable CtOrigin where
3464 ppr = pprCtOrigin
3465
3466 ctoHerald :: SDoc
3467 ctoHerald = text "arising from"
3468
3469 -- | Extract a suitable CtOrigin from a HsExpr
3470 lexprCtOrigin :: LHsExpr GhcRn -> CtOrigin
3471 lexprCtOrigin (L _ e) = exprCtOrigin e
3472
3473 exprCtOrigin :: HsExpr GhcRn -> CtOrigin
3474 exprCtOrigin (HsVar _ (L _ name)) = OccurrenceOf name
3475 exprCtOrigin (HsUnboundVar _ uv) = UnboundOccurrenceOf (unboundVarOcc uv)
3476 exprCtOrigin (HsConLikeOut {}) = panic "exprCtOrigin HsConLikeOut"
3477 exprCtOrigin (HsRecFld _ f) = OccurrenceOfRecSel (rdrNameAmbiguousFieldOcc f)
3478 exprCtOrigin (HsOverLabel _ _ l) = OverLabelOrigin l
3479 exprCtOrigin (HsIPVar _ ip) = IPOccOrigin ip
3480 exprCtOrigin (HsOverLit _ lit) = LiteralOrigin lit
3481 exprCtOrigin (HsLit {}) = Shouldn'tHappenOrigin "concrete literal"
3482 exprCtOrigin (HsLam _ matches) = matchesCtOrigin matches
3483 exprCtOrigin (HsLamCase _ ms) = matchesCtOrigin ms
3484 exprCtOrigin (HsApp _ e1 _) = lexprCtOrigin e1
3485 exprCtOrigin (HsAppType _ e1) = lexprCtOrigin e1
3486 exprCtOrigin (OpApp _ _ op _) = lexprCtOrigin op
3487 exprCtOrigin (NegApp _ e _) = lexprCtOrigin e
3488 exprCtOrigin (HsPar _ e) = lexprCtOrigin e
3489 exprCtOrigin (SectionL _ _ _) = SectionOrigin
3490 exprCtOrigin (SectionR _ _ _) = SectionOrigin
3491 exprCtOrigin (ExplicitTuple {}) = Shouldn'tHappenOrigin "explicit tuple"
3492 exprCtOrigin ExplicitSum{} = Shouldn'tHappenOrigin "explicit sum"
3493 exprCtOrigin (HsCase _ _ matches) = matchesCtOrigin matches
3494 exprCtOrigin (HsIf _ (Just syn) _ _ _) = exprCtOrigin (syn_expr syn)
3495 exprCtOrigin (HsIf {}) = Shouldn'tHappenOrigin "if expression"
3496 exprCtOrigin (HsMultiIf _ rhs) = lGRHSCtOrigin rhs
3497 exprCtOrigin (HsLet _ _ e) = lexprCtOrigin e
3498 exprCtOrigin (HsDo {}) = DoOrigin
3499 exprCtOrigin (ExplicitList {}) = Shouldn'tHappenOrigin "list"
3500 exprCtOrigin (RecordCon {}) = Shouldn'tHappenOrigin "record construction"
3501 exprCtOrigin (RecordUpd {}) = Shouldn'tHappenOrigin "record update"
3502 exprCtOrigin (ExprWithTySig {}) = ExprSigOrigin
3503 exprCtOrigin (ArithSeq {}) = Shouldn'tHappenOrigin "arithmetic sequence"
3504 exprCtOrigin (HsSCC _ _ _ e) = lexprCtOrigin e
3505 exprCtOrigin (HsCoreAnn _ _ _ e) = lexprCtOrigin e
3506 exprCtOrigin (HsBracket {}) = Shouldn'tHappenOrigin "TH bracket"
3507 exprCtOrigin (HsRnBracketOut {})= Shouldn'tHappenOrigin "HsRnBracketOut"
3508 exprCtOrigin (HsTcBracketOut {})= panic "exprCtOrigin HsTcBracketOut"
3509 exprCtOrigin (HsSpliceE {}) = Shouldn'tHappenOrigin "TH splice"
3510 exprCtOrigin (HsProc {}) = Shouldn'tHappenOrigin "proc"
3511 exprCtOrigin (HsStatic {}) = Shouldn'tHappenOrigin "static expression"
3512 exprCtOrigin (HsArrApp {}) = panic "exprCtOrigin HsArrApp"
3513 exprCtOrigin (HsArrForm {}) = panic "exprCtOrigin HsArrForm"
3514 exprCtOrigin (HsTick _ _ e) = lexprCtOrigin e
3515 exprCtOrigin (HsBinTick _ _ _ e) = lexprCtOrigin e
3516 exprCtOrigin (HsTickPragma _ _ _ _ e) = lexprCtOrigin e
3517 exprCtOrigin (EWildPat {}) = panic "exprCtOrigin EWildPat"
3518 exprCtOrigin (EAsPat {}) = panic "exprCtOrigin EAsPat"
3519 exprCtOrigin (EViewPat {}) = panic "exprCtOrigin EViewPat"
3520 exprCtOrigin (ELazyPat {}) = panic "exprCtOrigin ELazyPat"
3521 exprCtOrigin (HsWrap {}) = panic "exprCtOrigin HsWrap"
3522 exprCtOrigin (XExpr {}) = panic "exprCtOrigin XExpr"
3523
3524 -- | Extract a suitable CtOrigin from a MatchGroup
3525 matchesCtOrigin :: MatchGroup GhcRn (LHsExpr GhcRn) -> CtOrigin
3526 matchesCtOrigin (MG { mg_alts = alts })
3527 | L _ [L _ match] <- alts
3528 , Match { m_grhss = grhss } <- match
3529 = grhssCtOrigin grhss
3530
3531 | otherwise
3532 = Shouldn'tHappenOrigin "multi-way match"
3533 matchesCtOrigin (XMatchGroup{}) = panic "matchesCtOrigin"
3534
3535 -- | Extract a suitable CtOrigin from guarded RHSs
3536 grhssCtOrigin :: GRHSs GhcRn (LHsExpr GhcRn) -> CtOrigin
3537 grhssCtOrigin (GRHSs { grhssGRHSs = lgrhss }) = lGRHSCtOrigin lgrhss
3538 grhssCtOrigin (XGRHSs _) = panic "grhssCtOrigin"
3539
3540 -- | Extract a suitable CtOrigin from a list of guarded RHSs
3541 lGRHSCtOrigin :: [LGRHS GhcRn (LHsExpr GhcRn)] -> CtOrigin
3542 lGRHSCtOrigin [L _ (GRHS _ _ (L _ e))] = exprCtOrigin e
3543 lGRHSCtOrigin [L _ (XGRHS _)] = panic "lGRHSCtOrigin"
3544 lGRHSCtOrigin _ = Shouldn'tHappenOrigin "multi-way GRHS"
3545
3546 pprCtLoc :: CtLoc -> SDoc
3547 -- "arising from ... at ..."
3548 -- Not an instance of Outputable because of the "arising from" prefix
3549 pprCtLoc (CtLoc { ctl_origin = o, ctl_env = lcl})
3550 = sep [ pprCtOrigin o
3551 , text "at" <+> ppr (tcl_loc lcl)]
3552
3553 pprCtOrigin :: CtOrigin -> SDoc
3554 -- "arising from ..."
3555 -- Not an instance of Outputable because of the "arising from" prefix
3556 pprCtOrigin (GivenOrigin sk) = ctoHerald <+> ppr sk
3557
3558 pprCtOrigin (SpecPragOrigin ctxt)
3559 = case ctxt of
3560 FunSigCtxt n _ -> text "a SPECIALISE pragma for" <+> quotes (ppr n)
3561 SpecInstCtxt -> text "a SPECIALISE INSTANCE pragma"
3562 _ -> text "a SPECIALISE pragma" -- Never happens I think
3563
3564 pprCtOrigin (FunDepOrigin1 pred1 loc1 pred2 loc2)
3565 = hang (ctoHerald <+> text "a functional dependency between constraints:")
3566 2 (vcat [ hang (quotes (ppr pred1)) 2 (pprCtLoc loc1)
3567 , hang (quotes (ppr pred2)) 2 (pprCtLoc loc2) ])
3568
3569 pprCtOrigin (FunDepOrigin2 pred1 orig1 pred2 loc2)
3570 = hang (ctoHerald <+> text "a functional dependency between:")
3571 2 (vcat [ hang (text "constraint" <+> quotes (ppr pred1))
3572 2 (pprCtOrigin orig1 )
3573 , hang (text "instance" <+> quotes (ppr pred2))
3574 2 (text "at" <+> ppr loc2) ])
3575
3576 pprCtOrigin (KindEqOrigin t1 (Just t2) _ _)
3577 = hang (ctoHerald <+> text "a kind equality arising from")
3578 2 (sep [ppr t1, char '~', ppr t2])
3579
3580 pprCtOrigin (KindEqOrigin t1 Nothing _ _)
3581 = hang (ctoHerald <+> text "a kind equality when matching")
3582 2 (ppr t1)
3583
3584 pprCtOrigin (UnboundOccurrenceOf name)
3585 = ctoHerald <+> text "an undeclared identifier" <+> quotes (ppr name)
3586
3587 pprCtOrigin (DerivOriginDC dc n _)
3588 = hang (ctoHerald <+> text "the" <+> speakNth n
3589 <+> text "field of" <+> quotes (ppr dc))
3590 2 (parens (text "type" <+> quotes (ppr ty)))
3591 where
3592 ty = dataConOrigArgTys dc !! (n-1)
3593
3594 pprCtOrigin (DerivOriginCoerce meth ty1 ty2 _)
3595 = hang (ctoHerald <+> text "the coercion of the method" <+> quotes (ppr meth))
3596 2 (sep [ text "from type" <+> quotes (ppr ty1)
3597 , nest 2 $ text "to type" <+> quotes (ppr ty2) ])
3598
3599 pprCtOrigin (DoPatOrigin pat)
3600 = ctoHerald <+> text "a do statement"
3601 $$
3602 text "with the failable pattern" <+> quotes (ppr pat)
3603
3604 pprCtOrigin (MCompPatOrigin pat)
3605 = ctoHerald <+> hsep [ text "the failable pattern"
3606 , quotes (ppr pat)
3607 , text "in a statement in a monad comprehension" ]
3608 pprCtOrigin (FailablePattern pat)
3609 = ctoHerald <+> text "the failable pattern" <+> quotes (ppr pat)
3610 $$
3611 text "(this will become an error in a future GHC release)"
3612
3613 pprCtOrigin (Shouldn'tHappenOrigin note)
3614 = sdocWithDynFlags $ \dflags ->
3615 if xopt LangExt.ImpredicativeTypes dflags
3616 then text "a situation created by impredicative types"
3617 else
3618 vcat [ text "<< This should not appear in error messages. If you see this"
3619 , text "in an error message, please report a bug mentioning" <+> quotes (text note) <+> text "at"
3620 , text "https://ghc.haskell.org/trac/ghc/wiki/ReportABug >>" ]
3621
3622 pprCtOrigin (ProvCtxtOrigin PSB{ psb_id = (L _ name) })
3623 = hang (ctoHerald <+> text "the \"provided\" constraints claimed by")
3624 2 (text "the signature of" <+> quotes (ppr name))
3625
3626 pprCtOrigin (InstProvidedOrigin mod cls_inst)
3627 = vcat [ text "arising when attempting to show that"
3628 , ppr cls_inst
3629 , text "is provided by" <+> quotes (ppr mod)]
3630
3631 pprCtOrigin simple_origin
3632 = ctoHerald <+> pprCtO simple_origin
3633
3634 -- | Short one-liners
3635 pprCtO :: CtOrigin -> SDoc
3636 pprCtO (OccurrenceOf name) = hsep [text "a use of", quotes (ppr name)]
3637 pprCtO (OccurrenceOfRecSel name) = hsep [text "a use of", quotes (ppr name)]
3638 pprCtO AppOrigin = text "an application"
3639 pprCtO (IPOccOrigin name) = hsep [text "a use of implicit parameter", quotes (ppr name)]
3640 pprCtO (OverLabelOrigin l) = hsep [text "the overloaded label"
3641 ,quotes (char '#' <> ppr l)]
3642 pprCtO RecordUpdOrigin = text "a record update"
3643 pprCtO ExprSigOrigin = text "an expression type signature"
3644 pprCtO PatSigOrigin = text "a pattern type signature"
3645 pprCtO PatOrigin = text "a pattern"
3646 pprCtO ViewPatOrigin = text "a view pattern"
3647 pprCtO IfOrigin = text "an if expression"
3648 pprCtO (LiteralOrigin lit) = hsep [text "the literal", quotes (ppr lit)]
3649 pprCtO (ArithSeqOrigin seq) = hsep [text "the arithmetic sequence", quotes (ppr seq)]
3650 pprCtO SectionOrigin = text "an operator section"
3651 pprCtO TupleOrigin = text "a tuple"
3652 pprCtO NegateOrigin = text "a use of syntactic negation"
3653 pprCtO (ScOrigin n) = text "the superclasses of an instance declaration"
3654 <> whenPprDebug (parens (ppr n))
3655 pprCtO DerivClauseOrigin = text "the 'deriving' clause of a data type declaration"
3656 pprCtO StandAloneDerivOrigin = text "a 'deriving' declaration"
3657 pprCtO DefaultOrigin = text "a 'default' declaration"
3658 pprCtO DoOrigin = text "a do statement"
3659 pprCtO MCompOrigin = text "a statement in a monad comprehension"
3660 pprCtO ProcOrigin = text "a proc expression"
3661 pprCtO (TypeEqOrigin t1 t2 _ _)= text "a type equality" <+> sep [ppr t1, char '~', ppr t2]
3662 pprCtO AnnOrigin = text "an annotation"
3663 pprCtO HoleOrigin = text "a use of" <+> quotes (text "_")
3664 pprCtO ListOrigin = text "an overloaded list"
3665 pprCtO StaticOrigin = text "a static form"
3666 pprCtO _ = panic "pprCtOrigin"
3667
3668 {-
3669 Constraint Solver Plugins
3670 -------------------------
3671 -}
3672
3673 type TcPluginSolver = [Ct] -- given
3674 -> [Ct] -- derived
3675 -> [Ct] -- wanted
3676 -> TcPluginM TcPluginResult
3677
3678 newtype TcPluginM a = TcPluginM (EvBindsVar -> TcM a)
3679
3680 instance Functor TcPluginM where
3681 fmap = liftM
3682
3683 instance Applicative TcPluginM where
3684 pure x = TcPluginM (const $ pure x)
3685 (<*>) = ap
3686
3687 instance Monad TcPluginM where
3688 fail = MonadFail.fail
3689 TcPluginM m >>= k =
3690 TcPluginM (\ ev -> do a <- m ev
3691 runTcPluginM (k a) ev)
3692
3693 instance MonadFail.MonadFail TcPluginM where
3694 fail x = TcPluginM (const $ fail x)
3695
3696 runTcPluginM :: TcPluginM a -> EvBindsVar -> TcM a
3697 runTcPluginM (TcPluginM m) = m
3698
3699 -- | This function provides an escape for direct access to
3700 -- the 'TcM` monad. It should not be used lightly, and
3701 -- the provided 'TcPluginM' API should be favoured instead.
3702 unsafeTcPluginTcM :: TcM a -> TcPluginM a
3703 unsafeTcPluginTcM = TcPluginM . const
3704
3705 -- | Access the 'EvBindsVar' carried by the 'TcPluginM' during
3706 -- constraint solving. Returns 'Nothing' if invoked during
3707 -- 'tcPluginInit' or 'tcPluginStop'.
3708 getEvBindsTcPluginM :: TcPluginM EvBindsVar
3709 getEvBindsTcPluginM = TcPluginM return
3710
3711
3712 data TcPlugin = forall s. TcPlugin
3713 { tcPluginInit :: TcPluginM s
3714 -- ^ Initialize plugin, when entering type-checker.
3715
3716 , tcPluginSolve :: s -> TcPluginSolver
3717 -- ^ Solve some constraints.
3718 -- TODO: WRITE MORE DETAILS ON HOW THIS WORKS.
3719
3720 , tcPluginStop :: s -> TcPluginM ()
3721 -- ^ Clean up after the plugin, when exiting the type-checker.
3722 }
3723
3724 data TcPluginResult
3725 = TcPluginContradiction [Ct]
3726 -- ^ The plugin found a contradiction.
3727 -- The returned constraints are removed from the inert set,
3728 -- and recorded as insoluble.
3729
3730 | TcPluginOk [(EvTerm,Ct)] [Ct]
3731 -- ^ The first field is for constraints that were solved.
3732 -- These are removed from the inert set,
3733 -- and the evidence for them is recorded.
3734 -- The second field contains new work, that should be processed by
3735 -- the constraint solver.
3736
3737 {- *********************************************************************
3738 * *
3739 Role annotations
3740 * *
3741 ********************************************************************* -}
3742
3743 type RoleAnnotEnv = NameEnv (LRoleAnnotDecl GhcRn)
3744
3745 mkRoleAnnotEnv :: [LRoleAnnotDecl GhcRn] -> RoleAnnotEnv
3746 mkRoleAnnotEnv role_annot_decls
3747 = mkNameEnv [ (name, ra_decl)
3748 | ra_decl <- role_annot_decls
3749 , let name = roleAnnotDeclName (unLoc ra_decl)
3750 , not (isUnboundName name) ]
3751 -- Some of the role annots will be unbound;
3752 -- we don't wish to include these
3753
3754 emptyRoleAnnotEnv :: RoleAnnotEnv
3755 emptyRoleAnnotEnv = emptyNameEnv
3756
3757 lookupRoleAnnot :: RoleAnnotEnv -> Name -> Maybe (LRoleAnnotDecl GhcRn)
3758 lookupRoleAnnot = lookupNameEnv
3759
3760 getRoleAnnots :: [Name] -> RoleAnnotEnv
3761 -> ([LRoleAnnotDecl GhcRn], RoleAnnotEnv)
3762 getRoleAnnots bndrs role_env
3763 = ( mapMaybe (lookupRoleAnnot role_env) bndrs
3764 , delListFromNameEnv role_env bndrs )