Put liftStringName into the known-key names
[ghc-hetmet.git] / compiler / types / TyCon.lhs
index 958a0cb..12f3935 100644 (file)
@@ -8,11 +8,12 @@ The @TyCon@ datatype
 \begin{code}
 module TyCon(
         -- * Main TyCon data types
-       TyCon, FieldLabel, CoTyConKindChecker,
+       TyCon, FieldLabel, 
 
        AlgTyConRhs(..), visibleDataCons, 
         TyConParent(..), 
        SynTyConRhs(..),
+        CoTyConDesc(..),
        AssocFamilyPermutation,
 
         -- ** Constructing TyCons
@@ -94,9 +95,128 @@ import Maybes
 import Outputable
 import FastString
 import Constants
+import Util
+import qualified Data.Data as Data
 import Data.List( elemIndex )
 \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...
+
+* 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!
+
+* 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".
+
+* 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
+       FamilyTyCon 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
+
+       FamilyTyCon 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}
@@ -114,8 +234,8 @@ import Data.List( elemIndex )
 --
 -- 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
+-- 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.
@@ -128,46 +248,56 @@ data TyCon
        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,
        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.
-
-       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,
@@ -188,42 +318,46 @@ data TyCon
 
        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,
-       tc_kind     :: Kind,
-       tyConArity    :: Arity,                 -- SLPJ Oct06: I'm not sure what the significance
-                                               --             of the arity of a primtycon is!
+       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.
-                                               -- Only relevant if tc_kind = *
+       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: Coercion TyCons are always fully applied
-  --           But note that a CoercionTyCon can be over-saturated in a type.
+  --           But note that a CoTyCon can be *over*-saturated in a type.
   --           E.g.  (sym g1) Int  will be represented as (TyConApp sym [g1,Int])
-  | CoercionTyCon {    
+  | CoTyCon {  
        tyConUnique :: Unique,
         tyConName   :: Name,
        tyConArity  :: Arity,
-       coKindFun   :: CoTyConKindChecker
+       coTcDesc    :: CoTyConDesc
     }
 
   -- | Any types.  Like tuples, this is a potentially-infinite family of TyCons
@@ -239,10 +373,11 @@ data TyCon
                                -- 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 {
@@ -250,90 +385,78 @@ data TyCon
         tyConName   :: Name
     }
 
-type CoTyConKindChecker = forall m. Monad m => CoTyConKindCheckerFun m
-
-type CoTyConKindCheckerFun m 
-  =    (Type -> m Kind)                -- Kind checker for types
-    -> (Type -> m (Type,Type)) -- and for coercions
-    -> Bool                    -- True => apply consistency checks
-    -> [Type]                  -- Exactly right number of args
-    -> m (Type, Type)          -- Kind of this application
-
-               -- ^ Function that when given a list of the type arguments to the 'TyCon'
-               -- constructs the types that the resulting coercion relates.
-               -- Returns Nothing if ill-kinded.
-               --
-               -- 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)@
-
 -- | Names of the fields in an algebraic record type
 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 :: *
-
+    -- | 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 :: AssocFamilyPermutation
     }
 
-  -- | Information about those 'TyCon's derived from a @data@ declaration. This includes 
-  -- data types with no constructors at all.
+    -- | 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 'isEnumerationTyCon')
     }
 
   -- | 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.
-                                
-                               -- 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.
+        nt_co :: Maybe TyCon   -- ^ A 'TyCon' (which is always a 'CoTyCon') 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.
+                               
+                              -- 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.
     }
 
 type AssocFamilyPermutation
@@ -348,8 +471,9 @@ type AssocFamilyPermutation
         --     TyCon's arity; e.g. class C a where { data D a :: *->* }
         --                    here D gets arity 2
 
--- | 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 {}                 = []
@@ -377,19 +501,13 @@ 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
+  | FamilyTyCon          -- See Note [Data type families]
        TyCon
        [Type]
        TyCon  -- c.f. Note [Newtype coercions]
 
-       --
-       -- 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
 
 -- | Checks the invariants of a 'TyConParent' given the appropriate type class name, if any
 okParent :: Name -> TyConParent -> Bool
@@ -409,6 +527,20 @@ data SynTyConRhs
   | SynonymTyCon Type   -- ^ The synonym mentions head type variables. It acts as a
                        -- template for the expansion when the 'TyCon' is applied to some
                        -- types.
+
+--------------------
+data CoTyConDesc
+  = CoSym   | CoTrans
+  | CoLeft  | CoRight
+  | CoCsel1 | CoCsel2 | CoCselR
+  | CoInst
+
+  | CoAxiom    -- C tvs : F lhs-tys ~ rhs-ty
+      { co_ax_tvs :: [TyVar]
+      , co_ax_lhs :: Type
+      , co_ax_rhs :: Type }
+
+  | CoUnsafe 
 \end{code}
 
 Note [Newtype coercions]
@@ -420,7 +552,7 @@ 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
+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
@@ -438,7 +570,7 @@ 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]
@@ -485,39 +617,6 @@ 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)
-
-  * The representation TyCon :R1T has an AlgTyConParent of
-
-       FamilyTyCon T [(b,c)] :Co:R1T
-
-
-
 %************************************************************************
 %*                                                                     *
 \subsection{PrimRep}
@@ -595,11 +694,14 @@ mkFunTyCon name 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
            -> TyConParent
