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