fix haddock submodule pointer
[ghc-hetmet.git] / compiler / typecheck / TcRnTypes.lhs
index 62281b5..d94ecd7 100644 (file)
@@ -1,4 +1,5 @@
-%
+
+% (c) The University of Glasgow 2006
 % (c) The GRASP Project, Glasgow University, 1992-2002
 %
 \begin{code}
 % (c) The GRASP Project, Glasgow University, 1992-2002
 %
 \begin{code}
@@ -12,67 +13,85 @@ module TcRnTypes(
        IfGblEnv(..), IfLclEnv(..), 
 
        -- Ranamer types
        IfGblEnv(..), IfLclEnv(..), 
 
        -- Ranamer types
-       ErrCtxt,
+       ErrCtxt, RecFieldEnv(..),
        ImportAvails(..), emptyImportAvails, plusImportAvails, 
        ImportAvails(..), emptyImportAvails, plusImportAvails, 
-       plusAvail, pruneAvails,  
-       AvailEnv, emptyAvailEnv, unitAvailEnv, plusAvailEnv, 
-       mkAvailEnv, lookupAvailEnv, lookupAvailEnv_maybe, availEnvElts, addAvail,
        WhereFrom(..), mkModDeps,
 
        -- Typechecker types
        WhereFrom(..), mkModDeps,
 
        -- Typechecker types
-       TcTyThing(..), pprTcTyThingCategory, 
-       GadtRefinement,
+       TcTypeEnv, TcTyThing(..), pprTcTyThingCategory, 
 
        -- Template Haskell
 
        -- Template Haskell
-       ThStage(..), topStage, topSpliceStage,
-       ThLevel, impLevel, topLevel,
+       ThStage(..), topStage, topAnnStage, topSpliceStage,
+       ThLevel, impLevel, outerLevel, thLevel,
 
        -- Arrows
        ArrowCtxt(NoArrowCtxt), newArrowScope, escapeArrowScope,
 
 
        -- Arrows
        ArrowCtxt(NoArrowCtxt), newArrowScope, escapeArrowScope,
 
-       -- Insts
-       Inst(..), InstOrigin(..), InstLoc(..), pprInstLoc, 
-       instLocSrcLoc, instLocSrcSpan,
-       LIE, emptyLIE, unitLIE, plusLIE, consLIE, 
-       plusLIEs, mkLIE, isEmptyLIE, lieToList, listToLIE,
+       -- Constraints
+        Untouchables(..), inTouchableRange, isNoUntouchables,
+
+        WantedConstraints(..), insolubleWC, emptyWC, isEmptyWC,
+        andWC, addFlats, addImplics, mkFlatWC,
+
+        EvVarX(..), mkEvVarX, evVarOf, evVarX, evVarOfPred,
+        WantedEvVar, wantedToFlavored,
+        keepWanted,
+
+        Implication(..),
+        CtLoc(..), ctLocSpan, ctLocOrigin, setCtLocOrigin,
+       CtOrigin(..), EqOrigin(..), 
+        WantedLoc, GivenLoc, GivenKind(..), pushErrCtxt,
+
+       SkolemInfo(..),
+
+        CtFlavor(..), pprFlavorArising, isWanted, 
+        isGivenOrSolved, isGiven_maybe,
+        isDerived,
+        FlavoredEvVar,
+
+       -- Pretty printing
+        pprEvVarTheta, pprWantedEvVar, pprWantedsWithLocs,
+       pprEvVars, pprEvVarWithType,
+        pprArising, pprArisingAt,
 
        -- Misc other types
 
        -- Misc other types
-       TcId, TcIdSet, TcDictBinds
+       TcId, TcIdSet, TcTyVarBind(..), TcTyVarBinds
+       
   ) where
 
 #include "HsVersions.h"
 
   ) where
 
 #include "HsVersions.h"
 
-import HsSyn           ( PendingSplice, HsOverLit, LRuleDecl, LForeignDecl,
-                         ArithSeqInfo, DictBinds, LHsBinds, LImportDecl, HsGroup,
-                          IE )
-import HscTypes                ( FixityEnv,
-                         HscEnv, TypeEnv, TyThing, 
-                         GenAvailInfo(..), AvailInfo, HscSource(..),
-                         availName, IsBootInterface, Deprecations )
-import Packages                ( PackageId, HomeModules )
-import Type            ( Type, pprTyThingCategory )
-import TcType          ( TcTyVarSet, TcType, TcThetaType, SkolemInfo, TvSubst,
-                         TcPredType, TcKind, tcCmpPred, tcCmpType, tcCmpTypes, pprSkolInfo )
-import InstEnv         ( Instance, InstEnv )
+import HsSyn
+import HscTypes
+import Type
+import Id      ( evVarPred )
+import Class    ( Class )
+import DataCon  ( DataCon, dataConUserType )
+import TcType
+import Annotations
+import InstEnv
+import FamInstEnv
 import IOEnv
 import IOEnv
-import RdrName         ( GlobalRdrEnv, LocalRdrEnv )
-import Name            ( Name )
+import RdrName
+import Name
 import NameEnv
 import NameEnv
-import NameSet         ( NameSet, unionNameSets, DefUses )
-import OccName         ( OccEnv )
-import Var             ( Id, TyVar )
-import VarEnv          ( TidyEnv )
+import NameSet
+import Var
+import VarEnv
 import Module
 import Module
-import SrcLoc          ( SrcSpan, SrcLoc, Located, srcSpanStart )
-import VarSet          ( IdSet )
-import ErrUtils                ( Messages, Message )
-import UniqSupply      ( UniqSupply )
-import BasicTypes      ( IPName )
-import Util            ( thenCmp )
+import SrcLoc
+import VarSet
+import ErrUtils
+import UniqFM
+import UniqSupply
+import Unique
+import BasicTypes
 import Bag
 import Outputable
 import Bag
 import Outputable
-import Maybe           ( mapMaybe )
-import ListSetOps      ( unionLists )
+import ListSetOps
+import FastString
+
+import Data.Set (Set)
 \end{code}
 
 
 \end{code}
 
 
@@ -87,14 +106,13 @@ The monad itself has to be defined here, because it is mentioned by ErrCtxt
 
 \begin{code}
 type TcRef a    = IORef a
 
 \begin{code}
 type TcRef a    = IORef a
-type TcId       = Id                   -- Type may be a TcType
+type TcId       = Id                   -- Type may be a TcType  DV: WHAT??????????
 type TcIdSet    = IdSet
 type TcIdSet    = IdSet
-type TcDictBinds = DictBinds TcId      -- Bag of dictionary bindings
-
 
 
 type TcRnIf a b c = IOEnv (Env a b) c
 type IfM lcl a  = TcRnIf IfGblEnv lcl a                -- Iface stuff
 
 
 type TcRnIf a b c = IOEnv (Env a b) c
 type IfM lcl a  = TcRnIf IfGblEnv lcl a                -- Iface stuff
+
 type IfG a  = IfM () a                         -- Top level
 type IfL a  = IfM IfLclEnv a                   -- Nested
 type TcRn a = TcRnIf TcGblEnv TcLclEnv a
 type IfG a  = IfM () a                         -- Top level
 type IfL a  = IfM IfLclEnv a                   -- Nested
 type TcRn a = TcRnIf TcGblEnv TcLclEnv a
@@ -102,6 +120,18 @@ type RnM  a = TcRn a               -- Historical
 type TcM  a = TcRn a           -- Historical
 \end{code}
 
 type TcM  a = TcRn a           -- Historical
 \end{code}
 
+Representation of type bindings to uninstantiated meta variables used during
+constraint solving.
+
+\begin{code}
+data TcTyVarBind = TcTyVarBind TcTyVar TcType
+
+type TcTyVarBinds = Bag TcTyVarBind
+
+instance Outputable TcTyVarBind where
+  ppr (TcTyVarBind tv ty) = ppr tv <+> text ":=" <+> ppr ty
+\end{code}
+
 
 %************************************************************************
 %*                                                                     *
 
 %************************************************************************
 %*                                                                     *
@@ -115,13 +145,13 @@ data Env gbl lcl  -- Changes as we move into an expression
        env_top  :: HscEnv,     -- Top-level stuff that never changes
                                -- Includes all info about imported things
 
        env_top  :: HscEnv,     -- Top-level stuff that never changes
                                -- Includes all info about imported things
 
-       env_us   :: TcRef UniqSupply,   -- Unique supply for local varibles
+       env_us   :: {-# UNPACK #-} !(IORef UniqSupply), 
+                               -- Unique supply for local varibles
 
        env_gbl  :: gbl,        -- Info about things defined at the top level
                                -- of the module being compiled
 
 
        env_gbl  :: gbl,        -- Info about things defined at the top level
                                -- of the module being compiled
 
-       env_lcl  :: lcl         -- Nested stuff; changes as we go into 
-                               -- an expression
+       env_lcl  :: lcl         -- Nested stuff; changes as we go into 
     }
 
 -- TcGblEnv describes the top-level of the module at the 
     }
 
 -- TcGblEnv describes the top-level of the module at the 
