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