New handling of overlapping inst in Safe Haskell
[ghc.git] / compiler / typecheck / TcRnTypes.hs
index 7ea9ae9..3014755 100644 (file)
@@ -16,7 +16,7 @@ For state that is global and should be returned at the end (e.g not part
 of the stack mechanism), you should use an TcRef (= IORef) to store them.
 -}
 
-{-# LANGUAGE CPP, ExistentialQuantification #-}
+{-# LANGUAGE CPP, ExistentialQuantification, GeneralizedNewtypeDeriving #-}
 
 module TcRnTypes(
         TcRnIf, TcRn, TcM, RnM, IfM, IfL, IfG, -- The monad is opaque outside this module
@@ -27,21 +27,26 @@ module TcRnTypes(
         TcGblEnv(..), TcLclEnv(..),
         IfGblEnv(..), IfLclEnv(..),
 
-        -- Ranamer types
+        -- Renamer types
         ErrCtxt, RecFieldEnv(..),
         ImportAvails(..), emptyImportAvails, plusImportAvails,
         WhereFrom(..), mkModDeps,
 
         -- Typechecker types
-        TcTypeEnv, TcIdBinder(..), TcTyThing(..), PromotionErr(..),
+        TcTypeEnv, TcIdBinderStack, TcIdBinder(..),
+        TcTyThing(..), PromotionErr(..),
         pprTcTyThingCategory, pprPECategory,
 
+        -- Desugaring types
+        DsM, DsLclEnv(..), DsGblEnv(..), PArrBuiltin(..),
+        DsMetaEnv, DsMetaVal(..),
+
         -- Template Haskell
         ThStage(..), PendingStuff(..), topStage, topAnnStage, topSpliceStage,
         ThLevel, impLevel, outerLevel, thLevel,
 
         -- Arrows
-        ArrowCtxt(NoArrowCtxt), newArrowScope, escapeArrowScope,
+        ArrowCtxt(..),
 
         -- Canonical constraints
         Xi, Ct(..), Cts, emptyCts, andCts, andManyCts, pprCts,
@@ -49,21 +54,21 @@ module TcRnTypes(
         isEmptyCts, isCTyEqCan, isCFunEqCan,
         isCDictCan_Maybe, isCFunEqCan_maybe,
         isCIrredEvCan, isCNonCanonical, isWantedCt, isDerivedCt,
-        isGivenCt, isHoleCt, isTypedHoleCt, isPartialTypeSigCt,
+        isGivenCt, isHoleCt, isExprHoleCt, isTypeHoleCt,
         ctEvidence, ctLoc, ctPred, ctFlavour, ctEqRel,
         mkNonCanonical, mkNonCanonicalCt,
         ctEvPred, ctEvLoc, ctEvEqRel,
-        ctEvTerm, ctEvCoercion, ctEvId, ctEvCheckDepth,
+        ctEvTerm, ctEvCoercion, ctEvId,
 
         WantedConstraints(..), insolubleWC, emptyWC, isEmptyWC,
         andWC, unionsWC, addSimples, addImplics, mkSimpleWC, addInsols,
-        dropDerivedWC,
+        dropDerivedWC, dropDerivedSimples, dropDerivedInsols,
+        insolubleImplic, trulyInsoluble,
 
-        Implication(..),
-        SubGoalCounter(..),
-        SubGoalDepth, initialSubGoalDepth, maxSubGoalDepth,
-        bumpSubGoalDepth, subGoalCounterValue, subGoalDepthExceeded,
-        CtLoc(..), ctLocSpan, ctLocEnv, ctLocOrigin,
+        Implication(..), ImplicStatus(..), isInsolubleStatus,
+        SubGoalDepth, initialSubGoalDepth,
+        bumpSubGoalDepth, subGoalDepthExceeded,
+        CtLoc(..), ctLocSpan, ctLocEnv, ctLocLevel, ctLocOrigin,
         ctLocDepth, bumpCtLocDepth,
         setCtLocOrigin, setCtLocEnv, setCtLocSpan,
         CtOrigin(..), pprCtOrigin,
@@ -88,7 +93,7 @@ module TcRnTypes(
         pprArising, pprArisingAt,
 
         -- Misc other types
-        TcId, TcIdSet, TcTyVarBind(..), TcTyVarBinds, HoleSort(..)
+        TcId, TcIdSet, HoleSort(..)
 
   ) where
 
@@ -105,7 +110,6 @@ import TyCon    ( TyCon )
 import ConLike  ( ConLike(..) )
 import DataCon  ( DataCon, dataConUserType, dataConOrigArgTys )
 import PatSyn   ( PatSyn, patSynType )
-import TysWiredIn ( coercibleClass )
 import TcType
 import Annotations
 import InstEnv
@@ -130,6 +134,7 @@ import DynFlags
 import Outputable
 import ListSetOps
 import FastString
+import GHC.Fingerprint
 
 import Data.Set (Set)
 import Control.Monad (ap, liftM)
@@ -153,27 +158,19 @@ import qualified Language.Haskell.TH as TH
 The monad itself has to be defined here, because it is mentioned by ErrCtxt
 -}
 
--- | Type alias for 'IORef'; the convention is we'll use this for mutable
--- bits of data in 'TcGblEnv' which are updated during typechecking and
--- returned at the end.
-type TcRef a     = IORef a
--- ToDo: when should I refer to it as a 'TcId' instead of an 'Id'?
-type TcId        = Id
-type TcIdSet     = IdSet
-
-
 type TcRnIf a b = IOEnv (Env a b)
-type IfM lcl  = TcRnIf IfGblEnv lcl         -- Iface stuff
-
-type IfG  = IfM ()                          -- Top level
-type IfL  = IfM IfLclEnv                    -- Nested
-
--- | Type-checking and renaming monad: the main monad that most type-checking
--- takes place in.  The global environment is 'TcGblEnv', which tracks
--- all of the top-level type-checking information we've accumulated while
--- checking a module, while the local environment is 'TcLclEnv', which
--- tracks local information as we move inside expressions.
-type TcRn = TcRnIf TcGblEnv TcLclEnv
+type TcRn       = TcRnIf TcGblEnv TcLclEnv    -- Type inference
+type IfM lcl    = TcRnIf IfGblEnv lcl         -- Iface stuff
+type IfG        = IfM ()                      --    Top level
+type IfL        = IfM IfLclEnv                --    Nested
+type DsM        = TcRnIf DsGblEnv DsLclEnv    -- Desugaring
+
+-- TcRn is the type-checking and renaming monad: the main monad that
+-- most type-checking takes place in.  The global environment is
+-- 'TcGblEnv', which tracks all of the top-level type-checking
+-- information we've accumulated while checking a module, while the
+-- local environment is 'TcLclEnv', which tracks local information as
+-- we move inside expressions.
 
 -- | Historical "renaming monad" (now it's just 'TcRn').
 type RnM  = TcRn
@@ -181,26 +178,6 @@ type RnM  = TcRn
 -- | Historical "type-checking monad" (now it's just 'TcRn').
 type TcM  = TcRn
 
-{-
-Representation of type bindings to uninstantiated meta variables used during
-constraint solving.
--}
-
-data TcTyVarBind = TcTyVarBind TcTyVar TcType
-
-type TcTyVarBinds = Bag TcTyVarBind
-
-instance Outputable TcTyVarBind where
-  ppr (TcTyVarBind tv ty) = ppr tv <+> text ":=" <+> ppr ty
-
-{-
-************************************************************************
-*                                                                      *
-                The main environment types
-*                                                                      *
-************************************************************************
--}
-
 -- We 'stack' these envs through the Reader like monad infastructure
 -- as we move into an expression (although the change is focused in
 -- the lcl type).
@@ -226,6 +203,125 @@ instance ContainsDynFlags (Env gbl lcl) where
 instance ContainsModule gbl => ContainsModule (Env gbl lcl) where
     extractModule env = extractModule (env_gbl env)
 
+
+{-
+************************************************************************
+*                                                                      *
+                The interface environments
+              Used when dealing with IfaceDecls
+*                                                                      *
+************************************************************************
+-}
+
+data IfGblEnv
+  = IfGblEnv {
+        -- The type environment for the module being compiled,
+        -- in case the interface refers back to it via a reference that
+        -- was originally a hi-boot file.
+        -- We need the module name so we can test when it's appropriate
+        -- to look in this env.
+        if_rec_types :: Maybe (Module, IfG TypeEnv)
+                -- Allows a read effect, so it can be in a mutable
+                -- variable; c.f. handling the external package type env
+                -- Nothing => interactive stuff, no loops possible
+    }
+
+data IfLclEnv
+  = IfLclEnv {
+        -- The module for the current IfaceDecl
+        -- So if we see   f = \x -> x
+        -- it means M.f = \x -> x, where M is the if_mod
+        if_mod :: Module,
+
+        -- The field is used only for error reporting
+        -- if (say) there's a Lint error in it
+        if_loc :: SDoc,
+                -- Where the interface came from:
+                --      .hi file, or GHCi state, or ext core
+                -- 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
+    }
+
+{-
+************************************************************************
+*                                                                      *
+                Desugarer monad
+*                                                                      *
+************************************************************************
+
+Now the mondo monad magic (yes, @DsM@ is a silly name)---carry around
+a @UniqueSupply@ and some annotations, which
+presumably include source-file location information:
+-}
+
+-- If '-XParallelArrays' is given, the desugarer populates this table with the corresponding
+-- variables found in 'Data.Array.Parallel'.
+--
+data PArrBuiltin
+        = PArrBuiltin
+        { lengthPVar         :: Var     -- ^ lengthP
+        , replicatePVar      :: Var     -- ^ replicateP
+        , singletonPVar      :: Var     -- ^ singletonP
+        , mapPVar            :: Var     -- ^ mapP
+        , filterPVar         :: Var     -- ^ filterP
+        , zipPVar            :: Var     -- ^ zipP
+        , crossMapPVar       :: Var     -- ^ crossMapP
+        , indexPVar          :: Var     -- ^ (!:)
+        , emptyPVar          :: Var     -- ^ emptyP
+        , appPVar            :: Var     -- ^ (+:+)
+        , enumFromToPVar     :: Var     -- ^ enumFromToP
+        , enumFromThenToPVar :: Var     -- ^ enumFromThenToP
+        }
+
+data DsGblEnv
+        = DsGblEnv
+        { ds_mod          :: Module             -- For SCC profiling
+        , ds_fam_inst_env :: FamInstEnv         -- Like tcg_fam_inst_env
+        , ds_unqual  :: PrintUnqualified
+        , ds_msgs    :: IORef Messages          -- Warning messages
+        , ds_if_env  :: (IfGblEnv, IfLclEnv)    -- Used for looking up global,
+                                                -- possibly-imported things
+        , ds_dph_env :: GlobalRdrEnv            -- exported entities of 'Data.Array.Parallel.Prim'
+                                                -- iff '-fvectorise' flag was given as well as
+                                                -- exported entities of 'Data.Array.Parallel' iff
+                                                -- '-XParallelArrays' was given; otherwise, empty
+        , ds_parr_bi :: PArrBuiltin             -- desugarar names for '-XParallelArrays'
+        , ds_static_binds :: IORef [(Fingerprint, (Id,CoreExpr))]
+          -- ^ Bindings resulted from floating static forms
+        }
+
+instance ContainsModule DsGblEnv where
+    extractModule = ds_mod
+
+data DsLclEnv = DsLclEnv {
+        dsl_meta    :: DsMetaEnv,        -- Template Haskell bindings
+        dsl_loc     :: SrcSpan           -- to put in pattern-matching error msgs
+     }
+
+-- Inside [| |] brackets, the desugarer looks
+-- up variables in the DsMetaEnv
+type DsMetaEnv = NameEnv DsMetaVal
+
+data DsMetaVal
+   = DsBound Id         -- Bound by a pattern inside the [| |].
+                        -- Will be dynamically alpha renamed.
+                        -- The Id has type THSyntax.Var
+
+   | DsSplice (HsExpr Id) -- These bindings are introduced by
+                          -- the PendingSplices on a HsBracketOut
+
+
+{-
+************************************************************************
+*                                                                      *
+                Global typechecker environment
+*                                                                      *
+************************************************************************
+-}
+
 -- | 'TcGblEnv' describes the top-level of the module at the
 -- point at which the typechecker is finished work.
 -- It is this structure that is handed on to the desugarer
@@ -238,6 +334,8 @@ data TcGblEnv
           -- ^ What kind of module (regular Haskell, hs-boot, ext-core)
         tcg_sig_of  :: Maybe Module,
           -- ^ Are we being compiled as a signature of an implementation?
+        tcg_mod_name :: Maybe (Located ModuleName),
+          -- ^ @Nothing@: \"module X where\" is omitted
         tcg_impl_rdr_env :: Maybe GlobalRdrEnv,
           -- ^ Environment used only during -sig-of for resolving top level
           -- bindings.  See Note [Signature parameters in TcGblEnv and DynFlags]
@@ -334,6 +432,8 @@ data TcGblEnv
         -- initially in un-zonked form and are finally zonked in tcRnSrcDecls
 
         tcg_rn_exports :: Maybe [Located (IE Name)],
+                -- Nothing <=> no explicit export list
+
         tcg_rn_imports :: [LImportDecl Name],
                 -- Keep the renamed imports regardless.  They are not
                 -- voluminous and are needed if you want to report unused imports
@@ -360,20 +460,21 @@ data TcGblEnv
 
         tcg_ev_binds  :: Bag EvBind,        -- Top-level evidence bindings
 
-        -- Things defined in this module, or (in GHCi) in the interactive package
-        --   For the latter, see Note [The interactive package] in HscTypes
-        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_tcs       :: [TyCon],           -- ...TyCons and Classes
-        tcg_insts     :: [ClsInst],         -- ...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_patsyns   :: [PatSyn],          -- ...Pattern synonyms
+        -- Things defined in this module, or (in GHCi)
+        -- in the declarations for a single GHCi command.
+        -- For the latter, see Note [The interactive package] in HscTypes
+        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_tcs       :: [TyCon],            -- ...TyCons and Classes
+        tcg_insts     :: [ClsInst],          -- ...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_patsyns   :: [PatSyn],           -- ...Pattern synonyms
 
         tcg_doc_hdr   :: Maybe LHsDocString, -- ^ Maybe Haddock header docs
         tcg_hpc       :: AnyHpcUsage,        -- ^ @True@ if any part of the
@@ -382,12 +483,14 @@ data TcGblEnv
         tcg_main      :: Maybe Name,         -- ^ The Name of the main
                                              -- function, if this module is
                                              -- the main module.
-        tcg_safeInfer :: TcRef Bool,         -- Has the typechecker
-                                             -- inferred this module
-                                             -- as -XSafe (Safe Haskell)
 
-        -- | A list of user-defined plugins for the constraint solver.
+        tcg_safeInfer :: TcRef (Bool, WarningMessages),
+        -- ^ Has the typechecker inferred this module as -XSafe (Safe Haskell)
+        -- See Note [Safe Haskell Overlapping Instances Implementation],
+        -- although this is used for more than just that failure case.
+
         tcg_tc_plugins :: [TcPluginSolver],
+        -- ^ A list of user-defined plugins for the constraint solver.
 
         tcg_static_wc :: TcRef WantedConstraints
           -- ^ Wanted constraints of static forms.
@@ -482,47 +585,6 @@ We gather two sorts of usage information
 
 ************************************************************************
 *                                                                      *
-                The interface environments
-              Used when dealing with IfaceDecls
-*                                                                      *
-************************************************************************
--}
-
-data IfGblEnv
-  = IfGblEnv {
-        -- The type environment for the module being compiled,
-        -- in case the interface refers back to it via a reference that
-        -- was originally a hi-boot file.
-        -- We need the module name so we can test when it's appropriate
-        -- to look in this env.
-        if_rec_types :: Maybe (Module, IfG TypeEnv)
-                -- Allows a read effect, so it can be in a mutable
-                -- variable; c.f. handling the external package type env
-                -- Nothing => interactive stuff, no loops possible
-    }
-
-data IfLclEnv
-  = IfLclEnv {
-        -- The module for the current IfaceDecl
-        -- So if we see   f = \x -> x
-        -- it means M.f = \x -> x, where M is the if_mod
-        if_mod :: Module,
-
-        -- The field is used only for error reporting
-        -- if (say) there's a Lint error in it
-        if_loc :: SDoc,
-                -- Where the interface came from:
-                --      .hi file, or GHCi state, or ext core
-                -- 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
-    }
-
-{-
-************************************************************************
-*                                                                      *
                 The local typechecker environment
 *                                                                      *
 ************************************************************************
@@ -546,9 +608,9 @@ Why?  Because they are now Ids not TcIds.  This final GlobalEnv is
 data TcLclEnv           -- Changes as we move inside an expression
                         -- Discarded after typecheck/rename; not passed on to desugarer
   = TcLclEnv {
-        tcl_loc        :: SrcSpan,         -- Source span
+        tcl_loc        :: RealSrcSpan,     -- Source span
         tcl_ctxt       :: [ErrCtxt],       -- Error context, innermost on top
-        tcl_tclvl      :: TcLevel,    -- Birthplace for new unification variables
+        tcl_tclvl      :: TcLevel,         -- Birthplace for new unification variables
 
         tcl_th_ctxt    :: ThStage,         -- Template Haskell context
         tcl_th_bndrs   :: ThBindEnv,       -- Binding level of in-scope Names
@@ -571,8 +633,7 @@ data TcLclEnv           -- Changes as we move inside an expression
         tcl_env  :: TcTypeEnv,    -- The local type environment:
                                   -- Ids and TyVars defined in this module
 
-        tcl_bndrs :: [TcIdBinder],   -- Stack of locally-bound Ids, innermost on top
-                                     -- Used only for error reporting
+        tcl_bndrs :: TcIdBinderStack,   -- Used for reporting relevant bindings
 
         tcl_tidy :: TidyEnv,      -- Used for tidying types; contains all
                                   -- in-scope type variables (but not term variables)
@@ -598,13 +659,6 @@ type ThBindEnv = NameEnv (TopLevelFlag, ThLevel)
    -- Nota bene: a ThLevel of 'outerLevel' is *not* the same as being
    -- bound at top level!  See Note [Template Haskell levels] in TcSplice
 
-data TcIdBinder
-  = TcIdBndr
-       TcId
-       TopLevelFlag    -- Tells whether the bindind is syntactically top-level
-                       -- (The monomorphic Ids for a recursive group count
-                       --  as not-top-level for this purpose.)
-
 {- Note [Given Insts]
    ~~~~~~~~~~~~~~~~~~
 Because of GADTs, we have to pass inwards the Insts provided by type signatures
@@ -619,6 +673,32 @@ pass it inwards.
 
 -}
 
+-- | Type alias for 'IORef'; the convention is we'll use this for mutable
+-- bits of data in 'TcGblEnv' which are updated during typechecking and
+-- returned at the end.
+type TcRef a     = IORef a
+-- ToDo: when should I refer to it as a 'TcId' instead of an 'Id'?
+type TcId        = Id
+type TcIdSet     = IdSet
+
+---------------------------
+-- The TcIdBinderStack
+---------------------------
+
+type TcIdBinderStack = [TcIdBinder]
+   -- This is a stack of locally-bound ids, innermost on top
+   -- Used ony in error reporting (relevantBindings in TcError)
+
+data TcIdBinder
+  = TcIdBndr
+       TcId
+       TopLevelFlag    -- Tells whether the bindind is syntactically top-level
+                       -- (The monomorphic Ids for a recursive group count
+                       --  as not-top-level for this purpose.)
+
+instance Outputable TcIdBinder where
+   ppr (TcIdBndr id top_lvl) = ppr id <> brackets (ppr top_lvl)
+
 ---------------------------
 -- Template Haskell stages and levels
 ---------------------------
@@ -698,31 +778,30 @@ recording the environment when passing a proc (using newArrowScope),
 and returning to that (using escapeArrowScope) on the left of -< and the
 head of (|..|).
 
-All this can be dealt with by the *renamer*; by the time we get to
-the *type checker* we have sorted out the scopes
+All this can be dealt with by the *renamer*. But the type checker needs
+to be involved too.  Example (arrowfail001)
+  class Foo a where foo :: a -> ()
+  data Bar = forall a. Foo a => Bar a
+  get :: Bar -> ()
+  get = proc x -> case x of Bar a -> foo -< a
+Here the call of 'foo' gives rise to a (Foo a) constraint that should not
+be captured by the pattern match on 'Bar'.  Rather it should join the
+constraints from further out.  So we must capture the constraint bag
+from further out in the ArrowCtxt that we push inwards.
 -}
 
-data ArrowCtxt
+data ArrowCtxt   -- Note [Escaping the arrow scope]
   = NoArrowCtxt
-  | ArrowCtxt (Env TcGblEnv TcLclEnv)
+  | ArrowCtxt LocalRdrEnv (TcRef WantedConstraints)
 
--- Record the current environment (outside a proc)
-newArrowScope :: TcM a -> TcM a
-newArrowScope
-  = updEnv $ \env ->
-        env { env_lcl = (env_lcl env) { tcl_arrow_ctxt = ArrowCtxt env } }
-
--- Return to the stored environment (from the enclosing proc)
-escapeArrowScope :: TcM a -> TcM a
-escapeArrowScope
-  = updEnv $ \ env -> case tcl_arrow_ctxt (env_lcl env) of
-        NoArrowCtxt -> env
-        ArrowCtxt env' -> env'
 
 ---------------------------
 -- TcTyThing
 ---------------------------
 
+-- | A typecheckable thing available in a local context.  Could be
+-- 'AGlobal' 'TyThing', but also lexically scoped variables, etc.
+-- See 'TcEnv' for how to retrieve a 'TyThing' given a 'Name'.
 data TcTyThing
   = AGlobal TyThing             -- Used only in the return type of a lookup
 
@@ -785,9 +864,8 @@ pprPECategory FamDataConPE = ptext (sLit "Data constructor")
 pprPECategory RecDataConPE = ptext (sLit "Data constructor")
 pprPECategory NoDataKinds  = ptext (sLit "Data constructor")
 
-{-
-Note [Bindings with closed types]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- Note [Bindings with closed types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider
 
   f x = let g ys = map not ys
@@ -799,10 +877,9 @@ have no free type variables, and it is the type variables in the
 environment that makes things tricky for OutsideIn generalisation.
 
 Definition:
-
    A variable is "closed", and has tct_closed set to TopLevel,
-      iff
-   a) all its free variables are imported, or are themselves closed
+iff
+   a) all its free variables are imported, or are let-bound with closed types
    b) generalisation is not restricted by the monomorphism restriction
 
 Under OutsideIn we are free to generalise a closed let-binding.
@@ -812,7 +889,7 @@ anyway -- the MR can make a top-level binding with a free type
 variable.)
 
 Note that:
-  * A top-level binding may not be closed, if it suffer from the MR
+  * A top-level binding may not be closed, if it suffers from the MR
 
   * A nested binding may be closed (eg 'g' in the example we started with)
     Indeed, that's the point; whether a function is defined at top level
@@ -1075,8 +1152,9 @@ data Ct
       cc_ev  :: CtEvidence
     }
 
-  | CHoleCan {             -- Treated as an "insoluble" constraint
-                           -- See Note [Insoluble constraints]
+  | CHoleCan {             -- See Note [Hole constraints]
+       -- Treated as an "insoluble" constraint
+       -- See Note [Insoluble constraints]
       cc_ev   :: CtEvidence,
       cc_occ  :: OccName,   -- The name of this hole
       cc_hole :: HoleSort   -- The sort of this hole (expr, type, ...)
@@ -1087,6 +1165,18 @@ data HoleSort = ExprHole  -- ^ A hole in an expression (TypedHoles)
               | TypeHole  -- ^ A hole in a type (PartialTypeSignatures)
 
 {-
+Note [Hole constraints]
+~~~~~~~~~~~~~~~~~~~~~~~
+CHoleCan constraints are used for two kinds of holes,
+distinguished by cc_hole:
+
+  * For holes in expressions
+    e.g.   f x = g _ x
+
+  * For holes in type signatures
+    e.g.   f :: _ -> _
+           f x = [x,True]
+
 Note [Kind orientation for CTyEqCan]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Given an equality (t:* ~ s:Open), we can't solve it by updating t:=s,
@@ -1188,34 +1278,59 @@ ctEqRel = ctEvEqRel . ctEvidence
 
 dropDerivedWC :: WantedConstraints -> WantedConstraints
 -- See Note [Dropping derived constraints]
-dropDerivedWC wc@(WC { wc_simple = simples })
-  = wc { wc_simple  = filterBag isWantedCt simples }
+dropDerivedWC wc@(WC { wc_simple = simples, wc_insol = insols })
+  = wc { wc_simple = dropDerivedSimples simples
+       , wc_insol  = dropDerivedInsols insols }
     -- The wc_impl implications are already (recursively) filtered
 
-{-
-Note [Dropping derived constraints]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+dropDerivedSimples :: Cts -> Cts
+dropDerivedSimples simples = filterBag isWantedCt simples
+                             -- simples are all Wanted or Derived
+
+dropDerivedInsols :: Cts -> Cts
+-- See Note [Dropping derived constraints]
+dropDerivedInsols insols = filterBag keep insols
+  where                    -- insols can include Given
+    keep ct
+      | isDerivedCt ct = keep_orig (ctLocOrigin (ctLoc ct))
+      | otherwise      = True
+
+    keep_orig :: CtOrigin -> Bool
+    keep_orig (KindEqOrigin {})          = True
+    keep_orig (GivenOrigin {})           = True
+    keep_orig (FunDepOrigin1 {}) = True
+    keep_orig (FunDepOrigin2 {}) = True
+--    keep_orig (FunDepOrigin1 _ loc _ _)  = keep_orig (ctLocOrigin loc)
+--    keep_orig (FunDepOrigin2 _ orig _ _) = keep_orig orig
+    keep_orig _                          = False
+
+
+{- Note [Dropping derived constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 In general we discard derived constraints at the end of constraint solving;
 see dropDerivedWC.  For example
- * If we have an unsolved (Ord a), we don't want to complain about
-   an unsolved (Eq a) as well.
 
-But we keep Derived *insoluble* constraints because they indicate a solid,
-comprehensible error.  Particularly:
+ * If we have an unsolved [W] (Ord a), we don't want to complain about
+   an unsolved [D] (Eq a) as well.
+
+ * If we have [W] a ~ Int, [W] a ~ Bool, improvement will generate
+   [D] Int ~ Bool, and we don't want to report that because it's incomprehensible.
+   That is why we don't rewrite wanteds with wanteds!
 
- * Insolubles Givens indicate unreachable code
+But (tiresomely) we do keep *some* Derived insolubles:
 
  * Insoluble kind equalities (e.g. [D] * ~ (* -> *)) may arise from
-   a type equality a ~ Int#, say
+   a type equality a ~ Int#, say.  In future they'll be Wanted, not Derived,
+   but at the moment they are Derived.
 
- * Insoluble derived wanted equalities (e.g. [D] Int ~ Bool) may
-   arise from functional dependency interactions.  We are careful
-   to keep a good CtOrigin on such constraints (FunDepOrigin1, FunDepOrigin2)
-   so that we can produce a good error message (Trac #9612)
+ * Insoluble derived equalities (e.g. [D] Int ~ Bool) may arise from
+   functional dependency interactions, either between Givens or
+   Wanteds.  It seems sensible to retain these:
+   - For Givens they reflect unreachable code
+   - For Wanteds it is arguably better to get a fundep error than
+     a no-instance error (Trac #9612)
 
-Since we leave these Derived constraints in the residual WantedConstraints,
-we must filter them out when we re-process the WantedConstraint,
-in TcSimplify.solve_wanteds.
+To distinguish these cases we use the CtOrigin.
 
 
 ************************************************************************
@@ -1264,13 +1379,13 @@ isHoleCt:: Ct -> Bool
 isHoleCt (CHoleCan {}) = True
 isHoleCt _ = False
 
-isTypedHoleCt :: Ct -> Bool
-isTypedHoleCt (CHoleCan { cc_hole = ExprHole }) = True
-isTypedHoleCt _ = False
+isExprHoleCt :: Ct -> Bool
+isExprHoleCt (CHoleCan { cc_hole = ExprHole }) = True
+isExprHoleCt _ = False
 
-isPartialTypeSigCt :: Ct -> Bool
-isPartialTypeSigCt (CHoleCan { cc_hole = TypeHole }) = True
-isPartialTypeSigCt _ = False
+isTypeHoleCt :: Ct -> Bool
+isTypeHoleCt (CHoleCan { cc_hole = TypeHole }) = True
+isTypeHoleCt _ = False
 
 instance Outputable Ct where
   ppr ct = ppr (cc_ev ct) <+> parens (text ct_sort)
@@ -1340,22 +1455,16 @@ data WantedConstraints
 emptyWC :: WantedConstraints
 emptyWC = WC { wc_simple = emptyBag, wc_impl = emptyBag, wc_insol = emptyBag }
 
-mkSimpleWC :: [Ct] -> WantedConstraints
+mkSimpleWC :: [CtEvidence] -> WantedConstraints
 mkSimpleWC cts
-  = WC { wc_simple = listToBag cts, wc_impl = emptyBag, wc_insol = emptyBag }
+  = WC { wc_simple = listToBag (map mkNonCanonical cts)
+       , wc_impl = emptyBag
+       , wc_insol = emptyBag }
 
 isEmptyWC :: WantedConstraints -> Bool
 isEmptyWC (WC { wc_simple = 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. Ignore
--- constraints arising from PartialTypeSignatures to solve as much of the
--- constraints as possible before reporting the holes.
-insolubleWC wc = not (isEmptyBag (filterBag (not . isPartialTypeSigCt)
-                                  (wc_insol wc)))
-               || anyBag ic_insol (wc_impl wc)
-
 andWC :: WantedConstraints -> WantedConstraints -> WantedConstraints
 andWC (WC { wc_simple = f1, wc_impl = i1, wc_insol = n1 })
       (WC { wc_simple = f2, wc_impl = i2, wc_insol = n2 })
@@ -1369,6 +1478,7 @@ unionsWC = foldr andWC emptyWC
 addSimples :: WantedConstraints -> Bag Ct -> WantedConstraints
 addSimples wc cts
   = wc { wc_simple = wc_simple wc `unionBags` cts }
+    -- Consider: Put the new constraints at the front, so they get solved first
 
 addImplics :: WantedConstraints -> Bag Implication -> WantedConstraints
 addImplics wc implic = wc { wc_impl = wc_impl wc `unionBags` implic }
@@ -1377,6 +1487,30 @@ addInsols :: WantedConstraints -> Bag Ct -> WantedConstraints
 addInsols wc cts
   = wc { wc_insol = wc_insol wc `unionBags` cts }
 
+isInsolubleStatus :: ImplicStatus -> Bool
+isInsolubleStatus IC_Insoluble = True
+isInsolubleStatus _            = False
+
+insolubleImplic :: Implication -> Bool
+insolubleImplic ic = isInsolubleStatus (ic_status ic)
+
+insolubleWC :: WantedConstraints -> Bool
+insolubleWC (WC { wc_impl = implics, wc_insol = insols })
+  =  anyBag trulyInsoluble  insols
+  || anyBag insolubleImplic implics
+
+trulyInsoluble :: Ct -> Bool
+-- The constraint is in the wc_insol set,
+-- but we do not treat as truly isoluble
+--  a) type-holes, arising from PartialTypeSignatures,
+--  b) superclass constraints, arising from the emitInsoluble
+--     in TcInstDcls.tcSuperClasses. In fact only equalities
+--     are truly-insoluble.
+-- Yuk!
+trulyInsoluble insol
+  =  isEqPred (ctPred insol)
+  && not (isTypeHoleCt insol)
+
 instance Outputable WantedConstraints where
   ppr (WC {wc_simple = s, wc_impl = i, wc_insol = n})
    = ptext (sLit "WC") <+> braces (vcat
@@ -1415,32 +1549,63 @@ data Implication
                                  -- False <=> ic_givens might have equalities
 
       ic_env   :: TcLclEnv,      -- Gives the source location and error context
-                                 -- for the implicatdion, and hence for all the
+                                 -- for the implication, and hence for 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
+      ic_binds  :: EvBindsVar,    -- Points to the place to fill in the
+                                  -- abstraction and bindings
+
+      ic_status   :: ImplicStatus
     }
 
+data ImplicStatus
+  = IC_Solved     -- All wanteds in the tree are solved, all the way down
+       { ics_need :: VarSet     -- Evidence variables needed by this implication
+       , ics_dead :: [EvVar] }  -- Subset of ic_given that are not needed
+         -- See Note [Tracking redundant constraints] in TcSimplify
+
+  | IC_Insoluble  -- At least one insoluble constraint in the tree
+
+  | IC_Unsolved   -- Neither of the above; might go either way
+
 instance Outputable Implication where
   ppr (Implic { ic_tclvl = tclvl, ic_skols = skols
               , ic_given = given, ic_no_eqs = no_eqs
-              , ic_wanted = wanted, ic_insol = insol
+              , ic_wanted = wanted, ic_status = status
               , ic_binds = binds, ic_info = info })
    = hang (ptext (sLit "Implic") <+> lbrace)
         2 (sep [ ptext (sLit "TcLevel =") <+> ppr tclvl
                , ptext (sLit "Skolems =") <+> pprTvBndrs skols
                , ptext (sLit "No-eqs =") <+> ppr no_eqs
-               , ptext (sLit "Insol =") <+> ppr insol
+               , ptext (sLit "Status =") <+> ppr status
                , hang (ptext (sLit "Given ="))  2 (pprEvVars given)
                , hang (ptext (sLit "Wanted =")) 2 (ppr wanted)
                , ptext (sLit "Binds =") <+> ppr binds
                , pprSkolInfo info ] <+> rbrace)
 
+instance Outputable ImplicStatus where
+  ppr IC_Insoluble   = ptext (sLit "Insoluble")
+  ppr IC_Unsolved    = ptext (sLit "Unsolved")
+  ppr (IC_Solved { ics_need = vs, ics_dead = dead })
+    = ptext (sLit "Solved")
+      <+> (braces $ vcat [ ptext (sLit "Dead givens =") <+> ppr dead
+                         , ptext (sLit "Needed =") <+> ppr vs ])
+
 {-
+Note [Needed evidence variables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Th ic_need_evs field holds the free vars of ic_binds, and all the
+ic_binds in nested implications.
+
+  * Main purpose: if one of the ic_givens is not mentioned in here, it
+    is redundant.
+
+  * solveImplication may drop an implication altogether if it has no
+    remaining 'wanteds'. But we still track the free vars of its
+    evidence binds, even though it has now disappeared.
+
 Note [Shadowing in a constraint]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We assume NO SHADOWING in a constraint.  Specifically
@@ -1519,14 +1684,39 @@ pprEvVarWithType v = ppr v <+> dcolon <+> pprType (evVarPred v)
 
 Note [Evidence field of CtEvidence]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-During constraint solving we never look at the type of ctev_evtm, or
-ctev_evar; instead we look at the cte_pred field.  The evtm/evar field
+During constraint solving we never look at the type of ctev_evar;
+instead we look at the cte_pred field.  The evtm/evar field
 may be un-zonked.
+
+Note [Bind new Givens immediately]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+For Givens we make new EvVars and bind them immediately. Two main reasons:
+  * Gain sharing.  E.g. suppose we start with g :: C a b, where
+       class D a => C a b
+       class (E a, F a) => D a
+    If we generate all g's superclasses as separate EvTerms we might
+    get    selD1 (selC1 g) :: E a
+           selD2 (selC1 g) :: F a
+           selC1 g :: D a
+    which we could do more economically as:
+           g1 :: D a = selC1 g
+           g2 :: E a = selD1 g1
+           g3 :: F a = selD2 g1
+
+  * For *coercion* evidence we *must* bind each given:
+      class (a~b) => C a b where ....
+      f :: C a b => ....
+    Then in f's Givens we have g:(C a b) and the superclass sc(g,0):a~b.
+    But that superclass selector can't (yet) appear in a coercion
+    (see evTermCoercion), so the easy thing is to bind it to an Id.
+
+So a Given has EvVar inside it rather that (as previously) an EvTerm.
 -}
 
+
 data CtEvidence
   = CtGiven { ctev_pred :: TcPredType      -- See Note [Ct/evidence invariant]
-            , ctev_evtm :: EvTerm          -- See Note [Evidence field of CtEvidence]
+            , ctev_evar :: EvVar           -- See Note [Evidence field of CtEvidence]
             , ctev_loc  :: CtLoc }
     -- Truly given, not depending on subgoals
     -- NB: Spontaneous unifications belong here
@@ -1558,25 +1748,19 @@ ctEvRole :: CtEvidence -> Role
 ctEvRole = eqRelRole . ctEvEqRel
 
 ctEvTerm :: CtEvidence -> EvTerm
-ctEvTerm (CtGiven   { ctev_evtm = tm }) = tm
-ctEvTerm (CtWanted  { ctev_evar = ev }) = EvId ev
-ctEvTerm ctev@(CtDerived {}) = pprPanic "ctEvTerm: derived constraint cannot have id"
-                                      (ppr ctev)
+ctEvTerm ev = EvId (ctEvId ev)
 
 ctEvCoercion :: CtEvidence -> TcCoercion
--- ctEvCoercion ev = evTermCoercion (ctEvTerm ev)
-ctEvCoercion (CtGiven   { ctev_evtm = tm }) = evTermCoercion tm
-ctEvCoercion (CtWanted  { ctev_evar = v })  = mkTcCoVarCo v
-ctEvCoercion ctev@(CtDerived {}) = pprPanic "ctEvCoercion: derived constraint cannot have id"
-                                      (ppr ctev)
+ctEvCoercion ev = mkTcCoVarCo (ctEvId ev)
 
 ctEvId :: CtEvidence -> TcId
-ctEvId (CtWanted  { ctev_evar = ev }) = ev
+ctEvId (CtWanted { ctev_evar = ev }) = ev
+ctEvId (CtGiven  { ctev_evar = ev }) = ev
 ctEvId ctev = pprPanic "ctEvId:" (ppr ctev)
 
 instance Outputable CtEvidence where
   ppr fl = case fl of
-             CtGiven {}   -> ptext (sLit "[G]") <+> ppr (ctev_evtm fl) <+> ppr_pty
+             CtGiven {}   -> ptext (sLit "[G]") <+> ppr (ctev_evar fl) <+> ppr_pty
              CtWanted {}  -> ptext (sLit "[W]") <+> ppr (ctev_evar fl) <+> ppr_pty
              CtDerived {} -> ptext (sLit "[D]") <+> text "_" <+> ppr_pty
          where ppr_pty = dcolon <+> ppr (ctEvPred fl)
@@ -1627,31 +1811,30 @@ ctEvFlavour (CtDerived {}) = Derived
 
 Note [SubGoalDepth]
 ~~~~~~~~~~~~~~~~~~~
-The 'SubGoalCounter' takes care of stopping the constraint solver from looping.
-Because of the different use-cases of regular constaints and type function
-applications, there are two independent counters. Therefore, this datatype is
-abstract. See Note [WorkList]
+The 'SubGoalDepth' takes care of stopping the constraint solver from looping.
+
+The counter starts at zero and increases. It includes dictionary constraints,
+equality simplification, and type family reduction. (Why combine these? Because
+it's actually quite easy to mistake one for another, in sufficiently involved
+scenarios, like ConstraintKinds.)
 
-Each counter starts at zero and increases.
+The flag -fcontext-stack=n (not very well named!) fixes the maximium
+level.
 
-* The "dictionary constraint counter" counts the depth of type class
-  instance declarations.  Example:
+* The counter includes the depth of type class instance declarations.  Example:
      [W] d{7} : Eq [Int]
   That is d's dictionary-constraint depth is 7.  If we use the instance
      $dfEqList :: Eq a => Eq [a]
   to simplify it, we get
      d{7} = $dfEqList d'{8}
-  where d'{8} : Eq Int, and d' has dictionary-constraint depth 8.
+  where d'{8} : Eq Int, and d' has depth 8.
 
   For civilised (decidable) instance declarations, each increase of
   depth removes a type constructor from the type, so the depth never
   gets big; i.e. is bounded by the structural depth of the type.
 
-  The flag -fcontext-stack=n (not very well named!) fixes the maximium
-  level.
-
-* The "type function reduction counter" does the same thing when resolving
-* qualities involving type functions. Example:
+* The counter also increments when resolving
+equalities involving type functions. Example:
   Assume we have a wanted at depth 7:
     [W] d{7} : F () ~ a
   If thre is an type function equation "F () = Int", this would be rewritten to
@@ -1659,79 +1842,37 @@ Each counter starts at zero and increases.
   and remembered as having depth 8.
 
   Again, without UndecidableInstances, this counter is bounded, but without it
-  can resolve things ad infinitum. Hence there is a maximum level. But we use a
-  different maximum, as we expect possibly many more type function reductions
-  in sensible programs than type class constraints.
+  can resolve things ad infinitum. Hence there is a maximum level.
 
-  The flag -ftype-function-depth=n fixes the maximium level.
--}
+* Lastly, every time an equality is rewritten, the counter increases. Again,
+  rewriting an equality constraint normally makes progress, but it's possible
+  the "progress" is just the reduction of an infinitely-reducing type family.
+  Hence we need to track the rewrites.
 
-data SubGoalCounter = CountConstraints | CountTyFunApps
+When compiling a program requires a greater depth, then GHC recommends turning
+off this check entirely by setting -freduction-depth=0. This is because the
+exact number that works is highly variable, and is likely to change even between
+minor releases. Because this check is solely to prevent infinite compilation
+times, it seems safe to disable it when a user has ascertained that their program
+doesn't loop at the type level.
 
-data SubGoalDepth  -- See Note [SubGoalDepth]
-   = SubGoalDepth
-         {-# UNPACK #-} !Int      -- Dictionary constraints
-         {-# UNPACK #-} !Int      -- Type function reductions
-  deriving (Eq, Ord)
+-}
 
-instance Outputable SubGoalDepth where
- ppr (SubGoalDepth c f) =  angleBrackets $
-        char 'C' <> colon <> int c <> comma <>
-        char 'F' <> colon <> int f
+-- | See Note [SubGoalDepth]
+newtype SubGoalDepth = SubGoalDepth Int
+  deriving (Eq, Ord, Outputable)
 
 initialSubGoalDepth :: SubGoalDepth
-initialSubGoalDepth = SubGoalDepth 0 0
-
-maxSubGoalDepth :: DynFlags -> SubGoalDepth
-maxSubGoalDepth dflags = SubGoalDepth (ctxtStkDepth dflags) (tyFunStkDepth dflags)
-
-bumpSubGoalDepth :: SubGoalCounter -> SubGoalDepth -> SubGoalDepth
-bumpSubGoalDepth CountConstraints (SubGoalDepth c f) = SubGoalDepth (c+1) f
-bumpSubGoalDepth CountTyFunApps   (SubGoalDepth c f) = SubGoalDepth c (f+1)
-
-subGoalCounterValue :: SubGoalCounter -> SubGoalDepth -> Int
-subGoalCounterValue CountConstraints (SubGoalDepth c _) = c
-subGoalCounterValue CountTyFunApps   (SubGoalDepth _ f) = f
-
-subGoalDepthExceeded :: SubGoalDepth -> SubGoalDepth -> Maybe SubGoalCounter
-subGoalDepthExceeded (SubGoalDepth mc mf) (SubGoalDepth c f)
-        | c > mc    = Just CountConstraints
-        | f > mf    = Just CountTyFunApps
-        | otherwise = Nothing
-
--- | Checks whether the evidence can be used to solve a goal with the given minimum depth
--- See Note [Preventing recursive dictionaries]
-ctEvCheckDepth :: Class -> CtLoc -> CtEvidence -> Bool
-ctEvCheckDepth cls target ev
-  | isWanted ev
-  , cls == coercibleClass  -- The restriction applies only to Coercible
-  = ctLocDepth target <= ctLocDepth (ctEvLoc ev)
-  | otherwise = True
-
-{-
-Note [Preventing recursive dictionaries]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-NB: this will go away when we start treating Coercible as an equality.
-
-We have some classes where it is not very useful to build recursive
-dictionaries (Coercible, at the moment). So we need the constraint solver to
-prevent that. We conservatively ensure this property using the subgoal depth of
-the constraints: When solving a Coercible constraint at depth d, we do not
-consider evidence from a depth <= d as suitable.
+initialSubGoalDepth = SubGoalDepth 0
 
-Therefore we need to record the minimum depth allowed to solve a CtWanted. This
-is done in the SubGoalDepth field of CtWanted. Most code now uses mkCtWanted,
-which initializes it to initialSubGoalDepth (i.e. 0); but when requesting a
-Coercible instance (requestCoercible in TcInteract), we bump the current depth
-by one and use that.
-
-There are two spots where wanted contraints attempted to be solved
-using existing constraints: lookupInertDict and lookupSolvedDict in
-TcSMonad.  Both use ctEvCheckDepth to make the check. That function
-ensures that a Given constraint can always be used to solve a goal
-(i.e. they are at depth infinity, for our purposes)
+bumpSubGoalDepth :: SubGoalDepth -> SubGoalDepth
+bumpSubGoalDepth (SubGoalDepth n) = SubGoalDepth (n + 1)
 
+subGoalDepthExceeded :: DynFlags -> SubGoalDepth -> Bool
+subGoalDepthExceeded dflags (SubGoalDepth d)
+  = mkIntWithInf d > reductionDepth dflags
 
+{-
 ************************************************************************
 *                                                                      *
             CtLoc
@@ -1748,9 +1889,9 @@ data CtLoc = CtLoc { ctl_origin :: CtOrigin
                    , ctl_env    :: TcLclEnv
                    , ctl_depth  :: !SubGoalDepth }
   -- The TcLclEnv includes particularly
-  --    source location:  tcl_loc   :: SrcSpan
+  --    source location:  tcl_loc   :: RealSrcSpan
   --    context:          tcl_ctxt  :: [ErrCtxt]
-  --    binder stack:     tcl_bndrs :: [TcIdBinders]
+  --    binder stack:     tcl_bndrs :: TcIdBinderStack
   --    level:            tcl_tclvl :: TcLevel
 
 mkGivenLoc :: TcLevel -> SkolemInfo -> TcLclEnv -> CtLoc
@@ -1762,20 +1903,23 @@ mkGivenLoc tclvl skol_info env
 ctLocEnv :: CtLoc -> TcLclEnv
 ctLocEnv = ctl_env
 
+ctLocLevel :: CtLoc -> TcLevel
+ctLocLevel loc = tcl_tclvl (ctLocEnv loc)
+
 ctLocDepth :: CtLoc -> SubGoalDepth
 ctLocDepth = ctl_depth
 
 ctLocOrigin :: CtLoc -> CtOrigin
 ctLocOrigin = ctl_origin
 
-ctLocSpan :: CtLoc -> SrcSpan
+ctLocSpan :: CtLoc -> RealSrcSpan
 ctLocSpan (CtLoc { ctl_env = lcl}) = tcl_loc lcl
 
-setCtLocSpan :: CtLoc -> SrcSpan -> CtLoc
+setCtLocSpan :: CtLoc -> RealSrcSpan -> CtLoc
 setCtLocSpan ctl@(CtLoc { ctl_env = lcl }) loc = setCtLocEnv ctl (lcl { tcl_loc = loc })
 
-bumpCtLocDepth :: SubGoalCounter -> CtLoc -> CtLoc
-bumpCtLocDepth cnt loc@(CtLoc { ctl_depth = d }) = loc { ctl_depth = bumpSubGoalDepth cnt d }
+bumpCtLocDepth :: CtLoc -> CtLoc
+bumpCtLocDepth loc@(CtLoc { ctl_depth = d }) = loc { ctl_depth = bumpSubGoalDepth d }
 
 setCtLocOrigin :: CtLoc -> CtOrigin -> CtLoc
 setCtLocOrigin ctl orig = ctl { ctl_origin = orig }
@@ -1856,35 +2000,21 @@ instance Outputable SkolemInfo where
 
 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 (pprPrefixOcc f <+> dcolon <+> ppr ty)
-pprSkolInfo (SigSkol cx ty) = hang (pprUserTypeCtxt cx <> colon)
-                                 2 (ppr ty)
-pprSkolInfo (IPSkol ips)    = ptext (sLit "the implicit-parameter binding") <> plural ips <+> ptext (sLit "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 cl mc) = case cl of
-    RealDataCon dc -> sep [ ptext (sLit "a pattern with constructor")
-                          , nest 2 $ ppr dc <+> dcolon
-                            <+> pprType (dataConUserType dc) <> comma
-                            -- pprType prints forall's regardless of -fprint-explict-foralls
-                            -- which is what we want here, since we might be saying
-                            -- type variable 't' is bound by ...
-                          , ptext (sLit "in") <+> pprMatchContext mc ]
-    PatSynCon ps -> sep [ ptext (sLit "a pattern with pattern synonym")
-                        , nest 2 $ ppr ps <+> dcolon
-                          <+> pprType (patSynType ps) <> 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 ]]
+pprSkolInfo (SigSkol ctxt ty) = pprSigSkolInfo ctxt ty
+pprSkolInfo (IPSkol ips)      = ptext (sLit "the implicit-parameter binding") <> plural ips <+> ptext (sLit "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 "a data type declaration")
+pprSkolInfo FamInstSkol       = ptext (sLit "a 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 "an arrow form")
+pprSkolInfo (PatSkol cl mc)   = sep [ pprPatSkolInfo cl
+                                    , ptext (sLit "in") <+> pprMatchContext mc ]
+pprSkolInfo (InferSkol ids)   = sep [ ptext (sLit "the inferred type of")
+                                    , vcat [ ppr name <+> dcolon <+> ppr ty
+                                           | (name,ty) <- ids ]]
 pprSkolInfo (UnifyForAllSkol tvs ty) = ptext (sLit "the type") <+> ppr (mkForAllTys tvs ty)
 
 -- UnkSkol
@@ -1892,6 +2022,30 @@ pprSkolInfo (UnifyForAllSkol tvs ty) = ptext (sLit "the type") <+> ppr (mkForAll
 -- For Insts, these cases should not happen
 pprSkolInfo UnkSkol = WARN( True, text "pprSkolInfo: UnkSkol" ) ptext (sLit "UnkSkol")
 
+pprSigSkolInfo :: UserTypeCtxt -> Type -> SDoc
+pprSigSkolInfo ctxt ty
+  = case ctxt of
+       FunSigCtxt f _ -> pp_sig f
+       _              -> hang (pprUserTypeCtxt ctxt <> colon)
+                            2 (ppr ty)
+  where
+    pp_sig f = sep [ ptext (sLit "the type signature for:")
+                   , pprPrefixOcc f <+> dcolon <+> ppr ty ]
+
+pprPatSkolInfo :: ConLike -> SDoc
+pprPatSkolInfo (RealDataCon dc)
+  = sep [ ptext (sLit "a pattern with constructor:")
+        , nest 2 $ ppr dc <+> dcolon
+          <+> pprType (dataConUserType dc) <> comma ]
+          -- pprType prints forall's regardless of -fprint-explict-foralls
+          -- which is what we want here, since we might be saying
+          -- type variable 't' is bound by ...
+
+pprPatSkolInfo (PatSynCon ps)
+  = sep [ ptext (sLit "a pattern with pattern synonym:")
+        , nest 2 $ ppr ps <+> dcolon
+                   <+> pprType (patSynType ps) <> comma ]
+
 {-
 ************************************************************************
 *                                                                      *
@@ -1904,10 +2058,11 @@ data CtOrigin
   = GivenOrigin SkolemInfo
 
   -- All the others are for *wanted* constraints
-  | OccurrenceOf Name           -- Occurrence of an overloaded identifier
-  | AppOrigin                   -- An application of some kind
+  | OccurrenceOf Name              -- Occurrence of an overloaded identifier
+  | AppOrigin                      -- An application of some kind
 
-  | SpecPragOrigin Name         -- Specialisation pragma for identifier
+  | SpecPragOrigin UserTypeCtxt    -- Specialisation pragma for
+                                   -- function or instance
 
   | TypeEqOrigin { uo_actual   :: TcType
                  , uo_expected :: TcType }
@@ -1968,6 +2123,12 @@ pprCtOrigin :: CtOrigin -> SDoc
 
 pprCtOrigin (GivenOrigin sk) = ctoHerald <+> ppr sk
 
+pprCtOrigin (SpecPragOrigin ctxt) 
+  = case ctxt of
+       FunSigCtxt n _ -> ptext (sLit "a SPECIALISE pragma for") <+> quotes (ppr n)
+       SpecInstCtxt   -> ptext (sLit "a SPECIALISE INSTANCE pragma")
+       _              -> ptext (sLit "a SPECIALISE pragma")  -- Never happens I think
+
 pprCtOrigin (FunDepOrigin1 pred1 loc1 pred2 loc2)
   = hang (ctoHerald <+> ptext (sLit "a functional dependency between constraints:"))
        2 (vcat [ hang (quotes (ppr pred1)) 2 (pprArisingAt loc1)
@@ -2011,7 +2172,6 @@ pprCtOrigin simple_origin
 pprCtO :: CtOrigin -> SDoc  -- Ones that are short one-liners
 pprCtO (OccurrenceOf name)   = hsep [ptext (sLit "a use of"), quotes (ppr name)]
 pprCtO AppOrigin             = ptext (sLit "an application")
-pprCtO (SpecPragOrigin name) = hsep [ptext (sLit "a specialisation pragma for"), quotes (ppr name)]
 pprCtO (IPOccOrigin name)    = hsep [ptext (sLit "a use of implicit parameter"), quotes (ppr name)]
 pprCtO RecordUpdOrigin       = ptext (sLit "a record update")
 pprCtO ExprSigOrigin         = ptext (sLit "an expression type signature")