Inconsistent type inference

Prerequisites

• 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.

Run the two self-contained declarations from the issue with Lean 4 version 4.0.0-nightly-2022-09-12 and compare their inferred types and diagnostics. Trace the type-inference path for implicit binder types when an explicit result type is present; done means the second declaration accepts the binder and infers the same type as the first, with regression coverage for both examples.