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