Recently I’ve been working on type inference work on System F with subtyping, which basically does the job of Pierce’s local type inference, but in a different flavor and mechanical formalisation in Agda.

When crafting concrete examples, I wrote down the following ones:

`((\x. x) : ∀a. a -> a) 1`

This expression was however, commented on by my colleague: “`\x.x`

is a monomorphic function, you can’t annotate it with a forall type”. I paused for several seconds and started drafting on my paper:

```
-------------------- Lam
⊢ (\x. x) : a -> a
------------------------ ?
⊢ (\x. x) : ∀a. a -> a
--------------------------------------- Ann
⊢ ((\x. x) : ∀a. a -> a) : Int -> Int
-------------------------------------- App
⊢ ((\x. x) : ∀a. a -> a) 1
```

Well, which rule we are missing here? Gen rule!

```
Γ ⊢ e : A a ∉ free(Γ)
---------------------------- Gen
Γ ⊢ e : ∀a. A
```

This rule usually appears in HM-like type systems, while not in our settings. Without the Gen rule, we only can create polymorphic functions using big lambda:

`(/\a. (\x. x : a -> a)) 1`

To conclude, without adopting techniques like generalisation, `\x. x`

is not a polymorphic function.