Is this behavior in a programming language inconsistent?
Yes, your type inference seems incomplete. This example can be dealt with fairly trivially, by computing the respective type equations, e.g. in the style Hindley/Milner does it.
Alpha-renaming the example makes it easier to follow:
((\x.x) (\y.y)) 10

For maximum clarity, let's start by assigning type variables to each sub expression:

x : A
(\x.x) : B
y : C
(\y.y) : D
(\x.x) (\y.y) : E
10 : F
((\x.x) (\y.y)) 10 : G

Now, the typing rules of the language impose certain equality constraints for each language construct:

From the typing rule for lambda, applied to (\x.x), it follows that B = A -&gt; A
Likewise, D = C -&gt; C
From the typing rule for application, applied to (\x.x) (\y.y), it follows that A = D and E = D
From the typing rule for integers it follows that F = Int
From the typing rule for application, applied to (...) 10, it follows that E = F -&gt; G

In summary, this yields the following equations:

B = A -&gt; A

D = C -&gt; C

A = D

E = D

F = Int

E = F -&gt; G
Now you just solve the equations using unification:

From (2) and (3) it follows that A = C -&gt; C

From (2) and (4) it follows that E = C -&gt; C

From (5) and (6) it follows that E = Int -&gt; G

From (8) and (9) it follows that C -&gt; C = Int -&gt; G, and thus, C = Int and C = G, and thus, G = Int

From (7) and (10) it follows that A = Int -&gt; Int


A and C are the types you are ultimately interested in, because they are the ones you have to assign to x and y, respectively. They yield the typed term
((\x:(Int-&gt;Int).x) (\y.Int.y)) 10

Its overall type is G = Int.