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