fix haddock submodule pointer
[ghc-hetmet.git] / compiler / typecheck / TcRnTypes.lhs
index fce06d1..d94ecd7 100644 (file)
@@ -28,23 +28,31 @@ module TcRnTypes(
        ArrowCtxt(NoArrowCtxt), newArrowScope, escapeArrowScope,
 
        -- Constraints
-        Untouchables,
-       WantedConstraints, emptyWanteds, andWanteds, extendWanteds,
-       WantedConstraint(..), WantedEvVar(..), wantedEvVarLoc, 
-        wantedEvVarToVar, wantedEvVarPred, splitWanteds,
+        Untouchables(..), inTouchableRange, isNoUntouchables,
 
-       evVarsToWanteds,
-       Implication(..), 
+        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,
+        WantedLoc, GivenLoc, GivenKind(..), pushErrCtxt,
 
        SkolemInfo(..),
 
+        CtFlavor(..), pprFlavorArising, isWanted, 
+        isGivenOrSolved, isGiven_maybe,
+        isDerived,
+        FlavoredEvVar,
+
        -- Pretty printing
-       pprEvVarTheta, pprWantedsWithLocs, pprWantedWithLoc, 
+        pprEvVarTheta, pprWantedEvVar, pprWantedsWithLocs,
        pprEvVars, pprEvVarWithType,
-       pprArising, pprArisingAt,
+        pprArising, pprArisingAt,
 
        -- Misc other types
        TcId, TcIdSet, TcTyVarBind(..), TcTyVarBinds
@@ -56,6 +64,9 @@ module TcRnTypes(
 import HsSyn
 import HscTypes
 import Type
+import Id      ( evVarPred )
+import Class    ( Class )
+import DataCon  ( DataCon, dataConUserType )
 import TcType
 import Annotations
 import InstEnv
@@ -68,17 +79,17 @@ import NameSet
 import Var
 import VarEnv
 import Module
-import UniqFM
 import SrcLoc
 import VarSet
 import ErrUtils
+import UniqFM
 import UniqSupply
+import Unique
 import BasicTypes
 import Bag
 import Outputable
 import ListSetOps
 import FastString
-import StaticFlags( opt_ErrorSpans )
 
 import Data.Set (Set)
 \end{code}
@@ -216,22 +227,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,
@@ -257,12 +259,14 @@ data TcGblEnv
         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_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
@@ -323,6 +327,7 @@ data IfLclEnv
                -- plus which bit is currently being examined
 
        if_tv_env  :: UniqFM TyVar,     -- Nested tyvar bindings
+                                       -- (and coercions)
        if_id_env  :: UniqFM Id         -- Nested id binding
     }
 \end{code}
@@ -372,6 +377,7 @@ 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_hetMetLevel  :: [TyVar],    -- The current environment classifier level (list-of-names)
        tcl_env  :: TcTypeEnv,    -- The local type environment: Ids and
                                  -- TyVars defined in this module
                                        
@@ -382,7 +388,13 @@ data TcLclEnv              -- Changes as we move inside an expression
                         -- Why mutable? see notes with tcGetGlobalTyVars
 
        tcl_lie   :: TcRef WantedConstraints,    -- Place to accumulate type constraints
-       tcl_untch :: Untouchables                -- Untouchables
+
+       -- 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
@@ -502,7 +514,9 @@ data TcTyThing
 
   | ATcId   {          -- Ids defined in this module; may not be fully zonked
        tct_id    :: TcId,              
-       tct_level :: ThLevel }
+       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
@@ -517,7 +531,8 @@ instance Outputable TcTyThing where -- Debugging only
    ppr elt@(ATcId {})   = text "Identifier" <> 
                          brackets (ppr (tct_id elt) <> dcolon 
                                  <> ppr (varType (tct_id elt)) <> comma
-                                <+> ppr (tct_level elt))
+                                <+> ppr (tct_level elt)
+                                <+> ppr (tct_hetMetLevel elt))
    ppr (ATyVar tv _)    = text "Type variable" <+> quotes (ppr tv)
    ppr (AThing k)       = text "AThing" <+> ppr k
 
