Initial checkin of HetMet / -XModalTypes modifications
[ghc-hetmet.git] / compiler / typecheck / TcRnTypes.lhs
index a91e95e..eee07e8 100644 (file)
@@ -18,7 +18,7 @@ module TcRnTypes(
        WhereFrom(..), mkModDeps,
 
        -- Typechecker types
-       TcTyThing(..), pprTcTyThingCategory, RefinementVisibility(..),
+       TcTypeEnv, TcTyThing(..), pprTcTyThingCategory, 
 
        -- Template Haskell
        ThStage(..), topStage, topAnnStage, topSpliceStage,
@@ -27,23 +27,43 @@ module TcRnTypes(
        -- Arrows
        ArrowCtxt(NoArrowCtxt), newArrowScope, escapeArrowScope,
 
-       -- Insts
-       Inst(..), EqInstCo, InstOrigin(..), InstLoc(..), 
-       pprInstLoc, pprInstArising, instLocSpan, instLocOrigin, setInstLoc,
-       LIE, emptyLIE, unitLIE, plusLIE, consLIE, instLoc, instSpan,
-       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, pushErrCtxt,
+
+        SkolemInfo(..),
+
+        CtFlavor(..), pprFlavorArising, isWanted, isGiven, isDerived,
+        FlavoredEvVar,
+
+       -- Pretty printing
+        pprEvVarTheta, pprWantedEvVar, pprWantedsWithLocs,
+       pprEvVars, pprEvVarWithType,
+        pprArising, pprArisingAt,
 
        -- Misc other types
-       TcId, TcIdSet, TcDictBinds, TcTyVarBind(..), TcTyVarBinds
+       TcId, TcIdSet, TcTyVarBind(..), TcTyVarBinds
        
   ) where
 
 #include "HsVersions.h"
 
-import HsSyn hiding (LIE)
+import HsSyn
 import HscTypes
 import Type
-import Coercion
+import Class    ( Class )
+import DataCon  ( DataCon, dataConUserType )
 import TcType
 import Annotations
 import InstEnv
@@ -56,13 +76,13 @@ import NameSet
 import Var
 import VarEnv
 import Module
-import LazyUniqFM
 import SrcLoc
 import VarSet
 import ErrUtils
+import UniqFM
 import UniqSupply
+import Unique
 import BasicTypes
-import Util
 import Bag
 import Outputable
 import ListSetOps
@@ -83,9 +103,9 @@ The monad itself has to be defined here, because it is mentioned by ErrCtxt
 
 \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 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
@@ -204,22 +224,13 @@ data TcGblEnv
           --
           --   * 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,
+        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
+          -- 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,
@@ -233,12 +244,19 @@ data TcGblEnv
         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
@@ -354,8 +372,9 @@ 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
 
-       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, 
@@ -363,13 +382,18 @@ data TcLclEnv             -- Changes as we move inside an expression
                        -- in tcl_lenv. 
                         -- Why mutable? see notes with tcGetGlobalTyVars
 
-       tcl_lie   :: TcRef LIE,         -- Place to accumulate type constraints
+       tcl_lie   :: TcRef WantedConstraints,    -- Place to accumulate type constraints
 
-        tcl_tybinds :: TcRef TcTyVarBinds -- Meta and coercion type variable
-                                          -- bindings accumulated during
-                                          -- constraint solving
+       -- 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 TcTypeEnv = NameEnv TcTyThing
+
 
 {- Note [Given Insts]
    ~~~~~~~~~~~~~~~~~~
@@ -401,7 +425,7 @@ data ThStage        -- See Note [Template Haskell state diagram] in TcSplice
   | Brack                      -- Inside brackets 
       ThStage                  --   Binding level = level(stage) + 1
       (TcRef [PendingSplice])  --   Accumulate pending splices here
-      (TcRef LIE)              --     and type constraints here
+      (TcRef WantedConstraints)        --     and type constraints here
 
 topStage, topAnnStage, topSpliceStage :: ThStage
 topStage       = Comp
@@ -484,41 +508,26 @@ data TcTyThing
   = AGlobal TyThing            -- Used only in the return type of a lookup
 
   | ATcId   {          -- Ids defined in this module; may not be fully zonked
-       tct_id :: TcId,         
-       tct_co :: RefinementVisibility, -- Previously: Maybe HsWrapper
-                                       -- Nothing <=>  Do not apply a GADT type refinement
-                                       --              I am wobbly, or have no free
-                                       --              type variables
-                                       -- Just co <=>  Apply any type refinement to me,
-                                       --              and record it in the coercion
-       tct_type  :: TcType,    -- Type of (coercion applied to id)
-       tct_level :: ThLevel }
+       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
-                               -- 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
 
-data RefinementVisibility
-  = Unrefineable                       -- Do not apply a GADT refinement
-                                       -- I have no free variables     
-
-  | Rigid HsWrapper                    -- Apply any refinement to me
-                                       -- and record it in the coercion
-
-  | Wobbly                             -- Do not apply a GADT refinement
-                                       -- I am wobbly
-
-  | WobblyInvisible                    -- Wobbly type, not available inside current
-                                       -- GADT refinement
-
 instance Outputable TcTyThing where    -- Debugging only
    ppr (AGlobal g)      = pprTyThing g
    ppr elt@(ATcId {})   = text "Identifier" <> 
-                         ifPprDebug (brackets (ppr (tct_id elt) <> dcolon <> ppr (tct_type elt) <> comma
-                                <+> ppr (tct_level elt) <+> ppr (tct_co elt)))
+                         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
 
@@ -527,13 +536,6 @@ pprTcTyThingCategory (AGlobal thing) = pprTyThingCategory thing
 pprTcTyThingCategory (ATyVar {})     = ptext (sLit "Type variable")
 pprTcTyThingCategory (ATcId {})      = ptext (sLit "Local identifier")
 pprTcTyThingCategory (AThing {})     = ptext (sLit "Kinded thing")
-
-instance Outputable RefinementVisibility where
-    ppr Unrefineable         = ptext (sLit "unrefineable")
-    ppr (Rigid co)           = ptext (sLit "rigid") <+> ppr co
-    ppr        Wobbly                = ptext (sLit "wobbly")
-    ppr WobblyInvisible              = ptext (sLit "wobbly-invisible")
-
 \end{code}
 
 \begin{code}
@@ -674,269 +676,429 @@ instance Outputable WhereFrom where
 
 %************************************************************************
 %*                                                                     *
-\subsection[Inst-types]{@Inst@ types}
+               Wanted constraints
+
+     These are forced to be in TcRnTypes because
+          TcLclEnv mentions WantedConstraints
+          WantedConstraint mentions CtLoc
+          CtLoc mentions ErrCtxt
+          ErrCtxt mentions TcM
 %*                                                                     *
 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
-
-       Method 34 doubleId [Int] origin
-
-In addition to the basic Haskell variants of 'Inst's, they can now also
-represent implication constraints 'forall tvs. given => wanted'
-and equality constraints 'co :: ty1 ~ ty2'.
+\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]
+    }
 
