Inconsistent type inference

[lovettchris]

Prerequisites

• [x] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

This function:

def foo (a : Nat) (b)  := a + b

resolves to foo : Nat → Nat → Nat

But this one does not:

def foo (a : Nat) (b) : Nat := a + b

saying failed to infer binder type when the resulting type of a declaration is explicitly provided, all holes (e.g.,_) in the header are resolved before the declaration body is processed

Steps to Reproduce

See above.

Expected behavior: [What you expect to happen]

Actual behavior: [What actually happens]

Reproduces how often: [What percentage of the time does it reproduce?]

Versions

Lean (version 4.0.0-nightly-2022-09-12, commit ec2372e8d4ca, Release)

Additional Information

Any additional information, configuration or data that might be necessary to reproduce the issue.

[digama0]

This is expected behavior. When you use def foo (args) : ty := val, the type of the definition (args) -> ty is elaborated without looking at val (to prevent issues where changes in val cause nonlocal breakage), while the def foo (args) := val form infers the type of val and uses it for the definition type.

[lovettchris]

As a user though the result still feels inconsistent and broken. Why can't it fall back on val if the former fails?

[digama0]

It's a deliberate design decision in order to make the type predictable. There were many issues with subtle things like universes getting unified based on something in the definition body, and the compromise here is that you can have type inference if you leave off the : ty entirely, but if you provide it then the type should stand on its own.

If you want type inference without leaving off the expected type completely, you can use def foo (args) := show ty from val instead of def foo (args) : ty := val.

[lovettchris]

You are giving me lots of deep insights into why it is, but you must admit that when you try these two samples side by side, the first less specified one works and the second more specified one doesn't, it seems pretty silly.

def foo (a : Nat) (b)  := a + b
def foo (a : Nat) (b) : Nat := a + b

So far your answer seems to be "it is too hard to fix". Well, perhaps we should try harder because inconsistencies like this in any language will drive a user crazy.

[digama0]

No, my answer is not "it's too hard to fix" but "it's working exactly the way it's supposed to, we used to have the other behavior and it was worse". Perhaps we should improve the error message (which does attempt to explain this), or link to a relevant section of the documentation which explains why this behavior exists.

[digama0]

See #331

[lovettchris]

Thanks for the link to #331, that indeed looks like an interesting variation on the same issue. Mine doesn't involve "underscore holes". At least Leo is making def and theorem consistent, but I still feel like this is a bug and will continue to confuse people moving forwards and it's not just me, JasonGross felt the same way. At a minimum it will need detailed coverage in the reference manual, and an FAQ.

[leodemoura]

I still feel like this is a bug and will continue to confuse people moving forwards and it's not just me, JasonGross felt the same way. At a minimum it will need detailed coverage in the reference manual, and an FAQ.

No, this is not a bug. I agree with @digama0, we should improve the error message, and add a link from the error message to the relevant section of the documentation.