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