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