Infinite loops in the elaborator

[Vtec234]

It has been noted by Abel and Coquand in a recent preprint that Lean's type theory allows looping proof terms. See also here for more discussion. It is unclear what effect this has on typechecking, but in principle it shouldn't matter -- the only terms that we can get to loop are proofs, i.e. have types in Prop. Proof irrelevance states that any two proofs of the same proposition are definitionally equal, so there should be no need to reduce any proof terms in order to check them for equality, since the proof-irrelevance rule always applies.

Sadly, the elaborator does not always deal with this properly and fixing that is the actual target of this issue. In current Lean (537f489), the following bit of code goes into an infinite loop in the elaborator:

def top := ∀ p : Prop, p → p
def pext := ∀ (A B : Prop), A → B → A = B
def supercast (h : pext) (A B : Prop) (a : A) (b : B) : B
  := @cast A B (h A B a b) a
def omega : pext → top :=
  λ h A a, supercast h (top → top) A
    (λ z: top, z (top → top) (λ x, x) z) a
def Omega : pext → top :=
  λ h, omega h (top → top) (λ x, x) (omega h)
def Omega' : pext → top := λ h, (λ p x, x)

theorem loopy : Omega = Omega' := rfl -- loops

A naive solution to this which seems not to break other aspects of elaboration is to add a proof-irrelevant (is_def_eq_proof_irrel) equality check before delta-reduction in type_context::is_def_eq_core_core. This prevents definitions from being unfolded in proofs and stops the elaborator loop in the above code, but a fully unfolded term:

theorem loopy : (λ h, (λ h A a, (λ (h': (∀ (A B : Prop), A → B → A = B)) T U t u, (λ α β (h: α = β) (a: α), (eq.rec a h: β)) T U (h' T U t u) t) h ((∀ p : Prop, p → p) → (∀ p : Prop, p → p)) A (λ z: (∀ p : Prop, p → p), z ((∀ p : Prop, p → p) → (∀ p : Prop, p → p)) (λ x, x) z) a) h ((∀ p : Prop, p → p) → (∀ p : Prop, p → p)) (λ x, x) ((λ h A a, (λ (h': (∀ (A B : Prop), A → B → A = B)) T U t u, (λ α β (h: α = β) (a: α), (eq.rec a h: β)) T U (h' T U t u) t) h ((∀ p : Prop, p → p) → (∀ p : Prop, p → p)) A (λ z: (∀ p : Prop, p → p), z ((∀ p : Prop, p → p) → (∀ p : Prop, p → p)) (λ x, x) z) a) h)) = (λ h, (λ p x, x)) := rfl

still gets stuck repeatedly calling type_checker::infer_type_core. At the moment I am unsure how to fix the latter. There is also the question of whether we want to fix it, i.e. prevent the elaborator from reducing proofs, in the first place -- as Mario mentioned, perhaps Turing-complete computation can be useful in proofs.

[cipher1024]

This is an interesting shortcoming to document. Unless it stops progress on actual projects, I wouldn't delve into changing the way the elaborator works. If you do find a fix, I'll be happy to consider it. You should make sure it doesn't break mathlib and check the difference in build time of mathlib when applying the fix.