Major refactoring of CoAxioms

This patch should have no user-visible effect.  It implements a
significant internal refactoring of the way that FC axioms are
handled.  The ultimate goal is to put us in a position to implement
"pattern-matching axioms".  But the changes here are only does
refactoring; there is no change in functionality.

Specifically:

 * We now treat data/type family instance declarations very,
   very similarly to types class instance declarations:

   - Renamed InstEnv.Instance as InstEnv.ClsInst, for symmetry with
     FamInstEnv.FamInst.  This change does affect the GHC API, but
     for the better I think.

   - Previously, each family type/data instance declaration gave rise
     to a *TyCon*; typechecking a type/data instance decl produced
     that TyCon.  Now, each type/data instance gives rise to
     a *FamInst*, by direct analogy with each class instance
     declaration giving rise to a ClsInst.

   - Just as each ClsInst contains its evidence, a DFunId, so each FamInst
     contains its evidence, a CoAxiom.  See Note [FamInsts and CoAxioms]
     in FamInstEnv.  The CoAxiom is a System-FC thing, and can relate any
     two types, whereas the FamInst relates directly to the Haskell source
     language construct, and always has a function (F tys) on the LHS.

   - Just as a DFunId has its own declaration in an interface file, so now
     do CoAxioms (see IfaceSyn.IfaceAxiom).

   These changes give rise to almost all the refactoring.

 * We used to have a hack whereby a type family instance produced a dummy
   type synonym, thus
      type instance F Int = Bool -> Bool
   translated to
      axiom FInt :: F Int ~ R:FInt
      type R:FInt = Bool -> Bool
   This was always a hack, and now it's gone.  Instead the type instance
   declaration produces a FamInst, whose axiom has kind
      axiom FInt :: F Int ~ Bool -> Bool
   just as you'd expect.

 * Newtypes are done just as before; they generate a CoAxiom. These
   CoAxioms are "implicit" (do not generate an IfaceAxiom declaration),
   unlike the ones coming from family instance declarations.  See
   Note [Implicit axioms] in TyCon

On the whole the code gets significantly nicer.  There were consequential
tidy-ups in the vectoriser, but I think I got them right.

1 files changed, 70 insertions, 77 deletions

diff --git a/compiler/iface/IfaceSyn.lhs b/compiler/iface/IfaceSyn.lhs
index 6f59e38736..fd8b361b3d 100644
--- a/compiler/iface/IfaceSyn.lhs
+++ b/compiler/iface/IfaceSyn.lhs
@@ -20,13 +20,13 @@ module IfaceSyn (
         IfaceBinding(..), IfaceConAlt(..),
         IfaceIdInfo(..), IfaceIdDetails(..), IfaceUnfolding(..),
         IfaceInfoItem(..), IfaceRule(..), IfaceAnnotation(..), IfaceAnnTarget,
-        IfaceInst(..), IfaceFamInst(..), IfaceTickish(..),
+        IfaceClsInst(..), IfaceFamInst(..), IfaceTickish(..),
 
         -- Misc
-        ifaceDeclSubBndrs, visibleIfConDecls,
+        ifaceDeclImplicitBndrs, visibleIfConDecls,
 
         -- Free Names
-        freeNamesIfDecl, freeNamesIfRule,
+        freeNamesIfDecl, freeNamesIfRule, freeNamesIfFamInst,
 
         -- Pretty printing
         pprIfaceExpr, pprIfaceDeclHead
@@ -70,26 +70,19 @@ data IfaceDecl
   | IfaceData { ifName       :: OccName,        -- Type constructor
                 ifTyVars     :: [IfaceTvBndr],  -- Type variables
                 ifCtxt       :: IfaceContext,   -- The "stupid theta"
-                ifCons       :: IfaceConDecls,  -- Includes new/data info
+                ifCons       :: IfaceConDecls,  -- Includes new/data/data family info
                 ifRec        :: RecFlag,        -- Recursive or not?
                 ifGadtSyntax :: Bool,           -- True <=> declared using
                                                 -- GADT syntax
-                ifFamInst    :: Maybe (IfaceTyCon, [IfaceType])
-                                                -- Just <=> instance of family
-                                                -- Invariant:
-                                                --   ifCons /= IfOpenDataTyCon
-                                                --   for family instances
+                ifAxiom      :: Maybe IfExtName -- The axiom, for a newtype, 
+                                                -- or data/newtype family instance
     }
 
   | IfaceSyn  { ifName    :: OccName,           -- Type constructor
                 ifTyVars  :: [IfaceTvBndr],     -- Type variables
                 ifSynKind :: IfaceKind,         -- Kind of the *rhs* (not of the tycon)
-                ifSynRhs  :: Maybe IfaceType,   -- Just rhs for an ordinary synonyn
-                                                -- Nothing for an open family
-                ifFamInst :: Maybe (IfaceTyCon, [IfaceType])
-                                                -- Just <=> instance of family
-                                                -- Invariant: ifOpenSyn == False
-                                                --   for family instances
+                ifSynRhs  :: Maybe IfaceType    -- Just rhs for an ordinary synonyn
+                                                -- Nothing for an type family declaration
     }
 
   | IfaceClass { ifCtxt    :: IfaceContext,     -- Context...
@@ -102,6 +95,11 @@ data IfaceDecl
                                                 --   with the class recursive?
     }
 
+  | IfaceAxiom { ifName   :: OccName       -- Axiom name
+               , ifTyVars :: [IfaceTvBndr] -- Axiom tyvars
+               , ifLHS    :: IfaceType     -- Axiom LHS
+               , ifRHS    :: IfaceType }   -- and RHS
+
   | IfaceForeign { ifName :: OccName,           -- Needs expanding when we move
                                                 -- beyond .NET
                    ifExtName :: Maybe FastString }
@@ -123,13 +121,13 @@ data IfaceATDefault = IfaceATD [IfaceTvBndr] [IfaceType] IfaceType
 
 data IfaceConDecls
   = IfAbstractTyCon Bool        -- c.f TyCon.AbstractTyCon
-  | IfOpenDataTyCon             -- Open data family
-  | IfDataTyCon [IfaceConDecl]  -- data type decls
-  | IfNewTyCon  IfaceConDecl    -- newtype decls
+  | IfDataFamTyCon              -- Data family
+  | IfDataTyCon [IfaceConDecl]  -- Data type decls
+  | IfNewTyCon  IfaceConDecl    -- Newtype decls
 
 visibleIfConDecls :: IfaceConDecls -> [IfaceConDecl]
 visibleIfConDecls (IfAbstractTyCon {}) = []
-visibleIfConDecls IfOpenDataTyCon      = []
+visibleIfConDecls IfDataFamTyCon      = []
 visibleIfConDecls (IfDataTyCon cs)     = cs
 visibleIfConDecls (IfNewTyCon c)       = [c]
 
@@ -147,12 +145,12 @@ data IfaceConDecl
         ifConStricts :: [HsBang]}               -- Empty (meaning all lazy),
                                                 -- or 1-1 corresp with arg tys
 
-data IfaceInst
-  = IfaceInst { ifInstCls  :: IfExtName,                -- See comments with
-                ifInstTys  :: [Maybe IfaceTyCon],       -- the defn of Instance
-                ifDFun     :: IfExtName,                -- The dfun
-                ifOFlag    :: OverlapFlag,              -- Overlap flag
-                ifInstOrph :: Maybe OccName }           -- See Note [Orphans]
+data IfaceClsInst
+  = IfaceClsInst { ifInstCls  :: IfExtName,                -- See comments with
+                   ifInstTys  :: [Maybe IfaceTyCon],       -- the defn of ClsInst
+                   ifDFun     :: IfExtName,                -- The dfun
+                   ifOFlag    :: OverlapFlag,              -- Overlap flag
+                   ifInstOrph :: Maybe OccName }           -- See Note [Orphans]
         -- There's always a separate IfaceDecl for the DFun, which gives
         -- its IdInfo with its full type and version number.
         -- The instance declarations taken together have a version number,
