bug: nonsensical disapperarence of kernel error message

Stream: lean4

[Julien Marquet-Wagner]

Hello,
I encountered a bug where I can get the kernel to complain or not about a non valid occurrence of the datatypes being declared. I triggered this with mutually inductive definitions.
Here's a MWE, plus, depending on whether I got this right or not, some additional test cases.

What kind of bug is this? Should I post this on https://github.com/leanprover/lean4/issues? And how can I work around it? (I mean, is there a more elegant solution than adding this f in a mutual block :laughing: )

/- MWE -/

structure ISignature (I : Type u) : Type (max u v + 1) where
  symbols : I → Type v
  indices : {i : I} → symbols i → List I

inductive All {I : Type u} (P : I → Type v) : List I → Type (max u v) where
  | nil : All P []
  | cons : P x → All P xs → All P (x :: xs)

namespace MWE

mutual /- Comment `f` to get
  `(kernel) arg #6 of '_nested.All_1.cons' contains a non valid occurrence of the datatypes being declared`
  Why should the presence of `f` affect the validity of `Iμ`? -/

inductive f {I : Type u} (ζ : ISignature.{u,v} I) : Type (max u v)
inductive Iμ {I : Type u} (ζ : ISignature.{u,v} I) : I → Type (max u v) where
  | mk : (i : I) → (s : ζ.symbols i) → All (Iμ ζ) (ζ.indices s) → Iμ ζ i

end -- tested on nightly-2024-02-21

end MWE

/- Additional cases -/

section PotentialTestCases

inductive IInterp (ζ : ISignature.{u,v} I) (P : I → Type w) (i : I) : Type (max u v w) where
  | mk : (s : ζ.symbols i) → All P (ζ.indices s) → IInterp ζ P i

namespace Case1
/- I'm not sure whether this is really strictly positive or not, should Lean accept this ? -/

inductive Iμ {I : Type u} (ζ : ISignature.{u,v} I) : I → Type (max u v) where
  | mk : (i : I) → (s : ζ.symbols i) → All (Iμ ζ) (ζ.indices s) → Iμ ζ i

end Case1

namespace Case2
/- If Case1 is OK (and if I got it right) Lean should accept this -/

notation:max "I⟦ " ζ " ⟧" => IInterp ζ

inductive Iμ {I : Type u} (ζ : ISignature.{u,v} I) : I → Type (max u v) where
  | mk : (i : I) → I⟦ ζ ⟧ (Iμ ζ) i → Iμ ζ i

end Case2

namespace Case3
/- This is probably *not* a planned feature for Lean, but just for reference
  this is my best try at a faithful translation of the code. -/

def i_universal {I : Type u} (P : I → Type v) := {i : I} → P i
local notation:max "∀[ " P " ]" => i_universal P

def i_exponential {I : Type u} (P : I → Type v) (Q : I → Type w) := fun i => (P i → Q i)
local infixr:30 " ⇒ " => i_exponential

inductive Iμ {I : Type u} (ζ : ISignature.{u,v} I) : I → Type (max u v) where
  | mk : ∀[ I⟦ ζ ⟧ (Iμ ζ) ⇒ Iμ ζ]

end Case3

end PotentialTestCases

/- This is from -- specifically 3.3
  Cas van der Rest, Casper Bach Poulsen, Arjen Rouvoet, Eelco Visser, and Peter Mosses. 2022
  Intrinsically-Typed Definitional Interpreters à la Carte
  https://doi.org/10.1145/3563355

  I'm trying to translate their code from Agda to Lean 4
  artifact https://doi.org/10.5281/zenodo.7074690
  oopsla-code/oopsla-src/Supplementary/Signature.agda, l.90-118
  -/

[Mario Carneiro]

In your first example, it's not that with f you don't get the arg #6 of '_nested.All_1.cons' contains a non valid occurrence error, you get a different error (kernel) declaration has free variables 'MWE.Iμ' which is presumably shadowing the first error.

[Mario Carneiro]

If I unfold the nested inductive use like so we get the declaration has free variables error again, so I think that's the original error:

mutual

inductive Iμ {I : Type u} (ζ : ISignature.{u,v} I) : I → Type (max u v) where
  | mk : (i : I) → (s : ζ.symbols i) → All_Iμ ζ (ζ.indices s) → Iμ ζ i

