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