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