autoParam is evaluated before arguments are applied

Stream: lean4

[Jakub Nowak]

I find this behaviour very strange. It caused problems here #general > choose and autoparams. Why Lean expands autoParam so eagerly, even before any argument was applied? Or is this a bug?

/--
error: could not synthesize default value for parameter 'x._@.test.2021293395._hygCtx._hyg.5' using tactics
---
error: `grind` failed
case grind
h : ∀ (k : Nat), True
k : Nat
⊢ False
[grind] Goal diagnostics
  [facts] Asserted facts
    [prop] ∀ (k : Nat), True
  [eqc] True propositions
    [prop] ∀ (k : Nat), True
---
error: unsolved goals
h : ∀ (k : Nat), autoParam (k < 0) _auto✝ → True
h' : ∀ (k : Nat), True
⊢ True
-/
#guard_msgs in
example (h : (k : Nat) → (_ : k < 0 := by grind) → True) : True := by
  have h' := h

/--
error: could not synthesize default value for parameter 'x._@.test.2021293396._hygCtx._hyg.7' using tactics
---
error: `grind` failed
case grind
h : ∀ (k k' : Nat), True
k k' : Nat
⊢ False
[grind] Goal diagnostics
  [facts] Asserted facts
    [prop] ∀ (k k' : Nat), True
  [eqc] True propositions
    [prop] ∀ (k k' : Nat), True
---
error: unsolved goals
h : ∀ (k k' : Nat), autoParam (k < 0) _auto✝ → True
h' : ∀ (k k' : Nat), True
⊢ True
-/
#guard_msgs in
example (h : (k : Nat) → (k' : Nat) → (_ : k < 0 := by grind) → True) : True := by
  have h' := h

-- this works
example (h : (k : Nat) → ⦃k' : Nat⦄ → (_ : k < 0 := by grind) → True) : True := by
  have h' := h

[Kyle Miller]

Currently both opt-params and auto-params are filled in eagerly. You should be able to write have h' := @h to suppress it.

I agree that it's a little weird for it to apply auto-params if the type depends on one of the regular parameters... Right now the way the logic works is that it elaborates h as fun k => h k (by grind), using an "eta argument" (by constructing this fun) to get to the auto-param.

I think this logic makes sense for opt-params, and for consistency it's nice if opt-params and auto-params have the same rule for when they apply. Maybe there's a case for having opt-params delay elaboration if they've got a dependency on a regular parameter, not sure. I'd guess almost all uses of opt-params have a type that depends on nothing, or at most on some implicit parameters. (If you think it's worth trying to change, I'd be very happy if someone analyzed opt-params across Lean, Batteries, Mathlib, and CSLib, to see if my guess is correct!)

[Jakub Nowak]

I think you might be correct about opt-params, but it's hard to imagine auto-param that doesn't have a dependency on arguments.

[Jakub Nowak]

One use case for evaluating eagerly could be this:

def foo (n m : Nat) (h : n ≤ m := by grind) := m + n
example := List.range 10 |>.map (foo 0)

Here, in the call foo 0, h : 0 ≤ m := by grind is instantiated before m. If it weren't, then it wouldn't have a correct type to pass to List.map.

[Jakub Nowak]

But I think that autoParam without all it's dependencies instantiated is likely to be unprovable in most cases.

[Jakub Nowak]

One thing we could do, is to look at the expected type of partial function application, and decide to instantiate autoParam if the expected type requires it. Otherwise, only instantiate autoParam if either all previous arguments were instantiated, or all dependant arguments were instantiated.

[Kyle Miller]

Jakub Nowak said:

I think you might be correct about opt-params, but it's hard to image auto-param that doesn't have a dependency on arguments.

Yeah, I left that part unsaid. The thought is (1) it would be confusing if opt-params and auto-params had different elaboration rules but (2) potentially we can change the rules for opt-params at the same time, if it does not affect anyone.

Looking at the expected type seems reasonable... but that also feels like an uneasy compromise. It's a big difference in elaboration between whether eta arguments are used or not used. Plus, auto-params are generally for proof arguments, so proof irrelevance means the expected type won't meaningfully depend on them. That said, sometimes people use them for supplying a default value that can't be elaborated ahead of time (e.g. (v : t := by exact default), if you don't want an [Inhabited t] instance in the type signature).

[Jakub Nowak]

By expected type, I really only meant to look at, whether the type can be a function or not. So you just instantiate the argument, if the expected type cannot be a function. In this example:

def foo (n m : Nat) (h : n ≤ m := by grind) := m + n
example := List.range 10 |>.map (foo 0)

The expected type of foo 0 is ?m.0 → ?m.1, while the type of foo 0 is (m : Nat) → (_ : 0 ≤ m := by grind) → Nat. Hm, I guess it's still hard, because the type checker would need to realize that ?m.1 cannot a function, but that's only because there's no instance of OfNat for function.

[Jakub Nowak]

If we choose an approach of instantiating optParam and autoParam as soon as all dependant arguments are instantiated, and your assumption that optParams are usually non-dependant, then optParams won't be affected in this usual cases.

[Jakub Nowak]

Maybe that could be a valid example of optParam that depends on the arguments?

def h {α : Type} [Inhabited α] (a : α := default) : Prop := sorry

/--
error: typeclass instance problem is stuck
  Inhabited ?m.3

Note: Lean will not try to resolve this typeclass instance problem because the type argument to `Inhabited` is a metavariable. This argument must be fully determined before Lean will try to resolve the typeclass.

Hint: Adding type annotations and supplying implicit arguments to functions can give Lean more information for typeclass resolution. For example, if you have a variable `x` that you intend to be a `Nat`, but Lean reports it as having an unresolved type like `?m`, replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck.
-/
#guard_msgs in
example : False := by
  have h' := h

But in this case you do only want to instantiate the optParam, after α and _ : Inhabited α are instantiated. Otherwise, you get the error above.

[Jakub Nowak]

Kyle Miller said:

(If you think it's worth trying to change, I'd be very happy if someone analyzed opt-params across Lean, Batteries, Mathlib, and CSLib, to see if my guess is correct!)

Do you think there's still a need to analyze this, with the proposal of only expanding opt-param/auto-param, when all other dependant arguments that the type of an param depends on are (syntactically) instantiated, and function term doesn't use @ to explicitly disable this?