@@ -130,105 +160,135 @@ data Env gbl lcl        -- Changes as we move into an expression
 
 data TcGblEnv
   = TcGblEnv {
 
 data TcGblEnv
   = TcGblEnv {
-       tcg_mod     :: Module,          -- Module being compiled
-       tcg_src     :: HscSource,       -- What kind of module 
-                                       -- (regular Haskell, hs-boot, ext-core)
-
-       tcg_rdr_env :: GlobalRdrEnv,    -- Top level envt; used during renaming
-       tcg_default :: Maybe [Type],    -- Types used for defaulting
-                                       -- Nothing => no 'default' decl
-
-       tcg_fix_env  :: FixityEnv,      -- Just for things in this module
-
-       tcg_type_env :: TypeEnv,        -- Global type env for the module we are compiling now
-               -- All TyCons and Classes (for this module) end up in here right away,
-               -- along with their derived constructors, selectors.
-               --
-               -- (Ids defined in this module start in the local envt, 
-               --  though they move to the global envt during zonking)
-
-       tcg_type_env_var :: TcRef TypeEnv,      
+       tcg_mod     :: Module,         -- ^ Module being compiled
+       tcg_src     :: HscSource,
+          -- ^ What kind of module (regular Haskell, hs-boot, ext-core)
+
+       tcg_rdr_env :: GlobalRdrEnv,   -- ^ Top level envt; used during renaming
+       tcg_default :: Maybe [Type],
+          -- ^ Types used for defaulting. @Nothing@ => no @default@ decl
+
+       tcg_fix_env   :: FixityEnv,     -- ^ Just for things in this module
+       tcg_field_env :: RecFieldEnv,   -- ^ Just for things in this module
+
+       tcg_type_env :: TypeEnv,
+          -- ^ Global type env for the module we are compiling now.  All
+         -- TyCons and Classes (for this module) end up in here right away,
+         -- along with their derived constructors, selectors.
+         --
+         -- (Ids defined in this module start in the local envt, though they
+         --  move to the global envt during zonking)
+
+       tcg_type_env_var :: TcRef TypeEnv,
                -- Used only to initialise the interface-file
                -- typechecker in initIfaceTcRn, so that it can see stuff
                -- bound in this module when dealing with hi-boot recursions
                -- Updated at intervals (e.g. after dealing with types and classes)
        
                -- Used only to initialise the interface-file
                -- typechecker in initIfaceTcRn, so that it can see stuff
                -- bound in this module when dealing with hi-boot recursions
                -- Updated at intervals (e.g. after dealing with types and classes)
        
-       tcg_inst_env :: InstEnv,        -- Instance envt for *home-package* modules
-                                       -- Includes the dfuns in tcg_insts
+       tcg_inst_env     :: InstEnv,
+          -- ^ Instance envt for /home-package/ modules; Includes the dfuns in
+         -- tcg_insts
+       tcg_fam_inst_env :: FamInstEnv, -- ^ Ditto for family instances
+
                -- Now a bunch of things about this module that are simply 
                -- accumulated, but never consulted until the end.  
                -- Nevertheless, it's convenient to accumulate them along 
                -- with the rest of the info from this module.
                -- Now a bunch of things about this module that are simply 
                -- accumulated, but never consulted until the end.  
                -- Nevertheless, it's convenient to accumulate them along 
                -- with the rest of the info from this module.
-       tcg_exports :: NameSet,         -- What is exported
-       tcg_imports :: ImportAvails,    -- Information about what was imported 
-                                       --    from where, including things bound
-                                       --    in this module
-
-       tcg_home_mods :: HomeModules,
-                               -- Calculated from ImportAvails, allows us to
-                               -- call Packages.isHomeModule
-
-       tcg_dus :: DefUses,     -- What is defined in this module and what is used.
-                               -- The latter is used to generate 
-                               --      (a) version tracking; no need to recompile if these
-                               --              things have not changed version stamp
-                               --      (b) unused-import info
-
-       tcg_keep :: TcRef NameSet,      -- Locally-defined top-level names to keep alive
-               -- "Keep alive" means give them an Exported flag, so
-               -- that the simplifier does not discard them as dead 
-               -- code, and so that they are exposed in the interface file
-               -- (but not to export to the user).
-               --
-               -- Some things, like dict-fun Ids and default-method Ids are 
-               -- "born" with the Exported flag on, for exactly the above reason,
-               -- but some we only discover as we go.  Specifically:
-               --      * The to/from functions for generic data types
-               --      * Top-level variables appearing free in the RHS of an orphan rule
-               --      * Top-level variables appearing free in a TH bracket
-
-       tcg_inst_uses :: TcRef NameSet, -- Home-package Dfuns actually used 
-               -- Used to generate version dependencies
-               -- This records usages, rather like tcg_dus, but it has to
-               -- be a mutable variable so it can be augmented 
-               -- when we look up an instance.  These uses of dfuns are
-               -- rather like the free variables of the program, but
-               -- are implicit instead of explicit.
-
-       tcg_th_used :: TcRef Bool,      -- True <=> Template Haskell syntax used
-               -- We need this so that we can generate a dependency on the
-               -- Template Haskell package, becuase the desugarer is going to
-               -- emit loads of references to TH symbols.  It's rather like 
-               -- tcg_inst_uses; the reference is implicit rather than explicit,
-               -- so we have to zap a mutable variable.
-
-       tcg_dfun_n  :: TcRef Int,       -- Allows us to number off the names of DFuns
-               -- It's convenient to allocate an External Name for a DFun, with
-               -- a permanently-fixed unique, just like other top-level functions
-               -- defined in this module.  But that means we need a canonical 
-               -- occurrence name, distinct from all other dfuns in this module,
-               -- and this name supply serves that purpose (df1, df2, etc).
-
-               -- The next fields accumulate the payload of the module
-               -- The binds, rules and foreign-decl fiels are collected
-               -- initially in un-zonked form and are finally zonked in tcRnSrcDecls
-
-               -- The next fields accumulate the payload of the
-               -- module The binds, rules and foreign-decl fiels are
-               -- collected initially in un-zonked form and are
-               -- finally zonked in tcRnSrcDecls
-
-        tcg_rn_imports :: Maybe [LImportDecl Name],
+       tcg_exports :: [AvailInfo],     -- ^ What is exported
+       tcg_imports :: ImportAvails,
+          -- ^ Information about what was imported from where, including
+         -- things bound in this module.
+
+       tcg_dus :: DefUses,
+          -- ^ What is defined in this module and what is used.
+          -- The latter is used to generate
+          --
+          --  (a) version tracking; no need to recompile if these things have
+          --      not changed version stamp
+          --
+          --  (b) unused-import info
+
+       tcg_keep :: TcRef NameSet,
+          -- ^ Locally-defined top-level names to keep alive.
+          --
+          -- "Keep alive" means give them an Exported flag, so that the
+          -- simplifier does not discard them as dead code, and so that they
+          -- are exposed in the interface file (but not to export to the
+          -- user).
+          --
+          -- Some things, like dict-fun Ids and default-method Ids are "born"
+          -- with the Exported flag on, for exactly the above reason, but some
+          -- we only discover as we go.  Specifically:
+          --
+          --   * The to/from functions for generic data types
+          --
+          --   * Top-level variables appearing free in the RHS of an orphan
+          --     rule
+          --
+          --   * Top-level variables appearing free in a TH bracket
+
+        tcg_th_used :: TcRef Bool,
+          -- ^ @True@ <=> Template Haskell syntax used.
+          --
+          -- We need this so that we can generate a dependency on the
+          -- Template Haskell package, becuase the desugarer is going
+          -- to emit loads of references to TH symbols.  The reference
+          -- is implicit rather than explicit, so we have to zap a
+          -- mutable variable.
+
+       tcg_dfun_n  :: TcRef OccSet,
+          -- ^ Allows us to choose unique DFun names.
+
+       -- The next fields accumulate the payload of the module
+       -- The binds, rules and foreign-decl fiels are collected
+       -- initially in un-zonked form and are finally zonked in tcRnSrcDecls
+
         tcg_rn_exports :: Maybe [Located (IE Name)],
         tcg_rn_exports :: Maybe [Located (IE Name)],
-       tcg_rn_decls :: Maybe (HsGroup Name),   -- renamed decls, maybe
-               -- Nothing <=> Don't retain renamed decls
-
-       tcg_binds   :: LHsBinds Id,             -- Value bindings in this module
-       tcg_deprecs :: Deprecations,            -- ...Deprecations 
-       tcg_insts   :: [Instance],              -- ...Instances
-       tcg_rules   :: [LRuleDecl Id],          -- ...Rules
-       tcg_fords   :: [LForeignDecl Id]        -- ...Foreign import & exports
+        tcg_rn_imports :: [LImportDecl Name],
+               -- Keep the renamed imports regardless.  They are not 
+               -- voluminous and are needed if you want to report unused imports
+
+        tcg_used_rdrnames :: TcRef (Set RdrName),
+               -- The set of used *imported* (not locally-defined) RdrNames
+               -- Used only to report unused import declarations
+
+       tcg_rn_decls :: Maybe (HsGroup Name),
+          -- ^ Renamed decls, maybe.  @Nothing@ <=> Don't retain renamed
+          -- decls.
+
+        tcg_ev_binds  :: Bag EvBind,       -- Top-level evidence bindings
+       tcg_binds     :: LHsBinds Id,       -- Value bindings in this module
+        tcg_sigs      :: NameSet,          -- ...Top-level names that *lack* a signature
+        tcg_imp_specs :: [LTcSpecPrag],     -- ...SPECIALISE prags for imported Ids
+       tcg_warns     :: Warnings,          -- ...Warnings and deprecations
+       tcg_anns      :: [Annotation],      -- ...Annotations
+       tcg_insts     :: [Instance],        -- ...Instances
+        tcg_fam_insts :: [FamInst],         -- ...Family instances
+        tcg_rules     :: [LRuleDecl Id],    -- ...Rules
+        tcg_fords     :: [LForeignDecl Id], -- ...Foreign import & exports
+        tcg_vects     :: [LVectDecl Id],    -- ...Vectorisation declarations
+
+       tcg_doc_hdr   :: Maybe LHsDocString, -- ^ Maybe Haddock header docs
+        tcg_hpc       :: AnyHpcUsage,        -- ^ @True@ if any part of the
+                                             --  prog uses hpc instrumentation.
+
+        tcg_main      :: Maybe Name          -- ^ The Name of the main
+                                             -- function, if this module is
+                                             -- the main module.
     }
     }
