equation compiler type mismatch

Stream: new members

[Horatiu Cheval]

I get the following type mismatch when I try this.

import tactic

inductive type
| ground : type
| arrow : type → type → type

@[reducible]
def context := list type

inductive term : context → type → Type
| var {ctx} {σ : type} : σ ∈ ctx → term ctx σ

set_option trace.eqn_compiler.elim_match false

open term

def subst : Π {ctx : context} {σ τ : type}, term (σ :: ctx) τ → term ctx σ → term ctx τ
| ctx σ τ (@var _ .(σ) _) s := s

equation compiler failed to create auxiliary declaration 'subst._main'
nested exception message:
type mismatch at application
  eq.rec (id_rhs (term ctx σ) ᾰ)
term
  id_rhs (term ctx σ) ᾰ
has type
  term ctx σ
but is expected to have type
  (λ (ᾰ : term (σ :: ctx) τ), term ctx τ) (var ᾰ_ᾰ)

[Horatiu Cheval]

On the other hand, when I look at

| ctx σ τ (@var _ .(σ) _) s := _

I get the state:

don't know how to synthesize placeholder
context:
subst : Π {ctx : context} {σ τ : type}, term (σ :: ctx) τ → term ctx σ → term ctx τ,
ctx : context,
τ : type,
_x : τ ∈ τ :: ctx,
s : term ctx τ
⊢ term ctx τ

which shows the type of s as being precisely the right type. So my question is, why is the mismatch happening here?