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