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