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