This BIG PATCH contains most of the work for the New Coercion Representation
[ghc-hetmet.git] / compiler / types / TyCon.lhs
index 6693ca2..1d8d48a 100644 (file)
@@ -8,24 +8,27 @@ The @TyCon@ datatype
 \begin{code}
 module TyCon(
         -- * Main TyCon data types
-       TyCon, FieldLabel,
+       TyCon, FieldLabel, 
 
        AlgTyConRhs(..), visibleDataCons, 
-        TyConParent(..), 
+        TyConParent(..), isNoParent,
        SynTyConRhs(..),
 
+       -- ** Coercion axiom constructors
+        CoAxiom(..), coAxiomName, coAxiomArity,
+
         -- ** Constructing TyCons
        mkAlgTyCon,
        mkClassTyCon,
        mkFunTyCon,
        mkPrimTyCon,
-       mkVoidPrimTyCon,
+       mkKindTyCon,
        mkLiftedPrimTyCon,
        mkTupleTyCon,
        mkSynTyCon,
         mkSuperKindTyCon,
-        mkCoercionTyCon,
         mkForeignTyCon,
+        mkAnyTyCon,
 
         -- ** Predicates on TyCons
         isAlgTyCon,
@@ -33,13 +36,14 @@ module TyCon(
         isFunTyCon, 
         isPrimTyCon,
         isTupleTyCon, isUnboxedTupleTyCon, isBoxedTupleTyCon, 
-        isSynTyCon, isClosedSynTyCon, isOpenSynTyCon,
-        isSuperKindTyCon,
-        isCoercionTyCon, isCoercionTyCon_maybe,
-        isForeignTyCon,
+        isSynTyCon, isClosedSynTyCon,
+        isSuperKindTyCon, isDecomposableTyCon,
+        isForeignTyCon, isAnyTyCon, tyConHasKind,
 
+       isInjectiveTyCon,
        isDataTyCon, isProductTyCon, isEnumerationTyCon, 
-       isNewTyCon, isAbstractTyCon, isOpenTyCon,
+        isNewTyCon, isAbstractTyCon,
+        isFamilyTyCon, isSynFamilyTyCon, isDataFamilyTyCon,
         isUnLiftedTyCon,
        isGadtSyntaxTyCon,
        isTyConAssoc,
@@ -54,23 +58,21 @@ module TyCon(
        tyConTyVars,
        tyConDataCons, tyConDataCons_maybe, tyConSingleDataCon_maybe,
        tyConFamilySize,
-       tyConSelIds,
        tyConStupidTheta,
        tyConArity,
+        tyConParent,
        tyConClass_maybe,
-       tyConFamInst_maybe, tyConFamilyCoercion_maybe,
-       synTyConDefn, synTyConRhs, synTyConType, synTyConResKind,
-       tyConExtName,           -- External name for foreign types
+       tyConFamInst_maybe, tyConFamilyCoercion_maybe,tyConFamInstSig_maybe,
+        synTyConDefn, synTyConRhs, synTyConType,
+        tyConExtName,           -- External name for foreign types
        algTyConRhs,
         newTyConRhs, newTyConEtadRhs, unwrapNewTyCon_maybe, 
-        assocTyConArgPoss_maybe,
         tupleTyConBoxity,
 
         -- ** Manipulating TyCons
        tcExpandTyCon_maybe, coreExpandTyCon_maybe,
        makeTyConAbstract,
-       newTyConCo_maybe,
-       setTyConArgPoss, 
+       newTyConCo, newTyConCo_maybe,
 
         -- * Primitive representations of Types
        PrimRep(..),
@@ -92,8 +94,180 @@ import Maybes
 import Outputable
 import FastString
 import Constants
+import Util
+import qualified Data.Data as Data
 \end{code}
 
+-----------------------------------------------
+       Notes about type families
+-----------------------------------------------
+
+Note [Type synonym families]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+* Type synonym families, also known as "type functions", map directly
+  onto the type functions in FC:
+
+       type family F a :: *
+       type instance F Int = Bool
+       ..etc...
+
+* Reply "yes" to isSynFamilyTyCon, and isFamilyTyCon
+
+* From the user's point of view (F Int) and Bool are simply
+  equivalent types.
+
+* A Haskell 98 type synonym is a degenerate form of a type synonym
+  family.
+
+* Type functions can't appear in the LHS of a type function:
+       type instance F (F Int) = ...   -- BAD!
+
+* 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 "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)
+  but we don't at the moment [2010]
+
+Note [Data type families]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+See also Note [Wrappers for data instance tycons] in MkId.lhs
+
+* Data type families are declared thus
+       data family T a :: *
+       data instance T Int = T1 | T2 Bool
+
+  Here T is the "family TyCon".
+
+* Reply "yes" to isDataFamilyTyCon, and isFamilyTyCon
+
+* Reply "yes" to isDataFamilyTyCon, and isFamilyTyCon
+
+* The user does not see any "equivalent types" as he did with type
+  synonym families.  He just sees constructors with types
+       T1 :: T Int
+       T2 :: Bool -> T Int
+
+* Here's the FC version of the above declarations:
+
+       data T a
+       data R:TInt = T1 | T2 Bool
+       axiom ax_ti : T Int ~ R:TInt
+
+  The R:TInt is the "representation TyCons".
+  It has an AlgTyConParent of
+       FamInstTyCon T [Int] ax_ti
+
+* The data contructor T2 has a wrapper (which is what the 
+  source-level "T2" invokes):
+
+       $WT2 :: Bool -> T Int
+       $WT2 b = T2 b `cast` sym ax_ti
+
+* A data instance can declare a fully-fledged GADT:
+
+       data instance T (a,b) where
+          X1 :: T (Int,Bool)
+         X2 :: a -> b -> T (a,b)
+
+  Here's the FC version of the above declaration:
+
+       data R:TPair a where
+         X1 :: R:TPair Int Bool
+         X2 :: a -> b -> R:TPair a b
+       axiom ax_pr :: T (a,b) ~ R:TPair a b
+
+       $WX1 :: forall a b. a -> b -> T (a,b)
+       $WX1 a b (x::a) (y::b) = X2 a b x y `cast` sym (ax_pr a b)
+
+  The R:TPair are the "representation TyCons".
+  We have a bit of work to do, to unpick the result types of the
+  data instance declaration for T (a,b), to get the result type in the
+  representation; e.g.  T (a,b) --> R:TPair a b
+
+  The representation TyCon R:TList, has an AlgTyConParent of
+
+       FamInstTyCon T [(a,b)] ax_pr
+
+* Notice that T is NOT translated to a FC type function; it just
+  becomes a "data type" with no constructors, which can be coerced inot
+  into R:TInt, R:TPair by the axioms.  These axioms
+  axioms come into play when (and *only* when) you
+       - use a data constructor
+       - do pattern matching
+  Rather like newtype, in fact
+
+  As a result
+
+  - T behaves just like a data type so far as decomposition is concerned
+
+  - (T Int) is not implicitly converted to R:TInt during type inference. 
+    Indeed the latter type is unknown to the programmer.
+
+  - There *is* an instance for (T Int) in the type-family instance 
+    environment, but it is only used for overlap checking
+
+  - It's fine to have T in the LHS of a type function:
+    type instance F (T a) = [a]
+
+  It was this last point that confused me!  The big thing is that you
+  should not think of a data family T as a *type function* at all, not
+  even an injective one!  We can't allow even injective type functions
+  on the LHS of a type function:
+       type family injective G a :: *
+       type instance F (G Int) = Bool
+  is no good, even if G is injective, because consider
+       type instance G Int = Bool
+       type instance F Bool = Char
+
+  So a data type family is not an injective type function. It's just a
+  data type with some axioms that connect it to other data types. 
+
 %************************************************************************
 %*                                                                     *
 \subsection{The data type}
@@ -101,7 +275,7 @@ import Constants
 %************************************************************************
 
 \begin{code}
--- | Represents type constructors. Type constructors are introduced by things such as:
+-- | TyCons represent type constructors. Type constructors are introduced by things such as:
 --
 -- 1) Data declarations: @data Foo = ...@ creates the @Foo@ type constructor of kind @*@
 --
@@ -111,9 +285,6 @@ import Constants
 --
 -- 4) Class declarations: @class Foo where@ creates the @Foo@ type constructor of kind @*@
 --
--- 5) Type coercions! This is because we represent a coercion from @t1@ to @t2@ as a 'Type', where
---    that type has kind @t1 :=: t2@. See "Coercion" for more on this
---
 -- This data type also encodes a number of primitive, built in type constructors such as those
 -- for function and tuple types.
 data TyCon
