The book Types and Programming Languages said System F sub type checking introduce exposure typing rules alongside algorithmic typing and sub-typing rules.       exposure algorithm       X<:T           |- T  T'       --------------------------- (XA-PROMOTE)                |- X  T'        T is not a type variable       --------------------------- (XA-other)                |- T  TThe first one seems simple, but the second rule seems bit wrong to me.T is not a type variable, which T it is referring to?Does  |- T  T mean left and right hand side of  are same types?For example, with the type checking             |- sone: SPoswhere           sone=  A <: Top.                   B <: A.                    C <: A.                     m : A->B.                      n : C. m n.          and           SPos= All A <: Top. All B<: A. All C<: A. (A-> B) -> (C-> A).After applying TA_TABS and TA_ABS rules {A <: Top, B<: A, C<: A, m : A->B, n : C } |- m n :B-----------------------------------------------------------TA-APP {...} |- :- m:T1   ,  {...}|-T1  (T11->B)  ,  {...}|-n:T2  , {...}|-T2<:T11 {...}|-n:T2    we know  T2=C then  {...}|-C<:T11  we get T11=top then put it in place   {...} |- :- m:T1   , {...}|-T1  (top->B) ------------------------------------------ which rule applies now? I believe from{...}|-T1  (top->B)we should get T1=A->B , but how?both (XA-PROMOTE) and (XA-other) seems cannot be applied.please help!
How to understand these exposure algorithm rules for System F sub?
type theory;type checking
In a typing rule (and more generally any deduction rule), all metavariables are universally quantified. That is, the rule can be applied for any instantiation that is syntactically correct. For example, (XA-PROMOTE) means for any context $\Gamma$, for any type variable $X$, for any type $T$, for any type $T'$, if $\Gamma$ contains $X <: T$ and the typing judgement $\Gamma \vdash T \Uparrow T'$ is true, then the typing judgement $\Gamma \vdash X \Uparrow T'$ is true. The rule (XA-other) states for any type $T$, for any context $\Gamma$, if $T$ is not a type variable then the typing judgement $T \vdash T \Uparrow T$ is true.The question which $T$ is it referring to? is not meaningful: the rule does not refer to a particular $T$. On the contrary, the rule applies to any $T$; the conclusion applies to any $T$ that matches the premise.In $\Gamma \vdash T \Uparrow T$, the left- and right-hand sides of $\Uparrow$ are the same type. The rule states that the relation $\Uparrow$ in any given context $\Gamma$ is symmetric on the subset of the set of all types that consists of the types that are not type variables. Some examples of typing judgements that can be derived by this rule are:$$\vdash \mathsf{Top} \Uparrow \mathsf{Top} \\X <: \mathsf{Top}, Y <: X \vdash X \rightarrow \mathsf{Top} \Uparrow X \rightarrow \mathsf{Top} \\X <: \mathsf{Top}, Y <: X \vdash (\forall Z <: Y, X \rightarrow Z) \Uparrow (\forall Z <: Y, X \rightarrow Z) \\$$I don't remember Pierce's presentation and I don't have the book here, but I think the reason XA-other has the premise that $T$ must not be a type variable is to make these rules syntax-directed: there's another rule that allows deriving judgement $\Gamma \vdash T \uparrow T$ when $T$ is a type variable. This is a presentation choice.  A metavariable is a variable that is used to describe the system, for example $X$, $T$, $T'$ and $\Gamma$ in the rule (XA-PROMOTE). We use the term metavariable to distinguish this concept from a variable, which refers whatever the language calls a variable.  