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