Unpacking Subtype leads to recursor error

[msprotz]

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

In the presence of Subtype and a destructuring let-binding, the recursor seems to be incorrectly synthesized before being sent off to the kernel.

def Option.attach {α: Type} (o : Option α): Option { x : α // o = .some x } :=
  match o with
  | .some x => .some ⟨x, rfl⟩
  | .none => .none

-- works
def g' (T : Type) (ls : List T) : (Option (List T)) :=
  match ls with
  | _::tl =>
      let res := Option.attach (g' T tl)
      res.bind fun x => x.val
  | [] => .none

-- doesn't
def g'' (T : Type) (ls : List T) : (Option (List T)) :=
  match ls with
  | _::tl =>
      let res := Option.attach (g'' T tl)
      res.bind fun ⟨x,h⟩ => x
  | [] => .none

Thanks to @JamesGallicchio and @digama0 for helping reproduce this error. Link to original Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/naming.20hypotheses.20when.20using.20do-notation/near/326891317 onwards

Versions

Lean (version 4.0.0-nightly-2023-01-29, commit 38a0d1e, Release) (OSX)

[leodemoura]

@nomeata I explored this issue a bit. The problem is the auxiliary match-declaration for fun ⟨x,h⟩ => x. We have an application of the form

 g''.match_1 g'' -- <<< This is the problematic occurrence
  T tl
  (fun (x : { x : List T // g'' T tl = some x }) => Option (List T)) x
  fun (x : List T) (h : g'' T tl = some x) => some x

When Lean generates the auxiliary match-declaration, it will abstract over free variables. g'' is one of them during elaboration :( Not sure what is the best fix here. The first hack that comes to mind: unfold this kind of match-declaration while checking for termination.

[nomeata]

One maybe bearable work-around is to let-abstract the recursive call:

-- doesn't
def g'' (T : Type) (ls : List T) : (Option (List T)) :=
  match ls with
  | _::tl =>
      let r := g'' T tl
      let res := Option.attach r
      res.bind fun ⟨x,h⟩ => x
  | [] => .none

I am not sure if it is possible or wise to try to do such a transformation automatically during elaboration.

I am facing a related problem when generating induction principles, and Lean.Meta.abstractNestedProofs abstracts over the g''. I wonder if there is a more sophisticated abstraction mechanism that, instead of abstracting over g'', T and tl separately, recognize that T and tl only appear tas arguments to g'' and then abstract over g'' T tl as a whole. But this can only work if the expression doesn’t depend on the precise value of g'' T tl, and that is probably not easy or check to recognize…

For reference, this is g''.match_1’s definition:

def g''.match_1.{u_1} : (g'' : (T : Type) → List T → Option (List T)) →
  (T : Type) →
    (tl : List T) →
      (motive : { x // g'' T tl = some x } → Sort u_1) →
        (x : { x // g'' T tl = some x }) →
          ((x : List T) → (h : g'' T tl = some x) → motive { val := x, property := h }) → motive x :=
fun g'' T tl motive x h_1 => Subtype.casesOn x fun val property => h_1 val property