fix(tactic/set): use provided type for new variable (leanprover-commu…

…nity#3126)

closes leanprover-community#3111




Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>

src/tactic/core.lean

@@ -856,7 +856,7 @@ do h ← get_local hyp,
    tp ← infer_type h,
    olde ← to_expr olde, newe ← to_expr newe,
    let repl_tp := tp.replace (λ a n, if a = olde then some newe else none),
-   change_core repl_tp (some h)
+   when (repl_tp ≠ tp) $ change_core repl_tp (some h)
 
 /-- Returns a list of all metavariables in the current partial proof. This can differ from
 the list of goals, since the goals can be manually edited. -/

src/tactic/interactive.lean

@@ -937,16 +937,15 @@ end
 meta def set (h_simp : parse (tk "!")?) (a : parse ident) (tp : parse ((tk ":") >> texpr)?)
   (_ : parse (tk ":=")) (pv : parse texpr)
   (rev_name : parse opt_dir_with) :=
-do let vt := match tp with | some t := t | none := pexpr.mk_placeholder end,
-   let pv := ``(%%pv : %%vt),
-   v ← to_expr pv,
-   tp ← infer_type v,
-   definev a tp v,
-   when h_simp.is_none $ change' pv (some (expr.const a [])) loc.wildcard,
+do tp ← i_to_expr $ tp.get_or_else pexpr.mk_placeholder,
+   pv ← to_expr ``(%%pv : %%tp),
+   tp ← instantiate_mvars tp,
+   definev a tp pv,
+   when h_simp.is_none $ change' ``(%%pv) (some (expr.const a [])) $ interactive.loc.wildcard,
    match rev_name with
    | some (flip, id) :=
      do nv ← get_local a,
-        pf ← to_expr (cond flip ``(%%pv = %%nv) ``(%%nv = %%pv)) >>= assert id,
+        mk_app `eq (cond flip [pv, nv] [nv, pv]) >>= assert id,
         reflexivity
    | none := skip
    end

test/set.lean

@@ -0,0 +1,38 @@
+import data.matrix.notation
+
+example (x : ℕ) (h : x = 3)  : x + x + x = 9 :=
+begin
+  set y := x with ←h_xy,
+  guard_hyp y := ℕ,
+  guard_hyp h_xy := x = y,
+  guard_hyp h := y = 3,
+  guard_target y + y + y = 9,
+  set! z : ℕ := y,
+  guard_target y + y + y = 9,
+  simp [h]
+end
+
+example : true :=
+let X1 := (![![1, 0], ![0, 0]] : matrix (fin 2) (fin 2) ℕ), -- X1 : fin 1.succ → fin 2 → ℕ
+    X2 : matrix (fin 2) (fin 2) ℕ := ![![1, 0], ![0, 0]] in -- X2 : matrix (fin 2) (fin 2) ℕ
+begin
+  set Y1 := (![![1, 0], ![0, 0]] : matrix (fin 2) (fin 2) ℕ),
+  set Y2 : matrix (fin 2) (fin 2) ℕ := ![![1, 0], ![0, 0]],
+  let Z1 := (![![1, 0], ![0, 0]] : matrix (fin 2) (fin 2) ℕ),
+  let Z2 : matrix (fin 2) (fin 2) ℕ := ![![1, 0], ![0, 0]],
+  guard_hyp Y2 := matrix (fin 2) (fin 2) ℕ,
+  trivial
+end
+
+def T {α : Type} := ℕ
+def v : @T ℕ := nat.zero
+
+def S := @T ℕ
+def u : S := nat.zero
+
+def p : true :=
+begin
+  set a : T := v,
+  set b : T := u, -- the type `T` can't be fully elaborated without the body but this is fine
+  trivial
+end