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