https://no-learns.neocities.org/2019/06/matching-in-types/

Abs.v

Class Signature := B_S { ops : Type ; consts : Type }.

Section Arith.
  Context {Sigma : Signature}.

  Inductive arith : Type :=
  | Op : ops -> arith -> arith -> arith
  | C : consts -> arith.

  Fixpoint eval (oint : ops -> nat -> nat -> nat) (cint : consts -> nat) e :=
    match e with
    | Op o e1 e2 => oint o (eval oint cint e1) (eval oint cint e2)
    | C c => cint c
    end.
End Arith.

(* Original code for comparison *)
Module Abs.

Definition sig_ext (Sigma : Signature) :=
  match Sigma with
    B_S ops consts => B_S ops (consts + True)
  end.

Fixpoint lift_arith {Sigma : Signature} (e : @arith Sigma) : @arith (sig_ext Sigma) :=
  (match Sigma with
    B_S os cs as Sig => fun e' : @arith Sig =>
      match e' with
      | Op o e1 e2 => @Op (sig_ext Sig) o (lift_arith e1) (lift_arith e2)
      | C c => @C (sig_ext Sig) (inl c)
      end
  end) e.

End Abs.

(* Use projections instead of outright pattern-matching on Sigma. *)
Module Proj.

Definition sig_ext (Sigma : Signature) :=
  B_S (@ops Sigma) (@consts Sigma + True).

(* This is the first, naive implementation of the post, now typechecks. *)
Fixpoint lift_arith {Sigma : Signature} (e : @arith Sigma) : @arith (sig_ext Sigma) :=
  match e with
  | Op o e1 e2 => @Op (sig_ext Sigma) o (lift_arith e1) (lift_arith e2)
  | C c => @C (sig_ext Sigma) (inl c)
  end.

End Proj.

(* The Primitive Projections extension makes it so that records can be
   accessed through projections first, rather than pattern-matching. Actually,
   the pattern-matching _syntax_ is still available, but it desugars to
   projections (which can be convenient, avoiding repetitive applications of
   projections to [Sigma]). What is no longer allowed is *dependent*
   pattern-matching, which could be argued to be, in a nonobvious way,
   the root of the problem. *)
Set Primitive Projections.

Module PProj.

Record Signature := B_S { ops : Type ; consts : Type }.

Section Arith.
  Context (Sigma : Signature).

  Inductive arith : Type :=
  | Op : ops Sigma -> arith -> arith -> arith
  | C : consts Sigma -> arith.

  Fixpoint eval (oint : ops Sigma -> nat -> nat -> nat) (cint : consts Sigma -> nat) e :=
    match e with
    | Op o e1 e2 => oint o (eval oint cint e1) (eval oint cint e2)
    | C c => cint c
    end.

End Arith.

Arguments Op {Sigma}.
Arguments C {Sigma}.

Definition sig_ext (Sigma : Signature) :=
  match Sigma with
    B_S ops consts => B_S ops (consts + True)
  end.

Fixpoint lift_arith {Sigma : Signature} (e : @arith Sigma) : @arith (sig_ext Sigma) :=
  match e with
  | Op o e1 e2 => @Op (sig_ext Sigma) o (lift_arith e1) (lift_arith e2)
  | C c => @C (sig_ext Sigma) (inl c)
  end.

End PProj.