Regression in v4.33.0-rc1: simp changes the type of hoisted proof #14467

Activity

1. TWal

   added

   bugSomething isn't workingSomething isn't working

   on Jul 20, 2026
2. Kha commented on Jul 21, 2026

   

   Kha

   on Jul 21, 2026

   Member

   More actions

   The impact of this issue is not clear to me, is the actual problem that the linter is triggered? How did you determine that previous version used a different type?
3. TWal commented on Jul 21, 2026

   

   TWal

   on Jul 21, 2026

   ContributorAuthor

   More actions

   Ah indeed, you are correct: it is not a regression, in that v4.32.0 and v4.31.0 also show the same behavior.

   However, this behavior combined with #13895 creates problems down the line, for example:

   • deriving instance does not work
   • some simple theorems proved by simp do not work anymore

   Theses are a reproduction of the actual problems I encountered in DyLean, but I am sure we can find many more. For now, my workaround has been to use grind instead of simp for my proof internal to bar (shown below). But given that Lean comes with proof irrelevance, I find it weird that the tactics chosen for this inner proof actually impacts downstream proofs abour bar.

   opaque Bytes: Type
   opaque Bytes.length: Bytes → Nat
   
   structure F (α: Type) where
     serialize: α → Bytes
   class C {α: Type} (β: F α) where
   axiom wf {α: Type} (β: F α): Prop
   
   axiom foo {a: Type} (f: F a) (len: Nat) (h: ∀ x, (f.serialize x).length = len): F a
   
   instance {a: Type} (f: F a) (len: Nat) (h: ∀ x, (f.serialize x).length = len): C (foo f len h) where
   
   axiom foo_wf {a: Type} (f: F a) (len: Nat) (h: ∀ x, (f.serialize x).length = len): wf (foo f len h) = wf f
   
   def f (len: Nat): F { b: Bytes // b.length = len} where
     serialize b := b.val
   
   axiom f_wf (len: Nat): wf (f len)
   
   section WithSimp
   
   /--
   error: failed to synthesize instance of type class
     C (foo (f len) len ⋯)
   
   Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
   ---
   error: Failed to delta derive `C` instance for `bar`.
   
   Note: Delta deriving tries the following strategies: (1) inserting the definition into each explicit non-out-param parameter of a class and (2) unfolding definitions further.
   -/
   #guard_msgs in
   noncomputable
   def bar (len: Nat) : F {b: Bytes // b.length = len} :=
     foo (f len) len (by
       simp [f]
     )
   deriving C
   
   /--
   error: unsolved goals
   len : Nat
   ⊢ wf (foo (f len) len ⋯)
   ---
   warning: This simp argument is unused:
     foo_wf
   
   Hint: Omit it from the simp argument list.
     [apply] simp only [bar, f_wf]
   
   Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
   ---
   warning: This simp argument is unused:
     f_wf
   
   Hint: Omit it from the simp argument list.
     [apply] simp only [bar, foo_wf]
   
   Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
   -/
   #guard_msgs in
   theorem bar_wf (len: Nat): wf (bar len) := by
     simp only [bar, foo_wf, f_wf]
   
   end WithSimp
   
   section WithGrind
   
   noncomputable
   def baz (len: Nat) : F {b: Bytes // b.length = len} :=
     foo (f len) len (by
       grind [f]
     )
   deriving C
   
   theorem baz_wf (len: Nat): wf (baz len) := by
     simp only [baz, foo_wf, f_wf]
   
   end WithGrind
4. TWal commented on Jul 21, 2026

   

   TWal

   on Jul 21, 2026

   ContributorAuthor

   More actions

   I found a general workaround: start the tactic with apply id, like this:

   noncomputable
   def bar (len: Nat) : F {b: Bytes // b.length = len} :=
     foo (f len) len (by
       apply id
       simp [f]
     )
   deriving C