calc interaction with default instances

[hrmacbeth]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

This is an example where calc fails to figure out a type in an example also featuring a default instance, but there is enough information that I hope it would be able to.

Steps to Reproduce

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

example {n : Int} : n ^ 2 < 1 :=
  calc
    n ^ 2 ≤ 1 ^ 2 := sorry
    _ < 1 := sorry

Expected behavior: [What you expect to happen]

Expected to be error-free. The following, with a type annotation, does work:

example {n : Int} : n ^ 2 < 1 :=
  calc
    (n ^ 2 : Int) ≤ 1 ^ 2 := sorry
    _ < 1 := sorry

Actual behavior: [What actually happens]

invalid 'calc' step, failed to synthesize `Trans` instance
  Trans LE.le LT.lt ?m.548

Reproduces how often: [What percentage of the time does it reproduce?]

Always

Versions

nightly-2023-02-01

Additional Information

Zulip discussion