Propagation of intermediate instances in grind

Stream: lean4

[Robin Carlier]

Consider this very artificial mwe

class Even (n : Nat) : Prop where

class Odd (n : Nat) : Prop where

theorem even_and_odd (n : Nat) [Even n] [Odd n] : n = 0 := sorry

instance even_add (n m : Nat) [Even n] [Even m] : Even (n + m) := sorry

structure Foo (n : Nat) : Prop where

theorem foo_iff_even (n : Nat) : Foo n ↔ Even n := sorry

theorem foo_and_odd_add (n m : Nat) (h : Foo n) [Even m] [Odd (n + m)] : n + m = 0 := by
  -- grind [even_add, even_and_odd, foo_iff_even]  -- fails but the following two works
  haveI := (foo_iff_even n).mp h
  grind [even_add, even_and_odd]

The failure on the commented line indicates that grind does assert Even n as a "true fact", but it fails to go further, complaining that it can’t infer an Even n instance to instantiate even_add, when the instance is registered beforehand, it’s okay. I guess this is because grind does not try to re-synth instances at each generation (that would be too expensive maybe?)

A "real world" example where this kind of things arise is category theory: you have some (non-instance) lemmas that tell you that a morphism is an epimorphism or monomorphism (e.g from a Function.injective hyp in concrete categories), that can’t be instance (because e.g Function.injective is not a class). Then, you have a bunch of lemmas that expects a Mono instance, and grind is unable to use them as soon as a goal starts from some Function.injective hyps.

For an example in mathlib that concretely prompted this question, in file#Mathlib/AlgebraicTopology/DoldKan/NCompGamma.lean, line 58, you can’t replace

        have h' := len_le_of_epi (SimplexCategory.epi_iff_surjective.2 h)
        dsimp at h'
        omega

by

        grind [→ len_le_of_epi, len_mk, SimplexCategory.epi_iff_surjective]

but you can only replace it by

        have := epi_iff_surjective.2 h
        grind [→ len_le_of_epi, len_mk]

and it would be nice if this could be a one-liner.

Is there a workaround around this? An option that tells grind to resynthesize instances between generations? or is that kind of things simply out of scope for this tactic?