unsupported `.casesOn` application during code generation

Stream: new members

[An Qi Zhang]

Hello, after the Lean v22 update, lean has problems with definitions that use a structure that is a Prop. Lean throws an error stating there's an "unsupported ....casesOn application during code generation", for match/cases on SubTypes that use a structure : Prop to define the SubType.

Are there plans to fix this?

An MWE in Lean v4.22.0-rc3:

structure AType where
  n : Nat
  b : Bool

def AType.Big : AType → Prop
| a => a.n > 10 ∧ a.b
def AType.NotBig : AType → Prop
| a => a.n < 10 ∧ a.b

structure AType.NotTen (a : AType) : Prop where
  big : a.Big
  notBig : a.NotBig

def SpecificType : Type := {a : AType // a.NotTen}

-- Error: unsupported `AType.NotTen.casesOn` application during code generation
def SpecificType.toNat : SpecificType → Nat
| ⟨⟨n, true⟩,{big,notBig}⟩ => n

-- Error: unsupported `AType.NotTen.casesOn` application during code generation
def SpecificType.fn (s : SpecificType) : Nat :=
  match s with
  | ⟨⟨11, true⟩,_⟩ => 11
  | ⟨⟨n, true⟩,_⟩ => n

[Aaron Liu]

@Cameron Zwarich

[Cameron Zwarich]

I actually didn't realize that this was supported by the old compiler. I added this back in lean4#9411. Apologies for the inconvenience!