fix(library/init/meta/interactive): fixes #1943

library/init/meta/interactive.lean

@@ -1595,7 +1595,8 @@ protected meta def apply_inj_lemma : tactic unit :=
 do h ← intro `h,
    some (lhs, rhs) ← expr.is_eq <$> infer_type h,
    (expr.const C _) ← return lhs.get_app_fn,
-   applyc (name.mk_string "inj" C),
+   -- We disable auto_param and opt_param support to address issue #1943
+   applyc (name.mk_string "inj" C) {auto_param := ff, opt_param := ff},
    assumption
 
 /- Auxiliary tactic for proving `I.C.inj_eq` lemmas.

library/init/meta/tactic.lean

@@ -1001,8 +1001,8 @@ do env  ← get_env,
    return (expr.const c ls)
 
 /-- Apply the constant `c` -/
-meta def applyc (c : name) : tactic unit :=
-do c ← mk_const c, apply c, skip
+meta def applyc (c : name) (cfg : apply_cfg := {}) : tactic unit :=
+do c ← mk_const c, apply c cfg, skip
 
 meta def eapplyc (c : name) : tactic unit :=
 do c ← mk_const c, eapply c, skip

tests/lean/run/1943.lean

@@ -0,0 +1,6 @@
+open tactic
+meta def c := abstract `[assumption]
+
+structure B (U : Type) :=
+  (f : U → U)
+  (w : ∀ u : U, f u = u . c)