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