bug with $ in equation compiler

Stream: general

[Kenny Lau]

@[simp] def B : ℕ → ℕ := λ x, 0
def A : ℕ → ℕ
| 0 := 0
| (x+1) := x + A $ B 0

type mismatch at application
  x + A
term
  A
has type
  ℕ → ℕ
but is expected to have type
  ℕ
Additional information:
c:\XXX.lean:4:17: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
  too many arguments

[Mario Carneiro]

Since $ has ridiculously low precedence, this is interpreted as (x + A) (B 0)