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