s/FrontendMerge/FrontendInterface/g
[ghc.git] / compiler / typecheck / TcRnTypes.hs
index 7ea9ae9..f4cfa4f 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
@@ -26,22 +26,33 @@ module TcRnTypes(
         Env(..),
         TcGblEnv(..), TcLclEnv(..),
         IfGblEnv(..), IfLclEnv(..),
+        tcVisibleOrphanMods,
 
-        -- Ranamer types
-        ErrCtxt, RecFieldEnv(..),
+        -- Frontend types (shouldn't really be here)
+        FrontendResult(..),
+
+        -- Renamer types
+        ErrCtxt, RecFieldEnv,
         ImportAvails(..), emptyImportAvails, plusImportAvails,
         WhereFrom(..), mkModDeps,
 
         -- Typechecker types
-        TcTypeEnv, TcIdBinder(..), TcTyThing(..), PromotionErr(..),
+        TcTypeEnv, TcIdBinderStack, TcIdBinder(..),
+        TcTyThing(..), PromotionErr(..),
+        SelfBootInfo(..),
         pprTcTyThingCategory, pprPECategory,
 
+        -- Desugaring types
+        DsM, DsLclEnv(..), DsGblEnv(..), PArrBuiltin(..),
+        DsMetaEnv, DsMetaVal(..),
+
         -- Template Haskell
-        ThStage(..), PendingStuff(..), topStage, topAnnStage, topSpliceStage,
+        ThStage(..), SpliceType(..), PendingStuff(..),
+        topStage, topAnnStage, topSpliceStage,
         ThLevel, impLevel, outerLevel, thLevel,
 
         -- Arrows
-        ArrowCtxt(NoArrowCtxt), newArrowScope, escapeArrowScope,
+        ArrowCtxt(..),
 
         -- Canonical constraints
         Xi, Ct(..), Cts, emptyCts, andCts, andManyCts, pprCts,
@@ -49,24 +60,25 @@ module TcRnTypes(
         isEmptyCts, isCTyEqCan, isCFunEqCan,
         isCDictCan_Maybe, isCFunEqCan_maybe,
         isCIrredEvCan, isCNonCanonical, isWantedCt, isDerivedCt,
-        isGivenCt, isHoleCt, isTypedHoleCt, isPartialTypeSigCt,
-        ctEvidence, ctLoc, ctPred, ctFlavour, ctEqRel,
+        isGivenCt, isHoleCt, isOutOfScopeCt, isExprHoleCt, isTypeHoleCt,
+        isUserTypeErrorCt, getUserTypeErrorMsg,
+        ctEvidence, ctLoc, setCtLoc, ctPred, ctFlavour, ctEqRel, ctOrigin,
         mkNonCanonical, mkNonCanonicalCt,
-        ctEvPred, ctEvLoc, ctEvEqRel,
-        ctEvTerm, ctEvCoercion, ctEvId, ctEvCheckDepth,
+        ctEvPred, ctEvLoc, ctEvOrigin, ctEvEqRel,
+        ctEvTerm, ctEvCoercion, ctEvId,
 
         WantedConstraints(..), insolubleWC, emptyWC, isEmptyWC,
         andWC, unionsWC, addSimples, addImplics, mkSimpleWC, addInsols,
-        dropDerivedWC,
+        dropDerivedWC, dropDerivedSimples, dropDerivedInsols,
+        isDroppableDerivedLoc, 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,
+        CtOrigin(..), pprCtOrigin, pprCtLoc,
         pushErrCtxt, pushErrCtxtSameOrigin,
 
         SkolemInfo(..),
@@ -79,16 +91,18 @@ module TcRnTypes(
         -- Constraint solver plugins
         TcPlugin(..), TcPluginResult(..), TcPluginSolver,
         TcPluginM, runTcPluginM, unsafeTcPluginTcM,
+        getEvBindsTcPluginM_maybe,
 
         CtFlavour(..), ctEvFlavour,
+        CtFlavourRole, ctEvFlavourRole, ctFlavourRole,
+        eqCanRewrite, eqCanRewriteFR, canDischarge, canDischargeFR,
 
         -- Pretty printing
         pprEvVarTheta,
         pprEvVars, pprEvVarWithType,
-        pprArising, pprArisingAt,
 
         -- Misc other types
-        TcId, TcIdSet, TcTyVarBind(..), TcTyVarBinds, HoleSort(..)
+        TcId, TcIdSet, HoleSort(..)
 
   ) where
 
@@ -105,7 +119,7 @@ import TyCon    ( TyCon )
 import ConLike  ( ConLike(..) )
 import DataCon  ( DataCon, dataConUserType, dataConOrigArgTys )
 import PatSyn   ( PatSyn, patSynType )
-import TysWiredIn ( coercibleClass )
+import FieldLabel ( FieldLabel )
 import TcType
 import Annotations
 import InstEnv
@@ -130,9 +144,9 @@ import DynFlags
 import Outputable
 import ListSetOps
 import FastString
+import GHC.Fingerprint
 
-import Data.Set (Set)
-import Control.Monad (ap, liftM)
+import Control.Monad (ap, liftM, msum)
 
 #ifdef GHCI
 import Data.Map      ( Map )
@@ -153,27 +167,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 +187,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 +212,137 @@ 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
+*                                                                      *
+************************************************************************
+-}
+
+-- | 'FrontendResult' describes the result of running the
+-- frontend of a Haskell module.  Usually, you'll get
+-- a 'FrontendTypecheck', since running the frontend involves
+-- typechecking a program, but for an hs-boot merge you'll
+-- just get a ModIface, since no actual typechecking occurred.
+--
+-- This data type really should be in HscTypes, but it needs
+-- to have a TcGblEnv which is only defined here.
+data FrontendResult
+        = FrontendTypecheck TcGblEnv
+        | FrontendInterface ModIface
+
 -- | '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
@@ -235,7 +352,7 @@ data TcGblEnv
   = TcGblEnv {
         tcg_mod     :: Module,         -- ^ Module being compiled
         tcg_src     :: HscSource,
-          -- ^ What kind of module (regular Haskell, hs-boot, ext-core)
+          -- ^ What kind of module (regular Haskell, hs-boot, hsig)
         tcg_sig_of  :: Maybe Module,
           -- ^ Are we being compiled as a signature of an implementation?
         tcg_impl_rdr_env :: Maybe GlobalRdrEnv,
@@ -273,12 +390,6 @@ data TcGblEnv
         tcg_fam_inst_env :: FamInstEnv, -- ^ Ditto for family instances
         tcg_ann_env      :: AnnEnv,     -- ^ And for annotations
 
-        tcg_visible_orphan_mods :: ModuleSet,
-          -- ^ The set of orphan modules which transitively reachable from
-          -- direct imports.  We use this to figure out if an orphan instance
-          -- in the global InstEnv should be considered visible.
-          -- See Note [Instance lookup and orphan instances] in InstEnv
-
                 -- Now a bunch of things about this module that are simply
                 -- accumulated, but never consulted until the end.
                 -- Nevertheless, it's convenient to accumulate them along
@@ -289,8 +400,8 @@ data TcGblEnv
           -- things bound in this module. Also store Safe Haskell info
           -- here about transative trusted packaage requirements.
 
-        tcg_dus :: DefUses,   -- ^ What is defined in this module and what is used.
-        tcg_used_rdrnames :: TcRef (Set RdrName),
+        tcg_dus       :: DefUses,   -- ^ What is defined in this module and what is used.
+        tcg_used_gres :: TcRef [GlobalRdrElt],  -- ^ Records occurrences of imported entities
           -- See Note [Tracking unused binding and imports]
 
         tcg_keep :: TcRef NameSet,
@@ -334,6 +445,10 @@ 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
+                -- Is always Nothing if we don't want to retain renamed
+                -- exports
+
         tcg_rn_imports :: [LImportDecl Name],
                 -- Keep the renamed imports regardless.  They are not
                 -- voluminous and are needed if you want to report unused imports
@@ -360,39 +475,52 @@ 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_tr_module :: Maybe Id,           -- Id for $trModule :: GHC.Types.Module
+                                             -- for which every module has a top-level defn
+                                             -- except in GHCi in which case we have Nothing
+        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
                                              --  prog uses hpc instrumentation.
 
+        tcg_self_boot :: SelfBootInfo,       -- ^ Whether this module has a
+                                             -- corresponding hi-boot file
+
         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.
     }
 
+tcVisibleOrphanMods :: TcGblEnv -> ModuleSet
+tcVisibleOrphanMods tcg_env
+    = mkModuleSet (tcg_mod tcg_env : imp_orphs (tcg_imports tcg_env))
+
 -- Note [Signature parameters in TcGblEnv and DynFlags]
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 -- When compiling signature files, we need to know which implementation
@@ -443,23 +571,28 @@ data TcGblEnv
 instance ContainsModule TcGblEnv where
     extractModule env = tcg_mod env
 
-data RecFieldEnv
-  = RecFields (NameEnv [Name])  -- Maps a constructor name *in this module*
-                                -- to the fields for that constructor
-              NameSet           -- Set of all fields declared *in this module*;
-                                -- used to suppress name-shadowing complaints
-                                -- when using record wild cards
-                                -- E.g.  let fld = e in C {..}
+type RecFieldEnv = NameEnv [FieldLabel]
+        -- Maps a constructor name *in this module*
+        -- to the fields for that constructor.
         -- This is used when dealing with ".." notation in record
         -- construction and pattern matching.
         -- The FieldEnv deals *only* with constructors defined in *this*
         -- module.  For imported modules, we get the same info from the
         -- TypeEnv
 
-{-
-Note [Tracking unused binding and imports]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+data SelfBootInfo
+  = NoSelfBoot    -- No corresponding hi-boot file
+  | SelfBoot
+       { sb_mds :: ModDetails   -- There was a hi-boot file,
+       , sb_tcs :: NameSet      -- defining these TyCons,
+       , sb_ids :: NameSet }    -- and these Ids
+  -- We need this info to compute a safe approximation to
+  -- recursive loops, to avoid infinite inlinings
+
+{- Note [Tracking unused binding and imports]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We gather two sorts of usage information
+
  * tcg_dus (defs/uses)
       Records *defined* Names (local, top-level)
           and *used*    Names (local or imported)
@@ -471,56 +604,17 @@ We gather two sorts of usage information
    This usage info is mainly gathered by the renamer's
    gathering of free-variables
 
- * tcg_used_rdrnames
-      Records used *imported* (not locally-defined) RdrNames
+ * tcg_used_gres
       Used only to report unused import declarations
-      Notice that they are RdrNames, not Names, so we can
-      tell whether the reference was qualified or unqualified, which
-      is esssential in deciding whether a particular import decl
-      is unnecessary.  This info isn't present in Names.
 
+      Records each *occurrence* an *imported* (not locally-defined) entity.
+      The occurrence is recorded by keeping a GlobalRdrElt for it.
+      These is not the GRE that is in the GlobalRdrEnv; rather it
+      is recorded *after* the filtering done by pickGREs.  So it reflect
+      /how that occurrence is in scope/.   See Note [GRE filtering] in
+      RdrName.
 
-************************************************************************
-*                                                                      *
-                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 +640,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 +665,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 +691,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,16 +705,43 @@ 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
 ---------------------------
 
+data SpliceType = Typed | Untyped
+
 data ThStage    -- See Note [Template Haskell state diagram] in TcSplice
-  = Splice      -- Inside a top-level splice splice
-                -- This code will be run *at compile time*;
-                --   the result replaces the splice
-                -- Binding level = 0
-      Bool      -- True if in a typed splice, False otherwise
+  = Splice SpliceType -- Inside a top-level splice
+                      -- This code will be run *at compile time*;
+                      --   the result replaces the splice
+                      -- Binding level = 0
 
   | Comp        -- Ordinary Haskell code
                 -- Binding level = 1
@@ -649,8 +762,8 @@ data PendingStuff
 
 topStage, topAnnStage, topSpliceStage :: ThStage
 topStage       = Comp
-topAnnStage    = Splice False
-topSpliceStage = Splice False
+topAnnStage    = Splice Untyped
+topSpliceStage = Splice Untyped
 
 instance Outputable ThStage where
    ppr (Splice _)  = text "Splice"
@@ -698,31 +811,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)
-
--- 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 } }
+  | ArrowCtxt LocalRdrEnv (TcRef WantedConstraints)
 
--- 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 +897,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,12 +910,13 @@ 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
 
+Invariant: a closed variable has no free type variables in its type.
+
 Under OutsideIn we are free to generalise a closed let-binding.
 This is an extension compared to the JFP paper on OutsideIn, which
 used "top-level" as a proxy for "closed".  (It's not a good proxy
@@ -812,7 +924,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
@@ -855,27 +967,11 @@ type ErrCtxt = (Bool, TidyEnv -> TcM (TidyEnv, MsgDoc))
 data ImportAvails
    = ImportAvails {
         imp_mods :: ImportedMods,
-          --      = ModuleEnv [(ModuleName, Bool, SrcSpan, Bool)],
+          --      = ModuleEnv [ImportedModsVal],
           -- ^ Domain is all directly-imported modules
-          -- The 'ModuleName' is what the module was imported as, e.g. in
-          -- @
-          --     import Foo as Bar
-          -- @
-          -- it is @Bar@.
-          --
-          -- The 'Bool' means:
           --
-          --  - @True@ => import was @import Foo ()@
-          --
-          --  - @False@ => import was some other form
-          --
-          -- Used
-          --
-          --   (a) to help construct the usage information in the interface
-          --       file; if we import something we need to recompile if the
-          --       export version changes
-          --
-          --   (b) to specify what child modules to initialise
+          -- See the documentaion on ImportedModsVal in HscTypes for the
+          -- meaning of the fields.
           --
           -- We need a full ModuleEnv rather than a ModuleNameEnv here,
           -- because we might be importing modules of the same name from
@@ -892,17 +988,17 @@ data ImportAvails
           -- compiling M might not need to consult X.hi, but X
           -- is still listed in M's dependencies.
 
-        imp_dep_pkgs :: [PackageKey],
+        imp_dep_pkgs :: [UnitId],
           -- ^ Packages needed by the module being compiled, whether directly,
           -- or via other modules in this package, or via modules imported
           -- from other packages.
 
-        imp_trust_pkgs :: [PackageKey],
+        imp_trust_pkgs :: [UnitId],
           -- ^ This is strictly a subset of imp_dep_pkgs and records the
           -- packages the current module needs to trust for Safe Haskell
           -- compilation to succeed. A package is required to be trusted if
           -- we are dependent on a trustworthy module in that package.
-          -- While perhaps making imp_dep_pkgs a tuple of (PackageKey, Bool)
+          -- While perhaps making imp_dep_pkgs a tuple of (UnitId, Bool)
           -- where True for the bool indicates the package is required to be
           -- trusted is the more logical  design, doing so complicates a lot
           -- of code not concerned with Safe Haskell.
@@ -1057,7 +1153,6 @@ data Ct
        --   * isTypeFamilyTyCon cc_fun
        --   * typeKind (F xis) = tyVarKind fsk
        --   * always Nominal role
-       --   * always Given or Wanted, never Derived
       cc_ev     :: CtEvidence,  -- See Note [Ct/evidence invariant]
       cc_fun    :: TyCon,       -- A type function
 
@@ -1075,8 +1170,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 +1183,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,
@@ -1174,6 +1282,12 @@ ctEvidence = cc_ev
 ctLoc :: Ct -> CtLoc
 ctLoc = ctEvLoc . ctEvidence
 
+setCtLoc :: Ct -> CtLoc -> Ct
+setCtLoc ct loc = ct { cc_ev = (cc_ev ct) { ctev_loc = loc } }
+
+ctOrigin :: Ct -> CtOrigin
+ctOrigin = ctLocOrigin . ctLoc
+
 ctPred :: Ct -> PredType
 -- See Note [Ct/evidence invariant]
 ctPred ct = ctEvPred (cc_ev ct)
@@ -1188,34 +1302,68 @@ 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 = not (isDroppableDerivedLoc (ctLoc ct))
+      | otherwise      = True
+
+isDroppableDerivedLoc :: CtLoc -> Bool
+-- Note [Dropping derived constraints]
+isDroppableDerivedLoc loc
+  = case ctLocOrigin loc of
+      KindEqOrigin {}  -> False
+      GivenOrigin {}   -> False
+      FunDepOrigin1 {} -> False
+      FunDepOrigin2 {} -> False
+      _                -> True
+
+
+{- 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 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)
 
- * 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)
+Moreover, we keep *all* derived insolubles under some circumstances:
 
-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.
+  * They are looked at by simplifyInfer, to decide whether to
+    generalise.  Example: [W] a ~ Int, [W] a ~ Bool
+    We get [D] Int ~ Bool, and indeed the constraints are insoluble,
+    and we want simplifyInfer to see that, even though we don't
+    ultimately want to generate an (inexplicable) error message from
+
+To distinguish these cases we use the CtOrigin.
 
 
 ************************************************************************
@@ -1264,13 +1412,38 @@ isHoleCt:: Ct -> Bool
 isHoleCt (CHoleCan {}) = True
 isHoleCt _ = False
 
-isTypedHoleCt :: Ct -> Bool
-isTypedHoleCt (CHoleCan { cc_hole = ExprHole }) = True
-isTypedHoleCt _ = False
+isOutOfScopeCt :: Ct -> Bool
+-- A Hole that does not have a leading underscore is
+-- simply an out-of-scope variable, and we treat that
+-- a bit differently when it comes to error reporting
+isOutOfScopeCt (CHoleCan { cc_occ = occ }) = not (startsWithUnderscore occ)
+isOutOfScopeCt _ = False
+
+isExprHoleCt :: Ct -> Bool
+isExprHoleCt (CHoleCan { cc_hole = ExprHole }) = True
+isExprHoleCt _ = False
+
+isTypeHoleCt :: Ct -> Bool
+isTypeHoleCt (CHoleCan { cc_hole = TypeHole }) = True
+isTypeHoleCt _ = False
+
+-- | The following constraints are considered to be a custom type error:
+--    1. TypeError msg
+--    2. TypeError msg ~ Something  (and the other way around)
+--    3. C (TypeError msg)          (for any parameter of class constraint)
+getUserTypeErrorMsg :: Ct -> Maybe (Kind, Type)
+getUserTypeErrorMsg ct
+  | Just (_,t1,t2) <- getEqPredTys_maybe ctT    = oneOf [t1,t2]
+  | Just (_,ts)    <- getClassPredTys_maybe ctT = oneOf ts
+  | otherwise                                   = isUserErrorTy ctT
+  where
+  ctT       = ctPred ct
+  oneOf xs  = msum (map isUserErrorTy xs)
 
-isPartialTypeSigCt :: Ct -> Bool
-isPartialTypeSigCt (CHoleCan { cc_hole = TypeHole }) = True
-isPartialTypeSigCt _ = False
+isUserTypeErrorCt :: Ct -> Bool
+isUserTypeErrorCt ct = case getUserTypeErrorMsg ct of
+                         Just _ -> True
+                         _      -> False
 
 instance Outputable Ct where
   ppr ct = ppr (cc_ev ct) <+> parens (text ct_sort)
@@ -1340,22 +1513,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 +1536,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 +1545,28 @@ 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 :: TcLevel -> WantedConstraints -> Bool
+insolubleWC tc_lvl (WC { wc_impl = implics, wc_insol = insols })
+  =  anyBag (trulyInsoluble tc_lvl) insols
+  || anyBag insolubleImplic implics
+
+trulyInsoluble :: TcLevel -> 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) an out-of-scope variable
+-- Yuk!
+trulyInsoluble tc_lvl insol
+  =  isOutOfScopeCt insol
+  || isRigidEqPred tc_lvl (classifyPredType (ctPred insol))
+
 instance Outputable WantedConstraints where
   ppr (WC {wc_simple = s, wc_impl = i, wc_insol = n})
    = ptext (sLit "WC") <+> braces (vcat
@@ -1415,32 +1605,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 +1740,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
@@ -1549,6 +1795,9 @@ ctEvPred = ctev_pred
 ctEvLoc :: CtEvidence -> CtLoc
 ctEvLoc = ctev_loc
 
+ctEvOrigin :: CtEvidence -> CtOrigin
+ctEvOrigin = ctLocOrigin . ctEvLoc
+
 -- | Get the equality relation relevant for a 'CtEvidence'
 ctEvEqRel :: CtEvidence -> EqRel
 ctEvEqRel = predTypeEqRel . ctEvPred
@@ -1558,25 +1807,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)
@@ -1618,6 +1861,94 @@ ctEvFlavour (CtWanted {})  = Wanted
 ctEvFlavour (CtGiven {})   = Given
 ctEvFlavour (CtDerived {}) = Derived
 
+-- | Whether or not one 'Ct' can rewrite another is determined by its
+-- flavour and its equality relation
+type CtFlavourRole = (CtFlavour, EqRel)
+
+-- | Extract the flavour and role from a 'CtEvidence'
+ctEvFlavourRole :: CtEvidence -> CtFlavourRole
+ctEvFlavourRole ev = (ctEvFlavour ev, ctEvEqRel ev)
+
+-- | Extract the flavour and role from a 'Ct'
+ctFlavourRole :: Ct -> CtFlavourRole
+ctFlavourRole = ctEvFlavourRole . cc_ev
+
+{- Note [eqCanRewrite]
+~~~~~~~~~~~~~~~~~~~
+(eqCanRewrite ct1 ct2) holds if the constraint ct1 (a CTyEqCan of form
+tv ~ ty) can be used to rewrite ct2.  It must satisfy the properties of
+a can-rewrite relation, see Definition [Can-rewrite relation]
+
+With the solver handling Coercible constraints like equality constraints,
+the rewrite conditions must take role into account, never allowing
+a representational equality to rewrite a nominal one.
+
+Note [Wanteds do not rewrite Wanteds]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We don't allow Wanteds to rewrite Wanteds, because that can give rise
+to very confusing type error messages.  A good example is Trac #8450.
+Here's another
+   f :: a -> Bool
+   f x = ( [x,'c'], [x,True] ) `seq` True
+Here we get
+  [W] a ~ Char
+  [W] a ~ Bool
+but we do not want to complain about Bool ~ Char!
+
+Note [Deriveds do rewrite Deriveds]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+However we DO allow Deriveds to rewrite Deriveds, because that's how
+improvement works; see Note [The improvement story] in TcInteract.
+
+However, for now at least I'm only letting (Derived,NomEq) rewrite
+(Derived,NomEq) and not doing anything for ReprEq.  If we have
+    eqCanRewriteFR (Derived, NomEq) (Derived, _)  = True
+then we lose the property of Note [Can-rewrite relation]
+  R2.  If f1 >= f, and f2 >= f,
+       then either f1 >= f2 or f2 >= f1
+Consider f1 = (Given, ReprEq)
+         f2 = (Derived, NomEq)
+          f = (Derived, ReprEq)
+
+I thought maybe we could never get Derived ReprEq constraints, but
+we can; straight from the Wanteds during improvment. And from a Derived
+ReprEq we could conceivably get a Derived NomEq improvment (by decomposing
+a type constructor with Nomninal role), and hence unify.
+
+Note [canRewriteOrSame]
+~~~~~~~~~~~~~~~~~~~~~~~
+canRewriteOrSame is similar but
+ * returns True for Wanted/Wanted.
+ * works for all kinds of constraints, not just CTyEqCans
+See the call sites for explanations.
+-}
+
+eqCanRewrite :: CtEvidence -> CtEvidence -> Bool
+eqCanRewrite ev1 ev2 = ctEvFlavourRole ev1 `eqCanRewriteFR` ctEvFlavourRole ev2
+
+eqCanRewriteFR :: CtFlavourRole -> CtFlavourRole -> Bool
+-- Very important function!
+-- See Note [eqCanRewrite]
+-- See Note [Wanteds do not rewrite Wanteds]
+-- See Note [Deriveds do rewrite Deriveds]
+eqCanRewriteFR (Given,   NomEq)   (_,       _)      = True
+eqCanRewriteFR (Given,   ReprEq)  (_,       ReprEq) = True
+eqCanRewriteFR (Derived, NomEq)   (Derived, NomEq)  = True
+eqCanRewriteFR _                 _                  = False
+
+canDischarge :: CtEvidence -> CtEvidence -> Bool
+-- See Note [canRewriteOrSame]
+canDischarge ev1 ev2 = ctEvFlavourRole ev1 `canDischargeFR` ctEvFlavourRole ev2
+
+canDischargeFR :: CtFlavourRole -> CtFlavourRole -> Bool
+canDischargeFR (_, ReprEq)  (_, NomEq)   = False
+canDischargeFR (Given, _)   _            = True
+canDischargeFR (Wanted, _)  (Wanted, _)  = True
+canDischargeFR (Wanted, _)  (Derived, _) = True
+canDischargeFR (Derived, _) (Derived, _) = True
+canDischargeFR _             _           = False
+
+
 {-
 ************************************************************************
 *                                                                      *
@@ -1627,31 +1958,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 +1989,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
+initialSubGoalDepth = SubGoalDepth 0
 
-{-
-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.
-
-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 +2036,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 +2050,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 }
@@ -1792,17 +2083,6 @@ pushErrCtxtSameOrigin :: ErrCtxt -> CtLoc -> CtLoc
 pushErrCtxtSameOrigin err loc@(CtLoc { ctl_env = lcl })
   = loc { ctl_env = lcl { tcl_ctxt = err : tcl_ctxt lcl } }
 
-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 orig              = pprCtOrigin orig
-
-pprArisingAt :: CtLoc -> SDoc
-pprArisingAt (CtLoc { ctl_origin = o, ctl_env = lcl})
-  = sep [ pprCtOrigin o
-        , text "at" <+> ppr (tcl_loc lcl)]
-
 {-
 ************************************************************************
 *                                                                      *
@@ -1821,7 +2101,14 @@ data SkolemInfo
 
         -- The rest are for non-scoped skolems
   | ClsSkol Class       -- Bound at a class decl
+
   | InstSkol            -- Bound at an instance decl
+  | InstSC TypeSize     -- A "given" constraint obtained by superclass selection.
+                        -- If (C ty1 .. tyn) is the largest class from
+                        --    which we made a superclass selection in the chain,
+                        --    then TypeSize = sizeTypes [ty1, .., tyn]
+                        -- See Note [Solving superclass constraints] in TcInstDcls
+
   | DataSkol            -- Bound at a data type declaration
   | FamInstSkol         -- Bound at a family instance decl
   | PatSkol             -- An existential type variable bound by a pattern for
@@ -1856,35 +2143,22 @@ 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 (InstSC n)        = ptext (sLit "the instance declaration") <> ifPprDebug (parens (ppr n))
+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") <+> pprRuleName 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 +2166,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 = vcat [ ptext (sLit "the type signature for:")
+                    , nest 2 (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,17 +2202,18 @@ 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
+  | OccurrenceOfRecSel RdrName     -- Occurrence of a record selector
+  | 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 }
   | KindEqOrigin
       TcType TcType             -- A kind equality arising from unifying these two types
       CtOrigin                  -- originally arising from this
-  | CoercibleOrigin TcType TcType  -- a Coercible constraint
 
   | IPOccOrigin  HsIPName       -- Occurrence of an implicit parameter
 
@@ -1931,7 +2230,11 @@ data CtOrigin
   | RecordUpdOrigin
   | ViewPatOrigin
 
-  | ScOrigin            -- Typechecking superclasses of an instance declaration
+  | ScOrigin TypeSize   -- Typechecking superclasses of an instance declaration
+                        -- If the instance head is C ty1 .. tyn
+                        --    then TypeSize = sizeTypes [ty1, .., tyn]
+                        -- See Note [Solving superclass constraints] in TcInstDcls
+
   | DerivOrigin         -- Typechecking deriving
   | DerivOriginDC DataCon Int
                         -- Checking constraints arising from this data con and field index
@@ -1964,19 +2267,33 @@ data CtOrigin
 ctoHerald :: SDoc
 ctoHerald = ptext (sLit "arising from")
 
-pprCtOrigin :: CtOrigin -> SDoc
+pprCtLoc :: CtLoc -> SDoc
+-- "arising from ... at ..."
+-- Not an instance of Outputable because of the "arising from" prefix
+pprCtLoc (CtLoc { ctl_origin = o, ctl_env = lcl})
+  = sep [ pprCtOrigin o
+        , text "at" <+> ppr (tcl_loc lcl)]
 
+pprCtOrigin :: CtOrigin -> SDoc
+-- "arising from ..."
+-- Not an instance of Outputable because of the "arising from" prefix
 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)
-               , hang (quotes (ppr pred2)) 2 (pprArisingAt loc2) ])
+       2 (vcat [ hang (quotes (ppr pred1)) 2 (pprCtLoc loc1)
+               , hang (quotes (ppr pred2)) 2 (pprCtLoc loc2) ])
 
 pprCtOrigin (FunDepOrigin2 pred1 orig1 pred2 loc2)
   = hang (ctoHerald <+> ptext (sLit "a functional dependency between:"))
        2 (vcat [ hang (ptext (sLit "constraint") <+> quotes (ppr pred1))
-                    2 (pprArising orig1 )
+                    2 (pprCtOrigin orig1 )
                , hang (ptext (sLit "instance") <+> quotes (ppr pred2))
                     2 (ptext (sLit "at") <+> ppr loc2) ])
 
