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