@@ -611,7 +713,7 @@ mkAlgTyCon name kind tyvars stupid rhs parent is_rec gen_info gadt_syn
   = AlgTyCon { 
        tyConName        = name,
        tyConUnique      = nameUnique name,
-       tc_kind  = kind,
+       tc_kind          = kind,
        tyConArity       = length tyvars,
        tyConTyVars      = tyvars,
        algTcStupidTheta = stupid,
@@ -619,7 +721,7 @@ mkAlgTyCon name kind tyvars stupid rhs parent is_rec gen_info gadt_syn
        algTcParent      = ASSERT( okParent name parent ) parent,
        algTcRec         = is_rec,
        algTcGadtSyntax  = gadt_syn,
-       hasGenerics = gen_info
+       hasGenerics      = gen_info
     }
 
 -- | Simpler specialization of 'mkAlgTyCon' for classes
@@ -710,21 +812,14 @@ mkSynTyCon name kind tyvars rhs parent
 
 -- | Create a coercion 'TyCon'
 mkCoercionTyCon :: Name -> Arity 
-                -> CoTyConKindChecker
+                -> CoTyConDesc
                 -> TyCon
-mkCoercionTyCon name arity rule_fn
-  = CoercionTyCon {
+mkCoercionTyCon name arity desc
+  = CoTyCon {
         tyConName   = name,
         tyConUnique = nameUnique name,
         tyConArity  = arity,
-#ifdef DEBUG
-        coKindFun   = \ ty co fail args -> 
-                      ASSERT2( length args == arity, ppr name )
-                      rule_fn ty co fail args
-#else
-       coKindFun   = rule_fn
-#endif
-    }
+        coTcDesc    = desc }
 
 mkAnyTyCon :: Name -> Kind -> TyCon
 mkAnyTyCon name kind 
@@ -768,7 +863,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
@@ -799,11 +895,6 @@ isNewTyCon :: TyCon -> Bool
 isNewTyCon (AlgTyCon {algTcRhs = NewTyCon {}}) = True
 isNewTyCon _                                   = False
 
-tyConHasKind :: TyCon -> Bool
-tyConHasKind (SuperKindTyCon {}) = False
-tyConHasKind (CoercionTyCon {})  = False
-tyConHasKind _                   = True
-
 -- | 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.
@@ -850,11 +941,11 @@ isOpenSynTyCon :: TyCon -> Bool
 isOpenSynTyCon tycon = isSynTyCon tycon && isOpenTyCon tycon
 
 isDecomposableTyCon :: TyCon -> Bool
--- True iff we can deocmpose (T a b c) into ((T a b) c)
+-- True iff we can decompose (T a b c) into ((T a b) c)
 -- Specifically NOT true of synonyms (open and otherwise) and coercions
-isDecomposableTyCon (SynTyCon      {}) = False
-isDecomposableTyCon (CoercionTyCon {}) = False
-isDecomposableTyCon _other             = True
+isDecomposableTyCon (SynTyCon {}) = False
+isDecomposableTyCon (CoTyCon {})  = False
+isDecomposableTyCon _other        = True
 
 -- | Is this an algebraic 'TyCon' declared with the GADT syntax?
 isGadtSyntaxTyCon :: TyCon -> Bool
@@ -972,15 +1063,15 @@ isAnyTyCon _              = 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 :: Monad m => TyCon -> Maybe (Arity, CoTyConKindCheckerFun m)
-isCoercionTyCon_maybe (CoercionTyCon {tyConArity = ar, coKindFun = rule}) 
-  = Just (ar, rule)
+isCoercionTyCon_maybe :: TyCon -> Maybe (Arity, CoTyConDesc)
+isCoercionTyCon_maybe (CoTyCon {tyConArity = ar, coTcDesc = desc}) 
+  = Just (ar, desc)
 isCoercionTyCon_maybe _ = Nothing
 
 -- | Is this a 'TyCon' that represents a coercion?
 isCoercionTyCon :: TyCon -> Bool
-isCoercionTyCon (CoercionTyCon {}) = True
-isCoercionTyCon _                  = False
+isCoercionTyCon (CoTyCon {}) = True
+isCoercionTyCon _            = False
 
 -- | Identifies implicit tycons that, in particular, do not go into interface
 -- files (because they are implicitly reconstructed when the interface is
@@ -1000,7 +1091,7 @@ isImplicitTyCon tycon | isTyConAssoc tycon           = True
                                                       isTupleTyCon tycon
 isImplicitTyCon _other                               = True
         -- catches: FunTyCon, PrimTyCon, 
-        -- CoercionTyCon, SuperKindTyCon
+        -- CoTyCon, SuperKindTyCon
 \end{code}
 
 
@@ -1064,7 +1155,12 @@ 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)
+tyConKind tc = pprPanic "tyConKind" (ppr tc)   -- SuperKindTyCon and CoTyCon
+
+tyConHasKind :: TyCon -> Bool
+tyConHasKind (SuperKindTyCon {}) = False
+tyConHasKind (CoTyCon {})        = False
+tyConHasKind _                   = True
 
 -- | As 'tyConDataCons_maybe', but returns the empty list of constructors if no constructors
 -- could be found
@@ -1243,9 +1339,30 @@ instance Ord TyCon where
 instance Uniquable TyCon where
     getUnique tc = tyConUnique tc
 
+instance Outputable CoTyConDesc where
+    ppr CoSym    = ptext (sLit "SYM")
+    ppr CoTrans  = ptext (sLit "TRANS")
+    ppr CoLeft   = ptext (sLit "LEFT")
+    ppr CoRight  = ptext (sLit "RIGHT")
+    ppr CoCsel1  = ptext (sLit "CSEL1")
+    ppr CoCsel2  = ptext (sLit "CSEL2")
+    ppr CoCselR  = ptext (sLit "CSELR")
+    ppr CoInst   = ptext (sLit "INST")
+    ppr CoUnsafe = ptext (sLit "UNSAFE")
+    ppr (CoAxiom {}) = ptext (sLit "AXIOM")
+
 instance Outputable TyCon where
     ppr tc  = ppr (getName tc) 
 
 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"
 \end{code}