-NB: Equalities occur in two flavours:
+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 = wevs `unionBags` wc_flat wc }
+
+addImplics :: WantedConstraints -> Bag Implication -> WantedConstraints
+addImplics wc implic = wc { wc_impl = implic `unionBags` wc_impl wc }
+
+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}
 
-  (1) Dict {tci_pred = EqPred ty1 ty2}
-  (2) EqInst {tci_left = ty1, tci_right = ty2, tci_co = coe}
+\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
 
-The former arises from equalities in contexts, whereas the latter is used
-whenever the type checker introduces an equality (e.g., during deferring
-unification).
+-- EvVar defined in module Var.lhs:
+-- Evidence variables include all *quantifiable* constraints
+--   dictionaries
+--   implicit parameters
+--   coercion variables
+\end{code}
 
-I am not convinced that this duplication is necessary or useful! -=chak
+%************************************************************************
+%*                                                                     *
+                Implication constraints
+%*                                                                      *
+%************************************************************************
 
 \begin{code}
-data Inst
-  = Dict {
-       tci_name :: Name,
-       tci_pred :: TcPredType,   -- Class or implicit parameter only
-       tci_loc  :: InstLoc 
+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
     }
 
-  | ImplicInst {       -- An implication constraint
-                       -- forall tvs. given => wanted
-       tci_name   :: Name,
-       tci_tyvars :: [TcTyVar],    -- Quantified type variables
-       tci_given  :: [Inst],       -- Only Dicts and EqInsts
-                                   --   (no Methods, LitInsts, ImplicInsts)
-       tci_wanted :: [Inst],       -- Only Dicts, EqInst, and ImplicInsts
-                                   --   (no Methods or LitInsts)
+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}
 
