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