A TcTyCon is one of the variants of TyCon. First, here are its invariants:
* TcTyCon: a TyCon built with the TcTyCon constructor
A TcTyCon contains TcTyVars in its binders and kind
* TcTyConBinder: a TyConBinder with a TcTyVar inside (not a TyVar)
* MonoTcTyCon: a form of TcTyCon
- Flag tcTyConIsPoly = False
- tyConBinders are TcTyConBinders: they contain TcTyVars, which are
unification variables (TyVarTv), and whose kinds may contain
unification variables.
- tyConKind: the Monomorphic Recursion Principle:
a MonoTcTyCon has a /monomorphic kind/.
See Note [No polymorphic recursion in type decls].
But the tyConKind may contain free unification variables.
- tyConScopedTyVars is important; maps a Name to a TyVarTv unification variable
The order matters: Specified then Required variables.
E.g. in
data T a (b :: k) = ...
the order will be [k, a, b].
We do not allow @k-binders in inference mode, so we do not need to worry about
data T a @k (b :: k) = ...
where we would have to put `k` (Specified) after `a` (Required)
NB: There are no Inferred binders in tyConScopedTyVars; 'a' may
also be poly-kinded, but that kind variable will be added by
generaliseTcTyCon, in the passage to a PolyTcTyCon.
- tyConBinders are irrelevant; we just use tcTyConScopedTyVars
Well not /quite/ irrelevant:
* its length gives the number of explicit binders, and so allows us to
distinguish between the implicit and explicit elements of
tyConScopedTyVars.
* at construction time (mkTcTyCon) for a MonoTcTyCon (the call to mkTcTyCon
in GHC.Tc.Gen.HsType.kcInferDeclHeader) the tyConBinders are used to
construct the tyConKind; all must have AnonTCB visiblity so we we get
a monokind.
* PolyTcTyCon: a form of TcTyCon
- Flag tcTyConIsPoly = True; this is used only to short-cut zonking
- tyConBinders are still TcTyConBinders, but they are /skolem/ TcTyVars,
with fixed kinds, and accurate skolem info: no unification variables here
tyConBinders includes the Inferred binders if any
tyConBinders uses the Names from the original, renamed program.
- tcTyConScopedTyVars is irrelevant: just use (binderVars tyConBinders)
All the types have been swizzled back to use the original Names
See Note [tyConBinders and lexical scoping] in GHC.Core.TyCon
The main purpose of these TcTyCons is during kind-checking of
type/class declarations (in GHC.Tc.TyCl). During kind checking we
come upon knowledge of the eventual tycon in bits and pieces, and we
use a TcTyCon to record what we know before we are ready to build the
final TyCon. Here is the plan:
* Step 1 (inferInitialKinds, called from kcTyClGroup
inference only, skipped for checking):
Make a MonoTcTyCon whose binders are TcTyVars,
that may contain free unification variables.
See Note [No polymorphic recursion in type decls]
* Step 2 (kcTyClDecl, called from kcTyClGroup)
Kind-check the declarations of the group; this step just does
unifications that affect the unification variables created in
Step 1
* Step 3 (generaliseTcTyCon, called from kcTyClGroup)
Generalise that MonoTcTyCon to make a PolyTcTyCon
Its binders are skolem TcTyVars, with accurate SkolemInfo
* Step 4 (tcTyClDecl, called from tcTyClDecls)
Typecheck the type and class decls to produce a final TyCon
Its binders are final TyVars, not TcTyVars
Note that a MonoTcTyCon can contain unification variables, but a
PolyTcTyCon does not: only skolem TcTyVars. See the invariants above.
More details about /kind inference/:
S1) In kcTyClGroup, we use inferInitialKinds to look over the
declaration of any TyCon that lacks a kind signature or
CUSK, to determine its "shape"; for example, the number of
parameters, and any kind signatures.
We record that shape record that shape in a MonoTcTyCon; it is
"mono" because it has not been been generalised, and its binders
and result kind may have free unification variables.
S2) Still in kcTyClGroup, we use kcLTyClDecl to kind-check the
body (class methods, data constructors, etc.) of each of
these MonoTcTyCons, which has the effect of filling in the
metavariables in the tycon's initial kind.
S3) Still in kcTyClGroup, we use generaliseTyClDecl to generalize
each MonoTcTyCon to get a PolyTcTyCon, with skolem TcTyVars in it,
and a final, fixed kind.
S4) Finally, back in tcTyClDecls, we extend the environment with
the PolyTcTyCons, and typecheck each declaration (regardless
of kind signatures etc) to get final TyCon.
More details about /kind checking/
S5) In kcTyClGroup, we use checkInitialKinds to get the
utterly-final Kind of all TyCons in the group that
(a) have a standalone kind signature or
(b) have a CUSK.
This produces a PolyTcTyCon, that is, a TcTyCon in which the binders
and result kind are full of TyVars (not TcTyVars). No unification
variables here; everything is in its final form.
Wrinkles:
(W1) When recovering from a type error in a type declaration,
we want to put the erroneous TyCon in the environment in a
way that won't lead to more errors. We use a PolyTcTyCon for this;
see makeRecoveryTyCon.
(W2) tyConScopedTyVars. A challenging piece in all of this is that we
end up taking three separate passes over every declaration:
- one in inferInitialKind (this pass look only at the head, not the body)
- one in kcTyClDecls (to kind-check the body)
- 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
GHC.Tc.Gen.HsType.splitTelescopeTvs!)
Instead of trying, we just store the list of type variables to
bring into scope, in the tyConScopedTyVars field of a MonoTcTyCon.
These tyvars are brought into scope by the calls to
tcExtendNameTyVarEnv (tcTyConScopedTyVars tycon)
in kcTyClDecl.
In a TcTyCon, why is tyConScopedTyVars :: [(Name,TcTyVar)] rather
than just [TcTyVar]? Consider these mutually-recursive decls
data T (a :: k1) b = MkT (S a b)
data S (c :: k2) d = MkS (T c d)
We start with k1 bound to kappa1, and k2 to kappa2; so initially
in the (Name,TcTyVar) pairs the Name is that of the TcTyVar. But
then kappa1 and kappa2 get unified; so after the zonking in
'generalise' in 'kcTyClGroup' the Name and TcTyVar may differ.
See also Note [Type checking recursive type and class declarations].