+
+data RecFieldEnv 
+  = RecFields (NameEnv [Name]) -- Maps a constructor name *in this module*
+                               -- to the fields for that constructor
+             NameSet           -- Set of all fields declared *in this module*;
+                               -- used to suppress name-shadowing complaints
+                               -- when using record wild cards
+                               -- E.g.  let fld = e in C {..}
+       -- This is used when dealing with ".." notation in record 
+       -- construction and pattern matching.
+       -- The FieldEnv deals *only* with constructors defined in *this*
+       -- module.  For imported modules, we get the same info from the
+       -- TypeEnv
 \end{code}
 
 %************************************************************************
 \end{code}
 
 %************************************************************************
@@ -266,8 +326,9 @@ data IfLclEnv
                --      .hi file, or GHCi state, or ext core
                -- plus which bit is currently being examined
 
                --      .hi file, or GHCi state, or ext core
                -- plus which bit is currently being examined
 
-       if_tv_env  :: OccEnv TyVar,     -- Nested tyvar bindings
-       if_id_env  :: OccEnv Id         -- Nested id binding
+       if_tv_env  :: UniqFM TyVar,     -- Nested tyvar bindings
+                                       -- (and coercions)
+       if_id_env  :: UniqFM Id         -- Nested id binding
     }
 \end{code}
 
     }
 \end{code}
 
@@ -298,11 +359,11 @@ data TcLclEnv             -- Changes as we move inside an expression
                        -- Discarded after typecheck/rename; not passed on to desugarer
   = TcLclEnv {
        tcl_loc  :: SrcSpan,            -- Source span
                        -- Discarded after typecheck/rename; not passed on to desugarer
   = TcLclEnv {
        tcl_loc  :: SrcSpan,            -- Source span
-       tcl_ctxt :: ErrCtxt,            -- Error context
+       tcl_ctxt :: [ErrCtxt],          -- Error context, innermost on top
        tcl_errs :: TcRef Messages,     -- Place to accumulate errors
 
        tcl_errs :: TcRef Messages,     -- Place to accumulate errors
 
-       tcl_th_ctxt    :: ThStage,      -- Template Haskell context
-       tcl_arrow_ctxt :: ArrowCtxt,    -- Arrow-notation context
+       tcl_th_ctxt    :: ThStage,            -- Template Haskell context
+       tcl_arrow_ctxt :: ArrowCtxt,          -- Arrow-notation context
 
        tcl_rdr :: LocalRdrEnv,         -- Local name envt
                -- Maintained during renaming, of course, but also during
 
        tcl_rdr :: LocalRdrEnv,         -- Local name envt
                -- Maintained during renaming, of course, but also during
@@ -316,18 +377,28 @@ data TcLclEnv             -- Changes as we move inside an expression
                -- We still need the unsullied global name env so that
                --   we can look up record field names
 
                -- We still need the unsullied global name env so that
                --   we can look up record field names
 
-       tcl_env  :: NameEnv TcTyThing,  -- The local type environment: Ids and TyVars
-                                       -- defined in this module
+        tcl_hetMetLevel  :: [TyVar],    -- The current environment classifier level (list-of-names)
+       tcl_env  :: TcTypeEnv,    -- The local type environment: Ids and
+                                 -- TyVars defined in this module
                                        
        tcl_tyvars :: TcRef TcTyVarSet, -- The "global tyvars"
                        -- Namely, the in-scope TyVars bound in tcl_env, 
                                        
        tcl_tyvars :: TcRef TcTyVarSet, -- The "global tyvars"
                        -- Namely, the in-scope TyVars bound in tcl_env, 
-                       -- plus the tyvars mentioned in the types of Ids bound in tcl_lenv
-                       -- Why mutable? see notes with tcGetGlobalTyVars
-
-       tcl_lie   :: TcRef LIE          -- Place to accumulate type constraints
+                       -- plus the tyvars mentioned in the types of Ids bound
+                       -- in tcl_lenv. 
+                        -- Why mutable? see notes with tcGetGlobalTyVars
+
+       tcl_lie   :: TcRef WantedConstraints,    -- Place to accumulate type constraints
+
+       -- TcMetaTyVars have 
+       tcl_meta  :: TcRef Unique,  -- The next free unique for TcMetaTyVars
+                                   -- Guaranteed to be allocated linearly
+       tcl_untch :: Unique         -- Any TcMetaTyVar with 
+                                   --     unique >= tcl_untch is touchable
+                                   --     unique <  tcl_untch is untouchable
     }
 
     }
 
-type GadtRefinement = TvSubst
+type TcTypeEnv = NameEnv TcTyThing
+
 
 {- Note [Given Insts]
    ~~~~~~~~~~~~~~~~~~
 
 {- Note [Given Insts]
    ~~~~~~~~~~~~~~~~~~
@@ -344,34 +415,55 @@ pass it inwards.
 -}
 
 ---------------------------
 -}
 
 ---------------------------
--- Template Haskell levels 
+-- Template Haskell stages and levels 
 ---------------------------
 
 ---------------------------
 
+data ThStage   -- See Note [Template Haskell state diagram] in TcSplice
+  = Splice     -- Top-level splicing
+               -- This code will be run *at compile time*;
+               --   the result replaces the splice
+               -- Binding level = 0
+  | Comp       -- Ordinary Haskell code
+               -- Binding level = 1
+
+  | Brack                      -- Inside brackets 
+      ThStage                  --   Binding level = level(stage) + 1
+      (TcRef [PendingSplice])  --   Accumulate pending splices here
+      (TcRef WantedConstraints)        --     and type constraints here
+
+topStage, topAnnStage, topSpliceStage :: ThStage
+topStage       = Comp
+topAnnStage    = Splice
+topSpliceStage = Splice
+
+instance Outputable ThStage where
+   ppr Splice        = text "Splice"
+   ppr Comp         = text "Comp"
+   ppr (Brack s _ _) = text "Brack" <> parens (ppr s)
+
 type ThLevel = Int     
 type ThLevel = Int     
-       -- Indicates how many levels of brackets we are inside
-       --      (always >= 0)
+        -- See Note [Template Haskell levels] in TcSplice
        -- Incremented when going inside a bracket,
        -- decremented when going inside a splice
        -- Incremented when going inside a bracket,
        -- decremented when going inside a splice
+       -- NB: ThLevel is one greater than the 'n' in Fig 2 of the
+       --     original "Template meta-programming for Haskell" paper
 
 
-impLevel, topLevel :: ThLevel
-topLevel = 1   -- Things defined at top level of this module
+impLevel, outerLevel :: ThLevel
 impLevel = 0   -- Imported things; they can be used inside a top level splice
 impLevel = 0   -- Imported things; they can be used inside a top level splice
+outerLevel = 1 -- Things defined outside brackets
+-- NB: Things at level 0 are not *necessarily* imported.
+--     eg  $( \b -> ... )   here b is bound at level 0
 --
 -- For example: 
 --     f = ...
 --     g1 = $(map ...)         is OK
 --     g2 = $(f ...)           is not OK; because we havn't compiled f yet
 
 --
 -- For example: 
 --     f = ...
 --     g1 = $(map ...)         is OK
 --     g2 = $(f ...)           is not OK; because we havn't compiled f yet
 
-
-data ThStage
-  = Comp                               -- Ordinary compiling, at level topLevel
-  | Splice ThLevel                     -- Inside a splice
-  | Brack  ThLevel                     -- Inside brackets; 
-          (TcRef [PendingSplice])      --   accumulate pending splices here
-          (TcRef LIE)                  --   and type constraints here
-topStage, topSpliceStage :: ThStage
-topStage       = Comp
-topSpliceStage = Splice (topLevel - 1) -- Stage for the body of a top-level splice
+thLevel :: ThStage -> ThLevel
+thLevel Splice        = 0
+thLevel Comp          = 1
+thLevel (Brack s _ _) = thLevel s + 1
 
 ---------------------------
 -- Arrow-notation context
 
 ---------------------------
 -- Arrow-notation context
@@ -420,36 +512,45 @@ escapeArrowScope
 data TcTyThing
   = AGlobal TyThing            -- Used only in the return type of a lookup
 
 data TcTyThing
   = AGlobal TyThing            -- Used only in the return type of a lookup
 
