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