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