partial recursive def: failed to show inhabited non empty

Stream: lean4

[Andrés Goens]

We're getting an issue with @An Qi Zhang where we have a definition that's marked as partial (because it is pretty complex to show termination) and recursive, but works by translating from one recursive type into a different recursive type. Lean won't compile it stating failed to compile partial definition 'someFunction', failed to show that type is inhabited and non empty. Here's an MWE:

inductive Foo
  | foo1 : Foo
  | foo2 : Foo → Foo

inductive Bar
  | bar1 : Bar
  | bar2 : Bar → Bar

partial def footobar : Foo → Bar
  | .foo1 => Bar.bar1
  | .foo2 f => footobar f

In this MWE, if we remove partial Lean can figure out the WF recursion and is happy to accept it, but in our real case it's not that simple. I imagine then marking footobar as partial here shouldn't produce that error though, right?

[Henrik Böving]

This is due to the implementation of partial, what Lean will do internally is translate this into an opaque footobar : Foo -> Bar with an implementedBy attribute pointing to an unsafe def that contains your actual code. in order for opaque footobar to be valid you have to provide proof that the type is inhabited, otherwise you are basically writing an axiom. So what you have to do here is:

inductive Foo
  | foo1 : Foo
  | foo2 : Foo → Foo

inductive Bar
  | bar1 : Bar
  | bar2 : Bar → Bar
  deriving Inhabited

partial def footobar : Foo → Bar
  | .foo1 => Bar.bar1
  | .foo2 f => footobar f

[Henrik Böving]

The argument for why this is a correct error to do is that basically your unsafe def can do whatever it wants and magically produce terms of arbitrary type out of thin air with unsafe cast operations which could corrupt consistency of the system if the resulting type wasn't shown to be inhabited in a safe way.