Note [tyConBinders and lexical scoping]

GHC/Core/TyCon.hs:681 compiler 2 tickets

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