-       tci_loc    :: InstLoc
-    }
-       -- NB: the tci_given are not necessarily rigid
+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'
 
-  | Method {
-       tci_id :: TcId,         -- The Id for the Inst
+%************************************************************************
+%*                                                                     *
+            EvVarX, WantedEvVar, FlavoredEvVar
+%*                                                                     *
+%************************************************************************
 
-       tci_oid :: 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
+\begin{code}
+data EvVarX a = EvVarX EvVar a
+     -- An evidence variable with accompanying info
 
-       tci_tys :: [TcType],    -- The types to which its polymorphic tyvars
-                               --      should be instantiated.
-                               -- These types must saturate the Id's foralls.
+type WantedEvVar   = EvVarX WantedLoc     -- The location where it arose
+type FlavoredEvVar = EvVarX CtFlavor
 
-       tci_theta :: TcThetaType,       
-                       -- The (types of the) dictionaries to which the function
-                       -- must be applied to get the method
+instance Outputable (EvVarX a) where
+  ppr (EvVarX ev _) = pprEvVarWithType ev
+  -- If you want to see the associated info,
+  -- use a more specific printing function
 
-       tci_loc :: InstLoc 
-    }
-       -- INVARIANT 1: in (Method m f tys theta tau loc)
-       --      type of m = type of (f tys dicts(from theta))
-
-       -- INVARIANT 2: type of m 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 {
-       tci_name :: Name,
-       tci_lit  :: 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
-
-       tci_ty :: TcType,       -- The type at which the literal is used
-       tci_loc :: InstLoc
-    }
+mkEvVarX :: EvVar -> a -> EvVarX a
+mkEvVarX = EvVarX
 
-  | EqInst {                     -- delayed unification of the form 
-                                 --    co :: ty1 ~ ty2
-       tci_left  :: TcType,      -- ty1    -- both types are...
-       tci_right :: TcType,      -- ty2    -- ...free of boxes
-       tci_co    :: EqInstCo,            -- co
-       tci_loc   :: InstLoc,
-
-       tci_name  :: Name       -- Debugging help only: this makes it easier to
-                               -- follow where a constraint is used in a morass
-                               -- of trace messages!  Unlike other Insts, it 
-                                -- has no semantic significance whatsoever.
-    }
+evVarOf :: EvVarX a -> EvVar
+evVarOf (EvVarX ev _) = ev
+
+evVarX :: EvVarX a -> a
+evVarX (EvVarX _ a) = a
+
+evVarOfPred :: EvVarX a -> PredType
+evVarOfPred wev = evVarPred (evVarOf wev)
 
-type EqInstCo = Either           -- Distinguish between given and wanted coercions
-                 TcTyVar   --  - a wanted equation, with a hole, to be filled
-                           --    with a witness for the equality; for equation
-                            --    arising from deferring unification, 'ty1' is
-                            --    the actual and 'ty2' the expected type
-                 Coercion  --  - a given equation, with a coercion witnessing
-                            --    the equality; a coercion that originates
-                            --    from a signature or a GADT is a CoVar, but
-                            --    after normalisation of coercions, they can
-                           --    be arbitrary Coercions involving constructors 
-                            --    and pseudo-constructors like sym and trans.
+wantedToFlavored :: WantedEvVar -> FlavoredEvVar
+wantedToFlavored (EvVarX v wl) = EvVarX v (Wanted wl)
+
+keepWanted :: Bag FlavoredEvVar -> Bag WantedEvVar
+keepWanted flevs
+  = foldlBag keep_wanted emptyBag flevs
+  where
+    keep_wanted :: Bag WantedEvVar -> FlavoredEvVar -> Bag WantedEvVar
+    keep_wanted r (EvVarX ev (Wanted wloc)) = consBag (EvVarX ev wloc) r
+    keep_wanted r _ = r
 \end{code}
 
-@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.  It's horrible that this code is here, rather
-than with the Avails handling stuff in TcSimplify
 
 \begin{code}
