Meta issue: Lean Kernel Logic renovation

This plan was worked out in collaboration with @nomeata.

Motivation

This summer's crop of implementation issues affecting the soundness of the kernel suggests that we should consider making changes to the kernel logic that make it easer to implement a bug-free kernel, that make verification of the kernel more feasible, and that play better with the module system.

One way to make the kernel simpler to implement and (hopefully) verify is to avoid inference and heuristics in the kernel, make its interface more explicit and leave these choices to the elaborator. This avoids implementation bugs where different code paths make accidentally different changes.

Concretely, we would like to achieve the following

• A decidable, transitive definitional equality algorithm
• Feature selection for inductives (large elimination, rule-K, projections, eta) is done by the elaborator and communicated explicitly, the kernel only checks.
• Such features are enabled/disabled once in general, not per-user and per-instantiation (e.g. which projections are allowed), for a simpler implementation and less corner cases
• Proofs never have to be reduced during type checking, so that the module system can omit proofs reliably
• Level comparison is complete, so that meta programs and encodings work reliably

Items

To achieve these, we plan to make the following changes: (Some points to be pulled into their own issues and just linked here)

• Complete level comparison algorithm (cf. Mario Carneiro’s research)
• Fixes to eta-related issues (#12636):
  • Expand the unit-like criteria to handle Pi types of which the codomain is unit-like, and structures whose fields are all unit-like or proof-irrelevant.
  • Expand the condition for which the major of a recursor can be eta-expanded to handle subsingleton types.
  • Eta-expand partial recursor applications when the major is missing and is an eta-expandable structure.
  • Eta-expand partial constructor applications during conversion when necessary.
• Quotients of propositions should live in Type, not Prop (#15023)
• whnf should only ever be called on terms that are known to not be proofs, e.g in is_def_eq, is_def_eq_proof_irrel should be called before the whnf_core calls, not after. (#15103)
• Inductive declarations are now declared with the following features explicitly via boolean flags. The kernel(s) then check against these features to ensure their validity:
  • Impredicativity: If true, the type must only live in Prop, its constructor fields may then be of a larger universe. If false, every field must always live in a universe smaller or equal than that of the type being defined.
  • Projections exist: true only if the type has one constructor, is non-indexed and is not impredicative.
  • Eta rule applies: true only if projections exist and the type is not recursive.
  • Rule-K applies: true if the type always lives in Prop, is non-mutual, has only one constructor and no field (e.g Eq) (This flag already exists in the type's recursor).
  • Large elimination: Recursor eliminates into any sort. True if a type is non-impredicative and either:
    • Never lives in Prop (e.g most inductive types)
    • Has no constructor (e.g False)
    • Has eta (i.e is a non-recursive structure, e.g And, PSigma)
    • has rule K (i.e has one constructor with no fields, e.g Eq)

Changes to large elimination

The main changes to whether a type largely eliminates compared to before is that

• Recursive predicates like Acc do not have large elimination anymore. This is currently a source of undecidability for definitional equality, the large eliminator (and a propositional version of its iota rule) can be recovered using the axiom of choice (see lean4#13851). The following paper justifies that having Acc's iota rule be a propositional equality rather than a definitional one is enough for Acc to not cause undecidability of type-checking in Lean.
• Sort-polymorphic structures now have large elimination, fixing a gap where for some types, some projections existed but could not be defined using their recursors lean4#7637. The reasoning for accepting this is that such structures must be non-impredicative, meaning each field's universe is always smaller or equal to that of the type getting defined. In particular, when instantiating the type to Prop, every field's universe must also be Prop, in which case the type is a syntactic subsingleton, making its large elimination okay.
• In the existing criteria, Prop inductive types with a single constructor and for which every field is either a Prop or a non-uniform parameter are large-eliminating. Lean does not have a concrete notion of non-uniform parameters, and instead makes a syntactic check for such parameters only in the large elimination check. As far as I'm aware, the only reason this was originally added was to support Acc, which will not largely eliminate in the new criteria since it is recursive anyway. As such, I believe the condition around non-uniform parameters can be safely dropped.

Changes to projections

The main change to projections is that structure types living in Prop and whose fields are not all Props do not have projections anymore. This means that the following examples do not work anymore:

structure Foo : Prop where
  n : Nat
  p : True
  
variable (x : Foo) 
#check x.2 -- used to work, would now fail 

variable (y : ∃ (_ : True), True)
#check y.1 -- similarly
#check y.2 -- similarly

We believe this to be okay, as such projections 1. can be recovered using the (non-largely eliminating) recursors for such types and 2. have no computational content anyway since they must return proofs. Changes to the elaborator can be made to recover the old behaviour for such projections at the user-level.

Furthermore, this change means that a structure will either have projections for every field of its constructor, or none at all.

This change ensures that less information is inferred at call-sites when type-checking a term, making things like projections and eta be checked consistently upon defining inductive types instead.

Plan of attack

Where we remove features, we can adjust the library and meta code to avoid them already now or at any time (e.g. https://github.com/leanprover/lean4/pull/14892, https://github.com/leanprover/lean4/pull/14925). The kernel changes we would prefer to bundle into a single release, together with an update of the ndjson output format (new flags). Kernel Arena tests and external checkers should only need one update.

Start with the plan in this issue and the kernel entry point src/kernel/type_checker.cpp, especially is_def_eq, is_def_eq_proof_irrel, and whnf_core. Review the linked issues for eta, quotients, and proof handling, then inspect the kernel Arena tests and external checkers mentioned in the plan. Done means the planned kernel changes, library and meta updates, ndjson format update, and checker updates are coordinated for a release.