Commit 067335a6 authored by Simon Peyton Jones's avatar Simon Peyton Jones

A raft of comments about TyBinders

I had a conversation with Richard about TyBinders
and VisibilityFlags.  This patch adds a lot of comments
to explain what is going on.  I feel much more secure now.

Richard please check.
parent 12372baa
......@@ -290,6 +290,12 @@ data DataCon
-- dcOrigArgTys = [x,y]
-- dcRepTyCon = T
-- In general, the dcUnivTyVars are NOT NECESSARILY THE SAME AS THE TYVARS
-- FOR THE PARENT TyCon. With GADTs the data con might not even have
-- the same number of type variables!
-- [This is a change (Oct05): previously, vanilla datacons guaranteed to
-- have the same type variables as their parent TyCon, but that seems ugly.]
dcVanilla :: Bool, -- True <=> This is a vanilla Haskell 98 data constructor
-- Its type is of form
-- forall a1..an . t1 -> ... tm -> T a1..an
......@@ -300,25 +306,18 @@ data DataCon
-- syntax, provided its type looks like the above.
-- The declaration format is held in the TyCon (algTcGadtSyntax)
dcUnivTyVars :: [TyVar], -- Universally-quantified type vars [a,b,c]
-- INVARIANT: length matches arity of the dcRepTyCon
--- result type of (rep) data con is exactly (T a b c)
dcUnivTyBinders :: [TyBinder], -- Binders for universal tyvars. These will all
-- be Named, and all be Invisible or Specified.
-- Storing these separately from dcUnivTyVars
-- is solely because we usually don't need the
-- binders, and the extraction of the tyvars is
-- unnecessary work. See also
-- Note [TyBinders in DataCons]
dcExTyVars :: [TyVar], -- Existentially-quantified type vars
-- In general, the dcUnivTyVars are NOT NECESSARILY THE SAME AS THE TYVARS
-- FOR THE PARENT TyCon. With GADTs the data con might not even have
-- the same number of type variables.
-- [This is a change (Oct05): previously, vanilla datacons guaranteed to
-- have the same type variables as their parent TyCon, but that seems ugly.]
dcExTyBinders :: [TyBinder], -- see dcUnivTyBinders
-- Universally-quantified type vars [a,b,c]
dcUnivTyVars :: [TyVar], -- Two linked fields
dcUnivTyBinders :: [TyBinder], -- see Note [TyBinders in DataCons]
-- INVARIANT: length matches arity of the dcRepTyCon
--
-- INFARIANT: result type of (rep) data con is exactly (T a b c)
-- Existentially-quantified type vars [x,y]
dcExTyVars :: [TyVar], -- Two linked fields
dcExTyBinders :: [TyBinder], -- see Note [TyBinders in DataCons]
-- INVARIANT: the UnivTyVars and ExTyVars all have distinct OccNames
-- Reason: less confusing, and easier to generate IfaceSyn
......@@ -420,6 +419,41 @@ data DataCon
}
deriving Data.Typeable.Typeable
{- Note [TyBinders in DataCons]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
DataCons and PatSyns store their universal and existential type
variables in a pair of fields, e.g.
dcUnivTyVars :: [TyVar],
dcUnivTyBinders :: [TyBinder],
and similarly dcExTyVars/dcExTyVarBinders
Of these, the former is always redundant:
dcUnivTyVars = [ tv | Named tv _ <- dcUnivTyBinders ]
Specifically:
* The two fields correspond 1-1
* Each TyBinder a Named (no Anons)
* The TyVar in each TyBinder is the same as the TyVar in
the corresponding tyvar in the TyVars list.
* Each Visibilty flag (va, vb, etc) is Invisible or Specified.
None are Visible. (See Note [No Visible TyBinder in terms];
a DataCon is a term-level function.)
Why store these fields redundantly? Purely convenience. In most
places in GHC, it's just the TyVars that are needed, so that's what's
returned from, say, dataConFullSig.
Why do we need the TyBinders? So that we can construct the right
type for the DataCon with its foralls attributed the correce visiblity.
That in turn governs whether you can use visible type application
at a call of the data constructor.
-}
data DataConRep
= NoDataConRep -- No wrapper
......@@ -718,49 +752,11 @@ isMarkedStrict :: StrictnessMark -> Bool
isMarkedStrict NotMarkedStrict = False
isMarkedStrict _ = True -- All others are strict
{-
************************************************************************
{- *********************************************************************
* *
\subsection{Construction}
* *
************************************************************************
Note [TyBinders in DataCons]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
A DataCon needs to keep track of the visibility of its universals and
existentials, so that visible type application can work properly. This
is done by storing the universal and existential TyBinders, along with
the TyVars. These TyBinders should all be Named and should all be
Invisible or Specified; we don't have Visible or Anon type arguments.
During construction of a DataCon, we often have the TyBinders of the
parent TyCon. But those TyBinders are *different* than those of the
DataCon. Here is an example:
data Proxy a = P
The TyCon has these TyBinders:
[ Named (k :: *) Invisible, Anon k ]
Note that Proxy's kind is forall k. k -> *. But the DataCon P should
have (universal) TyBinders
[ Named (k :: *) Invisible, Named (a :: k) Specified ]
So we want to take the TyCon's TyBinders and the TyCon's TyVars and
merge them, pulling variable names from the TyVars but visibilities
from the TyBinders, perserving Invisible but changing Visible to
Specified. (The `a` in Proxy is indeed Visible, but the `a` in P should
be Specified.) This merging operation is done in buildDataCon. In contrast,
the TyBinders passed to mkDataCon are the real TyBinders stored in the
DataCon. Note that passing the TyVars into mkDataCon is redundant, but
convenient for both caller and the function's implementation.
In most places in GHC, it's just the TyVars that are needed,
so that's what's returned from, say, dataConFullSig.
-}
********************************************************************* -}
-- | Build a new data constructor
mkDataCon :: Name
......
......@@ -64,16 +64,21 @@ data PatSyn
-- record pat syn or same length as
-- psArgs
psUnivTyVars :: [TyVar], -- Universially-quantified type variables
psUnivTyBinders :: [TyBinder], -- same, with visibility info
psReqTheta :: ThetaType, -- Required dictionaries
-- these constraints are very much like
-- stupid thetas (which is a useful
-- guideline when implementing)
-- but are actually needed.
psExTyVars :: [TyVar], -- Existentially-quantified type vars
psExTyBinders :: [TyBinder], -- same, with visibility info
psProvTheta :: ThetaType, -- Provided dictionaries
-- Universially-quantified type variables
psUnivTyVars :: [TyVar], -- Two linked fields; see DataCon
psUnivTyBinders :: [TyBinder], -- Note [TyBinders in DataCons]
-- Required dictionaries (may mention psUnivTyVars)
psReqTheta :: ThetaType,
-- Existentially-quantified type vars
psExTyVars :: [TyVar], -- Two linked fields; see DataCon
psExTyBinders :: [TyBinder], -- Note [TyBinders in DataCons]
-- Provided dictionaries (may mention psUnivTyVars or psExTyVars)
psProvTheta :: ThetaType,
-- Result type
psOrigResTy :: Type, -- Mentions only psUnivTyVars
-- See Note [Matchers and builders for pattern synonyms]
......
......@@ -29,6 +29,7 @@ import MkId
import Class
import TyCon
import Type
import TyCoRep( TyBinder(..) )
import Id
import TcType
......@@ -136,14 +137,7 @@ buildDataCon fam_envs src_name declared_infix prom_info src_bangs impl_bangs fie
; traceIf (text "buildDataCon 1" <+> ppr src_name)
; us <- newUniqueSupply
; dflags <- getDynFlags
; let -- See Note [TyBinders in DataCons] in DataCon
dc_bndrs = zipWith mk_binder univ_tvs univ_bndrs
mk_binder tv bndr = mkNamedBinder vis tv
where
vis = case binderVisibility bndr of
Invisible -> Invisible
_ -> Specified
; let dc_bndrs = mkDataConUnivTyBinders univ_bndrs univ_tvs
stupid_ctxt = mkDataConStupidTheta rep_tycon arg_tys univ_tvs
data_con = mkDataCon src_name declared_infix prom_info
src_bangs field_lbls
......@@ -177,6 +171,69 @@ mkDataConStupidTheta tycon arg_tys univ_tvs
tyCoVarsOfType pred `intersectVarSet` arg_tyvars
mkDataConUnivTyBinders :: [TyBinder] -> [TyVar] -- From the TyCon
-> [TyBinder] -- For the DataCon
-- See Note [Building the TyBinders for a DataCon]
mkDataConUnivTyBinders bndrs tvs
= zipWith mk_binder bndrs tvs
where
mk_binder bndr tv = mkNamedBinder vis tv
where
vis = case bndr of
Anon _ -> Specified
Named _ Visible -> Specified
Named _ vis -> vis
{- Note [Building the TyBinders for a DataCon]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
A DataCon needs to keep track of the visibility of its universals and
existentials, so that visible type application can work properly. This
is done by storing the universal and existential TyBinders, along with
the TyVars. See Note [TyBinders in DataCons] in DataCon.
During construction of a DataCon, we often start from the TyBinders of
the parent TyCon. For example
data Maybe a = Nothing | Just a
The DataCons start from the TyBinders of the parent TyCon.
But the ultimate TyBinders for the DataCon are *different* than those
of the DataCon. Here is an example:
data App a b = MkApp (a b) -- App :: forall {k}. (k->*) -> k -> *
The TyCon has
tyConTyVars = [ k:*, a:k->*, b:k]
tyConTyBinders = [ Named (k :: *) Invisible, Anon (k->*), Anon k ]
The TyBinders for App line up with App's kind, given above.
But the DataCon MkApp has the type
MkApp :: forall {k} (a:k->*) (b:k). a b -> App k a b
That is, its TyBinders should be
dataConUnivTyVars = [ Named (k:*) Invisible
, Named (a:k->*) Specified
, Named (b:k) Specified ]
So we want to take the TyCon's TyBinders and the TyCon's TyVars and
merge them, pulling
- variable names from the TyVars
- visibilities from the TyBinders
- but changing Anon/Visible to Specified
The last part about Visible->Specified comes from this:
data T k (a:k) b = MkT (a b)
Here k is Visible in T's kind, but we don't have Visible binders in
the TyBinders for a term (see Note [No Visible TyBinder in terms]
in TyCoRep), so we change it to Specified when making MkT's TyBinders
This merging operation is done by mkDataConUnivTyBinders. In contrast,
the TyBinders passed to mkDataCon are the final TyBinders stored in the
DataCon (mkDataCon does no further work).
-}
------------------------------------------------------
buildPatSyn :: Name -> Bool
-> (Id,Bool) -> Maybe (Id, Bool)
......
......@@ -902,7 +902,7 @@ tcDataDefn rec_info -- Knot-tied; don't look at this eagerly
, dd_cons = cons })
= do { (extra_tvs, extra_bndrs, real_res_kind) <- tcDataKindSig res_kind
; let final_bndrs = tycon_binders `chkAppend` extra_bndrs
final_tvs = tvs `chkAppend` extra_tvs
final_tvs = tvs `chkAppend` extra_tvs
roles = rti_roles rec_info tc_name
; stupid_tc_theta <- solveEqualities $ tcHsContext ctxt
......
......@@ -168,16 +168,19 @@ import Data.IORef ( IORef ) -- for CoercionHole
import GHC.Stack (CallStack)
#endif
{-
%************************************************************************
%* *
\subsection{The data type}
%* *
%************************************************************************
-}
{- **********************************************************************
* *
Type
* *
********************************************************************** -}
-- | The key representation of types within the compiler
type KindOrType = Type -- See Note [Arguments to type constructors]
-- | The key type representing kinds in the compiler.
type Kind = Type
-- If you edit this type, you may need to update the GHC formalism
-- See Note [GHC Formalism] in coreSyn/CoreLint.hs
data Type
......@@ -241,64 +244,8 @@ data TyLit
| StrTyLit FastString
deriving (Eq, Ord, Data.Data, Data.Typeable)
-- | A 'TyBinder' represents an argument to a function. TyBinders can be dependent
-- ('Named') or nondependent ('Anon'). They may also be visible or not.
-- See also Note [TyBinder]
data TyBinder
= Named TyVar VisibilityFlag -- Always a TyVar (not CoVar or Id)
| Anon Type -- Visibility is determined by the type (Constraint vs. *)
deriving (Data.Typeable, Data.Data)
-- | Is something required to appear in source Haskell ('Visible'),
-- permitted by request ('Specified') (visible type application), or
-- prohibited entirely from appearing in source Haskell ('Invisible')?
-- Examples in Note [VisibilityFlag]
data VisibilityFlag = Visible | Specified | Invisible
deriving (Eq, Data.Typeable, Data.Data)
-- | Do these denote the same level of visibility? Except that
-- 'Specified' and 'Invisible' are considered the same. Used
-- for printing.
sameVis :: VisibilityFlag -> VisibilityFlag -> Bool
sameVis Visible Visible = True
sameVis Visible _ = False
sameVis _ Visible = False
sameVis _ _ = True
instance Binary VisibilityFlag where
put_ bh Visible = putByte bh 0
put_ bh Specified = putByte bh 1
put_ bh Invisible = putByte bh 2
get bh = do
h <- getByte bh
case h of
0 -> return Visible
1 -> return Specified
_ -> return Invisible
type KindOrType = Type -- See Note [Arguments to type constructors]
-- | The key type representing kinds in the compiler.
type Kind = Type
{-
Note [TyBinder]
~~~~~~~~~~~~~~~
This represents the type of binders -- that is, the type of an argument
to a Pi-type. GHC Core currently supports two different Pi-types:
a non-dependent function, written with ->, and a dependent compile-time-only
polytype, written with forall. Both Pi-types classify terms/types that
take an argument. In other words, if `x` is either a function or a polytype,
`x arg` makes sense (for an appropriate `arg`). It is thus often convenient
to group Pi-types together. This is ForAllTy.
The two constructors for TyBinder sort out the two different possibilities.
`Named` builds a polytype, while `Anon` builds an ordinary function.
(ForAllTy (Anon arg) res used to be called FunTy arg res.)
Note [The kind invariant]
~~~~~~~~~~~~~~~~~~~~~~~~~
{- Note [The kind invariant]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The kinds
# UnliftedTypeKind
OpenKind super-kind of *, #
......@@ -408,54 +355,208 @@ Another helpful principle with eqType is this:
This principle also tells us that eqType must relate only types with the
same kinds.
-}
Note [VisibilityFlag]
~~~~~~~~~~~~~~~~~~~~~
All named binders are equipped with a visibility flag, which says
whether or not arguments for this binder should be visible (explicit)
in source Haskell. Historically, all named binders (that is, polytype
binders) have been Invisible. But now it's more complicated.
{- **********************************************************************
* *
TyBinder and VisibilityFlag
* *
********************************************************************** -}
Invisible:
Argument does not ever appear in source Haskell. With visible type
application, only GHC-generated polytypes have Invisible binders.
This exactly corresponds to "generalized" variables from the
Visible Type Applications paper (ESOP'16).
-- | A 'TyBinder' represents an argument to a function. TyBinders can be dependent
-- ('Named') or nondependent ('Anon'). They may also be visible or not.
-- See Note [TyBinders]
data TyBinder
= Named TyVar VisibilityFlag -- Always a TyVar (not CoVar or Id)
| Anon Type -- Visibility is determined by the type (Constraint vs. *)
deriving (Data.Typeable, Data.Data)
Example: f x = x
`f` will be inferred to have type `forall a. a -> a`, where `a` is
Invisible. Note that there is no type annotation for `f`.
-- | Is something required to appear in source Haskell ('Visible'),
-- permitted by request ('Specified') (visible type application), or
-- prohibited entirely from appearing in source Haskell ('Invisible')?
-- See Note [TyBinders and VisibilityFlags]
data VisibilityFlag = Visible | Specified | Invisible
deriving (Eq, Data.Typeable, Data.Data)
Printing: With -fprint-explicit-foralls, Invisible binders are written
in braces. Otherwise, they are printed like Specified binders.
-- | Do these denote the same level of visibility? Except that
-- 'Specified' and 'Invisible' are considered the same. Used
-- for printing.
sameVis :: VisibilityFlag -> VisibilityFlag -> Bool
sameVis Visible Visible = True
sameVis Visible _ = False
sameVis _ Visible = False
sameVis _ _ = True
Specified:
The argument for this binder may appear in source Haskell only with
visible type application. Otherwise, it is omitted.
{- Note [TyBinders]
~~~~~~~~~~~~~~~~~~~
A ForAllTy contains a TyBinder.
Example: id :: forall a. a -> a
`a` is a Specified binder, because you can say `id @Int` in source Haskell.
A TyBinder represents the type of binders -- that is, the type of an
argument to a Pi-type. GHC Core currently supports two different
Pi-types:
Example: const :: a -> b -> a
Both `a` and `b` are Specified binders, even though they are not bound
by an explicit forall.
* A non-dependent function,
written with ->, e.g. ty1 -> ty2
represented as ForAllTy (Anon ty1) ty2
Printing: a list of Specified binders are put between `forall` and `.`:
const :: forall a b. a -> b -> a
* A dependent compile-time-only polytype,
written with forall, e.g. forall (a:*). ty
represented as ForAllTy (Named a v) ty
Visible:
The argument must be given. Visible binders come up only with TypeInType.
Both Pi-types classify terms/types that take an argument. In other
words, if `x` is either a function or a polytype, `x arg` makes sense
(for an appropriate `arg`). It is thus often convenient to group
Pi-types together. This is ForAllTy.
Example: data Proxy k (a :: k) = P
The kind of Proxy is forall k -> k -> *, where k is a Visible binder.
The two constructors for TyBinder sort out the two different possibilities.
`Named` builds a polytype, while `Anon` builds an ordinary function.
(ForAllTy (Anon arg) res used to be called FunTy arg res.)
Printing: As in the example above, Visible binders are put between `forall`
and `->`. This syntax is not parsed (yet), however.
Note [TyBinders and VisibilityFlags]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
A ForAllTy contains a TyBinder. Each Named TyBinders are equipped
with a VisibilityFlag, which says whether or not arguments for this
binder should be visible (explicit) in source Haskell.
-----------------------------------------------------------------------
Occurrences look like this
TyBinder GHC displays type as in Haskell souce code
-----------------------------------------------------------------------
In the type of a term
Anon: f :: type -> type Arg required: f x
Named Invisible: f :: forall {a}. type Arg not allowed: f
Named Specified: f :: forall a. type Arg optional: f or f @Int
Named Visible: Illegal: See Note [No Visible TyBinder in terms]
In the kind of a type
Anon: T :: kind -> kind Required: T *
Named Invisible: T :: forall {k}. kind Arg not allowed: T
Named Specified: T :: forall k. kind Arg not allowed[1]: T
Named Visible: T :: forall k -> kind Required: T *
------------------------------------------------------------------------
[1] In types, in the Specified case, it would make sense to allow
optional kind applications, thus (T @*), but we have not
yet implemented that
---- Examples of where the different visiblities come from -----
In term declarations:
* Invisible. Function defn, with no signature: f1 x = x
We infer f1 :: forall {a}. a -> a, with 'a' Invisible
It's Invisible because it doesn't appear in any
user-written signature for f1
* Specified. Function defn, with signature (implicit forall):
f2 :: a -> a; f2 x = x
So f2 gets the type f2 :: forall a. a->a, with 'a' Specified
even though 'a' is not bound in the source code by an explicit forall
* Specified. Function defn, with signature (explicit forall):
f3 :: forall a. a -> a; f3 x = x
So f3 gets the type f3 :: forall a. a->a, with 'a' Specified
* Invisible/Specified. Function signature with inferred kind polymorphism.
f4 :: a b -> Int
So 'f4' get the type f4 :: forall {k} (a:k->*) (b:k). a b -> Int
Here 'k' is Invisible (it's not mentioned in the type),
but 'a' and 'b' are Specified.
* Specified. Function signature with explicit kind polymorphism
f5 :: a (b :: k) -> Int
This time 'k' is Specified, because it is mentioned explicitly,
so we get f5 :: forall (k:*) (a:k->*) (b:k). a b -> Int
* Similarly pattern synonyms:
Invisible - from inferred types (e.g. no pattern type signature)
- or from inferred kind polymorphism
In type declarations:
* Invisible (k)
data T1 a b = MkT1 (a b)
Here T1's kind is T1 :: forall {k:*}. (k->*) -> k -> *
The kind variable 'k' is Invisible, since it is not mentioned
Note that 'a' and 'b' correspond to /Anon/ TyBinders in T1's kind,
and Anon binders don't have a visibility flag. (Or you could think
of Anon having an implicit Visible flag.)
* Specified (k)
data T2 (a::k->*) b = MkT (a b)
Here T's kind is T :: forall (k:*). (k->*) -> k -> *
The kind vairable 'k' is Specified, since it is mentioned in
the signature.
* Visible (k)
data T k (a::k->*) b = MkT (a b)
Here T's kind is T :: forall k:* -> (k->*) -> k -> *
The kind Visible, since it bound in a positional way in T's declaration
Every use of T must be explicitly applied to a kind
* Invisible (k1), Specified (k)
data T a b (c :: k) = MkT (a b) (Proxy c)
Here T's kind is T :: forall {k1:*} (k:*). (k1->*) -> k1 -> k -> *
So 'k' is Specified, becuase it appears explicitly,
but 'k1' is Invisible, becuase it does not
---- Printing -----
We print forall types with enough syntax to tell you their visiblity
flag. But this is not source Haskell, and these types may not all
be parsable.
Specified: a list of Specified binders is written between `forall` and `.`:
const :: forall a b. a -> b -> a
Invisible: with -fprint-explicit-foralls, Invisible binders are written
in braces:
f :: forall {k} (a:k). S k a -> Int
Otherwise, they are printed like Specified binders.
Visible: binders are put between `forall` and `->`:
T :: forall k -> *
---- Other points -----
* In classic Haskell, all named binders (that is, the type variables in
a polymorphic function type f :: forall a. a -> a) have been Invisible.
* Invisible variables correspond to "generalized" variables from the
Visible Type Applications paper (ESOP'16).
Note [No Visible TyBinder in terms]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We don't allow Visible foralls for term variables, including pattern
synonyms and data constructors. Why? Because then an application
would need a /compulsory/ type argument (possibly without an "@"?),
thus (f Int); and we don't have concrete syntax for that.
-------------------------------------
Note [PredTy]
We could change this decision, but Visible, Named TyBinders are rare
anyway. (Most are Anons.)
-}
instance Binary VisibilityFlag where
put_ bh Visible = putByte bh 0
put_ bh Specified = putByte bh 1
put_ bh Invisible = putByte bh 2
get bh = do
h <- getByte bh
case h of
0 -> return Visible
1 -> return Specified
_ -> return Invisible
{- **********************************************************************
* *
PredType
* *
********************************************************************** -}
-- | A type of the form @p@ of kind @Constraint@ represents a value whose type is
-- the Haskell predicate @p@, where a predicate is what occurs before
-- the @=>@ in a Haskell type.
......@@ -494,6 +595,7 @@ The predicate really does turn into a real extra argument to the
function. If the argument has type (p :: Constraint) then the predicate p is
represented by evidence of type p.
%************************************************************************
%* *
Simple constructors
......
......@@ -307,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
......@@ -342,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
......@@ -397,19 +395,11 @@ data TyCon
tyConName :: Name, -- ^ Name of the constructor
-- See Note [The binders/kind/arity fields of a TyCon]
tyConBinders :: [TyBinder], -- ^ The TyBinders for this TyCon's kind.
-- length tyConBinders == tyConArity.
-- This is a cached value and is redundant with
-- the tyConKind.
tyConResKind :: Kind, -- ^ Cached result kind
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)
tyConResKind :: Kind, -- ^ Result kind
tyConKind :: Kind, -- ^ Kind of this TyCon
tyConArity :: Arity, -- ^ Arity