-  | ATcId   TcId               -- Ids defined in this module; may not be fully zonked
-           ThLevel 
-           Bool                -- True <=> apply the type refinement to me
+  | ATcId   {          -- Ids defined in this module; may not be fully zonked
+       tct_id    :: TcId,              
+       tct_level :: ThLevel,
+       tct_hetMetLevel :: [TyVar]
+    }
 
   | ATyVar  Name TcType                -- The type to which the lexically scoped type vaiable
                                -- is currently refined. We only need the Name
 
   | ATyVar  Name TcType                -- The type to which the lexically scoped type vaiable
                                -- is currently refined. We only need the Name
-                               -- for error-message purposes
+                               -- for error-message purposes; it is the corresponding
+                               -- Name in the domain of the envt
 
   | AThing  TcKind             -- Used temporarily, during kind checking, for the
                                --      tycons and clases in this recursive group
 
 instance Outputable TcTyThing where    -- Debugging only
 
   | AThing  TcKind             -- Used temporarily, during kind checking, for the
                                --      tycons and clases in this recursive group
 
 instance Outputable TcTyThing where    -- Debugging only
-   ppr (AGlobal g)      = ppr g
-   ppr (ATcId g tl rig) = text "Identifier" <> 
-                         ifPprDebug (brackets (ppr g <> comma <> ppr tl <+> ppr rig))
+   ppr (AGlobal g)      = pprTyThing g
+   ppr elt@(ATcId {})   = text "Identifier" <> 
+                         brackets (ppr (tct_id elt) <> dcolon 
+                                 <> ppr (varType (tct_id elt)) <> comma
+                                <+> ppr (tct_level elt)
+                                <+> ppr (tct_hetMetLevel elt))
    ppr (ATyVar tv _)    = text "Type variable" <+> quotes (ppr tv)
    ppr (AThing k)       = text "AThing" <+> ppr k
 
 pprTcTyThingCategory :: TcTyThing -> SDoc
 pprTcTyThingCategory (AGlobal thing) = pprTyThingCategory thing
    ppr (ATyVar tv _)    = text "Type variable" <+> quotes (ppr tv)
    ppr (AThing k)       = text "AThing" <+> ppr k
 
 pprTcTyThingCategory :: TcTyThing -> SDoc
 pprTcTyThingCategory (AGlobal thing) = pprTyThingCategory thing
-pprTcTyThingCategory (ATyVar {})     = ptext SLIT("Type variable")
-pprTcTyThingCategory (ATcId {})      = ptext SLIT("Local identifier")
-pprTcTyThingCategory (AThing {})     = ptext SLIT("Kinded thing")
+pprTcTyThingCategory (ATyVar {})     = ptext (sLit "Type variable")
+pprTcTyThingCategory (ATcId {})      = ptext (sLit "Local identifier")
+pprTcTyThingCategory (AThing {})     = ptext (sLit "Kinded thing")
 \end{code}
 
 \begin{code}
 \end{code}
 
 \begin{code}
-type ErrCtxt = [TidyEnv -> TcM (TidyEnv, Message)]     
-                       -- Innermost first.  Monadic so that we have a chance
-                       -- to deal with bound type variables just before error
-                       -- message construction
+type ErrCtxt = (Bool, TidyEnv -> TcM (TidyEnv, Message))
+       -- Monadic so that we have a chance
+       -- to deal with bound type variables just before error
+       -- message construction
+
+       -- Bool:  True <=> this is a landmark context; do not
+       --                 discard it when trimming for display
 \end{code}
 
 
 \end{code}
 
 
@@ -459,89 +560,98 @@ type ErrCtxt = [TidyEnv -> TcM (TidyEnv, Message)]
 %*                                                                     *
 %************************************************************************
 
 %*                                                                     *
 %************************************************************************
 
-ImportAvails summarises what was imported from where, irrespective
-of whether the imported things are actually used or not
-It is used     * when processing the export list
-               * when constructing usage info for the inteface file
-               * to identify the list of directly imported modules
-                       for initialisation purposes
-               * when figuring out what things are really unused
-
 \begin{code}
 \begin{code}
+-- | 'ImportAvails' summarises what was imported from where, irrespective of
+-- whether the imported things are actually used or not.  It is used:
+--
+--  * when processing the export list,
+--
+--  * when constructing usage info for the interface file,
+--
+--  * to identify the list of directly imported modules for initialisation
+--    purposes and for optimised overlap checking of family instances,
+--
+--  * when figuring out what things are really unused
+--
 data ImportAvails 
    = ImportAvails {
 data ImportAvails 
    = ImportAvails {
-       imp_env :: ModuleEnv NameSet,
-               -- All the things imported, classified by 
-               -- the *module qualifier* for its import
-               --   e.g.        import List as Foo
-               -- would add a binding Foo |-> ...stuff from List...
-               -- to imp_env.
-               -- 
-               -- We need to classify them like this so that we can figure out 
-               -- "module M" export specifiers in an export list 
-               -- (see 1.4 Report Section 5.1.1).  Ultimately, we want to find 
-               -- everything that is unambiguously in scope as 'M.x'
-               -- and where plain 'x' is (perhaps ambiguously) in scope.
-               -- So the starting point is all things that are in scope as 'M.x',
-               -- which is what this field tells us.
-
-       imp_mods :: ModuleEnv (Module, Bool, SrcSpan),
-               -- Domain is all directly-imported modules
-               -- Bool means:
-               --   True => import was "import Foo ()"
-               --   False  => import was some other form
-               --
-               -- We need the Module in the range because we can't get
-               --      the keys of a ModuleEnv
-               -- Used 
-               --   (a) to help construct the usage information in 
-               --       the interface file; if we import somethign we
-               --       need to recompile if the export version changes
-               --   (b) to specify what child modules to initialise
-
-       imp_dep_mods :: ModuleEnv (Module, IsBootInterface),
-               -- Home-package modules needed by the module being compiled
-               --
-               -- It doesn't matter whether any of these dependencies
-               -- are actually *used* when compiling the module; they
-               -- are listed if they are below it at all.  For
-               -- example, suppose M imports A which imports X.  Then
-               -- compiling M might not need to consult X.hi, but X
-               -- is still listed in M's dependencies.
+       imp_mods :: ModuleEnv [(ModuleName, Bool, SrcSpan)],
+          -- ^ Domain is all directly-imported modules
+          -- The 'ModuleName' is what the module was imported as, e.g. in
+          -- @
+          --     import Foo as Bar
+          -- @
+          -- it is @Bar@.
+          --
+          -- The 'Bool' means:
+          --
+          --  - @True@ => import was @import Foo ()@
+          --
+          --  - @False@ => import was some other form
+          --
+          -- Used
+          --
+          --   (a) to help construct the usage information in the interface
+          --       file; if we import somethign we need to recompile if the
+          --       export version changes
+          --
+          --   (b) to specify what child modules to initialise
+          --
+          -- We need a full ModuleEnv rather than a ModuleNameEnv here,
+          -- because we might be importing modules of the same name from
+          -- different packages. (currently not the case, but might be in the
+          -- future).
+
+       imp_dep_mods :: ModuleNameEnv (ModuleName, IsBootInterface),
+         -- ^ Home-package modules needed by the module being compiled
+         --
+         -- It doesn't matter whether any of these dependencies
+         -- are actually /used/ when compiling the module; they
+         -- are listed if they are below it at all.  For
+         -- example, suppose M imports A which imports X.  Then
+         -- compiling M might not need to consult X.hi, but X
+         -- is still listed in M's dependencies.
 
        imp_dep_pkgs :: [PackageId],
 
        imp_dep_pkgs :: [PackageId],
-               -- Packages needed by the module being compiled, whether
-               -- directly, or via other modules in this package, or via
-               -- modules imported from other packages.
+          -- ^ Packages needed by the module being compiled, whether directly,
+          -- or via other modules in this package, or via modules imported
+          -- from other packages.
+
+       imp_orphs :: [Module],
+          -- ^ Orphan modules below us in the import tree (and maybe including
+          -- us for imported modules)
 
 
-       imp_orphs :: [Module]
-               -- Orphan modules below us in the import tree
+       imp_finsts :: [Module]
+          -- ^ Family instance modules below us in the import tree (and maybe
+          -- including us for imported modules)
       }
 
       }
 
-mkModDeps :: [(Module, IsBootInterface)]
-         -> ModuleEnv (Module, IsBootInterface)
-mkModDeps deps = foldl add emptyModuleEnv deps
+mkModDeps :: [(ModuleName, IsBootInterface)]
+         -> ModuleNameEnv (ModuleName, IsBootInterface)
+mkModDeps deps = foldl add emptyUFM deps
               where
               where
-                add env elt@(m,_) = extendModuleEnv env m elt
+                add env elt@(m,_) = addToUFM env m elt
 
 emptyImportAvails :: ImportAvails
 
 emptyImportAvails :: ImportAvails
