How to understand these exposure algorithm rules for System F sub?

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 ⇑ T

The 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: SPos"

where

sone= λ A B. 
                    λ n : C. m n.

          and 

          SPos= All A  B) -> (C-> A).

After applying "TA_TABS" and "TA_ABS" rules

{A B, n : C } |- m n :B
-----------------------------------------------------------TA-APP
 {...} |- :- m:T1   ,  {...}|-T1 ⇑ (T11->B)  ,  {...}|-n:T2  , {...}|-T2B)
 ------------------------------------------ 

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!

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 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.

StackExchange Computer Science Q#64253, answer score: 4