Failure of type inference in autoImplicit

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

def go (decls : Array Nat) (h : 0 < decls.size) : Bool := sorry
theorem go_foo (x : Nat) (decls : Array Nat) : go decls h = true := sorry

This code throws an error in the theorem statement of go_foo while trying to figure out the correct type for h:

application type mismatch
  go decls h
argument
  h
has type
  ?m.56 : Sort ?u.55
but is expected to have type
  0 < Array.size decls : Prop

which is rather surprising given that there are mvars on the one side and concrete values on the other side. The error can be fixed by changing the theorem statement as follows:

theorem go_foo' (x : Nat) (decls : Array Nat) h : go decls h = true := sorry

@nomeata conjectures that this is because autoImplicit variables are inserted at the beginning of the arguments list which makes it impossible to model the dependency on decl.

Context

In my practical code the statement behind h is large so I would like to avoid writing it out, while I can manage to do that with the mentioned workaround it would be nice if we had better UX here.

Expected behavior: If Joachim is right, either addressing this issue to allow for such autoImplicits or producing a more reasonable error for a user is probably the way to go.

Actual behavior: Confusing mvar error.

Versions

"4.7.0-rc2"

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start with the minimal Lean example in the issue and reproduce the autoImplicit elaboration failure in version 4.7.0-rc2. Investigate how autoImplicit variables are inserted and how dependent types are inferred; done means the example elaborates correctly or reports a more understandable error.