@@ -632,7 +647,7 @@ plusImportAvails
   (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,    
+  = ImportAvails { imp_mods     = plusModuleEnv_C (++) mods1 mods2,
                   imp_dep_mods = plusUFM_C plus_mod_dep dmods1 dmods2, 
                   imp_dep_pkgs = dpkgs1 `unionLists` dpkgs2,
                   imp_orphs    = orphs1 `unionLists` orphs2,
@@ -667,7 +682,6 @@ instance Outputable WhereFrom where
 %************************************************************************
 %*                                                                     *
                Wanted constraints
-
      These are forced to be in TcRnTypes because
           TcLclEnv mentions WantedConstraints
           WantedConstraint mentions CtLoc
@@ -677,74 +691,134 @@ instance Outputable WhereFrom where
 v%************************************************************************
 
 \begin{code}
-type Untouchables = TcTyVarSet -- All MetaTyVars
+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]
+    }
 
-type WantedConstraints = Bag WantedConstraint
+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}
 
-data WantedConstraint
-  = WcEvVar  WantedEvVar
-  | WcImplic Implication
-  -- ToDo: add literals, methods
+\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
 
--- EvVar defined in module Var.lhs: 
+-- EvVar defined in module Var.lhs:
 -- Evidence variables include all *quantifiable* constraints
 --   dictionaries
 --   implicit parameters
 --   coercion variables
+\end{code}
 
-data WantedEvVar   -- The sort of constraint over which one can lambda-abstract
-   = WantedEvVar 
-         EvVar              -- The variable itself; make a binding for it please
-         WantedLoc   -- How the constraint arose in the first place
-                    -- (used for error messages only)
-
-type WantedLoc = CtLoc CtOrigin
-type GivenLoc  = CtLoc SkolemInfo
+%************************************************************************
+%*                                                                     *
+                Implication constraints
+%*                                                                      *
+%************************************************************************
 
+\begin{code}
 data Implication
   = Implic {  
-      ic_env_tvs :: Untouchables, -- Untouchables: unification variables
-                                  -- free in the environment
-      ic_env     :: TcTypeEnv,    -- The type environment
-                                 -- Used only when generating error messages
-         -- Generally, ic_env_tvs = tvsof(ic_env)
+      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_scoped :: [TcTyVar],    -- List of scoped variables to be unified 
-                                 -- bijectively to a subset of ic_tyvars
-                                -- Note [Scoped pattern variable]
-
       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,    -- Wanted constraints
+      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
-
-      ic_loc   :: GivenLoc }
-
-evVarsToWanteds :: WantedLoc -> [EvVar] -> WantedConstraints
-evVarsToWanteds loc evs = listToBag [WcEvVar (WantedEvVar ev loc) | ev <- evs]
-
-wantedEvVarLoc :: WantedEvVar -> WantedLoc 
-wantedEvVarLoc (WantedEvVar _ loc) = loc 
-
-wantedEvVarToVar :: WantedEvVar -> EvVar 
-wantedEvVarToVar (WantedEvVar ev _) = ev 
-
-wantedEvVarPred :: WantedEvVar -> PredType 
-wantedEvVarPred (WantedEvVar ev _)  = evVarPred ev 
+      ic_binds  :: EvBindsVar   -- Points to the place to fill in the
+                                -- abstraction and bindings
+    }
 
-splitWanteds :: WantedConstraints -> (Bag WantedEvVar, Bag Implication)
-splitWanteds wanted = partitionBagWith pick wanted
-  where
-    pick (WcEvVar v)  = Left v
-    pick (WcImplic i) = Right i
+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}
 
 Note [Skolems in an implication]
@@ -758,29 +832,74 @@ Instead, ic_skols is used only when considering floating a constraint
 outside the implication in TcSimplify.floatEqualities or 
 TcSimplify.approximateImplications
 
-Note [Scoped pattern variables]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-   data T where K :: forall a,b. a -> b -> T
+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'
 
-   ...(case x of K (p::c) (q::d) -> ...)...
-
-We create fresh MetaTvs for c,d, and later check that they are
-bound bijectively to the skolems we created for a,b.  So the
-implication constraint looks like
-           ic_skols  = {a',b'}  -- Skolem tvs created from a,b
-           ic_scoped = {c',d'}  -- Meta tvs created from c,d
+%************************************************************************
+%*                                                                     *
+            EvVarX, WantedEvVar, FlavoredEvVar
+%*                                                                     *
+%************************************************************************
 
 \begin{code}
-emptyWanteds :: WantedConstraints
-emptyWanteds = emptyBag
+data EvVarX a = EvVarX EvVar a
+     -- An evidence variable with accompanying info
+
+type WantedEvVar   = EvVarX WantedLoc     -- The location where it arose
+type FlavoredEvVar = EvVarX CtFlavor
+
+instance Outputable (EvVarX a) where
+  ppr (EvVarX ev _) = pprEvVarWithType ev
+  -- If you want to see the associated info,
+  -- use a more specific printing function
 
-andWanteds :: WantedConstraints -> WantedConstraints -> WantedConstraints
-andWanteds = unionBags
+mkEvVarX :: EvVar -> a -> EvVarX a
+mkEvVarX = EvVarX
 
-extendWanteds :: WantedConstraints -> WantedConstraint -> WantedConstraints
-extendWanteds = snocBag
+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)
+
+wantedToFlavored :: WantedEvVar -> FlavoredEvVar
+wantedToFlavored (EvVarX v wl) = EvVarX v (Wanted wl)
+
+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}
+
+
 \begin{code}
 pprEvVars :: [EvVar] -> SDoc   -- Print with their types
 pprEvVars ev_vars = vcat (map pprEvVarWithType ev_vars)
@@ -789,57 +908,82 @@ pprEvVarTheta :: [EvVar] -> SDoc
 pprEvVarTheta ev_vars = pprTheta (map evVarPred ev_vars)
                               
 pprEvVarWithType :: EvVar -> SDoc
-pprEvVarWithType v = ppr v <+> dcolon <+> pprPred (evVarPred v)
-
-pprWantedsWithLocs :: Bag WantedConstraint -> SDoc
-pprWantedsWithLocs = foldrBag (($$) . pprWantedWithLoc) empty 
-
-pprWantedWithLoc :: WantedConstraint -> SDoc
-pprWantedWithLoc (WcImplic i) = ppr i
-pprWantedWithLoc (WcEvVar v)  = pprWantedEvVarWithLoc v
-
-instance Outputable WantedConstraint where
-  ppr (WcEvVar v)  = ppr v
-  ppr (WcImplic i) = ppr i
+pprEvVarWithType v = ppr v <+> dcolon <+> pprPredTy (evVarPred v)
 
--- Adding -ferror-spans makes the output more voluminous
-instance Outputable WantedEvVar where
-  ppr wev | opt_ErrorSpans = pprWantedEvVarWithLoc wev
-          | otherwise      = pprWantedEvVar wev
+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 (WantedEvVar v loc) = hang (pprEvVarWithType v) 
-                                               2 (pprArisingAt loc) 
-pprWantedEvVar        (WantedEvVar v _)   = pprEvVarWithType v
+pprWantedEvVarWithLoc (EvVarX v loc) = hang (pprEvVarWithType v)
+                                          2 (pprArisingAt loc)
+pprWantedEvVar        (EvVarX v _)   = pprEvVarWithType v
+\end{code}
 
-instance Outputable Implication where
-  ppr (Implic { ic_env_tvs = env_tvs, ic_skols = skols, ic_given = given
-              , ic_wanted = wanted, ic_binds = binds, ic_loc = loc })
-   = ptext (sLit "Implic") <+> braces 
-     (sep [ ptext (sLit "Untouchables = ") <+> ppr env_tvs
-          , 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) ])
+%************************************************************************
+%*                                                                     *
+            CtLoc
+%*                                                                     *
+%************************************************************************
+
+\begin{code}
+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}
 
 %************************************************************************
 %*                                                                     *
-            CtLoc, CtOrigin
+            CtLoc
 %*                                                                     *
 %************************************************************************
 
-The 'CtLoc' and 'CtOrigin' types gives information about where a
-*wanted constraint* 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
 
@@ -849,14 +993,105 @@ 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 :: CtLoc CtOrigin -> SDoc
-pprArisingAt (CtLoc o s _) = sep [pprArising o, text "at" <+> ppr s]
+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}
+-- 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}
+
+
+%************************************************************************
+%*                                                                     *
+            CtOrigin
+%*                                                                     *
+%************************************************************************
+
+\begin{code}
 -- CtOrigin gives the origin of *wanted* constraints
 data CtOrigin
   = OccurrenceOf Name          -- Occurrence of an overloaded identifier
@@ -886,8 +1121,11 @@ data CtOrigin
   | StandAloneDerivOrigin -- Typechecking stand-alone deriving
   | 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
   | AnnOrigin           -- An annotation
+  | FunDepOrigin
 
 data EqOrigin 
   = UnifyOrigin 
@@ -907,6 +1145,7 @@ 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)]
@@ -918,10 +1157,13 @@ pprO DerivOrigin    = ptext (sLit "the 'deriving' clause of a data type declarat
 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}
+