leanprover
cdot function notation fails to macro expand properly when there is ambiguous syntax
Description
If ambiguous notation appears inside a cdot function, then the function can end up with more arguments than expected since expandCDot? collects cdots from each alternative in choice nodes.
Context
Appeared on Zulip
Steps to Reproduce
In the following, the cdot function should have one argument, but it ends up with two:
def tag (_ : α) (y : α) := y
notation "f" x => tag 1 x
notation "f" x => tag "2" x
#check (String.length <| f ·)
-- fun x x_1 => (f x).length : (x : String) → ?m.4972 x → Nat
Versions
nightly 7/25/2024
Impact
Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.
A way expandCDot? could work is to name the variables x_1, x_2, x_3, sequentially all in the same new macro scope, and then when coming across choice nodes, it saves the state, expands each alternative, and checks that each alternative creates the same number of arguments. The state could be reduced to a single Nat.
I think this would improve how (· + ·) looks when expanded, which would be fun x_1 x_2 => x_1 + x_2 rather than fun x x_1 => x + x_1.
Something that could simplify the implementation would be to do a pre-check to count arguments.