Order of constructor argument swapped

[ywata]

Prerequisites

• [X] 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

Mario investigated and minimized my example. I only report minimized example here.

Steps to Reproduce

1. Put the following code snippets in your lean4 enabled editor. The editor will show strange result on check command. Arguments of constructor are swapped.

inductive Foo : Nat -> Type  where
| mk (a b : Nat) : Foo a -> Foo b

#check @Foo.mk
-- Foo.mk : (b a : Nat) → Foo a → Foo b
example : (a b : Nat) → Foo a → Foo b := @Foo.mk -- fail

Expected behavior: The check command shows something like below:

Foo.mk : (a b : Nat) -> Foo a -> Foo b

Actual behavior: The check command actually shows

Foo.mk : (b a : Nat) -> Foo a -> Foo b

Note that arguments are swapped.

Reproduces how often: It always gives the same result

Versions

Lean (version 4.0.0-nightly-2022-05-14, commit 4934104eaf87, Release) Mac OS 10.15.7

[ammkrn]

Another small test case; this also seems to be triggered by dependent arguments:

def natToType : Nat → Type
| 0 => Unit
| _ => Bool

inductive Foo : Nat → Char → Prop
| mk (n : Nat) (elem : natToType n) (c : Char) : Foo n c

/-
constructor Foo.mk : ∀ (n : ℕ) (c : Char), natToType n → Foo n c
-/
#print Foo.mk

[leodemoura]

Thanks for posting the two examples. Lean 4 tries to reorder arguments when trying to transform inductive datatype indices into parameters. For example, in the second example, both indices are converted into indices.

#print Foo
-- it will say that `Foo` has 2 parameters

I can see this reordering feels unexpected. I will experiment and try to improve. For example, we can try to reorder only auto implicit parameters.