Small refactoringsghc-axioms

 - Define mkAxInstRHS and use it
 - Rename Instance to ClsInst

13 files changed, 167 insertions, 175 deletions

diff --git a/compiler/basicTypes/MkId.lhs b/compiler/basicTypes/MkId.lhs
index f3922fe40b..60f4cf16ae 100644
--- a/compiler/basicTypes/MkId.lhs
+++ b/compiler/basicTypes/MkId.lhs
@@ -228,7 +228,7 @@ mkDataConIds wrap_name wkr_name data_con
   = DCIds Nothing nt_work_id                 
 
   | any isBanged all_strict_marks      -- Algebraic, needs wrapper
-    || not (null eq_spec)              -- NB: LoadIface.ifaceDeclSubBndrs
+    || not (null eq_spec)              -- NB: LoadIface.ifaceDeclImplicitBndrs
     || isFamInstTyCon tycon            --     depends on this test
   = DCIds (Just alg_wrap_id) wrk_id
 
diff --git a/compiler/basicTypes/Var.lhs b/compiler/basicTypes/Var.lhs
index d7caf2a521..ea8e9d2622 100644
--- a/compiler/basicTypes/Var.lhs
+++ b/compiler/basicTypes/Var.lhs
@@ -85,7 +85,7 @@ import FastTypes
 import FastString
 import Outputable
 
-import StaticFlags ( opt_SuppressVarKinds )
+-- import StaticFlags ( opt_SuppressVarKinds )
 
 import Data.Data
 \end{code}
@@ -211,9 +211,11 @@ After CoreTidy, top-level LocalIds are turned into GlobalIds
 
 \begin{code}
 instance Outputable Var where
-  ppr var = ifPprDebug (text "(") <+> ppr (varName var) <+> ifPprDebug (brackets (ppr_debug var))
-            <+> if (not opt_SuppressVarKinds) then ifPprDebug (text "::" <+> ppr (tyVarKind var) <+> text ")")
-                else empty
+  ppr var = ppr (varName var) <+> ifPprDebug (brackets (ppr_debug var))
+-- Printing the type on every occurrence is too much!
+--            <+> if (not opt_SuppressVarKinds)
+--                then ifPprDebug (text "::" <+> ppr (tyVarKind var) <+> text ")")
+--                else empty
 
 ppr_debug :: Var -> SDoc
 ppr_debug (TyVar {})                           = ptext (sLit "tv")
