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