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