Buggy interaction between `refine` and `resetI`

Stream: general

[Markus Himmel]

Is this a known bug?

import tactic.cache

class foo :=
(a : ℕ)

example : foo → foo :=
begin
  intro h,
  resetI,
  apply_instance -- works
end

example : foo → foo :=
begin
  refine λ h, _,
  resetI,
  apply_instance,
  /-
    tactic.mk_instance failed to generate instance for
      foo
    state:
    h : foo
    ⊢ foo
  -/
end

[Kenny Lau]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/refine.20and.20resetI