Can in polymorphic lambda calculus two terms have identical normal forms if we assume that set of their possible types does not intersect?

Question

Let us assume, that we have context $\Gamma$ and two terms $M_1$ and $M_2$ in polymorphic lambda calculus. Let us also assume, that intersection of their possible types in context $\Gamma$ is empty(we assume that both of these terms can be typed). Is it possible for their normal forms to be identical?

Answer 1

Just a sketch. Whether it works probably depends on the formalism you use. If $M$ normalizes to $N$ and $\tau$ is a possible type for $N$, is then $\tau$ also a possible type for $M$?

If yes, then the answer to your question is no. For assume $M_1, M_2$ both normalize to $N$ and $\tau$ is a possible type of $N$, then $\tau$ is a possible type for both $M_1$ and $M_2$ which you assumed to be impossible.