From 50813429b85edd036eb2a9885ef3ef8082f51f60 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 16 Mar 2022 17:03:26 -0700
Subject: [PATCH] fix: add expected type hint

Other tactics (e.g., `simp_all`) may try to infer the type of the
proof, and `Nat.Linear.eq_of_toNormPoly_eq` has a messy resulting type.
---
 src/Lean/Meta/Tactic/LinearArith/Nat/Simp.lean | 2 +-
 tests/lean/run/shrinkFn.lean                   | 9 +++++++++
 2 files changed, 10 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/shrinkFn.lean

diff --git a/src/Lean/Meta/Tactic/LinearArith/Nat/Simp.lean b/src/Lean/Meta/Tactic/LinearArith/Nat/Simp.lean
index f201698022..75bd1b4a8a 100644
--- a/src/Lean/Meta/Tactic/LinearArith/Nat/Simp.lean
+++ b/src/Lean/Meta/Tactic/LinearArith/Nat/Simp.lean
@@ -22,7 +22,7 @@ def simpCnstrPos? (e : Expr) : MetaM (Option (Expr × Expr)) := do
     let r ← c₂.toArith ctx
     if r != e then
       let p := mkApp4 (mkConst ``Nat.Linear.ExprCnstr.eq_of_toNormPoly_eq) (← toContextExpr ctx) (toExpr c) (toExpr c₂) reflTrue
-      return some (r, p)
+      return some (r, ← mkExpectedTypeHint p (← mkEq e r))
     else
       return none
 
diff --git a/tests/lean/run/shrinkFn.lean b/tests/lean/run/shrinkFn.lean
new file mode 100644
index 0000000000..aa4e71fba6
--- /dev/null
+++ b/tests/lean/run/shrinkFn.lean
@@ -0,0 +1,9 @@
+abbrev shrinkFn (α : Type u) [sz : SizeOf α] := (x : α) → List { y : α // sz.sizeOf y < sz.sizeOf x }
+
+class Sampleable (α : Type u) [SizeOf α] where
+  shrink : shrinkFn α := fun _ => []
+
+def Prod.shrink [SizeOf α] [SizeOf β] (shrA : shrinkFn α) (shrB : shrinkFn β) : shrinkFn (α × β) := fun (fst, snd) =>
+  let shrink1 := shrA fst |>.map fun ⟨x, _⟩ => ⟨.mk x snd, by simp_all_arith⟩
+  let shrink2 := shrB snd |>.map fun ⟨x, _⟩ => ⟨.mk fst x, by simp_all_arith⟩
+  shrink1 ++ shrink2