Re-add FunTy (big patch)
[ghc.git] / compiler / types / TyCon.hs
index 356e2ea..c7c225d 100644 (file)
@@ -6,7 +6,7 @@
 The @TyCon@ datatype
 -}
 
-{-# LANGUAGE CPP, DeriveDataTypeable #-}
+{-# LANGUAGE CPP #-}
 
 module TyCon(
         -- * Main TyCon data types
@@ -15,6 +15,7 @@ module TyCon(
         AlgTyConRhs(..), visibleDataCons,
         AlgTyConFlav(..), isNoParent,
         FamTyConFlav(..), Role(..), Injectivity(..),
+        RuntimeRepInfo(..),
 
         -- ** Field labels
         tyConFieldLabels, tyConFieldLabelEnv,
@@ -51,7 +52,7 @@ module TyCon(
         isOpenTypeFamilyTyCon, isClosedSynFamilyTyConWithAxiom_maybe,
         familyTyConInjectivityInfo,
         isBuiltInSynFamTyCon_maybe,
-        isUnLiftedTyCon,
+        isUnliftedTyCon,
         isGadtSyntaxTyCon, isInjectiveTyCon, isGenerativeTyCon, isGenInjAlgRhs,
         isTyConAssoc, tyConAssoc_maybe,
         isRecursiveTyCon,
@@ -82,6 +83,9 @@ module TyCon(
         newTyConRhs, newTyConEtadArity, newTyConEtadRhs,
         unwrapNewTyCon_maybe, unwrapNewTyConEtad_maybe,
         algTcFields,
+        tyConRuntimeRepInfo,
+        tyConBinders, tyConResKind,
+        tcTyConScopedTyVars,
 
         -- ** Manipulating TyCons
         expandSynTyCon_maybe,
@@ -91,10 +95,12 @@ module TyCon(
 
         -- * Runtime type representation
         TyConRepName, tyConRepName_maybe,
+        mkPrelTyConRepName,
+        tyConRepModOcc,
 
         -- * Primitive representations of Types
         PrimRep(..), PrimElemRep(..),
-        tyConPrimRep, isVoidRep, isGcPtrRep,
+        isVoidRep, isGcPtrRep,
         primRepSizeW, primElemRepSizeB,
         primRepIsFloat,
 
@@ -105,7 +111,9 @@ module TyCon(
 
 #include "HsVersions.h"
 
-import {-# SOURCE #-} TyCoRep ( Kind, Type, PredType )
+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
@@ -124,9 +132,11 @@ 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)
 
 {-
 -----------------------------------------------
@@ -297,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
@@ -318,12 +327,13 @@ 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 levity vars]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-The contents of an unboxed tuple may be boxed or unboxed. Accordingly,
-the kind of the unboxed tuple constructor is sort-polymorphic. For example,
+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 (v :: Levity) (w :: Levity). TYPE v -> TYPE w -> #
+   (#,#) :: 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
@@ -331,7 +341,6 @@ 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
@@ -358,6 +367,15 @@ See also:
 ************************************************************************
 -}
 
+{- 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:
 --
@@ -386,12 +404,11 @@ 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
 
         tcRepName :: TyConRepName
     }
@@ -416,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'
@@ -436,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
@@ -479,19 +496,19 @@ 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
@@ -507,24 +524,18 @@ 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
@@ -554,23 +565,17 @@ 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 = *
@@ -581,22 +586,37 @@ data TyCon
 
   -- | 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
-        tcRepName   :: TyConRepName
+        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'
     }
 
   -- | These exist only during a recursive type/class type-checking knot.
   | TcTyCon {
-      tyConUnique :: Unique,
-      tyConName   :: Name,
-      tyConKind   :: Kind
+        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]
       }
-  deriving Typeable
 
 
 -- | Represents right-hand-sides of 'TyCon's for algebraic types
@@ -662,6 +682,19 @@ data AlgTyConRhs
                              -- again check Trac #1072.
     }
 
+-- | 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!
@@ -729,8 +762,8 @@ 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 ppr tys)
+    ppr (DataFamInstTyCon _ tc tys) = text "Family parent (family instance)"
+                                      <+> ppr tc <+> sep (map pprType tys)
 
 -- | Checks the invariants of a 'AlgTyConFlav' given the appropriate type class
 -- name, if any
@@ -782,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
@@ -890,6 +965,45 @@ 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.
+
 ************************************************************************
 *                                                                      *
                  TyConRepName
@@ -914,6 +1028,31 @@ 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
+
 
 {- *********************************************************************
 *                                                                      *
@@ -1065,20 +1204,20 @@ primRepIsFloat  _            = Just False
 
 -- | The labels for the fields of this particular 'TyCon'
 tyConFieldLabels :: TyCon -> [FieldLabel]
-tyConFieldLabels tc = fsEnvElts $ tyConFieldLabelEnv tc
+tyConFieldLabels tc = dFsEnvElts $ tyConFieldLabelEnv tc
 
 -- | The labels for the fields of this particular 'TyCon'
 tyConFieldLabelEnv :: TyCon -> FieldLabelEnv
 tyConFieldLabelEnv tc
   | isAlgTyCon tc = algTcFields tc
-  | otherwise     = emptyFsEnv
+  | otherwise     = emptyDFsEnv
 
 
 -- | Make a map from strings to FieldLabels from all the data
 -- constructors of this algebraic tycon
 fieldsOfAlgTcRhs :: AlgTyConRhs -> FieldLabelEnv
-fieldsOfAlgTcRhs rhs = mkFsEnv [ (flLabel fl, fl)
-                               | fl <- dataConsFields (visibleDataCons rhs) ]
+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
@@ -1101,14 +1240,16 @@ 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 'TyCoRep.funTyCon' if you want
 -- this functionality
-mkFunTyCon :: Name -> Kind -> Name -> TyCon
-mkFunTyCon name kind rep_nm
+mkFunTyCon :: Name -> [TyBinder] -> Name -> TyCon
+mkFunTyCon name binders rep_nm
   = FunTyCon {
-        tyConUnique = nameUnique name,
-        tyConName   = name,
-        tyConKind   = kind,
-        tyConArity  = 2,
-        tcRepName   = rep_nm
+        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
@@ -1116,7 +1257,8 @@ mkFunTyCon name kind rep_nm
 -- 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
@@ -1130,11 +1272,13 @@ mkAlgTyCon :: Name
            -> RecFlag           -- ^ Is the 'TyCon' recursive?
            -> Bool              -- ^ Was the 'TyCon' declared with GADT syntax?
            -> TyCon
-mkAlgTyCon name kind tyvars roles cType stupid rhs parent is_rec gadt_syn
+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,
@@ -1148,26 +1292,30 @@ mkAlgTyCon name kind tyvars roles cType stupid rhs parent is_rec gadt_syn
     }
 
 -- | Simpler specialization of 'mkAlgTyCon' for classes
-mkClassTyCon :: Name -> Kind -> [TyVar] -> [Role] -> AlgTyConRhs -> Class
+mkClassTyCon :: Name -> [TyBinder]
+             -> [TyVar] -> [Role] -> AlgTyConRhs -> Class
              -> RecFlag -> Name -> TyCon
-mkClassTyCon name kind tyvars roles rhs clas is_rec tc_rep_name
-  = mkAlgTyCon name kind tyvars roles Nothing [] rhs
+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
 
 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
              -> AlgTyConFlav
              -> TyCon
-mkTupleTyCon name kind arity tyvars con sort 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,
@@ -1175,7 +1323,7 @@ mkTupleTyCon name kind arity tyvars con sort parent
         algTcStupidTheta = [],
         algTcRhs         = TupleTyCon { data_con = con,
                                         tup_sort = sort },
-        algTcFields      = emptyFsEnv,
+        algTcFields      = emptyDFsEnv,
         algTcParent      = parent,
         algTcRec         = NonRecursive,
         algTcGadtSyntax  = False
@@ -1187,70 +1335,96 @@ mkTupleTyCon name kind arity tyvars con sort parent
 -- TcErrors sometimes calls typeKind.
 -- See also Note [Kind checking recursive type and class declarations]
 -- in TcTyClsDecls.
-mkTcTyCon :: Name -> Kind -> TyCon
-mkTcTyCon name kind
+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
-            , tyConKind    = kind }
+            , 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 Nothing
+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 -> [Role] -> Name -> TyCon
-mkKindTyCon name kind roles rep_nm
+mkKindTyCon :: Name -> [TyBinder]
+            -> Kind  -- ^ /result/ kind
+            -> [Role] -> Name -> TyCon
+mkKindTyCon name binders res_kind roles rep_nm
   = tc
   where
-    tc = mkPrimTyCon' name kind roles VoidRep False (Just rep_nm)
+    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 Nothing
-
-mkPrimTyCon' :: Name  -> Kind -> [Role] -> PrimRep
+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 kind roles rep is_unlifted rep_nm
+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] -> Maybe Name -> FamTyConFlav
-             -> Maybe Class -> Injectivity -> TyCon
-mkFamilyTyCon name kind tyvars resVar flav parent inj
+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
-      , famTcResVar = resVar
-      , famTcFlav   = flav
-      , famTcParent = parent
-      , famTcInj    = inj
+      { 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
       }
 
 
@@ -1258,16 +1432,20 @@ mkFamilyTyCon name kind tyvars resVar flav parent inj
 -- 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 -> TyConRepName -> Kind -> [Role] -> TyCon
-mkPromotedDataCon con name rep_name kind roles
+mkPromotedDataCon :: DataCon -> Name -> TyConRepName -> [TyBinder] -> Kind -> [Role]
+                  -> RuntimeRepInfo -> TyCon
+mkPromotedDataCon con name rep_name binders res_kind roles rep_info
   = PromotedDataCon {
-        tyConUnique = nameUnique name,
-        tyConName   = name,
-        tyConArity  = arity,
-        tcRoles     = roles,
-        tyConKind   = kind,
-        dataCon     = con,
-        tcRepName   = rep_name
+        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
@@ -1285,16 +1463,9 @@ isAbstractTyCon _ = False
 -- Used when recovering from errors
 makeTyConAbstract :: TyCon -> TyCon
 makeTyConAbstract tc
-  = PrimTyCon { tyConName        = name,
-                tyConUnique      = nameUnique name,
-                tyConKind        = tyConKind tc,
-                tyConArity       = tyConArity tc,
-                tcRoles          = tyConRoles tc,
-                primTyConRep     = PtrRep,
-                isUnLifted       = False,
-                primRepName      = Nothing }
-  where
-    name = tyConName 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
@@ -1303,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
@@ -1347,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
@@ -1367,7 +1538,7 @@ isInjectiveTyCon tc@(TcTyCon {})               _
 -- | '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 (FamilyTyCon { famTcFlav = DataFamilyTyCon _ }) Nominal = True
 isGenerativeTyCon (FamilyTyCon {}) _ = False
@@ -1479,6 +1650,7 @@ isTypeSynonymTyCon _                 = False
 mightBeUnsaturatedTyCon :: TyCon -> Bool
 mightBeUnsaturatedTyCon (SynonymTyCon {}) = 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?
@@ -1605,12 +1777,18 @@ 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 = isLiftedTypeKindTyConName (tyConName tc) ||
-                 tc `hasKey` constraintKindTyConKey ||
-                 tc `hasKey` tYPETyConKey ||
-                 tc `hasKey` levityTyConKey ||
-                 tc `hasKey` liftedDataConKey ||
-                 tc `hasKey` unliftedDataConKey
+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
@@ -1672,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
@@ -1818,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 ...@
@@ -1892,6 +2064,12 @@ 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.
+
 {-
 ************************************************************************
 *                                                                      *
@@ -1900,14 +2078,11 @@ tyConFamilyCoercion_maybe _ = Nothing
 ************************************************************************
 
 @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 }