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