A question about type rule

I realized that almost no one explained how to selected the type variable T1

Γ ⊢ e1 : T1 -> T  ,  Γ ⊢ e2 : T1
 -------------------------------- T-APP 
 Γ ⊢ e1 e2 : T

when doing type checking (from bottom to top).

So, the question is how T1 is introduced? Is there any condition about T1?

T1 is a schematic variable. Every consistent substitution of T1 with a type produces an instance of the rule. In a simple enough system, the inference rules can be used directly as the blueprint for a type-checking algorithm. In languages with richer type systems, type-checking algorithms become more complex or even undecidable (which is not a desirable features). Let me give an example where I type-check the program using a simple derivation.

Let's say I have the following program I wish to type-check:

(lambda x: nat. x = 0)(4)

First, we can deduce that 4 : nat by using the usual typing rules for natural numbers, which I will not reproduce here. Then we type-check the lambda abstraction with following derivation (I apologize for the sloppy latex):

$$ \underline{x : nat ⊢ x: nat \quad x: nat ⊢ 0 : nat} $$
$$ \underline{x : nat ⊢ x = 0 : bool}$$
$$ \underline{\lambda x: nat. \ x = 0 : nat \to bool} $$

Finally, using the application rules:

$$ \underline{\lambda x: nat. \ x = 0 : nat \to bool \quad 4 : nat} $$
$$ (\lambda x: nat. \ x = 0)(4) : bool $$

Note that type-checking is much simpler when we're working in a type system without subtyping, in that ever expression is monomorphic. The typing rules are syntax-directed. That is, the structure of the program dictates the type of every expression.

StackExchange Computer Science Q#64105, answer score: 4