Differing behavior on clashing binders

[dselsam]

This works in Lean3:

theorem foo : ∀ {x : Type}, Type := λ (x : Type), x

But this fails in Lean4:

theorem foo : ∀ {x : Type}, Type := λ (x : Type) => x
/-
error: type mismatch
  fun (x : Type) => x
has type
  Type → Type
but is expected to have type
  Type
-/

This is annoying, because the delaborator will print simple Lean3 proof terms that cannot be re-elaborated. The workaround is to manually add the curly braces:

theorem foo : ∀ {x : Type}, Type := λ {x : Type} => x

[digama0]

Another workaround is to use @, which seems to work here to mediate a difference in binder type:

theorem foo : ∀ {x : Type}, Type := @λ (x : Type) => x

[digama0]

Interestingly, that proof is delaborated to a term that doesn't typecheck:

#print foo
-- theorem foo : {x : Type} → Type :=
-- fun (x : Type) => x

So I think this can be classed as a delaborator bug.

[dselsam]

Yes, there is a disagreement between the elaborator and the delaborator. FYI here was my original example:

-- lean3
import ring_theory.nullstellensatz
#print mv_polynomial.zero_locus_anti_mono
/- 
theorem mv_polynomial.zero_locus_anti_mono : ... :=
λ ... (x : σ → k)
(hx : x ∈ mv_polynomial.zero_locus J) (p : mv_polynomial σ k) (hp : p ∈ I), hx p (h hp)
-/

Here the (x : σ → k) binder seems to be explicit in Lean3, and so (after auto-porting) the Lean4 delaborator is perhaps right to print it as explicit. But then it will not re-elaborate in Lean4 because of the issue I mentioned above.

[digama0]

The problem is that the expected type has an implicit forall and it's being provided an explicit lambda, which was okay in lean 3 and is not okay in lean 4. This would be a huge problem if they were literally (i.e. in the kernel) distinct types that were not defeq, but they are not; lean 4 will accept a difference in binders between the expected type and the provided term if you use @ before the lambda, just as I showed in my previous post.

So I think what lean 4 needs to do here is detect when the provided lambda sequence has different implicitness (or otherwise incompatible implicitness) with the expected type, and stick a @ in front of the lambda in that case so that it can be re-parsed. That is, in my example it should do this:

theorem foo : ∀ {x : Type}, Type := @λ (x : Type) => x

#print foo
-- theorem foo : {x : Type} → Type :=
-- @fun (x : Type) => x

Another possibility is to change the implicitness of the function to match the expected type:

theorem foo : ∀ {x : Type}, Type := @λ (x : Type) => x

#print foo
-- theorem foo : {x : Type} → Type :=
-- fun {x : Type} => x

but I'm not sure whether that approach is always an option.

[leodemoura]

Yes, this is a delaborator issue.