fix: check uniformity of occurrences of the datatypes being declared - #14582
Conversation
This PR makes the kernel reject inductive declarations in which a datatype being declared occurs applied to arguments that are not the parameters of the mutual declaration. Such non-uniform occurrences could hide in the parametric arguments of a nested inductive datatype, which are dropped from the generated auxiliary declaration and thus escaped type checking, making the kernel unsound. Parameter uniformity is now checked once per constructor by a `check_uniform_params` pass (which also recurses into indices), so `is_valid_ind_app` becomes the purely structural `is_ind_app`, and the "no occurrence of a datatype being declared in an index" rule (#2125) is checked by the positivity checker and the return-type check via `check_ind_app_idxs`. The same `check_uniform_params` is reused to check the dropped parameters of nested occurrences. This is one possible approach to the problem raised by Arthur Adjedj in #14577 (comment) . The indices of a dropped parameter are currently only checked for parameter uniformity, not for occurrences of the datatypes being declared; whether they should be rejected there as well is left as an open question (`tests/elab/issue_14576_nonuniform.lean` documents the current behaviour). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01M76j5tLx6UcuqjoAcM8iPS
|
This is just a discussion starter. I feel like the change is already a bit too big given the corner case it fixes, at this point it may be worth going for even bigger refactoring that make the code simpler (e.g. fully checking the pre-aux constructor types ahead of time, with just a more liberal positivity check) |
Identify the datatypes being declared by name (`is_ind_occ` / `m_ind_names`) throughout the inductive checker, instead of comparing against constants carrying the declaration's universe levels. Universe-level uniformity of recursive occurrences, which was previously enforced only implicitly by that constant comparison in `is_ind_app`, is now checked explicitly in `check_uniform_params`, so it also covers the dropped parameters of nested occurrences. `is_ind_app` becomes a structural name/arity test, `is_rec` reuses `has_ind_occ`, `check_uniform_params` takes the datatype names and levels directly instead of a predicate, and `m_ind_cnsts` is dropped in favour of `m_ind_names`. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01M76j5tLx6UcuqjoAcM8iPS
github-actions
Bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
|
Reference manual CI status:
|
|
As I attempt to fix this, I find that I dislike any fix that I can fit in the current design, and I'm drawn towards bigger refactoring. What I have in mind is a shared recursive pipeline for inductives that first does general checks (well-typed, uniform level and expr parameters). Then do a positivity check. If successful, create recursor. If not, create aux decls, call the whole pipeline again, and then transport the generated recursors as before. This might make it less likely that a check is missing from one of the two “views” in a bad way. But such a rewrite is risky, of course, as it can introduce new bugs. |
Replace the previous approach, which threaded parameter uniformity through `is_valid_ind_app`, the positivity checker and the nested-occurrence elimination, with a single self-contained pass over the type former and constructor types, run first thing in `environment::add_inductive`. The pass rejects every occurrence of a datatype being declared that is not applied to the declaration's universe levels and parameters, and leaves the code that follows untouched. Reduction can never create an occurrence of a datatype being declared, since those are not yet in the environment, so checking the syntactic occurrences up front covers all of them: those a later `whnf` erases, and those in the parametric arguments of a nested occurrence, which are dropped from the auxiliary declaration and used to escape checking. The frontend already enforces the same invariant (`lean.inductiveParamMismatch`, `lean.inductiveParamMissing`) and normalizes the occurrences it accepts, so this only affects declarations built with `addDecl` directly. `tests/elab/issue_14576_nonuniform.lean` documents the two cases that used to be accepted: an occurrence erased by `whnf`, and one with non-uniform universe levels. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Xn6AmBjbQhxRdfgwkdjyJo
nomeata
changed the title
…lean4 into joachim/nested-unif-param
|
@arthur-adjedj I gave this another shot with a less invasive change, no code refactoring. One thing I noticed: Right now the field of a constructor can contain references to This feels quite similar to a bad occurrence in a phantom parameter of an inductive. So probably best to remove as well? So this change would make the lean kernel be more restrictive:
WDYT? |
Log each `addDecl`-built inductive declaration in readable form before adding it, so the pretty-printed types show up in the `#guard_msgs` output and stay in sync with the `Expr`s that construct them. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Xn6AmBjbQhxRdfgwkdjyJo
github-actions
Bot
added
the
mathlib4-nightly-available
arthur-adjedj
left a comment
arthur-adjedj
left a comment
There was a problem hiding this comment.
I think this is a good change, and I don't really see a use-case where a user would want to change the parameters of an occurrence that gets erased after whnf.
| application itself is visited as a subterm of `t` and checked (and pruned) below. */ | ||
| if (args.size() > nparams) | ||
| return true; | ||
| bool ok = args.size() == nparams && offset >= nparams && const_levels(fn) == lvls; |
There was a problem hiding this comment.
Are the first two conditions ever supposed to return false ? If an inductive occurrence happens to have less parameters than needed, this should triggers errors down the line in the nested translation anyway. I'm happy to reinforce the checks early on in practice though.
There was a problem hiding this comment.
The return true on overapplied makes the for_each function go down the app, so this is really just zooming in on the application with just the parameters, not the indices.
and
this should triggers errors down the line in the nested translation anyway
is a line of thought that bit us before :-)
There was a problem hiding this comment.
In this case, how about throwing more fine-grained errors here depending on what causes false rather than bundle 4 errors in 1 ? If, for example, the offset >= nparams is false, this means the inductive type being declared appears recursively in the telescope of parameters at the beginning of the constructor. In this case, "it must be applied to the parameters and universe levels of the mutual declaration" is not really informative (then again, no normal user should ever encounter this issue in practice, so perhaps this isn't so bad..)
There was a problem hiding this comment.
yeah, no need to optimize for error messages.
But you are right, simply looking at offset here isn't quite right; it also should check that the parameter telescope at the beginning of the constructor matches that of the type, right?
There was a problem hiding this comment.
Ideally, every regular checks on inductives should also be ran on their initial, possibly nested version IMO, but that's a bigger refactor. If the short-term plan is to have this be merged, then ensuring that parameters telescopes are correct here makes sense. Note that currently, the type of each parameter bound by the telescope is checked up to defeq. It might be interesting to see if anything breaks from making this check syntactic, both early on in check_uniform_ind_occs and in the existing check in check_constructors (and perhaps also in check_inductive_types's ?)
There was a problem hiding this comment.
I guess users might want something like
inductive Id' (a : Type) : Type where
| mk : (a : Type := Bool) → a → Id' a
but right now that’s not valid, so one could probably make that a syntactic check.
But the elaborator allows
mutual
inductive Id1 (a : Type) : Type where
| mk : Id2 a → Id1 a
inductive Id2 (a : id Type) : Type where
| mk : Id1 a → Id2 a
end
so a syntactic check would break that.
There was a problem hiding this comment.
Added tests and comments in that direction, but am inclined to not do more here.
The pass no longer visits the type former types, so the per-expression helper has a single caller; fold it into `check_uniform_ind_occs`. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Xn6AmBjbQhxRdfgwkdjyJo
mathlib-lean-pr-testing
Bot
added
the
builds-mathlib
The rest of the inductive checker matches application spines without stripping `mdata` (`is_valid_ind_app`, the return type check), and binder domains are unwrapped with `consume_type_annotations` before use, so the check need not handle `mdata` either. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Xn6AmBjbQhxRdfgwkdjyJo
leanprover-bot
added
the
builds-manual
Note in `check_uniform_ind_occs` that treating the leading bound variables as the parameters relies on `get_params` and `check_constructors` establishing that they are the parameters, and add the two cases that exercise it: a constructor whose parameter binder is only definitionally equal to the type former's parameter, which is accepted, and one whose leading binder is a `let`, so that the check reads a `let`-bound variable as the parameter and the declaration is rejected downstream instead. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Xn6AmBjbQhxRdfgwkdjyJo
Cover that the datatypes of a mutual inductive declaration may spell their parameter types differently, as in `Id1 (a : Type)` next to `Id2 (a : id Type)`, and that nothing normalizes them afterwards. The constructors of both datatypes take the parameter type of the first type former, which is the one the kernel compares each constructor telescope against. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Xn6AmBjbQhxRdfgwkdjyJo
…14582) This PR makes the kernel reject inductive declarations in which a datatype being declared occurs applied to anything other than the parameters and universe levels of the declaration. Such non-uniform occurrences could previously hide in positions that escape the kernel's checks: behind a reduction that erases them, or in the parametric arguments of a nested occurrence, which are dropped from the auxiliary declaration the kernel generates and were therefore only checked for well-typedness. The check is a self-contained pass over the type former and constructor types, run first thing in `environment::add_inductive`. Since reduction can never create an occurrence of a datatype being declared, checking the syntactic occurrences up front covers all of them, and the rest of the inductive checker is left untouched. The frontend already enforces the same invariant (`lean.inductiveParamMismatch`, `lean.inductiveParamMissing`) and normalizes the occurrences it accepts, so only declarations built with `addDecl` directly are affected. `tests/elab/issue_14576_nonuniform.lean` documents the two kinds of declaration that used to be accepted: one where `whnf` erases the occurrence, and one where the universe levels are not uniform. Raised by Arthur Adjedj in #14577 (comment). Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com> (cherry picked from commit 6eb06a5)
…14582) This PR makes the kernel reject inductive declarations in which a datatype being declared occurs applied to anything other than the parameters and universe levels of the declaration. Such non-uniform occurrences could previously hide in positions that escape the kernel's checks: behind a reduction that erases them, or in the parametric arguments of a nested occurrence, which are dropped from the auxiliary declaration the kernel generates and were therefore only checked for well-typedness. The check is a self-contained pass over the type former and constructor types, run first thing in `environment::add_inductive`. Since reduction can never create an occurrence of a datatype being declared, checking the syntactic occurrences up front covers all of them, and the rest of the inductive checker is left untouched. The frontend already enforces the same invariant (`lean.inductiveParamMismatch`, `lean.inductiveParamMissing`) and normalizes the occurrences it accepts, so only declarations built with `addDecl` directly are affected. `tests/elab/issue_14576_nonuniform.lean` documents the two kinds of declaration that used to be accepted: one where `whnf` erases the occurrence, and one where the universe levels are not uniform. Raised by Arthur Adjedj in #14577 (comment). Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com> (cherry picked from commit 6eb06a5)
3 participants
This PR makes the kernel reject inductive declarations in which a datatype being declared occurs applied to anything other than the parameters and universe levels of the declaration. Such non-uniform occurrences could previously hide in positions that escape the kernel's checks: behind a reduction that erases them, or in the parametric arguments of a nested occurrence, which are dropped from the auxiliary declaration the kernel generates and were therefore only checked for well-typedness.
The check is a self-contained pass over the type former and constructor types, run first thing in
environment::add_inductive. Since reduction can never create an occurrence of a datatype being declared, checking the syntactic occurrences up front covers all of them, and the rest of the inductive checker is left untouched.The frontend already enforces the same invariant (
lean.inductiveParamMismatch,lean.inductiveParamMissing) and normalizes the occurrences it accepts, so only declarations built withaddDecldirectly are affected.tests/elab/issue_14576_nonuniform.leandocuments the two kinds of declaration that used to be accepted: one wherewhnferases the occurrence, and one where the universe levels are not uniform.Raised by Arthur Adjedj in #14577 (comment).
Co-Authored-By: Claude Opus 5 noreply@anthropic.com