@@ -121,55 +292,64 @@ data TyCon
     FunTyCon {
        tyConUnique :: Unique,
        tyConName   :: Name,
-       tyConKind   :: Kind,
+       tc_kind   :: Kind,
        tyConArity  :: Arity
     }
 
-  -- | Algebraic type constructors, which are defined to be those arising @data@ type and @newtype@ declarations.
-  -- All these constructors are lifted and boxed. See 'AlgTyConRhs' for more information.
+  -- | Algebraic type constructors, which are defined to be those
+  -- arising @data@ type and @newtype@ declarations.  All these
+  -- constructors are lifted and boxed. See 'AlgTyConRhs' for more
+  -- information.
   | AlgTyCon {         
        tyConUnique :: Unique,
        tyConName   :: Name,
-       tyConKind   :: Kind,
+       tc_kind   :: Kind,
        tyConArity  :: Arity,
 
-       tyConTyVars :: [TyVar],         -- ^ The type variables used in the type constructor.
-                                       -- Precisely, this list scopes over:
-                                       --
-                                       -- 1. The 'algTcStupidTheta'
-                                       --
-                                       -- 2. The cached types in 'algTyConRhs.NewTyCon'
-                                       -- 
-                                       -- 3. The family instance types if present
-                                       --
-                                       -- Note that it does /not/ scope over the data constructors.
-
-       algTcSelIds :: [Id],            -- ^ The record selectors of this type (possibly emptys)
-
-       algTcGadtSyntax  :: Bool,       -- ^ Was the data type declared with GADT syntax? If so,
-                                       -- that doesn't mean it's a true GADT; only that the "where"
-                                       --      form was used. This field is used only to guide
-                                       --      pretty-printing
-       algTcStupidTheta :: [PredType], -- ^ The \"stupid theta\" for the data type (always empty for GADTs).
-                                       -- A \"stupid theta\" is the context to the left of an algebraic type
-                                       -- declaration, e.g. @Eq a@ in the declaration @data Eq a => T a ...@.
-
-       algTcRhs :: AlgTyConRhs,        -- ^ Contains information about the data constructors of the algebraic type
-
-       algTcRec :: RecFlag,            -- ^ Tells us whether the data type is part of a mutually-recursive group or not
-
-       hasGenerics :: Bool,            -- ^ Whether generic (in the -XGenerics sense) to/from functions are
-                                       -- available in the exports of the data type's source module.
-
-       algTcParent :: TyConParent      -- ^ Gives the class or family declaration 'TyCon' for derived 'TyCon's
-                                       -- representing class or family instances, respectively. See also 'synTcParent'
+       tyConTyVars :: [TyVar],   -- ^ The type variables used in the type constructor.
+                                  -- Invariant: length tyvars = arity
+                                 -- Precisely, this list scopes over:
+                                 --
+                                 -- 1. The 'algTcStupidTheta'
+                                 -- 2. The cached types in 'algTyConRhs.NewTyCon'
+                                 -- 3. The family instance types if present
+                                 --
+                                 -- Note that it does /not/ scope over the data constructors.
+
+       algTcGadtSyntax  :: Bool,       -- ^ Was the data type declared with GADT syntax? 
+                                       -- If so, that doesn't mean it's a true GADT; 
+                                       -- only that the "where" form was used. 
+                                        -- This field is used only to guide pretty-printing
+
+       algTcStupidTheta :: [PredType], -- ^ The \"stupid theta\" for the data type 
+                                        -- (always empty for GADTs).
+                                       -- A \"stupid theta\" is the context to the left 
+                                       -- of an algebraic type declaration, 
+                                        -- e.g. @Eq a@ in the declaration 
+                                        --    @data Eq a => T a ...@.
+
+       algTcRhs :: AlgTyConRhs,  -- ^ Contains information about the 
+                                  -- data constructors of the algebraic type
+
+       algTcRec :: RecFlag,      -- ^ Tells us whether the data type is part 
+                                  -- of a mutually-recursive group or not
+
+       hasGenerics :: Bool,      -- ^ Whether generic (in the -XGenerics sense) 
+                                  -- to\/from functions are available in the exports 
+                                  -- of the data type's source module.
+
+       algTcParent :: TyConParent      -- ^ Gives the class or family declaration 'TyCon' 
+                                        -- for derived 'TyCon's representing class 
+                                        -- or family instances, respectively. 
+                                        -- See also 'synTcParent'
     }
 
