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