Refactor default methods (Trac #11105)

This patch does some signficant refactoring to the treatment
of default methods in class declarations, and more generally
to the type checking of type/class decls.

Highlights:

* When the class has a generic-default method, such as
     class C a where
       op :: a -> a -> Bool
       default op :: Ord a => a -> a -> a
  the ClassOpItem records the type of the generic-default,
  in this case the type (Ord a => a -> a -> a)

* I killed off Class.DefMeth in favour of the very-similar
  BasicTypes.DefMethSpec.  However it turned out to be better
  to use a Maybe, thus
      Maybe (DefMethSpec Type)
  with Nothing meaning "no default method".

* In TcTyClsDecls.tcTyClGroup, we used to accumulate a [TyThing],
  but I found a way to make it much simpler, accumulating only
  a [TyCon].  Much less wrapping and unwrapping.

* On the way I also fixed Trac #10896 in a better way. Instead
  of killing off all ambiguity checks whenever there are any type
  errors (the fix in commit 8e8b9ed), I instead recover in
  TcTyClsDecls.checkValidTyCl.

There was a lot of associated simplification all round

25 files changed, 386 insertions, 303 deletions

diff --git a/compiler/basicTypes/BasicTypes.hs b/compiler/basicTypes/BasicTypes.hs
index a3033dba94..ae51d07458 100644
--- a/compiler/basicTypes/BasicTypes.hs
+++ b/compiler/basicTypes/BasicTypes.hs
@@ -765,19 +765,17 @@ instance Outputable OccInfo where
 
 The DefMethSpec enumeration just indicates what sort of default method
 is used for a class. It is generated from source code, and present in
-interface files; it is converted to Class.DefMeth before begin put in a
+interface files; it is converted to Class.DefMethInfo before begin put in a
 Class object.
 -}
 
-data DefMethSpec = NoDM        -- No default method
-                 | VanillaDM   -- Default method given with polymorphic code
-                 | GenericDM   -- Default method given with generic code
-  deriving Eq
+data DefMethSpec ty
+  = VanillaDM     -- Default method given with polymorphic code
+  | GenericDM ty  -- Default method given with code of this type
 
-instance Outputable DefMethSpec where
-  ppr NoDM      = empty
-  ppr VanillaDM = ptext (sLit "{- Has default method -}")
-  ppr GenericDM = ptext (sLit "{- Has generic default method -}")
+instance Outputable (DefMethSpec ty) where
+  ppr VanillaDM      = ptext (sLit "{- Has default method -}")
+  ppr (GenericDM {}) = ptext (sLit "{- Has generic default method -}")
 
 {-
 ************************************************************************
diff --git a/compiler/hsSyn/HsDecls.hs b/compiler/hsSyn/HsDecls.hs
index 91c04fa08c..f75fff10af 100644
--- a/compiler/hsSyn/HsDecls.hs
+++ b/compiler/hsSyn/HsDecls.hs
@@ -368,8 +368,8 @@ Default methods
    E.g. $dmmax
 
  - If there is a default method name at all, it's recorded in
-   the ClassOpSig (in HsBinds), in the DefMeth field.
-   (DefMeth is defined in Class.hs)
+   the ClassOpSig (in HsBinds), in the DefMethInfo field.
+   (DefMethInfo is defined in Class.hs)
 
 Source-code class decls and interface-code class decls are treated subtly
 differently, which has given me a great deal of confusion over the years.
@@ -390,7 +390,8 @@ In *source-code* class declarations:
           op2 :: <type>
           op1 = ...
    We generate a binding for $dmop1 but not for $dmop2.
-   The Class for Foo has a NoDefMeth for op2 and a DefMeth for op1.
+   The Class for Foo has a Nothing for op2 and
+                         a Just ($dm_op1, VanillaDM) for op1.
    The Name for $dmop2 is simply discarded.
 
 In *interface-file* class declarations:
diff --git a/compiler/iface/BuildTyCl.hs b/compiler/iface/BuildTyCl.hs
index 6085b0cc3c..0b8680d164 100644
--- a/compiler/iface/BuildTyCl.hs
+++ b/compiler/iface/BuildTyCl.hs
@@ -230,7 +230,7 @@ buildPatSyn src_name declared_infix matcher@(matcher_id,_) builder
 
 -- ------------------------------------------------------
 
-type TcMethInfo = (Name, DefMethSpec, Type)
+type TcMethInfo = (Name, Type, Maybe (DefMethSpec Type))
         -- A temporary intermediate, to communicate between
         -- tcClassSigs and buildClass.
 
@@ -279,7 +279,7 @@ buildClass tycon_name tvs roles sc_theta fds at_items sig_stuff mindef tc_isrec
                 --     class C a => D a
                 -- we don't get a newtype with no arguments!
               args      = sc_sel_names ++ op_names
-              op_tys    = [ty | (_,_,ty) <- sig_stuff]
+              op_tys    = [ty | (_,ty,_) <- sig_stuff]
               op_names  = [op | (op,_,_) <- sig_stuff]
               arg_tys   = sc_theta ++ op_tys
               rec_tycon = classTyCon rec_clas
@@ -327,13 +327,11 @@ buildClass tycon_name tvs roles sc_theta fds at_items sig_stuff mindef tc_isrec
     no_bang = HsSrcBang Nothing NoSrcUnpack NoSrcStrict
 
     mk_op_item :: Class -> TcMethInfo -> TcRnIf n m ClassOpItem
-    mk_op_item rec_clas (op_name, dm_spec, _)
+    mk_op_item rec_clas (op_name, _, dm_spec)
       = do { dm_info <- case dm_spec of
-                          NoDM      -> return NoDefMeth
-                          GenericDM -> do { dm_name <- newImplicitBinder op_name mkGenDefMethodOcc
-                                          ; return (GenDefMeth dm_name) }
-                          VanillaDM -> do { dm_name <- newImplicitBinder op_name mkDefaultMethodOcc
-                                          ; return (DefMeth dm_name) }
+                          Nothing   -> return Nothing
+                          Just spec -> do { dm_name <- newImplicitBinder op_name mkDefaultMethodOcc
+                                          ; return (Just (dm_name, spec)) }
            ; return (mkDictSelId op_name rec_clas, dm_info) }
 
 {-
diff --git a/compiler/iface/IfaceSyn.hs b/compiler/iface/IfaceSyn.hs
index 41d6779785..463078ce67 100644
--- a/compiler/iface/IfaceSyn.hs
+++ b/compiler/iface/IfaceSyn.hs
@@ -173,10 +173,13 @@ data IfaceFamTyConFlav
   | IfaceAbstractClosedSynFamilyTyCon
   | IfaceBuiltInSynFamTyCon -- for pretty printing purposes only
 
-data IfaceClassOp = IfaceClassOp IfaceTopBndr DefMethSpec IfaceType
-        -- Nothing    => no default method
-        -- Just False => ordinary polymorphic default method
-        -- Just True  => generic default method
+data IfaceClassOp
+  = IfaceClassOp IfaceTopBndr
+                 IfaceType                         -- Class op type
+                 (Maybe (DefMethSpec IfaceType))   -- Default method
+                 -- The types of both the class op itself,
+                 -- and the default method, are *not* quantifed
+                 -- over the class variables
 
 data IfaceAT = IfaceAT  -- See Class.ClassATItem
                   IfaceDecl          -- The associated type declaration
@@ -814,9 +817,14 @@ instance Outputable IfaceClassOp where
    ppr = pprIfaceClassOp showAll
 
 pprIfaceClassOp :: ShowSub -> IfaceClassOp -> SDoc
-pprIfaceClassOp ss (IfaceClassOp n dm ty) = hang opHdr 2 (pprIfaceSigmaType ty)
-  where opHdr = pprPrefixIfDeclBndr ss n
-                <+> ppShowIface ss (ppr dm) <+> dcolon
+pprIfaceClassOp ss (IfaceClassOp n ty dm)
+  = pp_sig n ty $$ generic_dm
+  where
+   generic_dm | Just (GenericDM dm_ty) <- dm
+              =  ptext (sLit "default") <+> pp_sig n dm_ty
+              | otherwise
+              = empty
+   pp_sig n ty = pprPrefixIfDeclBndr ss n <+> dcolon <+> pprIfaceSigmaType ty
 
 instance Outputable IfaceAT where
    ppr = pprIfaceAT showAll
@@ -1182,7 +1190,11 @@ freeNamesIfAT (IfaceAT decl mb_def)
       Just rhs -> freeNamesIfType rhs
 
 freeNamesIfClsSig :: IfaceClassOp -> NameSet
-freeNamesIfClsSig (IfaceClassOp _n _dm ty) = freeNamesIfType ty
+freeNamesIfClsSig (IfaceClassOp _n ty dm) = freeNamesIfType ty &&& freeNamesDM dm
+
+freeNamesDM :: Maybe (DefMethSpec IfaceType) -> NameSet
+freeNamesDM (Just (GenericDM ty)) = freeNamesIfType ty
+freeNamesDM _                     = emptyNameSet
 
 freeNamesIfConDecls :: IfaceConDecls -> NameSet
 freeNamesIfConDecls (IfDataTyCon c _ _) = fnList freeNamesIfConDecl c
@@ -1538,16 +1550,16 @@ instance Binary IfaceFamTyConFlav where
                                   (ppr (fromIntegral h :: Int)) }
 
 instance Binary IfaceClassOp where
-    put_ bh (IfaceClassOp n def ty) = do
+    put_ bh (IfaceClassOp n ty def) = do
         put_ bh (occNameFS n)
-        put_ bh def
         put_ bh ty
+        put_ bh def
     get bh = do
         n   <- get bh
-        def <- get bh
         ty  <- get bh
+        def <- get bh
         occ <- return $! mkVarOccFS n
-        return (IfaceClassOp occ def ty)
+        return (IfaceClassOp occ ty def)
 
 instance Binary IfaceAT where
     put_ bh (IfaceAT dec defs) = do
diff --git a/compiler/iface/IfaceType.hs b/compiler/iface/IfaceType.hs
index 8be97dfe40..7bf949e24f 100644
--- a/compiler/iface/IfaceType.hs
+++ b/compiler/iface/IfaceType.hs
@@ -6,7 +6,9 @@
 This module defines interface types and binders
 -}
 
