why aren't these functions equivalent?

Stream: new members

[Alok Singh]

--works
def f (x : Int) : if x == 0 then Nat else Nat :=
  match _h: x == 0 with
    | true => (3:Nat)
    | false => (5:Nat)

--
def f' (x:Int) : if x == 0 then Int else Nat :=
  if _h: x == 0 then
/- type mismatch
  3
has type
  Nat : Type
but is expected to have type
  if (x == 0) = true then Int else Nat : Type
-/
    (3:Nat)
  else
/- type mismatch
  5
has type
  Nat : Type
but is expected to have type
  if (x == 0) = true then Int else Nat : Type
-/
    (5:Nat)

def f'' (x:Int) : if x == 0 then Nat else Nat :=
  match _h: x == 0 with
/- failed to synthesize
  OfNat (if true = true then Nat else Nat) 3
numerals are polymorphic in Lean, but the numeral `3` cannot be used in a context where the expected type is
  if true = true then Nat else Nat
due to the absence of the instance above
Additional diagnostic information may be available using the `set_option diagnostics true` command. -/
  | true => 3
-- ditto
  | false => 5

I thought if and match would be the same, but only the match with ascription works.

[Alok Singh]

similar issue with

def natOrStringThree (b : Bool) : if b then Nat else String :=
  if h: b then
    (3 : Nat)
  else
    "three"

def natOrStringThree' (b : Bool) : if b then Nat else String :=
  match b with
  | true => (3 : Nat)
  | false => "three"

taken from @David Thrane Christiansen 's FPIL.

[Eric Wieser]

I think the if version will work if you insert a cast (if_pos h)