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