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