Nested inductive types: uninformative error on inductive-inductive translation

[arthur-adjedj]

This is honestly a very minor paper-cut, I'm not sure whether this should be categorised as a small bug or as an RFC improvement. I'm mainly posting this issue for the sake of documenting it.

Description

When trying to translate nested inductive types into mutual inductive types, the translation might lead to the formation of inductive-inductive types. When this happens, the nested inductive type does not get accepted, as one would expect. However, the error is quite uninformative.

Context

@thomas-lamiaux, who is working on nested inductive types in Coq, has pointed out recently that, for a nested inductive type to be correctly translated into a mutual inductive type, it is necesary that, for each nested occurences I Ds Is:
(1) the parameters in which the type appears nested in appear strictly positively in the constructors of I
(2) those parameters must not appear in the indices of I

(1) is needed to ensure the soundness of the system, (2) is necessary to ensure that the mutual translation does not lead to the construction of an inductive-inductive type, which neither Lean nor Coq is supposed to support.
Lean currently checks (1) by translating nested inductive types into mutual inductive types. However, it does not check for (2) during that translation, leading to the construction of an inductive-inductive type that then gets rejected with an uninformative error.

Steps to Reproduce

MWE

set_option inductive.autoPromoteIndices false in
inductive Foo (A : Type) : (A -> A) → Type where

inductive Bar where
  | bar : Foo Bar (fun x => x) → Bar

The nested inductive type Bar gets wrongly translated into:

mutual 
  inductive Bar where
  | bar : FooBar (fun x => x) → Bar

  inductive FooBar : (Bar → Bar) → Type where
end

Expected behavior: The kernel gives a clear error which explains that this is not a valid nested inductive type

Actual behavior: The kernel throws an uninformative error (kernel) unknown constant 'Bar'

Versions

Lean 4.15.0-rc1
Target: x86_64-unknown-linux-gnu

Additional Information

The kernel could benefit from having (2) be checked in is_nested_inductive_app, and throw an early error when the condition is not met.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[nomeata]

I'd categorize it as a bug.