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