Reductive behaviour on recursively defined type families

Stream: lean4

[Jakob von Raumer]

inductive Bar where
| U : Bar
| L : List Bar → Bar

def Foo : Bar → Type
| .U => Unit
| .L [] => Unit
| .L [x] => Foo x
| .L (x::xs) => Foo x × Foo (.L xs)

example : Foo (.L [.U, .U]) := ⟨_, _⟩  -- invalid constructor ⟨...⟩, expected type must be an inductive type

This used to work in earlier Lean versions, does anyone know what change broke this?

[Floris van Doorn]

Hmmm... the following example still succeeds:

example : Foo (.L [.U, .U]) = (Unit × Unit) := by
  rfl

[Jakob von Raumer]

Just noticed that adding @[reducible] actually fixes it

[Jakob von Raumer]

What is the meaning of @[reducible] and @[semireducible] nowadays? @Joachim Breitner I think you told me the other day...

[Floris van Doorn]

dsimp [Foo] also fails to simplify the type (simp [Foo] succeeds, but modifies the constructed term).

[Floris van Doorn]

It means "unfold this more eagerly". The unification algorithm elaborator will unfold reducible definitions earlier, and many tactics will unfold reducible definitions, or index/match terms up to reducible definitions. This mostly affects simp, rw and similar tactics. But it's up to each tactic's implementation how it deals with reducible definitions, so it's hard to give a full list of what the attribute does.

[Jakob von Raumer]

@[semireducible] also suffices for the example to work correctly, so apparently the elaborator(?) also looks into the attribute?

[Floris van Doorn]

The elaborator definitely looks at these tags as well, but I'm surprised tagging it with semireducible fixes it, since I thought that was the default transparency. Maybe it isn't for definitions defined by well-founded recursion...?

[Jannis Limperg]

wfrec is now irreducible by default.

[Jakob von Raumer]

For performance reasons?

[Jannis Limperg]

I think so. Evaluation of a function defined by wfrec involves the reduction of the accessibility proofs, which can be large. So it was decided that it's safer to mark these functions as irreducible by default (and you can still simp with the generated equation lemmas). However, tagging a wfrec function as semireducible manually is still fine and supported. (reducible shouldn't be used for recursive functions in general afaik.)

[Joachim Breitner]

It's not just performance. A wfrec function is defeq to some complicated construction involving WellFounded.fix, and this construction is supposed to be “internal” and not visible to the user. If a proof relies on this definitional equality somehow, then should the internal construction change, this may break the proof. This is maybe ok if the user asks for it explicitly (using unseal or @[semireducible]), but it seems the default should be the safer @[irreducible].

[Jakob von Raumer]

To come back to this: How do I make type inference see through the above example? This doesn't work for me:

inductive Bar where
| U : Bar
| L : List Bar → Bar

@[reducible]
def Foo : Bar → Type
| .U => Unit
| .L [] => Unit
| .L [x] => Foo x
| .L (x::xs) => Foo x × Foo (.L xs)

example : Inhabited (Foo (.L [.U, .U])) := inferInstance

[Jakob von Raumer]

Is there any way at all to make it transparent to type class resolution?