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