Fix a long-standing infelicity in the type pretty printer

[ghc-hetmet.git] / compiler / types / TyCon.lhs

diff --git a/compiler/types/TyCon.lhs b/compiler/types/TyCon.lhs
index 09caf8e..958a0cb 100644 (file)
--- a/compiler/types/TyCon.lhs
+++ b/compiler/types/TyCon.lhs
@@ -8,24 +8,26 @@ The @TyCon@ datatype
 \begin{code}
 module TyCon(
         -- * Main TyCon data types
 \begin{code}
 module TyCon(
         -- * Main TyCon data types

-       TyCon, FieldLabel,
+       TyCon, FieldLabel, CoTyConKindChecker,

 
        AlgTyConRhs(..), visibleDataCons, 
         TyConParent(..), 
        SynTyConRhs(..),
 
        AlgTyConRhs(..), visibleDataCons, 
         TyConParent(..), 
        SynTyConRhs(..),

+       AssocFamilyPermutation,

 
         -- ** Constructing TyCons
        mkAlgTyCon,
        mkClassTyCon,
        mkFunTyCon,
        mkPrimTyCon,
 
         -- ** Constructing TyCons
        mkAlgTyCon,
        mkClassTyCon,
        mkFunTyCon,
        mkPrimTyCon,

-       mkVoidPrimTyCon,
+       mkKindTyCon,

        mkLiftedPrimTyCon,
        mkTupleTyCon,
        mkSynTyCon,
         mkSuperKindTyCon,
         mkCoercionTyCon,
         mkForeignTyCon,
        mkLiftedPrimTyCon,
        mkTupleTyCon,
        mkSynTyCon,
         mkSuperKindTyCon,
         mkCoercionTyCon,
         mkForeignTyCon,

+        mkAnyTyCon,

 
         -- ** Predicates on TyCons
         isAlgTyCon,
 
         -- ** Predicates on TyCons
         isAlgTyCon,

@@ -34,10 +36,11 @@ module TyCon(
         isPrimTyCon,
         isTupleTyCon, isUnboxedTupleTyCon, isBoxedTupleTyCon, 
         isSynTyCon, isClosedSynTyCon, isOpenSynTyCon,
         isPrimTyCon,
         isTupleTyCon, isUnboxedTupleTyCon, isBoxedTupleTyCon, 
         isSynTyCon, isClosedSynTyCon, isOpenSynTyCon,

-        isSuperKindTyCon,
+        isSuperKindTyCon, isDecomposableTyCon,

         isCoercionTyCon, isCoercionTyCon_maybe,
         isCoercionTyCon, isCoercionTyCon_maybe,

-        isForeignTyCon,
+        isForeignTyCon, isAnyTyCon, tyConHasKind,

 
 

+       isInjectiveTyCon,

        isDataTyCon, isProductTyCon, isEnumerationTyCon, 
        isNewTyCon, isAbstractTyCon, isOpenTyCon,
         isUnLiftedTyCon,
        isDataTyCon, isProductTyCon, isEnumerationTyCon, 
        isNewTyCon, isAbstractTyCon, isOpenTyCon,
         isUnLiftedTyCon,

@@ -54,7 +57,6 @@ module TyCon(
        tyConTyVars,
        tyConDataCons, tyConDataCons_maybe, tyConSingleDataCon_maybe,
        tyConFamilySize,
        tyConTyVars,
        tyConDataCons, tyConDataCons_maybe, tyConSingleDataCon_maybe,
        tyConFamilySize,

-       tyConSelIds,

        tyConStupidTheta,
        tyConArity,
        tyConClass_maybe,
        tyConStupidTheta,
        tyConArity,
        tyConClass_maybe,

@@ -92,6 +94,7 @@ import Maybes
 import Outputable
 import FastString
 import Constants
 import Outputable
 import FastString
 import Constants

+import Data.List( elemIndex )

 \end{code}
 
 %************************************************************************
 \end{code}
 
 %************************************************************************

@@ -101,7 +104,7 @@ import Constants
 %************************************************************************
 
 \begin{code}
 %************************************************************************
 
 \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 @*@
 --
 --
 -- 1) Data declarations: @data Foo = ...@ creates the @Foo@ type constructor of kind @*@
 --

@@ -112,7 +115,7 @@ 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
 -- 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
+--    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.
 --
 -- This data type also encodes a number of primitive, built in type constructors such as those
 -- for function and tuple types.

@@ -121,7 +124,7 @@ data TyCon
     FunTyCon {
        tyConUnique :: Unique,
        tyConName   :: Name,
     FunTyCon {
        tyConUnique :: Unique,
        tyConName   :: Name,

-       tyConKind   :: Kind,
+       tc_kind   :: Kind,

        tyConArity  :: Arity
     }
 
        tyConArity  :: Arity
     }
 

@@ -130,7 +133,7 @@ data TyCon
   | AlgTyCon {         
        tyConUnique :: Unique,
        tyConName   :: Name,
   | AlgTyCon {         
        tyConUnique :: Unique,
        tyConName   :: Name,

-       tyConKind   :: Kind,
+       tc_kind   :: Kind,

        tyConArity  :: Arity,
 
        tyConTyVars :: [TyVar],         -- ^ The type variables used in the type constructor.
        tyConArity  :: Arity,
 
        tyConTyVars :: [TyVar],         -- ^ The type variables used in the type constructor.

@@ -144,12 +147,11 @@ data TyCon
                                        --
                                        -- Note that it does /not/ scope over the data constructors.
 
                                        --
                                        -- 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
        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 ...@.
        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 ...@.

@@ -169,7 +171,7 @@ data TyCon
   | TupleTyCon {
        tyConUnique :: Unique,
        tyConName   :: Name,
   | TupleTyCon {
        tyConUnique :: Unique,
        tyConName   :: Name,

-       tyConKind   :: Kind,
+       tc_kind   :: Kind,

        tyConArity  :: Arity,
        tyConBoxed  :: Boxity,
        tyConTyVars :: [TyVar],
        tyConArity  :: Arity,
        tyConBoxed  :: Boxity,
        tyConTyVars :: [TyVar],

@@ -181,7 +183,7 @@ data TyCon
   | SynTyCon {
        tyConUnique  :: Unique,
        tyConName    :: Name,
   | SynTyCon {
        tyConUnique  :: Unique,
        tyConName    :: Name,

-       tyConKind    :: Kind,
+       tc_kind    :: Kind,

        tyConArity   :: Arity,
 
        tyConTyVars  :: [TyVar],        -- Bound tyvars
        tyConArity   :: Arity,
 
        tyConTyVars  :: [TyVar],        -- Bound tyvars

@@ -197,33 +199,44 @@ data TyCon
   | PrimTyCon {                        
        tyConUnique   :: Unique,
        tyConName     :: Name,
   | PrimTyCon {                        
        tyConUnique   :: Unique,
        tyConName     :: Name,

-       tyConKind     :: 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
-
-       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
+       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 = *
+
+       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

     }
 
     }
 

-  -- | Type coercions, such as @(:=:)@, @sym@, @trans@, @left@ and @right@.
-  -- INVARIANT: coercions are always fully applied
+  -- | 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.
+  --           E.g.  (sym g1) Int  will be represented as (TyConApp sym [g1,Int])

   | CoercionTyCon {    
        tyConUnique :: Unique,
         tyConName   :: Name,
        tyConArity  :: Arity,
   | 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)@
+       coKindFun   :: CoTyConKindChecker
+    }
+
+  -- | 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.
     }
 
   -- | Super-kinds. These are "kinds-of-kinds" and are never seen in Haskell source programs.

@@ -237,6 +250,23 @@ data TyCon
         tyConName   :: Name
     }
 
         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
 
 -- | Names of the fields in an algebraic record type
 type FieldLabel = Name
 

@@ -260,17 +290,7 @@ data AlgTyConRhs
   -- >   data T b :: *
 
   | OpenTyCon {
   -- >   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.
+      otArgPoss :: AssocFamilyPermutation

     }
 
   -- | Information about those 'TyCon's derived from a @data@ declaration. This includes 
     }
 
   -- | Information about those 'TyCon's derived from a @data@ declaration. This includes 

@@ -316,6 +336,18 @@ data AlgTyConRhs
                                -- again check Trac #1072.
     }
 
                                -- again check Trac #1072.
     }
 

+type AssocFamilyPermutation
+  = Maybe [Int]  -- Nothing for *top-level* type families
+                 -- For *associated* type families, gives the position
+                -- of that 'TyVar' in the class argument list (0-indexed)
+                -- e.g.  class C a b c where { type F c a :: *->* }
+                 --       Then we get Just [2,0]
+        -- For *synonyms*, the length of the list is identical to
+        --                 the TyCon's arity
+        -- For *data types*, the length may be smaller than the
+        --     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!
 visibleDataCons :: AlgTyConRhs -> [DataCon]
 -- | 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]

@@ -369,16 +401,10 @@ okParent _       (FamilyTyCon fam_tc tys _co_tc) = tyConArity fam_tc == length t
 
 -- | Information pertaining to the expansion of a type synonym (@type@)
 data SynTyConRhs
 
 -- | 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.
+  = OpenSynTyCon      -- e.g. type family F x y :: * -> *
+       Kind          -- Kind of the "rhs"; ie *excluding type indices*
+                             --     In the example, the kind is (*->*)
+       AssocFamilyPermutation

 
   | SynonymTyCon Type   -- ^ The synonym mentions head type variables. It acts as a
                        -- template for the expansion when the 'TyCon' is applied to some
 
   | SynonymTyCon Type   -- ^ The synonym mentions head type variables. It acts as a
                        -- template for the expansion when the 'TyCon' is applied to some

@@ -393,7 +419,7 @@ newtype, to the newtype itself. For example,
 
    newtype T a = MkT (a -> a)
 
 
    newtype T a = MkT (a -> a)
 

-the NewTyCon for T will contain nt_co = CoT where CoT t : T t :=: t ->
+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
 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
 t.  This TyCon is a CoercionTyCon, 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

@@ -403,11 +429,11 @@ ending with the same type variables as the left hand side, we
 
    newtype S a = MkT [a]
 
 
    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
 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])
 and then when we used CoT at a particular type, s, we'd say
        CoT @ s
 which encodes as (TyConApp instCoercionTyCon [TyConApp CoT [], s])