-instance Ord Inst where
-   compare = cmpInst
-       -- Used *only* for AvailEnv in TcSimplify
-
-instance Eq Inst where
-  (==) i1 i2 = case i1 `cmpInst` i2 of
-               EQ -> True
-               _  -> False
-
-cmpInst :: Inst -> Inst -> Ordering
-cmpInst d1@(Dict {})   d2@(Dict {})    = tci_pred d1 `tcCmpPred` tci_pred d2
-cmpInst (Dict {})       _               = LT
-
-cmpInst (Method {})    (Dict {})       = GT
-cmpInst m1@(Method {})         m2@(Method {})  = (tci_oid m1 `compare` tci_oid m2) `thenCmp`
-                                         (tci_tys m1 `tcCmpTypes` tci_tys m2)
-cmpInst (Method {})     _               = LT
-
-cmpInst (LitInst {})   (Dict {})       = GT
-cmpInst (LitInst {})   (Method {})     = GT
-cmpInst l1@(LitInst {})        l2@(LitInst {}) = (tci_lit l1 `compare` tci_lit l2) `thenCmp`
-                                         (tci_ty l1 `tcCmpType` tci_ty l2)
-cmpInst (LitInst {})    _               = LT
-
-       -- Implication constraints are compared by *name*
-       -- not by type; that is, we make no attempt to do CSE on them
-cmpInst (ImplicInst {})    (Dict {})         = GT
-cmpInst (ImplicInst {})    (Method {})       = GT
-cmpInst (ImplicInst {})    (LitInst {})              = GT
-cmpInst i1@(ImplicInst {}) i2@(ImplicInst {}) = tci_name i1 `compare` tci_name i2
-cmpInst (ImplicInst {})    _                  = LT
-
-       -- same for Equality constraints
-cmpInst (EqInst {})    (Dict {})       = GT
-cmpInst (EqInst {})    (Method {})     = GT
-cmpInst (EqInst {})    (LitInst {})    = GT
-cmpInst (EqInst {})    (ImplicInst {}) = GT
-cmpInst i1@(EqInst {}) i2@(EqInst {})  = (tci_left  i1 `tcCmpType` tci_left  i2) `thenCmp`
-                                         (tci_right i1 `tcCmpType` tci_right i2)
+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 <+> pprPred (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}
 
+%************************************************************************
+%*                                                                     *
+            CtLoc
+%*                                                                     *
+%************************************************************************
+
+\begin{code}
+data CtFlavor
+  = Given   GivenLoc  -- We have evidence for this constraint in TcEvBinds
+  | Derived WantedLoc 
+                      -- We have evidence for this constraint in TcEvBinds;
+                      --   *however* this evidence can contain wanteds, so 
+                      --   it's valid only provisionally to the solution of
+                      --   these wanteds 
+  | Wanted WantedLoc  -- We have no evidence bindings for this constraint. 
+
+-- data DerivedOrig = DerSC | DerInst | DerSelf
+-- Deriveds are either superclasses of other wanteds or deriveds, or partially
+-- solved wanteds from instances, or 'self' dictionaries containing yet wanted
+-- superclasses. 
+
+instance Outputable CtFlavor where
+  ppr (Given _)    = ptext (sLit "[Given]")
+  ppr (Wanted _)   = ptext (sLit "[Wanted]")
+  ppr (Derived {}) = ptext (sLit "[Derived]") 
+
+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
+
+isGiven :: CtFlavor -> Bool 
+isGiven (Given {}) = True 
+isGiven _          = False 
+
+isDerived :: CtFlavor -> Bool 
+isDerived (Derived {}) = True
+isDerived _            = False
+\end{code}
 
 %************************************************************************
 %*                                                                     *
-\subsection[Inst-collections]{LIE: a collection of Insts}
+            CtLoc
 %*                                                                     *
 %************************************************************************
 
+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}
--- FIXME: Rename this. It clashes with (Located (IE ...))
-type LIE = Bag Inst
+data CtLoc orig = CtLoc orig SrcSpan [ErrCtxt]
 
-isEmptyLIE :: LIE -> Bool
-isEmptyLIE = isEmptyBag
+type WantedLoc = CtLoc CtOrigin      -- Instantiation for wanted constraints
+type GivenLoc  = CtLoc SkolemInfo    -- Instantiation for given constraints
 
-emptyLIE :: LIE
-emptyLIE = emptyBag
+ctLocSpan :: CtLoc o -> SrcSpan
+ctLocSpan (CtLoc _ s _) = s
 
