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