simp scoped instance

Stream: lean4

[James Gallicchio]

namespace A

scoped instance : HAdd String String String where
  hAdd := String.append

end A

example : (open A in "a" + "b" = "ab") := by
  simp [HAdd.hAdd] -- simp made no progress

is this a symptom of instance resynth that will be resolved once the core change reaches my project?

[Kyle Miller]

On the master branch it still makes no progress

[Kyle Miller]

You can use unfold HAdd.hAdd though

[James Gallicchio]

yeah, it's not a huge deal, just a weird side effect of the pre v4.6 behavior

[Eric Wieser]

I guess you're expected to write

example : (open A in "a" + "b" = "ab") := by
  open A in
  simp [HAdd.hAdd]

[James Gallicchio]

yep. I've just been playing with scoped instances a bit and you can kinda quickly end up in weird situations like this.

another one that came up is when you use scoped instances with outParams and auto-opening namespaces in the body of defs. You can end up in a situation where you can't actually write what you want to write at all:

class SEntails (α : Type u) (β : outParam $ Type v) where
  entails : α → β → Prop

notation x " ⊨ " y => SEntails.entails x y

namespace A
scoped instance : SEntails String Nat where
  entails a b := a = toString b
end A

namespace B
scoped instance : SEntails String Bool where
  entails a b := a = toString b
end B

open A in
def B.hello : "0" ⊨ (0 : Nat) := sorry -- failed to synthesize instance

I think this counts as abuse of outParams, but we have essentially this code in LeanSAT and no great alternative