-{-# LANGUAGE CPP #-}
+{-# LANGUAGE CPP, FlexibleInstances #-}
+    -- FlexibleInstances for Binary (DefMethSpec IfaceType)
+
 module IfaceType (
         IfExtName, IfLclName,
 
@@ -1007,6 +1009,15 @@ instance Binary IfaceCoercion where
                    return $ IfaceAxiomRuleCo a b c
            _ -> panic ("get IfaceCoercion " ++ show tag)
 
+instance Binary (DefMethSpec IfaceType) where
+    put_ bh VanillaDM     = putByte bh 0
+    put_ bh (GenericDM t) = putByte bh 1 >> put_ bh t
+    get bh = do
+            h <- getByte bh
+            case h of
+              0 -> return VanillaDM
+              _ -> do { t <- get bh; return (GenericDM t) }
+
 {-
 ************************************************************************
 *                                                                      *
diff --git a/compiler/iface/MkIface.hs b/compiler/iface/MkIface.hs
index 98b8830e01..d955fa5fd9 100644
--- a/compiler/iface/MkIface.hs
+++ b/compiler/iface/MkIface.hs
@@ -1529,8 +1529,9 @@ classToIfaceDecl env clas
 
     toIfaceClassOp (sel_id, def_meth)
         = ASSERT(sel_tyvars == clas_tyvars)
-          IfaceClassOp (getOccName sel_id) (toDmSpec def_meth)
+          IfaceClassOp (getOccName sel_id)
                        (tidyToIfaceType env1 op_ty)
+                       (fmap toDmSpec def_meth)
         where
                 -- Be careful when splitting the type, because of things
                 -- like         class Foo a where
@@ -1540,9 +1541,9 @@ classToIfaceDecl env clas
           (sel_tyvars, rho_ty) = splitForAllTys (idType sel_id)
           op_ty                = funResultTy rho_ty
 
-    toDmSpec NoDefMeth      = NoDM
-    toDmSpec (GenDefMeth _) = GenericDM
-    toDmSpec (DefMeth _)    = VanillaDM
+    toDmSpec :: (Name, DefMethSpec Type) -> DefMethSpec IfaceType
+    toDmSpec (_, VanillaDM)       = VanillaDM
+    toDmSpec (_, GenericDM dm_ty) = GenericDM (tidyToIfaceType env1 dm_ty)
 
     toIfaceFD (tvs1, tvs2) = (map (getFS . tidyTyVar env1) tvs1,
                               map (getFS . tidyTyVar env1) tvs2)
diff --git a/compiler/iface/TcIface.hs b/compiler/iface/TcIface.hs
index 45b583cd91..da94136218 100644
--- a/compiler/iface/TcIface.hs
+++ b/compiler/iface/TcIface.hs
@@ -50,7 +50,7 @@ import PrelNames
 import TysWiredIn
 import TysPrim          ( superKindTyConName )
 import BasicTypes       ( strongLoopBreaker, Arity, TupleSort(..)
-                        , Boxity(..), pprRuleName )
+                        , Boxity(..), DefMethSpec(..), pprRuleName )
 import Literal
 import qualified Var
 import VarEnv
@@ -419,13 +419,23 @@ tc_iface_decl _parent ignore_prags
         -- Here the associated type T is knot-tied with the class, and
         -- so we must not pull on T too eagerly.  See Trac #5970
 
-   tc_sig (IfaceClassOp occ dm rdr_ty)
+   tc_sig :: IfaceClassOp -> IfL TcMethInfo
+   tc_sig (IfaceClassOp occ rdr_ty dm)
      = do { op_name <- lookupIfaceTop occ
-          ; op_ty   <- forkM (mk_op_doc op_name rdr_ty) (tcIfaceType rdr_ty)
+          ; ~(op_ty, dm') <- forkM (mk_op_doc op_name rdr_ty) $
+                             do { ty <- tcIfaceType rdr_ty
+                                ; dm' <- tc_dm dm
+                                ; return (ty, dm') }
                 -- Must be done lazily for just the same reason as the
                 -- type of a data con; to avoid sucking in types that
                 -- it mentions unless it's necessary to do so
-          ; return (op_name, dm, op_ty) }
+          ; return (op_name, op_ty, dm') }
+
+   tc_dm :: Maybe (DefMethSpec IfaceType) -> IfL (Maybe (DefMethSpec Type))
+   tc_dm Nothing               = return Nothing
+   tc_dm (Just VanillaDM)      = return (Just VanillaDM)
+   tc_dm (Just (GenericDM ty)) = do { ty' <- tcIfaceType ty
+                                    ; return (Just (GenericDM ty')) }
 
    tc_at cls (IfaceAT tc_decl if_def)
      = do ATyCon tc <- tc_iface_decl (Just cls) ignore_prags tc_decl
diff --git a/compiler/main/HscTypes.hs b/compiler/main/HscTypes.hs
index daf7eb2846..290f27b71c 100644
--- a/compiler/main/HscTypes.hs
+++ b/compiler/main/HscTypes.hs
@@ -1721,7 +1721,8 @@ implicitTyConThings tc
   = class_stuff ++
       -- fields (names of selectors)
 
-      -- (possibly) implicit newtype coercion
+      -- (possibly) implicit newtype axioms
+      -- or type family axioms
     implicitCoTyCon tc ++
 
       -- for each data constructor in order,
diff --git a/compiler/typecheck/TcClassDcl.hs b/compiler/typecheck/TcClassDcl.hs
index 846a19b05f..8be4cf6e13 100644
--- a/compiler/typecheck/TcClassDcl.hs
+++ b/compiler/typecheck/TcClassDcl.hs
@@ -97,16 +97,16 @@ Death to "ExpandingDicts".
 ************************************************************************
 -}
 
-tcClassSigs :: Name                  -- Name of the class
+tcClassSigs :: Name                -- Name of the class
             -> [LSig Name]
             -> LHsBinds Name
-            -> TcM ([TcMethInfo],    -- Exactly one for each method
-                    NameEnv Type)    -- Types of the generic-default methods
+            -> TcM [TcMethInfo]    -- Exactly one for each method
 tcClassSigs clas sigs def_methods
   = do { traceTc "tcClassSigs 1" (ppr clas)
 
        ; gen_dm_prs <- concat <$> mapM (addLocM tc_gen_sig) gen_sigs
-       ; let gen_dm_env = mkNameEnv gen_dm_prs
+       ; let gen_dm_env :: NameEnv Type
+             gen_dm_env = mkNameEnv gen_dm_prs
 
        ; op_info <- concat <$> mapM (addLocM (tc_sig gen_dm_env)) vanilla_sigs
 
@@ -120,22 +120,22 @@ tcClassSigs clas sigs def_methods
                    -- Generic signature without value binding
 
        ; traceTc "tcClassSigs 2" (ppr clas)
-       ; return (op_info, gen_dm_env) }
+       ; return op_info }
   where
     vanilla_sigs = [L loc (nm,ty) | L loc (TypeSig    nm ty _) <- sigs]
     gen_sigs     = [L loc (nm,ty) | L loc (GenericSig nm ty) <- sigs]
     dm_bind_names :: [Name]     -- These ones have a value binding in the class decl
     dm_bind_names = [op | L _ (FunBind {fun_id = L _ op}) <- bagToList def_methods]
 
-    tc_sig genop_env (op_names, op_hs_ty)
+    tc_sig gen_dm_env (op_names, op_hs_ty)
       = do { traceTc "ClsSig 1" (ppr op_names)
            ; op_ty <- tcClassSigType op_hs_ty   -- Class tyvars already in scope
            ; traceTc "ClsSig 2" (ppr op_names)
-           ; return [ (op_name, f op_name, op_ty) | L _ op_name <- op_names ] }
+           ; return [ (op_name, op_ty, f op_name) | L _ op_name <- op_names ] }
            where
-             f nm | nm `elemNameEnv` genop_env = GenericDM
-                  | nm `elem` dm_bind_names    = VanillaDM
-                  | otherwise                  = NoDM
+             f nm | Just ty <- lookupNameEnv gen_dm_env nm = Just (GenericDM ty)
+                  | nm `elem` dm_bind_names                = Just VanillaDM
+                  | otherwise                              = Nothing
 
     tc_gen_sig (op_names, gen_hs_ty)
       = do { gen_op_ty <- tcClassSigType gen_hs_ty
@@ -173,19 +173,8 @@ tcClassDecl2 (L loc (ClassDecl {tcdLName = class_name, tcdSigs = sigs,
               pred        = mkClassPred clas (mkTyVarTys clas_tyvars)
         ; this_dict <- newEvVar pred
 
-        ; let tc_item (sel_id, dm_info)
-                = case dm_info of
-                    DefMeth dm_name    -> tc_dm sel_id dm_name False
-                    GenDefMeth dm_name -> tc_dm sel_id dm_name True
-                       -- For GenDefMeth, warn if the user specifies a signature
-                       -- with redundant constraints; but not for DefMeth, where
-                       -- the default method may well be 'error' or something
-                    NoDefMeth          -> do { mapM_ (addLocM (badDmPrag sel_id))
-                                                     (lookupPragEnv prag_fn (idName sel_id))
-                                             ; return emptyBag }
-              tc_dm = tcDefMeth clas clas_tyvars this_dict
-                                default_binds sig_fn prag_fn
-
+        ; let tc_item = tcDefMeth clas clas_tyvars this_dict
+                                  default_binds sig_fn prag_fn
         ; dm_binds <- tcExtendTyVarEnv clas_tyvars $
                       mapM tc_item op_items
 
@@ -194,19 +183,25 @@ tcClassDecl2 (L loc (ClassDecl {tcdLName = class_name, tcdSigs = sigs,
 tcClassDecl2 d = pprPanic "tcClassDecl2" (ppr d)
 
 tcDefMeth :: Class -> [TyVar] -> EvVar -> LHsBinds Name
-          -> HsSigFun -> TcPragEnv -> Id -> Name -> Bool
+          -> HsSigFun -> TcPragEnv -> ClassOpItem
           -> TcM (LHsBinds TcId)
--- Generate code for polymorphic default methods only (hence DefMeth)
--- (Generic default methods have turned into instance decls by now.)
+-- Generate code for default methods
 -- This is incompatible with Hugs, which expects a polymorphic
 -- default method for every class op, regardless of whether or not
 -- the programmer supplied an explicit default decl for the class.
 -- (If necessary we can fix that, but we don't have a convenient Id to hand.)
-tcDefMeth clas tyvars this_dict binds_in
-          hs_sig_fn prag_fn sel_id dm_name warn_redundant
+
+tcDefMeth _ _ _ _ _ prag_fn (sel_id, Nothing)
+  = do { -- No default method
+         mapM_ (addLocM (badDmPrag sel_id))
+               (lookupPragEnv prag_fn (idName sel_id))
+       ; return emptyBag }
+
+tcDefMeth clas tyvars this_dict binds_in hs_sig_fn prag_fn
+          (sel_id, Just (dm_name, dm_spec))
   | Just (L bind_loc dm_bind, bndr_loc) <- findMethodBind sel_name binds_in
-    -- First look up the default method -- it should be there!
-  = do { global_dm_id  <- tcLookupId dm_name
+  = do { -- First look up the default method -- It should be there!
+         global_dm_id  <- tcLookupId dm_name
        ; global_dm_id  <- addInlinePrags global_dm_id prags
        ; local_dm_name <- setSrcSpan bndr_loc (newLocalName sel_name)
             -- Base the local_dm_name on the selector name, because
@@ -235,6 +230,13 @@ tcDefMeth clas tyvars this_dict binds_in
                              -- Substitute the local_meth_name for the binder
                              -- NB: the binding is always a FunBind
 
+             warn_redundant = case dm_spec of
+                                GenericDM {} -> True
+                                VanillaDM    -> False
+                -- For GenericDM, warn if the user specifies a signature
+                -- with redundant constraints; but not for VanillaDM, where
+                -- the default method may well be 'error' or something
+
              ctxt = FunSigCtxt sel_name warn_redundant
 
        ; local_dm_sig <- instTcTySig ctxt hs_ty local_dm_ty Nothing [] local_dm_name
@@ -283,7 +285,7 @@ tcClassMinimalDef _clas sigs op_info
     -- implementation whose names don't start with '_'
     defMindef :: ClassMinimalDef
     defMindef = mkAnd [ noLoc (mkVar name)
-                      | (name, NoDM, _) <- op_info
+                      | (name, _, Nothing) <- op_info
                       , not (startsWithUnderscore (getOccName name)) ]
 
 instantiateMethod :: Class -> Id -> [TcType] -> TcType
diff --git a/compiler/typecheck/TcDeriv.hs b/compiler/typecheck/TcDeriv.hs
index 8631bd3342..707195ea6b 100644
--- a/compiler/typecheck/TcDeriv.hs
+++ b/compiler/typecheck/TcDeriv.hs
@@ -410,9 +410,9 @@ tcDeriving deriv_infos deriv_decls
              liftIO (dumpIfSet_dyn dflags Opt_D_dump_deriv "Derived instances"
                         (ddump_deriving inst_info rn_binds newTyCons famInsts))
 
-        ; let all_tycons = map ATyCon (bagToList newTyCons)
-        ; gbl_env <- tcExtendGlobalEnv all_tycons $
-                     tcExtendGlobalEnvImplicit (concatMap implicitTyThings all_tycons) $
+        ; let all_tycons = bagToList newTyCons
+        ; gbl_env <- tcExtendTyConEnv all_tycons $
+                     tcExtendGlobalEnvImplicit (concatMap implicitTyConThings all_tycons) $
                      tcExtendLocalFamInstEnv (bagToList famInsts) $
                      tcExtendLocalInstEnv (map iSpec (bagToList inst_info)) getGblEnv
         ; let all_dus = rn_dus `plusDU` usesOnly (mkFVs $ catMaybes maybe_fvs)
diff --git a/compiler/typecheck/TcEnv.hs b/compiler/typecheck/TcEnv.hs
index 3bb2703104..4bf83b5f31 100644
--- a/compiler/typecheck/TcEnv.hs
+++ b/compiler/typecheck/TcEnv.hs
@@ -12,7 +12,8 @@ module TcEnv(
         InstBindings(..),
 
         -- Global environment
-        tcExtendGlobalEnv, tcExtendGlobalEnvImplicit, setGlobalTypeEnv,
+        tcExtendGlobalEnv, tcExtendTyConEnv,
+        tcExtendGlobalEnvImplicit, setGlobalTypeEnv,
         tcExtendGlobalValEnv,
         tcLookupLocatedGlobal, tcLookupGlobal,
         tcLookupTyCon, tcLookupClass,
@@ -260,10 +261,8 @@ setGlobalTypeEnv tcg_env new_type_env
 
 
 tcExtendGlobalEnvImplicit :: [TyThing] -> TcM r -> TcM r
-  -- Extend the global environment with some TyThings that can be obtained
-  -- via implicitTyThings from other entities in the environment.  Examples
-  -- are dfuns, famInstTyCons, data cons, etc.
-  -- These TyThings are not added to tcg_tcs.
+  -- Just extend the global environment with some TyThings
+  -- Do not extend tcg_tcs etc
 tcExtendGlobalEnvImplicit things thing_inside
    = do { tcg_env <- getGblEnv
         ; let ge'  = extendTypeEnvList (tcg_type_env tcg_env) things
@@ -281,6 +280,16 @@ tcExtendGlobalEnv things thing_inside
             tcExtendGlobalEnvImplicit things thing_inside
        }
 
+tcExtendTyConEnv :: [TyCon] -> TcM r -> TcM r
+  -- Given a mixture of Ids, TyCons, Classes, all defined in the
+  -- module being compiled, extend the global environment
+tcExtendTyConEnv tycons thing_inside
+  = do { env <- getGblEnv
+       ; let env' = env { tcg_tcs = tycons ++ tcg_tcs env }
+       ; setGblEnv env' $
+         tcExtendGlobalEnvImplicit (map ATyCon tycons) thing_inside
+       }
+
 tcExtendGlobalValEnv :: [Id] -> TcM a -> TcM a
   -- Same deal as tcExtendGlobalEnv, but for Ids
 tcExtendGlobalValEnv ids thing_inside
diff --git a/compiler/typecheck/TcInstDcls.hs b/compiler/typecheck/TcInstDcls.hs
index f810027fab..dc281d1df2 100644
--- a/compiler/typecheck/TcInstDcls.hs
+++ b/compiler/typecheck/TcInstDcls.hs
@@ -36,14 +36,13 @@ import MkCore     ( nO_METHOD_BINDING_ERROR_ID )
 import Type
 import TcEvidence
 import TyCon
-import CoAxiom
+import CoAxiom( toBranchedAxiom )
 import DataCon
 import Class
 import Var
 import VarEnv
 import VarSet
 import PrelNames  ( typeableClassName, genericClassNames )
---                   , knownNatClassName, knownSymbolClassName )
 import Bag
 import BasicTypes
 import DynFlags
@@ -462,14 +461,17 @@ addFamInsts :: [FamInst] -> TcM a -> TcM a
 --        (b) the type envt with stuff from data type decls
 addFamInsts fam_insts thing_inside
   = tcExtendLocalFamInstEnv fam_insts $
-    tcExtendGlobalEnv things  $
+    tcExtendGlobalEnv axioms $
+    tcExtendTyConEnv data_rep_tycons  $
     do { traceTc "addFamInsts" (pprFamInsts fam_insts)
-       ; tcg_env <- tcAddImplicits things
+       ; tcg_env <- tcAddImplicits data_rep_tycons
+                    -- Does not add its axiom; that comes from
+                    -- adding the 'axioms' above
        ; setGblEnv tcg_env thing_inside }
   where
-    axioms = map (toBranchedAxiom . famInstAxiom) fam_insts
-    tycons = famInstsRepTyCons fam_insts
-    things = map ATyCon tycons ++ map ACoAxiom axioms
+    axioms = map (ACoAxiom . toBranchedAxiom . famInstAxiom) fam_insts
+    data_rep_tycons = famInstsRepTyCons fam_insts
+      -- The representation tycons for 'data instances' declarations
 
 {-
 Note [Deriving inside TH brackets]
@@ -1228,7 +1230,7 @@ tcMethods :: DFunId -> Class
           -> [TcType]
           -> TcEvBinds
           -> ([Located TcSpecPrag], TcPragEnv)
-          -> [(Id, DefMeth)]
+          -> [ClassOpItem]
           -> InstBindings Name
           -> TcM ([Id], LHsBinds Id, Bag Implication)
         -- The returned inst_meth_ids all have types starting
@@ -1255,7 +1257,7 @@ tcMethods dfun_id clas tyvars dfun_ev_vars inst_tys
     inst_loc  = getSrcSpan dfun_id
 
     ----------------------
-    tc_item :: (Id, DefMeth) -> TcM (Id, LHsBind Id, Maybe Implication)
+    tc_item :: ClassOpItem -> TcM (Id, LHsBind Id, Maybe Implication)
     tc_item (sel_id, dm_info)
       | Just (user_bind, bndr_loc) <- findMethodBind (idName sel_id) binds
       = tcMethodBody clas tyvars dfun_ev_vars inst_tys
@@ -1266,15 +1268,15 @@ tcMethods dfun_id clas tyvars dfun_ev_vars inst_tys
            ; tc_default sel_id dm_info }
 
     ----------------------
-    tc_default :: Id -> DefMeth -> TcM (TcId, LHsBind Id, Maybe Implication)
+    tc_default :: Id -> DefMethInfo -> TcM (TcId, LHsBind Id, Maybe Implication)
 
-    tc_default sel_id (GenDefMeth dm_name)
+    tc_default sel_id (Just (dm_name, GenericDM {}))
       = do { meth_bind <- mkGenericDefMethBind clas inst_tys sel_id dm_name
            ; tcMethodBody clas tyvars dfun_ev_vars inst_tys
                                   dfun_ev_binds is_derived hs_sig_fn prags
                                   sel_id meth_bind inst_loc }
 
-    tc_default sel_id NoDefMeth     -- No default method at all
+    tc_default sel_id Nothing     -- No default method at all
       = do { traceTc "tc_def: warn" (ppr sel_id)
            ; (meth_id, _, _) <- mkMethIds hs_sig_fn clas tyvars dfun_ev_vars
                                           inst_tys sel_id
@@ -1292,7 +1294,7 @@ tcMethods dfun_id clas tyvars dfun_ev_vars inst_tys
                               (hcat [ppr inst_loc, vbar, ppr sel_id ])
         lam_wrapper  = mkWpTyLams tyvars <.> mkWpLams dfun_ev_vars
 
-    tc_default sel_id (DefMeth dm_name) -- A polymorphic default method
+    tc_default sel_id (Just (dm_name, VanillaDM)) -- A polymorphic default method
       = do {     -- Build the typechecked version directly,
                  -- without calling typecheck_method;
                  -- see Note [Default methods in instances]
diff --git a/compiler/typecheck/TcRnDriver.hs b/compiler/typecheck/TcRnDriver.hs
index e9c351515c..fb27c26cb9 100644
--- a/compiler/typecheck/TcRnDriver.hs
+++ b/compiler/typecheck/TcRnDriver.hs
@@ -931,7 +931,7 @@ checkBootTyCon tc1 tc2
            check (eqTypeX env op_ty1 op_ty2)
                  (text "The types of" <+> pname1 <+>
                   text "are different") `andThenCheck`
-           check (def_meth1 == def_meth2)
+           check (eqMaybeBy eqDM def_meth1 def_meth2)
                  (text "The default methods associated with" <+> pname1 <+>
                   text "are different")
          where
@@ -949,6 +949,10 @@ checkBootTyCon tc1 tc2
            check (eqATDef def_ats1 def_ats2)
                  (text "The associated type defaults differ")
 
+       eqDM (_, VanillaDM)    (_, VanillaDM)    = True
+       eqDM (_, GenericDM t1) (_, GenericDM t2) = eqTypeX env t1 t2
+       eqDM _ _ = False
+
        -- Ignore the location of the defaults
        eqATDef Nothing             Nothing             = True
        eqATDef (Just (ty1, _loc1)) (Just (ty2, _loc2)) = eqTypeX env ty1 ty2
diff --git a/compiler/typecheck/TcSplice.hs b/compiler/typecheck/TcSplice.hs
index e8ad9cc4b7..7a13d8b932 100644
--- a/compiler/typecheck/TcSplice.hs
+++ b/compiler/typecheck/TcSplice.hs
@@ -1214,10 +1214,9 @@ reifyClass cls
       = do { ty <- reifyType (idType op)
            ; let nm' = reifyName op
            ; case def_meth of
-                GenDefMeth gdm_nm ->
-                  do { gdm_id <- tcLookupId gdm_nm
-                     ; gdm_ty <- reifyType (idType gdm_id)
-                     ; return [TH.SigD nm' ty, TH.DefaultSigD nm' gdm_ty] }
+                Just (_, GenericDM gdm_ty) ->
+                  do { gdm_ty' <- reifyType gdm_ty
+                     ; return [TH.SigD nm' ty, TH.DefaultSigD nm' gdm_ty'] }
                 _ -> return [TH.SigD nm' ty] }
 
     reifyAT :: ClassATItem -> TcM [TH.Dec]
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index c773588429..05a79e2b51 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -44,7 +44,7 @@ import CoAxiom
 import TyCon
 import DataCon
 import Id
-import IdInfo
+-- import IdInfo
 import Var
 import VarEnv
 import VarSet
@@ -150,40 +150,46 @@ tcTyClGroup tyclds
              tcExtendKindEnv names_w_poly_kinds              $
 
                  -- Kind and type check declarations for this group
-             concatMapM (tcTyClDecl rec_flags) decls }
+             mapM (tcTyClDecl rec_flags) decls }
 
            -- Step 3: Perform the validity check
            -- We can do this now because we are done with the recursive knot
            -- Do it before Step 4 (adding implicit things) because the latter
            -- expects well-formed TyCons
-       ; tcExtendGlobalEnv tyclss $ do
-       { traceTc "Starting validity check" (ppr tyclss)
-       ; mapM_ (recoverM (return ()) . checkValidTyCl) tyclss
-           -- We recover, which allows us to report multiple validity errors
+       ; traceTc "Starting validity check" (ppr tyclss)
+       ; tyclss <- mapM checkValidTyCl tyclss
+       ; traceTc "Done validity check" (ppr tyclss)
        ; mapM_ (recoverM (return ()) . checkValidRoleAnnots role_annots) tyclss
            -- See Note [Check role annotations in a second pass]
 
            -- Step 4: Add the implicit things;
            -- we want them in the environment because
            -- they may be mentioned in interface files
-       ; tcAddImplicits tyclss } }
+       ; tcExtendTyConEnv tyclss $
+         tcAddImplicits tyclss }
 
 zipRecTyClss :: [(Name, Kind)]
-             -> [TyThing]           -- Knot-tied
+             -> [TyCon]           -- Knot-tied
              -> [(Name,TyThing)]
 -- Build a name-TyThing mapping for the things bound by decls
 -- being careful not to look at the [TyThing]
 -- The TyThings in the result list must have a visible ATyCon,
 -- because typechecking types (in, say, tcTyClDecl) looks at this outer constructor
-zipRecTyClss kind_pairs rec_things
+zipRecTyClss kind_pairs rec_tycons
   = [ (name, ATyCon (get name)) | (name, _kind) <- kind_pairs ]
   where
-    rec_type_env :: TypeEnv
-    rec_type_env = mkTypeEnv rec_things
+    rec_tc_env :: NameEnv TyCon
+    rec_tc_env = foldr add_tc emptyNameEnv rec_tycons
 
-    get name = case lookupTypeEnv rec_type_env name of
-                 Just (ATyCon tc) -> tc
-                 other            -> pprPanic "zipRecTyClss" (ppr name <+> ppr other)
+    add_tc :: TyCon -> NameEnv TyCon -> NameEnv TyCon
+    add_tc tc env = foldr add_one_tc env (tc : tyConATs tc)
+
+    add_one_tc :: TyCon -> NameEnv TyCon -> NameEnv TyCon
+    add_one_tc tc env = extendNameEnv env (tyConName tc) tc
+
+    get name = case lookupNameEnv rec_tc_env name of
+                 Just tc -> tc
+                 other   -> pprPanic "zipRecTyClss" (ppr name <+> ppr other)
 
 {-
 ************************************************************************
@@ -578,10 +584,12 @@ e.g. the need to make the data constructor worker name for
      a constraint tuple match the wired-in one
 -}
 
-tcTyClDecl :: RecTyInfo -> LTyClDecl Name -> TcM [TyThing]
+tcTyClDecl :: RecTyInfo -> LTyClDecl Name -> TcM TyCon
 tcTyClDecl rec_info (L loc decl)
   | Just thing <- wiredInNameTyThing_maybe (tcdName decl)
-  = return [thing]  -- See Note [Declarations for wired-in things]
+  = case thing of -- See Note [Declarations for wired-in things]
+      ATyCon tc -> return tc
+      _ -> pprPanic "tcTyClDecl" (ppr thing)
 
   | otherwise
   = setSrcSpan loc $ tcAddDeclCtxt decl $
@@ -589,7 +597,7 @@ tcTyClDecl rec_info (L loc decl)
        ; tcTyClDecl1 Nothing rec_info decl }
 
   -- "type family" declarations
-tcTyClDecl1 :: Maybe Class -> RecTyInfo -> TyClDecl Name -> TcM [TyThing]
+tcTyClDecl1 :: Maybe Class -> RecTyInfo -> TyClDecl Name -> TcM TyCon
 tcTyClDecl1 parent _rec_info (FamDecl { tcdFam = fd })
   = tcFamDecl1 parent fd
 
@@ -613,7 +621,7 @@ tcTyClDecl1 _parent rec_info
             , tcdFDs = fundeps, tcdSigs = sigs
             , tcdATs = ats, tcdATDefs = at_defs })
   = ASSERT( isNothing _parent )
-    do { (clas, tvs', gen_dm_env) <- fixM $ \ ~(clas,_,_) ->
+    do { clas <- fixM $ \ clas ->
             tcTyClTyVars class_name tvs $ \ tvs' kind ->
             do { MASSERT( isConstraintKind kind )
                  -- This little knot is just so we can get
@@ -628,28 +636,16 @@ tcTyClDecl1 _parent rec_info
                ; ctxt' <- zonkTcTypeToTypes emptyZonkEnv ctxt'
                        -- Squeeze out any kind unification variables
                ; fds'  <- mapM (addLocM tc_fundep) fundeps
-               ; (sig_stuff, gen_dm_env) <- tcClassSigs class_name sigs meths
+               ; sig_stuff <- tcClassSigs class_name sigs meths
                ; at_stuff <- tcClassATs class_name clas ats at_defs
                ; mindef <- tcClassMinimalDef class_name sigs sig_stuff
                ; clas <- buildClass
                             class_name tvs' roles ctxt' fds' at_stuff
                             sig_stuff mindef tc_isrec
                ; traceTc "tcClassDecl" (ppr fundeps $$ ppr tvs' $$ ppr fds')
-               ; return (clas, tvs', gen_dm_env) }
-
-       ; let { gen_dm_ids = [ AnId (mkExportedLocalId DefMethId gen_dm_name gen_dm_ty)
-                            | (sel_id, GenDefMeth gen_dm_name) <- classOpItems clas
-                            , let gen_dm_tau = expectJust "tcTyClDecl1" $
-                                               lookupNameEnv gen_dm_env (idName sel_id)
-                            , let gen_dm_ty = mkSigmaTy tvs'
-                                                      [mkClassPred clas (mkTyVarTys tvs')]
-                                                      gen_dm_tau
-                            ]
-             ; class_ats = map ATyCon (classATs clas) }
-
-       ; return (ATyCon (classTyCon clas) : gen_dm_ids ++ class_ats ) }
-         -- NB: Order is important due to the call to `mkGlobalThings' when
-         --     tying the the type and class declaration type checking knot.
+               ; return clas }
+
+         ; return (classTyCon clas) }
   where
     tc_fundep (tvs1, tvs2) = do { tvs1' <- mapM tcFdTyVar tvs1
                                 ; tvs2' <- mapM tcFdTyVar tvs2
@@ -668,7 +664,7 @@ tcFdTyVar (L _ name)
            Just tv' -> return tv'
            Nothing  -> pprPanic "tcFdTyVar" (ppr name $$ ppr tv $$ ppr ty) }
 
-tcFamDecl1 :: Maybe Class -> FamilyDecl Name -> TcM [TyThing]
+tcFamDecl1 :: Maybe Class -> FamilyDecl Name -> TcM TyCon
 tcFamDecl1 parent
             (FamilyDecl { fdInfo = OpenTypeFamily, fdLName = L _ tc_name
                         , fdTyVars = tvs, fdResultSig = L _ sig
@@ -679,7 +675,7 @@ tcFamDecl1 parent
   ; inj' <- tcInjectivity tvs' inj
   ; let tycon = buildFamilyTyCon tc_name tvs' (resultVariableName sig)
                                  OpenSynFamilyTyCon kind parent inj'
-  ; return [ATyCon tycon] }
+  ; return tycon }
 
 tcFamDecl1 parent
             (FamilyDecl { fdInfo = ClosedTypeFamily mb_eqns
@@ -699,9 +695,9 @@ tcFamDecl1 parent
          -- If Nothing, this is an abstract family in a hs-boot file;
          -- but eqns might be empty in the Just case as well
        ; case mb_eqns of
-           Nothing   -> return
-               [ ATyCon $ buildFamilyTyCon tc_name tvs' (resultVariableName sig)
-                                 AbstractClosedSynFamilyTyCon kind parent inj' ]
+           Nothing   -> return $
+                        buildFamilyTyCon tc_name tvs' (resultVariableName sig)
+                                 AbstractClosedSynFamilyTyCon kind parent inj'
            Just eqns -> do {
 
          -- Process the equations, creating CoAxBranches
@@ -732,7 +728,7 @@ tcFamDecl1 parent
              fam_tc = buildFamilyTyCon tc_name tvs' (resultVariableName sig)
                       (ClosedSynFamilyTyCon mb_co_ax) kind parent inj'
 
-       ; return $ ATyCon fam_tc : maybeToList (fmap ACoAxiom mb_co_ax) } }
+       ; return fam_tc } }
 
 -- We check for instance validity later, when doing validity checking for
 -- the tycon. Exception: checking equations overlap done by dropDominatedAxioms
@@ -753,7 +749,7 @@ tcFamDecl1 parent
                                  liftedTypeKind -- RHS kind
                                  parent
                                  NotInjective
-  ; return [ATyCon tycon] }
+  ; return tycon }
 
 -- | Maybe return a list of Bools that say whether a type family was declared
 -- injective in the corresponding type arguments. Length of the list is equal to
@@ -795,7 +791,7 @@ tcInjectivity tvs (Just (L loc (InjectivityAnn _ lInjNames)))
 tcTySynRhs :: RecTyInfo
            -> Name
            -> [TyVar] -> Kind
-           -> LHsType Name -> TcM [TyThing]
+           -> LHsType Name -> TcM TyCon
 tcTySynRhs rec_info tc_name tvs kind hs_ty
   = do { env <- getLclEnv
        ; traceTc "tc-syn" (ppr tc_name $$ ppr (tcl_env env))
@@ -803,11 +799,11 @@ tcTySynRhs rec_info tc_name tvs kind hs_ty
        ; rhs_ty <- zonkTcTypeToType emptyZonkEnv rhs_ty
        ; let roles = rti_roles rec_info tc_name
              tycon = buildSynonymTyCon tc_name tvs roles rhs_ty kind
-       ; return [ATyCon tycon] }
+       ; return tycon }
 
 tcDataDefn :: RecTyInfo -> Name
            -> [TyVar] -> Kind
-           -> HsDataDefn Name -> TcM [TyThing]
+           -> HsDataDefn Name -> TcM TyCon
   -- NB: not used for newtype/data instances (whether associated or not)
 tcDataDefn rec_info          -- Knot-tied; don't look at this eagerly
            tc_name tvs kind
@@ -845,7 +841,7 @@ tcDataDefn rec_info          -- Knot-tied; don't look at this eagerly
                                      is_prom
                                      gadt_syntax
                                      (VanillaAlgTyCon tc_rep_nm)) }
-       ; return [ATyCon tycon] }
+       ; return tycon }
   where
     mk_tc_rhs is_boot tycon data_cons
       | null data_cons, is_boot         -- In a hs-boot file, empty cons means
@@ -904,7 +900,7 @@ tcClassATs class_name cls ats at_defs
                                           (at_def_tycon at_def) [at_def])
                         emptyNameEnv at_defs
 
-    tc_at at = do { [ATyCon fam_tc] <- addLocM (tcFamDecl1 (Just cls)) at
+    tc_at at = do { fam_tc <- addLocM (tcFamDecl1 (Just cls)) at
                   ; let at_defs = lookupNameEnv at_defs_map (at_fam_name at)
                                   `orElse` []
                   ; atd <- tcDefaultAssocDecl fam_tc at_defs
@@ -1524,17 +1520,25 @@ tied, so we can look at things freely.
 checkClassCycleErrs :: Class -> TcM ()
 checkClassCycleErrs cls = mapM_ recClsErr (calcClassCycles cls)
 
-checkValidTyCl :: TyThing -> TcM ()
-checkValidTyCl thing
-  = setSrcSpan (getSrcSpan thing) $
-    addTyThingCtxt thing $
-    case thing of
-      ATyCon tc -> checkValidTyCon tc
-      AnId _    -> return ()  -- Generic default methods are checked
-                              -- with their parent class
-      ACoAxiom _ -> return () -- Axioms checked with their parent
-                              -- closed family tycon
-      _         -> pprTrace "checkValidTyCl" (ppr thing) $ return ()
+checkValidTyCl :: TyCon -> TcM TyCon
+checkValidTyCl tc
+  = setSrcSpan (getSrcSpan tc) $
+    addTyConCtxt tc $
+    recoverM (do { traceTc "Aborted validity for tycon" (ppr tc)
+                 ; return (makeTyConAbstract tc) })
+             (do { traceTc "Starting validity for tycon" (ppr tc)
+                 ; checkValidTyCon tc
+                 ; traceTc "Done validity for tycon" (ppr tc)
+                 ; return tc })
+    -- We recover, which allows us to report multiple validity errors
+    -- In the failure case we return a TyCon of the right kind, but
+    -- with no interesting behaviour (makeTyConAbstract). Why?
+    -- Suppose we have
+    --    type T a = Fun
+    -- where Fun is a type family of arity 1.  The RHS is invalid, but we
+    -- want to go on checking validity of subsequent type declarations.
+    -- So we replace T with an abstract TyCon which will do no harm.
+    -- See indexed-types/should_fail/BadSock ande Trac #10896
 
 -------------------------
 -- For data types declared with record syntax, we require
@@ -1810,9 +1814,8 @@ checkValidClass cls
           mapM_ check_constraint (tail (theta1 ++ theta2))
 
         ; case dm of
-            GenDefMeth dm_name -> do { dm_id <- tcLookupId dm_name
-                                     ; checkValidType ctxt (idType dm_id) }
-            _                  -> return ()
+            Just (_, GenericDM ty) -> checkValidType ctxt ty
+            _                      -> return ()
         }
         where
           ctxt    = FunSigCtxt op_name True -- Report redundant class constraints
@@ -1873,50 +1876,47 @@ This fixes Trac #9415, #9739
 ************************************************************************
 -}
 
-checkValidRoleAnnots :: RoleAnnots -> TyThing -> TcM ()
-checkValidRoleAnnots role_annots thing
-  = case thing of
-    { ATyCon tc
-        | isTypeSynonymTyCon tc -> check_no_roles
-        | isFamilyTyCon tc      -> check_no_roles
-        | isAlgTyCon tc         -> check_roles
-        where
-          name                   = tyConName tc
-
-     -- Role annotations are given only on *type* variables, but a tycon stores
-     -- roles for all variables. So, we drop the kind roles (which are all
-     -- Nominal, anyway).
-          tyvars                 = tyConTyVars tc
-          roles                  = tyConRoles tc
-          (kind_vars, type_vars) = span isKindVar tyvars
-          type_roles             = dropList kind_vars roles
-          role_annot_decl_maybe  = lookupRoleAnnots role_annots name
-
-          check_roles
-            = whenIsJust role_annot_decl_maybe $
-                \decl@(L loc (RoleAnnotDecl _ the_role_annots)) ->
-                addRoleAnnotCtxt name $
-                setSrcSpan loc $ do
-                { role_annots_ok <- xoptM Opt_RoleAnnotations
-                ; checkTc role_annots_ok $ needXRoleAnnotations tc
-                ; checkTc (type_vars `equalLength` the_role_annots)
-                          (wrongNumberOfRoles type_vars decl)
-                ; _ <- zipWith3M checkRoleAnnot type_vars the_role_annots type_roles
-                -- Representational or phantom roles for class parameters
-                -- quickly lead to incoherence. So, we require
-                -- IncoherentInstances to have them. See #8773.
-                ; incoherent_roles_ok <- xoptM Opt_IncoherentInstances
-                ; checkTc (  incoherent_roles_ok
-                          || (not $ isClassTyCon tc)
-                          || (all (== Nominal) type_roles))
-                          incoherentRoles
-
-                ; lint <- goptM Opt_DoCoreLinting
-                ; when lint $ checkValidRoles tc }
-
-          check_no_roles
-            = whenIsJust role_annot_decl_maybe illegalRoleAnnotDecl
-    ; _ -> return () }
+checkValidRoleAnnots :: RoleAnnots -> TyCon -> TcM ()
+checkValidRoleAnnots role_annots tc
+  | isTypeSynonymTyCon tc = check_no_roles
+  | isFamilyTyCon tc      = check_no_roles
+  | isAlgTyCon tc         = check_roles
+  | otherwise             = return ()
+  where
+    -- Role annotations are given only on *type* variables, but a tycon stores
+    -- roles for all variables. So, we drop the kind roles (which are all
+    -- Nominal, anyway).
+    name                   = tyConName tc
+    tyvars                 = tyConTyVars tc
+    roles                  = tyConRoles tc
+    (kind_vars, type_vars) = span isKindVar tyvars
+    type_roles             = dropList kind_vars roles
+    role_annot_decl_maybe  = lookupRoleAnnots role_annots name
+
+    check_roles
+      = whenIsJust role_annot_decl_maybe $
+          \decl@(L loc (RoleAnnotDecl _ the_role_annots)) ->
+          addRoleAnnotCtxt name $
+          setSrcSpan loc $ do
+          { role_annots_ok <- xoptM Opt_RoleAnnotations
+          ; checkTc role_annots_ok $ needXRoleAnnotations tc
+          ; checkTc (type_vars `equalLength` the_role_annots)
+                    (wrongNumberOfRoles type_vars decl)
+          ; _ <- zipWith3M checkRoleAnnot type_vars the_role_annots type_roles
+          -- Representational or phantom roles for class parameters
+          -- quickly lead to incoherence. So, we require
+          -- IncoherentInstances to have them. See #8773.
+          ; incoherent_roles_ok <- xoptM Opt_IncoherentInstances
+          ; checkTc (  incoherent_roles_ok
+                    || (not $ isClassTyCon tc)
+                    || (all (== Nominal) type_roles))
+                    incoherentRoles
+
+          ; lint <- goptM Opt_DoCoreLinting
+          ; when lint $ checkValidRoles tc }
+
+    check_no_roles
+      = whenIsJust role_annot_decl_maybe illegalRoleAnnotDecl
 
 checkRoleAnnot :: TyVar -> Located (Maybe Role) -> Role -> TcM ()
 checkRoleAnnot _  (L _ Nothing)   _  = return ()
@@ -2199,16 +2199,12 @@ incoherentRoles = (text "Roles other than" <+> quotes (text "nominal") <+>
                    text "for class parameters can lead to incoherence.") $$
                   (text "Use IncoherentInstances to allow this; bad role found")
 
-addTyThingCtxt :: TyThing -> TcM a -> TcM a
-addTyThingCtxt thing
+addTyConCtxt :: TyCon -> TcM a -> TcM a
+addTyConCtxt tc
   = addErrCtxt ctxt
   where
-    name = getName thing
-    flav = case thing of
-             ATyCon tc -> text (tyConFlavour tc)
-             _ -> pprTrace "addTyThingCtxt strange" (ppr thing)
-                  Outputable.empty
-
+    name = getName tc
+    flav = text (tyConFlavour tc)
     ctxt = hsep [ ptext (sLit "In the"), flav
                 , ptext (sLit "declaration for"), quotes (ppr name) ]
 
diff --git a/compiler/typecheck/TcTyDecls.hs b/compiler/typecheck/TcTyDecls.hs
index 42387dea8b..88b0df959a 100644
--- a/compiler/typecheck/TcTyDecls.hs
+++ b/compiler/typecheck/TcTyDecls.hs
@@ -375,18 +375,17 @@ data RecTyInfo = RTI { rti_promotable :: Bool
                      , rti_is_rec     :: Name -> RecFlag }
 
 calcRecFlags :: SelfBootInfo -> Bool  -- hs-boot file?
-             -> RoleAnnots -> [TyThing] -> RecTyInfo
+             -> RoleAnnots -> [TyCon] -> RecTyInfo
 -- The 'boot_names' are the things declared in M.hi-boot, if M is the current module.
 -- Any type constructors in boot_names are automatically considered loop breakers
-calcRecFlags boot_details is_boot mrole_env tyclss
+-- Recursion of newtypes/data types can happen via
+-- the class TyCon, so all_tycons includes the class tycons
+calcRecFlags boot_details is_boot mrole_env all_tycons
   = RTI { rti_promotable = is_promotable
         , rti_roles      = roles
         , rti_is_rec     = is_rec }
   where
     rec_tycon_names = mkNameSet (map tyConName all_tycons)
-    all_tycons = mapMaybe getTyCon tyclss
-                   -- Recursion of newtypes/data types can happen via
-                   -- the class TyCon, so tyclss includes the class tycons
 
     is_promotable = all (computeTyConPromotability rec_tycon_names) all_tycons
 
@@ -466,10 +465,6 @@ calcRecFlags boot_details is_boot mrole_env tyclss
 new_tc_rhs :: TyCon -> Type
 new_tc_rhs tc = snd (newTyConRhs tc)    -- Ignore the type variables
 
-getTyCon :: TyThing -> Maybe TyCon
-getTyCon (ATyCon tc) = Just tc
-getTyCon _           = Nothing
-
 findLoopBreakers :: [(TyCon, [TyCon])] -> [Name]
 -- Finds a set of tycons that cut all loops
 findLoopBreakers deps
@@ -811,19 +806,39 @@ updateRoleEnv name n role
 *                                                                      *
 ********************************************************************* -}
 
-tcAddImplicits :: [TyThing] -> TcM TcGblEnv
-tcAddImplicits tyclss
+tcAddImplicits :: [TyCon] -> TcM TcGblEnv
+tcAddImplicits tycons
   = discardWarnings $
     tcExtendGlobalEnvImplicit implicit_things  $
     tcExtendGlobalValEnv def_meth_ids          $
-    do { (typeable_ids, typeable_binds) <- mkTypeableBinds tycons
+    do { traceTc "tcAddImplicits" $ vcat
+            [ text "tycons" <+> ppr tycons
+            , text "implicits" <+> ppr implicit_things ]
+       ; (typeable_ids, typeable_binds) <- mkTypeableBinds tycons
        ; gbl_env <- tcExtendGlobalValEnv typeable_ids
                     $ tcRecSelBinds $ mkRecSelBinds tycons
        ; return (gbl_env `addTypecheckedBinds` typeable_binds) }
  where
-   implicit_things = concatMap implicitTyThings tyclss
-   tycons          = [tc | ATyCon tc <- tyclss]
-   def_meth_ids    = mkDefaultMethodIds tyclss
+   implicit_things = concatMap implicitTyConThings tycons
+   def_meth_ids    = mkDefaultMethodIds tycons
+
+mkDefaultMethodIds :: [TyCon] -> [Id]
+-- We want to put the default-method Ids (both vanilla and generic)
+-- into the type environment so that they are found when we typecheck
+-- the filled-in default methods of each instance declaration
+-- See Note [Default method Ids and Template Haskell]
+mkDefaultMethodIds tycons
+  = [ mkExportedLocalId VanillaId dm_name (mk_dm_ty cls sel_id dm_spec)
+    | tc <- tycons
+    , Just cls <- [tyConClass_maybe tc]
+    , (sel_id, Just (dm_name, dm_spec)) <- classOpItems cls ]
+  where
+    mk_dm_ty :: Class -> Id -> DefMethSpec Type -> Type
+    mk_dm_ty _ sel_id VanillaDM        = idType sel_id
+    mk_dm_ty cls _   (GenericDM dm_ty) = mkSigmaTy cls_tvs [pred] dm_ty
+       where
+         cls_tvs = classTyVars cls
+         pred    = mkClassPred cls (mkTyVarTys cls_tvs)
 
 {-
 ************************************************************************
@@ -833,14 +848,8 @@ tcAddImplicits tyclss
 ************************************************************************
 -}
 
-mkDefaultMethodIds :: [TyThing] -> [Id]
--- See Note [Default method Ids and Template Haskell]
-mkDefaultMethodIds things
-  = [ mkExportedLocalId VanillaId dm_name (idType sel_id)
-    | ATyCon tc <- things
-    , Just cls <- [tyConClass_maybe tc]
-    , (sel_id, DefMeth dm_name) <- classOpItems cls ]
-
+{-
+-}
 {-
 Note [Default method Ids and Template Haskell]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/typecheck/TcTypeable.hs b/compiler/typecheck/TcTypeable.hs
index f015eec79f..32777831bc 100644
--- a/compiler/typecheck/TcTypeable.hs
+++ b/compiler/typecheck/TcTypeable.hs
@@ -147,7 +147,9 @@ mkTypeableBinds tycons
                            Just mod_id -> nlHsVar mod_id
                            Nothing     -> pprPanic "tcMkTypeableBinds" (ppr tycons)
              stuff    = (dflags, mod_expr, pkg_str, mod_str, tr_datacon, trn_datacon)
-             tc_binds = map (mk_typeable_binds stuff) tycons
+             all_tycons = [ tc' | tc <- tycons, tc' <- tc : tyConATs tc ]
+                             -- We need type representations for any associated types
+             tc_binds = map (mk_typeable_binds stuff) all_tycons
              tycon_rep_ids = foldr ((++) . collectHsBindsBinders) [] tc_binds
        ; return (tycon_rep_ids, tc_binds) } }
 
diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index d3f8291881..91c5874e69 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -217,11 +217,7 @@ checkAmbiguity ctxt ty
        ; (_wrap, wanted) <- addErrCtxtM (mk_msg ty') $
                             captureConstraints $
                             tcSubType_NC ctxt ty' ty'
-       ; whenNoErrs $  -- only run the simplifier if we have a clean
-                       -- environment. Otherwise we might trip.
-                       -- example: indexed-types/should_fail/BadSock
-                       -- fails in DEBUG mode without this
-         simplifyAmbiguityCheck ty wanted
+       ; simplifyAmbiguityCheck ty wanted
 
        ; traceTc "Done ambiguity check for" (ppr ty) }
  where
diff --git a/compiler/types/Class.hs b/compiler/types/Class.hs
index 34f6edbcec..a1d5a400dd 100644
--- a/compiler/types/Class.hs
+++ b/compiler/types/Class.hs
@@ -7,10 +7,10 @@
 
 module Class (
         Class,
-        ClassOpItem, DefMeth (..),
+        ClassOpItem,
         ClassATItem(..),
         ClassMinimalDef,
-        defMethSpecOfDefMeth,
+        DefMethInfo, pprDefMethInfo, defMethSpecOfDefMeth,
 
         FunDep, pprFundeps, pprFunDep,
 
@@ -90,14 +90,17 @@ data Class
 -- For details on above see note [Api annotations] in ApiAnnotation
 type FunDep a = ([a],[a])
 
-type ClassOpItem = (Id, DefMeth)
+type ClassOpItem = (Id, DefMethInfo)
         -- Selector function; contains unfolding
         -- Default-method info
 
-data DefMeth = NoDefMeth                -- No default method
-             | DefMeth Name             -- A polymorphic default method
-             | GenDefMeth Name          -- A generic default method
-             deriving Eq
+type DefMethInfo = Maybe (Name, DefMethSpec Type)
+   -- Nothing                    No default method
+   -- Just ($dm, VanillaDM)      A polymorphic default method, name $dm
+   -- Just ($gm, GenericDM ty)   A generic default method, name $gm, type ty
+   --                              The generic dm type is *not* quantified
+   --                              over the class variables; ie has the
+   --                              class vaiables free
 
 data ClassATItem
   = ATI TyCon         -- See Note [Associated type tyvar names]
@@ -107,14 +110,13 @@ data ClassATItem
 
 type ClassMinimalDef = BooleanFormula Name -- Required methods
 
--- | Convert a `DefMethSpec` to a `DefMeth`, which discards the name field in
+-- | Convert a `DefMethInfo` to a `DefMethSpec`, which discards the name field in
 --   the `DefMeth` constructor of the `DefMeth`.
-defMethSpecOfDefMeth :: DefMeth -> DefMethSpec
+defMethSpecOfDefMeth :: DefMethInfo -> Maybe (DefMethSpec Type)
 defMethSpecOfDefMeth meth
  = case meth of
-        NoDefMeth       -> NoDM
-        DefMeth _       -> VanillaDM
-        GenDefMeth _    -> GenericDM
+     Nothing        -> Nothing
+     Just (_, spec) -> Just spec
 
 {-
 Note [Associated type defaults]
@@ -283,10 +285,11 @@ instance NamedThing Class where
 instance Outputable Class where
     ppr c = ppr (getName c)
 
-instance Outputable DefMeth where
-    ppr (DefMeth n)    =  ptext (sLit "Default method") <+> ppr n
-    ppr (GenDefMeth n) =  ptext (sLit "Generic default method") <+> ppr n
-    ppr NoDefMeth      =  empty   -- No default method
+pprDefMethInfo :: DefMethInfo -> SDoc
+pprDefMethInfo Nothing                  = empty   -- No default method
+pprDefMethInfo (Just (n, VanillaDM))    = ptext (sLit "Default method") <+> ppr n
+pprDefMethInfo (Just (n, GenericDM ty)) = ptext (sLit "Generic default method")
+                                          <+> ppr n <+> dcolon <+> ppr ty
 
 pprFundeps :: Outputable a => [FunDep a] -> SDoc
 pprFundeps []  = empty
diff --git a/compiler/types/TyCon.hs b/compiler/types/TyCon.hs
index a9482906e9..fd0d5e5aac 100644
--- a/compiler/types/TyCon.hs
+++ b/compiler/types/TyCon.hs
@@ -73,7 +73,7 @@ module TyCon(
         tyConArity,
         tyConRoles,
         tyConFlavour,
-        tyConTuple_maybe, tyConClass_maybe,
+        tyConTuple_maybe, tyConClass_maybe, tyConATs,
         tyConFamInst_maybe, tyConFamInstSig_maybe, tyConFamilyCoercion_maybe,
         tyConFamilyResVar_maybe,
         synTyConDefn_maybe, synTyConRhs_maybe,
@@ -1303,12 +1303,20 @@ isAbstractTyCon :: TyCon -> Bool
 isAbstractTyCon (AlgTyCon { algTcRhs = AbstractTyCon {} }) = True
 isAbstractTyCon _ = False
 
--- | Make an algebraic 'TyCon' abstract. Panics if the supplied 'TyCon' is not
--- algebraic
+-- | Make an fake, abstract 'TyCon' from an existing one.
+-- Used when recovering from errors
 makeTyConAbstract :: TyCon -> TyCon
-makeTyConAbstract tc@(AlgTyCon { algTcRhs = rhs })
-  = tc { algTcRhs = AbstractTyCon (isGenInjAlgRhs rhs) }
-makeTyConAbstract tc = pprPanic "makeTyConAbstract" (ppr tc)
+makeTyConAbstract tc
+  = PrimTyCon { tyConName        = name,
+                tyConUnique      = nameUnique name,
+                tyConKind        = tyConKind tc,
+                tyConArity       = tyConArity tc,
+                tcRoles          = tyConRoles tc,
+                primTyConRep     = PtrRep,
+                isUnLifted       = False,
+                primRepName      = Nothing }
+  where
+    name = tyConName tc
 
 -- | Does this 'TyCon' represent something that cannot be defined in Haskell?
 isPrimTyCon :: TyCon -> Bool
@@ -1867,6 +1875,11 @@ tyConClass_maybe :: TyCon -> Maybe Class
 tyConClass_maybe (AlgTyCon {algTcParent = ClassTyCon clas _}) = Just clas
 tyConClass_maybe _                                            = Nothing
 
+-- | Return the associated types of the 'TyCon', if any
+tyConATs :: TyCon -> [TyCon]
+tyConATs (AlgTyCon {algTcParent = ClassTyCon clas _}) = classATs clas
+tyConATs _                                            = []
+
 ----------------------------------------------------------------------------
 -- | Is this 'TyCon' that for a data family instance?
 isFamInstTyCon :: TyCon -> Bool
diff --git a/compiler/utils/Binary.hs b/compiler/utils/Binary.hs
index 5083804d6f..ab5b772eec 100644
--- a/compiler/utils/Binary.hs
+++ b/compiler/utils/Binary.hs
@@ -807,17 +807,6 @@ instance Binary InlineSpec where
                   2 -> return Inlinable
                   _ -> return NoInline
 
-instance Binary DefMethSpec where
-    put_ bh NoDM      = putByte bh 0
-    put_ bh VanillaDM = putByte bh 1
-    put_ bh GenericDM = putByte bh 2
-    get bh = do
-            h <- getByte bh
-            case h of
-              0 -> return NoDM
-              1 -> return VanillaDM
-              _ -> return GenericDM
-
 instance Binary RecFlag where
     put_ bh Recursive = do
             putByte bh 0
diff --git a/compiler/vectorise/Vectorise/Type/TyConDecl.hs b/compiler/vectorise/Vectorise/Type/TyConDecl.hs
index 40f28d18d8..e462d0fac1 100644
--- a/compiler/vectorise/Vectorise/Type/TyConDecl.hs
+++ b/compiler/vectorise/Vectorise/Type/TyConDecl.hs
@@ -6,7 +6,7 @@ module Vectorise.Type.TyConDecl (
 import Vectorise.Type.Type
 import Vectorise.Monad
 import Vectorise.Env( GlobalEnv( global_fam_inst_env ) )
-import BuildTyCl( buildClass, buildDataCon )
+import BuildTyCl( TcMethInfo, buildClass, buildDataCon )
 import OccName
 import Class
 import Type
@@ -120,7 +120,7 @@ vectTyConDecl tycon name'
 
 -- |Vectorise a class method.  (Don't enter it into the vectorisation map yet.)
 --
-vectMethod :: Id -> DefMeth -> Type -> VM (Name, DefMethSpec, Type)
+vectMethod :: Id -> DefMethInfo -> Type -> VM TcMethInfo
 vectMethod id defMeth ty
  = do {   -- Vectorise the method type.
       ; ty' <- vectType ty
@@ -128,7 +128,7 @@ vectMethod id defMeth ty
           -- Create a name for the vectorised method.
       ; id' <- mkVectId id ty'
 
-      ; return  (Var.varName id', defMethSpecOfDefMeth defMeth, ty')
+      ; return  (Var.varName id', ty', defMethSpecOfDefMeth defMeth)
       }
 
 -- |Vectorise the RHS of an algebraic type.
diff --git a/testsuite/tests/th/T9064.stderr b/testsuite/tests/th/T9064.stderr
index f9c171683d..24fdc8da83 100644
--- a/testsuite/tests/th/T9064.stderr
+++ b/testsuite/tests/th/T9064.stderr
@@ -1,7 +1,6 @@
 class T9064.C (a_0 :: *)
     where T9064.foo :: forall (a_0 :: *) . T9064.C a_0 =>
                                            a_0 -> GHC.Base.String
-          default T9064.foo :: forall (a_0 :: *) . (T9064.C a_0,
-                                                    GHC.Show.Show a_0) =>
-                                                   a_0 -> GHC.Base.String
+          default T9064.foo :: forall . GHC.Show.Show a_0 =>
+                                        a_0 -> GHC.Base.String
 instance T9064.C T9064.Bar
diff --git a/testsuite/tests/typecheck/should_fail/T5300.stderr b/testsuite/tests/typecheck/should_fail/T5300.stderr
index 7e06b620d2..524edc4446 100644
--- a/testsuite/tests/typecheck/should_fail/T5300.stderr
+++ b/testsuite/tests/typecheck/should_fail/T5300.stderr
@@ -1,17 +1,32 @@
 
+T5300.hs:11:7: error:
+    • Could not deduce (C1 a b c0)
+      from the context: (Monad m, C1 a b c)
+        bound by the type signature for:
+                   f1 :: (Monad m, C1 a b c) => a -> StateT (T b) m a
+        at T5300.hs:11:7-50
+      The type variable ‘c0’ is ambiguous
+    • In the ambiguity check for the type signature for ‘f1’:
+        f1 :: forall a b (m :: * -> *) c.
+              (Monad m, C1 a b c) =>
+              a -> StateT (T b) m a
+      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
+      In the type signature for ‘f1’:
+        f1 :: (Monad m, C1 a b c) => a -> StateT (T b) m a
+
 T5300.hs:14:7: error:
-    Could not deduce (C2 a2 b2 c20)
-    from the context: (Monad m, C1 a1 b1 c1, C2 a2 b2 c2)
-      bound by the type signature for:
-                 f2 :: (Monad m, C1 a1 b1 c1, C2 a2 b2 c2) =>
-                       a1 -> StateT (T b2) m a2
-      at T5300.hs:14:7-69
-    The type variable ‘c20’ is ambiguous
-    In the ambiguity check for the type signature for ‘f2’:
-      f2 :: forall a1 b2 (m :: * -> *) a2 b1 c1 c2.
-            (Monad m, C1 a1 b1 c1, C2 a2 b2 c2) =>
-            a1 -> StateT (T b2) m a2
-    To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
-    In the type signature for ‘f2’:
-      f2 :: (Monad m, C1 a1 b1 c1, C2 a2 b2 c2) =>
-            a1 -> StateT (T b2) m a2
+    • Could not deduce (C2 a2 b2 c20)
+      from the context: (Monad m, C1 a1 b1 c1, C2 a2 b2 c2)
+        bound by the type signature for:
+                   f2 :: (Monad m, C1 a1 b1 c1, C2 a2 b2 c2) =>
+                         a1 -> StateT (T b2) m a2
+        at T5300.hs:14:7-69
+      The type variable ‘c20’ is ambiguous
+    • In the ambiguity check for the type signature for ‘f2’:
+        f2 :: forall a1 b2 (m :: * -> *) a2 b1 c1 c2.
+              (Monad m, C1 a1 b1 c1, C2 a2 b2 c2) =>
+              a1 -> StateT (T b2) m a2
+      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
+      In the type signature for ‘f2’:
+        f2 :: (Monad m, C1 a1 b1 c1, C2 a2 b2 c2) =>
+              a1 -> StateT (T b2) m a2
diff --git a/testsuite/tests/typecheck/should_fail/T8030.stderr b/testsuite/tests/typecheck/should_fail/T8030.stderr
index 831cf42edd..24c9d59ff7 100644
--- a/testsuite/tests/typecheck/should_fail/T8030.stderr
+++ b/testsuite/tests/typecheck/should_fail/T8030.stderr
@@ -1,11 +1,24 @@
 
 T8030.hs:9:3: error:
-    Couldn't match expected type ‘Pr a’ with actual type ‘Pr a0’
-    NB: ‘Pr’ is a type function, and may not be injective
-    The type variable ‘a0’ is ambiguous
-    In the ambiguity check for the type signature for ‘op1’:
-      op1 :: forall (k :: BOX) (a :: k). C a => Pr a
-    To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
-    When checking the class method:
-      op1 :: forall (k :: BOX) (a :: k). C a => Pr a
-    In the class declaration for ‘C’
+    • Couldn't match expected type ‘Pr a’ with actual type ‘Pr a0’
+      NB: ‘Pr’ is a type function, and may not be injective
+      The type variable ‘a0’ is ambiguous
+    • In the ambiguity check for the type signature for ‘op1’:
+        op1 :: forall (k :: BOX) (a :: k). C a => Pr a
+      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
+      When checking the class method:
+        op1 :: forall (k :: BOX) (a :: k). C a => Pr a
+      In the class declaration for ‘C’
+
+T8030.hs:10:3: error:
+    • Couldn't match type ‘Pr a0’ with ‘Pr a’
+      NB: ‘Pr’ is a type function, and may not be injective
+      The type variable ‘a0’ is ambiguous
+      Expected type: Pr a -> Pr a -> Pr a
+        Actual type: Pr a0 -> Pr a0 -> Pr a0
+    • In the ambiguity check for the type signature for ‘op2’:
+        op2 :: forall (k :: BOX) (a :: k). C a => Pr a -> Pr a -> Pr a
+      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
+      When checking the class method:
+        op2 :: forall (k :: BOX) (a :: k). C a => Pr a -> Pr a -> Pr a
+      In the class declaration for ‘C’