@@ -418,7 +444,7 @@ be saturated, but which encodes as
        TyConApp CoT [s]
 In the vocabulary of the paper it's as if we had axiom declarations
 like
        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]
 ~~~~~~~~~~~~~~~~~~
 
 Note [Newtype eta]
 ~~~~~~~~~~~~~~~~~~

@@ -499,7 +525,7 @@ Then
 %************************************************************************
 
 A PrimRep is somewhat similar to a CgRep (see codeGen/SMRep) and a
 %************************************************************************
 
 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
 and clearly defined purpose:
 
   - A PrimRep is a CgRep + information about signedness + information

@@ -565,7 +591,7 @@ mkFunTyCon name kind
   = FunTyCon { 
        tyConUnique = nameUnique name,
        tyConName   = name,
   = FunTyCon { 
        tyConUnique = nameUnique name,
        tyConName   = name,

-       tyConKind   = kind,
+       tc_kind   = kind,

        tyConArity  = 2
     }
 
        tyConArity  = 2
     }
 

@@ -576,22 +602,20 @@ mkAlgTyCon :: Name
            -> [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
            -> [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
            -> 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,
   = AlgTyCon { 
        tyConName        = name,
        tyConUnique      = nameUnique name,

-       tyConKind        = kind,
+       tc_kind  = kind,

        tyConArity       = length tyvars,
        tyConTyVars      = tyvars,
        algTcStupidTheta = stupid,
        algTcRhs         = rhs,
        tyConArity       = length tyvars,
        tyConTyVars      = tyvars,
        algTcStupidTheta = stupid,
        algTcRhs         = rhs,

-       algTcSelIds      = sel_ids,

        algTcParent      = ASSERT( okParent name parent ) parent,
        algTcRec         = is_rec,
        algTcGadtSyntax  = gadt_syn,
        algTcParent      = ASSERT( okParent name parent ) parent,
        algTcRec         = is_rec,
        algTcGadtSyntax  = gadt_syn,

@@ -601,7 +625,7 @@ mkAlgTyCon name kind tyvars stupid rhs sel_ids parent is_rec gen_info gadt_syn
 -- | Simpler specialization of 'mkAlgTyCon' for classes
 mkClassTyCon :: Name -> Kind -> [TyVar] -> AlgTyConRhs -> Class -> RecFlag -> TyCon
 mkClassTyCon name kind tyvars rhs clas is_rec =
 -- | 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'
 
 mkTupleTyCon :: Name 
              -> Kind    -- ^ Kind of the resulting 'TyCon'

@@ -615,7 +639,7 @@ mkTupleTyCon name kind arity tyvars con boxed gen_info
   = TupleTyCon {
        tyConUnique = nameUnique name,
        tyConName = name,
   = TupleTyCon {
        tyConUnique = nameUnique name,
        tyConName = name,

-       tyConKind = kind,
+       tc_kind = kind,

        tyConArity = arity,
        tyConBoxed = boxed,
        tyConTyVars = tyvars,
        tyConArity = arity,
        tyConBoxed = boxed,
        tyConTyVars = tyvars,

@@ -636,7 +660,7 @@ mkForeignTyCon name ext_name kind arity
   = PrimTyCon {
        tyConName    = name,
        tyConUnique  = nameUnique name,
   = PrimTyCon {
        tyConName    = name,
        tyConUnique  = nameUnique name,

-       tyConKind    = kind,
+       tc_kind    = kind,

        tyConArity   = arity,
        primTyConRep = PtrRep, -- they all do
        isUnLifted   = False,
        tyConArity   = arity,
        primTyConRep = PtrRep, -- they all do
        isUnLifted   = False,

@@ -649,10 +673,10 @@ mkPrimTyCon :: Name  -> Kind -> Arity -> PrimRep -> TyCon
 mkPrimTyCon name kind arity rep
   = mkPrimTyCon' name kind arity rep True  
 
 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
 
 -- | Create a lifted primitive 'TyCon' such as @RealWorld@
 mkLiftedPrimTyCon :: Name  -> Kind -> Arity -> PrimRep -> TyCon

@@ -664,7 +688,7 @@ mkPrimTyCon' name kind arity rep is_unlifted
   = PrimTyCon {
        tyConName    = name,
        tyConUnique  = nameUnique name,
   = PrimTyCon {
        tyConName    = name,
        tyConUnique  = nameUnique name,

-       tyConKind    = kind,
+       tc_kind    = kind,

        tyConArity   = arity,
        primTyConRep = rep,
        isUnLifted   = is_unlifted,
        tyConArity   = arity,
        primTyConRep = rep,
        isUnLifted   = is_unlifted,

@@ -677,7 +701,7 @@ mkSynTyCon name kind tyvars rhs parent
   = SynTyCon { 
        tyConName = name,
        tyConUnique = nameUnique name,
   = SynTyCon { 
        tyConName = name,
        tyConUnique = nameUnique name,

-       tyConKind = kind,
+       tc_kind = kind,

        tyConArity = length tyvars,
        tyConTyVars = tyvars,
        synTcRhs = rhs,
        tyConArity = length tyvars,
        tyConTyVars = tyvars,
        synTcRhs = rhs,

@@ -685,15 +709,29 @@ mkSynTyCon name kind tyvars rhs parent
     }
 
 -- | Create a coercion 'TyCon'
     }
 
 -- | Create a coercion 'TyCon'

-mkCoercionTyCon :: Name -> Arity -> ([Type] -> (Type,Type)) -> TyCon
-mkCoercionTyCon name arity kindRule
+mkCoercionTyCon :: Name -> Arity 
+                -> CoTyConKindChecker
+                -> TyCon
+mkCoercionTyCon name arity rule_fn

   = CoercionTyCon {
   = CoercionTyCon {

-        tyConName = name,
+        tyConName   = name,

         tyConUnique = nameUnique name,
         tyConUnique = nameUnique name,

-        tyConArity = arity,
-        coKindFun = kindRule
+        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

     }
 
     }
 

+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
 mkSuperKindTyCon name
 -- | Create a super-kind 'TyCon'
 mkSuperKindTyCon :: Name -> TyCon -- Super kinds always have arity zero
 mkSuperKindTyCon name

@@ -761,6 +799,11 @@ isNewTyCon :: TyCon -> Bool
 isNewTyCon (AlgTyCon {algTcRhs = NewTyCon {}}) = True
 isNewTyCon _                                   = False
 
 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.
 -- | 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.

@@ -806,6 +849,13 @@ isClosedSynTyCon tycon = isSynTyCon tycon && not (isOpenTyCon tycon)
 isOpenSynTyCon :: TyCon -> Bool
 isOpenSynTyCon tycon = isSynTyCon tycon && isOpenTyCon tycon
 
 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)
+-- Specifically NOT true of synonyms (open and otherwise) and coercions
+isDecomposableTyCon (SynTyCon      {}) = False
+isDecomposableTyCon (CoercionTyCon {}) = False
+isDecomposableTyCon _other             = True
+

 -- | Is this an algebraic 'TyCon' declared with the GADT syntax?
 isGadtSyntaxTyCon :: TyCon -> Bool
 isGadtSyntaxTyCon (AlgTyCon { algTcGadtSyntax = res }) = res
 -- | Is this an algebraic 'TyCon' declared with the GADT syntax?
 isGadtSyntaxTyCon :: TyCon -> Bool
 isGadtSyntaxTyCon (AlgTyCon { algTcGadtSyntax = res }) = res

@@ -814,13 +864,25 @@ isGadtSyntaxTyCon _                                    = False
 -- | Is this an algebraic 'TyCon' which is just an enumeration of values?
 isEnumerationTyCon :: TyCon -> Bool
 isEnumerationTyCon (AlgTyCon {algTcRhs = DataTyCon { is_enum = res }}) = res
 -- | Is this an algebraic 'TyCon' which is just an enumeration of values?
 isEnumerationTyCon :: TyCon -> Bool
 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
 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
+isOpenTyCon (SynTyCon {synTcRhs = OpenSynTyCon {}}) = True
+isOpenTyCon (AlgTyCon {algTcRhs = OpenTyCon {}})    = True
+isOpenTyCon _                                      = False
+
+-- | 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!

 
 -- | 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
 
 -- | 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

@@ -836,14 +898,22 @@ assocTyConArgPoss_maybe _ = Nothing
 isTyConAssoc :: TyCon -> Bool
 isTyConAssoc = isJust . assocTyConArgPoss_maybe
 
 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)
+-- | Set the AssocFamilyPermutation structure in an 
+-- associated data or type synonym.  The [TyVar] are the
+-- class type variables.  Remember, the tyvars of an associated
+-- data/type are a subset of the class tyvars; except that an
+-- associated data type can have extra type variables at the
+-- end (see Note [Avoid name clashes for associated data types] in TcHsType)
+setTyConArgPoss :: [TyVar] -> TyCon -> TyCon
+setTyConArgPoss clas_tvs tc
+  = case tc of
+      AlgTyCon { algTcRhs = rhs }               -> tc { algTcRhs = rhs {otArgPoss = Just ps} }
+      SynTyCon { synTcRhs = OpenSynTyCon ki _ } -> tc { synTcRhs = OpenSynTyCon ki (Just ps) }
+      _                                         -> pprPanic "setTyConArgPoss" (ppr tc)
+  where
+    ps = catMaybes [tv `elemIndex` clas_tvs | tv <- tyConTyVars tc]
+       -- We will get Nothings for the "extra" type variables in an
+       -- associated data type

 
 -- The unit tycon didn't used to be classed as a tuple tycon
 -- but I thought that was silly so I've undone it
 
 -- 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,10 +964,15 @@ isSuperKindTyCon :: TyCon -> Bool
 isSuperKindTyCon (SuperKindTyCon {}) = True
 isSuperKindTyCon _                   = False
 
 isSuperKindTyCon (SuperKindTyCon {}) = True
 isSuperKindTyCon _                   = False
 

+-- | Is this an AnyTyCon?
+isAnyTyCon :: TyCon -> Bool
+isAnyTyCon (AnyTyCon {}) = True
+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
 -- | 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 :: Monad m => TyCon -> Maybe (Arity, CoTyConKindCheckerFun m)

 isCoercionTyCon_maybe (CoercionTyCon {tyConArity = ar, coKindFun = rule}) 
   = Just (ar, rule)
 isCoercionTyCon_maybe _ = Nothing
 isCoercionTyCon_maybe (CoercionTyCon {tyConArity = ar, coKindFun = rule}) 
   = Just (ar, rule)
 isCoercionTyCon_maybe _ = Nothing

@@ -953,7 +1028,7 @@ tcExpandTyCon_maybe _ _ = Nothing
 
 -- ^ 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
 
 -- ^ 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
+coreExpandTyCon_maybe (AlgTyCon {

          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
          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

@@ -982,6 +1057,15 @@ tyConHasGenerics (AlgTyCon {hasGenerics = hg})   = hg
 tyConHasGenerics (TupleTyCon {hasGenerics = hg}) = hg
 tyConHasGenerics _                               = False        -- Synonyms
 
 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)
+

 -- | As 'tyConDataCons_maybe', but returns the empty list of constructors if no constructors
 -- could be found
 tyConDataCons :: TyCon -> [DataCon]
 -- | As 'tyConDataCons_maybe', but returns the empty list of constructors if no constructors
 -- could be found
 tyConDataCons :: TyCon -> [DataCon]

@@ -1007,16 +1091,12 @@ tyConFamilySize (AlgTyCon   {algTcRhs = OpenTyCon {}})                 = 0
 tyConFamilySize (TupleTyCon {})                                               = 1
 tyConFamilySize other = pprPanic "tyConFamilySize:" (ppr other)
 
 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
 -- | 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}
 
 algTyConRhs other = pprPanic "algTyConRhs" (ppr other)
 \end{code}
 

@@ -1089,13 +1169,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
 -- 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}
 \end{code}
 
 \begin{code}