Public recursor can reference private declaration?

Stream: lean4

[Thomas Murrills]

Is it intended that recursors for structures with private fields should be public? This means that private decls used in the type of the private field can appear in the public type of the recursor.

module

private def PrivBar : Type := Bool

public structure Foo where
  private priv : PrivBar

-- public, but references private type `PrivBar`
/--
info: @[reducible] protected def Foo.recOn.{u} : {motive : Foo → Sort u} →
  (t : Foo) → ((priv : PrivBar) → motive { priv := priv }) → motive t :=
fun {motive} t _private.«external:file:///MathlibDemo/MathlibDemo.lean».0.Foo.mk =>
  Foo.rec _private.«external:file:///MathlibDemo/MathlibDemo.lean».0.Foo.mk t
-/
#guard_msgs in
#print Foo.recOn

I can imagine there might be some necessary carve-out given how fundamental recursors are to actually doing anything with the structure, but I was still surprised to hit an "unknown constant" error when looping through declarations in the environment using MetaM methods. Since this violated my expectations of how visibility should behave, I just thought I'd check. :)

[Thomas Murrills]

Still curious if I should open an issue for this, or if there's something to learn about visibility otherwise. :)

[Thomas Murrills]

Aha, with a slightly different search query I found #lean4 > Meaning of private structure constructor/fields, the issue lean4#8665, and a relevant (not yet merged) PR lean4#9648. So I suppose that covers it. :)