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