kernel error in inductive definition

Stream: lean4

[Ioannis Konstantoulas]

I am defining some crazy inductive types to try and understand recursors and stuff, and got at the following situation:

I define

variable (α β : Type)

structure Str where
  x : α
  y : β

inductive IndStr where
  | single : IndStr
  | composite : (s : Str ℕ ℕ) → (if s.x = 0 then ℕ else IndStr) → IndStr

I do not expect Lean to be ok with this definition, but the error message I get is a bit weird:

(kernel) arg #2 of 'IndStr.f' contains a non valid occurrence of the datatypes being declared

Can someone guide me through the definitions to understand the error? I am assuming it is a "positivity" error, but I don't really understand what positivity is.

Note : the active toolchain is 4.0.0-nightly-2023-07-12.

[Kevin Buzzard]

My understanding is that (kernel) messages are always bugs. Does it reproduce on current master?

[Ioannis Konstantoulas]

I will check; the above snippet should be a mwe, there are no imports necessary.

[Ioannis Konstantoulas]

Ouch; for some reason, I am downloading at 10kbps, so it's going to take a while to get the current nightly.

[Mario Carneiro]

kernel messages are always bugs, but I happen to know that the elaborator doesn't do any positivity checking, the kernel implementation is the only implementation

[Ioannis Konstantoulas]

On latest nightly:

variable (α β : Type)
structure Str where
  x : α
  y : β

def myS : Str Nat Nat := {x := 1, y := 2}
#eval myS.x + myS.y -- sanity check

inductive IndStr where
  | single : IndStr
  | composite : (s : Str Nat Nat) → (if s.x = 0 then Nat else IndStr) → IndStr

#eval Lean.versionString -- "4.3.0-nightly-2023-09-28"

/-
  Error : (kernel) arg #2 of 'IndStr.composite' contains a
  non valid occurrence of the datatypes being declared
-/

[Ioannis Konstantoulas]

In case we are suspicious of universe level mangling, the following variation of IndStr also fails with the same message:

inductive IndStr where
  | single : IndStr
  | composite : (s : Str Nat Nat) → (if s.x = 0 then IndStr else IndStr) → IndStr

[Ioannis Konstantoulas]

In the last variant, the type of IndStr.composite always resolves to Str Nat Nat -> IndStr -> IndStr, which should not produce any errors. But interpolating the ite makes the definition not pass the kernel. Interesting!

[Ioannis Konstantoulas]

Now, in contrast to the previous definition, I define an obviously non-positive inductive type:

inductive NegInd where
  | single : NegInd
  | composite : (NegInd → Nat) → NegInd

Now, I get the expected kernel message:

(kernel) arg #1 of 'NegInd.composite' has a non positive occurrence
of the datatypes being declared

[Ioannis Konstantoulas]

Now fully minimized:

#eval Lean.versionString -- "4.3.0-nightly-2023-09-28"

-- Expected kernel error
inductive NegInd where
  | composite : (NegInd → Nat) → NegInd
/-
(kernel) arg #1 of 'NegInd.composite' has a
non positive occurrence of the datatypes being declared
-/

-- Unexpected kernel error
inductive IndStr where
  | composite : (n : Nat) → (if n = 0 then IndStr else IndStr) → IndStr
/-
(kernel) arg #2 of 'IndStr.composite' contains a
non valid occurrence of the datatypes being declared
-/

[Mario Carneiro]

that's an expected error

[Mario Carneiro]

that type is not even definitionally equal to IndStr

[Mario Carneiro]

and I think the kernel requires syntactic equality to IndStr in that position

[Mario Carneiro]

although I could be wrong

[Arthur Adjedj]

This error is kind of expected. Lean can't say that if n = 0 then IndStr else IndStr is strictly positive, because it doesn't check branches of matches for strict positivity. Coq does handle this however, but such criterion isn't specified in their docs AFAIK.

[Ioannis Konstantoulas]

