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