Inference regression with destructuring let binding in do notation

[ia0]

This is a minimization from jxl-proofs. In particular this is not the output from Aeneas. This is a user-implementation of an external function. However, it uses the do notation which AFAICT has a custom elaborator in Aeneas, thus is an Aeneas issue.

import Aeneas

open Aeneas Aeneas.Std Result Error

def test (list : List Std.U8) : Result Nat := do
  let ⟨ b0, _ ⟩ ← Result.ofOption (list[0]?) panic
  Result.ok (b0 * 2)

New behavior

error: New.lean:5:46: analyzePat: unsupported anonymous-ctor pattern on type
  ?m.5

Aeneas version: 94fc4cc
Charon version: 5a501733 (0.1.223)

Old behavior

No error.

Aeneas version: 38d10a2
Charon version: a206b150 (0.1.183)