New handling of overlapping inst in Safe Haskell
[ghc.git] / compiler / typecheck / TcRnTypes.hs
index dbafa52..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,13 +27,14 @@ 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
@@ -57,16 +58,16 @@ module TcRnTypes(
         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, insolubleImplic, trulyInsoluble,
+        dropDerivedWC, dropDerivedSimples, dropDerivedInsols,
+        insolubleImplic, trulyInsoluble,
 
         Implication(..), ImplicStatus(..), isInsolubleStatus,
-        SubGoalCounter(..),
-        SubGoalDepth, initialSubGoalDepth, maxSubGoalDepth,
-        bumpSubGoalDepth, subGoalCounterValue, subGoalDepthExceeded,
+        SubGoalDepth, initialSubGoalDepth,
+        bumpSubGoalDepth, subGoalDepthExceeded,
         CtLoc(..), ctLocSpan, ctLocEnv, ctLocLevel, ctLocOrigin,
         ctLocDepth, bumpCtLocDepth,
         setCtLocOrigin, setCtLocEnv, setCtLocSpan,
@@ -109,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
@@ -334,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]
@@ -430,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
@@ -459,18 +463,18 @@ data TcGblEnv
         -- 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_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
@@ -479,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.
@@ -627,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)
@@ -654,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
@@ -684,6 +682,24 @@ 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
 ---------------------------
 
@@ -783,6 +799,9 @@ data ArrowCtxt   -- Note [Escaping the arrow scope]
 -- 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
 
@@ -845,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
@@ -859,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.
@@ -872,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
@@ -1261,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.
 
 
 ************************************************************************
@@ -1436,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 }
@@ -1457,10 +1500,16 @@ insolubleWC (WC { wc_impl = implics, wc_insol = insols })
   || anyBag insolubleImplic implics
 
 trulyInsoluble :: Ct -> Bool
--- The constraint is in the wc_insol set, but we do not
--- treat type-holes, arising from PartialTypeSignatures,
--- as "truly insoluble". Yuk.
-trulyInsoluble insol = not (isTypeHoleCt insol)
+-- 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})
@@ -1635,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
@@ -1674,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)
@@ -1743,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
@@ -1775,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.
+initialSubGoalDepth = SubGoalDepth 0
 
-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.
-
-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
@@ -1866,7 +1891,7 @@ data CtLoc = CtLoc { ctl_origin :: CtOrigin
   -- The TcLclEnv includes particularly
   --    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
@@ -1893,8 +1918,8 @@ ctLocSpan (CtLoc { ctl_env = lcl}) = tcl_loc lcl
 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 }
@@ -2033,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 }
@@ -2097,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)
@@ -2140,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")