@@ -161,9 +159,10 @@ data IfaceInst
         -- and if the head does not change it won't be used if it wasn't before
 
 data IfaceFamInst
-  = IfaceFamInst { ifFamInstFam   :: IfExtName                -- Family tycon
+  = IfaceFamInst { ifFamInstFam   :: IfExtName           -- Family name
                  , ifFamInstTys   :: [Maybe IfaceTyCon]  -- Rough match types
-                 , ifFamInstTyCon :: IfaceTyCon          -- Instance decl
+                 , ifFamInstAxiom :: IfExtName           -- The axiom
+                 , ifFamInstOrph  :: Maybe OccName       -- Just like IfaceClsInst
                  }
 
 data IfaceRule
@@ -175,7 +174,7 @@ data IfaceRule
         ifRuleArgs   :: [IfaceExpr],    -- Args of LHS
         ifRuleRhs    :: IfaceExpr,
         ifRuleAuto   :: Bool,
-        ifRuleOrph   :: Maybe OccName   -- Just like IfaceInst
+        ifRuleOrph   :: Maybe OccName   -- Just like IfaceClsInst
     }
 
 data IfaceAnnotation
@@ -375,38 +374,34 @@ 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 }),
-                              ifFamInst = famInst})
-  =   -- implicit coerion and (possibly) family instance coercion
-    (mkNewTyCoOcc tc_occ) : (famInstCo famInst tc_occ) ++
+                                        IfCon { ifConOcc = con_occ })})
+  =   -- implicit newtype coercion
+    (mkNewTyCoOcc tc_occ) : -- JPM: newtype coercions shouldn't be implicit
       -- data constructor and worker (newtypes don't have a wrapper)
     [con_occ, mkDataConWorkerOcc con_occ]
 
 
-ifaceDeclSubBndrs (IfaceData {ifName = tc_occ,
-                              ifCons = IfDataTyCon cons,
-                              ifFamInst = famInst})
-  =   -- (possibly) family instance coercion;
-      -- there is no implicit coercion for non-newtypes
-    famInstCo famInst tc_occ
-      -- for each data constructor in order,
-      --    data constructor, worker, and (possibly) wrapper
-    ++ concatMap dc_occs cons
+ifaceDeclImplicitBndrs (IfaceData {ifName = _tc_occ,
+                              ifCons = IfDataTyCon cons })
+  = -- for each data constructor in order,
+    --    data constructor, worker, and (possibly) wrapper
+    concatMap dc_occs cons
   where
     dc_occs con_decl
         | has_wrapper = [con_occ, work_occ, wrap_occ]
@@ -418,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 ++
@@ -441,16 +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 (IfaceSyn {ifName = tc_occ,
-                             ifFamInst = famInst})
-  = famInstCo famInst tc_occ
-
-ifaceDeclSubBndrs _ = []
-
--- coercion for data/newtype family instances
-famInstCo :: Maybe (IfaceTyCon, [IfaceType]) -> OccName -> [OccName]
-famInstCo Nothing  _       = []
-famInstCo (Just _) baseOcc = [mkInstTyCoOcc baseOcc]
+ifaceDeclImplicitBndrs _ = []
 
 ----------------------------- Printing IfaceDecl ------------------------------
 
@@ -468,10 +454,9 @@ pprIfaceDecl (IfaceForeign {ifName = tycon})
   = hsep [ptext (sLit "foreign import type dotnet"), ppr tycon]
 
 pprIfaceDecl (IfaceSyn {ifName = tycon, ifTyVars = tyvars,
-                        ifSynRhs = Just mono_ty,
-                        ifFamInst = mbFamInst})
+                        ifSynRhs = Just mono_ty})
   = hang (ptext (sLit "type") <+> pprIfaceDeclHead [] tycon tyvars)