-  -- | Represents the infinite family of tuple type constructors, @()@, @(a,b)@, @(# a, b #)@ etc.
+  -- | Represents the infinite family of tuple type constructors, 
+  --   @()@, @(a,b)@, @(# a, b #)@ etc.
   | TupleTyCon {
        tyConUnique :: Unique,
        tyConName   :: Name,
-       tyConKind   :: Kind,
+       tc_kind   :: Kind,
        tyConArity  :: Arity,
        tyConBoxed  :: Boxity,
        tyConTyVars :: [TyVar],
@@ -181,55 +361,60 @@ data TyCon
   | SynTyCon {
        tyConUnique  :: Unique,
        tyConName    :: Name,
-       tyConKind    :: Kind,
+       tc_kind    :: Kind,
        tyConArity   :: Arity,
 
        tyConTyVars  :: [TyVar],        -- Bound tyvars
 
-       synTcRhs     :: SynTyConRhs,    -- ^ Contains information about the expansion of the synonym
+       synTcRhs     :: SynTyConRhs,    -- ^ Contains information about the 
+                                        -- expansion of the synonym
 
-        synTcParent  :: TyConParent     -- ^ Gives the family declaration 'TyCon' of 'TyCon's representing family instances
+        synTcParent  :: TyConParent     -- ^ Gives the family declaration 'TyCon'
+                                        -- of 'TyCon's representing family instances
 
     }
 
-  -- | Primitive types; cannot be defined in Haskell. This includes the usual suspects (such as @Int#@)
-  -- as well as foreign-imported types and kinds
+  -- | Primitive types; cannot be defined in Haskell. This includes
+  -- the usual suspects (such as @Int#@) as well as foreign-imported
+  -- types and kinds
   | PrimTyCon {                        
        tyConUnique   :: Unique,
        tyConName     :: Name,
-       tyConKind     :: Kind,
+       tc_kind       :: Kind,
        tyConArity    :: Arity,         -- SLPJ Oct06: I'm not sure what the significance
                                        --             of the arity of a primtycon is!
 
-       primTyConRep  :: PrimRep,
-                       -- ^ Many primitive tycons are unboxed, but some are
-                       -- boxed (represented by pointers). This 'PrimRep' holds
-                       -- that information
+       primTyConRep  :: PrimRep,       -- ^ Many primitive tycons are unboxed, but some are
+                                               --   boxed (represented by pointers). This 'PrimRep'
+                                       --   holds that information.
+                                       -- Only relevant if tc_kind = *
+
+       isUnLifted   :: Bool,           -- ^ Most primitive tycons are unlifted 
+                                        --   (may not contain bottom)
+                                       --   but foreign-imported ones may be lifted
 
-       isUnLifted   :: Bool,           -- ^ Most primitive tycons are unlifted (may not contain bottom)
-                                       -- but foreign-imported ones may be lifted
-       tyConExtName :: Maybe FastString        -- ^ @Just e@ for foreign-imported types, holds the name of the imported thing
+       tyConExtName :: Maybe FastString   -- ^ @Just e@ for foreign-imported types, 
+                                           --   holds the name of the imported thing
     }
 
-  -- | Type coercions, such as @(:=:)@, @sym@, @trans@, @left@ and @right@.
-  -- INVARIANT: coercions are always fully applied
-  | CoercionTyCon {    
-       tyConUnique :: Unique,
-        tyConName   :: Name,
-       tyConArity  :: Arity,
-       coKindFun   :: [Type] -> (Type,Type)
-               -- ^ Function that when given a list of the type arguments to the 'TyCon'
-               -- constructs the types that the resulting coercion relates.
-               --
-               -- INVARIANT: 'coKindFun' is always applied to exactly 'tyConArity' args
-               -- E.g. for @trans (c1 :: ta=tb) (c2 :: tb=tc)@, the 'coKindFun' returns 
-               --      the kind as a pair of types: @(ta, tc)@
+  -- | Any types.  Like tuples, this is a potentially-infinite family of TyCons
+  --   one for each distinct Kind. They have no values at all.
+  --   Because there are infinitely many of them (like tuples) they are 
+  --   defined in GHC.Prim and have names like "Any(*->*)".  
+  --   Their Unique is derived from the OccName.
+  -- See Note [Any types] in TysPrim
+  | AnyTyCon {
+       tyConUnique  :: Unique,
+       tyConName    :: Name,
+       tc_kind      :: Kind    -- Never = *; that is done via PrimTyCon
+                               -- See Note [Any types] in TysPrim
     }
 
-  -- | Super-kinds. These are "kinds-of-kinds" and are never seen in Haskell source programs.
-  -- There are only two super-kinds: TY (aka "box"), which is the super-kind of kinds that 
-  -- construct types eventually, and CO (aka "diamond"), which is the super-kind of kinds
-  -- that just represent coercions.
+  -- | Super-kinds. These are "kinds-of-kinds" and are never seen in
+  -- Haskell source programs.  There are only two super-kinds: TY (aka
+  -- "box"), which is the super-kind of kinds that construct types
+  -- eventually, and CO (aka "diamond"), which is the super-kind of
+  -- kinds that just represent coercions.
   --
   -- Super-kinds have no kind themselves, and have arity zero
   | SuperKindTyCon {
@@ -243,84 +428,74 @@ type FieldLabel = Name
 -- | Represents right-hand-sides of 'TyCon's for algebraic types
 data AlgTyConRhs
 
-  -- | Says that we know nothing about this data type, except that it's represented
-  -- by a pointer.  Used when we export a data type abstractly into an .hi file.
+    -- | Says that we know nothing about this data type, except that
+    -- it's represented by a pointer.  Used when we export a data type
+    -- abstractly into an .hi file.
   = AbstractTyCon
 
-  -- | Represents an open type family without a fixed right hand
-  -- side.  Additional instances can appear at any time.
-  -- 
-  -- These are introduced by either a top level declaration:
-  --
-  -- > data T a :: *
-  --
-  -- Or an assoicated data type declaration, within a class declaration:
-  --
-  -- > class C a b where
-  -- >   data T b :: *
-
-  | OpenTyCon {
-
-      otArgPoss   :: Maybe [Int]
-       -- ^ @Nothing@ iff this is a top-level indexed type family.
-       -- @Just ns@ iff this is an associated (not top-level) family
-       --
-       -- In the latter case, for each 'TyVar' in the associated type declaration, 
-       -- @ns@ gives the position of that tyvar in the class argument list (starting 
-       -- from 0).
-       --
-       -- NB: The length of this list is less than the accompanying 'tyConArity' iff 
-       -- we have a higher kind signature.
-    }
-
-  -- | Information about those 'TyCon's derived from a @data@ declaration. This includes 
-  -- data types with no constructors at all.
+    -- | Represents an open type family without a fixed right hand
+    -- side.  Additional instances can appear at any time.
+    -- 
+    -- These are introduced by either a top level declaration:
+    --
+    -- > data T a :: *
+    --
+    -- Or an associated data type declaration, within a class declaration:
+    --
+    -- > class C a b where
+    -- >   data T b :: *
+  | DataFamilyTyCon
+
+    -- | Information about those 'TyCon's derived from a @data@
+    -- declaration. This includes data types with no constructors at
+    -- all.
   | DataTyCon {
        data_cons :: [DataCon],
-                       -- ^ The data type constructors; can be empty if the user declares
-                       --   the type to have no constructors
-                       --
-                       -- INVARIANT: Kept in order of increasing 'DataCon' tag
-                       
-                       --        (see the tag assignment in DataCon.mkDataCon)
-       is_enum :: Bool         -- ^ Cached value: is this an enumeration type? (See 'isEnumerationTyCon')
+                         -- ^ The data type constructors; can be empty if the user 
+                         --   declares the type to have no constructors
+                         --
+                         -- INVARIANT: Kept in order of increasing 'DataCon' tag
+                         --      (see the tag assignment in DataCon.mkDataCon)
+
+       is_enum :: Bool   -- ^ Cached value: is this an enumeration type? 
+                          --   See Note [Enumeration types]
     }
 
   -- | Information about those 'TyCon's derived from a @newtype@ declaration
   | NewTyCon {
-       data_con :: DataCon,    -- ^ The unique constructor for the @newtype@. It has no existentials
+       data_con :: DataCon,    -- ^ The unique constructor for the @newtype@. 
+                                --   It has no existentials
 
-       nt_rhs :: Type,         -- ^ Cached value: the argument type of the constructor, which
-                               -- is just the representation type of the 'TyCon' (remember that
-                               -- @newtype@s do not exist at runtime so need a different representation
-                               -- type).
+       nt_rhs :: Type,         -- ^ Cached value: the argument type of the constructor, 
+                               -- which is just the representation type of the 'TyCon'
+                               -- (remember that @newtype@s do not exist at runtime 
+                                -- so need a different representation type).
                                --
-                               -- The free 'TyVar's of this type are the 'tyConTyVars' from the corresponding
-                               -- 'TyCon'
+                               -- The free 'TyVar's of this type are the 'tyConTyVars' 
+                                -- from the corresponding 'TyCon'
 
        nt_etad_rhs :: ([TyVar], Type),
-                       -- ^ Same as the 'nt_rhs', but this time eta-reduced. Hence the list of 'TyVar's in 
-                       -- this field may be shorter than the declared arity of the 'TyCon'.
+                       -- ^ Same as the 'nt_rhs', but this time eta-reduced. 
+                        -- Hence the list of 'TyVar's in this field may be 
+                       -- shorter than the declared arity of the 'TyCon'.
                        
                        -- See Note [Newtype eta]
-      
-        nt_co :: Maybe TyCon   -- ^ A 'TyCon' (which is always a 'CoercionTyCon') that can have a 'Coercion' 
-                                -- extracted from it to create the @newtype@ from the representation 'Type'.
-                                --
-                                -- This field is optional for non-recursive @newtype@s only.
+        nt_co :: CoAxiom     -- The axiom coercion that creates the @newtype@ from 
+                             -- the representation 'Type'.
                                 
-                               -- See Note [Newtype coercions]
-                               -- Invariant: arity = #tvs in nt_etad_rhs;
-                               --      See Note [Newtype eta]
-                               -- Watch out!  If any newtypes become transparent
-                               -- again check Trac #1072.
+                             -- See Note [Newtype coercions]
+                             -- Invariant: arity = #tvs in nt_etad_rhs;
+                             --        See Note [Newtype eta]
+                             -- Watch out!  If any newtypes become transparent
+                             -- again check Trac #1072.
     }
 
--- | Extract those 'DataCon's that we are able to learn about. Note that visibility in this sense does not
--- correspond to visibility in the context of any particular user program!
+-- | Extract those 'DataCon's that we are able to learn about.  Note
+-- that visibility in this sense does not correspond to visibility in
+-- the context of any particular user program!
 visibleDataCons :: AlgTyConRhs -> [DataCon]
 visibleDataCons AbstractTyCon                = []
-visibleDataCons OpenTyCon {}                 = []
+visibleDataCons DataFamilyTyCon {}                   = []
 visibleDataCons (DataTyCon{ data_cons = cs }) = cs
 visibleDataCons (NewTyCon{ data_con = c })    = [c]
 
@@ -337,6 +512,27 @@ data TyConParent
   | ClassTyCon         
        Class           -- INVARIANT: the classTyCon of this Class is the current tycon
 
+  -- | An *associated* type of a class.  
+  | AssocFamilyTyCon   
+        Class          -- The class in whose declaration the family is declared
+                        -- The 'tyConTyVars' of this 'TyCon' may mention some
+                        -- of the same type variables as the classTyVars of the
+                        -- parent 'Class'.  E.g.
+                        --
+                        -- @
+                        --    class C a b where
+                        --      data T c a
+                        -- @
+                        --
+                        -- Here the 'a' is shared with the 'Class', and that is
+                        -- important. In an instance declaration we expect the
+                        -- two to be instantiated the same way.  Eg.
+                        --
+                        -- @
+                        --    instanc C [x] (Tree y) where
+                        --      data T c [x] = T1 x | T2 c
+                        -- @
+
   -- | Type constructors representing an instance of a type family. Parameters:
   --
   --  1) The type family in question
@@ -345,46 +541,65 @@ data TyConParent
   --  of the current 'TyCon' (not the family one). INVARIANT: 
   --  the number of types matches the arity of the family 'TyCon'
   --
-  --  3) A 'CoercionTyCon' identifying the representation
+  --  3) A 'CoTyCon' identifying the representation
   --  type with the type instance family
-  | FamilyTyCon
-       TyCon
-       [Type]
-       TyCon  -- c.f. Note [Newtype coercions]
+  | FamInstTyCon         -- See Note [Data type families]
+                         -- and Note [Type synonym families]
+       TyCon   -- The family TyCon
+       [Type]  -- Argument types (mentions the tyConTyVars of this TyCon)
+        CoAxiom   -- The coercion constructor
 
-       --
        -- E.g.  data intance T [a] = ...
        -- gives a representation tycon:
-       --      data :R7T a = ...
-       --      axiom co a :: T [a] ~ :R7T a
-       -- with :R7T's algTcParent = FamilyTyCon T [a] co
+       --      data R:TList a = ...
+       --      axiom co a :: T [a] ~ R:TList a
+       -- with R:TList's algTcParent = FamInstTyCon T [a] co
 
 -- | Checks the invariants of a 'TyConParent' given the appropriate type class name, if any
 okParent :: Name -> TyConParent -> Bool
-okParent _       NoParentTyCon                   = True
-okParent tc_name (ClassTyCon cls)                = tyConName (classTyCon cls) == tc_name
-okParent _       (FamilyTyCon fam_tc tys _co_tc) = tyConArity fam_tc == length tys
+okParent _       NoParentTyCon                    = True
+okParent tc_name (AssocFamilyTyCon cls)           = tc_name `elem` map tyConName (classATs cls)
+okParent tc_name (ClassTyCon cls)                 = tc_name == tyConName (classTyCon cls)
+okParent _       (FamInstTyCon fam_tc tys _co_tc) = tyConArity fam_tc == length tys
+
+isNoParent :: TyConParent -> Bool
+isNoParent NoParentTyCon = True
+isNoParent _             = False
 
 --------------------
 
 -- | Information pertaining to the expansion of a type synonym (@type@)
 data SynTyConRhs
-  = OpenSynTyCon Kind          
-                (Maybe [Int])  -- ^ A Type family synonym. The /result/ 'Kind' is
-                               -- given for associated families, and in this case the
-                               -- list of @Int@s is not empty, and for each 'TyVar' in
-                               -- the associated type declaration, it gives the position
-                               -- of that 'TyVar' in the class argument list (starting
-                               -- from 0). 
-                               --
-                               -- NB: The length of this list will be less than 'tyConArity' iff
-                               -- the family has a higher kind signature.
-
-  | SynonymTyCon Type   -- ^ The synonym mentions head type variables. It acts as a
-                       -- template for the expansion when the 'TyCon' is applied to some
-                       -- types.
+  = -- | An ordinary type synonyn.
+    SynonymTyCon      
+       Type          -- This 'Type' is the rhs, and may mention from 'tyConTyVars'. 
+                     -- It acts as a template for the expansion when the 'TyCon' 
+                      -- is applied to some types.
+
+   -- | A type synonym family  e.g. @type family F x y :: * -> *@
+   | SynFamilyTyCon
 \end{code}
 
+Note [Enumeration types]
+~~~~~~~~~~~~~~~~~~~~~~~~
+We define datatypes with no constructors to *not* be
+enumerations; this fixes trac #2578,  Otherwise we
+end up generating an empty table for
+  <mod>_<type>_closure_tbl
+which is used by tagToEnum# to map Int# to constructors
+in an enumeration. The empty table apparently upset
+the linker.
+
+Moreover, all the data constructor must be enumerations, meaning
+they have type  (forall abc. T a b c).  GADTs are not enumerations.
+For example consider
+    data T a where
+      T1 :: T Int
+      T2 :: T Bool
+      T3 :: T a
+What would [T1 ..] be?  [T1,T3] :: T Int? Easiest thing is to exclude them.
+See Trac #4528.
+
 Note [Newtype coercions]
 ~~~~~~~~~~~~~~~~~~~~~~~~
 The NewTyCon field nt_co is a a TyCon (a coercion constructor in fact)
@@ -393,8 +608,8 @@ 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 CoercionTyCon, so it does not have a kind on its
+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
@@ -403,22 +618,22 @@ ending with the same type variables as the left hand side, we
 
    newtype S a = MkT [a]
 
-then we would generate the arity 0 coercion CoS : S :=: [].  The
+then we would generate the arity 0 coercion CoS : S ~ [].  The
 primary reason we do this is to make newtype deriving cleaner.
 
 In the paper we'd write
-       axiom CoT : (forall t. T t) :=: (forall t. [t])
+       axiom CoT : (forall t. T t) ~ (forall t. [t])
 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, CoercionTyCon,
+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]
+       axiom CoT t :  T t ~ [t]
 
 Note [Newtype eta]
 ~~~~~~~~~~~~~~~~~~
@@ -459,37 +674,29 @@ so the coercion tycon CoT must have
  and   arity:   0
 
 
-Note [Indexed data types] (aka data type families)
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-   See also Note [Wrappers for data instance tycons] in MkId.lhs
-
-Consider
-       data family T a
-
-       data instance T (b,c) where
-         T1 :: b -> c -> T (b,c)
-
-Then
-  * T is the "family TyCon"
-
-  * We make "representation TyCon" :R1T, thus:
-       data :R1T b c where
-         T1 :: forall b c. b -> c -> :R1T b c
-
-  * It has a top-level coercion connecting it to the family TyCon
-
-       axiom :Co:R1T b c : T (b,c) ~ :R1T b c
-
-  * The data contructor T1 has a wrapper (which is what the source-level
-    "T1" invokes):
-
-       $WT1 :: forall b c. b -> c -> T (b,c)
-       $WT1 b c (x::b) (y::c) = T1 b c x y `cast` sym (:Co:R1T b c)
+%************************************************************************
+%*                                                                     *
+                    Coercion axioms
+%*                                                                     *
+%************************************************************************
 
-  * The representation TyCon :R1T has an AlgTyConParent of
+\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
+    }
 
-       FamilyTyCon T [(b,c)] :Co:R1T
+coAxiomArity :: CoAxiom -> Arity
+coAxiomArity ax = length (co_ax_tvs ax)
 
+coAxiomName :: CoAxiom -> Name
+coAxiomName = co_ax_name
+\end{code}
 
 
 %************************************************************************
@@ -499,7 +706,7 @@ Then
 %************************************************************************
 
 A PrimRep is somewhat similar to a CgRep (see codeGen/SMRep) and a
-MachRep (see cmm/MachOp), although each of these types has a distinct
+MachRep (see cmm/CmmExpr), although each of these types has a distinct
 and clearly defined purpose:
 
   - A PrimRep is a CgRep + information about signedness + information
@@ -565,43 +772,44 @@ mkFunTyCon name kind
   = FunTyCon { 
        tyConUnique = nameUnique name,
        tyConName   = name,
-       tyConKind   = kind,
+       tc_kind   = kind,
        tyConArity  = 2
     }
 
--- | This is the making of an algebraic 'TyCon'. Notably, you have to pass in the generic (in the -XGenerics sense)
--- information about the type constructor - you can get hold of it easily (see Generics module)
+-- | This is the making of an algebraic 'TyCon'. Notably, you have to
+-- pass in the generic (in the -XGenerics sense) information about the
+-- type constructor - you can get hold of it easily (see Generics
+-- module)
 mkAlgTyCon :: Name
            -> Kind              -- ^ Kind of the resulting 'TyCon'
-           -> [TyVar]           -- ^ 'TyVar's scoped over: see 'tyConTyVars'. Arity is inferred from the length of this list
+           -> [TyVar]           -- ^ 'TyVar's scoped over: see 'tyConTyVars'. 
+                                --   Arity is inferred from the length of this list
            -> [PredType]        -- ^ Stupid theta: see 'algTcStupidTheta'
            -> AlgTyConRhs       -- ^ Information about dat aconstructors
-           -> [Id]              -- ^ Selector 'Id's
            -> TyConParent
            -> RecFlag           -- ^ Is the 'TyCon' recursive?
            -> Bool              -- ^ Does it have generic functions? See 'hasGenerics'
            -> Bool              -- ^ Was the 'TyCon' declared with GADT syntax?
            -> TyCon
-mkAlgTyCon name kind tyvars stupid rhs sel_ids parent is_rec gen_info gadt_syn
+mkAlgTyCon name kind tyvars stupid rhs parent is_rec gen_info gadt_syn
   = AlgTyCon { 
        tyConName        = name,
        tyConUnique      = nameUnique name,
-       tyConKind        = kind,
+       tc_kind          = kind,
        tyConArity       = length tyvars,
        tyConTyVars      = tyvars,
        algTcStupidTheta = stupid,
        algTcRhs         = rhs,
-       algTcSelIds      = sel_ids,
        algTcParent      = ASSERT( okParent name parent ) parent,
        algTcRec         = is_rec,
        algTcGadtSyntax  = gadt_syn,
-       hasGenerics = gen_info
+       hasGenerics      = gen_info
     }
 
 -- | Simpler specialization of 'mkAlgTyCon' for classes
 mkClassTyCon :: Name -> Kind -> [TyVar] -> AlgTyConRhs -> Class -> RecFlag -> TyCon
 mkClassTyCon name kind tyvars rhs clas is_rec =
-  mkAlgTyCon name kind tyvars [] rhs [] (ClassTyCon clas) is_rec False False
+  mkAlgTyCon name kind tyvars [] rhs (ClassTyCon clas) is_rec False False
 
 mkTupleTyCon :: Name 
              -> Kind    -- ^ Kind of the resulting 'TyCon'
@@ -615,7 +823,7 @@ mkTupleTyCon name kind arity tyvars con boxed gen_info
   = TupleTyCon {
        tyConUnique = nameUnique name,
        tyConName = name,
-       tyConKind = kind,
+       tc_kind = kind,
        tyConArity = arity,
        tyConBoxed = boxed,
        tyConTyVars = tyvars,
@@ -636,7 +844,7 @@ mkForeignTyCon name ext_name kind arity
   = PrimTyCon {
        tyConName    = name,
        tyConUnique  = nameUnique name,
-       tyConKind    = kind,
+       tc_kind    = kind,
        tyConArity   = arity,
        primTyConRep = PtrRep, -- they all do
        isUnLifted   = False,
@@ -649,10 +857,10 @@ mkPrimTyCon :: Name  -> Kind -> Arity -> PrimRep -> TyCon
 mkPrimTyCon name kind arity rep
   = mkPrimTyCon' name kind arity rep True  
 
--- | Create the special void 'TyCon' which is unlifted and has 'VoidRep'
-mkVoidPrimTyCon :: Name -> Kind -> Arity -> TyCon
-mkVoidPrimTyCon name kind arity 
-  = mkPrimTyCon' name kind arity VoidRep True  
+-- | Kind constructors
+mkKindTyCon :: Name -> Kind -> TyCon
+mkKindTyCon name kind
+  = mkPrimTyCon' name kind 0 VoidRep True  
 
 -- | Create a lifted primitive 'TyCon' such as @RealWorld@
 mkLiftedPrimTyCon :: Name  -> Kind -> Arity -> PrimRep -> TyCon
@@ -664,7 +872,7 @@ mkPrimTyCon' name kind arity rep is_unlifted
   = PrimTyCon {
        tyConName    = name,
        tyConUnique  = nameUnique name,
-       tyConKind    = kind,
+       tc_kind    = kind,
        tyConArity   = arity,
        primTyConRep = rep,
        isUnLifted   = is_unlifted,
@@ -677,22 +885,18 @@ mkSynTyCon name kind tyvars rhs parent
   = SynTyCon { 
        tyConName = name,
        tyConUnique = nameUnique name,
-       tyConKind = kind,
+       tc_kind = kind,
        tyConArity = length tyvars,
        tyConTyVars = tyvars,
        synTcRhs = rhs,
         synTcParent = parent
     }
 
--- | Create a coercion 'TyCon'
-mkCoercionTyCon :: Name -> Arity -> ([Type] -> (Type,Type)) -> TyCon
-mkCoercionTyCon name arity kindRule
-  = CoercionTyCon {
-        tyConName = name,
-        tyConUnique = nameUnique name,
-        tyConArity = arity,
-        coKindFun = kindRule
-    }
+mkAnyTyCon :: Name -> Kind -> TyCon
+mkAnyTyCon name kind 
+  = AnyTyCon {  tyConName = name,
+               tc_kind = kind,
+               tyConUnique = nameUnique name }
 
 -- | Create a super-kind 'TyCon'
 mkSuperKindTyCon :: Name -> TyCon -- Super kinds always have arity zero
@@ -730,7 +934,8 @@ isUnLiftedTyCon (PrimTyCon  {isUnLifted = is_unlifted}) = is_unlifted
 isUnLiftedTyCon (TupleTyCon {tyConBoxed = boxity})      = not (isBoxed boxity)
 isUnLiftedTyCon _                                      = False
 
--- | Returns @True@ if the supplied 'TyCon' resulted from either a @data@ or @newtype@ declaration
+-- | Returns @True@ if the supplied 'TyCon' resulted from either a
+-- @data@ or @newtype@ declaration
 isAlgTyCon :: TyCon -> Bool
 isAlgTyCon (AlgTyCon {})   = True
 isAlgTyCon (TupleTyCon {}) = True
@@ -749,7 +954,7 @@ isDataTyCon :: TyCon -> Bool
 --     get an info table.  The family declaration 'TyCon' does not
 isDataTyCon (AlgTyCon {algTcRhs = rhs})
   = case rhs of
-        OpenTyCon {}  -> False
+        DataFamilyTyCon {}  -> False
        DataTyCon {}  -> True
        NewTyCon {}   -> False
        AbstractTyCon -> False   -- We don't know, so return False
@@ -764,11 +969,11 @@ isNewTyCon _                                   = False
 -- | Take a 'TyCon' apart into the 'TyVar's it scopes over, the 'Type' it expands
 -- into, and (possibly) a coercion from the representation type to the @newtype@.
 -- Returns @Nothing@ if this is not possible.
-unwrapNewTyCon_maybe :: TyCon -> Maybe ([TyVar], Type, Maybe TyCon)
+unwrapNewTyCon_maybe :: TyCon -> Maybe ([TyVar], Type, CoAxiom)
 unwrapNewTyCon_maybe (AlgTyCon { tyConTyVars = tvs, 
-                                algTcRhs = NewTyCon { nt_co = mb_co, 
+                                algTcRhs = NewTyCon { nt_co = co, 
                                                       nt_rhs = rhs }})
-                          = Just (tvs, rhs, mb_co)
+                          = Just (tvs, rhs, co)
 unwrapNewTyCon_maybe _     = Nothing
 
 isProductTyCon :: TyCon -> Bool
@@ -798,13 +1003,11 @@ isSynTyCon _              = False
 -- right hand side to which a synonym family application can expand.
 --
 
--- | Is this a synonym 'TyCon' that can have no further instances appear?
-isClosedSynTyCon :: TyCon -> Bool
-isClosedSynTyCon tycon = isSynTyCon tycon && not (isOpenTyCon tycon)
-
--- | Is this a synonym 'TyCon' that can have may have further instances appear?
-isOpenSynTyCon :: TyCon -> Bool
-isOpenSynTyCon tycon = isSynTyCon tycon && isOpenTyCon tycon
+isDecomposableTyCon :: TyCon -> Bool
+-- True iff we can decompose (T a b c) into ((T a b) c)
+-- Specifically NOT true of synonyms (open and otherwise)
+isDecomposableTyCon (SynTyCon {}) = False
+isDecomposableTyCon _other        = True
 
 -- | Is this an algebraic 'TyCon' declared with the GADT syntax?
 isGadtSyntaxTyCon :: TyCon -> Bool
@@ -813,37 +1016,48 @@ isGadtSyntaxTyCon _                                    = False
 
 -- | Is this an algebraic 'TyCon' which is just an enumeration of values?
 isEnumerationTyCon :: TyCon -> Bool
+-- See Note [Enumeration types] in TyCon
 isEnumerationTyCon (AlgTyCon {algTcRhs = DataTyCon { is_enum = res }}) = res
+isEnumerationTyCon (TupleTyCon {tyConArity = arity}) = arity == 0
 isEnumerationTyCon _                                                   = False
 
 -- | Is this a 'TyCon', synonym or otherwise, that may have further instances appear?
-isOpenTyCon :: TyCon -> Bool
-isOpenTyCon (SynTyCon {synTcRhs = OpenSynTyCon _ _}) = True
-isOpenTyCon (AlgTyCon {algTcRhs = OpenTyCon {}    }) = True
-isOpenTyCon _                                       = False
-
--- | Extract the mapping from 'TyVar' indexes to indexes in the corresponding family
--- argument lists form an open 'TyCon' of any sort, if the given 'TyCon' is indeed
--- such a beast and that information is available
-assocTyConArgPoss_maybe :: TyCon -> Maybe [Int]
-assocTyConArgPoss_maybe (AlgTyCon { 
-                          algTcRhs = OpenTyCon {otArgPoss = poss}})  = poss
-assocTyConArgPoss_maybe (SynTyCon { synTcRhs = OpenSynTyCon _ poss }) = poss
-assocTyConArgPoss_maybe _ = Nothing
+isFamilyTyCon :: TyCon -> Bool
+isFamilyTyCon (SynTyCon {synTcRhs = SynFamilyTyCon {}})  = True
+isFamilyTyCon (AlgTyCon {algTcRhs = DataFamilyTyCon {}}) = True
+isFamilyTyCon _        = False
+
+-- | Is this a synonym 'TyCon' that can have may have further instances appear?
+isSynFamilyTyCon :: TyCon -> Bool
+isSynFamilyTyCon (SynTyCon {synTcRhs = SynFamilyTyCon {}}) = True
+isSynFamilyTyCon _ = False
+
+-- | Is this a synonym 'TyCon' that can have may have further instances appear?
+isDataFamilyTyCon :: TyCon -> Bool
+isDataFamilyTyCon (AlgTyCon {algTcRhs = DataFamilyTyCon {}}) = True
+isDataFamilyTyCon _ = False
+
+-- | Is this a synonym 'TyCon' that can have no further instances appear?
+isClosedSynTyCon :: TyCon -> Bool
+isClosedSynTyCon tycon = isSynTyCon tycon && not (isFamilyTyCon tycon)
+
+-- | Injective 'TyCon's can be decomposed, so that
+--     T ty1 ~ T ty2  =>  ty1 ~ ty2
+isInjectiveTyCon :: TyCon -> Bool
+isInjectiveTyCon tc = not (isSynTyCon tc)
+       -- Ultimately we may have injective associated types
+        -- in which case this test will become more interesting
+       --
+        -- It'd be unusual to call isInjectiveTyCon on a regular H98
+       -- type synonym, because you should probably have expanded it first
+       -- But regardless, it's not injective!
 
 -- | Are we able to extract informationa 'TyVar' to class argument list
 -- mappping from a given 'TyCon'?
 isTyConAssoc :: TyCon -> Bool
-isTyConAssoc = isJust . assocTyConArgPoss_maybe
-
--- | Sets up a 'TyVar' to family argument-list mapping in the given 'TyCon' if it is
--- an open 'TyCon'. Panics otherwise
-setTyConArgPoss :: TyCon -> [Int] -> TyCon
-setTyConArgPoss tc@(AlgTyCon { algTcRhs = rhs })               poss = 
-  tc { algTcRhs = rhs {otArgPoss = Just poss} }
-setTyConArgPoss tc@(SynTyCon { synTcRhs = OpenSynTyCon ki _ }) poss = 
-  tc { synTcRhs = OpenSynTyCon ki (Just poss) }
-setTyConArgPoss tc _ = pprPanic "setTyConArgPoss" (ppr tc)
+isTyConAssoc tc = case tyConParent tc of
+                     AssocFamilyTyCon {} -> True
+                     _                   -> False
 
 -- The unit tycon didn't used to be classed as a tuple tycon
 -- but I thought that was silly so I've undone it
@@ -894,18 +1108,10 @@ isSuperKindTyCon :: TyCon -> Bool
 isSuperKindTyCon (SuperKindTyCon {}) = True
 isSuperKindTyCon _                   = False
 
--- | Attempt to pull a 'TyCon' apart into the arity and 'coKindFun' of
--- a coercion 'TyCon'. Returns @Nothing@ if the 'TyCon' is not of the
--- appropriate kind
-isCoercionTyCon_maybe :: TyCon -> Maybe (Arity, [Type] -> (Type,Type))
-isCoercionTyCon_maybe (CoercionTyCon {tyConArity = ar, coKindFun = rule}) 
-  = Just (ar, rule)
-isCoercionTyCon_maybe _ = Nothing
-
--- | Is this a 'TyCon' that represents a coercion?
-isCoercionTyCon :: TyCon -> Bool
-isCoercionTyCon (CoercionTyCon {}) = True
-isCoercionTyCon _                  = False
+-- | Is this an AnyTyCon?
+isAnyTyCon :: TyCon -> Bool
+isAnyTyCon (AnyTyCon {}) = True
+isAnyTyCon _              = False
 
 -- | Identifies implicit tycons that, in particular, do not go into interface
 -- files (because they are implicitly reconstructed when the interface is
@@ -925,7 +1131,7 @@ isImplicitTyCon tycon | isTyConAssoc tycon           = True
                                                       isTupleTyCon tycon
 isImplicitTyCon _other                               = True
         -- catches: FunTyCon, PrimTyCon, 
-        -- CoercionTyCon, SuperKindTyCon
+        -- CoTyCon, SuperKindTyCon
 \end{code}
 
 
@@ -936,14 +1142,15 @@ isImplicitTyCon _other                               = True
 \begin{code}
 tcExpandTyCon_maybe, coreExpandTyCon_maybe 
        :: TyCon 
-       -> [Type]                       -- ^ Arguments to 'TyCon'
-       -> Maybe ([(TyVar,Type)],       
+       -> [tyco]                 -- ^ Arguments to 'TyCon'
+       -> Maybe ([(TyVar,tyco)],       
                  Type,                 
-                 [Type])               -- ^ Returns a 'TyVar' substitution, the body type
-                                        -- of the synonym (not yet substituted) and any arguments
-                                        -- remaining from the application
+                 [tyco])         -- ^ Returns a 'TyVar' substitution, the body type
+                                  -- of the synonym (not yet substituted) and any arguments
+                                  -- remaining from the application
 
--- ^ Used to create the view the /typechecker/ has on 'TyCon's. We expand (closed) synonyms only, cf. 'coreExpandTyCon_maybe'
+-- ^ Used to create the view the /typechecker/ has on 'TyCon's. 
+-- We expand (closed) synonyms only, cf. 'coreExpandTyCon_maybe'
 tcExpandTyCon_maybe (SynTyCon {tyConTyVars = tvs, 
                               synTcRhs = SynonymTyCon rhs }) tys
    = expand tvs rhs tys
@@ -951,37 +1158,45 @@ tcExpandTyCon_maybe _ _ = Nothing
 
 ---------------
 
--- ^ Used to create the view /Core/ has on 'TyCon's. We expand not only closed synonyms like 'tcExpandTyCon_maybe',
+-- ^ Used to create the view /Core/ has on 'TyCon's. We expand 
+-- not only closed synonyms like 'tcExpandTyCon_maybe',
 -- but also non-recursive @newtype@s
-coreExpandTyCon_maybe (AlgTyCon {algTcRec = NonRecursive,      -- Not recursive
-         algTcRhs = NewTyCon { nt_etad_rhs = etad_rhs, nt_co = Nothing }}) tys
-   = case etad_rhs of  -- Don't do this in the pattern match, lest we accidentally
-                       -- match the etad_rhs of a *recursive* newtype
-       (tvs,rhs) -> expand tvs rhs tys
-
 coreExpandTyCon_maybe tycon tys = tcExpandTyCon_maybe tycon tys
 
 
 ----------------
-expand :: [TyVar] -> Type                      -- Template
-       -> [Type]                               -- Args
-       -> Maybe ([(TyVar,Type)], Type, [Type]) -- Expansion
+expand :: [TyVar] -> Type                 -- Template
+       -> [a]                             -- Args
+       -> Maybe ([(TyVar,a)], Type, [a])  -- Expansion
 expand tvs rhs tys
   = case n_tvs `compare` length tys of
        LT -> Just (tvs `zip` tys, rhs, drop n_tvs tys)
        EQ -> Just (tvs `zip` tys, rhs, [])
-       GT -> Nothing
+        GT -> Nothing
    where
      n_tvs = length tvs
 \end{code}
 
 \begin{code}
--- | Does this 'TyCon' have any generic to/from functions available? See also 'hasGenerics'
+-- | Does this 'TyCon' have any generic to\/from functions available? See also 'hasGenerics'
 tyConHasGenerics :: TyCon -> Bool
 tyConHasGenerics (AlgTyCon {hasGenerics = hg})   = hg
 tyConHasGenerics (TupleTyCon {hasGenerics = hg}) = hg
 tyConHasGenerics _                               = False        -- Synonyms
 
+tyConKind :: TyCon -> Kind
+tyConKind (FunTyCon   { tc_kind = k }) = k
+tyConKind (AlgTyCon   { tc_kind = k }) = k
+tyConKind (TupleTyCon { tc_kind = k }) = k
+tyConKind (SynTyCon   { tc_kind = k }) = k
+tyConKind (PrimTyCon  { tc_kind = k }) = k
+tyConKind (AnyTyCon   { tc_kind = k }) = k
+tyConKind tc = pprPanic "tyConKind" (ppr tc)   -- SuperKindTyCon and CoTyCon
+
+tyConHasKind :: TyCon -> Bool
+tyConHasKind (SuperKindTyCon {}) = False
+tyConHasKind _                   = True
+
 -- | As 'tyConDataCons_maybe', but returns the empty list of constructors if no constructors
 -- could be found
 tyConDataCons :: TyCon -> [DataCon]
@@ -1002,21 +1217,17 @@ tyConDataCons_maybe _                                                      = Not
 tyConFamilySize  :: TyCon -> Int
 tyConFamilySize (AlgTyCon   {algTcRhs = DataTyCon {data_cons = cons}}) = 
   length cons
-tyConFamilySize (AlgTyCon   {algTcRhs = NewTyCon {}})                  = 1
-tyConFamilySize (AlgTyCon   {algTcRhs = OpenTyCon {}})                 = 0
-tyConFamilySize (TupleTyCon {})                                               = 1
+tyConFamilySize (AlgTyCon   {algTcRhs = NewTyCon {}})        = 1
+tyConFamilySize (AlgTyCon   {algTcRhs = DataFamilyTyCon {}}) = 0
+tyConFamilySize (TupleTyCon {})                                     = 1
 tyConFamilySize other = pprPanic "tyConFamilySize:" (ppr other)
 
--- | Extract the record selector 'Id's from an algebraic 'TyCon' and returns the empty list otherwise
-tyConSelIds :: TyCon -> [Id]
-tyConSelIds (AlgTyCon {algTcSelIds = fs}) = fs
-tyConSelIds _                             = []
-
 -- | Extract an 'AlgTyConRhs' with information about data constructors from an algebraic or tuple
 -- 'TyCon'. Panics for any other sort of 'TyCon'
 algTyConRhs :: TyCon -> AlgTyConRhs
-algTyConRhs (AlgTyCon {algTcRhs = rhs})  = rhs
-algTyConRhs (TupleTyCon {dataCon = con}) = DataTyCon { data_cons = [con], is_enum = False }
+algTyConRhs (AlgTyCon {algTcRhs = rhs}) = rhs
+algTyConRhs (TupleTyCon {dataCon = con, tyConArity = arity})
+    = DataTyCon { data_cons = [con], is_enum = arity == 0 }
 algTyConRhs other = pprPanic "algTyConRhs" (ppr other)
 \end{code}
 
@@ -1036,9 +1247,14 @@ newTyConEtadRhs tycon = pprPanic "newTyConEtadRhs" (ppr tycon)
 -- | Extracts the @newtype@ coercion from such a 'TyCon', which can be used to construct something
 -- with the @newtype@s type from its representation type (right hand side). If the supplied 'TyCon'
 -- is not a @newtype@, returns @Nothing@
-newTyConCo_maybe :: TyCon -> Maybe TyCon
-newTyConCo_maybe (AlgTyCon {algTcRhs = NewTyCon { nt_co = co }}) = co
-newTyConCo_maybe _                                              = Nothing
+newTyConCo_maybe :: TyCon -> Maybe CoAxiom
+newTyConCo_maybe (AlgTyCon {algTcRhs = NewTyCon { nt_co = co }}) = Just co
+newTyConCo_maybe _                                              = Nothing
+
+newTyConCo :: TyCon -> CoAxiom
+newTyConCo tc = case newTyConCo_maybe tc of
+                Just co -> co
+                 Nothing -> pprPanic "newTyConCo" (ppr tc)
 
 -- | Find the primitive representation of a 'TyCon'
 tyConPrimRep :: TyCon -> PrimRep
@@ -1076,11 +1292,6 @@ synTyConType :: TyCon -> Type
 synTyConType tc = case synTcRhs tc of
                    SynonymTyCon t -> t
                    _              -> pprPanic "synTyConType" (ppr tc)
-
--- | Find the 'Kind' of an open type synonym. Panics if the 'TyCon' is not an open type synonym
-synTyConResKind :: TyCon -> Kind
-synTyConResKind (SynTyCon {synTcRhs = OpenSynTyCon kind _}) = kind
-synTyConResKind tycon  = pprPanic "synTyConResKind" (ppr tycon)
 \end{code}
 
 \begin{code}
@@ -1089,13 +1300,10 @@ synTyConResKind tycon  = pprPanic "synTyConResKind" (ppr tycon)
 -- has more than one constructor, or represents a primitive or function type constructor then
 -- @Nothing@ is returned. In any other case, the function panics
 tyConSingleDataCon_maybe :: TyCon -> Maybe DataCon
-tyConSingleDataCon_maybe (AlgTyCon {algTcRhs = DataTyCon {data_cons = [c] }}) = Just c
-tyConSingleDataCon_maybe (AlgTyCon {algTcRhs = NewTyCon { data_con = c }})    = Just c
-tyConSingleDataCon_maybe (AlgTyCon {})          = Nothing
-tyConSingleDataCon_maybe (TupleTyCon {dataCon = con}) = Just con
-tyConSingleDataCon_maybe (PrimTyCon {})               = Nothing
-tyConSingleDataCon_maybe (FunTyCon {})                = Nothing  -- case at funty
-tyConSingleDataCon_maybe tc = pprPanic "tyConSingleDataCon_maybe: unexpected tycon " $ ppr tc
+tyConSingleDataCon_maybe (TupleTyCon {dataCon = c})                           = Just c
+tyConSingleDataCon_maybe (AlgTyCon {algTcRhs = DataTyCon { data_cons = [c] }}) = Just c
+tyConSingleDataCon_maybe (AlgTyCon {algTcRhs = NewTyCon { data_con = c }})     = Just c
+tyConSingleDataCon_maybe _                                                    = Nothing
 \end{code}
 
 \begin{code}
@@ -1110,33 +1318,42 @@ tyConClass_maybe :: TyCon -> Maybe Class
 tyConClass_maybe (AlgTyCon {algTcParent = ClassTyCon clas}) = Just clas
 tyConClass_maybe _                                          = Nothing
 
+----------------------------------------------------------------------------
+tyConParent :: TyCon -> TyConParent
+tyConParent (AlgTyCon {algTcParent = parent}) = parent
+tyConParent (SynTyCon {synTcParent = parent}) = parent
+tyConParent _                                 = NoParentTyCon
+
+----------------------------------------------------------------------------
 -- | Is this 'TyCon' that for a family instance, be that for a synonym or an
 -- algebraic family instance?
 isFamInstTyCon :: TyCon -> Bool
-isFamInstTyCon (AlgTyCon {algTcParent = FamilyTyCon _ _ _ }) = True
-isFamInstTyCon (SynTyCon {synTcParent = FamilyTyCon _ _ _ }) = True
-isFamInstTyCon _                                             = False
+isFamInstTyCon tc = case tyConParent tc of
+                      FamInstTyCon {} -> True
+                      _               -> False
+
+tyConFamInstSig_maybe :: TyCon -> Maybe (TyCon, [Type], CoAxiom)
+tyConFamInstSig_maybe tc
+  = case tyConParent tc of
+      FamInstTyCon f ts co_tc -> Just (f, ts, co_tc)
+      _                       -> Nothing
 
 -- | If this 'TyCon' is that of a family instance, return the family in question
 -- and the instance types. Otherwise, return @Nothing@
 tyConFamInst_maybe :: TyCon -> Maybe (TyCon, [Type])
-tyConFamInst_maybe (AlgTyCon {algTcParent = FamilyTyCon fam instTys _}) = 
-  Just (fam, instTys)
-tyConFamInst_maybe (SynTyCon {synTcParent = FamilyTyCon fam instTys _}) = 
-  Just (fam, instTys)
-tyConFamInst_maybe _                                                    = 
-  Nothing
+tyConFamInst_maybe tc
+  = case tyConParent tc of
+      FamInstTyCon f ts _ -> Just (f, ts)
+      _                   -> Nothing
 
 -- | If this 'TyCon' is that of a family instance, return a 'TyCon' which represents 
 -- a coercion identifying the representation type with the type instance family.
 -- Otherwise, return @Nothing@
-tyConFamilyCoercion_maybe :: TyCon -> Maybe TyCon
-tyConFamilyCoercion_maybe (AlgTyCon {algTcParent = FamilyTyCon _ _ coe}) = 
-  Just coe
-tyConFamilyCoercion_maybe (SynTyCon {synTcParent = FamilyTyCon _ _ coe}) = 
-  Just coe
-tyConFamilyCoercion_maybe _                                              =
-  Nothing
+tyConFamilyCoercion_maybe :: TyCon -> Maybe CoAxiom
+tyConFamilyCoercion_maybe tc
+  = case tyConParent tc of
+      FamInstTyCon _ _ co -> Just co
+      _                   -> Nothing
 \end{code}
 
 
@@ -1171,4 +1388,43 @@ instance Outputable TyCon where
 
 instance NamedThing TyCon where
     getName = tyConName
+
+instance Data.Typeable TyCon where
+    typeOf _ = Data.mkTyConApp (Data.mkTyCon "TyCon") []
+
+instance Data.Data TyCon where
+    -- don't traverse?
+    toConstr _   = abstractConstr "TyCon"
+    gunfold _ _  = error "gunfold"
+    dataTypeOf _ = mkNoRepType "TyCon"
+
+-------------------
+instance Eq CoAxiom where
+    a == b = case (a `compare` b) of { EQ -> True;   _ -> False }
+    a /= b = case (a `compare` b) of { EQ -> False;  _ -> True  }
+  
+instance Ord CoAxiom where
+    a <= b = case (a `compare` b) of { LT -> True;  EQ -> True;  GT -> False }
+    a <  b = case (a `compare` b) of { LT -> True;  EQ -> False; GT -> False }
+    a >= b = case (a `compare` b) of { LT -> False; EQ -> True;  GT -> True  }
+    a >  b = case (a `compare` b) of { LT -> False; EQ -> False; GT -> True  }
+    compare a b = getUnique a `compare` getUnique b  
+
+instance Uniquable CoAxiom where
+    getUnique = co_ax_unique
+
+instance Outputable CoAxiom where
+    ppr = ppr . getName
+
+instance NamedThing CoAxiom where
+    getName = co_ax_name
+
+instance Data.Typeable CoAxiom where
+    typeOf _ = Data.mkTyConApp (Data.mkTyCon "CoAxiom") []
+
+instance Data.Data CoAxiom where
+    -- don't traverse?
+    toConstr _   = abstractConstr "CoAxiom"
+    gunfold _ _  = error "gunfold"
+    dataTypeOf _ = mkNoRepType "CoAxiom"
 \end{code}