inductive All_Iμ {I : Type u} (ζ : ISignature.{u,v} I) : List I → Type (max u v) where
  | nil : All_Iμ ζ []
  | cons : Iμ ζ x → All_Iμ ζ xs → All_Iμ ζ (x :: xs)

end

[Mario Carneiro]

unfolding the mutual as well results in something that passes:

inductive Iμ {I : Type u} (ζ : ISignature.{u,v} I) : I ⊕ List I → Type (max u v) where
  | mk : (i : I) → (s : ζ.symbols i) → Iμ ζ (.inr (ζ.indices s)) → Iμ ζ (.inl i)
  | nil : Iμ ζ (.inr [])
  | cons : Iμ ζ (.inl x) → Iμ ζ (.inr xs) → Iμ ζ (.inr (x :: xs))

[Arthur Adjedj]

Your Case1 errors out because Lean tries to promote Iμ's index (of type I) to a parameter, even though it shouldn't, and disabling that feature fixes the issue. However, there are no options currently to turn that off.

[Arthur Adjedj]

It would be nice to have some kind of option to turn the promotion of indices to parameters off.

[Arthur Adjedj]

Mario Carneiro said:

In your first example, it's not that with f you don't get the arg #6 of '_nested.All_1.cons' contains a non valid occurrence error, you get a different error (kernel) declaration has free variables 'MWE.Iμ' which is presumably shadowing the first error.

Are you testing this on nightly ? The declaration has free variables error should have been fixed in lean4#3246 (I don't get that error on nightly)

[Arthur Adjedj]

Furthermore, your Case2 shouldn't work, since a free variable appears in a parameter of IInterp

[Mario Carneiro]

I did not test on nightly

[Mario Carneiro]

I think Case1 reveals some issues in the promotion algorithm, which presumably are related to the fact that the elaborator currently doesn't try to simulate the nested inductive check at all and leaves the kernel to do all the error handling (even though generally this is something the elaborator tries to avoid elsewhere)

[Mario Carneiro]

Case2 also reveals issues in the promotion algorithm but in a different way: it's not always the case that promoting an index to a parameter makes it more usable. Using the trick of using mutual inductives to force no promotion, note that uncommenting foo makes Iμ pass:

mutual
-- inductive foo (ζ : ISignature.{u,v} I) (P : I → Type w) : Type (max u v w)
inductive IInterp (ζ : ISignature.{u,v} I) (P : I → Type w) : (i : I) → Type (max u v w) where
  | mk : (s : ζ.symbols i) → All P (ζ.indices s) → IInterp ζ P i
end

mutual
inductive bar {I : Type u} (ζ : ISignature.{u,v} I) : Type (max u v)
inductive Iμ {I : Type u} (ζ : ISignature.{u,v} I) : I → Type (max u v) where
  | mk : (i : I) → IInterp ζ (Iμ ζ) i → Iμ ζ i
end

[Mario Carneiro]

I think we should fix this by making the nested inductive algorithm allow such uses though

[Arthur Adjedj]

I believe there are a few things to look into here:

1. There should be an option to turn off the auto-promotion from index to paramater, users shouldn't be expected to use the mutual trick for their things to work
2. The promotion algorithm should be improved so that the index doesn't get promoted in Case1 (i.e by seeing that the index doesn't appear in the (Iμ ζ) expression, meaning it’s not fixed)
3. Lean could allow for more leniancy when it comes to having free variables in nested parameters. Note that Coq is already more lenient on that matter, but it's not clear why/how it should be justified, and whether this leads to theoretical issues. In particular, inductive types such as this one are accepted there:

Inductive EqBinTree :=
  | node
  | nil (tree1 tree2 : EqBinTree) : tree1 = tree2 -> EqBinTree.

Some Coq devs believe types such as this one could lead to a proof of UIP in Coq, which would be undesirable in their case. No-one has dived into the matter of nested inductives much in the type-theory community AFAIK.

[Julien Marquet-Wagner]

Mario Carneiro said:

Using the trick of using mutual inductives to force no promotion, note that uncommenting foo makes Iμ pass:

Thanks for this remark, this makes my code work again :tada: