Fix a nasty superclass expansion bug
[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 ViewPatterns #-}
21
22 module TcRnTypes(
23 TcRnIf, TcRn, TcM, RnM, IfM, IfL, IfG, -- The monad is opaque outside this module
24 TcRef,
25
26 -- The environment types
27 Env(..),
28 TcGblEnv(..), TcLclEnv(..),
29 IfGblEnv(..), IfLclEnv(..),
30 tcVisibleOrphanMods,
31
32 -- Frontend types (shouldn't really be here)
33 FrontendResult(..),
34
35 -- Renamer types
36 ErrCtxt, RecFieldEnv,
37 ImportAvails(..), emptyImportAvails, plusImportAvails,
38 WhereFrom(..), mkModDeps,
39
40 -- Typechecker types
41 TcTypeEnv, TcIdBinderStack, TcIdBinder(..),
42 TcTyThing(..), PromotionErr(..),
43 SelfBootInfo(..),
44 pprTcTyThingCategory, pprPECategory,
45
46 -- Desugaring types
47 DsM, DsLclEnv(..), DsGblEnv(..), PArrBuiltin(..),
48 DsMetaEnv, DsMetaVal(..),
49
50 -- Template Haskell
51 ThStage(..), SpliceType(..), PendingStuff(..),
52 topStage, topAnnStage, topSpliceStage,
53 ThLevel, impLevel, outerLevel, thLevel,
54
55 -- Arrows
56 ArrowCtxt(..),
57
58 -- TcSigInfo
59 TcSigFun, TcSigInfo(..), TcIdSigInfo(..),
60 TcPatSynInfo(..), TcIdSigBndr(..),
61 findScopedTyVars, isPartialSig, noCompleteSig, tcSigInfoName,
62 completeIdSigPolyId, completeSigPolyId_maybe,
63 completeIdSigPolyId_maybe,
64
65 -- Canonical constraints
66 Xi, Ct(..), Cts, emptyCts, andCts, andManyCts, pprCts,
67 singleCt, listToCts, ctsElts, consCts, snocCts, extendCtsList,
68 isEmptyCts, isCTyEqCan, isCFunEqCan,
69 isPendingScDict, superClassesMightHelp,
70 isCDictCan_Maybe, isCFunEqCan_maybe,
71 isCIrredEvCan, isCNonCanonical, isWantedCt, isDerivedCt,
72 isGivenCt, isHoleCt, isOutOfScopeCt, isExprHoleCt, isTypeHoleCt,
73 isUserTypeErrorCt, isCallStackDict, getUserTypeErrorMsg,
74 ctEvidence, ctLoc, setCtLoc, ctPred, ctFlavour, ctEqRel, ctOrigin,
75 mkTcEqPredLikeEv,
76 mkNonCanonical, mkNonCanonicalCt,
77 ctEvPred, ctEvLoc, ctEvOrigin, ctEvEqRel,
78 ctEvTerm, ctEvCoercion, ctEvId,
79 tyCoVarsOfCt, tyCoVarsOfCts,
80 tyCoVarsOfCtList, tyCoVarsOfCtsList,
81 toDerivedCt,
82
83 WantedConstraints(..), insolubleWC, emptyWC, isEmptyWC,
84 toDerivedWC,
85 andWC, unionsWC, mkSimpleWC, mkImplicWC,
86 addInsols, addSimples, addImplics,
87 tyCoVarsOfWC, dropDerivedWC, dropDerivedSimples, dropDerivedInsols,
88 isDroppableDerivedLoc, insolubleImplic,
89 arisesFromGivens,
90
91 Implication(..), ImplicStatus(..), isInsolubleStatus,
92 SubGoalDepth, initialSubGoalDepth,
93 bumpSubGoalDepth, subGoalDepthExceeded,
94 CtLoc(..), ctLocSpan, ctLocEnv, ctLocLevel, ctLocOrigin,
95 ctLocTypeOrKind_maybe,
96 ctLocDepth, bumpCtLocDepth,
97 setCtLocOrigin, setCtLocEnv, setCtLocSpan,
98 CtOrigin(..), exprCtOrigin, matchesCtOrigin, grhssCtOrigin,
99 ErrorThing(..), mkErrorThing, errorThingNumArgs_maybe,
100 TypeOrKind(..), isTypeLevel, isKindLevel,
101 pprCtOrigin, pprCtLoc,
102 pushErrCtxt, pushErrCtxtSameOrigin,
103
104 SkolemInfo(..), pprSigSkolInfo, pprSkolInfo,
105
106 CtEvidence(..), TcEvDest(..),
107 mkGivenLoc, mkKindLoc, toKindLoc,
108 isWanted, isGiven, isDerived,
109 ctEvRole,
110
111 -- Constraint solver plugins
112 TcPlugin(..), TcPluginResult(..), TcPluginSolver,
113 TcPluginM, runTcPluginM, unsafeTcPluginTcM,
114 getEvBindsTcPluginM_maybe,
115
116 CtFlavour(..), ctEvFlavour,
117 CtFlavourRole, ctEvFlavourRole, ctFlavourRole,
118 eqCanRewrite, eqCanRewriteFR, eqCanDischarge,
119 funEqCanDischarge, funEqCanDischargeFR,
120
121 -- Pretty printing
122 pprEvVarTheta,
123 pprEvVars, pprEvVarWithType,
124
125 -- Misc other types
126 TcId, TcIdSet, HoleSort(..)
127
128 ) where
129
130 #include "HsVersions.h"
131
132 import HsSyn
133 import CoreSyn
134 import HscTypes
135 import TcEvidence
136 import Type
137 import Class ( Class )
138 import TyCon ( TyCon )
139 import Coercion ( Coercion, mkHoleCo )
140 import ConLike ( ConLike(..) )
141 import DataCon ( DataCon, dataConUserType, dataConOrigArgTys )
142 import PatSyn ( PatSyn, patSynType )
143 import Id ( idName )
144 import PrelNames ( callStackTyConKey, ipClassKey )
145 import Unique ( hasKey )
146 import FieldLabel ( FieldLabel )
147 import TcType
148 import Annotations
149 import InstEnv
150 import FamInstEnv
151 import PmExpr
152 import IOEnv
153 import RdrName
154 import Name
155 import NameEnv
156 import NameSet
157 import Avail
158 import Var
159 import FV
160 import VarEnv
161 import Module
162 import SrcLoc
163 import VarSet
164 import ErrUtils
165 import UniqFM
166 import UniqSupply
167 import BasicTypes
168 import Bag
169 import DynFlags
170 import Outputable
171 import ListSetOps
172 import FastString
173 import GHC.Fingerprint
174 import qualified GHC.LanguageExtensions as LangExt
175
176 import Control.Monad (ap, liftM, msum)
177 #if __GLASGOW_HASKELL__ > 710
178 import qualified Control.Monad.Fail as MonadFail
179 #endif
180
181 #ifdef GHCI
182 import Data.Map ( Map )
183 import Data.Dynamic ( Dynamic )
184 import Data.Typeable ( TypeRep )
185 import GHCi.Message
186 import GHCi.RemoteTypes
187
188 import qualified Language.Haskell.TH as TH
189 #endif
190
191 {-
192 ************************************************************************
193 * *
194 Standard monad definition for TcRn
195 All the combinators for the monad can be found in TcRnMonad
196 * *
197 ************************************************************************
198
199 The monad itself has to be defined here, because it is mentioned by ErrCtxt
200 -}
201
202 type TcRnIf a b = IOEnv (Env a b)
203 type TcRn = TcRnIf TcGblEnv TcLclEnv -- Type inference
204 type IfM lcl = TcRnIf IfGblEnv lcl -- Iface stuff
205 type IfG = IfM () -- Top level
206 type IfL = IfM IfLclEnv -- Nested
207 type DsM = TcRnIf DsGblEnv DsLclEnv -- Desugaring
208
209 -- TcRn is the type-checking and renaming monad: the main monad that
210 -- most type-checking takes place in. The global environment is
211 -- 'TcGblEnv', which tracks all of the top-level type-checking
212 -- information we've accumulated while checking a module, while the
213 -- local environment is 'TcLclEnv', which tracks local information as
214 -- we move inside expressions.
215
216 -- | Historical "renaming monad" (now it's just 'TcRn').
217 type RnM = TcRn
218
219 -- | Historical "type-checking monad" (now it's just 'TcRn').
220 type TcM = TcRn
221
222 -- We 'stack' these envs through the Reader like monad infastructure
223 -- as we move into an expression (although the change is focused in
224 -- the lcl type).
225 data Env gbl lcl
226 = Env {
227 env_top :: HscEnv, -- Top-level stuff that never changes
228 -- Includes all info about imported things
229
230 env_us :: {-# UNPACK #-} !(IORef UniqSupply),
231 -- Unique supply for local variables
232
233 env_gbl :: gbl, -- Info about things defined at the top level
234 -- of the module being compiled
235
236 env_lcl :: lcl -- Nested stuff; changes as we go into
237 }
238
239 instance ContainsDynFlags (Env gbl lcl) where
240 extractDynFlags env = hsc_dflags (env_top env)
241
242 instance ContainsModule gbl => ContainsModule (Env gbl lcl) where
243 extractModule env = extractModule (env_gbl env)
244
245
246 {-
247 ************************************************************************
248 * *
249 The interface environments
250 Used when dealing with IfaceDecls
251 * *
252 ************************************************************************
253 -}
254
255 data IfGblEnv
256 = IfGblEnv {
257 -- The type environment for the module being compiled,
258 -- in case the interface refers back to it via a reference that
259 -- was originally a hi-boot file.
260 -- We need the module name so we can test when it's appropriate
261 -- to look in this env.
262 if_rec_types :: Maybe (Module, IfG TypeEnv)
263 -- Allows a read effect, so it can be in a mutable
264 -- variable; c.f. handling the external package type env
265 -- Nothing => interactive stuff, no loops possible
266 }
267
268 data IfLclEnv
269 = IfLclEnv {
270 -- The module for the current IfaceDecl
271 -- So if we see f = \x -> x
272 -- it means M.f = \x -> x, where M is the if_mod
273 if_mod :: Module,
274
275 -- The field is used only for error reporting
276 -- if (say) there's a Lint error in it
277 if_loc :: SDoc,
278 -- Where the interface came from:
279 -- .hi file, or GHCi state, or ext core
280 -- plus which bit is currently being examined
281
282 if_tv_env :: UniqFM TyVar, -- Nested tyvar bindings
283 if_id_env :: UniqFM Id -- Nested id binding
284 }
285
286 {-
287 ************************************************************************
288 * *
289 Desugarer monad
290 * *
291 ************************************************************************
292
293 Now the mondo monad magic (yes, @DsM@ is a silly name)---carry around
294 a @UniqueSupply@ and some annotations, which
295 presumably include source-file location information:
296 -}
297
298 -- If '-XParallelArrays' is given, the desugarer populates this table with the corresponding
299 -- variables found in 'Data.Array.Parallel'.
300 --
301 data PArrBuiltin
302 = PArrBuiltin
303 { lengthPVar :: Var -- ^ lengthP
304 , replicatePVar :: Var -- ^ replicateP
305 , singletonPVar :: Var -- ^ singletonP
306 , mapPVar :: Var -- ^ mapP
307 , filterPVar :: Var -- ^ filterP
308 , zipPVar :: Var -- ^ zipP
309 , crossMapPVar :: Var -- ^ crossMapP
310 , indexPVar :: Var -- ^ (!:)
311 , emptyPVar :: Var -- ^ emptyP
312 , appPVar :: Var -- ^ (+:+)
313 , enumFromToPVar :: Var -- ^ enumFromToP
314 , enumFromThenToPVar :: Var -- ^ enumFromThenToP
315 }
316
317 data DsGblEnv
318 = DsGblEnv
319 { ds_mod :: Module -- For SCC profiling
320 , ds_fam_inst_env :: FamInstEnv -- Like tcg_fam_inst_env
321 , ds_unqual :: PrintUnqualified
322 , ds_msgs :: IORef Messages -- Warning messages
323 , ds_if_env :: (IfGblEnv, IfLclEnv) -- Used for looking up global,
324 -- possibly-imported things
325 , ds_dph_env :: GlobalRdrEnv -- exported entities of 'Data.Array.Parallel.Prim'
326 -- iff '-fvectorise' flag was given as well as
327 -- exported entities of 'Data.Array.Parallel' iff
328 -- '-XParallelArrays' was given; otherwise, empty
329 , ds_parr_bi :: PArrBuiltin -- desugarar names for '-XParallelArrays'
330 , ds_static_binds :: IORef [(Fingerprint, (Id,CoreExpr))]
331 -- ^ Bindings resulted from floating static forms
332 }
333
334 instance ContainsModule DsGblEnv where
335 extractModule = ds_mod
336
337 data DsLclEnv = DsLclEnv {
338 dsl_meta :: DsMetaEnv, -- Template Haskell bindings
339 dsl_loc :: RealSrcSpan, -- To put in pattern-matching error msgs
340 dsl_dicts :: Bag EvVar, -- Constraints from GADT pattern-matching
341 dsl_tm_cs :: Bag SimpleEq,
342 dsl_pm_iter :: IORef Int -- no iterations for pmcheck
343 }
344
345 -- Inside [| |] brackets, the desugarer looks
346 -- up variables in the DsMetaEnv
347 type DsMetaEnv = NameEnv DsMetaVal
348
349 data DsMetaVal
350 = DsBound Id -- Bound by a pattern inside the [| |].
351 -- Will be dynamically alpha renamed.
352 -- The Id has type THSyntax.Var
353
354 | DsSplice (HsExpr Id) -- These bindings are introduced by
355 -- the PendingSplices on a HsBracketOut
356
357
358 {-
359 ************************************************************************
360 * *
361 Global typechecker environment
362 * *
363 ************************************************************************
364 -}
365
366 -- | 'FrontendResult' describes the result of running the
367 -- frontend of a Haskell module. Usually, you'll get
368 -- a 'FrontendTypecheck', since running the frontend involves
369 -- typechecking a program, but for an hs-boot merge you'll
370 -- just get a ModIface, since no actual typechecking occurred.
371 --
372 -- This data type really should be in HscTypes, but it needs
373 -- to have a TcGblEnv which is only defined here.
374 data FrontendResult
375 = FrontendTypecheck TcGblEnv
376
377 -- | 'TcGblEnv' describes the top-level of the module at the
378 -- point at which the typechecker is finished work.
379 -- It is this structure that is handed on to the desugarer
380 -- For state that needs to be updated during the typechecking
381 -- phase and returned at end, use a 'TcRef' (= 'IORef').
382 data TcGblEnv
383 = TcGblEnv {
384 tcg_mod :: Module, -- ^ Module being compiled
385 tcg_src :: HscSource,
386 -- ^ What kind of module (regular Haskell, hs-boot, hsig)
387 tcg_sig_of :: Maybe Module,
388 -- ^ Are we being compiled as a signature of an implementation?
389 tcg_impl_rdr_env :: Maybe GlobalRdrEnv,
390 -- ^ Environment used only during -sig-of for resolving top level
391 -- bindings. See Note [Signature parameters in TcGblEnv and DynFlags]
392
393 tcg_rdr_env :: GlobalRdrEnv, -- ^ Top level envt; used during renaming
394 tcg_default :: Maybe [Type],
395 -- ^ Types used for defaulting. @Nothing@ => no @default@ decl
396
397 tcg_fix_env :: FixityEnv, -- ^ Just for things in this module
398 tcg_field_env :: RecFieldEnv, -- ^ Just for things in this module
399 -- See Note [The interactive package] in HscTypes
400
401 tcg_type_env :: TypeEnv,
402 -- ^ Global type env for the module we are compiling now. All
403 -- TyCons and Classes (for this module) end up in here right away,
404 -- along with their derived constructors, selectors.
405 --
406 -- (Ids defined in this module start in the local envt, though they
407 -- move to the global envt during zonking)
408 --
409 -- NB: for what "things in this module" means, see
410 -- Note [The interactive package] in HscTypes
411
412 tcg_type_env_var :: TcRef TypeEnv,
413 -- Used only to initialise the interface-file
414 -- typechecker in initIfaceTcRn, so that it can see stuff
415 -- bound in this module when dealing with hi-boot recursions
416 -- Updated at intervals (e.g. after dealing with types and classes)
417
418 tcg_inst_env :: InstEnv,
419 -- ^ Instance envt for all /home-package/ modules;
420 -- Includes the dfuns in tcg_insts
421 tcg_fam_inst_env :: FamInstEnv, -- ^ Ditto for family instances
422 tcg_ann_env :: AnnEnv, -- ^ And for annotations
423
424 -- Now a bunch of things about this module that are simply
425 -- accumulated, but never consulted until the end.
426 -- Nevertheless, it's convenient to accumulate them along
427 -- with the rest of the info from this module.
428 tcg_exports :: [AvailInfo], -- ^ What is exported
429 tcg_imports :: ImportAvails,
430 -- ^ Information about what was imported from where, including
431 -- things bound in this module. Also store Safe Haskell info
432 -- here about transative trusted packaage requirements.
433
434 tcg_dus :: DefUses, -- ^ What is defined in this module and what is used.
435 tcg_used_gres :: TcRef [GlobalRdrElt], -- ^ Records occurrences of imported entities
436 -- See Note [Tracking unused binding and imports]
437
438 tcg_keep :: TcRef NameSet,
439 -- ^ Locally-defined top-level names to keep alive.
440 --
441 -- "Keep alive" means give them an Exported flag, so that the
442 -- simplifier does not discard them as dead code, and so that they
443 -- are exposed in the interface file (but not to export to the
444 -- user).
445 --
446 -- Some things, like dict-fun Ids and default-method Ids are "born"
447 -- with the Exported flag on, for exactly the above reason, but some
448 -- we only discover as we go. Specifically:
449 --
450 -- * The to/from functions for generic data types
451 --
452 -- * Top-level variables appearing free in the RHS of an orphan
453 -- rule
454 --
455 -- * Top-level variables appearing free in a TH bracket
456
457 tcg_th_used :: TcRef Bool,
458 -- ^ @True@ <=> Template Haskell syntax used.
459 --
460 -- We need this so that we can generate a dependency on the
461 -- Template Haskell package, because the desugarer is going
462 -- to emit loads of references to TH symbols. The reference
463 -- is implicit rather than explicit, so we have to zap a
464 -- mutable variable.
465
466 tcg_th_splice_used :: TcRef Bool,
467 -- ^ @True@ <=> A Template Haskell splice was used.
468 --
469 -- Splices disable recompilation avoidance (see #481)
470
471 tcg_dfun_n :: TcRef OccSet,
472 -- ^ Allows us to choose unique DFun names.
473
474 -- The next fields accumulate the payload of the module
475 -- The binds, rules and foreign-decl fields are collected
476 -- initially in un-zonked form and are finally zonked in tcRnSrcDecls
477
478 tcg_rn_exports :: Maybe [Located (IE Name)],
479 -- Nothing <=> no explicit export list
480 -- Is always Nothing if we don't want to retain renamed
481 -- exports
482
483 tcg_rn_imports :: [LImportDecl Name],
484 -- Keep the renamed imports regardless. They are not
485 -- voluminous and are needed if you want to report unused imports
486
487 tcg_rn_decls :: Maybe (HsGroup Name),
488 -- ^ Renamed decls, maybe. @Nothing@ <=> Don't retain renamed
489 -- decls.
490
491 tcg_dependent_files :: TcRef [FilePath], -- ^ dependencies from addDependentFile
492
493 #ifdef GHCI
494 tcg_th_topdecls :: TcRef [LHsDecl RdrName],
495 -- ^ Top-level declarations from addTopDecls
496
497 tcg_th_topnames :: TcRef NameSet,
498 -- ^ Exact names bound in top-level declarations in tcg_th_topdecls
499
500 tcg_th_modfinalizers :: TcRef [TH.Q ()],
501 -- ^ Template Haskell module finalizers
502
503 tcg_th_state :: TcRef (Map TypeRep Dynamic),
504 tcg_th_remote_state :: TcRef (Maybe (ForeignRef (IORef QState))),
505 -- ^ Template Haskell state
506 #endif /* GHCI */
507
508 tcg_ev_binds :: Bag EvBind, -- Top-level evidence bindings
509
510 -- Things defined in this module, or (in GHCi)
511 -- in the declarations for a single GHCi command.
512 -- For the latter, see Note [The interactive package] in HscTypes
513 tcg_tr_module :: Maybe Id, -- Id for $trModule :: GHC.Types.Module
514 -- for which every module has a top-level defn
515 -- except in GHCi in which case we have Nothing
516 tcg_binds :: LHsBinds Id, -- Value bindings in this module
517 tcg_sigs :: NameSet, -- ...Top-level names that *lack* a signature
518 tcg_imp_specs :: [LTcSpecPrag], -- ...SPECIALISE prags for imported Ids
519 tcg_warns :: Warnings, -- ...Warnings and deprecations
520 tcg_anns :: [Annotation], -- ...Annotations
521 tcg_tcs :: [TyCon], -- ...TyCons and Classes
522 tcg_insts :: [ClsInst], -- ...Instances
523 tcg_fam_insts :: [FamInst], -- ...Family instances
524 tcg_rules :: [LRuleDecl Id], -- ...Rules
525 tcg_fords :: [LForeignDecl Id], -- ...Foreign import & exports
526 tcg_vects :: [LVectDecl Id], -- ...Vectorisation declarations
527 tcg_patsyns :: [PatSyn], -- ...Pattern synonyms
528
529 tcg_doc_hdr :: Maybe LHsDocString, -- ^ Maybe Haddock header docs
530 tcg_hpc :: AnyHpcUsage, -- ^ @True@ if any part of the
531 -- prog uses hpc instrumentation.
532
533 tcg_self_boot :: SelfBootInfo, -- ^ Whether this module has a
534 -- corresponding hi-boot file
535
536 tcg_main :: Maybe Name, -- ^ The Name of the main
537 -- function, if this module is
538 -- the main module.
539
540 tcg_safeInfer :: TcRef (Bool, WarningMessages),
541 -- ^ Has the typechecker inferred this module as -XSafe (Safe Haskell)
542 -- See Note [Safe Haskell Overlapping Instances Implementation],
543 -- although this is used for more than just that failure case.
544
545 tcg_tc_plugins :: [TcPluginSolver],
546 -- ^ A list of user-defined plugins for the constraint solver.
547
548 tcg_static_wc :: TcRef WantedConstraints
549 -- ^ Wanted constraints of static forms.
550 }
551
552 tcVisibleOrphanMods :: TcGblEnv -> ModuleSet
553 tcVisibleOrphanMods tcg_env
554 = mkModuleSet (tcg_mod tcg_env : imp_orphs (tcg_imports tcg_env))
555
556 -- Note [Signature parameters in TcGblEnv and DynFlags]
557 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
558 -- When compiling signature files, we need to know which implementation
559 -- we've actually linked against the signature. There are three seemingly
560 -- redundant places where this information is stored: in DynFlags, there
561 -- is sigOf, and in TcGblEnv, there is tcg_sig_of and tcg_impl_rdr_env.
562 -- Here's the difference between each of them:
563 --
564 -- * DynFlags.sigOf is global per invocation of GHC. If we are compiling
565 -- with --make, there may be multiple signature files being compiled; in
566 -- which case this parameter is a map from local module name to implementing
567 -- Module.
568 --
569 -- * HscEnv.tcg_sig_of is global per the compilation of a single file, so
570 -- it is simply the result of looking up tcg_mod in the DynFlags.sigOf
571 -- parameter. It's setup in TcRnMonad.initTc. This prevents us
572 -- from having to repeatedly do a lookup in DynFlags.sigOf.
573 --
574 -- * HscEnv.tcg_impl_rdr_env is a RdrEnv that lets us look up names
575 -- according to the sig-of module. It's setup in TcRnDriver.tcRnSignature.
576 -- Here is an example showing why we need this map:
577 --
578 -- module A where
579 -- a = True
580 --
581 -- module ASig where
582 -- import B
583 -- a :: Bool
584 --
585 -- module B where
586 -- b = False
587 --
588 -- When we compile ASig --sig-of main:A, the default
589 -- global RdrEnv (tcg_rdr_env) has an entry for b, but not for a
590 -- (we never imported A). So we have to look in a different environment
591 -- to actually get the original name.
592 --
593 -- By the way, why do we need to do the lookup; can't we just use A:a
594 -- as the name directly? Well, if A is reexporting the entity from another
595 -- module, then the original name needs to be the real original name:
596 --
597 -- module C where
598 -- a = True
599 --
600 -- module A(a) where
601 -- import C
602
603 instance ContainsModule TcGblEnv where
604 extractModule env = tcg_mod env
605
606 type RecFieldEnv = NameEnv [FieldLabel]
607 -- Maps a constructor name *in this module*
608 -- to the fields for that constructor.
609 -- This is used when dealing with ".." notation in record
610 -- construction and pattern matching.
611 -- The FieldEnv deals *only* with constructors defined in *this*
612 -- module. For imported modules, we get the same info from the
613 -- TypeEnv
614
615 data SelfBootInfo
616 = NoSelfBoot -- No corresponding hi-boot file
617 | SelfBoot
618 { sb_mds :: ModDetails -- There was a hi-boot file,
619 , sb_tcs :: NameSet -- defining these TyCons,
620 , sb_ids :: NameSet } -- and these Ids
621 -- We need this info to compute a safe approximation to
622 -- recursive loops, to avoid infinite inlinings
623
624 {- Note [Tracking unused binding and imports]
625 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
626 We gather two sorts of usage information
627
628 * tcg_dus (defs/uses)
629 Records *defined* Names (local, top-level)
630 and *used* Names (local or imported)
631
632 Used (a) to report "defined but not used"
633 (see RnNames.reportUnusedNames)
634 (b) to generate version-tracking usage info in interface
635 files (see MkIface.mkUsedNames)
636 This usage info is mainly gathered by the renamer's
637 gathering of free-variables
638
639 * tcg_used_gres
640 Used only to report unused import declarations
641
642 Records each *occurrence* an *imported* (not locally-defined) entity.
643 The occurrence is recorded by keeping a GlobalRdrElt for it.
644 These is not the GRE that is in the GlobalRdrEnv; rather it
645 is recorded *after* the filtering done by pickGREs. So it reflect
646 /how that occurrence is in scope/. See Note [GRE filtering] in
647 RdrName.
648
649
650 ************************************************************************
651 * *
652 The local typechecker environment
653 * *
654 ************************************************************************
655
656 Note [The Global-Env/Local-Env story]
657 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
658 During type checking, we keep in the tcg_type_env
659 * All types and classes
660 * All Ids derived from types and classes (constructors, selectors)
661
662 At the end of type checking, we zonk the local bindings,
663 and as we do so we add to the tcg_type_env
664 * Locally defined top-level Ids
665
666 Why? Because they are now Ids not TcIds. This final GlobalEnv is
667 a) fed back (via the knot) to typechecking the
668 unfoldings of interface signatures
669 b) used in the ModDetails of this module
670 -}
671
672 data TcLclEnv -- Changes as we move inside an expression
673 -- Discarded after typecheck/rename; not passed on to desugarer
674 = TcLclEnv {
675 tcl_loc :: RealSrcSpan, -- Source span
676 tcl_ctxt :: [ErrCtxt], -- Error context, innermost on top
677 tcl_tclvl :: TcLevel, -- Birthplace for new unification variables
678
679 tcl_th_ctxt :: ThStage, -- Template Haskell context
680 tcl_th_bndrs :: ThBindEnv, -- Binding level of in-scope Names
681 -- defined in this module (not imported)
682
683 tcl_arrow_ctxt :: ArrowCtxt, -- Arrow-notation context
684
685 tcl_rdr :: LocalRdrEnv, -- Local name envt
686 -- Maintained during renaming, of course, but also during
687 -- type checking, solely so that when renaming a Template-Haskell
688 -- splice we have the right environment for the renamer.
689 --
690 -- Does *not* include global name envt; may shadow it
691 -- Includes both ordinary variables and type variables;
692 -- they are kept distinct because tyvar have a different
693 -- occurrence contructor (Name.TvOcc)
694 -- We still need the unsullied global name env so that
695 -- we can look up record field names
696
697 tcl_env :: TcTypeEnv, -- The local type environment:
698 -- Ids and TyVars defined in this module
699
700 tcl_bndrs :: TcIdBinderStack, -- Used for reporting relevant bindings
701
702 tcl_tidy :: TidyEnv, -- Used for tidying types; contains all
703 -- in-scope type variables (but not term variables)
704
705 tcl_tyvars :: TcRef TcTyVarSet, -- The "global tyvars"
706 -- Namely, the in-scope TyVars bound in tcl_env,
707 -- plus the tyvars mentioned in the types of Ids bound
708 -- in tcl_lenv.
709 -- Why mutable? see notes with tcGetGlobalTyCoVars
710
711 tcl_lie :: TcRef WantedConstraints, -- Place to accumulate type constraints
712 tcl_errs :: TcRef Messages -- Place to accumulate errors
713 }
714
715 type TcTypeEnv = NameEnv TcTyThing
716
717 type ThBindEnv = NameEnv (TopLevelFlag, ThLevel)
718 -- Domain = all Ids bound in this module (ie not imported)
719 -- The TopLevelFlag tells if the binding is syntactically top level.
720 -- We need to know this, because the cross-stage persistence story allows
721 -- cross-stage at arbitrary types if the Id is bound at top level.
722 --
723 -- Nota bene: a ThLevel of 'outerLevel' is *not* the same as being
724 -- bound at top level! See Note [Template Haskell levels] in TcSplice
725
726 {- Note [Given Insts]
727 ~~~~~~~~~~~~~~~~~~
728 Because of GADTs, we have to pass inwards the Insts provided by type signatures
729 and existential contexts. Consider
730 data T a where { T1 :: b -> b -> T [b] }
731 f :: Eq a => T a -> Bool
732 f (T1 x y) = [x]==[y]
733
734 The constructor T1 binds an existential variable 'b', and we need Eq [b].
735 Well, we have it, because Eq a refines to Eq [b], but we can only spot that if we
736 pass it inwards.
737
738 -}
739
740 -- | Type alias for 'IORef'; the convention is we'll use this for mutable
741 -- bits of data in 'TcGblEnv' which are updated during typechecking and
742 -- returned at the end.
743 type TcRef a = IORef a
744 -- ToDo: when should I refer to it as a 'TcId' instead of an 'Id'?
745 type TcId = Id
746 type TcIdSet = IdSet
747
748 ---------------------------
749 -- The TcIdBinderStack
750 ---------------------------
751
752 type TcIdBinderStack = [TcIdBinder]
753 -- This is a stack of locally-bound ids, innermost on top
754 -- Used ony in error reporting (relevantBindings in TcError)
755
756 data TcIdBinder
757 = TcIdBndr
758 TcId
759 TopLevelFlag -- Tells whether the bindind is syntactically top-level
760 -- (The monomorphic Ids for a recursive group count
761 -- as not-top-level for this purpose.)
762 | TcIdBndr_ExpType -- Variant that allows the type to be specified as
763 -- an ExpType
764 Name
765 ExpType
766 TopLevelFlag
767
768 instance Outputable TcIdBinder where
769 ppr (TcIdBndr id top_lvl) = ppr id <> brackets (ppr top_lvl)
770 ppr (TcIdBndr_ExpType id _ top_lvl) = ppr id <> brackets (ppr top_lvl)
771
772 ---------------------------
773 -- Template Haskell stages and levels
774 ---------------------------
775
776 data SpliceType = Typed | Untyped
777
778 data ThStage -- See Note [Template Haskell state diagram] in TcSplice
779 = Splice SpliceType -- Inside a top-level splice
780 -- This code will be run *at compile time*;
781 -- the result replaces the splice
782 -- Binding level = 0
783
784 | Comp -- Ordinary Haskell code
785 -- Binding level = 1
786
787 | Brack -- Inside brackets
788 ThStage -- Enclosing stage
789 PendingStuff
790
791 data PendingStuff
792 = RnPendingUntyped -- Renaming the inside of an *untyped* bracket
793 (TcRef [PendingRnSplice]) -- Pending splices in here
794
795 | RnPendingTyped -- Renaming the inside of a *typed* bracket
796
797 | TcPending -- Typechecking the inside of a typed bracket
798 (TcRef [PendingTcSplice]) -- Accumulate pending splices here
799 (TcRef WantedConstraints) -- and type constraints here
800
801 topStage, topAnnStage, topSpliceStage :: ThStage
802 topStage = Comp
803 topAnnStage = Splice Untyped
804 topSpliceStage = Splice Untyped
805
806 instance Outputable ThStage where
807 ppr (Splice _) = text "Splice"
808 ppr Comp = text "Comp"
809 ppr (Brack s _) = text "Brack" <> parens (ppr s)
810
811 type ThLevel = Int
812 -- NB: see Note [Template Haskell levels] in TcSplice
813 -- Incremented when going inside a bracket,
814 -- decremented when going inside a splice
815 -- NB: ThLevel is one greater than the 'n' in Fig 2 of the
816 -- original "Template meta-programming for Haskell" paper
817
818 impLevel, outerLevel :: ThLevel
819 impLevel = 0 -- Imported things; they can be used inside a top level splice
820 outerLevel = 1 -- Things defined outside brackets
821
822 thLevel :: ThStage -> ThLevel
823 thLevel (Splice _) = 0
824 thLevel Comp = 1
825 thLevel (Brack s _) = thLevel s + 1
826
827 ---------------------------
828 -- Arrow-notation context
829 ---------------------------
830
831 {- Note [Escaping the arrow scope]
832 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
833 In arrow notation, a variable bound by a proc (or enclosed let/kappa)
834 is not in scope to the left of an arrow tail (-<) or the head of (|..|).
835 For example
836
837 proc x -> (e1 -< e2)
838
839 Here, x is not in scope in e1, but it is in scope in e2. This can get
840 a bit complicated:
841
842 let x = 3 in
843 proc y -> (proc z -> e1) -< e2
844
845 Here, x and z are in scope in e1, but y is not.
846
847 We implement this by
848 recording the environment when passing a proc (using newArrowScope),
849 and returning to that (using escapeArrowScope) on the left of -< and the
850 head of (|..|).
851
852 All this can be dealt with by the *renamer*. But the type checker needs
853 to be involved too. Example (arrowfail001)
854 class Foo a where foo :: a -> ()
855 data Bar = forall a. Foo a => Bar a
856 get :: Bar -> ()
857 get = proc x -> case x of Bar a -> foo -< a
858 Here the call of 'foo' gives rise to a (Foo a) constraint that should not
859 be captured by the pattern match on 'Bar'. Rather it should join the
860 constraints from further out. So we must capture the constraint bag
861 from further out in the ArrowCtxt that we push inwards.
862 -}
863
864 data ArrowCtxt -- Note [Escaping the arrow scope]
865 = NoArrowCtxt
866 | ArrowCtxt LocalRdrEnv (TcRef WantedConstraints)
867
868
869 ---------------------------
870 -- TcTyThing
871 ---------------------------
872
873 -- | A typecheckable thing available in a local context. Could be
874 -- 'AGlobal' 'TyThing', but also lexically scoped variables, etc.
875 -- See 'TcEnv' for how to retrieve a 'TyThing' given a 'Name'.
876 data TcTyThing
877 = AGlobal TyThing -- Used only in the return type of a lookup
878
879 | ATcId { -- Ids defined in this module; may not be fully zonked
880 tct_id :: TcId,
881 tct_closed :: TopLevelFlag } -- See Note [Bindings with closed types]
882
883 | ATyVar Name TcTyVar -- The type variable to which the lexically scoped type
884 -- variable is bound. We only need the Name
885 -- for error-message purposes; it is the corresponding
886 -- Name in the domain of the envt
887
888 | ATcTyCon TyCon -- Used temporarily, during kind checking, for the
889 -- tycons and clases in this recursive group
890 -- The TyCon is always a TcTyCon. Its kind
891 -- can be a mono-kind or a poly-kind; in TcTyClsDcls see
892 -- Note [Type checking recursive type and class declarations]
893
894 | APromotionErr PromotionErr
895
896 data PromotionErr
897 = TyConPE -- TyCon used in a kind before we are ready
898 -- data T :: T -> * where ...
899 | ClassPE -- Ditto Class
900
901 | FamDataConPE -- Data constructor for a data family
902 -- See Note [AFamDataCon: not promoting data family constructors] in TcRnDriver
903 | PatSynPE -- Pattern synonyms
904 -- See Note [Don't promote pattern synonyms] in TcEnv
905
906 | RecDataConPE -- Data constructor in a recursive loop
907 -- See Note [ARecDataCon: recusion and promoting data constructors] in TcTyClsDecls
908 | NoDataKinds -- -XDataKinds not enabled
909 | NoTypeInTypeTC -- -XTypeInType not enabled (for a tycon)
910 | NoTypeInTypeDC -- -XTypeInType not enabled (for a datacon)
911
912 instance Outputable TcTyThing where -- Debugging only
913 ppr (AGlobal g) = pprTyThing g
914 ppr elt@(ATcId {}) = text "Identifier" <>
915 brackets (ppr (tct_id elt) <> dcolon
916 <> ppr (varType (tct_id elt)) <> comma
917 <+> ppr (tct_closed elt))
918 ppr (ATyVar n tv) = text "Type variable" <+> quotes (ppr n) <+> equals <+> ppr tv
919 ppr (ATcTyCon tc) = text "ATcTyCon" <+> ppr tc
920 ppr (APromotionErr err) = text "APromotionErr" <+> ppr err
921
922 instance Outputable PromotionErr where
923 ppr ClassPE = text "ClassPE"
924 ppr TyConPE = text "TyConPE"
925 ppr PatSynPE = text "PatSynPE"
926 ppr FamDataConPE = text "FamDataConPE"
927 ppr RecDataConPE = text "RecDataConPE"
928 ppr NoDataKinds = text "NoDataKinds"
929 ppr NoTypeInTypeTC = text "NoTypeInTypeTC"
930 ppr NoTypeInTypeDC = text "NoTypeInTypeDC"
931
932 pprTcTyThingCategory :: TcTyThing -> SDoc
933 pprTcTyThingCategory (AGlobal thing) = pprTyThingCategory thing
934 pprTcTyThingCategory (ATyVar {}) = text "Type variable"
935 pprTcTyThingCategory (ATcId {}) = text "Local identifier"
936 pprTcTyThingCategory (ATcTyCon {}) = text "Local tycon"
937 pprTcTyThingCategory (APromotionErr pe) = pprPECategory pe
938
939 pprPECategory :: PromotionErr -> SDoc
940 pprPECategory ClassPE = text "Class"
941 pprPECategory TyConPE = text "Type constructor"
942 pprPECategory PatSynPE = text "Pattern synonym"
943 pprPECategory FamDataConPE = text "Data constructor"
944 pprPECategory RecDataConPE = text "Data constructor"
945 pprPECategory NoDataKinds = text "Data constructor"
946 pprPECategory NoTypeInTypeTC = text "Type constructor"
947 pprPECategory NoTypeInTypeDC = text "Data constructor"
948
949 {- Note [Bindings with closed types]
950 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
951 Consider
952
953 f x = let g ys = map not ys
954 in ...
955
956 Can we generalise 'g' under the OutsideIn algorithm? Yes,
957 because all g's free variables are top-level; that is they themselves
958 have no free type variables, and it is the type variables in the
959 environment that makes things tricky for OutsideIn generalisation.
960
961 Definition:
962 A variable is "closed", and has tct_closed set to TopLevel,
963 iff
964 a) all its free variables are imported, or are let-bound with closed types
965 b) generalisation is not restricted by the monomorphism restriction
966
967 Invariant: a closed variable has no free type variables in its type.
968
969 Under OutsideIn we are free to generalise a closed let-binding.
970 This is an extension compared to the JFP paper on OutsideIn, which
971 used "top-level" as a proxy for "closed". (It's not a good proxy
972 anyway -- the MR can make a top-level binding with a free type
973 variable.)
974
975 Note that:
976 * A top-level binding may not be closed, if it suffers from the MR
977
978 * A nested binding may be closed (eg 'g' in the example we started with)
979 Indeed, that's the point; whether a function is defined at top level
980 or nested is orthogonal to the question of whether or not it is closed
981
982 * A binding may be non-closed because it mentions a lexically scoped
983 *type variable* Eg
984 f :: forall a. blah
985 f x = let g y = ...(y::a)...
986
987 -}
988
989 type ErrCtxt = (Bool, TidyEnv -> TcM (TidyEnv, MsgDoc))
990 -- Monadic so that we have a chance
991 -- to deal with bound type variables just before error
992 -- message construction
993
994 -- Bool: True <=> this is a landmark context; do not
995 -- discard it when trimming for display
996
997 {-
998 ************************************************************************
999 * *
1000 Operations over ImportAvails
1001 * *
1002 ************************************************************************
1003 -}
1004
1005 -- | 'ImportAvails' summarises what was imported from where, irrespective of
1006 -- whether the imported things are actually used or not. It is used:
1007 --
1008 -- * when processing the export list,
1009 --
1010 -- * when constructing usage info for the interface file,
1011 --
1012 -- * to identify the list of directly imported modules for initialisation
1013 -- purposes and for optimised overlap checking of family instances,
1014 --
1015 -- * when figuring out what things are really unused
1016 --
1017 data ImportAvails
1018 = ImportAvails {
1019 imp_mods :: ImportedMods,
1020 -- = ModuleEnv [ImportedModsVal],
1021 -- ^ Domain is all directly-imported modules
1022 --
1023 -- See the documentaion on ImportedModsVal in HscTypes for the
1024 -- meaning of the fields.
1025 --
1026 -- We need a full ModuleEnv rather than a ModuleNameEnv here,
1027 -- because we might be importing modules of the same name from
1028 -- different packages. (currently not the case, but might be in the
1029 -- future).
1030
1031 imp_dep_mods :: ModuleNameEnv (ModuleName, IsBootInterface),
1032 -- ^ Home-package modules needed by the module being compiled
1033 --
1034 -- It doesn't matter whether any of these dependencies
1035 -- are actually /used/ when compiling the module; they
1036 -- are listed if they are below it at all. For
1037 -- example, suppose M imports A which imports X. Then
1038 -- compiling M might not need to consult X.hi, but X
1039 -- is still listed in M's dependencies.
1040
1041 imp_dep_pkgs :: [UnitId],
1042 -- ^ Packages needed by the module being compiled, whether directly,
1043 -- or via other modules in this package, or via modules imported
1044 -- from other packages.
1045
1046 imp_trust_pkgs :: [UnitId],
1047 -- ^ This is strictly a subset of imp_dep_pkgs and records the
1048 -- packages the current module needs to trust for Safe Haskell
1049 -- compilation to succeed. A package is required to be trusted if
1050 -- we are dependent on a trustworthy module in that package.
1051 -- While perhaps making imp_dep_pkgs a tuple of (UnitId, Bool)
1052 -- where True for the bool indicates the package is required to be
1053 -- trusted is the more logical design, doing so complicates a lot
1054 -- of code not concerned with Safe Haskell.
1055 -- See Note [RnNames . Tracking Trust Transitively]
1056
1057 imp_trust_own_pkg :: Bool,
1058 -- ^ Do we require that our own package is trusted?
1059 -- This is to handle efficiently the case where a Safe module imports
1060 -- a Trustworthy module that resides in the same package as it.
1061 -- See Note [RnNames . Trust Own Package]
1062
1063 imp_orphs :: [Module],
1064 -- ^ Orphan modules below us in the import tree (and maybe including
1065 -- us for imported modules)
1066
1067 imp_finsts :: [Module]
1068 -- ^ Family instance modules below us in the import tree (and maybe
1069 -- including us for imported modules)
1070 }
1071
1072 mkModDeps :: [(ModuleName, IsBootInterface)]
1073 -> ModuleNameEnv (ModuleName, IsBootInterface)
1074 mkModDeps deps = foldl add emptyUFM deps
1075 where
1076 add env elt@(m,_) = addToUFM env m elt
1077
1078 emptyImportAvails :: ImportAvails
1079 emptyImportAvails = ImportAvails { imp_mods = emptyModuleEnv,
1080 imp_dep_mods = emptyUFM,
1081 imp_dep_pkgs = [],
1082 imp_trust_pkgs = [],
1083 imp_trust_own_pkg = False,
1084 imp_orphs = [],
1085 imp_finsts = [] }
1086
1087 -- | Union two ImportAvails
1088 --
1089 -- This function is a key part of Import handling, basically
1090 -- for each import we create a separate ImportAvails structure
1091 -- and then union them all together with this function.
1092 plusImportAvails :: ImportAvails -> ImportAvails -> ImportAvails
1093 plusImportAvails
1094 (ImportAvails { imp_mods = mods1,
1095 imp_dep_mods = dmods1, imp_dep_pkgs = dpkgs1,
1096 imp_trust_pkgs = tpkgs1, imp_trust_own_pkg = tself1,
1097 imp_orphs = orphs1, imp_finsts = finsts1 })
1098 (ImportAvails { imp_mods = mods2,
1099 imp_dep_mods = dmods2, imp_dep_pkgs = dpkgs2,
1100 imp_trust_pkgs = tpkgs2, imp_trust_own_pkg = tself2,
1101 imp_orphs = orphs2, imp_finsts = finsts2 })
1102 = ImportAvails { imp_mods = plusModuleEnv_C (++) mods1 mods2,
1103 imp_dep_mods = plusUFM_C plus_mod_dep dmods1 dmods2,
1104 imp_dep_pkgs = dpkgs1 `unionLists` dpkgs2,
1105 imp_trust_pkgs = tpkgs1 `unionLists` tpkgs2,
1106 imp_trust_own_pkg = tself1 || tself2,
1107 imp_orphs = orphs1 `unionLists` orphs2,
1108 imp_finsts = finsts1 `unionLists` finsts2 }
1109 where
1110 plus_mod_dep (m1, boot1) (m2, boot2)
1111 = WARN( not (m1 == m2), (ppr m1 <+> ppr m2) $$ (ppr boot1 <+> ppr boot2) )
1112 -- Check mod-names match
1113 (m1, boot1 && boot2) -- If either side can "see" a non-hi-boot interface, use that
1114
1115 {-
1116 ************************************************************************
1117 * *
1118 \subsection{Where from}
1119 * *
1120 ************************************************************************
1121
1122 The @WhereFrom@ type controls where the renamer looks for an interface file
1123 -}
1124
1125 data WhereFrom
1126 = ImportByUser IsBootInterface -- Ordinary user import (perhaps {-# SOURCE #-})
1127 | ImportBySystem -- Non user import.
1128 | ImportByPlugin -- Importing a plugin;
1129 -- See Note [Care with plugin imports] in LoadIface
1130
1131 instance Outputable WhereFrom where
1132 ppr (ImportByUser is_boot) | is_boot = text "{- SOURCE -}"
1133 | otherwise = empty
1134 ppr ImportBySystem = text "{- SYSTEM -}"
1135 ppr ImportByPlugin = text "{- PLUGIN -}"
1136
1137
1138 {- *********************************************************************
1139 * *
1140 Type signatures
1141 * *
1142 ********************************************************************* -}
1143
1144 type TcSigFun = Name -> Maybe TcSigInfo
1145
1146 data TcSigInfo = TcIdSig TcIdSigInfo
1147 | TcPatSynSig TcPatSynInfo
1148
1149 data TcIdSigInfo
1150 = TISI
1151 { sig_bndr :: TcIdSigBndr
1152
1153 , sig_skols :: [(Name, TcTyVar)]
1154 -- Instantiated type and kind variables SKOLEMS
1155 -- The Name is the Name that the renamer chose;
1156 -- but the TcTyVar may come from instantiating
1157 -- the type and hence have a different unique.
1158 -- No need to keep track of whether they are truly lexically
1159 -- scoped because the renamer has named them uniquely
1160 --
1161 -- For Partial signatures, this list /excludes/ any wildcards
1162 -- the named wildcards scope over the binding, and hence
1163 -- their Names may appear in renamed type signatures
1164 -- in the binding; get them from sig_bndr
1165 -- See Note [Binding scoped type variables]
1166
1167 , sig_theta :: TcThetaType -- Instantiated theta. In the case of a
1168 -- PartialSig, sig_theta does not include
1169 -- the extra-constraints wildcard
1170
1171 , sig_tau :: TcSigmaType -- Instantiated tau
1172 -- See Note [sig_tau may be polymorphic]
1173
1174 , sig_ctxt :: UserTypeCtxt -- In the case of type-class default methods,
1175 -- the Name in the FunSigCtxt is not the same
1176 -- as the TcId; the former is 'op', while the
1177 -- latter is '$dmop' or some such
1178
1179 , sig_loc :: SrcSpan -- Location of the type signature
1180 }
1181
1182 data TcIdSigBndr -- See Note [Complete and partial type signatures]
1183 = CompleteSig -- A complete signature with no wildards,
1184 -- so the complete polymorphic type is known.
1185 TcId -- The polymorphic Id with that type
1186
1187 | PartialSig -- A partial type signature (i.e. includes one or more
1188 -- wildcards). In this case it doesn't make sense to give
1189 -- the polymorphic Id, because we are going to /infer/ its
1190 -- type, so we can't make the polymorphic Id ab-initio
1191 { sig_name :: Name -- Name of the function; used when report wildcards
1192 , sig_hs_ty :: LHsType Name -- The original partial signature
1193 , sig_wcs :: [(Name,TcTyVar)] -- Instantiated wildcard variables (named and anonymous)
1194 -- The Name is what the user wrote, such as '_',
1195 -- including SrcSpan for the error message;
1196 -- The TcTyVar is just an ordinary unification variable
1197 , sig_cts :: Maybe SrcSpan -- Just loc <=> An extra-constraints wildcard was present
1198 } -- at location loc
1199 -- e.g. f :: (Eq a, _) => a -> a
1200
1201 data TcPatSynInfo
1202 = TPSI {
1203 patsig_name :: Name,
1204 patsig_univ_tvs :: [TcTyVar],
1205 patsig_req :: TcThetaType,
1206 patsig_ex_tvs :: [TcTyVar],
1207 patsig_prov :: TcThetaType,
1208 patsig_arg_tys :: [TcSigmaType],
1209 patsig_body_ty :: TcSigmaType
1210 }
1211
1212 findScopedTyVars -- See Note [Binding scoped type variables]
1213 :: TcType -- The Type: its forall'd variables are a superset
1214 -- of the lexically scoped variables
1215 -> [TcTyVar] -- The instantiated forall variables of the TcType
1216 -> [(Name, TcTyVar)] -- In 1-1 correspondence with the instantiated vars
1217 findScopedTyVars sig_ty inst_tvs
1218 = zipWith find sig_tvs inst_tvs
1219 where
1220 find sig_tv inst_tv = (tyVarName sig_tv, inst_tv)
1221 (sig_tvs,_) = tcSplitForAllTys sig_ty
1222
1223 instance Outputable TcSigInfo where
1224 ppr (TcIdSig idsi) = ppr idsi
1225 ppr (TcPatSynSig tpsi) = text "TcPatSynInfo" <+> ppr tpsi
1226
1227 instance Outputable TcIdSigInfo where
1228 ppr (TISI { sig_bndr = bndr, sig_skols = tyvars
1229 , sig_theta = theta, sig_tau = tau })
1230 = ppr (tcIdSigBndrName bndr) <+> dcolon <+>
1231 vcat [ pprSigmaType (mkSpecSigmaTy (map snd tyvars) theta tau)
1232 , ppr (map fst tyvars) ]
1233
1234 instance Outputable TcIdSigBndr where
1235 ppr (CompleteSig f) = text "CompleteSig" <+> ppr f
1236 ppr (PartialSig { sig_name = n }) = text "PartialSig" <+> ppr n
1237
1238 instance Outputable TcPatSynInfo where
1239 ppr (TPSI{ patsig_name = name}) = ppr name
1240
1241 isPartialSig :: TcIdSigInfo -> Bool
1242 isPartialSig (TISI { sig_bndr = PartialSig {} }) = True
1243 isPartialSig _ = False
1244
1245 -- | No signature or a partial signature
1246 noCompleteSig :: Maybe TcSigInfo -> Bool
1247 noCompleteSig (Just (TcIdSig sig)) = isPartialSig sig
1248 noCompleteSig _ = True
1249
1250 tcIdSigBndrName :: TcIdSigBndr -> Name
1251 tcIdSigBndrName (CompleteSig id) = idName id
1252 tcIdSigBndrName (PartialSig { sig_name = n }) = n
1253
1254 tcSigInfoName :: TcSigInfo -> Name
1255 tcSigInfoName (TcIdSig idsi) = tcIdSigBndrName (sig_bndr idsi)
1256 tcSigInfoName (TcPatSynSig tpsi) = patsig_name tpsi
1257
1258 -- Helper for cases when we know for sure we have a complete type
1259 -- signature, e.g. class methods.
1260 completeIdSigPolyId :: TcIdSigInfo -> TcId
1261 completeIdSigPolyId (TISI { sig_bndr = CompleteSig id }) = id
1262 completeIdSigPolyId _ = panic "completeSigPolyId"
1263
1264 completeIdSigPolyId_maybe :: TcIdSigInfo -> Maybe TcId
1265 completeIdSigPolyId_maybe (TISI { sig_bndr = CompleteSig id }) = Just id
1266 completeIdSigPolyId_maybe _ = Nothing
1267
1268 completeSigPolyId_maybe :: TcSigInfo -> Maybe TcId
1269 completeSigPolyId_maybe (TcIdSig sig) = completeIdSigPolyId_maybe sig
1270 completeSigPolyId_maybe (TcPatSynSig {}) = Nothing
1271
1272 {-
1273 Note [Binding scoped type variables]
1274 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1275 The type variables *brought into lexical scope* by a type signature may
1276 be a subset of the *quantified type variables* of the signatures, for two reasons:
1277
1278 * With kind polymorphism a signature like
1279 f :: forall f a. f a -> f a
1280 may actually give rise to
1281 f :: forall k. forall (f::k -> *) (a:k). f a -> f a
1282 So the sig_tvs will be [k,f,a], but only f,a are scoped.
1283 NB: the scoped ones are not necessarily the *inital* ones!
1284
1285 * Even aside from kind polymorphism, there may be more instantiated
1286 type variables than lexically-scoped ones. For example:
1287 type T a = forall b. b -> (a,b)
1288 f :: forall c. T c
1289 Here, the signature for f will have one scoped type variable, c,
1290 but two instantiated type variables, c' and b'.
1291
1292 The function findScopedTyVars takes
1293 * hs_ty: the original HsForAllTy
1294 * sig_ty: the corresponding Type (which is guaranteed to use the same Names
1295 as the HsForAllTy)
1296 * inst_tvs: the skolems instantiated from the forall's in sig_ty
1297 It returns a [(Maybe Name, TcTyVar)], in 1-1 correspondence with inst_tvs
1298 but with a (Just n) for the lexically scoped name of each in-scope tyvar.
1299
1300 Note [sig_tau may be polymorphic]
1301 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1302 Note that "sig_tau" might actually be a polymorphic type,
1303 if the original function had a signature like
1304 forall a. Eq a => forall b. Ord b => ....
1305 But that's ok: tcMatchesFun (called by tcRhs) can deal with that
1306 It happens, too! See Note [Polymorphic methods] in TcClassDcl.
1307
1308 Note [Existential check]
1309 ~~~~~~~~~~~~~~~~~~~~~~~~
1310 Lazy patterns can't bind existentials. They arise in two ways:
1311 * Let bindings let { C a b = e } in b
1312 * Twiddle patterns f ~(C a b) = e
1313 The pe_lazy field of PatEnv says whether we are inside a lazy
1314 pattern (perhaps deeply)
1315
1316 If we aren't inside a lazy pattern then we can bind existentials,
1317 but we need to be careful about "extra" tyvars. Consider
1318 (\C x -> d) : pat_ty -> res_ty
1319 When looking for existential escape we must check that the existential
1320 bound by C don't unify with the free variables of pat_ty, OR res_ty
1321 (or of course the environment). Hence we need to keep track of the
1322 res_ty free vars.
1323
1324 Note [Complete and partial type signatures]
1325 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1326 A type signature is partial when it contains one or more wildcards
1327 (= type holes). The wildcard can either be:
1328 * A (type) wildcard occurring in sig_theta or sig_tau. These are
1329 stored in sig_wcs.
1330 f :: Bool -> _
1331 g :: Eq _a => _a -> _a -> Bool
1332 * Or an extra-constraints wildcard, stored in sig_cts:
1333 h :: (Num a, _) => a -> a
1334
1335 A type signature is a complete type signature when there are no
1336 wildcards in the type signature, i.e. iff sig_wcs is empty and
1337 sig_extra_cts is Nothing. -}
1338
1339 {-
1340 ************************************************************************
1341 * *
1342 * Canonical constraints *
1343 * *
1344 * These are the constraints the low-level simplifier works with *
1345 * *
1346 ************************************************************************
1347 -}
1348
1349 -- The syntax of xi types:
1350 -- xi ::= a | T xis | xis -> xis | ... | forall a. tau
1351 -- Two important notes:
1352 -- (i) No type families, unless we are under a ForAll
1353 -- (ii) Note that xi types can contain unexpanded type synonyms;
1354 -- however, the (transitive) expansions of those type synonyms
1355 -- will not contain any type functions, unless we are under a ForAll.
1356 -- We enforce the structure of Xi types when we flatten (TcCanonical)
1357
1358 type Xi = Type -- In many comments, "xi" ranges over Xi
1359
1360 type Cts = Bag Ct
1361
1362 data Ct
1363 -- Atomic canonical constraints
1364 = CDictCan { -- e.g. Num xi
1365 cc_ev :: CtEvidence, -- See Note [Ct/evidence invariant]
1366 cc_class :: Class,
1367 cc_tyargs :: [Xi], -- cc_tyargs are function-free, hence Xi
1368 cc_pend_sc :: Bool -- True <=> (a) cc_class has superclasses
1369 -- (b) we have not (yet) added those
1370 -- superclasses as Givens
1371 -- NB: cc_pend_sc is used for G/W/D. For W/D the reason
1372 -- we need superclasses is to expose possible improvement
1373 -- via fundeps
1374 }
1375
1376 | CIrredEvCan { -- These stand for yet-unusable predicates
1377 cc_ev :: CtEvidence -- See Note [Ct/evidence invariant]
1378 -- The ctev_pred of the evidence is
1379 -- of form (tv xi1 xi2 ... xin)
1380 -- or (tv1 ~ ty2) where the CTyEqCan kind invariant fails
1381 -- or (F tys ~ ty) where the CFunEqCan kind invariant fails
1382 -- See Note [CIrredEvCan constraints]
1383 }
1384
1385 | CTyEqCan { -- tv ~ rhs
1386 -- Invariants:
1387 -- * See Note [Applying the inert substitution] in TcFlatten
1388 -- * tv not in tvs(rhs) (occurs check)
1389 -- * If tv is a TauTv, then rhs has no foralls
1390 -- (this avoids substituting a forall for the tyvar in other types)
1391 -- * typeKind ty `tcEqKind` typeKind tv
1392 -- * rhs may have at most one top-level cast
1393 -- * rhs (perhaps under the one cast) is not necessarily function-free,
1394 -- but it has no top-level function.
1395 -- E.g. a ~ [F b] is fine
1396 -- but a ~ F b is not
1397 -- * If the equality is representational, rhs has no top-level newtype
1398 -- See Note [No top-level newtypes on RHS of representational
1399 -- equalities] in TcCanonical
1400 -- * If rhs (perhaps under the cast) is also a tv, then it is oriented
1401 -- to give best chance of
1402 -- unification happening; eg if rhs is touchable then lhs is too
1403 cc_ev :: CtEvidence, -- See Note [Ct/evidence invariant]
1404 cc_tyvar :: TcTyVar,
1405 cc_rhs :: TcType, -- Not necessarily function-free (hence not Xi)
1406 -- See invariants above
1407 cc_eq_rel :: EqRel
1408 }
1409
1410 | CFunEqCan { -- F xis ~ fsk
1411 -- Invariants:
1412 -- * isTypeFamilyTyCon cc_fun
1413 -- * typeKind (F xis) = tyVarKind fsk
1414 -- * always Nominal role
1415 cc_ev :: CtEvidence, -- See Note [Ct/evidence invariant]
1416 cc_fun :: TyCon, -- A type function
1417
1418 cc_tyargs :: [Xi], -- cc_tyargs are function-free (hence Xi)
1419 -- Either under-saturated or exactly saturated
1420 -- *never* over-saturated (because if so
1421 -- we should have decomposed)
1422
1423 cc_fsk :: TcTyVar -- [Given] always a FlatSkol skolem
1424 -- [Wanted] always a FlatMetaTv unification variable
1425 -- See Note [The flattening story] in TcFlatten
1426 }
1427
1428 | CNonCanonical { -- See Note [NonCanonical Semantics] in TcSMonad
1429 cc_ev :: CtEvidence
1430 }
1431
1432 | CHoleCan { -- See Note [Hole constraints]
1433 -- Treated as an "insoluble" constraint
1434 -- See Note [Insoluble constraints]
1435 cc_ev :: CtEvidence,
1436 cc_occ :: OccName, -- The name of this hole
1437 cc_hole :: HoleSort -- The sort of this hole (expr, type, ...)
1438 }
1439
1440 -- | Used to indicate which sort of hole we have.
1441 data HoleSort = ExprHole -- ^ A hole in an expression (TypedHoles)
1442 | TypeHole -- ^ A hole in a type (PartialTypeSignatures)
1443
1444 {-
1445 Note [Hole constraints]
1446 ~~~~~~~~~~~~~~~~~~~~~~~
1447 CHoleCan constraints are used for two kinds of holes,
1448 distinguished by cc_hole:
1449
1450 * For holes in expressions
1451 e.g. f x = g _ x
1452
1453 * For holes in type signatures
1454 e.g. f :: _ -> _
1455 f x = [x,True]
1456
1457 Note [CIrredEvCan constraints]
1458 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1459 CIrredEvCan constraints are used for constraints that are "stuck"
1460 - we can't solve them (yet)
1461 - we can't use them to solve other constraints
1462 - but they may become soluble if we substitute for some
1463 of the type variables in the constraint
1464
1465 Example 1: (c Int), where c :: * -> Constraint. We can't do anything
1466 with this yet, but if later c := Num, *then* we can solve it
1467
1468 Example 2: a ~ b, where a :: *, b :: k, where k is a kind variable
1469 We don't want to use this to substitute 'b' for 'a', in case
1470 'k' is subequently unifed with (say) *->*, because then
1471 we'd have ill-kinded types floating about. Rather we want
1472 to defer using the equality altogether until 'k' get resolved.
1473
1474 Note [Ct/evidence invariant]
1475 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1476 If ct :: Ct, then extra fields of 'ct' cache precisely the ctev_pred field
1477 of (cc_ev ct), and is fully rewritten wrt the substitution. Eg for CDictCan,
1478 ctev_pred (cc_ev ct) = (cc_class ct) (cc_tyargs ct)
1479 This holds by construction; look at the unique place where CDictCan is
1480 built (in TcCanonical).
1481
1482 In contrast, the type of the evidence *term* (ccev_evtm or ctev_evar/dest) in
1483 the evidence may *not* be fully zonked; we are careful not to look at it
1484 during constraint solving. See Note [Evidence field of CtEvidence]
1485 -}
1486
1487 mkNonCanonical :: CtEvidence -> Ct
1488 mkNonCanonical ev = CNonCanonical { cc_ev = ev }
1489
1490 mkNonCanonicalCt :: Ct -> Ct
1491 mkNonCanonicalCt ct = CNonCanonical { cc_ev = cc_ev ct }
1492
1493 ctEvidence :: Ct -> CtEvidence
1494 ctEvidence = cc_ev
1495
1496 ctLoc :: Ct -> CtLoc
1497 ctLoc = ctEvLoc . ctEvidence
1498
1499 setCtLoc :: Ct -> CtLoc -> Ct
1500 setCtLoc ct loc = ct { cc_ev = (cc_ev ct) { ctev_loc = loc } }
1501
1502 ctOrigin :: Ct -> CtOrigin
1503 ctOrigin = ctLocOrigin . ctLoc
1504
1505 ctPred :: Ct -> PredType
1506 -- See Note [Ct/evidence invariant]
1507 ctPred ct = ctEvPred (cc_ev ct)
1508
1509 -- | Convert a Wanted to a Derived
1510 toDerivedCt :: Ct -> Ct
1511 toDerivedCt ct
1512 = case ctEvidence ct of
1513 CtWanted { ctev_pred = pred, ctev_loc = loc }
1514 -> ct {cc_ev = CtDerived {ctev_pred = pred, ctev_loc = loc}}
1515
1516 CtDerived {} -> ct
1517 CtGiven {} -> pprPanic "to_derived" (ppr ct)
1518
1519 -- | Makes a new equality predicate with the same role as the given
1520 -- evidence.
1521 mkTcEqPredLikeEv :: CtEvidence -> TcType -> TcType -> TcType
1522 mkTcEqPredLikeEv ev
1523 = case predTypeEqRel pred of
1524 NomEq -> mkPrimEqPred
1525 ReprEq -> mkReprPrimEqPred
1526 where
1527 pred = ctEvPred ev
1528
1529 -- | Get the flavour of the given 'Ct'
1530 ctFlavour :: Ct -> CtFlavour
1531 ctFlavour = ctEvFlavour . ctEvidence
1532
1533 -- | Get the equality relation for the given 'Ct'
1534 ctEqRel :: Ct -> EqRel
1535 ctEqRel = ctEvEqRel . ctEvidence
1536
1537 instance Outputable Ct where
1538 ppr ct = ppr (cc_ev ct) <+> parens pp_sort
1539 where
1540 pp_sort = case ct of
1541 CTyEqCan {} -> text "CTyEqCan"
1542 CFunEqCan {} -> text "CFunEqCan"
1543 CNonCanonical {} -> text "CNonCanonical"
1544 CDictCan { cc_pend_sc = pend_sc }
1545 | pend_sc -> text "CDictCan(psc)"
1546 | otherwise -> text "CDictCan"
1547 CIrredEvCan {} -> text "CIrredEvCan"
1548 CHoleCan { cc_occ = occ } -> text "CHoleCan:" <+> ppr occ
1549
1550 {-
1551 ************************************************************************
1552 * *
1553 Simple functions over evidence variables
1554 * *
1555 ************************************************************************
1556 -}
1557
1558 ---------------- Getting free tyvars -------------------------
1559
1560 -- | Returns free variables of constraints as a non-deterministic set
1561 tyCoVarsOfCt :: Ct -> TcTyCoVarSet
1562 tyCoVarsOfCt = runFVSet . tyCoVarsOfCtAcc
1563
1564 -- | Returns free variables of constraints as a deterministically ordered.
1565 -- list. See Note [Deterministic FV] in FV.
1566 tyCoVarsOfCtList :: Ct -> [TcTyCoVar]
1567 tyCoVarsOfCtList = runFVList . tyCoVarsOfCtAcc
1568
1569 -- | Returns free variables of constraints as a composable FV computation.
1570 -- See Note [Deterministic FV] in FV.
1571 tyCoVarsOfCtAcc :: Ct -> FV
1572 tyCoVarsOfCtAcc (CTyEqCan { cc_tyvar = tv, cc_rhs = xi })
1573 = tyCoVarsOfTypeAcc xi `unionFV` oneVar tv `unionFV` tyCoVarsOfTypeAcc (tyVarKind tv)
1574 tyCoVarsOfCtAcc (CFunEqCan { cc_tyargs = tys, cc_fsk = fsk })
1575 = tyCoVarsOfTypesAcc tys `unionFV` oneVar fsk `unionFV` tyCoVarsOfTypeAcc (tyVarKind fsk)
1576 tyCoVarsOfCtAcc (CDictCan { cc_tyargs = tys }) = tyCoVarsOfTypesAcc tys
1577 tyCoVarsOfCtAcc (CIrredEvCan { cc_ev = ev }) = tyCoVarsOfTypeAcc (ctEvPred ev)
1578 tyCoVarsOfCtAcc (CHoleCan { cc_ev = ev }) = tyCoVarsOfTypeAcc (ctEvPred ev)
1579 tyCoVarsOfCtAcc (CNonCanonical { cc_ev = ev }) = tyCoVarsOfTypeAcc (ctEvPred ev)
1580
1581 -- | Returns free variables of a bag of constraints as a non-deterministic
1582 -- set. See Note [Deterministic FV] in FV.
1583 tyCoVarsOfCts :: Cts -> TcTyCoVarSet
1584 tyCoVarsOfCts = runFVSet . tyCoVarsOfCtsAcc
1585
1586 -- | Returns free variables of a bag of constraints as a deterministically
1587 -- odered list. See Note [Deterministic FV] in FV.
1588 tyCoVarsOfCtsList :: Cts -> [TcTyCoVar]
1589 tyCoVarsOfCtsList = runFVList . tyCoVarsOfCtsAcc
1590
1591 -- | Returns free variables of a bag of constraints as a composable FV
1592 -- computation. See Note [Deterministic FV] in FV.
1593 tyCoVarsOfCtsAcc :: Cts -> FV
1594 tyCoVarsOfCtsAcc = foldrBag (unionFV . tyCoVarsOfCtAcc) noVars
1595
1596 tyCoVarsOfWC :: WantedConstraints -> TyCoVarSet
1597 -- Only called on *zonked* things, hence no need to worry about flatten-skolems
1598 tyCoVarsOfWC (WC { wc_simple = simple, wc_impl = implic, wc_insol = insol })
1599 = tyCoVarsOfCts simple `unionVarSet`
1600 tyCoVarsOfBag tyCoVarsOfImplic implic `unionVarSet`
1601 tyCoVarsOfCts insol
1602
1603 tyCoVarsOfImplic :: Implication -> TyCoVarSet
1604 -- Only called on *zonked* things, hence no need to worry about flatten-skolems
1605 tyCoVarsOfImplic (Implic { ic_skols = skols
1606 , ic_given = givens, ic_wanted = wanted })
1607 = (tyCoVarsOfWC wanted `unionVarSet` tyCoVarsOfTypes (map evVarPred givens))
1608 `delVarSetList` skols
1609
1610 tyCoVarsOfBag :: (a -> TyCoVarSet) -> Bag a -> TyCoVarSet
1611 tyCoVarsOfBag tvs_of = foldrBag (unionVarSet . tvs_of) emptyVarSet
1612
1613 --------------------------
1614 dropDerivedSimples :: Cts -> Cts
1615 dropDerivedSimples simples = filterBag isWantedCt simples
1616 -- simples are all Wanted or Derived
1617
1618 dropDerivedInsols :: Cts -> Cts
1619 -- See Note [Dropping derived constraints]
1620 dropDerivedInsols insols = filterBag keep insols
1621 where -- insols can include Given
1622 keep ct
1623 | isDerivedCt ct = not (isDroppableDerivedLoc (ctLoc ct))
1624 | otherwise = True
1625
1626 isDroppableDerivedLoc :: CtLoc -> Bool
1627 -- Note [Dropping derived constraints]
1628 isDroppableDerivedLoc loc
1629 = case ctLocOrigin loc of
1630 HoleOrigin {} -> False
1631 KindEqOrigin {} -> False
1632 GivenOrigin {} -> False
1633 FunDepOrigin1 {} -> False
1634 FunDepOrigin2 {} -> False
1635 _ -> True
1636
1637 arisesFromGivens :: Ct -> Bool
1638 arisesFromGivens ct
1639 = case ctEvidence ct of
1640 CtGiven {} -> True
1641 CtWanted {} -> False
1642 CtDerived { ctev_loc = loc } -> from_given loc
1643 where
1644 from_given :: CtLoc -> Bool
1645 from_given loc = from_given_origin (ctLocOrigin loc)
1646
1647 from_given_origin :: CtOrigin -> Bool
1648 from_given_origin (GivenOrigin {}) = True
1649 from_given_origin (FunDepOrigin1 _ l1 _ l2) = from_given l1 && from_given l2
1650 from_given_origin (FunDepOrigin2 _ o1 _ _) = from_given_origin o1
1651 from_given_origin _ = False
1652
1653 {- Note [Dropping derived constraints]
1654 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1655 In general we discard derived constraints at the end of constraint solving;
1656 see dropDerivedWC. For example
1657
1658 * If we have an unsolved [W] (Ord a), we don't want to complain about
1659 an unsolved [D] (Eq a) as well.
1660
1661 * If we have [W] a ~ Int, [W] a ~ Bool, improvement will generate
1662 [D] Int ~ Bool, and we don't want to report that because it's incomprehensible.
1663 That is why we don't rewrite wanteds with wanteds!
1664
1665 But (tiresomely) we do keep *some* Derived insolubles:
1666
1667 * Insoluble kind equalities (e.g. [D] * ~ (* -> *)) may arise from
1668 a type equality a ~ Int#, say. In future they'll be Wanted, not Derived,
1669 but at the moment they are Derived.
1670
1671 * Insoluble derived equalities (e.g. [D] Int ~ Bool) may arise from
1672 functional dependency interactions, either between Givens or
1673 Wanteds. It seems sensible to retain these:
1674 - For Givens they reflect unreachable code
1675 - For Wanteds it is arguably better to get a fundep error than
1676 a no-instance error (Trac #9612)
1677
1678 * Type holes are derived constraints because they have no evidence
1679 and we want to keep them so we get the error report
1680
1681 Moreover, we keep *all* derived insolubles under some circumstances:
1682
1683 * They are looked at by simplifyInfer, to decide whether to
1684 generalise. Example: [W] a ~ Int, [W] a ~ Bool
1685 We get [D] Int ~ Bool, and indeed the constraints are insoluble,
1686 and we want simplifyInfer to see that, even though we don't
1687 ultimately want to generate an (inexplicable) error message from
1688
1689 To distinguish these cases we use the CtOrigin.
1690
1691
1692 ************************************************************************
1693 * *
1694 CtEvidence
1695 The "flavor" of a canonical constraint
1696 * *
1697 ************************************************************************
1698 -}
1699
1700 isWantedCt :: Ct -> Bool
1701 isWantedCt = isWanted . cc_ev
1702
1703 isGivenCt :: Ct -> Bool
1704 isGivenCt = isGiven . cc_ev
1705
1706 isDerivedCt :: Ct -> Bool
1707 isDerivedCt = isDerived . cc_ev
1708
1709 isCTyEqCan :: Ct -> Bool
1710 isCTyEqCan (CTyEqCan {}) = True
1711 isCTyEqCan (CFunEqCan {}) = False
1712 isCTyEqCan _ = False
1713
1714 isCDictCan_Maybe :: Ct -> Maybe Class
1715 isCDictCan_Maybe (CDictCan {cc_class = cls }) = Just cls
1716 isCDictCan_Maybe _ = Nothing
1717
1718 isCIrredEvCan :: Ct -> Bool
1719 isCIrredEvCan (CIrredEvCan {}) = True
1720 isCIrredEvCan _ = False
1721
1722 isCFunEqCan_maybe :: Ct -> Maybe (TyCon, [Type])
1723 isCFunEqCan_maybe (CFunEqCan { cc_fun = tc, cc_tyargs = xis }) = Just (tc, xis)
1724 isCFunEqCan_maybe _ = Nothing
1725
1726 isCFunEqCan :: Ct -> Bool
1727 isCFunEqCan (CFunEqCan {}) = True
1728 isCFunEqCan _ = False
1729
1730 isCNonCanonical :: Ct -> Bool
1731 isCNonCanonical (CNonCanonical {}) = True
1732 isCNonCanonical _ = False
1733
1734 isHoleCt:: Ct -> Bool
1735 isHoleCt (CHoleCan {}) = True
1736 isHoleCt _ = False
1737
1738 isOutOfScopeCt :: Ct -> Bool
1739 -- A Hole that does not have a leading underscore is
1740 -- simply an out-of-scope variable, and we treat that
1741 -- a bit differently when it comes to error reporting
1742 isOutOfScopeCt (CHoleCan { cc_occ = occ }) = not (startsWithUnderscore occ)
1743 isOutOfScopeCt _ = False
1744
1745 isExprHoleCt :: Ct -> Bool
1746 isExprHoleCt (CHoleCan { cc_hole = ExprHole }) = True
1747 isExprHoleCt _ = False
1748
1749 isTypeHoleCt :: Ct -> Bool
1750 isTypeHoleCt (CHoleCan { cc_hole = TypeHole }) = True
1751 isTypeHoleCt _ = False
1752
1753 -- | The following constraints are considered to be a custom type error:
1754 -- 1. TypeError msg a b c
1755 -- 2. TypeError msg a b c ~ Something (and the other way around)
1756 -- 4. C (TypeError msg a b c) (for any parameter of class constraint)
1757 getUserTypeErrorMsg :: Ct -> Maybe Type
1758 getUserTypeErrorMsg ct
1759 | Just (_,t1,t2) <- getEqPredTys_maybe ctT = oneOf [t1,t2]
1760 | Just (_,ts) <- getClassPredTys_maybe ctT = oneOf ts
1761 | otherwise = userTypeError_maybe ctT
1762 where
1763 ctT = ctPred ct
1764 oneOf xs = msum (map userTypeError_maybe xs)
1765
1766 isUserTypeErrorCt :: Ct -> Bool
1767 isUserTypeErrorCt ct = case getUserTypeErrorMsg ct of
1768 Just _ -> True
1769 _ -> False
1770
1771 isPendingScDict :: Ct -> Maybe Ct
1772 -- Says whether cc_pend_sc is True, AND if so flips the flag
1773 isPendingScDict ct@(CDictCan { cc_pend_sc = True })
1774 = Just (ct { cc_pend_sc = False })
1775 isPendingScDict _ = Nothing
1776
1777 -- | Are we looking at an Implicit CallStack
1778 -- (i.e. @IP "name" CallStack@)?
1779 --
1780 -- If so, returns @Just "name"@.
1781 isCallStackDict :: Class -> [Type] -> Maybe FastString
1782 isCallStackDict cls tys
1783 | cls `hasKey` ipClassKey
1784 , [ip_name_ty, ty] <- tys
1785 , Just (tc, _) <- splitTyConApp_maybe ty
1786 , tc `hasKey` callStackTyConKey
1787 = isStrLitTy ip_name_ty
1788 isCallStackDict _ _
1789 = Nothing
1790
1791 superClassesMightHelp :: Ct -> Bool
1792 -- ^ True if taking superclasses of givens, or of wanteds (to perhaps
1793 -- expose more equalities or functional dependencies) might help to
1794 -- solve this constraint. See Note [When superclases help]
1795 superClassesMightHelp ct
1796 = isWantedCt ct && not (is_ip ct)
1797 where
1798 is_ip (CDictCan { cc_class = cls }) = isIPClass cls
1799 is_ip _ = False
1800
1801 {- Note [When superclasses help]
1802 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1803 First read Note [The superclass story] in TcCanonical.
1804
1805 We expand superclasses and iterate only if there is at unsolved wanted
1806 for which expansion of superclasses (e.g. from given constraints)
1807 might actually help. The function superClassesMightHelp tells if
1808 doing this superclass expansion might help solve this constraint.
1809 Note that
1810
1811 * Superclasses help only for Wanted constraints. Derived constraints
1812 are not really "unsolved" and we certainly don't want them to
1813 trigger superclass expansion. This was a good part of the loop
1814 in Trac #11523
1815
1816 * Even for Wanted constraints, we say "no" for implicit paramters.
1817 we have [W] ?x::ty, expanding superclasses won't help:
1818 - Superclasses can't be implicit parameters
1819 - If we have a [G] ?x:ty2, then we'll have another unsolved
1820 [D] ty ~ ty2 (from the functional dependency)
1821 which will trigger superclass expansion.
1822
1823 It's a bit of a special case, but it's easy to do. The runtime cost
1824 is low because the unsolved set is usually empty anyway (errors
1825 aside), and the first non-imlicit-parameter will terminate the search.
1826
1827 The special case is worth it (Trac #11480, comment:2) because it
1828 applies to CallStack constraints, which aren't type errors. If we have
1829 f :: (C a) => blah
1830 f x = ...undefined...
1831 we'll get a CallStack constraint. If that's the only unsolved
1832 constraint it'll eventually be solved by defaulting. So we don't
1833 want to emit warnings about hitting the simplifier's iteration
1834 limit. A CallStack constraint really isn't an unsolved
1835 constraint; it can always be solved by defaulting.
1836 -}
1837
1838 singleCt :: Ct -> Cts
1839 singleCt = unitBag
1840
1841 andCts :: Cts -> Cts -> Cts
1842 andCts = unionBags
1843
1844 listToCts :: [Ct] -> Cts
1845 listToCts = listToBag
1846
1847 ctsElts :: Cts -> [Ct]
1848 ctsElts = bagToList
1849
1850 consCts :: Ct -> Cts -> Cts
1851 consCts = consBag
1852
1853 snocCts :: Cts -> Ct -> Cts
1854 snocCts = snocBag
1855
1856 extendCtsList :: Cts -> [Ct] -> Cts
1857 extendCtsList cts xs | null xs = cts
1858 | otherwise = cts `unionBags` listToBag xs
1859
1860 andManyCts :: [Cts] -> Cts
1861 andManyCts = unionManyBags
1862
1863 emptyCts :: Cts
1864 emptyCts = emptyBag
1865
1866 isEmptyCts :: Cts -> Bool
1867 isEmptyCts = isEmptyBag
1868
1869 pprCts :: Cts -> SDoc
1870 pprCts cts = vcat (map ppr (bagToList cts))
1871
1872 {-
1873 ************************************************************************
1874 * *
1875 Wanted constraints
1876 These are forced to be in TcRnTypes because
1877 TcLclEnv mentions WantedConstraints
1878 WantedConstraint mentions CtLoc
1879 CtLoc mentions ErrCtxt
1880 ErrCtxt mentions TcM
1881 * *
1882 v%************************************************************************
1883 -}
1884
1885 data WantedConstraints
1886 = WC { wc_simple :: Cts -- Unsolved constraints, all wanted
1887 , wc_impl :: Bag Implication
1888 , wc_insol :: Cts -- Insoluble constraints, can be
1889 -- wanted, given, or derived
1890 -- See Note [Insoluble constraints]
1891 }
1892
1893 emptyWC :: WantedConstraints
1894 emptyWC = WC { wc_simple = emptyBag, wc_impl = emptyBag, wc_insol = emptyBag }
1895
1896 mkSimpleWC :: [CtEvidence] -> WantedConstraints
1897 mkSimpleWC cts
1898 = WC { wc_simple = listToBag (map mkNonCanonical cts)
1899 , wc_impl = emptyBag
1900 , wc_insol = emptyBag }
1901
1902 mkImplicWC :: Bag Implication -> WantedConstraints
1903 mkImplicWC implic
1904 = WC { wc_simple = emptyBag, wc_impl = implic, wc_insol = emptyBag }
1905
1906 isEmptyWC :: WantedConstraints -> Bool
1907 isEmptyWC (WC { wc_simple = f, wc_impl = i, wc_insol = n })
1908 = isEmptyBag f && isEmptyBag i && isEmptyBag n
1909
1910 andWC :: WantedConstraints -> WantedConstraints -> WantedConstraints
1911 andWC (WC { wc_simple = f1, wc_impl = i1, wc_insol = n1 })
1912 (WC { wc_simple = f2, wc_impl = i2, wc_insol = n2 })
1913 = WC { wc_simple = f1 `unionBags` f2
1914 , wc_impl = i1 `unionBags` i2
1915 , wc_insol = n1 `unionBags` n2 }
1916
1917 unionsWC :: [WantedConstraints] -> WantedConstraints
1918 unionsWC = foldr andWC emptyWC
1919
1920 -- | Convert all Wanteds into Deriveds (ignoring insolubles)
1921 toDerivedWC :: WantedConstraints -> WantedConstraints
1922 toDerivedWC wc@(WC { wc_simple = simples, wc_impl = implics })
1923 = wc { wc_simple = mapBag toDerivedCt simples
1924 , wc_impl = mapBag to_derived_implic implics }
1925 where
1926 to_derived_implic implic@(Implic { ic_wanted = inner_wanted })
1927 = implic { ic_wanted = toDerivedWC inner_wanted }
1928
1929
1930 addSimples :: WantedConstraints -> Bag Ct -> WantedConstraints
1931 addSimples wc cts
1932 = wc { wc_simple = wc_simple wc `unionBags` cts }
1933 -- Consider: Put the new constraints at the front, so they get solved first
1934
1935 addImplics :: WantedConstraints -> Bag Implication -> WantedConstraints
1936 addImplics wc implic = wc { wc_impl = wc_impl wc `unionBags` implic }
1937
1938 addInsols :: WantedConstraints -> Bag Ct -> WantedConstraints
1939 addInsols wc cts
1940 = wc { wc_insol = wc_insol wc `unionBags` cts }
1941
1942 dropDerivedWC :: WantedConstraints -> WantedConstraints
1943 -- See Note [Dropping derived constraints]
1944 dropDerivedWC wc@(WC { wc_simple = simples, wc_insol = insols })
1945 = wc { wc_simple = dropDerivedSimples simples
1946 , wc_insol = dropDerivedInsols insols }
1947 -- The wc_impl implications are already (recursively) filtered
1948
1949 isInsolubleStatus :: ImplicStatus -> Bool
1950 isInsolubleStatus IC_Insoluble = True
1951 isInsolubleStatus _ = False
1952
1953 insolubleImplic :: Implication -> Bool
1954 insolubleImplic ic = isInsolubleStatus (ic_status ic)
1955
1956 insolubleWC :: TcLevel -> WantedConstraints -> Bool
1957 insolubleWC tc_lvl (WC { wc_impl = implics, wc_insol = insols })
1958 = anyBag (trulyInsoluble tc_lvl) insols
1959 || anyBag insolubleImplic implics
1960
1961 trulyInsoluble :: TcLevel -> Ct -> Bool
1962 -- The constraint is in the wc_insol set,
1963 -- but we do not treat as truly isoluble
1964 -- a) type-holes, arising from PartialTypeSignatures,
1965 -- (except out-of-scope variables masquerading as type-holes)
1966 -- Yuk!
1967 trulyInsoluble _tc_lvl insol
1968 | CHoleCan {} <- insol = isOutOfScopeCt insol
1969 | otherwise = True
1970
1971 instance Outputable WantedConstraints where
1972 ppr (WC {wc_simple = s, wc_impl = i, wc_insol = n})
1973 = text "WC" <+> braces (vcat
1974 [ ppr_bag (text "wc_simple") s
1975 , ppr_bag (text "wc_insol") n
1976 , ppr_bag (text "wc_impl") i ])
1977
1978 ppr_bag :: Outputable a => SDoc -> Bag a -> SDoc
1979 ppr_bag doc bag
1980 | isEmptyBag bag = empty
1981 | otherwise = hang (doc <+> equals)
1982 2 (foldrBag (($$) . ppr) empty bag)
1983
1984 {-
1985 ************************************************************************
1986 * *
1987 Implication constraints
1988 * *
1989 ************************************************************************
1990 -}
1991
1992 data Implication
1993 = Implic {
1994 ic_tclvl :: TcLevel, -- TcLevel: unification variables
1995 -- free in the environment
1996
1997 ic_skols :: [TcTyVar], -- Introduced skolems
1998 ic_info :: SkolemInfo, -- See Note [Skolems in an implication]
1999 -- See Note [Shadowing in a constraint]
2000
2001 ic_given :: [EvVar], -- Given evidence variables
2002 -- (order does not matter)
2003 -- See Invariant (GivenInv) in TcType
2004
2005 ic_no_eqs :: Bool, -- True <=> ic_givens have no equalities, for sure
2006 -- False <=> ic_givens might have equalities
2007
2008 ic_env :: TcLclEnv, -- Gives the source location and error context
2009 -- for the implication, and hence for all the
2010 -- given evidence variables
2011
2012 ic_wanted :: WantedConstraints, -- The wanted
2013
2014 ic_binds :: Maybe EvBindsVar,
2015 -- Points to the place to fill in the
2016 -- abstraction and bindings.
2017 -- is Nothing if we can't deal with
2018 -- non-equality constraints here
2019 -- (this happens in TcS.deferTcSForAllEq)
2020
2021 ic_status :: ImplicStatus
2022 }
2023
2024 data ImplicStatus
2025 = IC_Solved -- All wanteds in the tree are solved, all the way down
2026 { ics_need :: VarSet -- Evidence variables needed by this implication
2027 , ics_dead :: [EvVar] } -- Subset of ic_given that are not needed
2028 -- See Note [Tracking redundant constraints] in TcSimplify
2029
2030 | IC_Insoluble -- At least one insoluble constraint in the tree
2031
2032 | IC_Unsolved -- Neither of the above; might go either way
2033
2034 instance Outputable Implication where
2035 ppr (Implic { ic_tclvl = tclvl, ic_skols = skols
2036 , ic_given = given, ic_no_eqs = no_eqs
2037 , ic_wanted = wanted, ic_status = status
2038 , ic_binds = binds, ic_info = info })
2039 = hang (text "Implic" <+> lbrace)
2040 2 (sep [ text "TcLevel =" <+> ppr tclvl
2041 , text "Skolems =" <+> pprTvBndrs skols
2042 , text "No-eqs =" <+> ppr no_eqs
2043 , text "Status =" <+> ppr status
2044 , hang (text "Given =") 2 (pprEvVars given)
2045 , hang (text "Wanted =") 2 (ppr wanted)
2046 , text "Binds =" <+> ppr binds
2047 , pprSkolInfo info ] <+> rbrace)
2048
2049 instance Outputable ImplicStatus where
2050 ppr IC_Insoluble = text "Insoluble"
2051 ppr IC_Unsolved = text "Unsolved"
2052 ppr (IC_Solved { ics_need = vs, ics_dead = dead })
2053 = text "Solved"
2054 <+> (braces $ vcat [ text "Dead givens =" <+> ppr dead
2055 , text "Needed =" <+> ppr vs ])
2056
2057 {-
2058 Note [Needed evidence variables]
2059 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2060 Th ic_need_evs field holds the free vars of ic_binds, and all the
2061 ic_binds in nested implications.
2062
2063 * Main purpose: if one of the ic_givens is not mentioned in here, it
2064 is redundant.
2065
2066 * solveImplication may drop an implication altogether if it has no
2067 remaining 'wanteds'. But we still track the free vars of its
2068 evidence binds, even though it has now disappeared.
2069
2070 Note [Shadowing in a constraint]
2071 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2072 We assume NO SHADOWING in a constraint. Specifically
2073 * The unification variables are all implicitly quantified at top
2074 level, and are all unique
2075 * The skolem variables bound in ic_skols are all freah when the
2076 implication is created.
2077 So we can safely substitute. For example, if we have
2078 forall a. a~Int => ...(forall b. ...a...)...
2079 we can push the (a~Int) constraint inwards in the "givens" without
2080 worrying that 'b' might clash.
2081
2082 Note [Skolems in an implication]
2083 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2084 The skolems in an implication are not there to perform a skolem escape
2085 check. That happens because all the environment variables are in the
2086 untouchables, and therefore cannot be unified with anything at all,
2087 let alone the skolems.
2088
2089 Instead, ic_skols is used only when considering floating a constraint
2090 outside the implication in TcSimplify.floatEqualities or
2091 TcSimplify.approximateImplications
2092
2093 Note [Insoluble constraints]
2094 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2095 Some of the errors that we get during canonicalization are best
2096 reported when all constraints have been simplified as much as
2097 possible. For instance, assume that during simplification the
2098 following constraints arise:
2099
2100 [Wanted] F alpha ~ uf1
2101 [Wanted] beta ~ uf1 beta
2102
2103 When canonicalizing the wanted (beta ~ uf1 beta), if we eagerly fail
2104 we will simply see a message:
2105 'Can't construct the infinite type beta ~ uf1 beta'
2106 and the user has no idea what the uf1 variable is.
2107
2108 Instead our plan is that we will NOT fail immediately, but:
2109 (1) Record the "frozen" error in the ic_insols field
2110 (2) Isolate the offending constraint from the rest of the inerts
2111 (3) Keep on simplifying/canonicalizing
2112
2113 At the end, we will hopefully have substituted uf1 := F alpha, and we
2114 will be able to report a more informative error:
2115 'Can't construct the infinite type beta ~ F alpha beta'
2116
2117 Insoluble constraints *do* include Derived constraints. For example,
2118 a functional dependency might give rise to [D] Int ~ Bool, and we must
2119 report that. If insolubles did not contain Deriveds, reportErrors would
2120 never see it.
2121
2122
2123 ************************************************************************
2124 * *
2125 Pretty printing
2126 * *
2127 ************************************************************************
2128 -}
2129
2130 pprEvVars :: [EvVar] -> SDoc -- Print with their types
2131 pprEvVars ev_vars = vcat (map pprEvVarWithType ev_vars)
2132
2133 pprEvVarTheta :: [EvVar] -> SDoc
2134 pprEvVarTheta ev_vars = pprTheta (map evVarPred ev_vars)
2135
2136 pprEvVarWithType :: EvVar -> SDoc
2137 pprEvVarWithType v = ppr v <+> dcolon <+> pprType (evVarPred v)
2138
2139 {-
2140 ************************************************************************
2141 * *
2142 CtEvidence
2143 * *
2144 ************************************************************************
2145
2146 Note [Evidence field of CtEvidence]
2147 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2148 During constraint solving we never look at the type of ctev_evar/ctev_dest;
2149 instead we look at the ctev_pred field. The evtm/evar field
2150 may be un-zonked.
2151
2152 Note [Bind new Givens immediately]
2153 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2154 For Givens we make new EvVars and bind them immediately. Two main reasons:
2155 * Gain sharing. E.g. suppose we start with g :: C a b, where
2156 class D a => C a b
2157 class (E a, F a) => D a
2158 If we generate all g's superclasses as separate EvTerms we might
2159 get selD1 (selC1 g) :: E a
2160 selD2 (selC1 g) :: F a
2161 selC1 g :: D a
2162 which we could do more economically as:
2163 g1 :: D a = selC1 g
2164 g2 :: E a = selD1 g1
2165 g3 :: F a = selD2 g1
2166
2167 * For *coercion* evidence we *must* bind each given:
2168 class (a~b) => C a b where ....
2169 f :: C a b => ....
2170 Then in f's Givens we have g:(C a b) and the superclass sc(g,0):a~b.
2171 But that superclass selector can't (yet) appear in a coercion
2172 (see evTermCoercion), so the easy thing is to bind it to an Id.
2173
2174 So a Given has EvVar inside it rather that (as previously) an EvTerm.
2175 -}
2176
2177 -- | A place for type-checking evidence to go after it is generated.
2178 -- Wanted equalities are always HoleDest; other wanteds are always
2179 -- EvVarDest.
2180 data TcEvDest
2181 = EvVarDest EvVar -- ^ bind this var to the evidence
2182 | HoleDest CoercionHole -- ^ fill in this hole with the evidence
2183 -- See Note [Coercion holes] in TyCoRep
2184
2185 data CtEvidence
2186 = CtGiven { ctev_pred :: TcPredType -- See Note [Ct/evidence invariant]
2187 , ctev_evar :: EvVar -- See Note [Evidence field of CtEvidence]
2188 , ctev_loc :: CtLoc }
2189 -- Truly given, not depending on subgoals
2190 -- NB: Spontaneous unifications belong here
2191
2192 | CtWanted { ctev_pred :: TcPredType -- See Note [Ct/evidence invariant]
2193 , ctev_dest :: TcEvDest
2194 , ctev_loc :: CtLoc }
2195 -- Wanted goal
2196
2197 | CtDerived { ctev_pred :: TcPredType
2198 , ctev_loc :: CtLoc }
2199 -- A goal that we don't really have to solve and can't immediately
2200 -- rewrite anything other than a derived (there's no evidence!)
2201 -- but if we do manage to solve it may help in solving other goals.
2202
2203 ctEvPred :: CtEvidence -> TcPredType
2204 -- The predicate of a flavor
2205 ctEvPred = ctev_pred
2206
2207 ctEvLoc :: CtEvidence -> CtLoc
2208 ctEvLoc = ctev_loc
2209
2210 ctEvOrigin :: CtEvidence -> CtOrigin
2211 ctEvOrigin = ctLocOrigin . ctEvLoc
2212
2213 -- | Get the equality relation relevant for a 'CtEvidence'
2214 ctEvEqRel :: CtEvidence -> EqRel
2215 ctEvEqRel = predTypeEqRel . ctEvPred
2216
2217 -- | Get the role relevant for a 'CtEvidence'
2218 ctEvRole :: CtEvidence -> Role
2219 ctEvRole = eqRelRole . ctEvEqRel
2220
2221 ctEvTerm :: CtEvidence -> EvTerm
2222 ctEvTerm ev@(CtWanted { ctev_dest = HoleDest _ }) = EvCoercion $ ctEvCoercion ev
2223 ctEvTerm ev = EvId (ctEvId ev)
2224
2225 ctEvCoercion :: CtEvidence -> Coercion
2226 ctEvCoercion ev@(CtWanted { ctev_dest = HoleDest hole, ctev_pred = pred })
2227 = case getEqPredTys_maybe pred of
2228 Just (role, ty1, ty2) -> mkHoleCo hole role ty1 ty2
2229 _ -> pprPanic "ctEvTerm" (ppr ev)
2230 ctEvCoercion (CtGiven { ctev_evar = ev_id }) = mkTcCoVarCo ev_id
2231 ctEvCoercion ev = pprPanic "ctEvCoercion" (ppr ev)
2232
2233 ctEvId :: CtEvidence -> TcId
2234 ctEvId (CtWanted { ctev_dest = EvVarDest ev }) = ev
2235 ctEvId (CtGiven { ctev_evar = ev }) = ev
2236 ctEvId ctev = pprPanic "ctEvId:" (ppr ctev)
2237
2238 instance Outputable TcEvDest where
2239 ppr (HoleDest h) = text "hole" <> ppr h
2240 ppr (EvVarDest ev) = ppr ev
2241
2242 instance Outputable CtEvidence where
2243 ppr fl = case fl of
2244 CtGiven {} -> text "[G]" <+> ppr (ctev_evar fl) <+> ppr_pty
2245 CtWanted {} -> text "[W]" <+> ppr (ctev_dest fl) <+> ppr_pty
2246 CtDerived {} -> text "[D]" <+> text "_" <+> ppr_pty
2247 where ppr_pty = dcolon <+> ppr (ctEvPred fl)
2248
2249 isWanted :: CtEvidence -> Bool
2250 isWanted (CtWanted {}) = True
2251 isWanted _ = False
2252
2253 isGiven :: CtEvidence -> Bool
2254 isGiven (CtGiven {}) = True
2255 isGiven _ = False
2256
2257 isDerived :: CtEvidence -> Bool
2258 isDerived (CtDerived {}) = True
2259 isDerived _ = False
2260
2261 {-
2262 %************************************************************************
2263 %* *
2264 CtFlavour
2265 %* *
2266 %************************************************************************
2267
2268 Just an enum type that tracks whether a constraint is wanted, derived,
2269 or given, when we need to separate that info from the constraint itself.
2270
2271 -}
2272
2273 data CtFlavour = Given | Wanted | Derived
2274 deriving Eq
2275
2276 instance Outputable CtFlavour where
2277 ppr Given = text "[G]"
2278 ppr Wanted = text "[W]"
2279 ppr Derived = text "[D]"
2280
2281 ctEvFlavour :: CtEvidence -> CtFlavour
2282 ctEvFlavour (CtWanted {}) = Wanted
2283 ctEvFlavour (CtGiven {}) = Given
2284 ctEvFlavour (CtDerived {}) = Derived
2285
2286 -- | Whether or not one 'Ct' can rewrite another is determined by its
2287 -- flavour and its equality relation. See also
2288 -- Note [Flavours with roles] in TcSMonad
2289 type CtFlavourRole = (CtFlavour, EqRel)
2290
2291 -- | Extract the flavour, role, and boxity from a 'CtEvidence'
2292 ctEvFlavourRole :: CtEvidence -> CtFlavourRole
2293 ctEvFlavourRole ev = (ctEvFlavour ev, ctEvEqRel ev)
2294
2295 -- | Extract the flavour, role, and boxity from a 'Ct'
2296 ctFlavourRole :: Ct -> CtFlavourRole
2297 ctFlavourRole = ctEvFlavourRole . cc_ev
2298
2299 {- Note [eqCanRewrite]
2300 ~~~~~~~~~~~~~~~~~~~
2301 (eqCanRewrite ct1 ct2) holds if the constraint ct1 (a CTyEqCan of form
2302 tv ~ ty) can be used to rewrite ct2. It must satisfy the properties of
2303 a can-rewrite relation, see Definition [Can-rewrite relation] in
2304 TcSMonad.
2305
2306 With the solver handling Coercible constraints like equality constraints,
2307 the rewrite conditions must take role into account, never allowing
2308 a representational equality to rewrite a nominal one.
2309
2310 Note [Wanteds do not rewrite Wanteds]
2311 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2312 We don't allow Wanteds to rewrite Wanteds, because that can give rise
2313 to very confusing type error messages. A good example is Trac #8450.
2314 Here's another
2315 f :: a -> Bool
2316 f x = ( [x,'c'], [x,True] ) `seq` True
2317 Here we get
2318 [W] a ~ Char
2319 [W] a ~ Bool
2320 but we do not want to complain about Bool ~ Char!
2321
2322 Note [Deriveds do rewrite Deriveds]
2323 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2324 However we DO allow Deriveds to rewrite Deriveds, because that's how
2325 improvement works; see Note [The improvement story] in TcInteract.
2326
2327 However, for now at least I'm only letting (Derived,NomEq) rewrite
2328 (Derived,NomEq) and not doing anything for ReprEq. If we have
2329 eqCanRewriteFR (Derived, NomEq) (Derived, _) = True
2330 then we lose property R2 of Definition [Can-rewrite relation]
2331 in TcSMonad
2332 R2. If f1 >= f, and f2 >= f,
2333 then either f1 >= f2 or f2 >= f1
2334 Consider f1 = (Given, ReprEq)
2335 f2 = (Derived, NomEq)
2336 f = (Derived, ReprEq)
2337
2338 I thought maybe we could never get Derived ReprEq constraints, but
2339 we can; straight from the Wanteds during improvment. And from a Derived
2340 ReprEq we could conceivably get a Derived NomEq improvment (by decomposing
2341 a type constructor with Nomninal role), and hence unify.
2342
2343 Note [funEqCanDischarge]
2344 ~~~~~~~~~~~~~~~~~~~~~~~~~
2345 Suppose we have two CFunEqCans with the same LHS:
2346 (x1:F ts ~ f1) `funEqCanDischarge` (x2:F ts ~ f2)
2347 Can we drop x2 in favour of x1, either unifying
2348 f2 (if it's a flatten meta-var) or adding a new Given
2349 (f1 ~ f2), if x2 is a Given?
2350
2351 Answer: yes if funEqCanDischarge is true.
2352
2353 Note [eqCanDischarge]
2354 ~~~~~~~~~~~~~~~~~~~~~
2355 Suppose we have two identicla equality constraints
2356 (i.e. both LHS and RHS are the same)
2357 (x1:s~t) `eqCanDischarge` (xs:s~t)
2358 Can we just drop x2 in favour of x1?
2359
2360 Answer: yes if eqCanDischarge is true.
2361
2362 Note that we do /not/ allow Wanted to discharge Derived.
2363 We must keep both. Why? Because the Derived may rewrite
2364 other Deriveds in the model whereas the Wanted cannot.
2365
2366 However a Wanted can certainly discharge an identical Wanted. So
2367 eqCanDischarge does /not/ define a can-rewrite relation in the
2368 sense of Definition [Can-rewrite relation] in TcSMonad.
2369 -}
2370
2371 -----------------
2372 eqCanRewrite :: CtEvidence -> CtEvidence -> Bool
2373 -- Very important function!
2374 -- See Note [eqCanRewrite]
2375 -- See Note [Wanteds do not rewrite Wanteds]
2376 -- See Note [Deriveds do rewrite Deriveds]
2377 eqCanRewrite ev1 ev2 = eqCanRewriteFR (ctEvFlavourRole ev1)
2378 (ctEvFlavourRole ev2)
2379
2380 eqCanRewriteFR :: CtFlavourRole -> CtFlavourRole -> Bool
2381 eqCanRewriteFR (Given, NomEq) (_, _) = True
2382 eqCanRewriteFR (Given, ReprEq) (_, ReprEq) = True
2383 eqCanRewriteFR (Derived, NomEq) (Derived, NomEq) = True
2384 eqCanRewriteFR _ _ = False
2385
2386 -----------------
2387 funEqCanDischarge :: CtEvidence -> CtEvidence -> Bool
2388 -- See Note [funEqCanDischarge]
2389 funEqCanDischarge ev1 ev2 = funEqCanDischargeFR (ctEvFlavourRole ev1)
2390 (ctEvFlavourRole ev2)
2391
2392 funEqCanDischargeFR :: CtFlavourRole -> CtFlavourRole -> Bool
2393 funEqCanDischargeFR (_, ReprEq) (_, NomEq) = False
2394 funEqCanDischargeFR (Given, _) _ = True
2395 funEqCanDischargeFR (Wanted, _) (Wanted, _) = True
2396 funEqCanDischargeFR (Wanted, _) (Derived, _) = True
2397 funEqCanDischargeFR (Derived, _) (Derived, _) = True
2398 funEqCanDischargeFR _ _ = False
2399
2400 -----------------
2401 eqCanDischarge :: CtEvidence -> CtEvidence -> Bool
2402 -- See Note [eqCanDischarge]
2403 eqCanDischarge ev1 ev2 = eqCanDischargeFR (ctEvFlavourRole ev1)
2404 (ctEvFlavourRole ev2)
2405 eqCanDischargeFR :: CtFlavourRole -> CtFlavourRole -> Bool
2406 eqCanDischargeFR (_, ReprEq) (_, NomEq) = False
2407 eqCanDischargeFR (Given, _) (Given,_) = True
2408 eqCanDischargeFR (Wanted, _) (Wanted, _) = True
2409 eqCanDischargeFR (Derived, _) (Derived, _) = True
2410 eqCanDischargeFR _ _ = False
2411
2412 {-
2413 ************************************************************************
2414 * *
2415 SubGoalDepth
2416 * *
2417 ************************************************************************
2418
2419 Note [SubGoalDepth]
2420 ~~~~~~~~~~~~~~~~~~~
2421 The 'SubGoalDepth' takes care of stopping the constraint solver from looping.
2422
2423 The counter starts at zero and increases. It includes dictionary constraints,
2424 equality simplification, and type family reduction. (Why combine these? Because
2425 it's actually quite easy to mistake one for another, in sufficiently involved
2426 scenarios, like ConstraintKinds.)
2427
2428 The flag -fcontext-stack=n (not very well named!) fixes the maximium
2429 level.
2430
2431 * The counter includes the depth of type class instance declarations. Example:
2432 [W] d{7} : Eq [Int]
2433 That is d's dictionary-constraint depth is 7. If we use the instance
2434 $dfEqList :: Eq a => Eq [a]
2435 to simplify it, we get
2436 d{7} = $dfEqList d'{8}
2437 where d'{8} : Eq Int, and d' has depth 8.
2438
2439 For civilised (decidable) instance declarations, each increase of
2440 depth removes a type constructor from the type, so the depth never
2441 gets big; i.e. is bounded by the structural depth of the type.
2442
2443 * The counter also increments when resolving
2444 equalities involving type functions. Example:
2445 Assume we have a wanted at depth 7:
2446 [W] d{7} : F () ~ a
2447 If thre is an type function equation "F () = Int", this would be rewritten to
2448 [W] d{8} : Int ~ a
2449 and remembered as having depth 8.
2450
2451 Again, without UndecidableInstances, this counter is bounded, but without it
2452 can resolve things ad infinitum. Hence there is a maximum level.
2453
2454 * Lastly, every time an equality is rewritten, the counter increases. Again,
2455 rewriting an equality constraint normally makes progress, but it's possible
2456 the "progress" is just the reduction of an infinitely-reducing type family.
2457 Hence we need to track the rewrites.
2458
2459 When compiling a program requires a greater depth, then GHC recommends turning
2460 off this check entirely by setting -freduction-depth=0. This is because the
2461 exact number that works is highly variable, and is likely to change even between
2462 minor releases. Because this check is solely to prevent infinite compilation
2463 times, it seems safe to disable it when a user has ascertained that their program
2464 doesn't loop at the type level.
2465
2466 -}
2467
2468 -- | See Note [SubGoalDepth]
2469 newtype SubGoalDepth = SubGoalDepth Int
2470 deriving (Eq, Ord, Outputable)
2471
2472 initialSubGoalDepth :: SubGoalDepth
2473 initialSubGoalDepth = SubGoalDepth 0
2474
2475 bumpSubGoalDepth :: SubGoalDepth -> SubGoalDepth
2476 bumpSubGoalDepth (SubGoalDepth n) = SubGoalDepth (n + 1)
2477
2478 subGoalDepthExceeded :: DynFlags -> SubGoalDepth -> Bool
2479 subGoalDepthExceeded dflags (SubGoalDepth d)
2480 = mkIntWithInf d > reductionDepth dflags
2481
2482 {-
2483 ************************************************************************
2484 * *
2485 CtLoc
2486 * *
2487 ************************************************************************
2488
2489 The 'CtLoc' gives information about where a constraint came from.
2490 This is important for decent error message reporting because
2491 dictionaries don't appear in the original source code.
2492 type will evolve...
2493 -}
2494
2495 data CtLoc = CtLoc { ctl_origin :: CtOrigin
2496 , ctl_env :: TcLclEnv
2497 , ctl_t_or_k :: Maybe TypeOrKind -- OK if we're not sure
2498 , ctl_depth :: !SubGoalDepth }
2499 -- The TcLclEnv includes particularly
2500 -- source location: tcl_loc :: RealSrcSpan
2501 -- context: tcl_ctxt :: [ErrCtxt]
2502 -- binder stack: tcl_bndrs :: TcIdBinderStack
2503 -- level: tcl_tclvl :: TcLevel
2504
2505 mkGivenLoc :: TcLevel -> SkolemInfo -> TcLclEnv -> CtLoc
2506 mkGivenLoc tclvl skol_info env
2507 = CtLoc { ctl_origin = GivenOrigin skol_info
2508 , ctl_env = env { tcl_tclvl = tclvl }
2509 , ctl_t_or_k = Nothing -- this only matters for error msgs
2510 , ctl_depth = initialSubGoalDepth }
2511
2512 mkKindLoc :: TcType -> TcType -- original *types* being compared
2513 -> CtLoc -> CtLoc
2514 mkKindLoc s1 s2 loc = setCtLocOrigin (toKindLoc loc)
2515 (KindEqOrigin s1 (Just s2) (ctLocOrigin loc)
2516 (ctLocTypeOrKind_maybe loc))
2517
2518 -- | Take a CtLoc and moves it to the kind level
2519 toKindLoc :: CtLoc -> CtLoc
2520 toKindLoc loc = loc { ctl_t_or_k = Just KindLevel }
2521
2522 ctLocEnv :: CtLoc -> TcLclEnv
2523 ctLocEnv = ctl_env
2524
2525 ctLocLevel :: CtLoc -> TcLevel
2526 ctLocLevel loc = tcl_tclvl (ctLocEnv loc)
2527
2528 ctLocDepth :: CtLoc -> SubGoalDepth
2529 ctLocDepth = ctl_depth
2530
2531 ctLocOrigin :: CtLoc -> CtOrigin
2532 ctLocOrigin = ctl_origin
2533
2534 ctLocSpan :: CtLoc -> RealSrcSpan
2535 ctLocSpan (CtLoc { ctl_env = lcl}) = tcl_loc lcl
2536
2537 ctLocTypeOrKind_maybe :: CtLoc -> Maybe TypeOrKind
2538 ctLocTypeOrKind_maybe = ctl_t_or_k
2539
2540 setCtLocSpan :: CtLoc -> RealSrcSpan -> CtLoc
2541 setCtLocSpan ctl@(CtLoc { ctl_env = lcl }) loc = setCtLocEnv ctl (lcl { tcl_loc = loc })
2542
2543 bumpCtLocDepth :: CtLoc -> CtLoc
2544 bumpCtLocDepth loc@(CtLoc { ctl_depth = d }) = loc { ctl_depth = bumpSubGoalDepth d }
2545
2546 setCtLocOrigin :: CtLoc -> CtOrigin -> CtLoc
2547 setCtLocOrigin ctl orig = ctl { ctl_origin = orig }
2548
2549 setCtLocEnv :: CtLoc -> TcLclEnv -> CtLoc
2550 setCtLocEnv ctl env = ctl { ctl_env = env }
2551
2552 pushErrCtxt :: CtOrigin -> ErrCtxt -> CtLoc -> CtLoc
2553 pushErrCtxt o err loc@(CtLoc { ctl_env = lcl })
2554 = loc { ctl_origin = o, ctl_env = lcl { tcl_ctxt = err : tcl_ctxt lcl } }
2555
2556 pushErrCtxtSameOrigin :: ErrCtxt -> CtLoc -> CtLoc
2557 -- Just add information w/o updating the origin!
2558 pushErrCtxtSameOrigin err loc@(CtLoc { ctl_env = lcl })
2559 = loc { ctl_env = lcl { tcl_ctxt = err : tcl_ctxt lcl } }
2560
2561 {-
2562 ************************************************************************
2563 * *
2564 SkolemInfo
2565 * *
2566 ************************************************************************
2567 -}
2568
2569 -- SkolemInfo gives the origin of *given* constraints
2570 -- a) type variables are skolemised
2571 -- b) an implication constraint is generated
2572 data SkolemInfo
2573 = SigSkol UserTypeCtxt -- A skolem that is created by instantiating
2574 ExpType -- a programmer-supplied type signature
2575 -- Location of the binding site is on the TyVar
2576
2577 | ClsSkol Class -- Bound at a class decl
2578
2579 | DerivSkol Type -- Bound by a 'deriving' clause;
2580 -- the type is the instance we are trying to derive
2581
2582 | InstSkol -- Bound at an instance decl
2583 | InstSC TypeSize -- A "given" constraint obtained by superclass selection.
2584 -- If (C ty1 .. tyn) is the largest class from
2585 -- which we made a superclass selection in the chain,
2586 -- then TypeSize = sizeTypes [ty1, .., tyn]
2587 -- See Note [Solving superclass constraints] in TcInstDcls
2588
2589 | DataSkol -- Bound at a data type declaration
2590 | FamInstSkol -- Bound at a family instance decl
2591 | PatSkol -- An existential type variable bound by a pattern for
2592 ConLike -- a data constructor with an existential type.
2593 (HsMatchContext Name)
2594 -- e.g. data T = forall a. Eq a => MkT a
2595 -- f (MkT x) = ...
2596 -- The pattern MkT x will allocate an existential type
2597 -- variable for 'a'.
2598
2599 | ArrowSkol -- An arrow form (see TcArrows)
2600
2601 | IPSkol [HsIPName] -- Binding site of an implicit parameter
2602
2603 | RuleSkol RuleName -- The LHS of a RULE
2604
2605 | InferSkol [(Name,TcType)]
2606 -- We have inferred a type for these (mutually-recursivive)
2607 -- polymorphic Ids, and are now checking that their RHS
2608 -- constraints are satisfied.
2609
2610 | BracketSkol -- Template Haskell bracket
2611
2612 | UnifyForAllSkol -- We are unifying two for-all types
2613 TcType -- The instantiated type *inside* the forall
2614
2615 | UnkSkol -- Unhelpful info (until I improve it)
2616
2617 instance Outputable SkolemInfo where
2618 ppr = pprSkolInfo
2619
2620 pprSkolInfo :: SkolemInfo -> SDoc
2621 -- Complete the sentence "is a rigid type variable bound by..."
2622 pprSkolInfo (SigSkol ctxt ty) = pprSigSkolInfo ctxt ty
2623 pprSkolInfo (IPSkol ips) = text "the implicit-parameter binding" <> plural ips <+> text "for"
2624 <+> pprWithCommas ppr ips
2625 pprSkolInfo (ClsSkol cls) = text "the class declaration for" <+> quotes (ppr cls)
2626 pprSkolInfo (DerivSkol pred) = text "the deriving clause for" <+> quotes (ppr pred)
2627 pprSkolInfo InstSkol = text "the instance declaration"
2628 pprSkolInfo (InstSC n) = text "the instance declaration" <> ifPprDebug (parens (ppr n))
2629 pprSkolInfo DataSkol = text "a data type declaration"
2630 pprSkolInfo FamInstSkol = text "a family instance declaration"
2631 pprSkolInfo BracketSkol = text "a Template Haskell bracket"
2632 pprSkolInfo (RuleSkol name) = text "the RULE" <+> pprRuleName name
2633 pprSkolInfo ArrowSkol = text "an arrow form"
2634 pprSkolInfo (PatSkol cl mc) = sep [ pprPatSkolInfo cl
2635 , text "in" <+> pprMatchContext mc ]
2636 pprSkolInfo (InferSkol ids) = sep [ text "the inferred type of"
2637 , vcat [ ppr name <+> dcolon <+> ppr ty
2638 | (name,ty) <- ids ]]
2639 pprSkolInfo (UnifyForAllSkol ty) = text "the type" <+> ppr ty
2640
2641 -- UnkSkol
2642 -- For type variables the others are dealt with by pprSkolTvBinding.
2643 -- For Insts, these cases should not happen
2644 pprSkolInfo UnkSkol = WARN( True, text "pprSkolInfo: UnkSkol" ) text "UnkSkol"
2645
2646 pprSigSkolInfo :: UserTypeCtxt -> ExpType -> SDoc
2647 pprSigSkolInfo ctxt ty
2648 = case ctxt of
2649 FunSigCtxt f _ -> pp_sig f
2650 _ -> vcat [ pprUserTypeCtxt ctxt <> colon
2651 , nest 2 (ppr ty) ]
2652 where
2653 pp_sig f = vcat [ text "the type signature for:"
2654 , nest 2 (pprPrefixOcc f <+> dcolon <+> ppr ty) ]
2655
2656 pprPatSkolInfo :: ConLike -> SDoc
2657 pprPatSkolInfo (RealDataCon dc)
2658 = sep [ text "a pattern with constructor:"
2659 , nest 2 $ ppr dc <+> dcolon
2660 <+> pprType (dataConUserType dc) <> comma ]
2661 -- pprType prints forall's regardless of -fprint-explict-foralls
2662 -- which is what we want here, since we might be saying
2663 -- type variable 't' is bound by ...
2664
2665 pprPatSkolInfo (PatSynCon ps)
2666 = sep [ text "a pattern with pattern synonym:"
2667 , nest 2 $ ppr ps <+> dcolon
2668 <+> pprType (patSynType ps) <> comma ]
2669
2670 {-
2671 ************************************************************************
2672 * *
2673 CtOrigin
2674 * *
2675 ************************************************************************
2676 -}
2677
2678 data CtOrigin
2679 = GivenOrigin SkolemInfo
2680
2681 -- All the others are for *wanted* constraints
2682 | OccurrenceOf Name -- Occurrence of an overloaded identifier
2683 | OccurrenceOfRecSel RdrName -- Occurrence of a record selector
2684 | AppOrigin -- An application of some kind
2685
2686 | SpecPragOrigin UserTypeCtxt -- Specialisation pragma for
2687 -- function or instance
2688
2689 | TypeEqOrigin { uo_actual :: TcType
2690 , uo_expected :: ExpType
2691 , uo_thing :: Maybe ErrorThing
2692 -- ^ The thing that has type "actual"
2693 }
2694
2695 | KindEqOrigin
2696 TcType (Maybe TcType) -- A kind equality arising from unifying these two types
2697 CtOrigin -- originally arising from this
2698 (Maybe TypeOrKind) -- the level of the eq this arises from
2699
2700 | IPOccOrigin HsIPName -- Occurrence of an implicit parameter
2701 | OverLabelOrigin FastString -- Occurrence of an overloaded label
2702
2703 | LiteralOrigin (HsOverLit Name) -- Occurrence of a literal
2704 | NegateOrigin -- Occurrence of syntactic negation
2705
2706 | ArithSeqOrigin (ArithSeqInfo Name) -- [x..], [x..y] etc
2707 | PArrSeqOrigin (ArithSeqInfo Name) -- [:x..y:] and [:x,y..z:]
2708 | SectionOrigin
2709 | TupleOrigin -- (..,..)
2710 | ExprSigOrigin -- e :: ty
2711 | PatSigOrigin -- p :: ty
2712 | PatOrigin -- Instantiating a polytyped pattern at a constructor
2713 | RecordUpdOrigin
2714 | ViewPatOrigin
2715
2716 | ScOrigin TypeSize -- Typechecking superclasses of an instance declaration
2717 -- If the instance head is C ty1 .. tyn
2718 -- then TypeSize = sizeTypes [ty1, .., tyn]
2719 -- See Note [Solving superclass constraints] in TcInstDcls
2720
2721 | DerivOrigin -- Typechecking deriving
2722 | DerivOriginDC DataCon Int
2723 -- Checking constraints arising from this data con and field index
2724 | DerivOriginCoerce Id Type Type
2725 -- DerivOriginCoerce id ty1 ty2: Trying to coerce class method `id` from
2726 -- `ty1` to `ty2`.
2727 | StandAloneDerivOrigin -- Typechecking stand-alone deriving
2728 | DefaultOrigin -- Typechecking a default decl
2729 | DoOrigin -- Arising from a do expression
2730 | DoPatOrigin (LPat Name) -- Arising from a failable pattern in
2731 -- a do expression
2732 | MCompOrigin -- Arising from a monad comprehension
2733 | MCompPatOrigin (LPat Name) -- Arising from a failable pattern in a
2734 -- monad comprehension
2735 | IfOrigin -- Arising from an if statement
2736 | ProcOrigin -- Arising from a proc expression
2737 | AnnOrigin -- An annotation
2738
2739 | FunDepOrigin1 -- A functional dependency from combining
2740 PredType CtLoc -- This constraint arising from ...
2741 PredType CtLoc -- and this constraint arising from ...
2742
2743 | FunDepOrigin2 -- A functional dependency from combining
2744 PredType CtOrigin -- This constraint arising from ...
2745 PredType SrcSpan -- and this instance
2746 -- We only need a CtOrigin on the first, because the location
2747 -- is pinned on the entire error message
2748
2749 | HoleOrigin
2750 | UnboundOccurrenceOf OccName
2751 | ListOrigin -- An overloaded list
2752 | StaticOrigin -- A static form
2753 | FailablePattern (LPat TcId) -- A failable pattern in do-notation for the
2754 -- MonadFail Proposal (MFP). Obsolete when
2755 -- actual desugaring to MonadFail.fail is live.
2756 | Shouldn'tHappenOrigin String
2757 -- the user should never see this one,
2758 -- unlesss ImpredicativeTypes is on, where all
2759 -- bets are off
2760
2761 -- | A thing that can be stored for error message generation only.
2762 -- It is stored with a function to zonk and tidy the thing.
2763 data ErrorThing
2764 = forall a. Outputable a => ErrorThing a
2765 (Maybe Arity) -- # of args, if known
2766 (TidyEnv -> a -> TcM (TidyEnv, a))
2767
2768 -- | Flag to see whether we're type-checking terms or kind-checking types
2769 data TypeOrKind = TypeLevel | KindLevel
2770 deriving Eq
2771
2772 instance Outputable TypeOrKind where
2773 ppr TypeLevel = text "TypeLevel"
2774 ppr KindLevel = text "KindLevel"
2775
2776 isTypeLevel :: TypeOrKind -> Bool
2777 isTypeLevel TypeLevel = True
2778 isTypeLevel KindLevel = False
2779
2780 isKindLevel :: TypeOrKind -> Bool
2781 isKindLevel TypeLevel = False
2782 isKindLevel KindLevel = True
2783
2784 -- | Make an 'ErrorThing' that doesn't need tidying or zonking
2785 mkErrorThing :: Outputable a => a -> ErrorThing
2786 mkErrorThing thing = ErrorThing thing Nothing (\env x -> return (env, x))
2787
2788 -- | Retrieve the # of arguments in the error thing, if known
2789 errorThingNumArgs_maybe :: ErrorThing -> Maybe Arity
2790 errorThingNumArgs_maybe (ErrorThing _ args _) = args
2791
2792 instance Outputable CtOrigin where
2793 ppr = pprCtOrigin
2794
2795 instance Outputable ErrorThing where
2796 ppr (ErrorThing thing _ _) = ppr thing
2797
2798 ctoHerald :: SDoc
2799 ctoHerald = text "arising from"
2800
2801 -- | Extract a suitable CtOrigin from a HsExpr
2802 exprCtOrigin :: HsExpr Name -> CtOrigin
2803 exprCtOrigin (HsVar (L _ name)) = OccurrenceOf name
2804 exprCtOrigin (HsUnboundVar occ) = UnboundOccurrenceOf occ
2805 exprCtOrigin (HsRecFld f) = OccurrenceOfRecSel (rdrNameAmbiguousFieldOcc f)
2806 exprCtOrigin (HsOverLabel l) = OverLabelOrigin l
2807 exprCtOrigin (HsIPVar ip) = IPOccOrigin ip
2808 exprCtOrigin (HsOverLit lit) = LiteralOrigin lit
2809 exprCtOrigin (HsLit {}) = Shouldn'tHappenOrigin "concrete literal"
2810 exprCtOrigin (HsLam matches) = matchesCtOrigin matches
2811 exprCtOrigin (HsLamCase _ ms) = matchesCtOrigin ms
2812 exprCtOrigin (HsApp (L _ e1) _) = exprCtOrigin e1
2813 exprCtOrigin (OpApp _ (L _ op) _ _) = exprCtOrigin op
2814 exprCtOrigin (NegApp (L _ e) _) = exprCtOrigin e
2815 exprCtOrigin (HsPar (L _ e)) = exprCtOrigin e
2816 exprCtOrigin (SectionL _ _) = SectionOrigin
2817 exprCtOrigin (SectionR _ _) = SectionOrigin
2818 exprCtOrigin (ExplicitTuple {}) = Shouldn'tHappenOrigin "explicit tuple"
2819 exprCtOrigin (HsCase _ matches) = matchesCtOrigin matches
2820 exprCtOrigin (HsIf (Just syn) _ _ _) = exprCtOrigin (syn_expr syn)
2821 exprCtOrigin (HsIf {}) = Shouldn'tHappenOrigin "if expression"
2822 exprCtOrigin (HsMultiIf _ rhs) = lGRHSCtOrigin rhs
2823 exprCtOrigin (HsLet _ (L _ e)) = exprCtOrigin e
2824 exprCtOrigin (HsDo _ _ _) = DoOrigin
2825 exprCtOrigin (ExplicitList {}) = Shouldn'tHappenOrigin "list"
2826 exprCtOrigin (ExplicitPArr {}) = Shouldn'tHappenOrigin "parallel array"
2827 exprCtOrigin (RecordCon {}) = Shouldn'tHappenOrigin "record construction"
2828 exprCtOrigin (RecordUpd {}) = Shouldn'tHappenOrigin "record update"
2829 exprCtOrigin (ExprWithTySig {}) = ExprSigOrigin
2830 exprCtOrigin (ExprWithTySigOut {}) = panic "exprCtOrigin ExprWithTySigOut"
2831 exprCtOrigin (ArithSeq {}) = Shouldn'tHappenOrigin "arithmetic sequence"
2832 exprCtOrigin (PArrSeq {}) = Shouldn'tHappenOrigin "parallel array sequence"
2833 exprCtOrigin (HsSCC _ _ (L _ e))= exprCtOrigin e
2834 exprCtOrigin (HsCoreAnn _ _ (L _ e)) = exprCtOrigin e
2835 exprCtOrigin (HsBracket {}) = Shouldn'tHappenOrigin "TH bracket"
2836 exprCtOrigin (HsRnBracketOut {})= Shouldn'tHappenOrigin "HsRnBracketOut"
2837 exprCtOrigin (HsTcBracketOut {})= panic "exprCtOrigin HsTcBracketOut"
2838 exprCtOrigin (HsSpliceE {}) = Shouldn'tHappenOrigin "TH splice"
2839 exprCtOrigin (HsProc {}) = Shouldn'tHappenOrigin "proc"
2840 exprCtOrigin (HsStatic {}) = Shouldn'tHappenOrigin "static expression"
2841 exprCtOrigin (HsArrApp {}) = panic "exprCtOrigin HsArrApp"
2842 exprCtOrigin (HsArrForm {}) = panic "exprCtOrigin HsArrForm"
2843 exprCtOrigin (HsTick _ (L _ e)) = exprCtOrigin e
2844 exprCtOrigin (HsBinTick _ _ (L _ e)) = exprCtOrigin e
2845 exprCtOrigin (HsTickPragma _ _ _ (L _ e)) = exprCtOrigin e
2846 exprCtOrigin EWildPat = panic "exprCtOrigin EWildPat"
2847 exprCtOrigin (EAsPat {}) = panic "exprCtOrigin EAsPat"
2848 exprCtOrigin (EViewPat {}) = panic "exprCtOrigin EViewPat"
2849 exprCtOrigin (ELazyPat {}) = panic "exprCtOrigin ELazyPat"
2850 exprCtOrigin (HsType {}) = Shouldn'tHappenOrigin "type application"
2851 exprCtOrigin (HsTypeOut {}) = panic "exprCtOrigin HsTypeOut"
2852 exprCtOrigin (HsWrap {}) = panic "exprCtOrigin HsWrap"
2853
2854 -- | Extract a suitable CtOrigin from a MatchGroup
2855 matchesCtOrigin :: MatchGroup Name (LHsExpr Name) -> CtOrigin
2856 matchesCtOrigin (MG { mg_alts = alts })
2857 | L _ [L _ match] <- alts
2858 , Match { m_grhss = grhss } <- match
2859 = grhssCtOrigin grhss
2860
2861 | otherwise
2862 = Shouldn'tHappenOrigin "multi-way match"
2863
2864 -- | Extract a suitable CtOrigin from guarded RHSs
2865 grhssCtOrigin :: GRHSs Name (LHsExpr Name) -> CtOrigin
2866 grhssCtOrigin (GRHSs { grhssGRHSs = lgrhss }) = lGRHSCtOrigin lgrhss
2867
2868 -- | Extract a suitable CtOrigin from a list of guarded RHSs
2869 lGRHSCtOrigin :: [LGRHS Name (LHsExpr Name)] -> CtOrigin
2870 lGRHSCtOrigin [L _ (GRHS _ (L _ e))] = exprCtOrigin e
2871 lGRHSCtOrigin _ = Shouldn'tHappenOrigin "multi-way GRHS"
2872
2873 pprCtLoc :: CtLoc -> SDoc
2874 -- "arising from ... at ..."
2875 -- Not an instance of Outputable because of the "arising from" prefix
2876 pprCtLoc (CtLoc { ctl_origin = o, ctl_env = lcl})
2877 = sep [ pprCtOrigin o
2878 , text "at" <+> ppr (tcl_loc lcl)]
2879
2880 pprCtOrigin :: CtOrigin -> SDoc
2881 -- "arising from ..."
2882 -- Not an instance of Outputable because of the "arising from" prefix
2883 pprCtOrigin (GivenOrigin sk) = ctoHerald <+> ppr sk
2884
2885 pprCtOrigin (SpecPragOrigin ctxt)
2886 = case ctxt of
2887 FunSigCtxt n _ -> text "a SPECIALISE pragma for" <+> quotes (ppr n)
2888 SpecInstCtxt -> text "a SPECIALISE INSTANCE pragma"
2889 _ -> text "a SPECIALISE pragma" -- Never happens I think
2890
2891 pprCtOrigin (FunDepOrigin1 pred1 loc1 pred2 loc2)
2892 = hang (ctoHerald <+> text "a functional dependency between constraints:")
2893 2 (vcat [ hang (quotes (ppr pred1)) 2 (pprCtLoc loc1)
2894 , hang (quotes (ppr pred2)) 2 (pprCtLoc loc2) ])
2895
2896 pprCtOrigin (FunDepOrigin2 pred1 orig1 pred2 loc2)
2897 = hang (ctoHerald <+> text "a functional dependency between:")
2898 2 (vcat [ hang (text "constraint" <+> quotes (ppr pred1))
2899 2 (pprCtOrigin orig1 )
2900 , hang (text "instance" <+> quotes (ppr pred2))
2901 2 (text "at" <+> ppr loc2) ])
2902
2903 pprCtOrigin (KindEqOrigin t1 (Just t2) _ _)
2904 = hang (ctoHerald <+> text "a kind equality arising from")
2905 2 (sep [ppr t1, char '~', ppr t2])
2906
2907 pprCtOrigin (KindEqOrigin t1 Nothing _ _)
2908 = hang (ctoHerald <+> text "a kind equality when matching")
2909 2 (ppr t1)
2910
2911 pprCtOrigin (UnboundOccurrenceOf name)
2912 = ctoHerald <+> text "an undeclared identifier" <+> quotes (ppr name)
2913
2914 pprCtOrigin (DerivOriginDC dc n)
2915 = hang (ctoHerald <+> text "the" <+> speakNth n
2916 <+> text "field of" <+> quotes (ppr dc))
2917 2 (parens (text "type" <+> quotes (ppr ty)))
2918 where
2919 ty = dataConOrigArgTys dc !! (n-1)
2920
2921 pprCtOrigin (DerivOriginCoerce meth ty1 ty2)
2922 = hang (ctoHerald <+> text "the coercion of the method" <+> quotes (ppr meth))
2923 2 (sep [ text "from type" <+> quotes (ppr ty1)
2924 , nest 2 $ text "to type" <+> quotes (ppr ty2) ])
2925
2926 pprCtOrigin (DoPatOrigin pat)
2927 = ctoHerald <+> text "a do statement"
2928 $$
2929 text "with the failable pattern" <+> quotes (ppr pat)
2930
2931 pprCtOrigin (MCompPatOrigin pat)
2932 = ctoHerald <+> hsep [ text "the failable pattern"
2933 , quotes (ppr pat)
2934 , text "in a statement in a monad comprehension" ]
2935 pprCtOrigin (FailablePattern pat)
2936 = ctoHerald <+> text "the failable pattern" <+> quotes (ppr pat)
2937 $$
2938 text "(this will become an error a future GHC release)"
2939
2940 pprCtOrigin (Shouldn'tHappenOrigin note)
2941 = sdocWithDynFlags $ \dflags ->
2942 if xopt LangExt.ImpredicativeTypes dflags
2943 then text "a situation created by impredicative types"
2944 else
2945 vcat [ text "<< This should not appear in error messages. If you see this"
2946 , text "in an error message, please report a bug mentioning" <+> quotes (text note) <+> text "at"
2947 , text "https://ghc.haskell.org/trac/ghc/wiki/ReportABug >>" ]
2948
2949 pprCtOrigin simple_origin
2950 = ctoHerald <+> pprCtO simple_origin
2951
2952 -- | Short one-liners
2953 pprCtO :: CtOrigin -> SDoc
2954 pprCtO (OccurrenceOf name) = hsep [text "a use of", quotes (ppr name)]
2955 pprCtO (OccurrenceOfRecSel name) = hsep [text "a use of", quotes (ppr name)]
2956 pprCtO AppOrigin = text "an application"
2957 pprCtO (IPOccOrigin name) = hsep [text "a use of implicit parameter", quotes (ppr name)]
2958 pprCtO (OverLabelOrigin l) = hsep [text "the overloaded label"
2959 ,quotes (char '#' <> ppr l)]
2960 pprCtO RecordUpdOrigin = text "a record update"
2961 pprCtO ExprSigOrigin = text "an expression type signature"
2962 pprCtO PatSigOrigin = text "a pattern type signature"
2963 pprCtO PatOrigin = text "a pattern"
2964 pprCtO ViewPatOrigin = text "a view pattern"
2965 pprCtO IfOrigin = text "an if expression"
2966 pprCtO (LiteralOrigin lit) = hsep [text "the literal", quotes (ppr lit)]
2967 pprCtO (ArithSeqOrigin seq) = hsep [text "the arithmetic sequence", quotes (ppr seq)]
2968 pprCtO (PArrSeqOrigin seq) = hsep [text "the parallel array sequence", quotes (ppr seq)]
2969 pprCtO SectionOrigin = text "an operator section"
2970 pprCtO TupleOrigin = text "a tuple"
2971 pprCtO NegateOrigin = text "a use of syntactic negation"
2972 pprCtO (ScOrigin n) = text "the superclasses of an instance declaration"
2973 <> ifPprDebug (parens (ppr n))
2974 pprCtO DerivOrigin = text "the 'deriving' clause of a data type declaration"
2975 pprCtO StandAloneDerivOrigin = text "a 'deriving' declaration"
2976 pprCtO DefaultOrigin = text "a 'default' declaration"
2977 pprCtO DoOrigin = text "a do statement"
2978 pprCtO MCompOrigin = text "a statement in a monad comprehension"
2979 pprCtO ProcOrigin = text "a proc expression"
2980 pprCtO (TypeEqOrigin t1 t2 _)= text "a type equality" <+> sep [ppr t1, char '~', ppr t2]
2981 pprCtO AnnOrigin = text "an annotation"
2982 pprCtO HoleOrigin = text "a use of" <+> quotes (text "_")
2983 pprCtO ListOrigin = text "an overloaded list"
2984 pprCtO StaticOrigin = text "a static form"
2985 pprCtO _ = panic "pprCtOrigin"
2986
2987 {-
2988 Constraint Solver Plugins
2989 -------------------------
2990 -}
2991
2992 type TcPluginSolver = [Ct] -- given
2993 -> [Ct] -- derived
2994 -> [Ct] -- wanted
2995 -> TcPluginM TcPluginResult
2996
2997 newtype TcPluginM a = TcPluginM (Maybe EvBindsVar -> TcM a)
2998
2999 instance Functor TcPluginM where
3000 fmap = liftM
3001
3002 instance Applicative TcPluginM where
3003 pure x = TcPluginM (const $ pure x)
3004 (<*>) = ap
3005
3006 instance Monad TcPluginM where
3007 fail x = TcPluginM (const $ fail x)
3008 TcPluginM m >>= k =
3009 TcPluginM (\ ev -> do a <- m ev
3010 runTcPluginM (k a) ev)
3011
3012 #if __GLASGOW_HASKELL__ > 710
3013 instance MonadFail.MonadFail TcPluginM where
3014 fail x = TcPluginM (const $ fail x)
3015 #endif
3016
3017 runTcPluginM :: TcPluginM a -> Maybe EvBindsVar -> TcM a
3018 runTcPluginM (TcPluginM m) = m
3019
3020 -- | This function provides an escape for direct access to
3021 -- the 'TcM` monad. It should not be used lightly, and
3022 -- the provided 'TcPluginM' API should be favoured instead.
3023 unsafeTcPluginTcM :: TcM a -> TcPluginM a
3024 unsafeTcPluginTcM = TcPluginM . const
3025
3026 -- | Access the 'EvBindsVar' carried by the 'TcPluginM' during
3027 -- constraint solving. Returns 'Nothing' if invoked during
3028 -- 'tcPluginInit' or 'tcPluginStop'.
3029 getEvBindsTcPluginM_maybe :: TcPluginM (Maybe EvBindsVar)
3030 getEvBindsTcPluginM_maybe = TcPluginM return
3031
3032
3033 data TcPlugin = forall s. TcPlugin
3034 { tcPluginInit :: TcPluginM s
3035 -- ^ Initialize plugin, when entering type-checker.
3036
3037 , tcPluginSolve :: s -> TcPluginSolver
3038 -- ^ Solve some constraints.
3039 -- TODO: WRITE MORE DETAILS ON HOW THIS WORKS.
3040
3041 , tcPluginStop :: s -> TcPluginM ()
3042 -- ^ Clean up after the plugin, when exiting the type-checker.
3043 }
3044
3045 data TcPluginResult
3046 = TcPluginContradiction [Ct]
3047 -- ^ The plugin found a contradiction.
3048 -- The returned constraints are removed from the inert set,
3049 -- and recorded as insoluable.
3050
3051 | TcPluginOk [(EvTerm,Ct)] [Ct]
3052 -- ^ The first field is for constraints that were solved.
3053 -- These are removed from the inert set,
3054 -- and the evidence for them is recorded.
3055 -- The second field contains new work, that should be processed by
3056 -- the constraint solver.