System f-sub, how to do type checking?
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