inductive datatype declaration is corrupted

Stream: lean4

[Trebor Huang]

def Set α := α → Prop
inductive Bad : Set Nat

Creates an error

(kernel) error in 'noConfusion' generation, 'Bad' inductive datatype declaration is corrupted

I'm using leanprover/lean4:v4.0.0-rc4.

[Trebor Huang]

I think it is because when checking whether the sort of the inductive is correct, lean reduces Set, but when generating noConfusion it doesn't. Is this a bug?

[Mario Carneiro]

(kernel) errors are always a bug

[Arthur Adjedj]

I reported this issue a year ago, and was told it was simply disallowed

[Arthur Adjedj]

Mario Carneiro said:

(kernel) errors are always a bug

Some errors (like non-strict positivity) are meant to be reported by the kernel only though

[Mario Carneiro]

usually those errors are modeled by the frontend

[Mario Carneiro]

It's true that currently the kernel reports strict positivity errors, but you get low quality errors because of that

[Mario Carneiro]

normally you would expect some kind of highlight on the part of the definition that is wrong

[Mario Carneiro]

You should probably report this in an actual lean issue if you want to see progress on it

[Mario Carneiro]

I'm just the help desk :)

[Henrik Böving]

Mario Carneiro said:

I'm just the help desk :)

damn the requirements for entry level positions keep rising

[Arthur Adjedj]

As it turns out, this issue is a one-line fix, you only have to replace to_telescope(lctx,...) by to_telescope(env,lctx,...) here. I've made an issue for it. Should I also make a PR ? @Mario Carneiro if so, I saw that PRs now needed the approval of a developer to be filed as anything but a draft, is your approval enough for such matters, or should I ask someone else ?

[Mario Carneiro]

I think it needs an RFC because it's resolving the issue by making the noConfusion implementation more permissive rather than making the inductive validity checker less permissive

[Mario Carneiro]

I don't think I count as a developer for the purpose of the PR approval process

[Arthur Adjedj]

I believe that this was an unintended bug, and not a missing feature. If everything else regarding the checking of inductive types works, there is no real reason as to why someone would want to restrict noConfusion and nothing else in that regards. The error message also shows that this sort of error isn't supposed to be thrown, since it calls the inductive "corrupted". But I'll make it an RFC just to get a confirmation, thanks for your help.

[Mario Carneiro]

The error message also shows that this sort of error isn't supposed to be thrown, since it calls the inductive "corrupted".

Well, you could also interpret this as an assertion that those inductives aren't supposed to exist, or at least the person writing noConfusion thought that when they wrote it :)

[Mario Carneiro]

As I said on the other thread, the feelings regarding the acceptability of this type have waxed and waned over time

[Mario Carneiro]

On the one hand, it's nice to be able to write an inductive like this from the user side, why not allow more generality? On the other hand it complicates everything to do with inductive processing, which has a lot of index manipulation and generally wants to assume the inductive has a particular syntactic form. If the kernel can be simpler and more correct that sounds like a plus

[Mario Carneiro]

Another example along the same lines is let binders in the middle of an inductive constructor, like

inductive Foo : Nat -> Type where
  | mk : (x : Nat) -> let y := x + 1; (z : Nat) -> Foo (x + y + z)

[Mario Carneiro]

I believe Coq accepts this

[Arthur Adjedj]

Coq does accept such inductives.

[Arthur Adjedj]

Mario Carneiro said:

On the one hand, it's nice to be able to write an inductive like this from the user side, why not allow more generality? On the other hand it complicates everything to do with inductive processing, which has a lot of index manipulation and generally wants to assume the inductive has a particular syntactic form. If the kernel can be simpler and more correct that sounds like a plus

Please note that every other feature of the kernel seems to work with that change, the draft PR passes all CI/CL