fix(tactic/refine_struct): don't add unnecessary eq.mpr or id (#2319)

* fix(tactic/interactive): don't unfold non-Prop goals

The old behaviour caused `eq.mpr`'s in `pi_instance` output.

* add a test file

* move test

* actually move test

* Update test/refine_struct.lean

* test: fix compile

* Apply suggestions from code review

Co-Authored-By: Gabriel Ebner <gebner@gebner.org>

* Try a fix by @gebner and @cipher1024

* Update test/refine_struct.lean

Co-Authored-By: Gabriel Ebner <gebner@gebner.org>

* apply Gabriel's suggestion

Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

Author: 5 people

src/tactic/interactive.lean

@@ -352,7 +352,7 @@ do    tgt ← target,
       gs ← with_enable_tags (
         mzip_with (λ (n : name × name) v, do
            set_goals [v],
-           try (interactive.unfold (provided.map $ λ ⟨s,f⟩, f.update_prefix s) (loc.ns [none])),
+           try (dsimp_target simp_lemmas.mk),
            apply_auto_param
              <|> apply_opt_param
              <|> (set_main_tag [`_field,n.2,n.1]),

test/refine_struct.lean

@@ -1,7 +1,55 @@
 import tactic.interactive
 
-section refine_struct
+/-!
+`refine_struct` caused a variety of interesting problems,
+which were identified in
+https://github.com/leanprover-community/mathlib/pull/2251
+and
+https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Need.20help.20with.20class.20instance.20resolution
+
+These tests are quite specific to testing the patch made in
+https://github.com/leanprover-community/mathlib/pull/2319
+and are not a complete test suite for `refine_struct`.
+-/
+
+instance pi_has_one {α : Type*} {β : α → Type*} [Π x, has_one (β x)] : has_one (Π x, β x) :=
+by refine_struct { .. }; exact λ _, 1
+
+open tactic
+
+run_cmd (do
+  (declaration.defn _ _ _ b _ _) ← get_decl ``pi_has_one,
+  -- Make sure that `eq.mpr` really doesn't occur in the body:
+  eq_mpr ← mk_const `eq.mpr,
+  k ← kabstract b eq_mpr, -- `expr.occurs` doesn't work here, always giving `ff` even before the patch.
+  when (b.list_constant.contains ``eq.mpr) $
+    fail "result generated by `refine_struct` contained an unnecessary `eq.mpr`",
+  -- Make sure that `id` really doesn't occur in the body:
+  id ← mk_const `id,
+  k ← kabstract b id,
+  guard (k = b) <|>
+    fail "result generated by `refine_struct` contained an unnecessary `id`")
+
+-- Next we check that fields defined for embedded structures are unfolded
+-- when seen by fields in the outer structure.
+structure foo (α : Type):=
+(a : α)
+
+structure bar (α : Type) extends foo α :=
+(b : a = a)
+
+example : bar ℕ :=
+begin
+  refine_struct { a := 1, .. },
+  -- We're making sure that the goal is
+  -- ⊢ 1 = 1
+  -- rather than
+  -- ⊢ {a := 1}.a = {a := 1}.a
+  guard_target 1 = 1,
+  trivial
+end
 
+section
 variables {α : Type} [_inst : monoid α]
 include _inst
 
@@ -13,8 +61,7 @@ begin
     guard_tags _field mul_left_inv group, admit, },
   trivial
 end
-
-end refine_struct
+end
 
 def my_foo {α} (x : semigroup α) (y : group α) : true := trivial