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