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