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