The motive argument to False.rec is explicit but elaboration does not use a supplied positional argument as the motive

[kmill]

Description

One normally expects the motive argument for eliminators to be implicit, but for False.rec it is explicit. This interacts in a confusing way with the app eliminator since this explicit argument does not make use of the supplied positional arguments.

Context

This question has come up a couple times recently: Zulip discussion 1 and discussion 2

Steps to Reproduce

As one can see, the type of False.rec is

#check False.rec -- False.rec.{u} (motive : False → Sort u) (t : False) : motive t

It has an explicit argument for the motive.

However, using False.rec with an explicit motive throws an error:

def bar (h : False) : Nat := False.rec (fun _ => Nat) h
/-
application type mismatch
  False.rec ?m.29 fun x => Nat
argument
  fun x => Nat
has type
  ?m.31 → Type : Sort (max 2 ?u.30)
but is expected to have type
  False : Prop
-/

This is because it's being elaborated as an eliminator, which causes the elaborator to solve for the motive and ignore that it's a positional argument.

The expected behavior is for explicit arguments to be filled positionally from supplied arguments.

A workaround is to write @False.rec (fun _ => Nat) h instead to disable elaborating as an eliminator.

Versions

4.8.0-rc2

Discussion

These are some potential solutions:

1. Make sure that the motive argument for False.rec is implicit.
2. Make the ElabAsElim code check to see if the motive argument is explicit, and if it is, use a positional argument. Users can supply _ if it is meant to be solved for. If x : False, then x.rec on its own should be the same as False.rec _ x.

They are not mutually exclusive, and even if the first is implemented, the second could still be useful for user @[elab_as_elim] declarations.

Impact

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

[leodemoura]

@kmill Thanks. Let's go with option 2.

[faenuccio]

@leodemoura If you have time, can you explain briefly why this seems more reasonable to you?

[leodemoura]

@faenuccio This is an elaboration issue. False.rec is generated by the kernel. We should not modify the kernel to fix an elaboration issue.