Unary/prefix minus precedence bug?

Stream: lean4

[Mac]

I discovered that trying to pass an argument with the unary minus - prefix operator applied to it results in the expression being mistaken for subtraction:

open Add
def foo :=
  add -3 4
/-
  failed to synthesize instance
    Sub (?m.631 → ?m.631 → ?m.631)
  function expected at
    3
  term has type
    ?m.965
-/

Is this a bug? Or is there some parser ambiguity problem with two different mixfix syntaxes that makes this not work in Lean?

[Brandon Brown]

Works if you put parentheses:

#reduce Int.add (-3) (-4) -- Int.negSucc 6

[Kevin Buzzard]

I think lean 3 is like this as well

[Sebastian Ullrich]

As well as Haskell

[Eric Wieser]

It looks to me like you're assuming that the lack of whitespace after - is significant to lean, but it isn't

[Eric Wieser]

f -a is parsed identically to f - a

[Mac]

Eric Wieser said:

It looks to me like you're assuming that the lack of whitespace after - is significant to lean, but it isn't

Why not though? Differentiating between prefix/postfix and infix operators by whitespace is pretty common in programming languages and Lean's notation certainly supports this possibility. It seems like this would be a major advantage of Lean's syntax over things like Haskell that cannot perform such disambiguation.

[Mario Carneiro]

what if you want a prefix notation which has a space between it and the symbol?

[Mario Carneiro]

for example most prefix notations that consist of alphabetic characters will probably want this

[Mario Carneiro]

plus even - wants it if you want to write neg_neg without starting a comment

[Mac]

Mario Carneiro said:

what if you want a prefix notation which has a space between it and the symbol?

My solution would be to define two notations for each prefix/postfix operator, one with no space and one with space. That way the absence of space can be used to disambiguate when useful while still allowing for the current behavior when that is useful.

[Mac]

My mind wander back to this and I managed to get a working example for how I would make this to work:

macro:65 (name := infixSub)
x:term:66 _sym:orelse(ws "-%" ws, noWs "-%" noWs) y:term:66 : term =>
  ``(Sub.sub $x $y)

macro:max (name := prefixSub)
_sym:"-%" x:term : term =>
  ``(Neg.neg $x)

#eval 8-%4    -- 4
#eval 5 -% 3  -- 2
#eval id -%3  -- -3
#eval (-% 2)  -- -2
#eval id-% 2  -- errors

The last expression id-% 2 would then be usable for postfix operations like the following contrived example:

macro:max (name := postfixSub)
x:term "-%" : term =>
  ``(Nat.pred ∘ $x)

#eval id-% 2  -- 1