-unitLIE :: Inst -> LIE
-unitLIE inst = unitBag inst
+ctLocOrigin :: CtLoc o -> o
+ctLocOrigin (CtLoc o _ _) = o
 
-mkLIE :: [Inst] -> LIE
-mkLIE insts = listToBag insts
+setCtLocOrigin :: CtLoc o -> o' -> CtLoc o'
+setCtLocOrigin (CtLoc _ s c) o = CtLoc o s c
 
-plusLIE :: LIE -> LIE -> LIE
-plusLIE lie1 lie2 = lie1 `unionBags` lie2
+pushErrCtxt :: orig -> ErrCtxt -> CtLoc orig -> CtLoc orig
+pushErrCtxt o err (CtLoc _ s errs) = CtLoc o s (err:errs)
 
-plusLIEs :: [LIE] -> LIE
-plusLIEs lies = unionManyBags lies
+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
 
-lieToList :: LIE -> [Inst]
-lieToList = bagToList
+pprArisingAt :: Outputable o => CtLoc o -> SDoc
+pprArisingAt (CtLoc o s _) = sep [ text "arising from" <+> ppr o
+                                 , text "at" <+> ppr s]
+\end{code}
 
-listToLIE :: [Inst] -> LIE
-listToLIE = listToBag
+%************************************************************************
+%*                                                                      *
+                SkolemInfo
+%*                                                                      *
+%************************************************************************
 
-consLIE :: Inst -> LIE -> LIE
-consLIE inst lie  = lie `snocBag` inst
--- Putting the new Inst at the *end* of the bag is a half-hearted attempt
--- to ensure that we tend to report the *leftmost* type-constraint error
--- E.g.        f :: [a]
---             f = [1,2,3]
--- we'd like to complain about the '1', not the '3'.
---
--- "Half-hearted" because the rest of the type checker makes no great
--- claims for retaining order in the constraint set.  Still, this 
--- seems to improve matters slightly.  Exampes: mdofail001, tcfail015
+\begin{code}
+-- 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.
+
+  | RuntimeUnkSkol      -- a type variable used to represent an unknown
+                        -- runtime type (used in the GHCi debugger)
+
+  | 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")
+pprSkolInfo RuntimeUnkSkol = WARN( True, text "pprSkolInfo: RuntimeUnkSkol" ) ptext (sLit "RuntimeUnkSkol")
 \end{code}
 
 
 %************************************************************************
 %*                                                                     *
-\subsection[Inst-origin]{The @InstOrigin@ type}
+            CtOrigin
 %*                                                                     *
 %************************************************************************
 
-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...
-
-It appears in TcMonad because there are a couple of error-message-generation
-functions that deal with it.
-
 \begin{code}
--------------------------------------------
-data InstLoc = InstLoc InstOrigin SrcSpan [ErrCtxt]
-
-instLoc :: Inst -> InstLoc
-instLoc inst = tci_loc inst
-
-setInstLoc :: Inst -> InstLoc -> Inst
-setInstLoc inst new_loc = inst { tci_loc = new_loc }
-
-instSpan :: Inst -> SrcSpan
-instSpan wanted = instLocSpan (instLoc wanted)
-
-instLocSpan :: InstLoc -> SrcSpan
-instLocSpan (InstLoc _ s _) = s
-
-instLocOrigin :: InstLoc -> InstOrigin
-instLocOrigin (InstLoc o _ _) = o
-
-pprInstArising :: Inst -> SDoc
-pprInstArising loc = ptext (sLit "arising from") <+> pprInstLoc (tci_loc loc)
-
-pprInstLoc :: InstLoc -> SDoc
-pprInstLoc (InstLoc orig span _) = sep [ppr orig, text "at" <+> ppr span]
+-- CtOrigin gives the origin of *wanted* constraints
+data CtOrigin
+  = OccurrenceOf Name          -- Occurrence of an overloaded identifier
+  | AppOrigin                  -- An application of some kind
 