-emptyImportAvails = ImportAvails { imp_env     = emptyModuleEnv, 
-                                  imp_mods     = emptyModuleEnv,
-                                  imp_dep_mods = emptyModuleEnv,
+emptyImportAvails = ImportAvails { imp_mods    = emptyModuleEnv,
+                                  imp_dep_mods = emptyUFM,
                                   imp_dep_pkgs = [],
                                   imp_dep_pkgs = [],
-                                  imp_orphs    = [] }
+                                  imp_orphs    = [],
+                                  imp_finsts   = [] }
 
 plusImportAvails ::  ImportAvails ->  ImportAvails ->  ImportAvails
 plusImportAvails
 
 plusImportAvails ::  ImportAvails ->  ImportAvails ->  ImportAvails
 plusImportAvails
-  (ImportAvails { imp_env = env1, imp_mods = mods1,
-                 imp_dep_mods = dmods1, imp_dep_pkgs = dpkgs1, imp_orphs = orphs1 })
-  (ImportAvails { imp_env = env2, imp_mods = mods2,
-                 imp_dep_mods = dmods2, imp_dep_pkgs = dpkgs2, imp_orphs = orphs2 })
-  = ImportAvails { imp_env      = plusModuleEnv_C unionNameSets env1 env2, 
-                  imp_mods     = mods1  `plusModuleEnv` mods2, 
-                  imp_dep_mods = plusModuleEnv_C plus_mod_dep dmods1 dmods2,   
+  (ImportAvails { imp_mods = mods1,
+                 imp_dep_mods = dmods1, imp_dep_pkgs = dpkgs1, 
+                  imp_orphs = orphs1, imp_finsts = finsts1 })
+  (ImportAvails { imp_mods = mods2,
+                 imp_dep_mods = dmods2, imp_dep_pkgs = dpkgs2,
+                  imp_orphs = orphs2, imp_finsts = finsts2 })
+  = ImportAvails { imp_mods     = plusModuleEnv_C (++) mods1 mods2,
+                  imp_dep_mods = plusUFM_C plus_mod_dep dmods1 dmods2, 
                   imp_dep_pkgs = dpkgs1 `unionLists` dpkgs2,
                   imp_dep_pkgs = dpkgs1 `unionLists` dpkgs2,
-                  imp_orphs    = orphs1 `unionLists` orphs2 }
+                  imp_orphs    = orphs1 `unionLists` orphs2,
+                  imp_finsts   = finsts1 `unionLists` finsts2 }
   where
     plus_mod_dep (m1, boot1) (m2, boot2) 
        = WARN( not (m1 == m2), (ppr m1 <+> ppr m2) $$ (ppr boot1 <+> ppr boot2) )
   where
     plus_mod_dep (m1, boot1) (m2, boot2) 
        = WARN( not (m1 == m2), (ppr m1 <+> ppr m2) $$ (ppr boot1 <+> ppr boot2) )
@@ -551,268 +661,509 @@ plusImportAvails
 
 %************************************************************************
 %*                                                                     *
 
 %************************************************************************
 %*                                                                     *
-       Avails, AvailEnv, etc
+\subsection{Where from}
 %*                                                                     *
 %*                                                                     *
