Make a smart mkAppTyM
[ghc.git] / compiler / typecheck / TcTyDecls.hs
index 42387de..dc983ca 100644 (file)
@@ -3,35 +3,37 @@
 (c) The GRASP/AQUA Project, Glasgow University, 1992-1999
 
 
-Analysis functions over data types.  Specficially, detecting recursive types.
+Analysis functions over data types.  Specifically, detecting recursive types.
 
 This stuff is only used for source-code decls; it's recorded in interface
 files for imported data types.
 -}
 
 {-# LANGUAGE CPP #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE ViewPatterns #-}
 
 module TcTyDecls(
-        calcRecFlags, RecTyInfo(..),
-        calcSynCycles, calcClassCycles,
-
-        -- * Roles
-        RoleAnnots, extractRoleAnnots, emptyRoleAnnots, lookupRoleAnnots,
+        RolesInfo,
+        inferRoles,
+        checkSynCycles,
+        checkClassCycles,
 
         -- * Implicits
-        tcAddImplicits,
+        addTyConsToGblEnv, mkDefaultMethodType,
 
         -- * Record selectors
-        mkRecSelBinds, mkOneRecordSelector
+        tcRecSelBinds, mkRecSelBinds, mkOneRecordSelector
     ) where
 
 #include "HsVersions.h"
 
+import GhcPrelude
+
 import TcRnMonad
 import TcEnv
-import TcTypeable( mkTypeableBinds )
-import TcBinds( tcRecSelBinds, addTypecheckedBinds )
-import TypeRep( Type(..) )
+import TcBinds( tcValBinds, addTypecheckedBinds )
+import TyCoRep( Type(..), Coercion(..), MCoercion(..), UnivCoProvenance(..) )
 import TcType
 import TysWiredIn( unitTy )
 import MkCore( rEC_SEL_ERROR_ID )
@@ -44,461 +46,301 @@ import ConLike
 import DataCon
 import Name
 import NameEnv
+import NameSet hiding (unitFV)
 import RdrName ( mkVarUnqual )
 import Id
 import IdInfo
 import VarEnv
 import VarSet
-import NameSet
 import Coercion ( ltRole )
-import Digraph
 import BasicTypes
 import SrcLoc
 import Unique ( mkBuiltinUnique )
 import Outputable
-import UniqSet
 import Util
 import Maybes
-import Data.List
 import Bag
-import FastString ( fastStringToByteString )
+import FastString
+import FV
+import Module
 
 import Control.Monad
 
 {-
 ************************************************************************
 *                                                                      *
-        Cycles in class and type synonym declarations
+        Cycles in type synonym declarations
 *                                                                      *
 ************************************************************************
-
-Checking for class-decl loops is easy, because we don't allow class decls
-in interface files.
-
-We allow type synonyms in hi-boot files, but we *trust* hi-boot files,
-so we don't check for loops that involve them.  So we only look for synonym
-loops in the module being compiled.
-
-We check for type synonym and class cycles on the *source* code.
-Main reasons:
-
-  a) Otherwise we'd need a special function to extract type-synonym tycons
-     from a type, whereas we already have the free vars pinned on the decl
-
-  b) If we checked for type synonym loops after building the TyCon, we
-        can't do a hoistForAllTys on the type synonym rhs, (else we fall into
-        a black hole) which seems unclean.  Apart from anything else, it'd mean
-        that a type-synonym rhs could have for-alls to the right of an arrow,
-        which means adding new cases to the validity checker
-
-        Indeed, in general, checking for cycles beforehand means we need to
-        be less careful about black holes through synonym cycles.
-
-The main disadvantage is that a cycle that goes via a type synonym in an
-.hi-boot file can lead the compiler into a loop, because it assumes that cycles
-only occur entirely within the source code of the module being compiled.
-But hi-boot files are trusted anyway, so this isn't much worse than (say)
-a kind error.
-
-[  NOTE ----------------------------------------------
-If we reverse this decision, this comment came from tcTyDecl1, and should
- go back there
-        -- dsHsType, not tcHsKindedType, to avoid a loop.  tcHsKindedType does hoisting,
-        -- which requires looking through synonyms... and therefore goes into a loop
-        -- on (erroneously) recursive synonyms.
-        -- Solution: do not hoist synonyms, because they'll be hoisted soon enough
-        --           when they are substituted
-
-We'd also need to add back in this definition
+-}
 
 synonymTyConsOfType :: Type -> [TyCon]
 -- Does not look through type synonyms at all
 -- Return a list of synonym tycons
+-- Keep this synchronized with 'expandTypeSynonyms'
 synonymTyConsOfType ty
   = nameEnvElts (go ty)
   where
      go :: Type -> NameEnv TyCon  -- The NameEnv does duplicate elim
-     go (TyVarTy v)               = emptyNameEnv
-     go (TyConApp tc tys)         = go_tc tc tys
+     go (TyConApp tc tys)         = go_tc tc `plusNameEnv` go_s tys
+     go (LitTy _)                 = emptyNameEnv
+     go (TyVarTy _)               = emptyNameEnv
      go (AppTy a b)               = go a `plusNameEnv` go b
      go (FunTy a b)               = go a `plusNameEnv` go b
      go (ForAllTy _ ty)           = go ty
