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