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