Note [tyConBinders and lexical scoping]
In a TyCon, and a PolyTcTyCon, we obey the following rule:
The Name of the TyConBinder is precisely
the lexically scoped Name from the original declaration
(precisely = both OccName and Unique)
For example,
data T a (b :: wombat) = MkT
We will get tyConBinders of [k, wombat, a::k, b::wombat]
The 'k' is made up; the user didn't specify it. But for the kind of 'b'
we must use 'wombat'.
Why do we have this invariant?
* Similarly, when typechecking default definitions for class methods, in
GHC.Tc.TyCl.Class.tcClassDecl2, we only have the (final) Class available;
but the variables bound in that class must be in scope. Example (#19738):
type P :: k -> Type
data P a = MkP
type T :: k -> Constraint
class T (a :: j) where
f :: P a
f = MkP @j @a -- 'j' must be in scope when we typecheck 'f'
* When typechecking `deriving` clauses for top-level data declarations, the
tcTyConScopedTyVars are brought into scope in through the `di_scoped_tvs`
field of GHC.Tc.Deriv.DerivInfo. Example (#16731):
class C x1 x2
type T :: a -> Type
data T (x :: z) deriving (C z)
When typechecking `C z`, we want `z` to map to `a`, which is exactly what the
tcTyConScopedTyVars for T give us. References 0
This Note does not link to any other.
Referenced by 2
- The binders/kind/arity fields of a TyCon GHC.Core.TyCon
- TcTyCon, MonoTcTyCon, and PolyTcTyCon GHC.Tc.TyCl