calc with LHS a nat

Stream: lean4

[Heather Macbeth]

One more observation about the nightly-2023-02-03 version of calc. The following gives an error

invalid 'calc' step, left-hand-side is
  Int.ofNat ?m.289 : Int
previous right-hand-side is
  3 : Nat

now, and doesn't on nightly-2023-02-02:

instance : @Trans Int Int Int LT.lt LT.lt LT.lt := sorry

example {x : Int} (hx : 3 < x) : 2 < x :=
  calc
    2 < 3 := sorry
    _ < x := sorry

The Lean 3 translation of this code also doesn't give an error.

I'm guessing the problem is that as of 02-03 Lean uses default instances to help elaborate the top-LHS, and OfNat Nat is a default instance. Is that right?

[Heather Macbeth]

In fact, the issue that prompted these changes, lean4#2079, is now broken in reverse:

instance [LE α] [LT α] : @Trans α α α LT.lt LE.le LT.lt := sorry
instance [LE α] [LT α] : @Trans α α α LE.le LT.lt LT.lt := sorry

class Monoid (M : Type) extends OfNat M (nat_lit 1), Mul M where
  npow : Nat → M → M := sorry

@[default_instance high] instance Monoid.Pow {M : Type} [Monoid M] : Pow M Nat :=
  ⟨fun x n ↦ Monoid.npow n x⟩

instance : Monoid Int where
  npow n x := x ^ n

-- works on 02-03, not 02-02
example {n : Int} : n ^ 2 < 1 :=
  calc
    n ^ 2 ≤ 1 ^ 2 := sorry
    _ < 1 := sorry

-- works on 02-02, not 02-03
example {n : Int} : 1 < n ^ 2 :=
  calc
    1 < 1 ^ 2 := sorry
    _ ≤ n ^ 2 := sorry

[Gabriel Ebner]

Is that right?

Yes.