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