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