I am also not too impressed by the existence of second-party checkers in the context of a language that lacks decidable type checking. Because something has to give, these checkers will be (necessarily) incomplete in one way or another, most likely each in different ways. This is because lean’s failure of completeness of conversion almost certainly manifests in heuristic ways that are not predictable or replicable…

For a fail safe checker to provide confidence, it needs to be complete. This is not possible with Lean’s core language as designed, and it will not be possible for Lean itself until they find new leadership.

@ncf Two examples.

Soundly reducing a well-typed beta redex requires the domain which was used to type the abstraction's body to match the type of the argument, and the return type of the abstraction to match the type of the entire term. You get this for free only if Pi is injective, otherwise you need to do it by hand. The classic example is nat -> nat = nat -> bool which is a sound (definitional) equation (it's true in the cardinal model, for instance), which lets you type (fun x => 0) 0 : bool, but you need to prevent this from reducing by noticing that bool <> nat.

More frightening (and less known): congruence of application!! The issue here is more subtle, and depends of how exactly you set things up. But the idea is that the reasonable invariant for neutral comparison is to only assume that both sides are well-typed, but _not necessarily at the same type_ (assuming they have the same type cannot be preserved recursively, because eg knowing f u = f' u' have the same type does not tell you f and f' do). Your post-condition will then assert the neutrals are defeq at a given type. Now if you again think about comparing f u = f' u', you assume both applications are well-typed, thus also f and f' are, recursively compare them, learn they are defeq at some (x : A) -> B. Now you want to know you can compare u to u'. But these are normal forms, so now you must provide a type at which to do that comparison. Surely enough, A should do? Well now you have to establish u' : A knowing only f' u' is well-typed and f' : (x : A) -> B. Without some sort of Pi injectivity (+ maybe an argument on uniqueness of types which typically follows from it), you're toast.

@ncf This sort of subtle argumentation is really all over the place when you seriously try to verify things and have to think hard about invariants. And it's really easy to do something that relies on some inversion principle without realising.

I mentioned it in another thread, but the one example I know which grapples seriously with this is the implementation of Andromeda 2, and particularly the conversion-checking algorithm described in Anja Petković Komel's PhD. This works on rather generic theories, only relying on simple properties that one can prove generically (things like weakening or presupposition/boundary lemmas).

The ingredients are : heavily annotated syntax (essentially GAT) but, more importantly, _actually constantly checking the defeq of these annotations_ which cannot be taken for granted. The two issues of the previous toot dissolve if you have fully annotated abstraction and application nodes and you check that the types on the application node coincide with those on the abstraction node, or that the type annotations on both application nodes coincide.

@ncf @jonmsterling @AndrasKovacs @mevenlennonbertrand
I'm doing something that seems very similar in a normalization proof that I am working on: some parts of the normalization model depends on the injectivity of Π. As a way around this, it is possible to add new neutral terms that correspond to "computations blocked due to the lack of injectivity".

The new neutral constructors look like this:
castΠΠ : (p : Π A₁ B₁ ＝ Π A₂ B₂) ∧ ¬ (nf(A₁) = nf(A₂) ∧ nf(B₁) = nf(B₂)) → Nf (Π A₁ B₁) f → Ne (Π A₂ B₂) f
(the second occurrence of f is transported over p)
(this is simplified, the negative condition is actually described using a frontier of instability)

(There are similar constructors for "computations blocked due to the lack of disjointness").