Polymorphism restriction on lambda-bound variables in HM
Yes, you are restricting it too much. The second code is perfectly fine.

For the record, Haskell has no issue with your code:

&gt; let myid = (\x-&gt;x)(\x-&gt;x) in (myid 'a', myid True)
('a',True)


and Ocaml as well works fine, after eta-expansion:

let myid y = (fun x -&gt; x)(fun x -&gt; x) y in (myid 'a', myid true);;
- : char * bool = ('a', true)


Eta expansion is needed in Ocaml, I think, because of the value restriction, where a binding is not generalized unless it is a function (let f x = ... instead of let f = ...). This restriction was needed to avoid some soundness issues with mutable variables -- remember Ocaml is not a "pure" language, and allows side effects everywhere.

Anyway, Hindley-Milner should generalize let f = (\x-&gt;x)(\y-&gt;y) in ... just fine. First, \y-&gt;y is given the monotype $\alpha\to\alpha$, where $\alpha$ is a fresh type variable. Then \x-&gt;x is given $\beta\to\beta$, with a fresh $\beta$. Then we type check the application, which succeeds and unifies $\beta = (\alpha\to\alpha)$. The resulting type for the application is $\alpha\to\alpha$. Since $\alpha$ is not present in the environment, it can be generalized so the we get
$f : \forall \alpha.\, \alpha\to\alpha$.

Bonus exercise: type check the following

# let myid y = (fun x -&gt; x)(fun x -&gt; x) y ;;
val myid : 'a -&gt; 'a = &lt;fun&gt;
# myid myid myid true;;
- : bool = true