Re-add FunTy (big patch)
[ghc.git] / compiler / types / TyCon.hs
index e1cd128..c7c225d 100644 (file)
@@ -6,15 +6,19 @@
 The @TyCon@ datatype
 -}
 
-{-# LANGUAGE CPP, DeriveDataTypeable #-}
+{-# LANGUAGE CPP #-}
 
 module TyCon(
         -- * Main TyCon data types
-        TyCon, FieldLabel,
+        TyCon,
 
         AlgTyConRhs(..), visibleDataCons,
-        TyConParent(..), isNoParent,
-        FamTyConFlav(..), Role(..),
+        AlgTyConFlav(..), isNoParent,
+        FamTyConFlav(..), Role(..), Injectivity(..),
+        RuntimeRepInfo(..),
+
+        -- ** Field labels
+        tyConFieldLabels, tyConFieldLabelEnv,
 
         -- ** Constructing TyCons
         mkAlgTyCon,
@@ -27,19 +31,18 @@ module TyCon(
         mkSynonymTyCon,
         mkFamilyTyCon,
         mkPromotedDataCon,
-        mkPromotedTyCon,
+        mkTcTyCon,
 
         -- ** Predicates on TyCons
-        isAlgTyCon,
+        isAlgTyCon, isVanillaAlgTyCon,
         isClassTyCon, isFamInstTyCon,
         isFunTyCon,
         isPrimTyCon,
         isTupleTyCon, isUnboxedTupleTyCon, isBoxedTupleTyCon,
         isTypeSynonymTyCon,
         mightBeUnsaturatedTyCon,
-        isPromotedDataCon, isPromotedTyCon,
-        isPromotedDataCon_maybe, isPromotedTyCon_maybe,
-        promotableTyCon_maybe, promoteTyCon,
+        isPromotedDataCon, isPromotedDataCon_maybe,
+        isKindTyCon, isLiftedTypeKindTyConName,
 
         isDataTyCon, isProductTyCon, isDataProductTyCon_maybe,
         isEnumerationTyCon,
@@ -47,12 +50,15 @@ module TyCon(
         isFamilyTyCon, isOpenFamilyTyCon,
         isTypeFamilyTyCon, isDataFamilyTyCon,
         isOpenTypeFamilyTyCon, isClosedSynFamilyTyConWithAxiom_maybe,
+        familyTyConInjectivityInfo,
         isBuiltInSynFamTyCon_maybe,
-        isUnLiftedTyCon,
+        isUnliftedTyCon,
         isGadtSyntaxTyCon, isInjectiveTyCon, isGenerativeTyCon, isGenInjAlgRhs,
         isTyConAssoc, tyConAssoc_maybe,
         isRecursiveTyCon,
         isImplicitTyCon,
+        isTyConWithSrcDataCons,
+        isTcTyCon,
 
         -- ** Extracting information out of TyCons
         tyConName,
@@ -67,14 +73,19 @@ module TyCon(
         tyConStupidTheta,
         tyConArity,
         tyConRoles,
-        tyConParent,
         tyConFlavour,
-        tyConTuple_maybe, tyConClass_maybe,
+        tyConTuple_maybe, tyConClass_maybe, tyConATs,
         tyConFamInst_maybe, tyConFamInstSig_maybe, tyConFamilyCoercion_maybe,
-        synTyConDefn_maybe, synTyConRhs_maybe, famTyConFlav_maybe,
+        tyConFamilyResVar_maybe,
+        synTyConDefn_maybe, synTyConRhs_maybe,
+        famTyConFlav_maybe, famTcResVar,
         algTyConRhs,
         newTyConRhs, newTyConEtadArity, newTyConEtadRhs,
         unwrapNewTyCon_maybe, unwrapNewTyConEtad_maybe,
+        algTcFields,
+        tyConRuntimeRepInfo,
+        tyConBinders, tyConResKind,
+        tcTyConScopedTyVars,
 
         -- ** Manipulating TyCons
         expandSynTyCon_maybe,
@@ -82,9 +93,14 @@ module TyCon(
         newTyConCo, newTyConCo_maybe,
         pprPromotionQuote,
 
+        -- * Runtime type representation
+        TyConRepName, tyConRepName_maybe,
+        mkPrelTyConRepName,
+        tyConRepModOcc,
+
         -- * Primitive representations of Types
         PrimRep(..), PrimElemRep(..),
-        tyConPrimRep, isVoidRep, isGcPtrRep,
+        isVoidRep, isGcPtrRep,
         primRepSizeW, primElemRepSizeB,
         primRepIsFloat,
 
@@ -95,24 +111,32 @@ module TyCon(
 
 #include "HsVersions.h"
 
-import {-# SOURCE #-} TypeRep ( Kind, Type, PredType )
-import {-# SOURCE #-} DataCon ( DataCon, dataConExTyVars )
+import {-# SOURCE #-} TyCoRep ( Kind, Type, PredType, TyBinder, pprType, mkPiTys )
+import {-# SOURCE #-} TysWiredIn  ( runtimeRepTyCon, constraintKind
+                                  , vecCountTyCon, vecElemTyCon, liftedTypeKind )
+import {-# SOURCE #-} DataCon ( DataCon, dataConExTyVars, dataConFieldLabels )
 
+import Binary
 import Var
 import Class
 import BasicTypes
 import DynFlags
 import ForeignCall
 import Name
-import NameSet
+import NameEnv
 import CoAxiom
 import PrelNames
 import Maybes
 import Outputable
+import FastStringEnv
+import FieldLabel
 import Constants
 import Util
+import Unique( tyConRepNameUnique, dataConRepNameUnique )
+import UniqSet
+import Module
+
 import qualified Data.Data as Data
-import Data.Typeable (Typeable)
 
 {-
 -----------------------------------------------
@@ -152,9 +176,7 @@ Note [Type synonym families]
     a FamilyTyCon 'G', whose FamTyConFlav is ClosedSynFamilyTyCon, with the
     appropriate CoAxiom representing the equations
 
-* In the future we might want to support
-    * injective type families (allow decomposition)
-  but we don't at the moment [2013]
+We also support injective type families -- see Note [Injective type families]
 
 Note [Data type families]
 ~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -177,11 +199,12 @@ See also Note [Wrappers for data instance tycons] in MkId.hs
 
         data T a
         data R:TInt = T1 | T2 Bool
-        axiom ax_ti : T Int ~ R:TInt
+        axiom ax_ti : T Int ~R R:TInt
 
+  Note that this is a *representational* coercion
   The R:TInt is the "representation TyCons".
-  It has an AlgTyConParent of
-        FamInstTyCon T [Int] ax_ti
+  It has an AlgTyConFlav of
+        DataFamInstTyCon T [Int] ax_ti
 
 * The axiom ax_ti may be eta-reduced; see
   Note [Eta reduction for data family axioms] in TcInstDcls
@@ -203,7 +226,7 @@ See also Note [Wrappers for data instance tycons] in MkId.hs
         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
+        axiom ax_pr :: T (a,b)  ~R  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)
@@ -213,9 +236,9 @@ See also Note [Wrappers for data instance tycons] in MkId.hs
   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
+  The representation TyCon R:TList, has an AlgTyConFlav of
 
-        FamInstTyCon T [(a,b)] ax_pr
+        DataFamInstTyCon 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
@@ -251,10 +274,15 @@ See also Note [Wrappers for data instance tycons] in MkId.hs
   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.
 
+* The tyConTyVars of the representation tycon are the tyvars that the
+  user wrote in the patterns. This is important in TcDeriv, where we
+  bring these tyvars into scope before type-checking the deriving
+  clause. This fact is arranged for in TcInstDecls.tcDataFamInstDecl.
+
 Note [Associated families and their parent class]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 *Associated* families are just like *non-associated* families, except
-that they have a TyConParent of AssocFamilyTyCon, which identifies the
+that they have a famTcParent field of (Just cls), which identifies the
 parent class.
 
 However there is an important sharing relationship between
@@ -279,7 +307,6 @@ This is important. In an instance declaration we expect
 
 Note [TyCon Role signatures]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
 Every tycon has a role signature, assigning a role to each of the tyConTyVars
 (or of equal length to the tyConArity, if there are no tyConTyVars). An
 example demonstrates these best: say we have a tycon T, with parameters a at
@@ -300,6 +327,39 @@ it's worth noting that (~#)'s parameters are at role N. Promoted data
 constructors' type arguments are at role R. All kind arguments are at role
 N.
 
+Note [Unboxed tuple RuntimeRep vars]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The contents of an unboxed tuple may have any representation. Accordingly,
+the kind of the unboxed tuple constructor is runtime-representation
+polymorphic. For example,
+
+   (#,#) :: forall (q :: RuntimeRep) (r :: RuntimeRep). TYPE q -> TYPE r -> #
+
+These extra tyvars (v and w) cause some delicate processing around tuples,
+where we used to be able to assume that the tycon arity and the
+datacon arity were the same.
+
+Note [Injective type families]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We allow injectivity annotations for type families (both open and closed):
+
+  type family F (a :: k) (b :: k) = r | r -> a
+  type family G a b = res | res -> a b where ...
+
+Injectivity information is stored in the `famTcInj` field of `FamilyTyCon`.
+`famTcInj` maybe stores a list of Bools, where each entry corresponds to a
+single element of `tyConTyVars` (both lists should have identical length). If no
+injectivity annotation was provided `famTcInj` is Nothing. From this follows an
+invariant that if `famTcInj` is a Just then at least one element in the list
+must be True.
+
+See also:
+ * [Injectivity annotation] in HsDecls
+ * [Renaming injectivity annotation] in RnSource
+ * [Verifying injectivity annotation] in FamInstEnv
+ * [Type inference for type families with injectivity] in TcInteract
+
+
 ************************************************************************
 *                                                                      *
 \subsection{The data type}
@@ -307,6 +367,15 @@ N.
 ************************************************************************
 -}
 
+{- Note [TyCon binders]
+~~~~~~~~~~~~~~~~~~~~~~~
+
+data TyConBinder = TCB TyVar TcConBinderVis
+
+data TyConBinderVis = NamedTCB VisiblityFlag
+                    | AnonTCB
+-}
+
 -- | TyCons represent type constructors. Type constructors are introduced by
 -- things such as:
 --
@@ -335,18 +404,28 @@ data TyCon
 
         tyConName   :: Name,     -- ^ Name of the constructor
 
-        tyConKind   :: Kind,     -- ^ Kind of this TyCon (full kind, not just
-                                 -- the return kind)
+        -- See Note [The binders/kind/arity fields of a TyCon]
+        tyConBinders :: [TyBinder], -- ^ The TyBinders for this TyCon's kind.
+        tyConResKind :: Kind,       -- ^ Result kind
+        tyConKind   :: Kind,        -- ^ Kind of this TyCon
+        tyConArity  :: Arity,       -- ^ Arity
 
-        tyConArity  :: Arity     -- ^ Number of arguments this TyCon must
-                                 -- receive to be considered saturated
-                                 -- (including implicit kind variables)
+        tcRepName :: TyConRepName
     }
 
-  -- | 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 data types, from
+  --     - @data@ declararations
+  --     - @newtype@ declarations
+  --     - data instance declarations
+  --     - type instance declarations
+  --     - the TyCon generated by a class declaration
+  --     - boxed tuples
+  --     - unboxed tuples
+  --     - constraint tuples
+  -- All these constructors are lifted and boxed except unboxed tuples
+  -- which should have an 'UnboxedAlgTyCon' parent.
+  -- Data/newtype/type /families/ are handled by 'FamilyTyCon'.
+  -- See 'AlgTyConRhs' for more information.
   | AlgTyCon {
         tyConUnique  :: Unique,  -- ^ A Unique of this TyCon. Invariant:
                                  -- identical to Unique of Name stored in
@@ -354,16 +433,16 @@ data TyCon
 
         tyConName    :: Name,    -- ^ Name of the constructor
 
-        tyConKind    :: Kind,    -- ^ Kind of this TyCon (full kind, not just
-                                 -- the return kind)
-
-        tyConArity   :: Arity,   -- ^ Number of arguments this TyCon must
-                                 -- receive to be considered saturated
-                                 -- (including implicit kind variables)
+        -- See Note [The binders/kind/arity fields of a TyCon]
+        tyConBinders :: [TyBinder], -- ^ The TyBinders for this TyCon's kind.
+        tyConResKind :: Kind,       -- ^ Result kind
+        tyConKind   :: Kind,        -- ^ Kind of this TyCon
+        tyConArity  :: Arity,       -- ^ Arity
 
+        -- See Note [tyConTyVars and tyConBinders]
         tyConTyVars  :: [TyVar], -- ^ The kind and type variables used in the
                                  -- type constructor.
-                                 -- Invariant: length tyvars = arity
+                                 -- Invariant: length tyConTyVars = tyConArity
                                  -- Precisely, this list scopes over:
                                  --
                                  -- 1. The 'algTcStupidTheta'
@@ -374,7 +453,7 @@ data TyCon
                                  -- constructors.
 
         tcRoles      :: [Role],  -- ^ The role for each type variable
-                                 -- This list has the same length as tyConTyVars
+                                 -- This list has length = tyConArity
                                  -- See also Note [TyCon Role signatures]
 
         tyConCType   :: Maybe CType,-- ^ The C type that should be used
@@ -397,15 +476,16 @@ data TyCon
         algTcRhs    :: AlgTyConRhs, -- ^ Contains information about the
                                     -- data constructors of the algebraic type
 
+        algTcFields :: FieldLabelEnv, -- ^ Maps a label to information
+                                      -- about the field
+
         algTcRec    :: RecFlag,     -- ^ Tells us whether the data type is part
                                     -- of a mutually-recursive group or not
 
-        algTcParent :: TyConParent, -- ^ Gives the class or family declaration
-                                    -- 'TyCon' for derived 'TyCon's representing
-                                    -- class or family instances, respectively.
-                                    -- See also 'synTcParent'
+        algTcParent :: AlgTyConFlav -- ^ Gives the class or family declaration
+                                       -- 'TyCon' for derived 'TyCon's representing
+                                       -- class or family instances, respectively.
 
-        tcPromoted  :: Maybe TyCon  -- ^ Promoted TyCon, if any
     }
 
   -- | Represents type synonyms
@@ -416,26 +496,27 @@ data TyCon
 
         tyConName    :: Name,    -- ^ Name of the constructor
 
-        tyConKind    :: Kind,    -- ^ Kind of this TyCon (full kind, not just
-                                 -- the return kind)
-
-        tyConArity   :: Arity,   -- ^ Number of arguments this TyCon must
-                                 -- receive to be considered saturated
-                                 -- (including implicit kind variables)
+        -- See Note [The binders/kind/arity fields of a TyCon]
+        tyConBinders :: [TyBinder], -- ^ The TyBinders for this TyCon's kind.
+        tyConResKind :: Kind,       -- ^ Result kind
+        tyConKind   :: Kind,        -- ^ Kind of this TyCon
+        tyConArity  :: Arity,       -- ^ Arity
 
+        -- See Note [tyConTyVars and tyConBinders]
         tyConTyVars  :: [TyVar], -- ^ List of type and kind variables in this
                                  -- TyCon. Includes implicit kind variables.
-                                 -- Invariant: length tyConTyVars = tyConArity
+                                 -- Scopes over: synTcRhs
 
         tcRoles      :: [Role],  -- ^ The role for each type variable
-                                 -- This list has the same length as tyConTyVars
+                                 -- This list has length = tyConArity
                                  -- See also Note [TyCon Role signatures]
 
         synTcRhs     :: Type     -- ^ Contains information about the expansion
                                  -- of the synonym
     }
 
-  -- | Represents type families
+  -- | Represents families (both type and data)
+  -- Argument roles are all Nominal
   | FamilyTyCon {
         tyConUnique  :: Unique,  -- ^ A Unique of this TyCon. Invariant:
                                  -- identical to Unique of Name stored in
@@ -443,37 +524,40 @@ data TyCon
 
         tyConName    :: Name,    -- ^ Name of the constructor
 
-        tyConKind    :: Kind,    -- ^ Kind of this TyCon (full kind, not just
-                                 -- the return kind)
-
-        tyConArity   :: Arity,   -- ^ Number of arguments this TyCon must
-                                 -- receive to be considered saturated
-                                 -- (including implicit kind variables)
+        -- See Note [The binders/kind/arity fields of a TyCon]
+        tyConBinders :: [TyBinder], -- ^ The TyBinders for this TyCon's kind.
+        tyConResKind :: Kind,       -- ^ Result kind
+        tyConKind   :: Kind,        -- ^ Kind of this TyCon
+        tyConArity  :: Arity,       -- ^ Arity
 
+        -- See Note [tyConTyVars and tyConBinders]
         tyConTyVars  :: [TyVar], -- ^ The kind and 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.
+            -- Needed to connect an associated family TyCon
+            -- with its parent class; see TcValidity.checkConsistentFamInst
+
+        famTcResVar  :: Maybe Name,   -- ^ Name of result type variable, used
+                                      -- for pretty-printing with --show-iface
+                                      -- and for reifying TyCon in Template
+                                      -- Haskell
 
         famTcFlav    :: FamTyConFlav, -- ^ Type family flavour: open, closed,
                                       -- abstract, built-in. See comments for
                                       -- FamTyConFlav
 
-        famTcParent  :: TyConParent   -- ^ TyCon of enclosing class for
-                                      -- associated type families
+        famTcParent  :: Maybe Class,  -- ^ For *associated* type/data families
+                                      -- The class in whose declaration the family is declared
+                                      -- See Note [Associated families and their parent class]
 
+        famTcInj     :: Injectivity   -- ^ is this a type family injective in
+                                      -- its type variables? Nothing if no
+                                      -- injectivity annotation was given
     }
 
   -- | Primitive types; cannot be defined in Haskell. This includes
   -- the usual suspects (such as @Int#@) as well as foreign-imported
-  -- types and kinds
+  -- types and kinds (@*@, @#@, and @?@)
   | PrimTyCon {
         tyConUnique   :: Unique, -- ^ A Unique of this TyCon. Invariant:
                                  -- identical to Unique of Name stored in
@@ -481,50 +565,59 @@ data TyCon
 
         tyConName     :: Name,   -- ^ Name of the constructor
 
-        tyConKind     :: Kind,   -- ^ Kind of this TyCon (full kind, not just
-                                 -- the return kind)
-
-        tyConArity    :: Arity,  -- ^ Number of arguments this TyCon must
-                                 -- receive to be considered saturated
-                                 -- (including implicit kind variables)
+        -- See Note [The binders/kind/arity fields of a TyCon]
+        tyConBinders :: [TyBinder], -- ^ The TyBinders for this TyCon's kind.
+        tyConResKind :: Kind,       -- ^ Result kind
+        tyConKind   :: Kind,        -- ^ Kind of this TyCon
+        tyConArity  :: Arity,       -- ^ Arity
 
         tcRoles       :: [Role], -- ^ The role for each type variable
-                                 -- This list has the same length as tyConTyVars
+                                 -- This list has length = tyConArity
                                  -- See also Note [TyCon Role signatures]
 
-        primTyConRep  :: PrimRep,-- ^ Many primitive tycons are unboxed, but
-                                 -- some are boxed (represented by
-                                 -- pointers). This 'PrimRep' holds that
-                                 -- information.  Only relevant if tyConKind = *
-
-        isUnLifted   :: Bool     -- ^ Most primitive tycons are unlifted (may
+        isUnlifted   :: Bool,    -- ^ Most primitive tycons are unlifted (may
                                  -- not contain bottom) but other are lifted,
                                  -- e.g. @RealWorld@
+                                 -- Only relevant if tyConKind = *
+
+        primRepName :: Maybe TyConRepName   -- Only relevant for kind TyCons
+                                            -- i.e, *, #, ?
     }
 
   -- | Represents promoted data constructor.
   | PromotedDataCon {          -- See Note [Promoted data constructors]
-        tyConUnique :: Unique, -- ^ Same Unique as the data constructor
-        tyConName   :: Name,   -- ^ Same Name as the data constructor
-        tyConArity  :: Arity,
-        tyConKind   :: Kind,   -- ^ Translated type of the data constructor
-        tcRoles     :: [Role], -- ^ Roles: N for kind vars, R for type vars
-        dataCon     :: DataCon -- ^ Corresponding data constructor
+        tyConUnique  :: Unique,     -- ^ Same Unique as the data constructor
+        tyConName    :: Name,       -- ^ Same Name as the data constructor
+
+        -- See Note [The binders/kind/arity fields of a TyCon]
+        tyConBinders :: [TyBinder], -- ^ The TyBinders for this TyCon's kind.
+        tyConResKind :: Kind,       -- ^ Result kind
+        tyConKind   :: Kind,        -- ^ Kind of this TyCon
+        tyConArity  :: Arity,       -- ^ Arity
+
+        tcRoles       :: [Role],    -- ^ Roles: N for kind vars, R for type vars
+        dataCon       :: DataCon,   -- ^ Corresponding data constructor
+        tcRepName     :: TyConRepName,
+        promDcRepInfo :: RuntimeRepInfo  -- ^ See comments with 'RuntimeRepInfo'
     }
 
-  -- | Represents promoted type constructor.
-  | PromotedTyCon {
-        tyConUnique :: Unique, -- ^ Same Unique as the type constructor
-        tyConName   :: Name,   -- ^ Same Name as the type constructor
-        tyConArity  :: Arity,  -- ^ n if ty_con :: * -> ... -> *  n times
-        tyConKind   :: Kind,   -- ^ Always TysPrim.superKind
-        ty_con      :: TyCon   -- ^ Corresponding type constructor
-    }
-
-  deriving Typeable
+  -- | These exist only during a recursive type/class type-checking knot.
+  | TcTyCon {
+        tyConUnique :: Unique,
+        tyConName   :: Name,
+        tyConUnsat  :: Bool,  -- ^ can this tycon be unsaturated?
+
+        -- See Note [The binders/kind/arity fields of a TyCon]
+        tyConTyVars  :: [TyVar],    -- ^ The TyCon's parameterised tyvars
+        tyConBinders :: [TyBinder], -- ^ The TyBinders for this TyCon's kind.
+        tyConResKind :: Kind,       -- ^ Result kind
+        tyConKind    :: Kind,       -- ^ Kind of this TyCon
+        tyConArity   :: Arity,      -- ^ Arity
+
+        tcTyConScopedTyVars :: [TyVar] -- ^ Scoped tyvars over the
+                                       -- tycon's body. See Note [TcTyCon]
+      }
 
--- | Names of the fields in an algebraic record type
-type FieldLabel = Name
 
 -- | Represents right-hand-sides of 'TyCon's for algebraic types
 data AlgTyConRhs
@@ -536,20 +629,6 @@ data AlgTyConRhs
       Bool      -- True  <=> It's definitely a distinct data type,
                 --           equal only to itself; ie not a newtype
                 -- False <=> Not sure
-                -- See Note [AbstractTyCon and type equality]
-
-    -- | 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
@@ -603,18 +682,24 @@ data AlgTyConRhs
                              -- again check Trac #1072.
     }
 
-{-
-Note [AbstractTyCon and type equality]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-TODO
--}
+-- | Some promoted datacons signify extra info relevant to GHC. For example,
+-- the @IntRep@ constructor of @RuntimeRep@ corresponds to the 'IntRep'
+-- constructor of 'PrimRep'. This data structure allows us to store this
+-- information right in the 'TyCon'. The other approach would be to look
+-- up things like @RuntimeRep@'s @PrimRep@ by known-key every time.
+data RuntimeRepInfo
+  = NoRRI       -- ^ an ordinary promoted data con
+  | RuntimeRep ([Type] -> PrimRep)
+      -- ^ A constructor of @RuntimeRep@. The argument to the function should
+      -- be the list of arguments to the promoted datacon.
+  | VecCount Int         -- ^ A constructor of @VecCount@
+  | VecElem PrimElemRep  -- ^ A constructor of @VecElem@
 
 -- | 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 DataFamilyTyCon {}            = []
 visibleDataCons (DataTyCon{ data_cons = cs }) = cs
 visibleDataCons (NewTyCon{ data_con = c })    = [c]
 visibleDataCons (TupleTyCon{ data_con = c })  = [c]
@@ -622,24 +707,24 @@ visibleDataCons (TupleTyCon{ data_con = c })  = [c]
 -- ^ Both type classes as well as family instances imply implicit
 -- type constructors.  These implicit type constructors refer to their parent
 -- structure (ie, the class or family from which they derive) using a type of
--- the following form.  We use 'TyConParent' for both algebraic and synonym
--- types, but the variant 'ClassTyCon' will only be used by algebraic 'TyCon's.
-data TyConParent
+-- the following form.
+data AlgTyConFlav
   = -- | An ordinary type constructor has no parent.
-    NoParentTyCon
+    VanillaAlgTyCon
+       TyConRepName
+
+    -- | An unboxed type constructor. Note that this carries no TyConRepName
+    -- as it is not representable.
+  | UnboxedAlgTyCon
 
   -- | Type constructors representing a class dictionary.
-  -- See Note [ATyCon for classes] in TypeRep
+  -- See Note [ATyCon for classes] in TyCoRep
   | ClassTyCon
         Class           -- INVARIANT: the classTyCon of this Class is the
                         -- current tycon
+        TyConRepName
 
-  -- | An *associated* type of a class.
-  | AssocFamilyTyCon
-        Class           -- The class in whose declaration the family is declared
-                        -- See Note [Associated families and their parent class]
-
-  -- | Type constructors representing an instance of a *data* family.
+  -- | Type constructors representing an *instance* of a *data* family.
   -- Parameters:
   --
   --  1) The type family in question
@@ -650,9 +735,10 @@ data TyConParent
   --
   --  3) A 'CoTyCon' identifying the representation
   --  type with the type instance family
-  | FamInstTyCon          -- See Note [Data type families]
+  | DataFamInstTyCon          -- See Note [Data type families]
         (CoAxiom Unbranched)  -- The coercion axiom.
-               -- Generally of kind   T ty1 ty2 ~ R:T a b c
+               -- A *Representational* coercion,
+               -- of kind   T ty1 ty2   ~R   R:T a b c
                -- where T is the family TyCon,
                -- and R:T is the representation TyCon (ie this one)
                -- and a,b,c are the tyConTyVars of this TyCon
@@ -670,34 +756,52 @@ data TyConParent
         -- gives a representation tycon:
         --      data R:TList a = ...
         --      axiom co a :: T [a] ~ R:TList a
-        -- with R:TList's algTcParent = FamInstTyCon T [a] co
+        -- with R:TList's algTcParent = DataFamInstTyCon T [a] co
 
-instance Outputable TyConParent where
-    ppr NoParentTyCon           = text "No parent"
-    ppr (ClassTyCon cls)        = text "Class parent" <+> ppr cls
-    ppr (AssocFamilyTyCon cls)  =
-        text "Class parent (assoc. family)" <+> ppr cls
-    ppr (FamInstTyCon _ tc tys) =
-        text "Family parent (family instance)" <+> ppr tc <+> sep (map ppr tys)
+instance Outputable AlgTyConFlav where
+    ppr (VanillaAlgTyCon {})        = text "Vanilla ADT"
+    ppr (UnboxedAlgTyCon {})        = text "Unboxed ADT"
+    ppr (ClassTyCon cls _)          = text "Class parent" <+> ppr cls
+    ppr (DataFamInstTyCon _ tc tys) = text "Family parent (family instance)"
+                                      <+> ppr tc <+> sep (map pprType tys)
 
--- | Checks the invariants of a 'TyConParent' given the appropriate type class
+-- | Checks the invariants of a 'AlgTyConFlav' given the appropriate type class
 -- name, if any
-okParent :: Name -> TyConParent -> Bool
-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) = tyConArity fam_tc == length tys
+okParent :: Name -> AlgTyConFlav -> Bool
+okParent _       (VanillaAlgTyCon {})            = True
+okParent _       (UnboxedAlgTyCon)               = True
+okParent tc_name (ClassTyCon cls _)              = tc_name == tyConName (classTyCon cls)
+okParent _       (DataFamInstTyCon _ fam_tc tys) = tyConArity fam_tc == length tys
 
-isNoParent :: TyConParent -> Bool
-isNoParent NoParentTyCon = True
-isNoParent _             = False
+isNoParent :: AlgTyConFlav -> Bool
+isNoParent (VanillaAlgTyCon {}) = True
+isNoParent _                   = False
 
 --------------------
 
+data Injectivity
+  = NotInjective
+  | Injective [Bool]   -- 1-1 with tyConTyVars (incl kind vars)
+  deriving( Eq )
+
 -- | Information pertaining to the expansion of a type synonym (@type@)
 data FamTyConFlav
-  = -- | An open type synonym family  e.g. @type family F x y :: * -> *@
-     OpenSynFamilyTyCon
+  = -- | 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 family T a :: *
+    --
+    -- Or an associated data type declaration, within a class declaration:
+    --
+    -- > class C a b where
+    -- >   data T b :: *
+     DataFamilyTyCon
+       TyConRepName
+
+     -- | An open type synonym family  e.g. @type family F x y :: * -> *@
+   | OpenSynFamilyTyCon
 
    -- | A closed type synonym family  e.g.
    -- @type family F x where { F Int = Bool }@
@@ -711,7 +815,49 @@ data FamTyConFlav
    -- | Built-in type family used by the TypeNats solver
    | BuiltInSynFamTyCon BuiltInSynFamily
 
-{-
+{- Note [The binders/kind/arity fields of a TyCon]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+All TyCons have this group of fields
+  tyConBinders :: [TyBinder]
+  tyConResKind :: Kind
+  tyConKind    :: Kind   -- Cached = mkPiTys tyConBinders tyConResKind
+  tyConArity   :: Arity  -- Cached = length tyConBinders
+
+They fit together like so:
+
+* tyConBinders gives the telescope of Named (forall'd)
+  Anon (ordinary ->) binders
+
+* Note that tyConBinders /includes/ Anon arguments.  For example:
+    type App a (b :: k) = a b
+      -- App :: forall {k}; (k->*) -> k -> *
+  we get
+    tyConTyBinders = [ Named (k :: *) Invisible, Anon (k->*), Anon k ]
+
+* tyConKind is the full kind of the TyCon,
+  not just the result kind
+
+* tyConArity is the arguments this TyCon must be applied to, to be
+  considered saturated.  Here we mean "applied to in the actual Type",
+  not surface syntax; i.e. including implicit kind variables.
+
+Note [tyConTyVars and tyConBinders]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+  type App a (b :: k) = a b
+    -- App :: forall {k}; (k->*) -> k -> *
+
+For App we get:
+  tyConTyVars    = [ k:*,                      a:k->*,      b:k]
+  tyConTyBinders = [ Named (k :: *) Invisible, Anon (k->*), Anon k ]
+
+The tyConBinder field is used to construct the kind of App, namely
+  App :: forall {k}; (k->*) -> k -> *
+The tyConTyVars field always corresponds 1-1 with tyConBinders, and
+records the names of the binders.  That is important for type synonyms,
+etc, where those names scope over some other field in the TyCon. In
+this case, 'a' and 'b' are mentioned in the RHS.
+
 Note [Closed type families]
 ~~~~~~~~~~~~~~~~~~~~~~~~~
 * In an open type family you can add new instances later.  This is the
@@ -728,27 +874,13 @@ nothing for the axiom to prove!
 
 Note [Promoted data constructors]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-A data constructor can be promoted to become a type constructor,
-via the PromotedTyCon alternative in TyCon.
-
-* Only data constructors with
-     (a) no kind polymorphism
-     (b) no constraints in its type (eg GADTs)
-  are promoted.  Existentials are ok; see Trac #7347.
+All data constructors can be promoted to become a type constructor,
+via the PromotedDataCon alternative in TyCon.
 
 * The TyCon promoted from a DataCon has the *same* Name and Unique as
   the DataCon.  Eg. If the data constructor Data.Maybe.Just(unique 78,
   say) is promoted to a TyCon whose name is Data.Maybe.Just(unique 78)
 
-* The *kind* of a promoted DataCon may be polymorphic.  Example:
-    type of DataCon           Just :: forall (a:*). a -> Maybe a
-    kind of (promoted) tycon  Just :: forall (a:box). a -> Maybe a
-  The kind is not identical to the type, because of the */box
-  kind signature on the forall'd variable; so the tyConKind field of
-  PromotedTyCon is not identical to the dataConUserType of the
-  DataCon.  But it's the same modulo changing the variable kinds,
-  done by DataCon.promoteType.
-
 * Small note: We promote the *user* type of the DataCon.  Eg
      data T = MkT {-# UNPACK #-} !(Bool, Bool)
   The promoted kind is
@@ -833,9 +965,98 @@ so the coercion tycon CoT must have
         kind:    T ~ []
  and    arity:   0
 
+Note [TcTyCon]
+~~~~~~~~~~~~~~
+When checking a type/class declaration (in module TcTyClsDecls), we come
+upon knowledge of the eventual tycon in bits and pieces. First, we use
+getInitialKinds to look over the user-provided kind signature of a tycon
+(including, for example, the number of parameters written to the tycon)
+to get an initial shape of the tycon's kind. Then, using these initial
+kinds, we kind-check the body of the tycon (class methods, data constructors,
+etc.), filling in the metavariables in the tycon's initial kind.
+We then generalize to get the tycon's final, fixed kind. Finally, once
+this has happened for all tycons in a mutually recursive group, we
+can desugar the lot.
+
+For convenience, we store partially-known tycons in TcTyCons, which
+might store meta-variables. These TcTyCons are stored in the local
+environment in TcTyClsDecls, until the real full TyCons can be created
+during desugaring. A desugared program should never have a TcTyCon.
+
+A challenging piece in all of this is that we end up taking three separate
+passes over every declaration: one in getInitialKind (this pass look only
+at the head, not the body), one in kcTyClDecls (to kind-check the body),
+and a final one in tcTyClDecls (to desugar). In the latter two passes,
+we need to connect the user-written type variables in an LHsQTyVars
+with the variables in the tycon's inferred kind. Because the tycon might
+not have a CUSK, this matching up is, in general, quite hard to do.
+(Look through the git history between Dec 2015 and Apr 2016 for
+TcHsType.splitTelescopeTvs!) Instead of trying, we just store the list
+of type variables to bring into scope in the later passes when we create
+a TcTyCon in getInitialKinds. Much easier this way! These tyvars are
+brought into scope in kcTyClTyVars and tcTyClTyVars, both in TcHsType.
+
+It is important that the scoped type variables not be zonked, as some
+scoped type variables come into existence as SigTvs. If we zonk, the
+Unique will change and the user-written occurrences won't match up with
+what we expect.
+
+In a TcTyCon, everything is zonked (except the scoped vars) after
+the kind-checking pass.
+
 ************************************************************************
 *                                                                      *
-\subsection{PrimRep}
+                 TyConRepName
+*                                                                      *
+********************************************************************* -}
+
+type TyConRepName = Name -- The Name of the top-level declaration
+                         --    $tcMaybe :: Data.Typeable.Internal.TyCon
+                         --    $tcMaybe = TyCon { tyConName = "Maybe", ... }
+
+tyConRepName_maybe :: TyCon -> Maybe TyConRepName
+tyConRepName_maybe (FunTyCon   { tcRepName = rep_nm })
+  = Just rep_nm
+tyConRepName_maybe (PrimTyCon  { primRepName = mb_rep_nm })
+  = mb_rep_nm
+tyConRepName_maybe (AlgTyCon { algTcParent = parent })
+  | VanillaAlgTyCon rep_nm <- parent = Just rep_nm
+  | ClassTyCon _ rep_nm    <- parent = Just rep_nm
+tyConRepName_maybe (FamilyTyCon { famTcFlav = DataFamilyTyCon rep_nm })
+  = Just rep_nm
+tyConRepName_maybe (PromotedDataCon { tcRepName = rep_nm })
+  = Just rep_nm
+tyConRepName_maybe _ = Nothing
+
+-- | Make a 'Name' for the 'Typeable' representation of the given wired-in type
+mkPrelTyConRepName :: Name -> TyConRepName
+-- See Note [Grand plan for Typeable] in 'TcTypeable' in TcTypeable.
+mkPrelTyConRepName tc_name  -- Prelude tc_name is always External,
+                            -- so nameModule will work
+  = mkExternalName rep_uniq rep_mod rep_occ (nameSrcSpan tc_name)
+  where
+    name_occ  = nameOccName tc_name
+    name_mod  = nameModule  tc_name
+    name_uniq = nameUnique  tc_name
+    rep_uniq | isTcOcc name_occ = tyConRepNameUnique   name_uniq
+             | otherwise        = dataConRepNameUnique name_uniq
+    (rep_mod, rep_occ) = tyConRepModOcc name_mod name_occ
+
+-- | The name (and defining module) for the Typeable representation (TyCon) of a
+-- type constructor.
+--
+-- See Note [Grand plan for Typeable] in 'TcTypeable' in TcTypeable.
+tyConRepModOcc :: Module -> OccName -> (Module, OccName)
+tyConRepModOcc tc_module tc_occ = (rep_module, mkTyConRepOcc tc_occ)
+  where
+    rep_module
+      | tc_module == gHC_PRIM = gHC_TYPES
+      | otherwise             = tc_module
+
+
+{- *********************************************************************
+*                                                                      *
+                 PrimRep
 *                                                                      *
 ************************************************************************
 
@@ -972,6 +1193,36 @@ primRepIsFloat  DoubleRep    = Just True
 primRepIsFloat  (VecRep _ _) = Nothing
 primRepIsFloat  _            = Just False
 
+
+{-
+************************************************************************
+*                                                                      *
+                             Field labels
+*                                                                      *
+************************************************************************
+-}
+
+-- | The labels for the fields of this particular 'TyCon'
+tyConFieldLabels :: TyCon -> [FieldLabel]
+tyConFieldLabels tc = dFsEnvElts $ tyConFieldLabelEnv tc
+
+-- | The labels for the fields of this particular 'TyCon'
+tyConFieldLabelEnv :: TyCon -> FieldLabelEnv
+tyConFieldLabelEnv tc
+  | isAlgTyCon tc = algTcFields tc
+  | otherwise     = emptyDFsEnv
+
+
+-- | Make a map from strings to FieldLabels from all the data
+-- constructors of this algebraic tycon
+fieldsOfAlgTcRhs :: AlgTyConRhs -> FieldLabelEnv
+fieldsOfAlgTcRhs rhs = mkDFsEnv [ (flLabel fl, fl)
+                                | fl <- dataConsFields (visibleDataCons rhs) ]
+  where
+    -- Duplicates in this list will be removed by 'mkFsEnv'
+    dataConsFields dcs = concatMap dataConFieldLabels dcs
+
+
 {-
 ************************************************************************
 *                                                                      *
@@ -987,15 +1238,18 @@ So we compromise, and move their Kind calculation to the call site.
 -}
 
 -- | Given the name of the function type constructor and it's kind, create the
--- corresponding 'TyCon'. It is reccomended to use 'TypeRep.funTyCon' if you want
+-- corresponding 'TyCon'. It is reccomended to use 'TyCoRep.funTyCon' if you want
 -- this functionality
-mkFunTyCon :: Name -> Kind -> TyCon
-mkFunTyCon name kind
+mkFunTyCon :: Name -> [TyBinder] -> Name -> TyCon
+mkFunTyCon name binders rep_nm
   = FunTyCon {
-        tyConUnique = nameUnique name,
-        tyConName   = name,
-        tyConKind   = kind,
-        tyConArity  = 2
+        tyConUnique  = nameUnique name,
+        tyConName    = name,
+        tyConBinders = binders,
+        tyConResKind = liftedTypeKind,
+        tyConKind    = mkPiTys binders liftedTypeKind,
+        tyConArity   = 2,
+        tcRepName    = rep_nm
     }
 
 -- | This is the making of an algebraic 'TyCon'. Notably, you have to
@@ -1003,7 +1257,8 @@ mkFunTyCon name kind
 -- type constructor - you can get hold of it easily (see Generics
 -- module)
 mkAlgTyCon :: Name
-           -> Kind              -- ^ Kind of the resulting 'TyCon'
+           -> [TyBinder]        -- ^ Binders of the resulting 'TyCon'
+           -> Kind              -- ^ Result kind
            -> [TyVar]           -- ^ 'TyVar's scoped over: see 'tyConTyVars'.
                                 --   Arity is inferred from the length of this
                                 --   list
@@ -1011,115 +1266,165 @@ mkAlgTyCon :: Name
            -> Maybe CType       -- ^ The C type this type corresponds to
                                 --   when using the CAPI FFI
            -> [PredType]        -- ^ Stupid theta: see 'algTcStupidTheta'
-           -> AlgTyConRhs       -- ^ Information about dat aconstructors
-           -> TyConParent
+           -> AlgTyConRhs       -- ^ Information about data constructors
+           -> AlgTyConFlav      -- ^ What flavour is it?
+                                -- (e.g. vanilla, type family)
            -> RecFlag           -- ^ Is the 'TyCon' recursive?
            -> Bool              -- ^ Was the 'TyCon' declared with GADT syntax?
-           -> Maybe TyCon       -- ^ Promoted version
            -> TyCon
-mkAlgTyCon name kind tyvars roles cType stupid rhs parent is_rec gadt_syn prom_tc
+mkAlgTyCon name binders res_kind tyvars roles cType stupid rhs parent is_rec gadt_syn
   = AlgTyCon {
         tyConName        = name,
         tyConUnique      = nameUnique name,
-        tyConKind        = kind,
+        tyConBinders     = binders,
+        tyConResKind     = res_kind,
+        tyConKind        = mkPiTys binders res_kind,
         tyConArity       = length tyvars,
         tyConTyVars      = tyvars,
         tcRoles          = roles,
         tyConCType       = cType,
         algTcStupidTheta = stupid,
         algTcRhs         = rhs,
+        algTcFields      = fieldsOfAlgTcRhs rhs,
         algTcParent      = ASSERT2( okParent name parent, ppr name $$ ppr parent ) parent,
         algTcRec         = is_rec,
-        algTcGadtSyntax  = gadt_syn,
-        tcPromoted       = prom_tc
+        algTcGadtSyntax  = gadt_syn
     }
 
 -- | Simpler specialization of 'mkAlgTyCon' for classes
-mkClassTyCon :: Name -> Kind -> [TyVar] -> [Role] -> AlgTyConRhs -> Class
-             -> RecFlag -> TyCon
-mkClassTyCon name kind tyvars roles rhs clas is_rec
-  = mkAlgTyCon name kind tyvars roles Nothing [] rhs (ClassTyCon clas)
+mkClassTyCon :: Name -> [TyBinder]
+             -> [TyVar] -> [Role] -> AlgTyConRhs -> Class
+             -> RecFlag -> Name -> TyCon
+mkClassTyCon name binders tyvars roles rhs clas is_rec tc_rep_name
+  = mkAlgTyCon name binders constraintKind tyvars roles Nothing [] rhs
+               (ClassTyCon clas tc_rep_name)
                is_rec False
-               Nothing    -- Class TyCons are not promoted
 
 mkTupleTyCon :: Name
-             -> Kind    -- ^ Kind of the resulting 'TyCon'
+             -> [TyBinder]
+             -> Kind    -- ^ Result kind of the 'TyCon'
              -> Arity   -- ^ Arity of the tuple
              -> [TyVar] -- ^ 'TyVar's scoped over: see 'tyConTyVars'
              -> DataCon
              -> TupleSort    -- ^ Whether the tuple is boxed or unboxed
-             -> Maybe TyCon  -- ^ Promoted version
-             -> TyConParent
+             -> AlgTyConFlav
              -> TyCon
-mkTupleTyCon name kind arity tyvars con sort prom_tc parent
+mkTupleTyCon name binders res_kind arity tyvars con sort parent
   = AlgTyCon {
         tyConName        = name,
         tyConUnique      = nameUnique name,
-        tyConKind        = kind,
+        tyConBinders     = binders,
+        tyConResKind     = res_kind,
+        tyConKind        = mkPiTys binders res_kind,
         tyConArity       = arity,
         tyConTyVars      = tyvars,
         tcRoles          = replicate arity Representational,
         tyConCType       = Nothing,
         algTcStupidTheta = [],
-        algTcRhs         = TupleTyCon { data_con = con, tup_sort = sort },
+        algTcRhs         = TupleTyCon { data_con = con,
+                                        tup_sort = sort },
+        algTcFields      = emptyDFsEnv,
         algTcParent      = parent,
         algTcRec         = NonRecursive,
-        algTcGadtSyntax  = False,
-        tcPromoted       = prom_tc
+        algTcGadtSyntax  = False
     }
 
+-- | Makes a tycon suitable for use during type-checking.
+-- The only real need for this is for printing error messages during
+-- a recursive type/class type-checking knot. It has a kind because
+-- TcErrors sometimes calls typeKind.
+-- See also Note [Kind checking recursive type and class declarations]
+-- in TcTyClsDecls.
+mkTcTyCon :: Name -> [TyVar]
+          -> [TyBinder] -> Kind  -- ^ /result/ kind only
+          -> Bool                -- ^ Can this be unsaturated?
+          -> [TyVar]             -- ^ Scoped type variables, see Note [TcTyCon]
+          -> TyCon
+mkTcTyCon name tvs binders res_kind unsat scoped_tvs
+  = TcTyCon { tyConUnique  = getUnique name
+            , tyConName    = name
+            , tyConTyVars  = tvs
+            , tyConBinders = binders
+            , tyConResKind = res_kind
+            , tyConKind    = mkPiTys binders res_kind
+            , tyConUnsat   = unsat
+            , tyConArity   = length binders
+            , tcTyConScopedTyVars = scoped_tvs }
+
 -- | Create an unlifted primitive 'TyCon', such as @Int#@
-mkPrimTyCon :: Name  -> Kind -> [Role] -> PrimRep -> TyCon
-mkPrimTyCon name kind roles rep
-  = mkPrimTyCon' name kind roles rep True
+mkPrimTyCon :: Name -> [TyBinder]
+            -> Kind   -- ^ /result/ kind
+            -> [Role] -> TyCon
+mkPrimTyCon name binders res_kind roles
+  = mkPrimTyCon' name binders res_kind roles True (Just $ mkPrelTyConRepName name)
 
 -- | Kind constructors
-mkKindTyCon :: Name -> Kind -> TyCon
-mkKindTyCon name kind
-  = mkPrimTyCon' name kind [] VoidRep True
+mkKindTyCon :: Name -> [TyBinder]
+            -> Kind  -- ^ /result/ kind
+            -> [Role] -> Name -> TyCon
+mkKindTyCon name binders res_kind roles rep_nm
+  = tc
+  where
+    tc = mkPrimTyCon' name binders res_kind roles False (Just rep_nm)
 
 -- | Create a lifted primitive 'TyCon' such as @RealWorld@
-mkLiftedPrimTyCon :: Name  -> Kind -> [Role] -> PrimRep -> TyCon
-mkLiftedPrimTyCon name kind roles rep
-  = mkPrimTyCon' name kind roles rep False
-
-mkPrimTyCon' :: Name  -> Kind -> [Role] -> PrimRep -> Bool -> TyCon
-mkPrimTyCon' name kind roles rep is_unlifted
+mkLiftedPrimTyCon :: Name -> [TyBinder]
+                  -> Kind   -- ^ /result/ kind
+                  -> [Role] -> TyCon
+mkLiftedPrimTyCon name binders res_kind roles
+  = mkPrimTyCon' name binders res_kind roles False (Just rep_nm)
+  where rep_nm = mkPrelTyConRepName name
+
+mkPrimTyCon' :: Name -> [TyBinder]
+             -> Kind    -- ^ /result/ kind
+             -> [Role]
+             -> Bool -> Maybe TyConRepName -> TyCon
+mkPrimTyCon' name binders res_kind roles is_unlifted rep_nm
   = PrimTyCon {
         tyConName    = name,
         tyConUnique  = nameUnique name,
-        tyConKind    = kind,
+        tyConBinders = binders,
+        tyConResKind = res_kind,
+        tyConKind    = mkPiTys binders res_kind,
         tyConArity   = length roles,
         tcRoles      = roles,
-        primTyConRep = rep,
-        isUnLifted   = is_unlifted
+        isUnlifted   = is_unlifted,
+        primRepName  = rep_nm
     }
 
 -- | Create a type synonym 'TyCon'
-mkSynonymTyCon :: Name -> Kind -> [TyVar] -> [Role] -> Type -> TyCon
-mkSynonymTyCon name kind tyvars roles rhs
+mkSynonymTyCon :: Name -> [TyBinder] -> Kind   -- ^ /result/ kind
+               -> [TyVar] -> [Role] -> Type -> TyCon
+mkSynonymTyCon name binders res_kind tyvars roles rhs
   = SynonymTyCon {
-        tyConName   = name,
-        tyConUnique = nameUnique name,
-        tyConKind   = kind,
-        tyConArity  = length tyvars,
-        tyConTyVars = tyvars,
-        tcRoles     = roles,
-        synTcRhs    = rhs
+        tyConName    = name,
+        tyConUnique  = nameUnique name,
+        tyConBinders = binders,
+        tyConResKind = res_kind,
+        tyConKind    = mkPiTys binders res_kind,
+        tyConArity   = length tyvars,
+        tyConTyVars  = tyvars,
+        tcRoles      = roles,
+        synTcRhs     = rhs
     }
 
 -- | Create a type family 'TyCon'
-mkFamilyTyCon:: Name -> Kind -> [TyVar] -> FamTyConFlav -> TyConParent
-             -> TyCon
-mkFamilyTyCon name kind tyvars flav parent
+mkFamilyTyCon :: Name -> [TyBinder] -> Kind  -- ^ /result/ kind
+              -> [TyVar] -> Maybe Name -> FamTyConFlav
+              -> Maybe Class -> Injectivity -> TyCon
+mkFamilyTyCon name binders res_kind tyvars resVar flav parent inj
   = FamilyTyCon
-      { tyConUnique = nameUnique name
-      , tyConName   = name
-      , tyConKind   = kind
-      , tyConArity  = length tyvars
-      , tyConTyVars = tyvars
-      , famTcFlav   = flav
-      , famTcParent = parent
+      { tyConUnique  = nameUnique name
+      , tyConName    = name
+      , tyConBinders = binders
+      , tyConResKind = res_kind
+      , tyConKind    = mkPiTys binders res_kind
+      , tyConArity   = length tyvars
+      , tyConTyVars  = tyvars
+      , famTcResVar  = resVar
+      , famTcFlav    = flav
+      , famTcParent  = parent
+      , famTcInj     = inj
       }
 
 
@@ -1127,32 +1432,24 @@ mkFamilyTyCon name kind tyvars flav parent
 -- Somewhat dodgily, we give it the same Name
 -- as the data constructor itself; when we pretty-print
 -- the TyCon we add a quote; see the Outputable TyCon instance
-mkPromotedDataCon :: DataCon -> Name -> Unique -> Kind -> [Role] -> TyCon
-mkPromotedDataCon con name unique kind roles
+mkPromotedDataCon :: DataCon -> Name -> TyConRepName -> [TyBinder] -> Kind -> [Role]
+                  -> RuntimeRepInfo -> TyCon
+mkPromotedDataCon con name rep_name binders res_kind roles rep_info
   = PromotedDataCon {
-        tyConName   = name,
-        tyConUnique = unique,
-        tyConArity  = arity,
-        tcRoles     = roles,
-        tyConKind   = kind,
-        dataCon     = con
+        tyConUnique   = nameUnique name,
+        tyConName     = name,
+        tyConArity    = arity,
+        tcRoles       = roles,
+        tyConBinders  = binders,
+        tyConResKind  = res_kind,
+        tyConKind     = mkPiTys binders res_kind,
+        dataCon       = con,
+        tcRepName     = rep_name,
+        promDcRepInfo = rep_info
   }
   where
     arity = length roles
 
--- | Create a promoted type constructor 'TyCon'
--- Somewhat dodgily, we give it the same Name
--- as the type constructor itself
-mkPromotedTyCon :: TyCon -> Kind -> TyCon
-mkPromotedTyCon tc kind
-  = PromotedTyCon {
-        tyConName   = getName tc,
-        tyConUnique = getUnique tc,
-        tyConArity  = tyConArity tc,
-        tyConKind   = kind,
-        ty_con      = tc
-  }
-
 isFunTyCon :: TyCon -> Bool
 isFunTyCon (FunTyCon {}) = True
 isFunTyCon _             = False
@@ -1162,12 +1459,13 @@ isAbstractTyCon :: TyCon -> Bool
 isAbstractTyCon (AlgTyCon { algTcRhs = AbstractTyCon {} }) = True
 isAbstractTyCon _ = False
 
--- | Make an algebraic 'TyCon' abstract. Panics if the supplied 'TyCon' is not
--- algebraic
+-- | Make an fake, abstract 'TyCon' from an existing one.
+-- Used when recovering from errors
 makeTyConAbstract :: TyCon -> TyCon
-makeTyConAbstract tc@(AlgTyCon { algTcRhs = rhs })
-  = tc { algTcRhs = AbstractTyCon (isGenInjAlgRhs rhs) }
-makeTyConAbstract tc = pprPanic "makeTyConAbstract" (ppr tc)
+makeTyConAbstract tc
+  = mkTcTyCon (tyConName tc) (tyConTyVars tc)
+              (tyConBinders tc) (tyConResKind tc)
+              (mightBeUnsaturatedTyCon tc) [{- no scoped vars -}]
 
 -- | Does this 'TyCon' represent something that cannot be defined in Haskell?
 isPrimTyCon :: TyCon -> Bool
@@ -1176,13 +1474,13 @@ isPrimTyCon _              = False
 
 -- | Is this 'TyCon' unlifted (i.e. cannot contain bottom)? Note that this can
 -- only be true for primitive and unboxed-tuple 'TyCon's
-isUnLiftedTyCon :: TyCon -> Bool
-isUnLiftedTyCon (PrimTyCon  {isUnLifted = is_unlifted})
+isUnliftedTyCon :: TyCon -> Bool
+isUnliftedTyCon (PrimTyCon  {isUnlifted = is_unlifted})
   = is_unlifted
-isUnLiftedTyCon (AlgTyCon { algTcRhs = rhs } )
+isUnliftedTyCon (AlgTyCon { algTcRhs = rhs } )
   | TupleTyCon { tup_sort = sort } <- rhs
   = not (isBoxed (tupleSortBoxity sort))
-isUnLiftedTyCon _ = False
+isUnliftedTyCon _ = False
 
 -- | Returns @True@ if the supplied 'TyCon' resulted from either a
 -- @data@ or @newtype@ declaration
@@ -1190,6 +1488,12 @@ isAlgTyCon :: TyCon -> Bool
 isAlgTyCon (AlgTyCon {})   = True
 isAlgTyCon _               = False
 
+-- | Returns @True@ for vanilla AlgTyCons -- that is, those created
+-- with a @data@ or @newtype@ declaration.
+isVanillaAlgTyCon :: TyCon -> Bool
+isVanillaAlgTyCon (AlgTyCon { algTcParent = VanillaAlgTyCon _ }) = True
+isVanillaAlgTyCon _                                              = False
+
 isDataTyCon :: TyCon -> Bool
 -- ^ Returns @True@ for data types that are /definitely/ represented by
 -- heap-allocated constructors.  These are scrutinised by Core-level
@@ -1207,7 +1511,6 @@ isDataTyCon (AlgTyCon {algTcRhs = rhs})
                            -> isBoxed (tupleSortBoxity sort)
         DataTyCon {}       -> True
         NewTyCon {}        -> False
-        DataFamilyTyCon {} -> False
         AbstractTyCon {}   -> False      -- We don't know, so return False
 isDataTyCon _ = False
 
@@ -1215,7 +1518,7 @@ isDataTyCon _ = False
 -- (where X is the role passed in):
 --   If (T a1 b1 c1) ~X (T a2 b2 c2), then (a1 ~X1 a2), (b1 ~X2 b2), and (c1 ~X3 c2)
 -- (where X1, X2, and X3, are the roles given by tyConRolesX tc X)
--- See also Note [Decomposing equalities] in TcCanonical
+-- See also Note [Decomposing equality] in TcCanonical
 isInjectiveTyCon :: TyCon -> Role -> Bool
 isInjectiveTyCon _                             Phantom          = False
 isInjectiveTyCon (FunTyCon {})                 _                = True
@@ -1223,27 +1526,30 @@ isInjectiveTyCon (AlgTyCon {})                 Nominal          = True
 isInjectiveTyCon (AlgTyCon {algTcRhs = rhs})   Representational
   = isGenInjAlgRhs rhs
 isInjectiveTyCon (SynonymTyCon {})             _                = False
+isInjectiveTyCon (FamilyTyCon { famTcFlav = DataFamilyTyCon _ })
+                                               Nominal          = True
+isInjectiveTyCon (FamilyTyCon { famTcInj = Injective inj }) _   = and inj
 isInjectiveTyCon (FamilyTyCon {})              _                = False
 isInjectiveTyCon (PrimTyCon {})                _                = True
 isInjectiveTyCon (PromotedDataCon {})          _                = True
-isInjectiveTyCon (PromotedTyCon {ty_con = tc}) r
-  = isInjectiveTyCon tc r
+isInjectiveTyCon tc@(TcTyCon {})               _
+  = pprPanic "isInjectiveTyCon sees a TcTyCon" (ppr tc)
 
 -- | 'isGenerativeTyCon' is true of 'TyCon's for which this property holds
 -- (where X is the role passed in):
 --   If (T tys ~X t), then (t's head ~X T).
--- See also Note [Decomposing equalities] in TcCanonical
+-- See also Note [Decomposing equality] in TcCanonical
 isGenerativeTyCon :: TyCon -> Role -> Bool
-isGenerativeTyCon = isInjectiveTyCon
-  -- as it happens, generativity and injectivity coincide, but there's
-  -- no a priori reason this must be the case
+isGenerativeTyCon (FamilyTyCon { famTcFlav = DataFamilyTyCon _ }) Nominal = True
+isGenerativeTyCon (FamilyTyCon {}) _ = False
+  -- in all other cases, injectivity implies generativitiy
+isGenerativeTyCon tc               r = isInjectiveTyCon tc r
 
 -- | Is this an 'AlgTyConRhs' of a 'TyCon' that is generative and injective
 -- with respect to representational equality?
 isGenInjAlgRhs :: AlgTyConRhs -> Bool
 isGenInjAlgRhs (TupleTyCon {})          = True
 isGenInjAlgRhs (DataTyCon {})           = True
-isGenInjAlgRhs (DataFamilyTyCon {})     = False
 isGenInjAlgRhs (AbstractTyCon distinct) = distinct
 isGenInjAlgRhs (NewTyCon {})            = False
 
@@ -1332,8 +1638,7 @@ isTypeSynonymTyCon _                 = False
 -- right hand side to which a synonym family application can expand.
 --
 
-mightBeUnsaturatedTyCon :: TyCon -> Bool
--- True iff we can decompose (T a b c) into ((T a b) c)
+-- | True iff we can decompose (T a b c) into ((T a b) c)
 --   I.e. is it injective and generative w.r.t nominal equality?
 --   That is, if (T a b) ~N d e f, is it always the case that
 --            (T ~N d), (a ~N e) and (b ~N f)?
@@ -1342,8 +1647,10 @@ mightBeUnsaturatedTyCon :: TyCon -> Bool
 -- It'd be unusual to call mightBeUnsaturatedTyCon on a regular H98
 -- type synonym, because you should probably have expanded it first
 -- But regardless, it's not decomposable
+mightBeUnsaturatedTyCon :: TyCon -> Bool
 mightBeUnsaturatedTyCon (SynonymTyCon {}) = False
-mightBeUnsaturatedTyCon (FamilyTyCon  {}) = False
+mightBeUnsaturatedTyCon (FamilyTyCon  { famTcFlav = flav}) = isDataFamFlav flav
+mightBeUnsaturatedTyCon (TcTyCon { tyConUnsat = unsat })   = unsat
 mightBeUnsaturatedTyCon _other            = True
 
 -- | Is this an algebraic 'TyCon' declared with the GADT syntax?
@@ -1363,22 +1670,28 @@ isEnumerationTyCon _ = False
 
 -- | Is this a 'TyCon', synonym or otherwise, that defines a family?
 isFamilyTyCon :: TyCon -> Bool
-isFamilyTyCon (FamilyTyCon {})                           = True
-isFamilyTyCon (AlgTyCon {algTcRhs = DataFamilyTyCon {}}) = True
-isFamilyTyCon _                                          = False
+isFamilyTyCon (FamilyTyCon {}) = True
+isFamilyTyCon _                = False
 
 -- | Is this a 'TyCon', synonym or otherwise, that defines a family with
 -- instances?
 isOpenFamilyTyCon :: TyCon -> Bool
-isOpenFamilyTyCon (FamilyTyCon {famTcFlav = OpenSynFamilyTyCon }) = True
-isOpenFamilyTyCon (AlgTyCon    {algTcRhs  = DataFamilyTyCon    }) = True
-isOpenFamilyTyCon _                                               = False
+isOpenFamilyTyCon (FamilyTyCon {famTcFlav = flav })
+  | OpenSynFamilyTyCon <- flav = True
+  | DataFamilyTyCon {} <- flav = True
+isOpenFamilyTyCon _            = False
 
 -- | Is this a synonym 'TyCon' that can have may have further instances appear?
 isTypeFamilyTyCon :: TyCon -> Bool
-isTypeFamilyTyCon (FamilyTyCon {}) = True
-isTypeFamilyTyCon _                = False
+isTypeFamilyTyCon (FamilyTyCon { famTcFlav = flav }) = not (isDataFamFlav flav)
+isTypeFamilyTyCon _                                  = False
+
+-- | Is this a synonym 'TyCon' that can have may have further instances appear?
+isDataFamilyTyCon :: TyCon -> Bool
+isDataFamilyTyCon (FamilyTyCon { famTcFlav = flav }) = isDataFamFlav flav
+isDataFamilyTyCon _                                  = False
 
+-- | Is this an open type family TyCon?
 isOpenTypeFamilyTyCon :: TyCon -> Bool
 isOpenTypeFamilyTyCon (FamilyTyCon {famTcFlav = OpenSynFamilyTyCon }) = True
 isOpenTypeFamilyTyCon _                                               = False
@@ -1390,25 +1703,29 @@ isClosedSynFamilyTyConWithAxiom_maybe
   (FamilyTyCon {famTcFlav = ClosedSynFamilyTyCon mb}) = mb
 isClosedSynFamilyTyConWithAxiom_maybe _               = Nothing
 
+-- | Try to read the injectivity information from a FamilyTyCon.
+-- For every other TyCon this function panics.
+familyTyConInjectivityInfo :: TyCon -> Injectivity
+familyTyConInjectivityInfo (FamilyTyCon { famTcInj = inj }) = inj
+familyTyConInjectivityInfo _ = panic "familyTyConInjectivityInfo"
+
 isBuiltInSynFamTyCon_maybe :: TyCon -> Maybe BuiltInSynFamily
 isBuiltInSynFamTyCon_maybe
   (FamilyTyCon {famTcFlav = BuiltInSynFamTyCon ops }) = Just ops
 isBuiltInSynFamTyCon_maybe _                          = Nothing
 
--- | Is this a synonym 'TyCon' that can have may have further instances appear?
-isDataFamilyTyCon :: TyCon -> Bool
-isDataFamilyTyCon (AlgTyCon {algTcRhs = DataFamilyTyCon {}}) = True
-isDataFamilyTyCon _ = False
+isDataFamFlav :: FamTyConFlav -> Bool
+isDataFamFlav (DataFamilyTyCon {}) = True   -- Data family
+isDataFamFlav _                    = False  -- Type synonym family
 
--- | Are we able to extract informationa 'TyVar' to class argument list
--- mappping from a given 'TyCon'?
+-- | Are we able to extract information 'TyVar' to class argument list
+-- mapping from a given 'TyCon'?
 isTyConAssoc :: TyCon -> Bool
 isTyConAssoc tc = isJust (tyConAssoc_maybe tc)
 
 tyConAssoc_maybe :: TyCon -> Maybe Class
-tyConAssoc_maybe tc = case tyConParent tc of
-                        AssocFamilyTyCon cls -> Just cls
-                        _                    -> Nothing
+tyConAssoc_maybe (FamilyTyCon { famTcParent = mb_cls }) = mb_cls
+tyConAssoc_maybe _                                      = Nothing
 
 -- The unit tycon didn't used to be classed as a tuple tycon
 -- but I thought that was silly so I've undone it
@@ -1447,25 +1764,6 @@ isRecursiveTyCon :: TyCon -> Bool
 isRecursiveTyCon (AlgTyCon {algTcRec = Recursive}) = True
 isRecursiveTyCon _                                 = False
 
-promotableTyCon_maybe :: TyCon -> Maybe TyCon
-promotableTyCon_maybe (AlgTyCon { tcPromoted = prom })   = prom
-promotableTyCon_maybe _                                  = Nothing
-
-promoteTyCon :: TyCon -> TyCon
-promoteTyCon tc = case promotableTyCon_maybe tc of
-                    Just prom_tc -> prom_tc
-                    Nothing      -> pprPanic "promoteTyCon" (ppr tc)
-
--- | Is this a PromotedTyCon?
-isPromotedTyCon :: TyCon -> Bool
-isPromotedTyCon (PromotedTyCon {}) = True
-isPromotedTyCon _                  = False
-
--- | Retrieves the promoted TyCon if this is a PromotedTyCon;
-isPromotedTyCon_maybe :: TyCon -> Maybe TyCon
-isPromotedTyCon_maybe (PromotedTyCon { ty_con = tc }) = Just tc
-isPromotedTyCon_maybe _ = Nothing
-
 -- | Is this a PromotedDataCon?
 isPromotedDataCon :: TyCon -> Bool
 isPromotedDataCon (PromotedDataCon {}) = True
@@ -1476,6 +1774,28 @@ isPromotedDataCon_maybe :: TyCon -> Maybe DataCon
 isPromotedDataCon_maybe (PromotedDataCon { dataCon = dc }) = Just dc
 isPromotedDataCon_maybe _ = Nothing
 
+-- | Is this tycon really meant for use at the kind level? That is,
+-- should it be permitted without -XDataKinds?
+isKindTyCon :: TyCon -> Bool
+isKindTyCon tc = getUnique tc `elementOfUniqSet` kindTyConKeys
+
+-- | These TyCons should be allowed at the kind level, even without
+-- -XDataKinds.
+kindTyConKeys :: UniqSet Unique
+kindTyConKeys = unionManyUniqSets
+  ( mkUniqSet [ liftedTypeKindTyConKey, starKindTyConKey, unicodeStarKindTyConKey
+              , constraintKindTyConKey, tYPETyConKey ]
+  : map (mkUniqSet . tycon_with_datacons) [ runtimeRepTyCon
+                                          , vecCountTyCon, vecElemTyCon ] )
+  where
+    tycon_with_datacons tc = getUnique tc : map getUnique (tyConDataCons tc)
+
+isLiftedTypeKindTyConName :: Name -> Bool
+isLiftedTypeKindTyConName
+  = (`hasKey` liftedTypeKindTyConKey) <||>
+    (`hasKey` starKindTyConKey) <||>
+    (`hasKey` unicodeStarKindTyConKey)
+
 -- | Identifies implicit tycons that, in particular, do not go into interface
 -- files (because they are implicitly reconstructed when the interface is
 -- read).
@@ -1495,20 +1815,23 @@ isImplicitTyCon :: TyCon -> Bool
 isImplicitTyCon (FunTyCon {})        = True
 isImplicitTyCon (PrimTyCon {})       = True
 isImplicitTyCon (PromotedDataCon {}) = True
-isImplicitTyCon (PromotedTyCon {})   = True
-isImplicitTyCon (AlgTyCon { algTcRhs = rhs, algTcParent = parent, tyConName = name })
+isImplicitTyCon (AlgTyCon { algTcRhs = rhs, tyConName = name })
   | TupleTyCon {} <- rhs             = isWiredInName name
-  | AssocFamilyTyCon {} <- parent    = True
-  | otherwise                        = False
-isImplicitTyCon (FamilyTyCon { famTcParent = parent })
-  | AssocFamilyTyCon {} <- parent    = True
   | otherwise                        = False
+isImplicitTyCon (FamilyTyCon { famTcParent = parent }) = isJust parent
 isImplicitTyCon (SynonymTyCon {})    = False
+isImplicitTyCon tc@(TcTyCon {})
+  = pprPanic "isImplicitTyCon sees a TcTyCon" (ppr tc)
 
 tyConCType_maybe :: TyCon -> Maybe CType
 tyConCType_maybe tc@(AlgTyCon {}) = tyConCType tc
 tyConCType_maybe _ = Nothing
 
+-- | Is this a TcTyCon? (That is, one only used during type-checking?)
+isTcTyCon :: TyCon -> Bool
+isTcTyCon (TcTyCon {}) = True
+isTcTyCon _            = False
+
 {-
 -----------------------------------------------
 --      Expand type-constructor applications
@@ -1527,10 +1850,9 @@ expandSynTyCon_maybe
 
 -- ^ Expand a type synonym application, if any
 expandSynTyCon_maybe tc tys
-  | SynonymTyCon { tyConTyVars = tvs, synTcRhs = rhs } <- tc
-  , let n_tvs = length tvs
-  = case n_tvs `compare` length tys of
-        LT -> Just (tvs `zip` tys, rhs, drop n_tvs tys)
+  | SynonymTyCon { tyConTyVars = tvs, synTcRhs = rhs, tyConArity = arity } <- tc
+  = case arity `compare` length tys of
+        LT -> Just (tvs `zip` tys, rhs, drop arity tys)
         EQ -> Just (tvs `zip` tys, rhs, [])
         GT -> Nothing
    | otherwise
@@ -1538,6 +1860,21 @@ expandSynTyCon_maybe tc tys
 
 ----------------
 
+-- | Check if the tycon actually refers to a proper `data` or `newtype`
+--  with user defined constructors rather than one from a class or other
+--  construction.
+isTyConWithSrcDataCons :: TyCon -> Bool
+isTyConWithSrcDataCons (AlgTyCon { algTcRhs = rhs, algTcParent = parent }) =
+  case rhs of
+    DataTyCon {}  -> isSrcParent
+    NewTyCon {}   -> isSrcParent
+    TupleTyCon {} -> isSrcParent
+    _ -> False
+  where
+    isSrcParent = isNoParent parent
+isTyConWithSrcDataCons _ = False
+
+
 -- | As 'tyConDataCons_maybe', but returns the empty list of constructors if no
 -- constructors could be found
 tyConDataCons :: TyCon -> [DataCon]
@@ -1595,7 +1932,6 @@ tyConFamilySize tc@(AlgTyCon { algTcRhs = rhs })
       DataTyCon { data_cons = cons } -> length cons
       NewTyCon {}                    -> 1
       TupleTyCon {}                  -> 1
-      DataFamilyTyCon {}             -> 0
       _                              -> pprPanic "tyConFamilySize 1" (ppr tc)
 tyConFamilySize tc = pprPanic "tyConFamilySize 2" (ppr tc)
 
@@ -1605,6 +1941,11 @@ algTyConRhs :: TyCon -> AlgTyConRhs
 algTyConRhs (AlgTyCon {algTcRhs = rhs}) = rhs
 algTyConRhs other = pprPanic "algTyConRhs" (ppr other)
 
+-- | Extract type variable naming the result of injective type family
+tyConFamilyResVar_maybe :: TyCon -> Maybe Name
+tyConFamilyResVar_maybe (FamilyTyCon {famTcResVar = res}) = res
+tyConFamilyResVar_maybe _                                 = Nothing
+
 -- | Get the list of roles for the type parameters of a TyCon
 tyConRoles :: TyCon -> [Role]
 -- See also Note [TyCon Role signatures]
@@ -1616,7 +1957,7 @@ tyConRoles tc
     ; FamilyTyCon {}                      -> const_role Nominal
     ; PrimTyCon { tcRoles = roles }       -> roles
     ; PromotedDataCon { tcRoles = roles } -> roles
-    ; PromotedTyCon {}                    -> const_role Nominal
+    ; TcTyCon {} -> pprPanic "tyConRoles sees a TcTyCon" (ppr tc)
     }
   where
     const_role r = replicate (tyConArity tc) r
@@ -1654,11 +1995,6 @@ 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
-tyConPrimRep (PrimTyCon {primTyConRep = rep}) = rep
-tyConPrimRep tc = ASSERT(not (isUnboxedTupleTyCon tc)) PtrRep
-
 -- | Find the \"stupid theta\" of the 'TyCon'. 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 ...@
@@ -1687,50 +2023,52 @@ famTyConFlav_maybe _                                = Nothing
 
 -- | Is this 'TyCon' that for a class instance?
 isClassTyCon :: TyCon -> Bool
-isClassTyCon (AlgTyCon {algTcParent = ClassTyCon _}) = True
-isClassTyCon _                                       = False
+isClassTyCon (AlgTyCon {algTcParent = ClassTyCon {}}) = True
+isClassTyCon _                                        = False
 
 -- | If this 'TyCon' is that for a class instance, return the class it is for.
 -- Otherwise returns @Nothing@
 tyConClass_maybe :: TyCon -> Maybe Class
-tyConClass_maybe (AlgTyCon {algTcParent = ClassTyCon clas}) = Just clas
-tyConClass_maybe _                                          = Nothing
+tyConClass_maybe (AlgTyCon {algTcParent = ClassTyCon clas _}) = Just clas
+tyConClass_maybe _                                            = Nothing
 
-----------------------------------------------------------------------------
-tyConParent :: TyCon -> TyConParent
-tyConParent (AlgTyCon    {algTcParent = parent}) = parent
-tyConParent (FamilyTyCon {famTcParent = parent}) = parent
-tyConParent _                                    = NoParentTyCon
+-- | Return the associated types of the 'TyCon', if any
+tyConATs :: TyCon -> [TyCon]
+tyConATs (AlgTyCon {algTcParent = ClassTyCon clas _}) = classATs clas
+tyConATs _                                            = []
 
 ----------------------------------------------------------------------------
 -- | Is this 'TyCon' that for a data family instance?
 isFamInstTyCon :: TyCon -> Bool
-isFamInstTyCon tc = case tyConParent tc of
-                      FamInstTyCon {} -> True
-                      _               -> False
+isFamInstTyCon (AlgTyCon {algTcParent = DataFamInstTyCon {} })
+  = True
+isFamInstTyCon _ = False
 
 tyConFamInstSig_maybe :: TyCon -> Maybe (TyCon, [Type], CoAxiom Unbranched)
-tyConFamInstSig_maybe tc
-  = case tyConParent tc of
-      FamInstTyCon ax f ts -> Just (f, ts, ax)
-      _                    -> Nothing
+tyConFamInstSig_maybe (AlgTyCon {algTcParent = DataFamInstTyCon ax f ts })
+  = Just (f, ts, ax)
+tyConFamInstSig_maybe _ = Nothing
 
--- | If this 'TyCon' is that of a family instance, return the family in question
+-- | If this 'TyCon' is that of a data family instance, return the family in question
 -- and the instance types. Otherwise, return @Nothing@
 tyConFamInst_maybe :: TyCon -> Maybe (TyCon, [Type])
-tyConFamInst_maybe tc
-  = case tyConParent tc of
-      FamInstTyCon _ f ts -> Just (f, ts)
-      _                   -> Nothing
+tyConFamInst_maybe (AlgTyCon {algTcParent = DataFamInstTyCon _ f ts })
+  = Just (f, ts)
+tyConFamInst_maybe _ = Nothing
 
--- | If this 'TyCon' is that of a family instance, return a 'TyCon' which
+-- | If this 'TyCon' is that of a data 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 (CoAxiom Unbranched)
-tyConFamilyCoercion_maybe tc
-  = case tyConParent tc of
-      FamInstTyCon co _ _ -> Just co
-      _                   -> Nothing
+tyConFamilyCoercion_maybe (AlgTyCon {algTcParent = DataFamInstTyCon ax _ _ })
+  = Just ax
+tyConFamilyCoercion_maybe _ = Nothing
+
+-- | Extract any 'RuntimeRepInfo' from this TyCon
+tyConRuntimeRepInfo :: TyCon -> RuntimeRepInfo
+tyConRuntimeRepInfo (PromotedDataCon { promDcRepInfo = rri }) = rri
+tyConRuntimeRepInfo _                                         = NoRRI
+  -- could panic in that second case. But Douglas Adams told me not to.
 
 {-
 ************************************************************************
@@ -1740,14 +2078,11 @@ tyConFamilyCoercion_maybe tc
 ************************************************************************
 
 @TyCon@s are compared by comparing their @Unique@s.
-
-The strictness analyser needs @Ord@. It is a lexicographic order with
-the property @(a<=b) || (b<=a)@.
 -}
 
 instance Eq TyCon where
-    a == b = case (a `compare` b) of { EQ -> True;   _ -> False }
-    a /= b = case (a `compare` b) of { EQ -> False;  _ -> True  }
+    a == b = getUnique a == getUnique b
+    a /= b = getUnique a /= getUnique b
 
 instance Ord TyCon where
     a <= b = case (a `compare` b) of { LT -> True;  EQ -> True;  GT -> False }
@@ -1766,31 +2101,30 @@ instance Outputable TyCon where
 
 tyConFlavour :: TyCon -> String
 tyConFlavour (AlgTyCon { algTcParent = parent, algTcRhs = rhs })
-  | ClassTyCon _ <- parent = "class"
+  | ClassTyCon _ <- parent = "class"
   | otherwise = case rhs of
                   TupleTyCon { tup_sort = sort }
                      | isBoxed (tupleSortBoxity sort) -> "tuple"
                      | otherwise                      -> "unboxed tuple"
                   DataTyCon {}       -> "data type"
                   NewTyCon {}        -> "newtype"
-                  DataFamilyTyCon {} -> "data family"
                   AbstractTyCon {}   -> "abstract type"
-tyConFlavour (FamilyTyCon {})     = "type family"
+tyConFlavour (FamilyTyCon { famTcFlav = flav })
+  | isDataFamFlav flav            = "data family"
+  | otherwise                     = "type family"
 tyConFlavour (SynonymTyCon {})    = "type synonym"
 tyConFlavour (FunTyCon {})        = "built-in type"
 tyConFlavour (PrimTyCon {})       = "built-in type"
 tyConFlavour (PromotedDataCon {}) = "promoted data constructor"
-tyConFlavour (PromotedTyCon {})   = "promoted type constructor"
+tyConFlavour tc@(TcTyCon {})
+  = pprPanic "tyConFlavour sees a TcTyCon" (ppr tc)
 
 pprPromotionQuote :: TyCon -> SDoc
-pprPromotionQuote (PromotedDataCon {}) = char '\''   -- Quote promoted DataCons
-                                                     -- in types
-pprPromotionQuote (PromotedTyCon {})   = ifPprDebug (char '\'')
-pprPromotionQuote _                    = empty -- However, we don't quote TyCons
-                                               -- in kinds e.g.
-                                               -- type family T a :: Bool -> *
-                                               -- cf Trac #5952.
-                                               -- Except with -dppr-debug
+-- Promoted data constructors already have a tick in their OccName
+pprPromotionQuote tc
+  = case tc of
+      PromotedDataCon {} -> char '\'' -- Always quote promoted DataCons in types
+      _                  -> empty
 
 instance NamedThing TyCon where
     getName = tyConName
@@ -1801,6 +2135,16 @@ instance Data.Data TyCon where
     gunfold _ _  = error "gunfold"
     dataTypeOf _ = mkNoRepType "TyCon"
 
+instance Binary Injectivity where
+    put_ bh NotInjective   = putByte bh 0
+    put_ bh (Injective xs) = putByte bh 1 >> put_ bh xs
+
+    get bh = do { h <- getByte bh
+                ; case h of
+                    0 -> return NotInjective
+                    _ -> do { xs <- get bh
+                            ; return (Injective xs) } }
+
 {-
 ************************************************************************
 *                                                                      *
@@ -1825,9 +2169,10 @@ the key examples:
   Id (Id Int)    Int
   Fix Id         NO NO NO
 
-Notice that we can expand T, even though it's recursive.
-And we can expand Id (Id Int), even though the Id shows up
-twice at the outer level.
+Notice that
+ * We can expand T, even though it's recursive.
+ * We can expand Id (Id Int), even though the Id shows up
+   twice at the outer level, because Id is non-recursive
 
 So, when expanding, we keep track of when we've seen a recursive
 newtype at outermost level; and bale out if we see it again.
@@ -1835,20 +2180,37 @@ newtype at outermost level; and bale out if we see it again.
 We sometimes want to do the same for product types, so that the
 strictness analyser doesn't unbox infinitely deeply.
 
-The function that manages this is checkRecTc.
+More precisely, we keep a *count* of how many times we've seen it.
+This is to account for
+   data instance T (a,b) = MkT (T a) (T b)
+Then (Trac #10482) if we have a type like
+        T (Int,(Int,(Int,(Int,Int))))
+we can still unbox deeply enough during strictness analysis.
+We have to treat T as potentially recursive, but it's still
+good to be able to unwrap multiple layers.
+
+The function that manages all this is checkRecTc.
 -}
 
-newtype RecTcChecker = RC NameSet
+data RecTcChecker = RC !Int (NameEnv Int)
+  -- The upper bound, and the number of times
+  -- we have encountered each TyCon
 
 initRecTc :: RecTcChecker
-initRecTc = RC emptyNameSet
+-- Intialise with a fixed max bound of 100
+-- We should probably have a flag for this
+initRecTc = RC 100 emptyNameEnv
 
 checkRecTc :: RecTcChecker -> TyCon -> Maybe RecTcChecker
 -- Nothing      => Recursion detected
 -- Just rec_tcs => Keep going
-checkRecTc (RC rec_nts) tc
-  | not (isRecursiveTyCon tc)     = Just (RC rec_nts)
-  | tc_name `elemNameSet` rec_nts = Nothing
-  | otherwise                     = Just (RC (extendNameSet rec_nts tc_name))
+checkRecTc rc@(RC bound rec_nts) tc
+  | not (isRecursiveTyCon tc)
+  = Just rc  -- Tuples are a common example here
+  | otherwise
+  = case lookupNameEnv rec_nts tc_name of
+      Just n | n >= bound -> Nothing
+             | otherwise  -> Just (RC bound (extendNameEnv rec_nts tc_name (n+1)))
+      Nothing             -> Just (RC bound (extendNameEnv rec_nts tc_name 1))
   where
     tc_name = tyConName tc