-
-     go_tc tc tys | isTypeSynonymTyCon tc = extendNameEnv (go_s tys)
-                                                          (tyConName tc) tc
-                  | otherwise             = go_s tys
+     go (CastTy ty co)            = go ty `plusNameEnv` go_co co
+     go (CoercionTy co)           = go_co co
+
+     -- Note [TyCon cycles through coercions?!]
+     -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+     -- Although, in principle, it's possible for a type synonym loop
+     -- could go through a coercion (since a coercion can refer to
+     -- a TyCon or Type), it doesn't seem possible to actually construct
+     -- a Haskell program which tickles this case.  Here is an example
+     -- program which causes a coercion:
+     --
+     --   type family Star where
+     --       Star = Type
+     --
+     --   data T :: Star -> Type
+     --   data S :: forall (a :: Type). T a -> Type
+     --
+     -- Here, the application 'T a' must first coerce a :: Type to a :: Star,
+     -- witnessed by the type family.  But if we now try to make Type refer
+     -- to a type synonym which in turn refers to Star, we'll run into
+     -- trouble: we're trying to define and use the type constructor
+     -- in the same recursive group.  Possibly this restriction will be
+     -- lifted in the future but for now, this code is "just for completeness
+     -- sake".
+     go_mco MRefl    = emptyNameEnv
+     go_mco (MCo co) = go_co co
+
+     go_co (Refl ty)              = go ty
+     go_co (GRefl _ ty mco)       = go ty `plusNameEnv` go_mco mco
+     go_co (TyConAppCo _ tc cs)   = go_tc tc `plusNameEnv` go_co_s cs
+     go_co (AppCo co co')         = go_co co `plusNameEnv` go_co co'
+     go_co (ForAllCo _ co co')    = go_co co `plusNameEnv` go_co co'
+     go_co (FunCo _ co co')       = go_co co `plusNameEnv` go_co co'
+     go_co (CoVarCo _)            = emptyNameEnv
+     go_co (HoleCo {})            = emptyNameEnv
+     go_co (AxiomInstCo _ _ cs)   = go_co_s cs
+     go_co (UnivCo p _ ty ty')    = go_prov p `plusNameEnv` go ty `plusNameEnv` go ty'
+     go_co (SymCo co)             = go_co co
+     go_co (TransCo co co')       = go_co co `plusNameEnv` go_co co'
+     go_co (NthCo _ _ co)         = go_co co
+     go_co (LRCo _ co)            = go_co co
+     go_co (InstCo co co')        = go_co co `plusNameEnv` go_co co'
+     go_co (KindCo co)            = go_co co
+     go_co (SubCo co)             = go_co co
+     go_co (AxiomRuleCo _ cs)     = go_co_s cs
+
+     go_prov UnsafeCoerceProv     = emptyNameEnv
+     go_prov (PhantomProv co)     = go_co co
+     go_prov (ProofIrrelProv co)  = go_co co
+     go_prov (PluginProv _)       = emptyNameEnv
+
+     go_tc tc | isTypeSynonymTyCon tc = unitNameEnv (tyConName tc) tc
+              | otherwise             = emptyNameEnv
      go_s tys = foldr (plusNameEnv . go) emptyNameEnv tys
----------------------------------------- END NOTE ]
--}
-
-mkSynEdges :: [LTyClDecl Name] -> [(LTyClDecl Name, Name, [Name])]
-mkSynEdges syn_decls = [ (ldecl, name, nameSetElems fvs)
-                       | ldecl@(L _ (SynDecl { tcdLName = L _ name
-                                             , tcdFVs = fvs })) <- syn_decls ]
-
-calcSynCycles :: [LTyClDecl Name] -> [SCC (LTyClDecl Name)]
-calcSynCycles = stronglyConnCompFromEdgedVertices . mkSynEdges
-
-{-
-Note [Superclass cycle check]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We can't allow cycles via superclasses because it would result in the
-type checker looping when it canonicalises a class constraint (superclasses
-are added during canonicalisation).  More precisely, given a constraint
-    C ty1 .. tyn
-we want to instantiate all of C's superclasses, transitively, and
-that set must be finite.  So if
-     class (D b, E b a) => C a b
-then when we encounter the constraint
-     C ty1 ty2
-we'll instantiate the superclasses
-     (D ty2, E ty2 ty1)
-and then *their* superclasses, and so on.  This set must be finite!
-
-It is OK for superclasses to be type synonyms for other classes, so
-must "look through" type synonyms. Eg
-     type X a = C [a]
-     class X a => C a   -- No!  Recursive superclass!
-
-We want definitions such as:
+     go_co_s cos = foldr (plusNameEnv . go_co) emptyNameEnv cos
 
-  class C cls a where cls a => a -> a
-  class C D a => D a where
+-- | A monad for type synonym cycle checking, which keeps
+-- track of the TyCons which are known to be acyclic, or
+-- a failure message reporting that a cycle was found.
+newtype SynCycleM a = SynCycleM {
+    runSynCycleM :: SynCycleState -> Either (SrcSpan, SDoc) (a, SynCycleState) }
 
-to be accepted, even though a naive acyclicity check would reject the
-program as having a cycle between D and its superclass.  Why? Because
-when we instantiate
-     D ty1
-we get the superclas
-     C D ty1
-and C has no superclasses, so we have terminated with a finite set.
+type SynCycleState = NameSet
 
-More precisely, the rule is this: the superclasses sup_C of a class C
-are rejected iff:
-
-  C \elem expand(sup_C)
-
-Where expand is defined as follows:
-
-(1)  expand(a ty1 ... tyN) = expand(ty1) \union ... \union expand(tyN)
-
-(2)  expand(D ty1 ... tyN) = {D}
-                             \union sup_D[ty1/x1, ..., tyP/xP]
-                             \union expand(ty(P+1)) ... \union expand(tyN)
-           where (D x1 ... xM) is a class, P = min(M,N)
-
-(3)  expand(T ty1 ... tyN) = expand(ty1) \union ... \union expand(tyN)
-        where T is not a class
-
-Eqn (1) is conservative; when there's a type variable at the head,
-look in all the argument types.  Eqn (2) expands superclasses; the
-third component of the union is like Eqn (1).  Eqn (3) happens mainly
-when the context is a (constraint) tuple, such as (Eq a, Show a).
+instance Functor SynCycleM where
+    fmap = liftM
 
-Furthermore, expand always looks through type synonyms.
--}
+instance Applicative SynCycleM where
+    pure x = SynCycleM $ \state -> Right (x, state)
+    (<*>) = ap
 
-calcClassCycles :: Class -> [[TyCon]]
-calcClassCycles cls
-  = nubBy eqAsCycle $
-    expandTheta (unitUniqSet cls) [classTyCon cls] (classSCTheta cls) []
+instance Monad SynCycleM where
+    m >>= f = SynCycleM $ \state ->
+        case runSynCycleM m state of
+            Right (x, state') ->
+                runSynCycleM (f x) state'
+            Left err -> Left err
+
+failSynCycleM :: SrcSpan -> SDoc -> SynCycleM ()
+failSynCycleM loc err = SynCycleM $ \_ -> Left (loc, err)
+
+-- | Test if a 'Name' is acyclic, short-circuiting if we've
+-- seen it already.
+checkNameIsAcyclic :: Name -> SynCycleM () -> SynCycleM ()
+checkNameIsAcyclic n m = SynCycleM $ \s ->
+    if n `elemNameSet` s
+        then Right ((), s) -- short circuit
+        else case runSynCycleM m s of
+                Right ((), s') -> Right ((), extendNameSet s' n)
+                Left err -> Left err
+
+-- | Checks if any of the passed in 'TyCon's have cycles.
+-- Takes the 'UnitId' of the home package (as we can avoid
+-- checking those TyCons: cycles never go through foreign packages) and
+-- the corresponding @LTyClDecl Name@ for each 'TyCon', so we
+-- can give better error messages.
+checkSynCycles :: UnitId -> [TyCon] -> [LTyClDecl GhcRn] -> TcM ()
+checkSynCycles this_uid tcs tyclds = do
+    case runSynCycleM (mapM_ (go emptyNameSet []) tcs) emptyNameSet of
+        Left (loc, err) -> setSrcSpan loc $ failWithTc err
+        Right _  -> return ()
   where
-    -- The last TyCon in the cycle is always the same as the first
-    eqAsCycle xs ys = any (xs ==) (cycles (tail ys))
-    cycles xs = take n . map (take n) . tails . cycle $ xs
-      where n = length xs
-
-    -- No more superclasses to expand ==> no problems with cycles
-    -- See Note [Superclass cycle check]
-    expandTheta :: UniqSet Class -- Path of Classes to here in set form
-                -> [TyCon]       -- Path to here
-                -> ThetaType     -- Superclass work list
-                -> [[TyCon]]     -- Input error paths
-                -> [[TyCon]]     -- Final error paths
-    expandTheta _    _    []           = id
-    expandTheta seen path (pred:theta) = expandType seen path pred . expandTheta seen path theta
-
-    expandType seen path (TyConApp tc tys)
-      -- Expand unsaturated classes to their superclass theta if they are yet unseen.
-      -- If they have already been seen then we have detected an error!
-      | Just cls <- tyConClass_maybe tc
-      , let (env, remainder) = papp (classTyVars cls) tys
-            rest_tys = either (const []) id remainder
-      = if cls `elementOfUniqSet` seen
-         then (reverse (classTyCon cls:path):)
-              . flip (foldr (expandType seen path)) tys
-         else expandTheta (addOneToUniqSet seen cls) (tc:path)
-                          (substTys (mkTopTvSubst env) (classSCTheta cls))
-              . flip (foldr (expandType seen path)) rest_tys
-
-      -- For synonyms, try to expand them: some arguments might be
-      -- phantoms, after all. We can expand with impunity because at
-      -- this point the type synonym cycle check has already happened.
-      | Just (tvs, rhs) <- synTyConDefn_maybe tc
-      , let (env, remainder) = papp tvs tys
-            rest_tys = either (const []) id remainder
-      = expandType seen (tc:path) (substTy (mkTopTvSubst env) rhs)
-        . flip (foldr (expandType seen path)) rest_tys
-
-      -- For non-class, non-synonyms, just check the arguments
-      | otherwise
-      = flip (foldr (expandType seen path)) tys
-
-    expandType _    _    (TyVarTy {})     = id
-    expandType _    _    (LitTy {})       = id
-    expandType seen path (AppTy t1 t2)    = expandType seen path t1 . expandType seen path t2
-    expandType seen path (FunTy t1 t2)    = expandType seen path t1 . expandType seen path t2
-    expandType seen path (ForAllTy _tv t) = expandType seen path t
-
-    papp :: [TyVar] -> [Type] -> ([(TyVar, Type)], Either [TyVar] [Type])
-    papp []       tys      = ([], Right tys)
-    papp tvs      []       = ([], Left tvs)
-    papp (tv:tvs) (ty:tys) = ((tv, ty):env, remainder)
-      where (env, remainder) = papp tvs tys
-
-{-
-************************************************************************
-*                                                                      *
-        Deciding which type constructors are recursive
-*                                                                      *
-************************************************************************
+    -- Try our best to print the LTyClDecl for locally defined things
+    lcl_decls = mkNameEnv (zip (map tyConName tcs) tyclds)
+
+    -- Short circuit if we've already seen this Name and concluded
+    -- it was acyclic.
+    go :: NameSet -> [TyCon] -> TyCon -> SynCycleM ()
+    go so_far seen_tcs tc =
+        checkNameIsAcyclic (tyConName tc) $ go' so_far seen_tcs tc
+
+    -- Expand type synonyms, complaining if you find the same
+    -- type synonym a second time.
+    go' :: NameSet -> [TyCon] -> TyCon -> SynCycleM ()
+    go' so_far seen_tcs tc
+        | n `elemNameSet` so_far
+            = failSynCycleM (getSrcSpan (head seen_tcs)) $
+                  sep [ text "Cycle in type synonym declarations:"
+                      , nest 2 (vcat (map ppr_decl seen_tcs)) ]
+        -- Optimization: we don't allow cycles through external packages,
+        -- so once we find a non-local name we are guaranteed to not
+        -- have a cycle.
+        --
+        -- This won't hold once we get recursive packages with Backpack,
+        -- but for now it's fine.
+        | not (isHoleModule mod ||
+               moduleUnitId mod == this_uid ||
+               isInteractiveModule mod)
+            = return ()
+        | Just ty <- synTyConRhs_maybe tc =
+            go_ty (extendNameSet so_far (tyConName tc)) (tc:seen_tcs) ty
+        | otherwise = return ()
+      where
+        n = tyConName tc
+        mod = nameModule n
+        ppr_decl tc =
+          case lookupNameEnv lcl_decls n of
+            Just (dL->L loc decl) -> ppr loc <> colon <+> ppr decl
+            Nothing -> ppr (getSrcSpan n) <> colon <+> ppr n
+                       <+> text "from external module"
+         where
+          n = tyConName tc
+
+    go_ty :: NameSet -> [TyCon] -> Type -> SynCycleM ()
+    go_ty so_far seen_tcs ty =
+        mapM_ (go so_far seen_tcs) (synonymTyConsOfType ty)
+
+{- Note [Superclass cycle check]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The superclass cycle check for C decides if we can statically
+guarantee that expanding C's superclass cycles transitively is
+guaranteed to terminate.  This is a Haskell98 requirement,
+but one that we lift with -XUndecidableSuperClasses.
 
-Identification of recursive TyCons
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-The knot-tying parameters: @rec_details_list@ is an alist mapping @Name@s to
-@TyThing@s.
-
-Identifying a TyCon as recursive serves two purposes
-
-1.  Avoid infinite types.  Non-recursive newtypes are treated as
-"transparent", like type synonyms, after the type checker.  If we did
-this for all newtypes, we'd get infinite types.  So we figure out for
-each newtype whether it is "recursive", and add a coercion if so.  In
-effect, we are trying to "cut the loops" by identifying a loop-breaker.
-
-2.  Avoid infinite unboxing.  This has nothing to do with newtypes.
-Suppose we have
-        data T = MkT Int T
-        f (MkT x t) = f t
-Well, this function diverges, but we don't want the strictness analyser
-to diverge.  But the strictness analyser will diverge because it looks
-deeper and deeper into the structure of T.   (I believe there are
-examples where the function does something sane, and the strictness
-analyser still diverges, but I can't see one now.)
-
-Now, concerning (1), the FC2 branch currently adds a coercion for ALL
-newtypes.  I did this as an experiment, to try to expose cases in which
-the coercions got in the way of optimisations.  If it turns out that we
-can indeed always use a coercion, then we don't risk recursive types,
-and don't need to figure out what the loop breakers are.
-
-For newtype *families* though, we will always have a coercion, so they
-are always loop breakers!  So you can easily adjust the current
-algorithm by simply treating all newtype families as loop breakers (and
-indeed type families).  I think.
-
-
-
-For newtypes, we label some as "recursive" such that
-
-    INVARIANT: there is no cycle of non-recursive newtypes
-
-In any loop, only one newtype need be marked as recursive; it is
-a "loop breaker".  Labelling more than necessary as recursive is OK,
-provided the invariant is maintained.
-
-A newtype M.T is defined to be "recursive" iff
-        (a) it is declared in an hi-boot file (see RdrHsSyn.hsIfaceDecl)
-        (b) it is declared in a source file, but that source file has a
-            companion hi-boot file which declares the type
-   or   (c) one can get from T's rhs to T via type
-            synonyms, or non-recursive newtypes *in M*
-             e.g.  newtype T = MkT (T -> Int)
-
-(a) is conservative; declarations in hi-boot files are always
-        made loop breakers. That's why in (b) we can restrict attention
-        to tycons in M, because any loops through newtypes outside M
-        will be broken by those newtypes
-(b) ensures that a newtype is not treated as a loop breaker in one place
-and later as a non-loop-breaker.  This matters in GHCi particularly, when
-a newtype T might be embedded in many types in the environment, and then
-T's source module is compiled.  We don't want T's recursiveness to change.
-
-The "recursive" flag for algebraic data types is irrelevant (never consulted)
-for types with more than one constructor.
-
-
-An algebraic data type M.T is "recursive" iff
-        it has just one constructor, and
-        (a) it is declared in an hi-boot file (see RdrHsSyn.hsIfaceDecl)
-        (b) it is declared in a source file, but that source file has a
-            companion hi-boot file which declares the type
- or     (c) one can get from its arg types to T via type synonyms,
-            or by non-recursive newtypes or non-recursive product types in M
-             e.g.  data T = MkT (T -> Int) Bool
-Just like newtype in fact
-
-A type synonym is recursive if one can get from its
-right hand side back to it via type synonyms.  (This is
-reported as an error.)
-
-A class is recursive if one can get from its superclasses
-back to it.  (This is an error too.)
-
-Hi-boot types
-~~~~~~~~~~~~~
-A data type read from an hi-boot file will have an AbstractTyCon as its AlgTyConRhs
-and will respond True to isAbstractTyCon. The idea is that we treat these as if one
-could get from these types to anywhere.  So when we see
-
-        module Baz where
-        import {-# SOURCE #-} Foo( T )
-        newtype S = MkS T
-
-then we mark S as recursive, just in case. What that means is that if we see
-
-        import Baz( S )
-        newtype R = MkR S
-
-then we don't need to look inside S to compute R's recursiveness.  Since S is imported
-(not from an hi-boot file), one cannot get from R back to S except via an hi-boot file,
-and that means that some data type will be marked recursive along the way.  So R is
-unconditionly non-recursive (i.e. there'll be a loop breaker elsewhere if necessary)
-
-This in turn means that we grovel through fewer interface files when computing
-recursiveness, because we need only look at the type decls in the module being
-compiled, plus the outer structure of directly-mentioned types.
+The worry is that a superclass cycle could make the type checker loop.
+More precisely, with a constraint (Given or Wanted)
+    C ty1 .. tyn
+one approach is to instantiate all of C's superclasses, transitively.
+We can only do so if that set is finite.
+
+This potential loop occurs only through superclasses.  This, for
+example, is fine
+  class C a where
+    op :: C b => a -> b -> b
+even though C's full definition uses C.
+
+Making the check static also makes it conservative.  Eg
+  type family F a
+  class F a => C a
+Here an instance of (F a) might mention C:
+  type instance F [a] = C a
+and now we'd have a loop.
+
+The static check works like this, starting with C
+  * Look at C's superclass predicates
+  * If any is a type-function application,
+    or is headed by a type variable, fail
+  * If any has C at the head, fail
+  * If any has a type class D at the head,
+    make the same test with D
+
+A tricky point is: what if there is a type variable at the head?
+Consider this:
+   class f (C f) => C f
+   class c       => Id c
+and now expand superclasses for constraint (C Id):
+     C Id
+ --> Id (C Id)
+ --> C Id
+ --> ....
+Each step expands superclasses one layer, and clearly does not terminate.
 -}
 
-data RecTyInfo = RTI { rti_promotable :: Bool
-                     , rti_roles      :: Name -> [Role]
-                     , rti_is_rec     :: Name -> RecFlag }
-
-calcRecFlags :: SelfBootInfo -> Bool  -- hs-boot file?
-             -> RoleAnnots -> [TyThing] -> 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
-  = RTI { rti_promotable = is_promotable
-        , rti_roles      = roles
-        , rti_is_rec     = is_rec }
+checkClassCycles :: Class -> Maybe SDoc
+-- Nothing  <=> ok
+-- Just err <=> possible cycle error
+checkClassCycles cls
+  = do { (definite_cycle, err) <- go (unitNameSet (getName cls))
+                                     cls (mkTyVarTys (classTyVars cls))
+       ; let herald | definite_cycle = text "Superclass cycle for"
+                    | otherwise      = text "Potential superclass cycle for"
+       ; return (vcat [ herald <+> quotes (ppr cls)
+                      , nest 2 err, hint]) }
   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
-
-    roles = inferRoles is_boot mrole_env all_tycons
-
-    ----------------- Recursion calculation ----------------
-    is_rec n | n `elemNameSet` rec_names = Recursive
-             | otherwise                 = NonRecursive
-
-    boot_name_set = case boot_details of
-                      NoSelfBoot                -> emptyNameSet
-                      SelfBoot { sb_tcs = tcs } -> tcs
-    rec_names = boot_name_set     `unionNameSet`
-                nt_loop_breakers  `unionNameSet`
-                prod_loop_breakers
-
-
-        -------------------------------------------------
-        --                      NOTE
-        -- These edge-construction loops rely on
-        -- every loop going via tyclss, the types and classes
-        -- in the module being compiled.  Stuff in interface
-        -- files should be correctly marked.  If not (e.g. a
-        -- type synonym in a hi-boot file) we can get an infinite
-        -- loop.  We could program round this, but it'd make the code
-        -- rather less nice, so I'm not going to do that yet.
-
-    single_con_tycons = [ tc | tc <- all_tycons
-                             , not (tyConName tc `elemNameSet` boot_name_set)
-                                 -- Remove the boot_name_set because they are
-                                 -- going to be loop breakers regardless.
-                             , isSingleton (tyConDataCons tc) ]
-        -- Both newtypes and data types, with exactly one data constructor
-
-    (new_tycons, prod_tycons) = partition isNewTyCon single_con_tycons
-        -- NB: we do *not* call isProductTyCon because that checks
-        --     for vanilla-ness of data constructors; and that depends
-        --     on empty existential type variables; and that is figured
-        --     out by tcResultType; which uses tcMatchTy; which uses
-        --     coreView; which calls expandSynTyCon_maybe; which uses
-        --     the recursiveness of the TyCon.  Result... a black hole.
-        -- YUK YUK YUK
-
-        --------------- Newtypes ----------------------
-    nt_loop_breakers = mkNameSet (findLoopBreakers nt_edges)
-    is_rec_nt tc = tyConName tc  `elemNameSet` nt_loop_breakers
-        -- is_rec_nt is a locally-used helper function
-
-    nt_edges = [(t, mk_nt_edges t) | t <- new_tycons]
-
-    mk_nt_edges nt      -- Invariant: nt is a newtype
-        = [ tc | tc <- nameEnvElts (tyConsOfType (new_tc_rhs nt))
-                        -- tyConsOfType looks through synonyms
-               , tc `elem` new_tycons ]
-           -- If not (tc `elem` new_tycons) we know that either it's a local *data* type,
-           -- or it's imported.  Either way, it can't form part of a newtype cycle
-
-        --------------- Product types ----------------------
-    prod_loop_breakers = mkNameSet (findLoopBreakers prod_edges)
-
-    prod_edges = [(tc, mk_prod_edges tc) | tc <- prod_tycons]
-
-    mk_prod_edges tc    -- Invariant: tc is a product tycon
-        = concatMap (mk_prod_edges1 tc) (dataConOrigArgTys (head (tyConDataCons tc)))
-
-    mk_prod_edges1 ptc ty = concatMap (mk_prod_edges2 ptc) (nameEnvElts (tyConsOfType ty))
-
-    mk_prod_edges2 ptc tc
-        | tc `elem` prod_tycons   = [tc]                -- Local product
-        | tc `elem` new_tycons    = if is_rec_nt tc     -- Local newtype
-                                    then []
-                                    else mk_prod_edges1 ptc (new_tc_rhs tc)
-                -- At this point we know that either it's a local non-product data type,
-                -- or it's imported.  Either way, it can't form part of a cycle
-        | otherwise = []
-
-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
-  = go [(tc,tc,ds) | (tc,ds) <- deps]
-  where
-    go edges = [ name
-               | CyclicSCC ((tc,_,_) : edges') <- stronglyConnCompFromEdgedVerticesR edges,
-                 name <- tyConName tc : go edges']
-
-{-
-************************************************************************
-*                                                                      *
-        Role annotations
-*                                                                      *
-************************************************************************
--}
-
-type RoleAnnots = NameEnv (LRoleAnnotDecl Name)
-
-extractRoleAnnots :: TyClGroup Name -> RoleAnnots
-extractRoleAnnots (TyClGroup { group_roles = roles })
-  = mkNameEnv [ (tycon, role_annot)
-              | role_annot@(L _ (RoleAnnotDecl (L _ tycon) _)) <- roles ]
-
-emptyRoleAnnots :: RoleAnnots
-emptyRoleAnnots = emptyNameEnv
-
-lookupRoleAnnots :: RoleAnnots -> Name -> Maybe (LRoleAnnotDecl Name)
-lookupRoleAnnots = lookupNameEnv
+    hint = text "Use UndecidableSuperClasses to accept this"
+
+    -- Expand superclasses starting with (C a b), complaining
+    -- if you find the same class a second time, or a type function
+    -- or predicate headed by a type variable
+    --
+    -- NB: this code duplicates TcType.transSuperClasses, but
+    --     with more error message generation clobber
+    -- Make sure the two stay in sync.
+    go :: NameSet -> Class -> [Type] -> Maybe (Bool, SDoc)
+    go so_far cls tys = firstJusts $
+                        map (go_pred so_far) $
+                        immSuperClasses cls tys
+
+    go_pred :: NameSet -> PredType -> Maybe (Bool, SDoc)
+       -- Nothing <=> ok
+       -- Just (True, err)  <=> definite cycle
+       -- Just (False, err) <=> possible cycle
+    go_pred so_far pred  -- NB: tcSplitTyConApp looks through synonyms
+       | Just (tc, tys) <- tcSplitTyConApp_maybe pred
+       = go_tc so_far pred tc tys
+       | hasTyVarHead pred
+       = Just (False, hang (text "one of whose superclass constraints is headed by a type variable:")
+                         2 (quotes (ppr pred)))
+       | otherwise
+       = Nothing
+
+    go_tc :: NameSet -> PredType -> TyCon -> [Type] -> Maybe (Bool, SDoc)
+    go_tc so_far pred tc tys
+      | isFamilyTyCon tc
+      = Just (False, hang (text "one of whose superclass constraints is headed by a type family:")
+                        2 (quotes (ppr pred)))
+      | Just cls <- tyConClass_maybe tc
+      = go_cls so_far cls tys
+      | otherwise   -- Equality predicate, for example
+      = Nothing
+
+    go_cls :: NameSet -> Class -> [Type] -> Maybe (Bool, SDoc)
+    go_cls so_far cls tys
+       | cls_nm `elemNameSet` so_far
+       = Just (True, text "one of whose superclasses is" <+> quotes (ppr cls))
+       | isCTupleClass cls
+       = go so_far cls tys
+       | otherwise
+       = do { (b,err) <- go  (so_far `extendNameSet` cls_nm) cls tys
+          ; return (b, text "one of whose superclasses is" <+> quotes (ppr cls)
+                       $$ err) }
+       where
+         cls_nm = getName cls
 
 {-
 ************************************************************************
@@ -600,50 +442,99 @@ so we need to take into account
   * the arguments:   (F a) and (a->a)
   * the context:     C a b
   * the result type: (G a)   -- this is in the eq_spec
+
+
+Note [Coercions in role inference]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Is (t |> co1) representationally equal to (t |> co2)? Of course they are! Changing
+the kind of a type is totally irrelevant to the representation of that type. So,
+we want to totally ignore coercions when doing role inference. This includes omitting
+any type variables that appear in nominal positions but only within coercions.
 -}
 
-type RoleEnv    = NameEnv [Role]        -- from tycon names to roles
+type RolesInfo = Name -> [Role]
+
+type RoleEnv = NameEnv [Role]        -- from tycon names to roles
 
 -- This, and any of the functions it calls, must *not* look at the roles
 -- field of a tycon we are inferring roles about!
 -- See Note [Role inference]
-inferRoles :: Bool -> RoleAnnots -> [TyCon] -> Name -> [Role]
-inferRoles is_boot annots tycons
-  = let role_env  = initialRoleEnv is_boot annots tycons
+inferRoles :: HscSource -> RoleAnnotEnv -> [TyCon] -> Name -> [Role]
+inferRoles hsc_src annots tycons
+  = let role_env  = initialRoleEnv hsc_src annots tycons
         role_env' = irGroup role_env tycons in
     \name -> case lookupNameEnv role_env' name of
       Just roles -> roles
       Nothing    -> pprPanic "inferRoles" (ppr name)
 
-initialRoleEnv :: Bool -> RoleAnnots -> [TyCon] -> RoleEnv
-initialRoleEnv is_boot annots = extendNameEnvList emptyNameEnv .
-                                map (initialRoleEnv1 is_boot annots)
+initialRoleEnv :: HscSource -> RoleAnnotEnv -> [TyCon] -> RoleEnv
+initialRoleEnv hsc_src annots = extendNameEnvList emptyNameEnv .
+                                map (initialRoleEnv1 hsc_src annots)
 
-initialRoleEnv1 :: Bool -> RoleAnnots -> TyCon -> (Name, [Role])
-initialRoleEnv1 is_boot annots_env tc
-  | isFamilyTyCon tc      = (name, map (const Nominal) tyvars)
+initialRoleEnv1 :: HscSource -> RoleAnnotEnv -> TyCon -> (Name, [Role])
+initialRoleEnv1 hsc_src annots_env tc
+  | isFamilyTyCon tc      = (name, map (const Nominal) bndrs)
   | isAlgTyCon tc         = (name, default_roles)
   | isTypeSynonymTyCon tc = (name, default_roles)
   | otherwise             = pprPanic "initialRoleEnv1" (ppr tc)
   where name         = tyConName tc
-        tyvars       = tyConTyVars tc
-        (kvs, tvs)   = span isKindVar tyvars
+        bndrs        = tyConBinders tc
+        argflags     = map tyConBinderArgFlag bndrs
+        num_exps     = count isVisibleArgFlag argflags
 
           -- if the number of annotations in the role annotation decl
           -- is wrong, just ignore it. We check this in the validity check.
         role_annots
-          = case lookupNameEnv annots_env name of
-              Just (L _ (RoleAnnotDecl _ annots))
-                | annots `equalLength` tvs -> map unLoc annots
-              _                            -> map (const Nothing) tvs
-        default_roles = map (const Nominal) kvs ++
-                        zipWith orElse role_annots (repeat default_role)
+          = case lookupRoleAnnot annots_env name of
+              Just (dL->L _ (RoleAnnotDecl _ _ annots))
+                | annots `lengthIs` num_exps -> map unLoc annots
+              _                              -> replicate num_exps Nothing
+        default_roles = build_default_roles argflags role_annots
+
+        build_default_roles (argf : argfs) (m_annot : ras)
+          | isVisibleArgFlag argf
+          = (m_annot `orElse` default_role) : build_default_roles argfs ras
+        build_default_roles (_argf : argfs) ras
+          = Nominal : build_default_roles argfs ras
+        build_default_roles [] [] = []
+        build_default_roles _ _ = pprPanic "initialRoleEnv1 (2)"
+                                           (vcat [ppr tc, ppr role_annots])
 
         default_role
           | isClassTyCon tc               = Nominal
-          | is_boot && isAbstractTyCon tc = Representational
+          -- Note [Default roles for abstract TyCons in hs-boot/hsig]
+          | HsBootFile <- hsc_src
+          , isAbstractTyCon tc            = Representational
+          | HsigFile   <- hsc_src
+          , isAbstractTyCon tc            = Nominal
           | otherwise                     = Phantom
 
+-- Note [Default roles for abstract TyCons in hs-boot/hsig]
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+-- What should the default role for an abstract TyCon be?
+--
+-- Originally, we inferred phantom role for abstract TyCons
+-- in hs-boot files, because the type variables were never used.
+--
+-- This was silly, because the role of the abstract TyCon
+-- was required to match the implementation, and the roles of
+-- data types are almost never phantom.  Thus, in ticket #9204,
+-- the default was changed so be representational (the most common case).  If
+-- the implementing data type was actually nominal, you'd get an easy
+-- to understand error, and add the role annotation yourself.
+--
+-- Then Backpack was added, and with it we added role *subtyping*
+-- the matching judgment: if an abstract TyCon has a nominal
+-- parameter, it's OK to implement it with a representational
+-- parameter.  But now, the representational default is not a good
+-- one, because you should *only* request representational if
+-- you're planning to do coercions. To be maximally flexible
+-- with what data types you will accept, you want the default
+-- for hsig files is nominal.  We don't allow role subtyping
+-- with hs-boot files (it's good practice to give an exactly
+-- accurate role here, because any types that use the abstract
+-- type will propagate the role information.)
+
 irGroup :: RoleEnv -> [TyCon] -> RoleEnv
 irGroup env tcs
   = let (env', update) = runRoleM env $ mapM_ irTyCon tcs in
@@ -657,63 +548,98 @@ irTyCon tc
   = do { old_roles <- lookupRoles tc
        ; unless (all (== Nominal) old_roles) $  -- also catches data families,
                                                 -- which don't want or need role inference
-    do { whenIsJust (tyConClass_maybe tc) (irClass tc_name)
-       ; addRoleInferenceInfo tc_name (tyConTyVars tc) $
-         mapM_ (irType emptyVarSet) (tyConStupidTheta tc)  -- See #8958
-       ; mapM_ (irDataCon tc_name) (visibleDataCons $ algTyConRhs tc) }}
+         irTcTyVars tc $
+         do { mapM_ (irType emptyVarSet) (tyConStupidTheta tc)  -- See #8958
+            ; whenIsJust (tyConClass_maybe tc) irClass
+            ; mapM_ irDataCon (visibleDataCons $ algTyConRhs tc) }}
 
   | Just ty <- synTyConRhs_maybe tc
-  = addRoleInferenceInfo tc_name (tyConTyVars tc) $
+  = irTcTyVars tc $
     irType emptyVarSet ty
 
   | otherwise
   = return ()
 
-  where
-    tc_name = tyConName tc
-
 -- any type variable used in an associated type must be Nominal
-irClass :: Name -> Class -> RoleM ()
-irClass tc_name cls
-  = addRoleInferenceInfo tc_name cls_tvs $
-    mapM_ ir_at (classATs cls)
+irClass :: Class -> RoleM ()
+irClass cls
+  = mapM_ ir_at (classATs cls)
   where
     cls_tvs    = classTyVars cls
     cls_tv_set = mkVarSet cls_tvs
 
     ir_at at_tc
-      = mapM_ (updateRole Nominal) (varSetElems nvars)
-      where nvars = (mkVarSet $ tyConTyVars at_tc) `intersectVarSet` cls_tv_set
+      = mapM_ (updateRole Nominal) nvars
+      where nvars = filter (`elemVarSet` cls_tv_set) $ tyConTyVars at_tc
 
 -- See Note [Role inference]
-irDataCon :: Name -> DataCon -> RoleM ()
-irDataCon tc_name datacon
-  = addRoleInferenceInfo tc_name univ_tvs $
-    mapM_ (irType ex_var_set) (eqSpecPreds eq_spec ++ theta ++ arg_tys)
+irDataCon :: DataCon -> RoleM ()
+irDataCon datacon
+  = setRoleInferenceVars univ_tvs $
+    irExTyVars ex_tvs $ \ ex_var_set ->
+    mapM_ (irType ex_var_set)
+          (map tyVarKind ex_tvs ++ eqSpecPreds eq_spec ++ theta ++ arg_tys)
       -- See Note [Role-checking data constructor arguments]
   where
-    (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _res_ty) = dataConFullSig datacon
-    ex_var_set = mkVarSet ex_tvs
+    (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _res_ty)
+      = dataConFullSig datacon
 
 irType :: VarSet -> Type -> RoleM ()
 irType = go
   where
-    go lcls (TyVarTy tv) = unless (tv `elemVarSet` lcls) $
-                           updateRole Representational tv
-    go lcls (AppTy t1 t2) = go lcls t1 >> mark_nominal lcls t2
-    go lcls (TyConApp tc tys)
-      = do { roles <- lookupRolesX tc
-           ; zipWithM_ (go_app lcls) roles tys }
-    go lcls (FunTy t1 t2) = go lcls t1 >> go lcls t2
-    go lcls (ForAllTy tv ty) = go (extendVarSet lcls tv) ty
-    go _    (LitTy {}) = return ()
+    go lcls ty                 | Just ty' <- coreView ty -- #14101
+                               = go lcls ty'
+    go lcls (TyVarTy tv)       = unless (tv `elemVarSet` lcls) $
+                                 updateRole Representational tv
+    go lcls (AppTy t1 t2)      = go lcls t1 >> markNominal lcls t2
+    go lcls (TyConApp tc tys)  = do { roles <- lookupRolesX tc
+                                    ; zipWithM_ (go_app lcls) roles tys }
+    go lcls (ForAllTy tvb ty)  = do { let tv = binderVar tvb
+                                          lcls' = extendVarSet lcls tv
+                                    ; markNominal lcls (tyVarKind tv)
+                                    ; go lcls' ty }
+    go lcls (FunTy arg res)    = go lcls arg >> go lcls res
+    go _    (LitTy {})         = return ()
+      -- See Note [Coercions in role inference]
+    go lcls (CastTy ty _)      = go lcls ty
+    go _    (CoercionTy _)     = return ()
 
     go_app _ Phantom _ = return ()                 -- nothing to do here
-    go_app lcls Nominal ty = mark_nominal lcls ty  -- all vars below here are N
+    go_app lcls Nominal ty = markNominal lcls ty  -- all vars below here are N
     go_app lcls Representational ty = go lcls ty
 
-    mark_nominal lcls ty = let nvars = tyVarsOfType ty `minusVarSet` lcls in
-                           mapM_ (updateRole Nominal) (varSetElems nvars)
+irTcTyVars :: TyCon -> RoleM a -> RoleM a
+irTcTyVars tc thing
+  = setRoleInferenceTc (tyConName tc) $ go (tyConTyVars tc)
+  where
+    go []       = thing
+    go (tv:tvs) = do { markNominal emptyVarSet (tyVarKind tv)
+                     ; addRoleInferenceVar tv $ go tvs }
+
+irExTyVars :: [TyVar] -> (TyVarSet -> RoleM a) -> RoleM a
+irExTyVars orig_tvs thing = go emptyVarSet orig_tvs
+  where
+    go lcls []       = thing lcls
+    go lcls (tv:tvs) = do { markNominal lcls (tyVarKind tv)
+                          ; go (extendVarSet lcls tv) tvs }
+
+markNominal :: TyVarSet   -- local variables
+            -> Type -> RoleM ()
+markNominal lcls ty = let nvars = fvVarList (FV.delFVs lcls $ get_ty_vars ty) in
+                      mapM_ (updateRole Nominal) nvars
+  where
+     -- get_ty_vars gets all the tyvars (no covars!) from a type *without*
+     -- recurring into coercions. Recall: coercions are totally ignored during
+     -- role inference. See [Coercions in role inference]
+    get_ty_vars :: Type -> FV
+    get_ty_vars (TyVarTy tv)      = unitFV tv
+    get_ty_vars (AppTy t1 t2)     = get_ty_vars t1 `unionFV` get_ty_vars t2
+    get_ty_vars (FunTy t1 t2)     = get_ty_vars t1 `unionFV` get_ty_vars t2
+    get_ty_vars (TyConApp _ tys)  = mapUnionFV get_ty_vars tys
+    get_ty_vars (ForAllTy tvb ty) = tyCoFVsBndr tvb (get_ty_vars ty)
+    get_ty_vars (LitTy {})        = emptyFV
+    get_ty_vars (CastTy ty _)     = get_ty_vars ty
+    get_ty_vars (CoercionTy _)    = emptyFV
 
 -- like lookupRoles, but with Nominal tags at the end for oversaturated TyConApps
 lookupRolesX :: TyCon -> RoleM [Role]
@@ -733,11 +659,10 @@ lookupRoles tc
 updateRole :: Role -> TyVar -> RoleM ()
 updateRole role tv
   = do { var_ns <- getVarNs
+       ; name <- getTyConName
        ; case lookupVarEnv var_ns tv of
-       { Nothing -> pprPanic "updateRole" (ppr tv)
-       ; Just n  -> do
-       { name <- getTyConName
-       ; updateRoleEnv name n role }}}
+           Nothing -> pprPanic "updateRole" (ppr name $$ ppr tv $$ ppr var_ns)
+           Just n  -> updateRoleEnv name n role }
 
 -- the state in the RoleM monad
 data RoleInferenceState = RIS { role_env  :: RoleEnv
@@ -745,11 +670,11 @@ data RoleInferenceState = RIS { role_env  :: RoleEnv
 
 -- the environment in the RoleM monad
 type VarPositions = VarEnv Int
-data RoleInferenceInfo = RII { var_ns :: VarPositions
-                             , name   :: Name }
 
 -- See [Role inference]
-newtype RoleM a = RM { unRM :: Maybe RoleInferenceInfo
+newtype RoleM a = RM { unRM :: Maybe Name -- of the tycon
+                            -> VarPositions
+                            -> Int          -- size of VarPositions
                             -> RoleInferenceState
                             -> (a, RoleInferenceState) }
 
@@ -757,44 +682,56 @@ instance Functor RoleM where
     fmap = liftM
 
 instance Applicative RoleM where
-    pure x = RM $ \_ state -> (x, state)
+    pure x = RM $ \_ _ _ state -> (x, state)
     (<*>) = ap
 
 instance Monad RoleM where
-  return = pure
-  a >>= f  = RM $ \m_info state -> let (a', state') = unRM a m_info state in
-                                   unRM (f a') m_info state'
+  a >>= f  = RM $ \m_info vps nvps state ->
+                  let (a', state') = unRM a m_info vps nvps state in
+                  unRM (f a') m_info vps nvps state'
 
 runRoleM :: RoleEnv -> RoleM () -> (RoleEnv, Bool)
 runRoleM env thing = (env', update)
-  where RIS { role_env = env', update = update } = snd $ unRM thing Nothing state
-        state = RIS { role_env  = env, update    = False }
-
-addRoleInferenceInfo :: Name -> [TyVar] -> RoleM a -> RoleM a
-addRoleInferenceInfo name tvs thing
-  = RM $ \_nothing state -> ASSERT( isNothing _nothing )
-                            unRM thing (Just info) state
-  where info = RII { var_ns = mkVarEnv (zip tvs [0..]), name = name }
+  where RIS { role_env = env', update = update }
+          = snd $ unRM thing Nothing emptyVarEnv 0 state
+        state = RIS { role_env  = env
+                    , update    = False }
+
+setRoleInferenceTc :: Name -> RoleM a -> RoleM a
+setRoleInferenceTc name thing = RM $ \m_name vps nvps state ->
+                                ASSERT( isNothing m_name )
+                                ASSERT( isEmptyVarEnv vps )
+                                ASSERT( nvps == 0 )
+                                unRM thing (Just name) vps nvps state
+
+addRoleInferenceVar :: TyVar -> RoleM a -> RoleM a
+addRoleInferenceVar tv thing
+  = RM $ \m_name vps nvps state ->
+    ASSERT( isJust m_name )
+    unRM thing m_name (extendVarEnv vps tv nvps) (nvps+1) state
+
+setRoleInferenceVars :: [TyVar] -> RoleM a -> RoleM a
+setRoleInferenceVars tvs thing
+  = RM $ \m_name _vps _nvps state ->
+    ASSERT( isJust m_name )
+    unRM thing m_name (mkVarEnv (zip tvs [0..])) (panic "setRoleInferenceVars")
+         state
 
 getRoleEnv :: RoleM RoleEnv
-getRoleEnv = RM $ \_ state@(RIS { role_env = env }) -> (env, state)
+getRoleEnv = RM $ \_ _ _ state@(RIS { role_env = env }) -> (env, state)
 
 getVarNs :: RoleM VarPositions
-getVarNs = RM $ \m_info state ->
-                case m_info of
-                  Nothing -> panic "getVarNs"
-                  Just (RII { var_ns = var_ns }) -> (var_ns, state)
+getVarNs = RM $ \_ vps _ state -> (vps, state)
 
 getTyConName :: RoleM Name
-getTyConName = RM $ \m_info state ->
-                    case m_info of
-                      Nothing -> panic "getTyConName"
-                      Just (RII { name = name }) -> (name, state)
-
+getTyConName = RM $ \m_name _ _ state ->
+                    case m_name of
+                      Nothing   -> panic "getTyConName"
+                      Just name -> (name, state)
 
 updateRoleEnv :: Name -> Int -> Role -> RoleM ()
 updateRoleEnv name n role
-  = RM $ \_ state@(RIS { role_env = role_env }) -> ((),
+  = RM $ \_ _ _ state@(RIS { role_env = role_env }) -> ((),
          case lookupNameEnv role_env name of
            Nothing -> pprPanic "updateRoleEnv" (ppr name)
            Just roles -> let (before, old_role : after) = splitAt n roles in
@@ -811,20 +748,52 @@ updateRoleEnv name n role
 *                                                                      *
 ********************************************************************* -}
 
-tcAddImplicits :: [TyThing] -> TcM TcGblEnv
-tcAddImplicits tyclss
-  = discardWarnings $
+addTyConsToGblEnv :: [TyCon] -> TcM TcGblEnv
+-- Given a [TyCon], add to the TcGblEnv
+--   * extend the TypeEnv with the tycons
+--   * extend the TypeEnv with their implicitTyThings
+--   * extend the TypeEnv with any default method Ids
+--   * add bindings for record selectors
+addTyConsToGblEnv tyclss
+  = tcExtendTyConEnv tyclss                    $
     tcExtendGlobalEnvImplicit implicit_things  $
     tcExtendGlobalValEnv def_meth_ids          $
-    do { (typeable_ids, typeable_binds) <- mkTypeableBinds tycons
-       ; gbl_env <- tcExtendGlobalValEnv typeable_ids
-                    $ tcRecSelBinds $ mkRecSelBinds tycons
-       ; return (gbl_env `addTypecheckedBinds` typeable_binds) }
+    do { traceTc "tcAddTyCons" $ vcat
+            [ text "tycons" <+> ppr tyclss
+            , text "implicits" <+> ppr implicit_things ]
+       ; gbl_env <- tcRecSelBinds (mkRecSelBinds tyclss)
+       ; return gbl_env }
  where
-   implicit_things = concatMap implicitTyThings tyclss
-   tycons          = [tc | ATyCon tc <- tyclss]
+   implicit_things = concatMap implicitTyConThings tyclss
    def_meth_ids    = mkDefaultMethodIds tyclss
 
+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
+  = [ mkExportedVanillaId dm_name (mkDefaultMethodType cls sel_id dm_spec)
+    | tc <- tycons
+    , Just cls <- [tyConClass_maybe tc]
+    , (sel_id, Just (dm_name, dm_spec)) <- classOpItems cls ]
+
+mkDefaultMethodType :: Class -> Id -> DefMethSpec Type -> Type
+-- Returns the top-level type of the default method
+mkDefaultMethodType _ sel_id VanillaDM        = idType sel_id
+mkDefaultMethodType cls _   (GenericDM dm_ty) = mkSigmaTy tv_bndrs [pred] dm_ty
+   where
+     pred      = mkClassPred cls (mkTyVarTys (binderVars cls_bndrs))
+     cls_bndrs = tyConBinders (classTyCon cls)
+     tv_bndrs  = tyConTyVarBinders cls_bndrs
+     -- NB: the Class doesn't have TyConBinders; we reach into its
+     --     TyCon to get those.  We /do/ need the TyConBinders because
+     --     we need the correct visibility: these default methods are
+     --     used in code generated by the fill-in for missing
+     --     methods in instances (TcInstDcls.mkDefMethBind), and
+     --     then typechecked.  So we need the right visibilty info
+     --     (Trac #13998)
+
 {-
 ************************************************************************
 *                                                                      *
@@ -833,14 +802,6 @@ 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]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -859,30 +820,45 @@ must bring the default method Ids into scope first (so they can be seen
 when typechecking the [d| .. |] quote, and typecheck them later.
 -}
 
-mkRecSelBinds :: [TyCon] -> HsValBinds Name
+{-
+************************************************************************
+*                                                                      *
+                Building record selectors
+*                                                                      *
+************************************************************************
+-}
+
+tcRecSelBinds :: [(Id, LHsBind GhcRn)] -> TcM TcGblEnv
+tcRecSelBinds sel_bind_prs
+  = tcExtendGlobalValEnv [sel_id | (dL->L _ (IdSig _ sel_id)) <- sigs] $
+    do { (rec_sel_binds, tcg_env) <- discardWarnings $
+                                     tcValBinds TopLevel binds sigs getGblEnv
+       ; return (tcg_env `addTypecheckedBinds` map snd rec_sel_binds) }
+  where
+    sigs = [ cL loc (IdSig noExt sel_id)   | (sel_id, _) <- sel_bind_prs
+                                          , let loc = getSrcSpan sel_id ]
+    binds = [(NonRecursive, unitBag bind) | (_, bind) <- sel_bind_prs]
+
+mkRecSelBinds :: [TyCon] -> [(Id, LHsBind GhcRn)]
 -- NB We produce *un-typechecked* bindings, rather like 'deriving'
 --    This makes life easier, because the later type checking will add
 --    all necessary type abstractions and applications
 mkRecSelBinds tycons
-  = ValBindsOut binds sigs
-  where
-    (sigs, binds) = unzip rec_sels
-    rec_sels = map mkRecSelBind [ (tc,fld)
-                                | tc <- tycons
+  = map mkRecSelBind [ (tc,fld) | tc <- tycons
                                 , fld <- tyConFieldLabels tc ]
 
-mkRecSelBind :: (TyCon, FieldLabel) -> (LSig Name, (RecFlag, LHsBinds Name))
+mkRecSelBind :: (TyCon, FieldLabel) -> (Id, LHsBind GhcRn)
 mkRecSelBind (tycon, fl)
   = mkOneRecordSelector all_cons (RecSelData tycon) fl
   where
-    all_cons     = map RealDataCon (tyConDataCons tycon)
+    all_cons = map RealDataCon (tyConDataCons tycon)
 
 mkOneRecordSelector :: [ConLike] -> RecSelParent -> FieldLabel
-                    -> (LSig Name, (RecFlag, LHsBinds Name))
+                    -> (Id, LHsBind GhcRn)
 mkOneRecordSelector all_cons idDetails fl
-  = (L loc (IdSig sel_id), (NonRecursive, unitBag (L loc sel_bind)))
+  = (sel_id, cL loc sel_bind)
   where
-    loc    = getSrcSpan sel_name
+    loc      = getSrcSpan sel_name
     lbl      = flLabel fl
     sel_name = flSelector fl
 
@@ -895,45 +871,52 @@ mkOneRecordSelector all_cons idDetails fl
 
     -- Selector type; Note [Polymorphic selectors]
     field_ty   = conLikeFieldType con1 lbl
-    data_tvs   = tyVarsOfType data_ty
-    is_naughty = not (tyVarsOfType field_ty `subVarSet` data_tvs)
+    data_tvs   = tyCoVarsOfTypesWellScoped inst_tys
+    data_tv_set= mkVarSet data_tvs
+    is_naughty = not (tyCoVarsOfType field_ty `subVarSet` data_tv_set)
     (field_tvs, field_theta, field_tau) = tcSplitSigmaTy field_ty
     sel_ty | is_naughty = unitTy  -- See Note [Naughty record selectors]
-           | otherwise  = mkForAllTys (varSetElemsKvsFirst $
-                                       data_tvs `extendVarSetList` field_tvs) $
+           | otherwise  = mkSpecForAllTys data_tvs          $
                           mkPhiTy (conLikeStupidTheta con1) $   -- Urgh!
-                          mkPhiTy field_theta               $   -- Urgh!
+                          mkFunTy data_ty                   $
+                          mkSpecForAllTys field_tvs         $
+                          mkPhiTy field_theta               $
                           -- req_theta is empty for normal DataCon
                           mkPhiTy req_theta                 $
-                          mkFunTy data_ty field_tau
+                          field_tau
 
     -- Make the binding: sel (C2 { fld = x }) = x
     --                   sel (C7 { fld = x }) = x
     --    where cons_w_field = [C2,C7]
     sel_bind = mkTopFunBind Generated sel_lname alts
       where
-        alts | is_naughty = [mkSimpleMatch [] unit_rhs]
+        alts | is_naughty = [mkSimpleMatch (mkPrefixFunRhs sel_lname)
+                                           [] unit_rhs]
              | otherwise =  map mk_match cons_w_field ++ deflt
-    mk_match con = mkSimpleMatch [L loc (mk_sel_pat con)]
-                                 (L loc (HsVar (L loc field_var)))
-    mk_sel_pat con = ConPatIn (L loc (getName con)) (RecCon rec_fields)
+    mk_match con = mkSimpleMatch (mkPrefixFunRhs sel_lname)
+                                 [cL loc (mk_sel_pat con)]
+                                 (cL loc (HsVar noExt (cL loc field_var)))
+    mk_sel_pat con = ConPatIn (cL loc (getName con)) (RecCon rec_fields)
     rec_fields = HsRecFields { rec_flds = [rec_field], rec_dotdot = Nothing }
     rec_field  = noLoc (HsRecField
-                        { hsRecFieldLbl = L loc (FieldOcc (mkVarUnqual lbl)
-                                                 sel_name)
-                        , hsRecFieldArg = L loc (VarPat (L loc field_var))
+                        { hsRecFieldLbl
+                           = cL loc (FieldOcc sel_name
+                                     (cL loc $ mkVarUnqual lbl))
+                        , hsRecFieldArg
+                           = cL loc (VarPat noExt (cL loc field_var))
                         , hsRecPun = False })
-    sel_lname = L loc sel_name
+    sel_lname = cL loc sel_name
     field_var = mkInternalName (mkBuiltinUnique 1) (getOccName sel_name) loc
 
     -- Add catch-all default case unless the case is exhaustive
     -- We do this explicitly so that we get a nice error message that
     -- mentions this particular record selector
     deflt | all dealt_with all_cons = []
-          | otherwise = [mkSimpleMatch [L loc (WildPat placeHolderType)]
-                            (mkHsApp (L loc (HsVar
-                                            (L loc (getName rEC_SEL_ERROR_ID))))
-                                     (L loc (HsLit msg_lit)))]
+          | otherwise = [mkSimpleMatch CaseAlt
+                            [cL loc (WildPat noExt)]
+                            (mkHsApp (cL loc (HsVar noExt
+                                         (cL loc (getName rEC_SEL_ERROR_ID))))
+                                     (cL loc (HsLit noExt msg_lit)))]
 
         -- Do not add a default case unless there are unmatched
         -- constructors.  We must take account of GADTs, else we
@@ -951,22 +934,23 @@ mkOneRecordSelector all_cons idDetails fl
 
     (univ_tvs, _, eq_spec, _, req_theta, _, data_ty) = conLikeFullSig con1
 
-    inst_tys = substTyVars (mkTopTvSubst eq_spec) univ_tvs
+    eq_subst = mkTvSubstPrs (map eqSpecPair eq_spec)
+    inst_tys = substTyVars eq_subst univ_tvs
 
     unit_rhs = mkLHsTupleExpr []
-    msg_lit = HsStringPrim "" (fastStringToByteString lbl)
+    msg_lit = HsStringPrim NoSourceText (bytesFS lbl)
 
 {-
 Note [Polymorphic selectors]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When a record has a polymorphic field, we pull the foralls out to the front.
-   data T = MkT { f :: forall a. [a] -> a }
-Then f :: forall a. T -> [a] -> a
-NOT  f :: T -> forall a. [a] -> a
+We take care to build the type of a polymorphic selector in the right
+order, so that visible type application works.
+
+  data Ord a => T a = MkT { field :: forall b. (Num a, Show b) => (a, b) }
+
+We want
 
-This is horrid.  It's only needed in deeply obscure cases, which I hate.
-The only case I know is test tc163, which is worth looking at.  It's far
-from clear that this test should succeed at all!
+  field :: forall a. Ord a => T a -> forall b. (Num a, Show b) => (a, b)
 
 Note [Naughty record selectors]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -987,9 +971,9 @@ like     sel :: T [a] -> a
 
 For naughty selectors we make a dummy binding
    sel = ()
-for naughty selectors, so that the later type-check will add them to the
-environment, and they'll be exported.  The function is never called, because
-the tyepchecker spots the sel_naughty field.
+so that the later type-check will add them to the environment, and they'll be
+exported.  The function is never called, because the typechecker spots the
+sel_naughty field.
 
 Note [GADT record selectors]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~