Match doesn't work when generating inductive via metaprogram

Stream: lean4

[Michael Jam]

I have this code:

import Lean.Elab.Command
open Lean Elab Command

elab "gen_structure" id:ident : command => do
  let level_u := mkLevelParam `u
  let type_u := mkSort <| mkLevelSucc level_u
  let decl := mkInductiveDeclEs [`u] 1 [{
    name := id.getId
    type := mkForall .anonymous .default type_u type_u
    ctors := [{
      name := id.getId ++ `mk
      type := mkForall `α .implicit type_u
        <| mkForall `x .default (mkBVar 0)
        <| mkApp (mkConst id.getId [level_u]) (mkBVar 1)
    }]
  }] false
  match (← getEnv).addAndCompile {} decl with
  | .error e => throwError (e.toMessageData {})
  | .ok env => setEnv env

-- inductive struct.{u} : Type u → Type u | mk : {α : Type u} → α → struct α
gen_structure struct
#print struct
#print struct.rec

def proj (s : struct α) : α :=
  match s with
  | struct.mk x => x

Where last line fails with this error message:

tactic 'cases' failed, not applicable to the given hypothesis

Why is that? How can I fix it?
It works if I give it the inductive directly (uncomment the inductive line and comment the gen_structure line).
Thanks for suggestions!

[Sebastian Ullrich]

Your type is missing the casesOn function defined for regular structures https://github.com/leanprover/lean4/blob/56cd6c1ff519d8be39f35875b5bf8719e6101c20/src/Lean/Elab/Structure.lean#L717