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