-v%************************************************************************
-
-\begin{code}
-plusAvail (Avail n1)      (Avail n2)       = Avail n1
-plusAvail (AvailTC n1 ns1) (AvailTC n2 ns2) = AvailTC n2 (ns1 `unionLists` ns2)
--- Added SOF 4/97
-#ifdef DEBUG
-plusAvail a1 a2 = pprPanic "RnEnv.plusAvail" (hsep [ppr a1,ppr a2])
-#endif
-
--------------------------
-pruneAvails :: (Name -> Bool)  -- Keep if this is True
-           -> [AvailInfo]
-           -> [AvailInfo]
-pruneAvails keep avails
-  = mapMaybe del avails
-  where
-    del :: AvailInfo -> Maybe AvailInfo        -- Nothing => nothing left!
-    del (Avail n) | keep n    = Just (Avail n)
-                 | otherwise = Nothing
-    del (AvailTC n ns) | null ns'  = Nothing
-                      | otherwise = Just (AvailTC n ns')
-                      where
-                        ns' = filter keep ns
-\end{code}
+%************************************************************************
 
 
----------------------------------------
-       AvailEnv and friends
----------------------------------------
+The @WhereFrom@ type controls where the renamer looks for an interface file
 
 \begin{code}
 
 \begin{code}
-type AvailEnv = NameEnv AvailInfo      -- Maps a Name to the AvailInfo that contains it
-
-emptyAvailEnv :: AvailEnv
-emptyAvailEnv = emptyNameEnv
+data WhereFrom 
+  = ImportByUser IsBootInterface       -- Ordinary user import (perhaps {-# SOURCE #-})
+  | ImportBySystem                     -- Non user import.
 
 
-unitAvailEnv :: AvailInfo -> AvailEnv
-unitAvailEnv a = unitNameEnv (availName a) a
+instance Outputable WhereFrom where
+  ppr (ImportByUser is_boot) | is_boot     = ptext (sLit "{- SOURCE -}")
+                            | otherwise   = empty
+  ppr ImportBySystem                      = ptext (sLit "{- SYSTEM -}")
+\end{code}
 
 
-plusAvailEnv :: AvailEnv -> AvailEnv -> AvailEnv
-plusAvailEnv = plusNameEnv_C plusAvail
 
 
-lookupAvailEnv_maybe :: AvailEnv -> Name -> Maybe AvailInfo
-lookupAvailEnv_maybe = lookupNameEnv
+%************************************************************************
+%*                                                                     *
+               Wanted constraints
+     These are forced to be in TcRnTypes because
+          TcLclEnv mentions WantedConstraints
+          WantedConstraint mentions CtLoc
+          CtLoc mentions ErrCtxt
+          ErrCtxt mentions TcM
+%*                                                                     *
+v%************************************************************************
 
 
-lookupAvailEnv :: AvailEnv -> Name -> AvailInfo
-lookupAvailEnv env n = case lookupNameEnv env n of
-                        Just avail -> avail
-                        Nothing    -> pprPanic "lookupAvailEnv" (ppr n)
+\begin{code}
+data WantedConstraints
+  = WC { wc_flat  :: Bag WantedEvVar   -- Unsolved constraints, all wanted
+       , wc_impl  :: Bag Implication
+       , wc_insol :: Bag FlavoredEvVar -- Insoluble constraints, can be
+                                       -- wanted, given, or derived
+                                       -- See Note [Insoluble constraints]
+    }
 
 
-availEnvElts = nameEnvElts
+emptyWC :: WantedConstraints
+emptyWC = WC { wc_flat = emptyBag, wc_impl = emptyBag, wc_insol = emptyBag }
+
+mkFlatWC :: Bag WantedEvVar -> WantedConstraints
+mkFlatWC wevs = WC { wc_flat = wevs, wc_impl = emptyBag, wc_insol = emptyBag }
+
+isEmptyWC :: WantedConstraints -> Bool
+isEmptyWC (WC { wc_flat = f, wc_impl = i, wc_insol = n })
+  = isEmptyBag f && isEmptyBag i && isEmptyBag n
+
+insolubleWC :: WantedConstraints -> Bool
+-- True if there are any insoluble constraints in the wanted bag
+insolubleWC wc = not (isEmptyBag (wc_insol wc))
+               || anyBag ic_insol (wc_impl wc)
+
+andWC :: WantedConstraints -> WantedConstraints -> WantedConstraints
+andWC (WC { wc_flat = f1, wc_impl = i1, wc_insol = n1 })
+      (WC { wc_flat = f2, wc_impl = i2, wc_insol = n2 })
+  = WC { wc_flat  = f1 `unionBags` f2
+       , wc_impl  = i1 `unionBags` i2
+       , wc_insol = n1 `unionBags` n2 }
+
+addFlats :: WantedConstraints -> Bag WantedEvVar -> WantedConstraints
+addFlats wc wevs = wc { wc_flat = wc_flat wc `unionBags` wevs }
+
+addImplics :: WantedConstraints -> Bag Implication -> WantedConstraints
+addImplics wc implic = wc { wc_impl = wc_impl wc `unionBags` implic }
+
+instance Outputable WantedConstraints where
+  ppr (WC {wc_flat = f, wc_impl = i, wc_insol = n})
+   = ptext (sLit "WC") <+> braces (vcat
+        [ if isEmptyBag f then empty else
+          ptext (sLit "wc_flat =")  <+> pprBag pprWantedEvVar f
+        , if isEmptyBag i then empty else
+          ptext (sLit "wc_impl =")  <+> pprBag ppr i
+        , if isEmptyBag n then empty else
+          ptext (sLit "wc_insol =") <+> pprBag ppr n ])
+
+pprBag :: (a -> SDoc) -> Bag a -> SDoc
+pprBag pp b = foldrBag (($$) . pp) empty b
+\end{code}
 
 
-addAvail :: AvailEnv -> AvailInfo -> AvailEnv
-addAvail avails avail = extendNameEnv_C plusAvail avails (availName avail) avail
+\begin{code}
+data Untouchables = NoUntouchables
+                  | TouchableRange
+                          Unique  -- Low end
+                          Unique  -- High end
+ -- A TcMetaTyvar is *touchable* iff its unique u satisfies
+ --   u >= low
+ --   u < high
+
+instance Outputable Untouchables where
+  ppr NoUntouchables = ptext (sLit "No untouchables")
+  ppr (TouchableRange low high) = ptext (sLit "Touchable range:") <+> 
+                                  ppr low <+> char '-' <+> ppr high
+
+isNoUntouchables :: Untouchables -> Bool
+isNoUntouchables NoUntouchables      = True
+isNoUntouchables (TouchableRange {}) = False
+
+inTouchableRange :: Untouchables -> TcTyVar -> Bool
+inTouchableRange NoUntouchables _ = True
+inTouchableRange (TouchableRange low high) tv 
+  = uniq >= low && uniq < high
+  where
+    uniq = varUnique tv
 
 
-mkAvailEnv :: [AvailInfo] -> AvailEnv
-       -- 'avails' may have several items with the same availName
-       -- E.g  import Ix( Ix(..), index )
-       -- will give Ix(Ix,index,range) and Ix(index)
-       -- We want to combine these; addAvail does that
-mkAvailEnv avails = foldl addAvail emptyAvailEnv avails
+-- EvVar defined in module Var.lhs:
+-- Evidence variables include all *quantifiable* constraints
+--   dictionaries
+--   implicit parameters
+--   coercion variables
 \end{code}
 
 %************************************************************************
 %*                                                                     *
 \end{code}
 
 %************************************************************************
 %*                                                                     *
-\subsection{Where from}
-%*                                                                     *
+                Implication constraints
+%*                                                                      *
 %************************************************************************
 
 %************************************************************************
 
-The @WhereFrom@ type controls where the renamer looks for an interface file
-
 \begin{code}
 \begin{code}
-data WhereFrom 
-  = ImportByUser IsBootInterface       -- Ordinary user import (perhaps {-# SOURCE #-})
-  | ImportBySystem                     -- Non user import.
+data Implication
+  = Implic {  
+      ic_untch :: Untouchables, -- Untouchables: unification variables
+                                -- free in the environment
+      ic_env   :: TcTypeEnv,    -- The type environment
+                                -- Used only when generating error messages
+         -- Generally, ic_untch is a superset of tvsof(ic_env)
+         -- However, we don't zonk ic_env when zonking the Implication
+         -- Instead we do that when generating a skolem-escape error message
+
+      ic_skols  :: TcTyVarSet,   -- Introduced skolems 
+                                -- See Note [Skolems in an implication]
+
+      ic_given  :: [EvVar],      -- Given evidence variables
+                                --   (order does not matter)
+      ic_loc   :: GivenLoc,      -- Binding location of the implication,
+                                 --   which is also the location of all the
+                                 --   given evidence variables
+
+      ic_wanted :: WantedConstraints,  -- The wanted
+      ic_insol  :: Bool,               -- True iff insolubleWC ic_wanted is true
+
+      ic_binds  :: EvBindsVar   -- Points to the place to fill in the
+                                -- abstraction and bindings
+    }
 
 
-instance Outputable WhereFrom where
-  ppr (ImportByUser is_boot) | is_boot     = ptext SLIT("{- SOURCE -}")
-                            | otherwise   = empty
-  ppr ImportBySystem                      = ptext SLIT("{- SYSTEM -}")
+instance Outputable Implication where
+  ppr (Implic { ic_untch = untch, ic_skols = skols, ic_given = given
+              , ic_wanted = wanted
+              , ic_binds = binds, ic_loc = loc })
+   = ptext (sLit "Implic") <+> braces 
+     (sep [ ptext (sLit "Untouchables = ") <+> ppr untch
+          , ptext (sLit "Skolems = ") <+> ppr skols
+          , ptext (sLit "Given = ") <+> pprEvVars given
+          , ptext (sLit "Wanted = ") <+> ppr wanted
+          , ptext (sLit "Binds = ") <+> ppr binds
+          , pprSkolInfo (ctLocOrigin loc)
+          , ppr (ctLocSpan loc) ])
 \end{code}
 
 \end{code}
 
+Note [Skolems in an implication]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The skolems in an implication are not there to perform a skolem escape
+check.  That happens because all the environment variables are in the
+untouchables, and therefore cannot be unified with anything at all,
+let alone the skolems.
+
+Instead, ic_skols is used only when considering floating a constraint
+outside the implication in TcSimplify.floatEqualities or 
+TcSimplify.approximateImplications
+
+Note [Insoluble constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Some of the errors that we get during canonicalization are best
+reported when all constraints have been simplified as much as
+possible. For instance, assume that during simplification the
+following constraints arise:
+   
+ [Wanted]   F alpha ~  uf1 
+ [Wanted]   beta ~ uf1 beta 
+
+When canonicalizing the wanted (beta ~ uf1 beta), if we eagerly fail
+we will simply see a message:
+    'Can't construct the infinite type  beta ~ uf1 beta' 
+and the user has no idea what the uf1 variable is.
+
+Instead our plan is that we will NOT fail immediately, but:
+    (1) Record the "frozen" error in the ic_insols field
+    (2) Isolate the offending constraint from the rest of the inerts 
+    (3) Keep on simplifying/canonicalizing
+
+At the end, we will hopefully have substituted uf1 := F alpha, and we
+will be able to report a more informative error:
+    'Can't construct the infinite type beta ~ F alpha beta'
 
 %************************************************************************
 %*                                                                     *
 
 %************************************************************************
 %*                                                                     *
-\subsection[Inst-types]{@Inst@ types}
+            EvVarX, WantedEvVar, FlavoredEvVar
 %*                                                                     *
 %*                                                                     *
-v%************************************************************************
+%************************************************************************
 
 
-An @Inst@ is either a dictionary, an instance of an overloaded
-literal, or an instance of an overloaded value.  We call the latter a
-``method'' even though it may not correspond to a class operation.
-For example, we might have an instance of the @double@ function at
-type Int, represented by
+\begin{code}
+data EvVarX a = EvVarX EvVar a
+     -- An evidence variable with accompanying info
 
 
-       Method 34 doubleId [Int] origin
+type WantedEvVar   = EvVarX WantedLoc     -- The location where it arose
+type FlavoredEvVar = EvVarX CtFlavor
 
 
-\begin{code}
-data Inst
-  = Dict
-       Name
-       TcPredType
-       InstLoc
-
-  | Method
-       Id
-
-       TcId    -- The overloaded function
-                       -- This function will be a global, local, or ClassOpId;
-                       --   inside instance decls (only) it can also be an InstId!
-                       -- The id needn't be completely polymorphic.
-                       -- You'll probably find its name (for documentation purposes)
-                       --        inside the InstOrigin
-
-       [TcType]        -- The types to which its polymorphic tyvars
-                       --      should be instantiated.
-                       -- These types must saturate the Id's foralls.
-
-       TcThetaType     -- The (types of the) dictionaries to which the function
-                       -- must be applied to get the method
-
-       InstLoc
-
-       -- INVARIANT 1: in (Method u f tys theta tau loc)
-       --      type of (f tys dicts(from theta)) = tau
-
-       -- INVARIANT 2: tau must not be of form (Pred -> Tau)
-       --   Reason: two methods are considered equal if the 
-       --           base Id matches, and the instantiating types
-       --           match.  The TcThetaType should then match too.
-       --   This only bites in the call to tcInstClassOp in TcClassDcl.mkMethodBind
-
-  | LitInst
-       Name
-       (HsOverLit Name)        -- The literal from the occurrence site
-                               -- INVARIANT: never a rebindable-syntax literal
-                               -- Reason: tcSyntaxName does unification, and we
-                               --         don't want to deal with that during tcSimplify,
-                               --         when resolving LitInsts
-       TcType          -- The type at which the literal is used
-       InstLoc
-\end{code}
+instance Outputable (EvVarX a) where
+  ppr (EvVarX ev _) = pprEvVarWithType ev
+  -- If you want to see the associated info,
+  -- use a more specific printing function
 
 
-@Insts@ are ordered by their class/type info, rather than by their
-unique.  This allows the context-reduction mechanism to use standard finite
-maps to do their stuff.
+mkEvVarX :: EvVar -> a -> EvVarX a
+mkEvVarX = EvVarX
 
 
-\begin{code}
-instance Ord Inst where
-  compare = cmpInst
+evVarOf :: EvVarX a -> EvVar
+evVarOf (EvVarX ev _) = ev
 
 
-instance Eq Inst where
-  (==) i1 i2 = case i1 `cmpInst` i2 of
-                EQ    -> True
-                other -> False
+evVarX :: EvVarX a -> a
+evVarX (EvVarX _ a) = a
 
 
-cmpInst (Dict _ pred1 _)       (Dict _ pred2 _)        = pred1 `tcCmpPred` pred2
-cmpInst (Dict _ _ _)           other                   = LT
+evVarOfPred :: EvVarX a -> PredType
+evVarOfPred wev = evVarPred (evVarOf wev)
 
 
-cmpInst (Method _ _ _ _ _)     (Dict _ _ _)            = GT
-cmpInst (Method _ id1 tys1 _ _) (Method _ id2 tys2 _ _) = (id1 `compare` id2) `thenCmp` (tys1 `tcCmpTypes` tys2)
-cmpInst (Method _ _ _ _ _)      other                  = LT
+wantedToFlavored :: WantedEvVar -> FlavoredEvVar
+wantedToFlavored (EvVarX v wl) = EvVarX v (Wanted wl)
 
 
-cmpInst (LitInst _ _ _ _)      (Dict _ _ _)            = GT
-cmpInst (LitInst _ _ _ _)      (Method _ _ _ _ _)      = GT
-cmpInst (LitInst _ lit1 ty1 _) (LitInst _ lit2 ty2 _)  = (lit1 `compare` lit2) `thenCmp` (ty1 `tcCmpType` ty2)
+keepWanted :: Bag FlavoredEvVar -> Bag WantedEvVar
+keepWanted flevs
+  = foldrBag keep_wanted emptyBag flevs
+    -- Important: use fold*r*Bag to preserve the order of the evidence variables.
+  where
+    keep_wanted :: FlavoredEvVar -> Bag WantedEvVar -> Bag WantedEvVar
+    keep_wanted (EvVarX ev (Wanted wloc)) r = consBag (EvVarX ev wloc) r
+    keep_wanted _                         r = r
 \end{code}
 
 
 \end{code}
 
 
+\begin{code}
+pprEvVars :: [EvVar] -> SDoc   -- Print with their types
+pprEvVars ev_vars = vcat (map pprEvVarWithType ev_vars)
+
+pprEvVarTheta :: [EvVar] -> SDoc
+pprEvVarTheta ev_vars = pprTheta (map evVarPred ev_vars)
+                              
+pprEvVarWithType :: EvVar -> SDoc
+pprEvVarWithType v = ppr v <+> dcolon <+> pprPredTy (evVarPred v)
+
+pprWantedsWithLocs :: WantedConstraints -> SDoc
+pprWantedsWithLocs wcs
+  =  vcat [ pprBag pprWantedEvVarWithLoc (wc_flat wcs)
+          , pprBag ppr (wc_impl wcs)
+          , pprBag ppr (wc_insol wcs) ]
+
+pprWantedEvVarWithLoc, pprWantedEvVar :: WantedEvVar -> SDoc
+pprWantedEvVarWithLoc (EvVarX v loc) = hang (pprEvVarWithType v)
+                                          2 (pprArisingAt loc)
+pprWantedEvVar        (EvVarX v _)   = pprEvVarWithType v
+\end{code}
+
 %************************************************************************
 %*                                                                     *
 %************************************************************************
 %*                                                                     *
-\subsection[Inst-collections]{LIE: a collection of Insts}
+            CtLoc
 %*                                                                     *
 %************************************************************************
 
 \begin{code}
 %*                                                                     *
 %************************************************************************
 
 \begin{code}
--- FIXME: Rename this. It clashes with (Located (IE ...))
-type LIE = Bag Inst
-
-isEmptyLIE       = isEmptyBag
-emptyLIE          = emptyBag
-unitLIE inst     = unitBag inst
-mkLIE insts      = listToBag insts
-plusLIE lie1 lie2 = lie1 `unionBags` lie2
-consLIE inst lie  = inst `consBag` lie
-plusLIEs lies    = unionManyBags lies
-lieToList        = bagToList
-listToLIE        = listToBag
+data CtFlavor
+  = Given GivenLoc GivenKind -- We have evidence for this constraint in TcEvBinds
+  | Derived WantedLoc        -- Derived's are just hints for unifications 
+  | Wanted WantedLoc         -- We have no evidence bindings for this constraint. 
+
+data GivenKind
+  = GivenOrig   -- Originates in some given, such as signature or pattern match
+  | GivenSolved -- Is given as result of being solved, maybe provisionally on
+                -- some other wanted constraints. 
+
+instance Outputable CtFlavor where
+  ppr (Given _ GivenOrig)   = ptext (sLit "[G]")
+  ppr (Given _ GivenSolved) = ptext (sLit "[S]") -- Print [S] for Given/Solved's
+  ppr (Wanted {})           = ptext (sLit "[W]")
+  ppr (Derived {})          = ptext (sLit "[D]") 
+
+pprFlavorArising :: CtFlavor -> SDoc
+pprFlavorArising (Derived wl)   = pprArisingAt wl
+pprFlavorArising (Wanted  wl)   = pprArisingAt wl
+pprFlavorArising (Given gl _)   = pprArisingAt gl
+
+isWanted :: CtFlavor -> Bool
+isWanted (Wanted {}) = True
+isWanted _           = False
+
+isGivenOrSolved :: CtFlavor -> Bool
+isGivenOrSolved (Given {}) = True
+isGivenOrSolved _ = False
+
+isGiven_maybe :: CtFlavor -> Maybe GivenKind 
+isGiven_maybe (Given _ gk) = Just gk
+isGiven_maybe _            = Nothing
+
+isDerived :: CtFlavor -> Bool 
+isDerived (Derived {}) = True
+isDerived _            = False
 \end{code}
 
 \end{code}
 
-
 %************************************************************************
 %*                                                                     *
 %************************************************************************
 %*                                                                     *
-\subsection[Inst-origin]{The @InstOrigin@ type}
+            CtLoc
 %*                                                                     *
 %************************************************************************
 
 %*                                                                     *
 %************************************************************************
 
-The @InstOrigin@ type gives information about where a dictionary came from.
-This is important for decent error message reporting because dictionaries
-don't appear in the original source code.  Doubtless this type will evolve...
+The 'CtLoc' gives information about where a constraint came from.
+This is important for decent error message reporting because
+dictionaries don't appear in the original source code.
+type will evolve...
+
+\begin{code}
+data CtLoc orig = CtLoc orig SrcSpan [ErrCtxt]
+
+type WantedLoc = CtLoc CtOrigin      -- Instantiation for wanted constraints
+type GivenLoc  = CtLoc SkolemInfo    -- Instantiation for given constraints
+
+ctLocSpan :: CtLoc o -> SrcSpan
+ctLocSpan (CtLoc _ s _) = s
 
 
-It appears in TcMonad because there are a couple of error-message-generation
-functions that deal with it.
+ctLocOrigin :: CtLoc o -> o
+ctLocOrigin (CtLoc o _ _) = o
+
+setCtLocOrigin :: CtLoc o -> o' -> CtLoc o'
+setCtLocOrigin (CtLoc _ s c) o = CtLoc o s c
+
+pushErrCtxt :: orig -> ErrCtxt -> CtLoc orig -> CtLoc orig
+pushErrCtxt o err (CtLoc _ s errs) = CtLoc o s (err:errs)
+
+pprArising :: CtOrigin -> SDoc
+-- Used for the main, top-level error message
+-- We've done special processing for TypeEq and FunDep origins
+pprArising (TypeEqOrigin {}) = empty
+pprArising FunDepOrigin      = empty
+pprArising orig              = text "arising from" <+> ppr orig
+
+pprArisingAt :: Outputable o => CtLoc o -> SDoc
+pprArisingAt (CtLoc o s _) = sep [ text "arising from" <+> ppr o
+                                 , text "at" <+> ppr s]
+\end{code}
+
+%************************************************************************
+%*                                                                      *
+                SkolemInfo
+%*                                                                      *
+%************************************************************************
 
 \begin{code}
 
 \begin{code}
-data InstLoc = InstLoc InstOrigin SrcSpan ErrCtxt
+-- SkolemInfo gives the origin of *given* constraints
+--   a) type variables are skolemised
+--   b) an implication constraint is generated
+data SkolemInfo
+  = SigSkol UserTypeCtxt       -- A skolem that is created by instantiating
+            Type                -- a programmer-supplied type signature
+                               -- Location of the binding site is on the TyVar
+
+       -- The rest are for non-scoped skolems
+  | ClsSkol Class      -- Bound at a class decl
+  | InstSkol           -- Bound at an instance decl
+  | DataSkol            -- Bound at a data type declaration
+  | FamInstSkol         -- Bound at a family instance decl
+  | PatSkol            -- An existential type variable bound by a pattern for
+      DataCon           -- a data constructor with an existential type.
+      (HsMatchContext Name)    
+            -- e.g.   data T = forall a. Eq a => MkT a
+            --        f (MkT x) = ...
+            -- The pattern MkT x will allocate an existential type
+            -- variable for 'a'.  
+
+  | ArrowSkol          -- An arrow form (see TcArrows)
+
+  | IPSkol [IPName Name]  -- Binding site of an implicit parameter
+
+  | RuleSkol RuleName  -- The LHS of a RULE
+
+  | InferSkol [(Name,TcType)]
+                        -- We have inferred a type for these (mutually-recursivive)
+                        -- polymorphic Ids, and are now checking that their RHS
+                        -- constraints are satisfied.
+
+  | BracketSkol         -- Template Haskell bracket
+
+  | UnkSkol             -- Unhelpful info (until I improve it)
+
+instance Outputable SkolemInfo where
+  ppr = pprSkolInfo
+
+pprSkolInfo :: SkolemInfo -> SDoc
+-- Complete the sentence "is a rigid type variable bound by..."
+pprSkolInfo (SigSkol (FunSigCtxt f) ty)
+                            = hang (ptext (sLit "the type signature for"))
+                                 2 (ppr f <+> dcolon <+> ppr ty)
+pprSkolInfo (SigSkol cx ty) = hang (pprUserTypeCtxt cx <> colon)
+                                 2 (ppr ty)
+pprSkolInfo (IPSkol ips)    = ptext (sLit "the implicit-parameter bindings for")
+                              <+> pprWithCommas ppr ips
+pprSkolInfo (ClsSkol cls)   = ptext (sLit "the class declaration for") <+> quotes (ppr cls)
+pprSkolInfo InstSkol        = ptext (sLit "the instance declaration")
+pprSkolInfo DataSkol        = ptext (sLit "the data type declaration")
+pprSkolInfo FamInstSkol     = ptext (sLit "the family instance declaration")
+pprSkolInfo BracketSkol     = ptext (sLit "a Template Haskell bracket")
+pprSkolInfo (RuleSkol name) = ptext (sLit "the RULE") <+> doubleQuotes (ftext name)
+pprSkolInfo ArrowSkol       = ptext (sLit "the arrow form")
+pprSkolInfo (PatSkol dc mc)  = sep [ ptext (sLit "a pattern with constructor")
+                                   , nest 2 $ ppr dc <+> dcolon
+                                              <+> ppr (dataConUserType dc) <> comma
+                                  , ptext (sLit "in") <+> pprMatchContext mc ]
+pprSkolInfo (InferSkol ids) = sep [ ptext (sLit "the inferred type of")
+                                  , vcat [ ppr name <+> dcolon <+> ppr ty
+                                         | (name,ty) <- ids ]]
+
+-- UnkSkol
+-- For type variables the others are dealt with by pprSkolTvBinding.  
+-- For Insts, these cases should not happen
+pprSkolInfo UnkSkol = WARN( True, text "pprSkolInfo: UnkSkol" ) ptext (sLit "UnkSkol")
+\end{code}
 
 
-instLocSrcLoc :: InstLoc -> SrcLoc
-instLocSrcLoc (InstLoc _ src_span _) = srcSpanStart src_span
 
 
-instLocSrcSpan :: InstLoc -> SrcSpan
-instLocSrcSpan (InstLoc _ src_span _) = src_span
+%************************************************************************
+%*                                                                     *
+            CtOrigin
+%*                                                                     *
+%************************************************************************
 
 
-data InstOrigin
-  = SigOrigin SkolemInfo       -- Pattern, class decl, inst decl etc;
-                               -- Places that bind type variables and introduce
-                               -- available constraints
+\begin{code}
+-- CtOrigin gives the origin of *wanted* constraints
+data CtOrigin
+  = OccurrenceOf Name          -- Occurrence of an overloaded identifier
+  | AppOrigin                  -- An application of some kind
 
 
-  | IPBindOrigin (IPName Name) -- Binding site of an implicit parameter
+  | SpecPragOrigin Name                -- Specialisation pragma for identifier
 
 
-       -------------------------------------------------------
-       -- The rest are all occurrences: Insts that are 'wanted'
-       -------------------------------------------------------
-  | OccurrenceOf Name          -- Occurrence of an overloaded identifier
+  | TypeEqOrigin EqOrigin
 
   | IPOccOrigin  (IPName Name) -- Occurrence of an implicit parameter
 
   | LiteralOrigin (HsOverLit Name)     -- Occurrence of a literal
 
   | IPOccOrigin  (IPName Name) -- Occurrence of an implicit parameter
 
   | LiteralOrigin (HsOverLit Name)     -- Occurrence of a literal
+  | NegateOrigin                       -- Occurrence of syntactic negation
 
   | ArithSeqOrigin (ArithSeqInfo Name) -- [x..], [x..y] etc
   | PArrSeqOrigin  (ArithSeqInfo Name) -- [:x..y:] and [:x,y..z:]
 
   | ArithSeqOrigin (ArithSeqInfo Name) -- [x..], [x..y] etc
   | PArrSeqOrigin  (ArithSeqInfo Name) -- [:x..y:] and [:x,y..z:]
-
-  | InstSigOrigin      -- A dict occurrence arising from instantiating
-                       -- a polymorphic type during a subsumption check
-
+  | SectionOrigin
+  | TupleOrigin                               -- (..,..)
+  | ExprSigOrigin      -- e :: ty
+  | PatSigOrigin       -- p :: ty
+  | PatOrigin          -- Instantiating a polytyped pattern at a constructor
   | RecordUpdOrigin
   | RecordUpdOrigin
-  | InstScOrigin       -- Typechecking superclasses of an instance declaration
+  | ViewPatOrigin
+
+  | ScOrigin           -- Typechecking superclasses of an instance declaration
   | DerivOrigin                -- Typechecking deriving
   | DerivOrigin                -- Typechecking deriving
+  | StandAloneDerivOrigin -- Typechecking stand-alone deriving
   | DefaultOrigin      -- Typechecking a default decl
   | DoOrigin           -- Arising from a do expression
   | DefaultOrigin      -- Typechecking a default decl
   | DoOrigin           -- Arising from a do expression
+  | MCompOrigin         -- Arising from a monad comprehension
+  | IfOrigin            -- Arising from an if statement
   | ProcOrigin         -- Arising from a proc expression
   | ProcOrigin         -- Arising from a proc expression
+  | AnnOrigin           -- An annotation
+  | FunDepOrigin
+
+data EqOrigin 
+  = UnifyOrigin 
+       { uo_actual   :: TcType
+       , uo_expected :: TcType }
+
+instance Outputable CtOrigin where
+  ppr orig = pprO orig
+
+pprO :: CtOrigin -> SDoc
+pprO (OccurrenceOf name)   = hsep [ptext (sLit "a use of"), quotes (ppr name)]
+pprO AppOrigin             = ptext (sLit "an application")
+pprO (SpecPragOrigin name) = hsep [ptext (sLit "a specialisation pragma for"), quotes (ppr name)]
+pprO (IPOccOrigin name)    = hsep [ptext (sLit "a use of implicit parameter"), quotes (ppr name)]
+pprO RecordUpdOrigin       = ptext (sLit "a record update")
+pprO ExprSigOrigin         = ptext (sLit "an expression type signature")
+pprO PatSigOrigin          = ptext (sLit "a pattern type signature")
+pprO PatOrigin             = ptext (sLit "a pattern")
+pprO ViewPatOrigin         = ptext (sLit "a view pattern")
+pprO IfOrigin              = ptext (sLit "an if statement")
+pprO (LiteralOrigin lit)   = hsep [ptext (sLit "the literal"), quotes (ppr lit)]
+pprO (ArithSeqOrigin seq)  = hsep [ptext (sLit "the arithmetic sequence"), quotes (ppr seq)]
+pprO (PArrSeqOrigin seq)   = hsep [ptext (sLit "the parallel array sequence"), quotes (ppr seq)]
+pprO SectionOrigin        = ptext (sLit "an operator section")
+pprO TupleOrigin          = ptext (sLit "a tuple")
+pprO NegateOrigin         = ptext (sLit "a use of syntactic negation")
+pprO ScOrigin             = ptext (sLit "the superclasses of an instance declaration")
+pprO DerivOrigin          = ptext (sLit "the 'deriving' clause of a data type declaration")
+pprO StandAloneDerivOrigin = ptext (sLit "a 'deriving' declaration")
+pprO DefaultOrigin        = ptext (sLit "a 'default' declaration")
+pprO DoOrigin             = ptext (sLit "a do statement")
+pprO MCompOrigin           = ptext (sLit "a statement in a monad comprehension")
+pprO ProcOrigin                   = ptext (sLit "a proc expression")
+pprO (TypeEqOrigin eq)     = ptext (sLit "an equality") <+> ppr eq
+pprO AnnOrigin             = ptext (sLit "an annotation")
+pprO FunDepOrigin          = ptext (sLit "a functional dependency")
+
+instance Outputable EqOrigin where
+  ppr (UnifyOrigin t1 t2) = ppr t1 <+> char '~' <+> ppr t2
 \end{code}
 
 \end{code}
 
-\begin{code}
-pprInstLoc :: InstLoc -> SDoc
-pprInstLoc (InstLoc orig locn _)
-  = hsep [text "arising from", pp_orig orig, text "at", ppr locn]
-  where
-    pp_orig (OccurrenceOf name)  = hsep [ptext SLIT("use of"), quotes (ppr name)]
-    pp_orig (IPOccOrigin name)   = hsep [ptext SLIT("use of implicit parameter"), quotes (ppr name)]
-    pp_orig (IPBindOrigin name)  = hsep [ptext SLIT("binding for implicit parameter"), quotes (ppr name)]
-    pp_orig RecordUpdOrigin     = ptext SLIT("a record update")
-    pp_orig (LiteralOrigin lit)         = hsep [ptext SLIT("the literal"), quotes (ppr lit)]
-    pp_orig (ArithSeqOrigin seq) = hsep [ptext SLIT("the arithmetic sequence"), quotes (ppr seq)]
-    pp_orig (PArrSeqOrigin seq)         = hsep [ptext SLIT("the parallel array sequence"), quotes (ppr seq)]
-    pp_orig InstSigOrigin       = ptext SLIT("instantiating a type signature")
-    pp_orig InstScOrigin        = ptext SLIT("the superclasses of an instance declaration")
-    pp_orig DerivOrigin                 = ptext SLIT("the 'deriving' clause of a data type declaration")
-    pp_orig DefaultOrigin       = ptext SLIT("a 'default' declaration")
-    pp_orig DoOrigin            = ptext SLIT("a do statement")
-    pp_orig ProcOrigin          = ptext SLIT("a proc expression")
-    pp_orig (SigOrigin info)    = pprSkolInfo info
-\end{code}