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