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