Changing variable type and introducing new variables cannot be done in one command.

[adamtopaz]

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

The variable command is used in two different ways: a) to introduce new variables and b) to change the variable type (e.g. from explicit to implicit). In some situations, lean4 allows us to do both things using a single variable command, and in some cases this fails.

Steps to Reproduce

Example 1:

variable (α : Type _) [OfNat α (nat_lit 0)] 

variable {α} (x : α) (h : x = 0)

Example 2:

variable (α : Type _) [OfNat α (nat_lit 0)] 

variable {α} (x : α) 
variable (h : x = 0)

Example 3:

variable (α : Type _) [OfNat α (nat_lit 0)] 

variable {α} 
variable (x : α) (h : x = 0)

Expected behavior:

All three examples above should work with no error and result in equivalent behavior.

Actual behavior:

In example 1, we have an error at the 0 on the last line:

failed to synthesize instance
  OfNat α 0

Examples 2 and 3 work with no error.

Reproduces how often:

100%

Versions

Lean version:
Lean (version 4.0.0-nightly-2023-03-09, commit 0cc9d7a43de7, Release)

Tested on Linux nixos 5.15.94.

Additional Information

See associated zulip discussion.