Termination proofs and default parameters

Stream: lean4

[Frédéric Dupuis]

In the following function, I'm getting a strange error about the proof of termination:

def pack (disk : Array (Option Nat)) (i := 0) (j := disk.size - 1) : Array (Option Nat) :=
  if j ≤ i then disk
  else
    match disk[i]!, disk[j]! with
    | none, none => pack disk i (j-1)
    | none, some id₂ =>
        let newdisk := (disk.set! i (some id₂)).set! j none
        pack newdisk (i+1) (j-1)
    | some _, none => pack disk (i+1) (j-1)
    | some _, some _ => pack disk (i+1) j
termination_by j - i

The error I get is

The termination argument's type must not depend on the function's varying parameters, but Day09.pack's termination argument does:
  (disk : Array (Option Nat)) → optParam Nat 0 → optParam Nat (disk.size - 1) → optParam Nat (disk.size - 1)
Try using `sizeOf` explicitly

I'm not too sure what this means, but if I remove the default parameters for i and j, the error goes away. I'm guessing this has to do with the details of optParam somehow, but is this normal?

[Joachim Breitner]

This looks like it's fixable, probably lean needs to strip the default parameters from the type at the right point. Would you be so kind and open an issue at the lean repo?

[Frédéric Dupuis]

Done: lean4#6351