System f-sub, how to do type checking? I was reading that system f-sub (polymorphic lambda calculus with sub-typing) and I was quite confused with its one checking rule called "T-TAPP".

This rule as following (ctx denotes the typing context)

   ctx |- t1 : ∀X&lt;:T11. T12    ,    ctx |- T2&lt;:T11
   -----------------------------------------------
            ctx |- t1 [T2] : [X--&gt;T2]T12


I could not understand how '[x-->T2]T12' will be used (I know it is substitution). This rule appears on page 10 in the following source.
I am looking for two type checking examples, in which above inference rule will be applied and at least one example is a case of type checking failure.

Could anyone provide me with concrete examples?
Description of system F-sub
I know this is old but the previous answer has a huge misconception.

The following function is in System F.

$f = \lambda X. X \rightarrow X \rightarrow X$

All we know of this function is it selects one of its arguments and can be instantieded with any type; $\ f$ [Bool] : Bool $\rightarrow$ Bool $\rightarrow$ Bool.

In System $F_{&lt;:}$ is possible to have the following function.

$f' = \lambda X&lt;:$Number$.\ X \rightarrow X \rightarrow X$

This function can be the addition, multiplication, division, subtraction, etc, and can be instantiated with subtypes of Number.

$f'$ [Int], $\ f'$ [Double], $\ f'$ [Real] are valid instantiations, but $\ f'$ [Bool] not, because Bool is not a subtype of Nat.

Dependent types are a different thing. It has nothing to do here and is out of the scope of the question, but it is a very interesting topic. See Lambda Cube