Dependent elimination failed due to constructor not matched

[nomeata]

Consider this attempt at pattern matching on a redex in an intrinsically typed lambda calculus:

inductive Ty where
  | unit : Ty
  | arrow (t₁ t₂ : Ty) : Ty

def Env (n : Nat) := Fin n → Ty

@[reducible] def Env.add (Γ : Env n) (t : Ty) : Env (n + 1) :=
  Fin.cases t Γ

inductive Term : Env n → Ty → Type where
  | var (i : Fin n) : Term Γ (Γ i)
  | app (e₁ : Term Γ (.arrow t₁ t₂)) (e₂ : Term Γ t₁) : Term Γ t₂
  | lam (e : Term (Γ.add t₁) t₂) : Term Γ (.arrow t₁ t₂)

axiom Term.subst : Term (Γ.add t₁) t₂ → Term Γ t₁ → Term Γ t₂ 

/--
error: Tactic `cases` failed with a nested error:
Dependent elimination failed: Failed to solve equation
  t₁✝.arrow t✝ = Γ i✝
at case `var` after processing
  _, (app _ _ _ _ _ _)
the dependent pattern matcher can solve the following kinds of equations
- <var> = <term> and <term> = <var>
- <term> = <term> where the terms are definitionally equal
- <constructor> = <constructor>, examples: List.cons x xs = List.cons y ys, and List.cons x xs = List.nil
-/
#guard_msgs in
def Term.step : (e : Term Γ t) → Option (Term Γ t)
  | .var i => none
  | .app (.lam e₁) e₂ => some (e₁.subst e₂)
  | .app _ _ => none
  | .lam e => none

-- Minimized

/--
error: Tactic `cases` failed with a nested error:
Dependent elimination failed: Failed to solve equation
  t₁.arrow t₂ = Γ i✝
at case `Term.var` after processing
  _
the dependent pattern matcher can solve the following kinds of equations
- <var> = <term> and <term> = <var>
- <term> = <term> where the terms are definitionally equal
- <constructor> = <constructor>, examples: List.cons x xs = List.cons y ys, and List.cons x xs = List.nil
-/
#guard_msgs in
def getLamBody? : Term Γ (.arrow t₁ t₂) → Option (Term (Γ.add t₁) t₂)
    | .lam e' => some e'
    | _ => none

-- Workaround 1: Manual generalization
def getLamBody?' : Term Γ (.arrow t₁ t₂) → Option (Term (Γ.add t₁) t₂) := aux rfl
where
  aux {t} : (t = Ty.arrow t₁ t₂) → Term Γ t → Option (Term (Γ.add t₁) t₂)
    | h, .lam e' => Ty.noConfusion h fun h₁ h₂ => some (h₁ ▸ h₂ ▸ e')
    | _, _ => none

-- Non-Workaround 2: Boolean predicate (did not actually work)

@[reducible] def isLam : Term Γ t → Bool
  | .lam _ => true
  | _ => false

def getLamBody : (e : Term Γ (.arrow t₁ t₂)) → isLam e → Term (Γ.add t₁) t₂
  | .lam e, rfl => e

This during match compilation in the inner match, see the more minimal example getLamBody?.

It is a workaround to manually generalize the index. I was hoping that adding a reducible predicate that asserts we are in the case would help, but it doesn't.

I wonder if this should work: The pattern does not mention .var, so why is it trying to solve for it.

I’ll wager (but didn't check yet) that using sparse casesOn (#10823) might fix this issue – but accidentialy so, or for good reasons?

Also, should the “discriminant refinement procedure” auto-generalize the indices here, or is that out of scope?

Version

Lean 4.25.0-nightly-2025-10-21

[nomeata]

Another work-around is to simplify the return type of .var:

inductive Ty where
  | unit : Ty
  | arrow (t₁ t₂ : Ty) : Ty

def Env (n : Nat) := Fin n → Ty

@[reducible] def Env.add (Γ : Env n) (t : Ty) : Env (n + 1) :=
  Fin.cases t Γ

inductive Term : Env n → Ty → Type where
  | var (i : Fin n) (h : t = Γ i) : Term Γ t
  | app (e₁ : Term Γ (.arrow t₁ t₂)) (e₂ : Term Γ t₁) : Term Γ t₂
  | lam (e : Term (Γ.add t₁) t₂) : Term Γ (.arrow t₁ t₂)

def Term.subst : Term (Γ.add t₁) t₂ → Term Γ t₁ → Term Γ t₂  := sorry

def Term.step : (e : Term Γ t) → Option (Term Γ t)
  | .var i _ => none
  | .app (.lam e₁) e₂ => some (e₁.subst e₂)
  | .app _ _ => none
  | .lam e => none

This means however that really slick stuff like

def Ty.denote : Ty → Type
  | .unit => Unit
  | .arrow t₁ t₂ => Ty.denote t₁ → Ty.denote t₂

def Term.denote (ctx : ∀ i, Ty.denote (Γ i)) : Term Γ t → t.denote
  | .var i     => ctx i
  | .app e₁ e₂ => e₁.denote ctx (e₂.denote ctx)
  | .lam e     => fun a => e.denote (Fin.cases a ctx)

now needs an explicit cast

def Ty.denote : Ty → Type
  | .unit => Unit
  | .arrow t₁ t₂ => Ty.denote t₁ → Ty.denote t₂

def Term.denote (ctx : ∀ i, Ty.denote (Γ i)) : Term Γ t → t.denote
  | .var i h   => h ▸ ctx i
  | .app e₁ e₂ => e₁.denote ctx (e₂.denote ctx)
  | .lam e     => fun a => e.denote (Fin.cases a ctx)

[JasonGross]

The way Rocq handles this is with the "small inversions" trick. Assuming the equations are of the form "have = desired", we can make progress on " = " , by doing case analysis on the term and returning a unit type on constructors other than the given one. The solution is guaranteed to be unique in cases where all arguments to the constructor are recursively either constructors or variables which do not appear in the term.

I believe we can also make progress on "<(co)inductive type family> = <(co)inductive type family>"

In Rocq, we would write

Definition getLamBody_opt (tm : Term Γ (arrow t₁ t₂) ) : option (Term (Γ.add t₁) t₂)
  := match tm in Term Γv tyv
        return option (match tyv with
           | arrow t₁v t₂v =>  (Term (Γ.add t₁v) t₂v)
           | _ => forall P : Prop, P -> P
           end) 
     with
     | lam e' => Some e'
     | _ => None
     end. 

[nomeata]

When you say “Rocq handles this”, do you mean that Rocq does some construction for the user here, or are you referring to the encoding with match … in Term (which seems to be a similar detour than the other workarounds)?

[nomeata]

I have some hope that #11104 might fix this.

[JasonGross]

Sorry, I missed the response.

If I am not mistaken, Rocq will automatically elaborate

Definition getLamBody_opt (tm : Term Γ (arrow t₁ t₂) ) : option (Term (Γ.add t₁) t₂)
  := match tm with
     | lam e' => Some e'
     | _ => None
     end.

to what I wrote above