Arthur Adjedj said:

This error is kind of expected. Lean can't say that if n = 0 then IndStr else IndStr is strictly positive, because it doesn't check branches of matches for strict positivity. Coq does handle this however, but such criterion isn't specified in their docs AFAIK.

So, if I understand correctly: the kernel does not know if the argument occurs positively, but it also does not know that it doesn't; thus it cannot display the non-positivity error, and gives up and simply says it cannot validate the type. Is this more-or-less correct?

[Arthur Adjedj]

no no, the kernel has a specific criteria as to whether some argument type is strictly positive or not, it just turns out its criteria isn't general enough to accept such definition

[Arthur Adjedj]

One solution in your case would be to split branches here:

variable (α β : Type)

structure Str where
  x : α
  y : β

inductive IndStr where
  | single : IndStr
  | composite0 : (s : Str Nat Nat) → (s.x = 0) → Nat → IndStr
  | compositeS : (s : Str Nat Nat) → (s.x ≠ 0) → IndStr → IndStr

[Arthur Adjedj]

That's not ideal, and you do lose some definitional equality, but that's probably your best solution here

[Ioannis Konstantoulas]

Thank you for the clarification!

For the record, I do not have any goal in making these weird definitions other than to understand how Lean inductive types work. :smile:

[Arthur Adjedj]

Ioannis Konstantoulas said:

Arthur Adjedj said:

This error is kind of expected. Lean can't say that if n = 0 then IndStr else IndStr is strictly positive, because it doesn't check branches of matches for strict positivity. Coq does handle this however, but such criterion isn't specified in their docs AFAIK.

So, if I understand correctly: the kernel does not know if the argument occurs positively, but it also does not know that it doesn't; thus it cannot display the non-positivity error, and gives up and simply says it cannot validate the type. Is this more-or-less correct?

To be more specific than that: the kernel only knows about recursors, not pattern matching, and since your if condition here reduces to something like Decidable.rec (fun _ => Nat) (fun _ => DecidableEq), it'd pretty hard for the kernel to guess that something like this is indeed strictly positive. The situation is much easier for Coq/Agda since their main checkers do know about pattern-matching.

[Mario Carneiro]

well lean of course does know about pattern matching, after all we are talking about the very module that produces the recursors

[Arthur Adjedj]

Lean's elaborator layer does know about it, sure, but pattern-matching is non-existent in the kernel, isn't it ? That was the point I was trying to make here

[Mario Carneiro]

no, pattern matching exists in the kernel in the form of recursors with a computation rule

[Mario Carneiro]

(this is also basically how the elaborator sees pattern matching)

[Arthur Adjedj]

Sure, I wasn't arguing otherwise, but the fact still stands that recursors are syntaxically functions (with computational rules, but functions nonetheless), whereas pattern-matches are a distinct syntaxical objects in other ITPs, which makes it easier forthem to handle strict-positivity over them.

[Arthur Adjedj]

To be clear, I don't think it'd be impossible for Lean's kernel to extend its positivity-checker to handle the "branches" of recursors, simply that recursors aren't ideal to deal with for such things.

[Mario Carneiro]

I don't see why it would make any difference at all

[Mario Carneiro]

the better question is why such a pass is justified

[Mario Carneiro]

to me, it's not just about positivity, it's about knowing the inductive has a certain shape, which is relevant to computing the recursor. If you have arbitrary functions in the constructors, then even setting aside the consistency issues it's not at all clear what the recursor is supposed to look like

[Arthur Adjedj]

I don't think I've ever encountered a justification as to why branching over matches for strict positivity is "okay" in coq, its page discussing its Theory of Inductive Types doesn't discuss anything of the sort.

[Joachim Breitner]

Just guessing here, but maybe because it's equivalent to a (dependent) product with positive occurrence of the inductive? I.e. factor the branch into one that returns a sum type, and the body of the branch into a function type depending on that result?