I’m gonna chime in with my experience with this syntax in somewhat similar language. I use this syntax very frequently in Lean. It’s a pretty common case that I have two enums with cases of the same name. Without the syntax that Lean allows, I would have to add a prefix (like in haskell) or use the name of the qualified name. If you have an enum for each step of some data processing pipeline (like a compiler for example), you would want adjacent data models both in scope. Also, when you can have nested structures(again like in compilers) the noise really adds up. Here is some lean code that I recently wrote that would be much more verbose without this kind of syntax:
def num_head: Term → Term := λ t => .Lam (.Lam t)
def zero: Term := num_head $ .Var ⟨0⟩
def iterate (fn: α → α) (n: Nat): α → α := match n with
| 0 => id
| .succ n => fn ∘ iterate fn n
def five: Term := num_head $ iterate (.App (.Var ⟨1⟩)) 5 $ .Var ⟨0⟩
def Term.apply (f: Term) (args: List Term) := match args with
| [] => f
| .cons h t => (Term.App f h).apply t
def add: Term := iterate (.Lam) 4 $ (Term.Var ⟨3⟩).apply [
.Var ⟨1⟩, (Term.Var ⟨2⟩).apply [
.Var ⟨1⟩,
.Var ⟨0⟩
]
]
def mul: Term := iterate (.Lam) 4 $ (Term.Var ⟨3⟩).apply [
.App (.Var ⟨2⟩) (.Var ⟨1⟩),
.Var ⟨0⟩
]
def let_chain (chain: List Term) (last : Term): Term := match chain with
| [] => last
| .cons h t => .Let h (let_chain t last)
def ex: Term := let_chain [
five,
add,
mul,
(Term.Var ⟨1⟩).apply [.Var ⟨2⟩, .Var ⟨2⟩],
(Term.Var ⟨1⟩).apply [.Var ⟨0⟩, .Var ⟨0⟩],
(Term.Var ⟨2⟩).apply [.Var ⟨1⟩, .Var ⟨0⟩]
] (.Var ⟨0⟩)
