simp with custom rule set succeeds unexpectedly

Stream: lean4

[Raghuram]

Is it expected behaviour for the following simp to succeed?

-- File1
import Lean.Meta.Tactic.Simp.Attr

initialize do pure () <*
  Lean.Meta.registerSimpAttr `myrule "rule for my purpose"

import File1
-- File 2

def foo : Nat := 1

class CustomClass (α : Type _) where
  data : α

theorem foo_def [CustomClass Nat] : foo = 1 := rfl

attribute [myrule 1] foo_def

-- local instance instClassNat : CustomClass Nat where
--   data := 1

-- Succeeds, even without an instance of `CustomClass Nat`
#check_tactic foo ~> 1 by
  simp only [myrule]

If I replace the definition of foo with axiom foo : Nat and add axiom bar : foo = 1 and replace the proof of foo_def with bar, then the simp succeeds iff the instance is defined, as I expected.

[Robin Arnez]

You don't need a custom ruleset for this:

def foo : Nat := 1

class CustomClass (α : Type _) where
  data : α

theorem foo_def [CustomClass Nat] : foo = 1 := rfl

theorem th : foo = 1 := by
  simp only [foo_def]

Why is this? simp tracks proofs by rfl separately, so it applies it as an rfl lemma instead of actually using it as a proof term. Because it holds by defeq (as simp knows) it only needs to match the left-hand side and doesn't need to synthesize anything. It still tries to though because you might have something like

def bar : Unit := ()

theorem bar_eq_data [CustomClass Unit] : bar = CustomClass.data := rfl

instance : CustomClass Unit := ⟨()⟩

theorem th2 : bar = () := by
  conv => lhs; simp only [bar_eq_data]