@@ -1999,19 +2316,14 @@ pprCtOrigin (DerivOriginCoerce meth ty1 ty2)
        2 (sep [ text "from type" <+> quotes (ppr ty1)
               , nest 2 $ text "to type" <+> quotes (ppr ty2) ])
 
-pprCtOrigin (CoercibleOrigin ty1 ty2)
-  = hang (ctoHerald <+> text "trying to show that the representations of")
-       2 (quotes (ppr ty1) <+> text "and" $$
-          quotes (ppr ty2) <+> text "are the same")
-
 pprCtOrigin simple_origin
   = ctoHerald <+> pprCtO simple_origin
 
 ----------------
 pprCtO :: CtOrigin -> SDoc  -- Ones that are short one-liners
 pprCtO (OccurrenceOf name)   = hsep [ptext (sLit "a use of"), quotes (ppr name)]
+pprCtO (OccurrenceOfRecSel 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")
@@ -2025,7 +2337,8 @@ pprCtO (PArrSeqOrigin seq)   = hsep [ptext (sLit "the parallel array sequence"),
 pprCtO SectionOrigin         = ptext (sLit "an operator section")
 pprCtO TupleOrigin           = ptext (sLit "a tuple")
 pprCtO NegateOrigin          = ptext (sLit "a use of syntactic negation")
-pprCtO ScOrigin              = ptext (sLit "the superclasses of an instance declaration")
+pprCtO (ScOrigin n)          = ptext (sLit "the superclasses of an instance declaration")
+                               <> ifPprDebug (parens (ppr n))
 pprCtO DerivOrigin           = ptext (sLit "the 'deriving' clause of a data type declaration")
 pprCtO StandAloneDerivOrigin = ptext (sLit "a 'deriving' declaration")
 pprCtO DefaultOrigin         = ptext (sLit "a 'default' declaration")
@@ -2049,31 +2362,37 @@ type TcPluginSolver = [Ct]    -- given
                    -> [Ct]    -- wanted
                    -> TcPluginM TcPluginResult
 
-newtype TcPluginM a = TcPluginM (TcM a)
+newtype TcPluginM a = TcPluginM (Maybe EvBindsVar -> TcM a)
 
 instance Functor     TcPluginM where
   fmap = liftM
 
 instance Applicative TcPluginM where
-  pure  = return
+  pure x = TcPluginM (const $ pure x)
   (<*>) = ap
 
 instance Monad TcPluginM where
-  return x = TcPluginM (return x)
-  fail x   = TcPluginM (fail x)
+  return = pure
+  fail x   = TcPluginM (const $ fail x)
   TcPluginM m >>= k =
-    TcPluginM (do a <- m
-                  let TcPluginM m1 = k a
-                  m1)
+    TcPluginM (\ ev -> do a <- m ev
+                          runTcPluginM (k a) ev)
 
-runTcPluginM :: TcPluginM a -> TcM a
+runTcPluginM :: TcPluginM a -> Maybe EvBindsVar -> TcM a
 runTcPluginM (TcPluginM m) = m
 
 -- | This function provides an escape for direct access to
 -- the 'TcM` monad.  It should not be used lightly, and
 -- the provided 'TcPluginM' API should be favoured instead.
 unsafeTcPluginTcM :: TcM a -> TcPluginM a
-unsafeTcPluginTcM = TcPluginM
+unsafeTcPluginTcM = TcPluginM . const
+
+-- | Access the 'EvBindsVar' carried by the 'TcPluginM' during
+-- constraint solving.  Returns 'Nothing' if invoked during
+-- 'tcPluginInit' or 'tcPluginStop'.
+getEvBindsTcPluginM_maybe :: TcPluginM (Maybe EvBindsVar)
+getEvBindsTcPluginM_maybe = TcPluginM return
+
 
 data TcPlugin = forall s. TcPlugin
   { tcPluginInit  :: TcPluginM s