Inductive tm' {V : Set} : Set :=
| Var : V -> tm'
| App : tm' -> tm' -> tm'
| Abs : (V -> tm') -> tm'.

Definition tm := forall X, @tm' X.

Fail Example id : tm := Abs Var.

The term "Abs Var" has type "tm'" while it is expected to have type "tm".

Example id : tm := fun _ => Abs Var.