termination_by regression

Stream: lean4

[Sky Wilshaw]

The following code fails to compile on latest Lean 4 with no imports:

def Recursive : Nat → Type
  | α => ∀ β : Nat, β < α → Recursive β
termination_by Recursive x => x

The error is:

MathlibLatest.lean:3:25
too many variable names

MathlibLatest.lean:3:0
Too many extra parameters bound; the function definition only has 1 extra parameters.

This code worked on previous versions.

[Sky Wilshaw]

In fact, even this fails (with the same message):

def Recursive : Nat → Type
  | α => Recursive 0
termination_by Recursive x => x

[Sky Wilshaw]

(Of course, this example is supposed to fail, but this is failing for the wrong reason.)

[Jannis Limperg]

You shouldn't write the function name (Recursive) any more in termination_by clauses. See the Lean release notes. This works:

def Recursive : Nat → Type
  | α => ∀ β : Nat, β < α → Recursive β
termination_by x => x

(The error message is questionable though.)

[Sky Wilshaw]

Ah, I see. Thanks for letting me know!

[Kim Morrison]

@Joachim Breitner, what would you think of adding a special test to check if the first "parameter" is actually the definition name, and then print a more helpful error message?

[Joachim Breitner]

It's plausible. I didn't do it because I was unsure how often it will be useful, but it might well be worth it. It won't (easily) catch the common termination_by _ => case, though.

[Jannis Limperg]

I would suggest an error message like "termination_by: <x> parameters bound, but <fun> only has <y> parameters", with the squiggly line below the first extraneous parameter. Also, there is currently an additional message "too many variable names"; I guess that's an oversight.

[Joachim Breitner]

Oh, yeah, that's a bit silly to print it twice. Sloppy programming on my side (I think I assumed the longer error would prevent the shorter from even be reached). I'll have a look.

[Joachim Breitner]

https://github.com/leanprover/lean4/pull/3255 should improve matters. Thanks for the nudge.

[Joachim Breitner]

@Scott Morrison , what is the workflow to get something backported onto the v4.6 release branch? Just ping you after I merged this? Cherry-pick and push? Cherry-pick and open PR?

[Jannis Limperg]

Thank you! :tada:

[Kim Morrison]

@Joachim Breitner there is a releases/v4.6.0 branch that you can cherry-pick onto. (Ping me so I know it is happening, but I don't think it requires a PR.)

[Joachim Breitner]

@Scott Morrison please consider yourself pinged; I just pushed.