Codegen can't support recursor

Stream: mathlib4

[Lars Ericson]

This works in Lean 3:

def quaternion_group_zero_equiv_dihedral_group_zero : quaternion_group 0 ≃* dihedral_group 0 :=
{ to_fun := λ i, quaternion_group.rec_on i dihedral_group.r dihedral_group.sr,
  inv_fun := λ i, match i with
                | (dihedral_group.r j) := a j
                | (dihedral_group.sr j) := xa j
                end,
  left_inv := by rintro (k | k); refl,
  right_inv := by rintro (k | k); refl,
  map_mul' := by { rintros (k | k) (l | l); { dsimp, simp, }, } }

For this mathport produces

def quaternionGroupZeroEquivDihedralGroupZero : QuaternionGroup 0 ≃* DihedralGroup 0 where
  toFun i := QuaternionGroup.recOn i DihedralGroup.r DihedralGroup.sr
  invFun i :=
    match i with
    | DihedralGroup.r j => a j
    | DihedralGroup.sr j => xa j
  left_inv := by rintro (k | k) <;> rfl
  right_inv := by rintro (k | k) <;> rfl
  map_mul' := by
    rintro (k | k) (l | l) <;>
      · dsimp
        simp

To which Lean Infoview responds

code generator does not support recursor 'QuaternionGroup.recOn' yet,
consider using 'match ... with' and/or structural recursion.

for the toFun so I should do something syntactically similar to the invFun, right?

Note that .recOn is used in 146 fully ported files so I don't know why it is rejecting it in this case.

[Mario Carneiro]

It seems !4#4097 is still awaiting-review, it will fix all problems of this form

[Mario Carneiro]

if you want a quick patch, put noncomputable on the def and leave a porting note

[Adam Topaz]

You can also use the equation compiler directly in this case (I think)

[Damiano Testa]

It seems that this file is already being ported: !4#4448.

[Eric Wieser]

I thought this was supposed to be fixed, but I still get this error with:

import Mathlib

-- warning: already compiled List.rec
compile_inductive% List

-- code generator does not support recursor 'List.rec'
def List.chooseX' (p : _ → Prop) : ∀ l : List α, ∀ _ : ∃ a, a ∈ l ∧ p a, { a // a ∈ l ∧ p a } := by
  intro l hp
  induction l with
  | nil => exact False.elim (Exists.elim hp fun a h => not_mem_nil a h.left)
  | cons l ls ih =>
    if pl : p l then
      exact ⟨l, ⟨mem_cons.mpr <| Or.inl rfl, pl⟩⟩
    else
      let ⟨a, ⟨a_mem_ls, pa⟩⟩ :=
        ih
          (hp.imp fun _ ⟨o, h₂⟩ => ⟨(mem_cons.mp o).resolve_left fun e => pl <| e ▸ h₂, h₂⟩)
      exact ⟨a, ⟨mem_cons.mpr <| Or.inr a_mem_ls, pa⟩⟩

[Mario Carneiro]

The error message seems to be wrong, the actual problem is that p l is decided using Classical.propDecidable. Adding have : Decidable (p l) := sorry fixes the issue