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