-       4 (vcat [equals <+> ppr mono_ty, pprFamily mbFamInst])
+       4 (vcat [equals <+> ppr mono_ty])
 
 pprIfaceDecl (IfaceSyn {ifName = tycon, ifTyVars = tyvars,
                         ifSynRhs = Nothing, ifSynKind = kind })
@@ -480,14 +465,14 @@ pprIfaceDecl (IfaceSyn {ifName = tycon, ifTyVars = tyvars,
 
 pprIfaceDecl (IfaceData {ifName = tycon, ifCtxt = context,
                          ifTyVars = tyvars, ifCons = condecls,
-                         ifRec = isrec, ifFamInst = mbFamInst})
+                         ifRec = isrec, ifAxiom = mbAxiom})
   = hang (pp_nd <+> pprIfaceDeclHead context tycon tyvars)
        4 (vcat [pprRec isrec, pp_condecls tycon condecls,
-                pprFamily mbFamInst])
+                pprAxiom mbAxiom])
   where
     pp_nd = case condecls of
                 IfAbstractTyCon dis -> ptext (sLit "abstract") <> parens (ppr dis)
-                IfOpenDataTyCon     -> ptext (sLit "data family")
+                IfDataFamTyCon     -> ptext (sLit "data family")
                 IfDataTyCon _       -> ptext (sLit "data")
                 IfNewTyCon _        -> ptext (sLit "newtype")
 
@@ -499,12 +484,17 @@ pprIfaceDecl (IfaceClass {ifCtxt = context, ifName = clas, ifTyVars = tyvars,
                 sep (map ppr ats),
                 sep (map ppr sigs)])
 
+pprIfaceDecl (IfaceAxiom {ifName = name, ifTyVars = tyvars,
+                          ifLHS = lhs, ifRHS = rhs})
+  = hang (ptext (sLit "axiom") <+> ppr name <+> ppr tyvars)
+       2 (dcolon <+> ppr lhs <+> text "~#" <+> ppr rhs)
+
 pprRec :: RecFlag -> SDoc
 pprRec isrec = ptext (sLit "RecFlag") <+> ppr isrec
 
-pprFamily :: Maybe (IfaceTyCon, [IfaceType]) -> SDoc
-pprFamily Nothing        = ptext (sLit "FamilyInstance: none")
-pprFamily (Just famInst) = ptext (sLit "FamilyInstance:") <+> ppr famInst
+pprAxiom :: Maybe Name -> SDoc
+pprAxiom Nothing   = ptext (sLit "FamilyInstance: none")
+pprAxiom (Just ax) = ptext (sLit "FamilyInstance:") <+> ppr ax
 
 instance Outputable IfaceClassOp where
    ppr (IfaceClassOp n dm ty) = ppr n <+> ppr dm <+> dcolon <+> ppr ty
@@ -522,7 +512,7 @@ pprIfaceDeclHead context thing tyvars
 
 pp_condecls :: OccName -> IfaceConDecls -> SDoc
 pp_condecls _  (IfAbstractTyCon {}) = empty
-pp_condecls _  IfOpenDataTyCon      = empty
+pp_condecls _  IfDataFamTyCon      = empty
 pp_condecls tc (IfNewTyCon c)   = equals <+> pprIfaceConDecl tc c
 pp_condecls tc (IfDataTyCon cs) = equals <+> sep (punctuate (ptext (sLit " |"))
                                                             (map (pprIfaceConDecl tc) cs))
@@ -571,8 +561,8 @@ instance Outputable IfaceRule where
                         ptext (sLit "=") <+> ppr rhs])
       ]
 
