How to coerce/convert constant to the type of a given variable?

First, this isn't really about macros or notation, or even coercion. It is about how Lean elaborates terms.

When Lean elaborates the following:

#check 123 + (-456)

It has to go through a bunch of type class inference to figure out what types are involved. For example, when it sees 123 it doesn't see a Nat. What it sees is a special un-elaborated set of numeral symbols. It directly converts these numerals to some type using the OfNat typeclass. (Despite its name, OfNat is not the same thing a coercion from Nat. For example, there is an OfNat instance for UInt16, but not a coercion from Nat to UInt16, since the coercion goes the other way.) So to elaborate 123 + (-456), Lean has to make a bunch of guesses, as to what type the whole expression is, what type 123 and 456 are, what type - is, and what types + refers to. You can see all the different paths it takes (most of them failures) by turning the following option on:

set_option trace.Meta.synthInstance true
#check 123 + (-456)

(The output of synthInstance is hard to read, and too long to put in this answer, but the main point is that it goes through lots of cases before it finds the right one.)

Now in your situation, let's consider your example but using + instead of your new notation.

#check 1 + "2"

The elaborator gets stuck. It is really trying to convert the numeral 1 to a string. Elaboration failure isn't an uncommon situation in Lean. If Lean can't figure out the type from context, then give Lean a type hint. In this case, it is enough to hint to Lean that 1 is Nat (because again, Lean doesn't know that it should treat 1 as a Nat) or that the type of the whole expression is Nat. All of these work, either via type hints or type context.

#check (1 : Nat) + "2"
#check (Nat.succ Nat.zero) + "2"
#check (Nat.max 0 1) + "2"
#check (1 + "2" : Nat)
#check 1 + "2" = (3 : Nat)
#check Nat.max 0 (1 + "2")

Also, this isn't really about Lean expecting (or not expecting) the terms to be of the same type. For example, these both fails even though Lean clearly expects both arguments to be the same type:

def add3 {α : Type} [HAdd α α α] (x y : α) : α := x + y
#check add3 1 "2"

def add4 {α : Type} [Add α] (x y : α) : α := x + y
#check add4 1 "2"

Here is another example which doesn’t use existing type class instances. Even in this case you see how Lean sometimes gets stuck.

class Foo (A: Type)

inductive Bar
| mk : Bar

instance : Inhabited Bar := ⟨Bar.mk⟩
instance : (Foo Bar) := ⟨⟩

def foo {A : Type} [Foo A] [Inhabited A] (a b : A) : A := Inhabited.default

instance : Coe String Bar := ⟨fun _ => Bar.mk⟩
#check foo "a" "b"  -- fails
#check foo "a" ("b": Bar)  -- fails
#check foo ("a": Bar) "b"  -- checks
#check (foo "a" "b" : Bar)  -- checks

instance (n : Nat) : OfNat Bar n := ⟨Bar.mk⟩
#check foo 1 2  -- fails
#check foo (1 : Bar) 2  -- checks
#check foo 1 (2 : Bar)  -- checks
#check (foo 1 2 : Bar)  -- checks

Again, note that notation like (1 + "2" : Nat) is not necessarily type coercion. It is type hinting. Lean has lots of options to make a type hint work. Implicit coercion is just one method, but there are others (usually involving the type class system), such as using OfNat. For example, in (1 + 2 : Int), there is no coercion. If you click in the infoview on the 1 you see it is @OfNat.ofNat Int 1 instOfNat : Int. In (1 + "2" : Nat) there is coercion, but on "2", even though the type hint is on the outer expression. This is a subtle point, but might help clear up some confusion.

Also, in the comments Andrej makes a good point about the XY problem. It isn't clear what you are trying to do. If it is just fighting with Lean's type system, the best answer is to give more type hints. If it is something more specific, it might help to ask another more specific question (in a new post).