--------------------------------------------
-data InstOrigin
-  = SigOrigin SkolemInfo       -- Pattern, class decl, inst decl etc;
-                               -- Places that bind type variables and introduce
-                               -- available constraints
-
-  | IPBindOrigin (IPName Name) -- Binding site of an implicit parameter
-
-       -------------------------------------------------------
-       -- The rest are all occurrences: Insts that are 'wanted'
-       -------------------------------------------------------
-  | OccurrenceOf Name          -- Occurrence of an overloaded identifier
   | SpecPragOrigin Name                -- Specialisation pragma for identifier
 
+  | TypeEqOrigin EqOrigin
+
   | IPOccOrigin  (IPName Name) -- Occurrence of an implicit parameter
 
   | LiteralOrigin (HsOverLit Name)     -- Occurrence of a literal
@@ -944,53 +1106,60 @@ data InstOrigin
 
   | ArithSeqOrigin (ArithSeqInfo Name) -- [x..], [x..y] etc
   | PArrSeqOrigin  (ArithSeqInfo Name) -- [:x..y:] and [:x,y..z:]
+  | SectionOrigin
   | TupleOrigin                               -- (..,..)
-
-  | InstSigOrigin      -- A dict occurrence arising from instantiating
-                       -- a polymorphic type during a subsumption check
-
   | ExprSigOrigin      -- e :: ty
+  | PatSigOrigin       -- p :: ty
+  | PatOrigin          -- Instantiating a polytyped pattern at a constructor
   | RecordUpdOrigin
   | ViewPatOrigin
 
-  | InstScOrigin       -- Typechecking superclasses of an instance declaration
-
-  | NoScOrigin          -- A very special hack; see TcSimplify,
-                       --   Note [Recursive instances and superclases]
-                          
-
+  | ScOrigin           -- Typechecking superclasses of an instance declaration
   | DerivOrigin                -- Typechecking deriving
   | StandAloneDerivOrigin -- Typechecking stand-alone deriving
   | DefaultOrigin      -- Typechecking a default decl
   | DoOrigin           -- Arising from a do expression
+  | IfOrigin            -- Arising from an if statement
   | ProcOrigin         -- Arising from a proc expression
-  | ImplicOrigin SDoc  -- An implication constraint
-  | EqOrigin           -- A type equality
   | AnnOrigin           -- An annotation
-
-instance Outputable InstOrigin where
-    ppr (OccurrenceOf name)   = hsep [ptext (sLit "a use of"), quotes (ppr name)]
-    ppr (SpecPragOrigin name) = hsep [ptext (sLit "a specialisation pragma for"), quotes (ppr name)]
-    ppr (IPOccOrigin name)    = hsep [ptext (sLit "a use of implicit parameter"), quotes (ppr name)]
-    ppr (IPBindOrigin name)   = hsep [ptext (sLit "a binding for implicit parameter"), quotes (ppr name)]
-    ppr RecordUpdOrigin       = ptext (sLit "a record update")
-    ppr ExprSigOrigin         = ptext (sLit "an expression type signature")
-    ppr ViewPatOrigin         = ptext (sLit "a view pattern")
-    ppr (LiteralOrigin lit)   = hsep [ptext (sLit "the literal"), quotes (ppr lit)]
-    ppr (ArithSeqOrigin seq)  = hsep [ptext (sLit "the arithmetic sequence"), quotes (ppr seq)]
-    ppr (PArrSeqOrigin seq)   = hsep [ptext (sLit "the parallel array sequence"), quotes (ppr seq)]
-    ppr TupleOrigin          = ptext (sLit "a tuple")
-    ppr NegateOrigin         = ptext (sLit "a use of syntactic negation")
-    ppr InstScOrigin         = ptext (sLit "the superclasses of an instance declaration")
-    ppr NoScOrigin            = ptext (sLit "an instance declaration")
-    ppr DerivOrigin          = ptext (sLit "the 'deriving' clause of a data type declaration")
-    ppr StandAloneDerivOrigin = ptext (sLit "a 'deriving' declaration")
-    ppr DefaultOrigin        = ptext (sLit "a 'default' declaration")
-    ppr DoOrigin             = ptext (sLit "a do statement")
-    ppr ProcOrigin           = ptext (sLit "a proc expression")
-    ppr (ImplicOrigin doc)    = doc
-    ppr (SigOrigin info)      = pprSkolInfo info
-    ppr EqOrigin             = ptext (sLit "a type equality")
-    ppr InstSigOrigin         = panic "ppr InstSigOrigin"
-    ppr AnnOrigin             = ptext (sLit "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 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}
+