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