diff --git a/tests/lean/297.lean b/tests/lean/297.lean
new file mode 100644
index 0000000000..8731bcf440
--- /dev/null
+++ b/tests/lean/297.lean
@@ -0,0 +1,2 @@
+theorem r:0:=do
+0if 0then 0
diff --git a/tests/lean/297.lean.expected.out b/tests/lean/297.lean.expected.out
new file mode 100644
index 0000000000..c72f5ed62a
--- /dev/null
+++ b/tests/lean/297.lean.expected.out
@@ -0,0 +1,18 @@
+297.lean:1:10-1:11: error: typeclass instance problem contains metavariables
+  OfNat (Sort ?u) 0
+297.lean:2:0-2:1: error: failed to synthesize instance
+  OfNat (Id PUnit) 0
+297.lean:2:4-2:5: error: failed to synthesize instance
+  OfNat Prop 0
+297.lean:2:10-2:11: error: failed to synthesize instance
+  OfNat (Id 0) 0
+297.lean:1:10-1:11: error: failed to synthesize instance
+  OfNat (Type ?u) 0
+297.lean:2:1-2:11: error: application type mismatch
+  pure PUnit.unit
+argument
+  PUnit.unit
+has type
+  PUnit
+but is expected to have type
+  0