Does there exist a type system for a non-let-polymorphic lambda calculus?

I'm wondering if there is a way to extend Hinley-Milner's type system to allow polymorphic types without the need of a let construct, by adding an intersection type (as Dan pointed out) that represents the possible types of a function type.

Say I have this expression:

$\lambda x.\lambda y.(x\ (x\ y))$

While running the type inference algorithm, I'd normally, after looking at the expression $(x\ y)$, assign to $x$ some type $Y \rightarrow A$, where $Y$ is the type of $y$ and $A$ is whatever $x$ returns. Then, since $x$ also takes $(x\ y)$ which has the type $A$, I replace $Y$ with $A$, such that the type of $x$ becomes $A \rightarrow A$ and give to the whole thing the type $(A \rightarrow A) \rightarrow (A \rightarrow A)$.

But what if I, instead of replacing $Y$ with $A$ when I see $(x\ (x\ y))$, add a new type to $x$, say, $A \rightarrow B$, such that the final type is $((Y \rightarrow A) \wedge (A \rightarrow B)) \rightarrow (Y \rightarrow B)$, which is also a tautology and seems like a better representation of what the function does.

Now say I give to this abstraction the term $\lambda n.n$ like this:

$(\lambda x.\lambda y.(x\ (x\ y))\ \lambda n.n)$

Since $\lambda n.n$ has the type $N \rightarrow N$, I'd need to unify $N \rightarrow N$ with $((Y \rightarrow A) \wedge (A \rightarrow B))$. So I instantiate two copies of $N \rightarrow N$, say $N_1 \rightarrow N_1$ and $N_2 \rightarrow N_2$, and unify $N_1 \rightarrow N_1$ with $Y \rightarrow A$ and $N_2 \rightarrow N_2$ with $A \rightarrow B$. Because $A$ would be equal to $N_1$ on one side and equal to $N_2$ on the other side, $N_1$, $Y$, $A$ and $B$ are all equal to $N_2$, so the type $Y \rightarrow B$ becomes $N_2 \rightarrow N_2$, which is consistent with the expression you'd get after evaluating the lambda term.

With this type system I should be able to type things like this:

$(\lambda i.\lambda x.\lambda y.((i\ x)\ (i\ y))\ \lambda n.n)$

But these examples are simple, and it becomes a pain to type so

I am not sure what you mean by type system being decidable. I guess you mean type checking and type inference. (strictly speaking type inference is not a decision problem, although it can be casted as one and people usually think of it that way).

In addition to intersection types, I would also suggest looking at System F where universal quantification does not appear only at the let construct. For system F, type inference is undecidable: paper

StackExchange Computer Science Q#23249, answer score: 3