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