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