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