When does dependent pattern-matching produce HEq?

Stream: general

[nrs]

In the code below, refining the match produces a HEq for the hypothesis p stating vec's equality with the pattern, and I'm trying to understand why. Does pattern-matching on indexed families always produce a HEq?

inductive Vect (α : Type) : Nat -> Type
| vnil : Vect α 0
| vcons : (a : α) -> Vect α n -> Vect α n.succ


structure Sig where
  symbol : Type
  arity : symbol -> Nat

example {σ : Sig} : (s : σ.symbol) -> (vec : Vect α (σ.arity s)) -> ∃ n : Nat, n = (σ.arity s) := fun s vec => match h : (σ.arity s), p : vec with
| .zero, .vnil => sorry
| _, .vcons a rest => by trace_state; sorry
/-
α : Type
σ : Sig
s : σ.symbol
vec : Vect α (σ.arity s)
n✝ : Nat
a : α
rest : Vect α n✝
h : σ.arity s = n✝.succ
p : HEq vec (vcons a rest)
⊢ ∃ n, n = n✝.succ
-/

[nrs]

Concretely this issue is showing up in the following proof, and I'm trying to avoid HEq as much as possible but I end up using it introduce Vect.Mem.head.

--Context for proof
inductive Vect.Mem : α -> Vect α n -> Prop
| head : (a : α) -> (vec : Vect α n) -> Vect.Mem a (.vcons a vec)
| tail : (b : α) -> Vect.Mem a as -> Vect.Mem a (.vcons b as)

inductive Vect.All : (α -> Prop) -> Vect α n -> Prop
| nil : Vect.All pred .vnil
| cons {p : α -> Prop} : p a -> All p vec -> All p (.vcons a vec)

inductive Ext (σ : Sig) (α : Type)
| mk : (s : σ.symbol) -> Vect α (σ.arity s) -> Ext σ α

abbrev Coalg (σ : Sig) (α : Type) := α -> Ext σ α

inductive isCoalgResultSubtermOf (a : α) (h : Coalg σ α) (x : α) : Prop
| intro : a ∈ (h x).2 -> isCoalgResultSubtermOf a h x

--Proof where I need to reason with HEq

theorem coalgResultsMembershipRelation : (h : Coalg σ α) -> h x = ⟨s, vec⟩ -> Vect.All (isCoalgResultSubtermOf · h x) vec := sorry

Ultimately, I'm trying to determine to what extent it is possible to completely avoid HEq, to be able to tell when it is absolutely necessary and when I can restructure my code to avoid it.

[Kyle Miller]

HEq appears when the types are not defeq

[nrs]

thank you for the answer, will be thinking about it