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