From d4b9a532d235a97e737a6bc1b0984d2334e1ab6c Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Thu, 2 Feb 2023 14:29:21 -0800
Subject: [PATCH] fix: calc: synthesize default instances

This is necessary to figure out the types with exponentiations.

Fixes #2079
---
 src/Lean/Elab/Calc.lean           |  2 +-
 tests/lean/2040.lean              |  2 +-
 tests/lean/2040.lean.expected.out |  9 ++++++++-
 tests/lean/run/2079.lean          | 10 ++++++++++
 4 files changed, 20 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/run/2079.lean

diff --git a/src/Lean/Elab/Calc.lean b/src/Lean/Elab/Calc.lean
index 8c963ad64c..e892d6cdf8 100644
--- a/src/Lean/Elab/Calc.lean
+++ b/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]!
diff --git a/tests/lean/2040.lean b/tests/lean/2040.lean
index 0dbe315aa9..4fff37f95f 100644
--- a/tests/lean/2040.lean
+++ b/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
diff --git a/tests/lean/2040.lean.expected.out b/tests/lean/2040.lean.expected.out
index ac321bca75..58cb3305ed 100644
--- a/tests/lean/2040.lean.expected.out
+++ b/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
diff --git a/tests/lean/run/2079.lean b/tests/lean/run/2079.lean
new file mode 100644
index 0000000000..189f2dac2c
--- /dev/null
+++ b/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