[hoping1]

See cvoss's comment in another thread:

" What happens in the evaluator when you have

(\ a . a a) (\ x . \ y . x y)

Variables are uniquely named at parse time, but after one beta step, you have two distinct instances each of x and y, albeit in different scopes, and after a second beta step, you have two distinct variables named y in the same scope. "

This doesn't come up in most mainstream languages, but Zig and Jai are getting people excited about comptime evaluation, and dependent types need comptime evaluation as well. Uniqueness is fine until you're doing higher-order evaluation in your compilation pipeline like this, which will be more and more desirable in the future, at least if the current trends are any indication.

[guerrilla]

(\ a#0 . a#0 a#0) (\ x#1 . \ y#2 . x#1 y#2)

-->

(\ x#3 . \ y#4 . x#3 y#4)(\ x#5 . \ y#6 . x#5 y#6)

[SkiFire13]

This implies that applying a function is no longer the same as a plain substitution. Moreover this can be pretty expensive computationally.