refine and resetI

Stream: general

[Kenny Lau]

import tactic.cache

example : ∀ [has_add unit], true :=
begin
  refine λ _, _, resetI,
  letI : has_add unit := by apply_instance,
  -- tactic.mk_instance failed to generate instance for
  --   has_add unit
  trivial
end

[Kenny Lau]

resetI fails to cache instances generated by refine

[Yaël Dillies]

I'm getting the same problem. Any fix in view?

[Kevin Buzzard]

Kenny's code works for me. Oh lol this is probably because unit didn't used to have an addition but now it does.

Modified MWE:

import tactic

example : ∀ [has_add bool], true :=
begin
  refine λ _, _, resetI,
  -- _x: has_add bool
  letI : has_add bool := by apply_instance,
  -- tactic.mk_instance failed to generate instance for
  --   has_add bool
  trivial,
end

[Yaël Dillies]

I'm hitting that in #11490 in ring_theory.local_properties

[Kevin Buzzard]

  letI : has_add bool := _x,

works as a workaround

[Yaël Dillies]

Yeah, unfortunately I have two of them, so using introsI is shorter.