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