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