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