diff --git a/compiler/iface/IfaceSyn.lhs b/compiler/iface/IfaceSyn.lhs
index 08a98af2f5..fd8b361b3d 100644
--- a/compiler/iface/IfaceSyn.lhs
+++ b/compiler/iface/IfaceSyn.lhs
@@ -23,7 +23,7 @@ module IfaceSyn (
         IfaceClsInst(..), IfaceFamInst(..), IfaceTickish(..),
 
         -- Misc
-        ifaceDeclSubBndrs, visibleIfConDecls,
+        ifaceDeclImplicitBndrs, visibleIfConDecls,
 
         -- Free Names
         freeNamesIfDecl, freeNamesIfRule, freeNamesIfFamInst,
@@ -374,20 +374,21 @@ See [http://hackage.haskell.org/trac/ghc/wiki/Commentary/Compiler/RecompilationA
 -- -----------------------------------------------------------------------------
 -- Utils on IfaceSyn
 
-ifaceDeclSubBndrs :: IfaceDecl -> [OccName]
+ifaceDeclImplicitBndrs :: IfaceDecl -> [OccName]
 --  *Excludes* the 'main' name, but *includes* the implicitly-bound names
 -- Deeply revolting, because it has to predict what gets bound,
 -- especially the question of whether there's a wrapper for a datacon
+-- See Note [Implicit TyThings] in HscTypes
 
 -- N.B. the set of names returned here *must* match the set of
 -- TyThings returned by HscTypes.implicitTyThings, in the sense that
 -- TyThing.getOccName should define a bijection between the two lists.
 -- This invariant is used in LoadIface.loadDecl (see note [Tricky iface loop])
 -- The order of the list does not matter.
-ifaceDeclSubBndrs IfaceData {ifCons = IfAbstractTyCon {}}  = []
+ifaceDeclImplicitBndrs IfaceData {ifCons = IfAbstractTyCon {}}  = []
 
 -- Newtype
-ifaceDeclSubBndrs (IfaceData {ifName = tc_occ,
+ifaceDeclImplicitBndrs (IfaceData {ifName = tc_occ,
                               ifCons = IfNewTyCon (
                                         IfCon { ifConOcc = con_occ })})
   =   -- implicit newtype coercion
@@ -396,7 +397,7 @@ ifaceDeclSubBndrs (IfaceData {ifName = tc_occ,
     [con_occ, mkDataConWorkerOcc con_occ]
 
 
-ifaceDeclSubBndrs (IfaceData {ifName = _tc_occ,
+ifaceDeclImplicitBndrs (IfaceData {ifName = _tc_occ,
                               ifCons = IfDataTyCon cons })
   = -- for each data constructor in order,
     --    data constructor, worker, and (possibly) wrapper
@@ -412,7 +413,7 @@ ifaceDeclSubBndrs (IfaceData {ifName = _tc_occ,
           has_wrapper = ifConWrapper con_decl     -- This is the reason for
                                                   -- having the ifConWrapper field!
 
-ifaceDeclSubBndrs (IfaceClass {ifCtxt = sc_ctxt, ifName = cls_tc_occ,
+ifaceDeclImplicitBndrs (IfaceClass {ifCtxt = sc_ctxt, ifName = cls_tc_occ,
                                ifSigs = sigs, ifATs = ats })
   = --   (possibly) newtype coercion
     co_occs ++
@@ -435,7 +436,7 @@ ifaceDeclSubBndrs (IfaceClass {ifCtxt = sc_ctxt, ifName = cls_tc_occ,
     dc_occ = mkClassDataConOcc cls_tc_occ
     is_newtype = n_sigs + n_ctxt == 1 -- Sigh
 
-ifaceDeclSubBndrs _ = []
+ifaceDeclImplicitBndrs _ = []
 
 ----------------------------- Printing IfaceDecl ------------------------------
 
diff --git a/compiler/iface/LoadIface.lhs b/compiler/iface/LoadIface.lhs
index a685bb77e1..ec1205f83d 100644
--- a/compiler/iface/LoadIface.lhs
+++ b/compiler/iface/LoadIface.lhs
@@ -372,7 +372,7 @@ loadDecl ignore_prags mod (_version, decl)
                 -- the names associated with the decl
           main_name      <- lookupOrig mod (ifName decl)
 --        ; traceIf (text "Loading decl for " <> ppr main_name)
-        ; implicit_names <- mapM (lookupOrig mod) (ifaceDeclSubBndrs decl)
+        ; implicit_names <- mapM (lookupOrig mod) (ifaceDeclImplicitBndrs decl)
 
         -- Typecheck the thing, lazily
         -- NB. Firstly, the laziness is there in case we never need the
@@ -402,7 +402,7 @@ loadDecl ignore_prags mod (_version, decl)
         -- (where the "MkT" is the *Name* associated with MkT, etc.)
         --
         -- We do this by mapping the implict_names to the associated
-        -- TyThings.  By the invariant on ifaceDeclSubBndrs and
+        -- TyThings.  By the invariant on ifaceDeclImplicitBndrs and
         -- implicitTyThings, we can use getOccName on the implicit
         -- TyThings to make this association: each Name's OccName should
         -- be the OccName of exactly one implictTyThing.  So the key is
diff --git a/compiler/iface/TcIface.lhs b/compiler/iface/TcIface.lhs
index 524cb1f63a..570a6315cc 100644
--- a/compiler/iface/TcIface.lhs
+++ b/compiler/iface/TcIface.lhs
@@ -529,7 +529,12 @@ tc_iface_decl _ _ (IfaceAxiom {ifName = tc_occ, ifTyVars = tv_bndrs,
     { tc_name <- lookupIfaceTop tc_occ
     ; tc_lhs  <- tcIfaceType lhs
     ; tc_rhs  <- tcIfaceType rhs
-    ; let axiom = mkCoAxiom (nameUnique tc_name) tc_name tvs tc_lhs tc_rhs
+    ; let axiom = CoAxiom { co_ax_unique   = nameUnique tc_name
+                          , co_ax_name     = tc_name
+                          , co_ax_implicit = False
+                          , co_ax_tvs      = tvs
+                          , co_ax_lhs      = tc_lhs
+                          , co_ax_rhs      = tc_rhs }
     ; return (ACoAxiom axiom) }
 
 tcIfaceDataCons :: Name -> TyCon -> [TyVar] -> IfaceConDecls -> IfL AlgTyConRhs
@@ -624,14 +629,9 @@ tcIfaceFamInst :: IfaceFamInst -> IfL FamInst
 tcIfaceFamInst (IfaceFamInst { ifFamInstFam = fam, ifFamInstTys = mb_tcs
                              , ifFamInstAxiom = axiom_name } )
     = do axiom' <- forkM (ptext (sLit "Axiom") <+> ppr axiom_name) $
-                     tcIfaceCoAxiom axiom_name
-         -- Derive the flavor from splitting the axiom
-         let flavor = case coAxiomSplitLHS axiom' of
-                        (tc,_) | isDataFamilyTyCon tc -> DataFamilyInst tc
-                               | otherwise            -> ASSERT( isSynFamilyTyCon tc )
-                                                         SynFamilyInst
-             mb_tcs' = map (fmap ifaceTyConName) mb_tcs
-         return (mkImportedFamInst fam mb_tcs' flavor axiom')
+                   tcIfaceCoAxiom axiom_name
+         let mb_tcs' = map (fmap ifaceTyConName) mb_tcs
+         return (mkImportedFamInst fam mb_tcs' axiom')
 \end{code}
 
 
diff --git a/compiler/main/HscTypes.lhs b/compiler/main/HscTypes.lhs
index b022a1c3e2..3eda19fba1 100644
--- a/compiler/main/HscTypes.lhs
+++ b/compiler/main/HscTypes.lhs
@@ -1163,10 +1163,34 @@ mkPrintUnqualified dflags env = (qual_name, qual_mod)
 
 %************************************************************************
 %*                                                                      *
-                TyThing
+                Implicit TyThings
 %*                                                                      *
 %************************************************************************
 
+Note [Implicit TyThings]
+~~~~~~~~~~~~~~~~~~~~~~~~
+  DEFINITION: An "implicit" TyThing is one that does not have its own
+  IfaceDecl in an interface file.  Instead, its binding in the type
+  environment is created as part of typechecking the IfaceDecl for
+  some other thing.
+
+Examples:
+  * All DataCons are implicit, because they are generated from the
+    IfaceDecl for the data/newtype.  Ditto class methods.
+
+  * Record selectors are *not* implicit, because they get their own
+    free-standing IfaceDecl.
+
+  * Associated data/type families are implicit because they are
+    included in the IfaceDecl of the parent class.  (NB: the
+    IfaceClass decl happens to use IfaceDecl recursively for the
+    associated types, but that's irrelevant here.)
+
+  * Dictionary function Ids are not implict.
+
+  * Axioms for newtypes are implicit (same as above), but axioms
+    for data/type family instances are *not* implicit (like DFunIds).
+
 \begin{code}
 -- | Determine the 'TyThing's brought into scope by another 'TyThing'
 -- /other/ than itself. For example, Id's don't have any implicit TyThings
@@ -1175,7 +1199,7 @@ mkPrintUnqualified dflags env = (qual_name, qual_mod)
 -- scope, just for a start!
 
 -- N.B. the set of TyThings returned here *must* match the set of
--- names returned by LoadIface.ifaceDeclSubBndrs, in the sense that
+-- names returned by LoadIface.ifaceDeclImplicitBndrs, in the sense that
 -- TyThing.getOccName should define a bijection between the two lists.
 -- This invariant is used in LoadIface.loadDecl (see note [Tricky iface loop])
 -- The order of the list does not matter.
@@ -1219,14 +1243,11 @@ implicitTyConThings tc
 extras_plus :: TyThing -> [TyThing]
 extras_plus thing = thing : implicitTyThings thing
 
--- For newtypes and indexed data types (and both),
--- add the implicit coercion tycon
+-- For newtypes (only) add the implicit coercion tycon
 implicitCoTyCon :: TyCon -> [TyThing]
 implicitCoTyCon tc
-  = map ACoAxiom . catMaybes $ [ -- Just if newtype, Nothing if not
-                                 newTyConCo_maybe tc
-                                 -- Just if family instance, Nothing if not
-                               {- , tyConFamilyCoercion_maybe tc -} ]
+  | Just co <- newTyConCo_maybe tc = [ACoAxiom co]
+  | otherwise                      = []
 
 -- | Returns @True@ if there should be no interface-file declaration
 -- for this thing on its own: either it is built-in, or it is part
@@ -1236,7 +1257,7 @@ isImplicitTyThing :: TyThing -> Bool
 isImplicitTyThing (ADataCon {}) = True
 isImplicitTyThing (AnId id)     = isImplicitId id
 isImplicitTyThing (ATyCon tc)   = isImplicitTyCon tc
-isImplicitTyThing (ACoAxiom _)  = False -- JPM even for newtypes!
+isImplicitTyThing (ACoAxiom ax) = isImplicitCoAxiom ax
 
 -- | tyThingParent_maybe x returns (Just p)
 -- when pprTyThingInContext sould print a declaration for p
@@ -1434,7 +1455,7 @@ mkIfaceHashCache pairs
   = \occ -> lookupOccEnv env occ
   where
     env = foldr add_decl emptyOccEnv pairs
-    add_decl (v,d) env0 = foldr add_imp env1 (ifaceDeclSubBndrs d)
+    add_decl (v,d) env0 = foldr add_imp env1 (ifaceDeclImplicitBndrs d)
       where
           decl_name = ifName d
           env1 = extendOccEnv env0 decl_name (decl_name, v)
diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index bb792c92c4..08086e4e56 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -21,10 +21,10 @@ import VarSet
 import Type
 import Unify
 import FamInstEnv
+import Coercion( mkAxInstRHS )
 
 import Id 
 import Var
-import VarEnv ( ) -- unitVarEnv, mkInScopeSet
 
 import TcType
 
@@ -1512,13 +1512,8 @@ doTopReact _inerts workItem@(CFunEqCan { cc_id = eqv, cc_flavor = fl
            Nothing -> return NoTopInt 
            Just (famInst, rep_tys)
              -> do { let coe_ax = famInstAxiom famInst
-                         rhs_ty = substTyWith (coAxiomTyVars coe_ax) rep_tys
-                                    (coAxiomRHS coe_ax)
-			    -- Eagerly expand away the type synonym on the
-			    -- RHS of a type function, so that it never
-			    -- appears in an error message
-                            -- See Note [Type synonym families] in TyCon
-                         coe = mkTcAxInstCo coe_ax rep_tys 
+                         rhs_ty = mkAxInstRHS coe_ax rep_tys
+                         coe    = mkTcAxInstCo coe_ax rep_tys 
                    ; case fl of
                        Wanted {} -> do { evc <- newEqVar fl rhs_ty xi -- Wanted version
                                        ; let eqv' = evc_the_evvar evc
diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs
index 7f86377c74..836c9e55cc 100644
--- a/compiler/types/Coercion.lhs
+++ b/compiler/types/Coercion.lhs
@@ -29,7 +29,8 @@ module Coercion (
 
 	-- ** Constructing coercions
         mkReflCo, mkCoVarCo, 
-        mkAxInstCo, mkPiCo, mkPiCos,
+        mkAxInstCo, mkAxInstRHS,
+        mkPiCo, mkPiCos,
         mkSymCo, mkTransCo, mkNthCo,
 	mkInstCo, mkAppCo, mkTyConAppCo, mkFunCo,
         mkForAllCo, mkUnsafeCo,
@@ -531,6 +532,8 @@ mkReflCo :: Type -> Coercion
 mkReflCo = Refl
 
 mkAxInstCo :: CoAxiom -> [Type] -> Coercion
+-- mkAxInstCo can legitimately be called over-staturated; 
+-- i.e. with more type arguments than the coercion requires
 mkAxInstCo ax tys
   | arity == n_tys = AxiomInstCo ax rtys
   | otherwise      = ASSERT( arity < n_tys )
@@ -541,6 +544,19 @@ mkAxInstCo ax tys
     arity = coAxiomArity ax
     rtys  = map Refl tys
 
+mkAxInstRHS :: CoAxiom -> [Type] -> Type
+-- Instantiate the axiom with specified types,
+-- returning the instantiated RHS
+-- A companion to mkAxInstCo: 
+--    mkAxInstRhs ax tys = snd (coercionKind (mkAxInstCo ax tys))
+mkAxInstRHS ax tys
+  = ASSERT( tvs `equalLength` tys1 ) 
+    mkAppTys rhs' tys2
+  where
+    tvs          = coAxiomTyVars ax
+    (tys1, tys2) = splitAtList tvs tys
+    rhs'         = substTyWith tvs tys1 (coAxiomRHS ax)
+
 -- | Apply a 'Coercion' to another 'Coercion'.
 mkAppCo :: Coercion -> Coercion -> Coercion
 mkAppCo (Refl ty1) (Refl ty2)       = Refl (mkAppTy ty1 ty2)
@@ -631,11 +647,12 @@ mkUnsafeCo ty1 ty2 = UnsafeCo ty1 ty2
 --   the free variables a subset of those 'TyVar's.
 mkNewTypeCo :: Name -> TyCon -> [TyVar] -> Type -> CoAxiom
 mkNewTypeCo name tycon tvs rhs_ty
-  = CoAxiom { co_ax_unique = nameUnique name
-            , co_ax_name   = name
-            , co_ax_tvs    = tvs
-            , co_ax_lhs    = mkTyConApp tycon (mkTyVarTys tvs)
-            , co_ax_rhs    = rhs_ty }
+  = CoAxiom { co_ax_unique   = nameUnique name
+            , co_ax_name     = name
+            , co_ax_implicit = True  -- See Note [Implicit axioms] in TyCon
+            , co_ax_tvs      = tvs
+            , co_ax_lhs      = mkTyConApp tycon (mkTyVarTys tvs)
+            , co_ax_rhs      = rhs_ty }
 
 mkPiCos :: [Var] -> Coercion -> Coercion
 mkPiCos vs co = foldr mkPiCo co vs
diff --git a/compiler/types/FamInstEnv.lhs b/compiler/types/FamInstEnv.lhs
index 262402540e..f103b6439a 100644
--- a/compiler/types/FamInstEnv.lhs
+++ b/compiler/types/FamInstEnv.lhs
@@ -17,7 +17,7 @@ module FamInstEnv (
         famInstsRepTyCons, famInstRepTyCon_maybe, dataFamInstRepTyCon, 
         famInstLHS,
 	pprFamInst, pprFamInstHdr, pprFamInsts, 
-	mkLocalFamInst, mkSynFamInst, mkDataFamInst, mkImportedFamInst,
+	mkSynFamInst, mkDataFamInst, mkImportedFamInst,
 
 	FamInstEnvs, FamInstEnv, emptyFamInstEnv, emptyFamInstEnvs, 
 	extendFamInstEnv, overwriteFamInstEnv, extendFamInstEnvList, 
@@ -139,10 +139,11 @@ instance Outputable FamInst where
 pprFamInst :: FamInst -> SDoc
 pprFamInst famInst
   = hang (pprFamInstHdr famInst)
-       2 (vcat [ ifPprDebug (ptext (sLit "Coercion axiom:") <+> pp_ax)
+       2 (vcat [ ifPprDebug (ptext (sLit "Coercion axiom:") <+> ppr ax)
+               , ifPprDebug (ptext (sLit "RHS:") <+> ppr (coAxiomRHS ax))
                , ptext (sLit "--") <+> pprDefinedAt (getName famInst)])
   where
-    pp_ax = ppr (fi_axiom famInst)
+    ax = fi_axiom famInst
 
 pprFamInstHdr :: FamInst -> SDoc
 pprFamInstHdr (FamInst {fi_axiom = axiom, fi_flavor = flavor})
@@ -159,11 +160,11 @@ pprFamInstHdr (FamInst {fi_axiom = axiom, fi_flavor = flavor})
     pprHead = pprTypeApp fam_tc tys
     pprTyConSort = case flavor of
                      SynFamilyInst        -> ptext (sLit "type")
-                     DataFamilyInst tycon -> case () of
-                         _ | isDataTyCon     tycon -> ptext (sLit "data")
-                         _ | isNewTyCon      tycon -> ptext (sLit "newtype")
-                         _ | isAbstractTyCon tycon -> ptext (sLit "data")
-                         _ | otherwise             -> panic "pprTyConSort"
+                     DataFamilyInst tycon
+                       | isDataTyCon     tycon -> ptext (sLit "data")
+                       | isNewTyCon      tycon -> ptext (sLit "newtype")
+                       | isAbstractTyCon tycon -> ptext (sLit "data")
+                       | otherwise             -> ptext (sLit "WEIRD") <+> ppr tycon
 
 pprFamInsts :: [FamInst] -> SDoc
 pprFamInsts finsts = vcat (map pprFamInst finsts)
@@ -187,11 +188,12 @@ mkSynFamInst name tvs fam_tc inst_tys rep_ty
               fi_flavor = SynFamilyInst,
               fi_axiom  = axiom }
   where
-    axiom = CoAxiom { co_ax_unique = nameUnique name
-                    , co_ax_name   = name
-                    , co_ax_tvs    = tvs
-                    , co_ax_lhs    = mkTyConApp fam_tc inst_tys 
-                    , co_ax_rhs    = rep_ty }
+    axiom = CoAxiom { co_ax_unique   = nameUnique name
+                    , co_ax_name     = name
+                    , co_ax_implicit = False
+                    , co_ax_tvs      = tvs
+                    , co_ax_lhs      = mkTyConApp fam_tc inst_tys 
+                    , co_ax_rhs      = rep_ty }
 
 -- | Create a coercion identifying a @data@ or @newtype@ representation type
 -- and its family instance.  It has the form @Co tvs :: F ts ~ R tvs@,
@@ -212,36 +214,21 @@ mkDataFamInst name tvs fam_tc inst_tys rep_tc
               fi_flavor = DataFamilyInst rep_tc,
               fi_axiom  = axiom }
   where
-    axiom = CoAxiom { co_ax_unique = nameUnique name
-                    , co_ax_name   = name
-                    , co_ax_tvs    = tvs
-                    , co_ax_lhs    = mkTyConApp fam_tc inst_tys 
-                    , co_ax_rhs    = mkTyConApp rep_tc (mkTyVarTys tvs) }
-
--- Make a family instance representation from an indexed thing. 
--- This is used for local instances, where we can safely pull on the thing.
-mkLocalFamInst :: CoAxiom -> FamFlavor -> FamInst
-mkLocalFamInst axiom flavour
-  = FamInst {
-          fi_fam    = tyConName fam_tc,
-          fi_fam_tc = fam_tc,
-          fi_tcs    = roughMatchTcs tys,
-          fi_tvs    = mkVarSet (coAxiomTyVars axiom),
-          fi_tys    = tys,
-          fi_flavor = flavour,
-          fi_axiom  = axiom }
-  where 
-     (fam_tc, tys) = coAxiomSplitLHS axiom
+    axiom = CoAxiom { co_ax_unique   = nameUnique name
+                    , co_ax_name     = name
+                    , co_ax_implicit = False
+                    , co_ax_tvs      = tvs
+                    , co_ax_lhs      = mkTyConApp fam_tc inst_tys 
+                    , co_ax_rhs      = mkTyConApp rep_tc (mkTyVarTys tvs) }
 
 -- Make a family instance representation from the information found in an
 -- interface file.  In particular, we get the rough match info from the iface
 -- (instead of computing it here).
 mkImportedFamInst :: Name               -- Name of the family
                   -> [Maybe Name]       -- Rough match info
-                  -> FamFlavor          -- Family flavor
                   -> CoAxiom            -- Axiom introduced
                   -> FamInst            -- Resulting family instance
-mkImportedFamInst fam mb_tcs flavor axiom
+mkImportedFamInst fam mb_tcs axiom
   = FamInst {
       fi_fam    = fam,
       fi_fam_tc = fam_tc,
@@ -252,9 +239,19 @@ mkImportedFamInst fam mb_tcs flavor axiom
       fi_flavor = flavor }
   where 
      (fam_tc, tys) = coAxiomSplitLHS axiom
+
+         -- Derive the flavor for an imported FamInst rather disgustingly
+         -- Maybe we should store it in the IfaceFamInst?
+     flavor = case splitTyConApp_maybe (coAxiomRHS axiom) of
+                Just (tc, _)
+                  | Just ax' <- tyConFamilyCoercion_maybe tc
+                  , ax' == axiom
+                  -> DataFamilyInst tc
+                _ -> SynFamilyInst
 \end{code}
 
 
+
 %************************************************************************
 %*									*
 		FamInstEnv
@@ -421,9 +418,9 @@ lookupFamInstEnvConflicts envs fam_inst skol_tvs
   = lookup_fam_inst_env my_unify False envs fam tys1
   where
     inst_axiom = famInstAxiom fam_inst
-    (fam, tys) = coAxiomSplitLHS inst_axiom
-    skol_tys = mkTyVarTys skol_tvs
-    tys1     = substTys (zipTopTvSubst (coAxiomTyVars inst_axiom) skol_tys) tys
+    (fam, tys) = famInstLHS fam_inst
+    skol_tys   = mkTyVarTys skol_tvs
+    tys1       = substTys (zipTopTvSubst (coAxiomTyVars inst_axiom) skol_tys) tys
         -- In example above,   fam tys' = F [b]   
 
     my_unify old_fam_inst tpl_tvs tpl_tys match_tys
@@ -443,10 +440,8 @@ lookupFamInstEnvConflicts envs fam_inst skol_tvs
       where
         old_axiom = famInstAxiom old_fam_inst
         old_tvs   = coAxiomTyVars old_axiom
-        old_rhs   = substTyWith old_tvs
-                      (substTyVars subst old_tvs)  (coAxiomRHS old_axiom)
-        new_rhs   = substTyWith (coAxiomTyVars inst_axiom)
-                      (substTyVars subst skol_tvs) (coAxiomRHS inst_axiom)
+        old_rhs   = mkAxInstRHS old_axiom  (substTyVars subst old_tvs)
+        new_rhs   = mkAxInstRHS inst_axiom (substTyVars subst skol_tvs)
 
 -- This variant is called when we want to check if the conflict is only in the
 -- home environment (see FamInst.addLocalFamInst)
@@ -642,13 +637,9 @@ normaliseTcApp env tc tys
   , tyConArity tc <= length tys	   -- Unsaturated data families are possible
   , [(fam_inst, inst_tys)] <- lookupFamInstEnv env tc ntys 
   = let    -- A matching family instance exists
-        coAxiom         = famInstAxiom fam_inst
-        co              = mkAxInstCo coAxiom inst_tys
-        rhs             = case fi_flavor fam_inst of
-                            DataFamilyInst tycon -> mkTyConApp tycon inst_tys
-                            SynFamilyInst        ->
-                              substTyWith (coAxiomTyVars coAxiom) inst_tys
-                                (coAxiomRHS coAxiom)
+        ax              = famInstAxiom fam_inst
+        co              = mkAxInstCo  ax inst_tys
+        rhs             = mkAxInstRHS ax inst_tys
 	first_coi       = mkTransCo tycon_coi co
 	(rest_coi,nty)  = normaliseType env rhs
 	fix_coi         = mkTransCo first_coi rest_coi
diff --git a/compiler/types/TyCon.lhs b/compiler/types/TyCon.lhs
index 09524b363f..f5c05677e1 100644
--- a/compiler/types/TyCon.lhs
+++ b/compiler/types/TyCon.lhs
@@ -22,9 +22,9 @@ module TyCon(
 	SynTyConRhs(..),
 
 	-- ** Coercion axiom constructors
-        CoAxiom(..), mkCoAxiom,
+        CoAxiom(..), 
         coAxiomName, coAxiomArity, coAxiomTyVars,
-        coAxiomLHS, coAxiomRHS,
+        coAxiomLHS, coAxiomRHS, isImplicitCoAxiom,
 
         -- ** Constructing TyCons
 	mkAlgTyCon,
@@ -140,48 +140,11 @@ Note [Type synonym families]
   translates to
     a SynTyCon 'F', whose SynTyConRhs is SynFamilyTyCon
 
-* Translation of type instance decl:
-	type instance F [a] = Maybe a
-  translates to a "representation TyCon", 'R:FList', where
-     R:FList is a SynTyCon, whose 
-       SynTyConRhs is (SynonymTyCon (Maybe a))
-       TyConParent is (FamInstTyCon F [a] co)
-         where co :: F [a] ~ R:FList a
-
-  It's very much as if the user had written
-       type instance F [a] = R:FList a
-       type R:FList a = Maybe a
-  Indeed, in GHC's internal representation, the RHS of every
-  'type instance' is simply an application of the representation
-  TyCon to the quantified varaibles.
-
-  The intermediate representation TyCon is a bit gratuitous, but 
-  it means that:
-
-        each 'type instance' decls is in 1-1 correspondance 
-	with its representation TyCon
-
-  So the result of typechecking a 'type instance' decl is just a
-  TyCon.  In turn this means that type and data families can be
-  treated uniformly.
-
 * Translation of type family decl:
 	type family F a :: *
   translates to
     a SynTyCon 'F', whose SynTyConRhs is SynFamilyTyCon
 
-* Translation of type instance decl:
-	type instance F [a] = Maybe a
-  translates to
-    A SynTyCon 'R:FList a', whose 
-       SynTyConRhs is (SynonymTyCon (Maybe a))
-       TyConParent is (FamInstTyCon F [a] co)
-         where co :: F [a] ~ R:FList a
-    Notice that we introduce a gratuitous vanilla type synonym
-       type R:FList a = Maybe a
-    solely so that type and data families can be treated more
-    uniformly, via a single FamInstTyCon descriptor        
-
 * In the future we might want to support
     * closed type families (esp when we have proper kinds)
     * injective type families (allow decomposition)
@@ -589,7 +552,8 @@ data TyConParent
                   -- and R:T is the representation TyCon (ie this one)
                   -- and a,b,c are the tyConTyVars of this TyCon
 
-          -- Cached fields of the CoAxiom
+          -- Cached fields of the CoAxiom, but adjusted to
+          -- use the tyConTyVars of this TyCon
 	TyCon   -- The family TyCon
 	[Type]	-- Argument types (mentions the tyConTyVars of this TyCon)
 		-- Match in length the tyConTyVars of the family TyCon
@@ -683,23 +647,21 @@ See Trac #4528.
 
 Note [Newtype coercions]
 ~~~~~~~~~~~~~~~~~~~~~~~~
-The NewTyCon field nt_co is a a TyCon (a coercion constructor in fact)
-which is used for coercing from the representation type of the
-newtype, to the newtype itself. For example,
+The NewTyCon field nt_co is a CoAxiom which is used for coercing from
+the representation type of the newtype, to the newtype itself. For
+example,
 
    newtype T a = MkT (a -> a)
 
-the NewTyCon for T will contain nt_co = CoT where CoT t : T t ~ t ->
-t.  This TyCon is a CoTyCon, so it does not have a kind on its
-own; it basically has its own typing rule for the fully-applied
-version.  If the newtype T has k type variables then CoT has arity at
-most k.  In the case that the right hand side is a type application
+the NewTyCon for T will contain nt_co = CoT where CoT t : T t ~ t -> t.  
+
+In the case that the right hand side is a type application
 ending with the same type variables as the left hand side, we
 "eta-contract" the coercion.  So if we had
 
    newtype S a = MkT [a]
 
-then we would generate the arity 0 coercion CoS : S ~ [].  The
+then we would generate the arity 0 axiom CoS : S ~ [].  The
 primary reason we do this is to make newtype deriving cleaner.
 
 In the paper we'd write
@@ -708,14 +670,6 @@ and then when we used CoT at a particular type, s, we'd say
 	CoT @ s
 which encodes as (TyConApp instCoercionTyCon [TyConApp CoT [], s])
 
-But in GHC we instead make CoT into a new piece of type syntax, CoTyCon,
-(like instCoercionTyCon, symCoercionTyCon etc), which must always
-be saturated, but which encodes as
-	TyConApp CoT [s]
-In the vocabulary of the paper it's as if we had axiom declarations
-like
-	axiom CoT t :  T t ~ [t]
-
 Note [Newtype eta]
 ~~~~~~~~~~~~~~~~~~
 Consider
@@ -764,18 +718,17 @@ so the coercion tycon CoT must have
 \begin{code}
 -- | A 'CoAxiom' is a \"coercion constructor\", i.e. a named equality axiom.
 data CoAxiom
-  = CoAxiom                   -- type equality axiom.
-    { co_ax_unique :: Unique      -- unique identifier
-    , co_ax_name   :: Name        -- name for pretty-printing
-    , co_ax_tvs    :: [TyVar]     -- bound type variables 
-    , co_ax_lhs    :: Type        -- left-hand side of the equality
-    , co_ax_rhs    :: Type        -- right-hand side of the equality
+  = CoAxiom                   -- Type equality axiom.
+    { co_ax_unique   :: Unique      -- unique identifier
+    , co_ax_name     :: Name        -- name for pretty-printing
+    , co_ax_tvs      :: [TyVar]     -- bound type variables 
+    , co_ax_lhs      :: Type        -- left-hand side of the equality
+    , co_ax_rhs      :: Type        -- right-hand side of the equality
+    , co_ax_implicit :: Bool        -- True <=> the axiom is "implicit"
+                                    -- See Note [Implicit axioms]
     }
   deriving Typeable
 
-mkCoAxiom :: Unique -> Name -> [TyVar] -> Type -> Type -> CoAxiom
-mkCoAxiom u n tvs lhs rhs = CoAxiom u n tvs lhs rhs
-
 coAxiomArity :: CoAxiom -> Arity
 coAxiomArity ax = length (co_ax_tvs ax)
 
@@ -788,8 +741,22 @@ coAxiomTyVars = co_ax_tvs
 coAxiomLHS, coAxiomRHS :: CoAxiom -> Type
 coAxiomLHS = co_ax_lhs
 coAxiomRHS = co_ax_rhs
+
+isImplicitCoAxiom :: CoAxiom -> Bool
+isImplicitCoAxiom = co_ax_implicit
 \end{code}
 
+Note [Implicit axioms]
+~~~~~~~~~~~~~~~~~~~~~~
+See also Note [Implicit TyThings] in HscTypes
+* A CoAxiom arising from data/type family instances is not "implicit".
+  That is, it has its own IfaceAxiom declaration in an interface file
+
+* The CoAxiom arising from a newtype declaration *is* "implicit".
+  That is, it does not have its own IfaceAxiom declaration in an
+  interface file; instead the CoAxiom is generated by type-checking
+  the newtype declaration
+
 
 %************************************************************************
 %*									*
@@ -1268,12 +1235,13 @@ isPromotedTypeTyCon _                      = False
 -- * Family instances are /not/ implicit as they represent the instance body
 --   (similar to a @dfun@ does that for a class instance).
 isImplicitTyCon :: TyCon -> Bool
-isImplicitTyCon tycon | isTyConAssoc tycon           = True
-		      | isSynTyCon tycon	     = False
-		      | isAlgTyCon tycon	     = isTupleTyCon tycon
-isImplicitTyCon _other                               = True
-        -- catches: FunTyCon, PrimTyCon, 
-        -- CoTyCon, SuperKindTyCon
+isImplicitTyCon tycon 
+  | isTyConAssoc tycon = True
+  | isSynTyCon tycon   = False
+  | isAlgTyCon tycon   = isTupleTyCon tycon
+  | otherwise          = True
+        -- 'otherwise' catches: FunTyCon, PrimTyCon, 
+        -- PromotedDataCon, PomotedTypeTyCon, SuperKindTyCon
 \end{code}
 
 
diff --git a/compiler/vectorise/Vectorise/Utils/Base.hs b/compiler/vectorise/Vectorise/Utils/Base.hs
index 0c111f49c7..2b47ddfb9b 100644
--- a/compiler/vectorise/Vectorise/Utils/Base.hs
+++ b/compiler/vectorise/Vectorise/Utils/Base.hs
@@ -36,7 +36,6 @@ import DataCon
 import MkId
 import FastString
 
-
 -- Simple Types ---------------------------------------------------------------
 
 voidType :: VM Type
diff --git a/compiler/vectorise/Vectorise/Utils/PADict.hs b/compiler/vectorise/Vectorise/Utils/PADict.hs
index cb3495d315..dfc08bcf58 100644
--- a/compiler/vectorise/Vectorise/Utils/PADict.hs
+++ b/compiler/vectorise/Vectorise/Utils/PADict.hs
@@ -114,9 +114,9 @@ paMethod method _ ty
 -- Note that @ty@ is only used for error messages
 --
 prDictOfPReprInstTyCon :: Type -> CoAxiom -> [Type] -> VM CoreExpr
-prDictOfPReprInstTyCon ty prepr_ax prepr_args
-  | Just rhs <- coreView (coAxiomRHS prepr_ax)
+prDictOfPReprInstTyCon _ty prepr_ax prepr_args
   = do
+      let rhs = mkAxInstRHS prepr_ax prepr_args
       dict <- prDictOfReprType' rhs
       pr_co <- mkBuiltinCo prTyCon
       let co = mkAppCo pr_co
@@ -124,8 +124,6 @@ prDictOfPReprInstTyCon ty prepr_ax prepr_args
              $ mkAxInstCo prepr_ax prepr_args
       return $ mkCast dict co
 
-  | otherwise = cantVectorise "Invalid PRepr type instance" (ppr ty)
-
 -- |Get the PR dictionary for a type. The argument must be a representation
 -- type.
 --
diff --git a/ghc/InteractiveUI.hs b/ghc/InteractiveUI.hs
index cc4be40f44..de65b1d48d 100644
--- a/ghc/InteractiveUI.hs
+++ b/ghc/InteractiveUI.hs
@@ -962,7 +962,7 @@ filterOutChildren get_thing xs
                      Just p  -> getName p `elemNameSet` all_names
                      Nothing -> False
 
-pprInfo :: PrintExplicitForalls -> (TyThing, Fixity, [GHC.Instance]) -> SDoc
+pprInfo :: PrintExplicitForalls -> (TyThing, Fixity, [GHC.ClsInst]) -> SDoc
 pprInfo pefas (thing, fixity, insts)
   =  pprTyThingInContextLoc pefas thing
   $$ show_fixity fixity
@@ -2005,7 +2005,7 @@ showBindings = do
         let pefas = dopt Opt_PrintExplicitForalls dflags
         mb_stuff <- GHC.getInfo (getName tt)
         return $ maybe (text "") (pprTT pefas) mb_stuff
-    pprTT :: PrintExplicitForalls -> (TyThing, Fixity, [GHC.Instance]) -> SDoc
+    pprTT :: PrintExplicitForalls -> (TyThing, Fixity, [GHC.ClsInst]) -> SDoc
     pprTT pefas (thing, fixity, _insts) =
         pprTyThing pefas thing
         $$ show_fixity fixity