fix: calc: synthesize default instances

This is necessary to figure out the types with exponentiations.

Fixes #2079

src/Lean/Elab/Calc.lean

@@ -86,7 +86,7 @@ def elabCalcSteps (steps : Array Syntax) : TermElabM Expr := do
         throwErrorAt step[0] "invalid 'calc' step, left-hand-side is{indentD m!"{lhs} : {← inferType lhs}"}\nprevious right-hand-side is{indentD m!"{prevRhs} : {← inferType prevRhs}"}"
     types := types.push type
     let proof ← elabTermEnsuringType step[2] type
-    synthesizeSyntheticMVars
+    synthesizeSyntheticMVarsUsingDefault
     proofs := proofs.push proof
     prevRhs? := rhs
   let mut result := proofs[0]!

tests/lean/2040.lean

@@ -12,7 +12,7 @@ example (n : Nat) (a : Int) : a = 22 :=
 example (n : Nat) (a : Int) : a = (2 : Int) ^ n :=
   calc
     a = (37 : Int) := sorry
-    _ = 2 ^ n := sorry -- could be an error, but here unification figures out that (2 : Int) from the goal
+    _ = 2 ^ n := sorry -- should be same error as above
 
 example (n : Nat) (h : n = 42) : 42 = (n : Int) :=
   calc

tests/lean/2040.lean.expected.out

@@ -2,4 +2,11 @@
   HPow Nat Nat Int
 2040.lean:9:8-9:13: error: failed to synthesize instance
   HPow Nat Nat Int
-2040.lean:12:0-12:7: warning: declaration uses 'sorry'
+2040.lean:15:8-15:13: error: failed to synthesize instance
+  HPow Nat Nat Int
+2040.lean:13:2-15:22: error: type mismatch
+  trans (sorryAx (a = 37)) (sorryAx (37 = 2 ^ n))
+has type
+  a = @OfNat.ofNat Nat 2 (instOfNatNat 2) ^ n : Prop
+but is expected to have type
+  a = @OfNat.ofNat Int 2 instOfNatInt ^ n : Prop

tests/lean/run/2079.lean

@@ -0,0 +1,10 @@
+@[default_instance] instance : Pow Int Nat where
+  pow m n := m ^ n
+
+instance : @Trans Int Int Int (· < ·) (· < ·) (· < ·) where
+  trans := sorry
+
+example {n : Int} : n ^ 2 < 1 :=
+  calc
+    n ^ 2 < 1 ^ 2 := sorry
+    _ < 1 := sorry