Invalid tokens are silently accepted

[leodemoura]

Consider the following example

def a := "hello"

macro (priority := high) "0" : term => `(a)

#eval 0
-- 0 

The parser above is bogus, but Lean does not report an error.
Note that the parser always parses numerals as numLit independently of tokens defined by the user. I think this is a sensible behavior, but we should probably report an error at macro definition time.
BTW, we can create variants of this issue using different kinds of built-in literals: char, string, scientific, etc.
Example:

def  m := "hello"
macro (priority := high) "'a'" : term => `(m)
#eval 'a'
-- 'a'

Remark: users can overload individual numerals using the OfNat type class.