-instance Outputable IfaceInst where
-  ppr (IfaceInst {ifDFun = dfun_id, ifOFlag = flag,
+instance Outputable IfaceClsInst where
+  ppr (IfaceClsInst {ifDFun = dfun_id, ifOFlag = flag,
                   ifInstCls = cls, ifInstTys = mb_tcs})
     = hang (ptext (sLit "instance") <+> ppr flag
                 <+> ppr cls <+> brackets (pprWithCommas ppr_rough mb_tcs))
@@ -580,10 +570,10 @@ instance Outputable IfaceInst where
 
 instance Outputable IfaceFamInst where
   ppr (IfaceFamInst {ifFamInstFam = fam, ifFamInstTys = mb_tcs,
-                     ifFamInstTyCon = tycon_id})
+                     ifFamInstAxiom = tycon_ax})
     = hang (ptext (sLit "family instance") <+>
             ppr fam <+> brackets (pprWithCommas ppr_rough mb_tcs))
-         2 (equals <+> ppr tycon_id)
+         2 (equals <+> ppr tycon_ax)
 
 ppr_rough :: Maybe IfaceTyCon -> SDoc
 ppr_rough Nothing   = dot
@@ -741,13 +731,12 @@ freeNamesIfDecl IfaceForeign{} =
   emptyNameSet
 freeNamesIfDecl d@IfaceData{} =
   freeNamesIfTvBndrs (ifTyVars d) &&&
-  freeNamesIfTcFam (ifFamInst d) &&&
+  maybe emptyNameSet unitNameSet (ifAxiom d) &&&
   freeNamesIfContext (ifCtxt d) &&&
   freeNamesIfConDecls (ifCons d)
 freeNamesIfDecl d@IfaceSyn{} =
   freeNamesIfTvBndrs (ifTyVars d) &&&
   freeNamesIfSynRhs (ifSynRhs d) &&&
-  freeNamesIfTcFam (ifFamInst d) &&&
   freeNamesIfKind (ifSynKind d) -- IA0_NOTE: because of promotion, we
                                 -- return names in the kind signature
 freeNamesIfDecl d@IfaceClass{} =
@@ -755,6 +744,10 @@ freeNamesIfDecl d@IfaceClass{} =
   freeNamesIfContext (ifCtxt d) &&&
   fnList freeNamesIfAT     (ifATs d) &&&
   fnList freeNamesIfClsSig (ifSigs d)
+freeNamesIfDecl d@IfaceAxiom{} =
+  freeNamesIfTvBndrs (ifTyVars d) &&&
+  freeNamesIfType (ifLHS d) &&&
+  freeNamesIfType (ifRHS d)
 
 freeNamesIfIdDetails :: IfaceIdDetails -> NameSet
 freeNamesIfIdDetails (IfRecSelId tc _) = freeNamesIfTc tc
@@ -765,12 +758,6 @@ freeNamesIfSynRhs :: Maybe IfaceType -> NameSet
 freeNamesIfSynRhs (Just ty) = freeNamesIfType ty
 freeNamesIfSynRhs Nothing   = emptyNameSet
 
-freeNamesIfTcFam :: Maybe (IfaceTyCon, [IfaceType]) -> NameSet
-freeNamesIfTcFam (Just (tc,tys)) =
-  freeNamesIfTc tc &&& fnList freeNamesIfType tys
-freeNamesIfTcFam Nothing =
-  emptyNameSet
-
 freeNamesIfContext :: IfaceContext -> NameSet
 freeNamesIfContext = fnList freeNamesIfType
 
@@ -902,6 +889,12 @@ freeNamesIfRule (IfaceRule { ifRuleBndrs = bs, ifRuleHead = f
     fnList freeNamesIfBndr bs &&&
     fnList freeNamesIfExpr es &&&
     freeNamesIfExpr rhs
+    
+freeNamesIfFamInst :: IfaceFamInst -> NameSet
+freeNamesIfFamInst (IfaceFamInst { ifFamInstFam = famName
+                                 , ifFamInstAxiom = axName })
+  = unitNameSet famName &&&
+    unitNameSet axName
 
 -- helpers
 (&&&) :: NameSet -> NameSet -> NameSet