Equation compiler failure: tactic cases failed, unexpected inductive datatype type

[timjb]

When checking

inductive some_dep_type : bool → Type
| lala : Π b, some_dep_type b

def some_function (b : bool) (p : some_dep_type b) : unit := ()

lemma some_function_congruence :
    Π {b₁ b₂ : bool}
      (p₁ : some_dep_type b₁) (p₂ : some_dep_type b₂)
      (eq : p₁ == p₂),
    some_function b₁ p₁ == some_function b₂ p₂
| b₁ ._ p₁ ._ (heq.refl ._) := heq.refl _

-- This definition works:

--| _ _ _ _ _ := heq.refl b

with Lean (current HEAD version 40bf75cbff89135489b8489ef694c2abd7006cf2), I get the error

equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
nested exception message:
tactic cases failed, unexpected inductive datatype type

[leodemoura]

Note that, eq : p₁ == p₂ implies some_dep_type b₁ = some_dep_type b₂. However, in Lean, some_dep_type b₁ = some_dep_type b₂ does not imply b₁ = b₂. The error message is bad, but the lemma is not provable. The following alternative one is

inductive some_dep_type : bool → Type
| lala : Π b, some_dep_type b

def some_function (b : bool) (p : some_dep_type b) : unit := ()

lemma some_function_congruence :
    Π {b₁ b₂ : bool}
      (p₁ : some_dep_type b₁) (p₂ : some_dep_type b₂)
      (h₁ : b₁ = b₂)
      (h₂ : p₁ == p₂), 
    some_function b₁ p₁ = some_function b₂ p₂
| b ._ p ._ rfl (heq.refl ._) := rfl

[timjb]

@leodemoura Thanks for the explanation! I see that for a general type family another_dep_type, another_dep_type b₁ = another_dep_type b₂ doesn't necessarily imply b₁ = b₂ since another_dep_type need not be injective. But intuitively, for dependent types like some_dep_type above, (p : some_dep_type b₁) == (q : some_dep_type b₂) → b₁ = b₂ feels like it should be provable by simultaneously pattern matching on p, q and the equality proof. I guess I'll have to adjust my intuition then.

[leodemoura]

See #1594