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