Partial type annotation

Stream: lean4

[Youngju Song]

I found that partial type annotation in usual places work (e.g., inside function body or inside #check):

def foo: Nat → Nat := id
#check foo
#check (foo: _ → _)
#check (foo: Nat → _)
#check (foo: _ → Nat)

but it is not allowed for function definition:

-- def bar := foo -- works
-- def bar: _ → _ := foo -- does not work
-- def bar: Nat → _ := foo -- does not work
-- def bar: _ → Nat := foo -- does not work

I agree that enforcing full explicit types for function signatures has benefit for readability (iirc Scala also did?), but in my experience it sometimes is convenient to partially annotate types and rely on type inference for the rest. Lean already allows fully omitting types (the first definition checks), but partially omitting types seems to be disabled in function definitions. I am curious if this is an intended feature / if there is some flag to control this.

[Eric Wieser]

I've also found myself wanting a flag to control this

[Eric Wieser]

Or even to demote it to a linter that emits a warning rather than an immediate error

[Eric Wieser]

It's helpful to be able to write

def foo : MetaM _ := do
  let x := 1

and start writing some code before I've decided on the return type

[Eric Wieser]

I can of course work around this with

def foo := show MetaM _  from do
  let x := 1

[Kim Morrison]

I'd personally agree this should be a warning not an error. However there may be a bad interaction with parallel elaboration, and we don't want to add any complication there right now.

[Youngju Song]

@Eric Wieser @Kim Morrison Thank you for the comments! Thank you for letting me know about the "show" keyword - I think I can live with it right now. Hope this could be relaxed sometime in the future :)

[Eric Wieser]

Thanks for making me think about this annoyance hard enough to make me realize that show does the trick!