CoeDep not unifying?

Stream: lean4

[Tom Kranz]

Why does the instance derivation mechanism not look inside idahoSpiders.tail to see that it is in fact a .consed list that can be unified with h :: t?

structure NonEmptyList (α : Type) : Type where
  head : α
  tail : List α deriving Repr
def idahoSpiders : NonEmptyList String := ⟨"Banded Garden Spider", ["Long-legged Sac Spider"]⟩
instance : CoeDep (List α) (h :: t) (NonEmptyList α) := ⟨⟨h, t⟩⟩
#eval (idahoSpiders.tail : NonEmptyList String)
/-
type mismatch
  idahoSpiders.tail
has type
  List String : Type
but is expected to have type
  NonEmptyList String : Type
-/

Even requesting the coercion very explicitly gives no dice.

set_option diagnostics true
#eval (CoeDep.coe idahoSpiders.tail : NonEmptyList String)
/-
failed to synthesize
  CoeDep (List String) idahoSpiders.tail (NonEmptyList String)
-/

At least giving a .consed list directly works. But is this really the extent of dependent coercions' utility?

#eval (["Long-legged Sac Spider"] : NonEmptyList String)
-- { head := "Long-legged Sac Spider", tail := [] }

[Edward van de Meent]

that is because of the transparency setting of idahoSpiders. if you make it an abbrev or mark it with @[reducible], instance search is allowed to unfold it and find that it indeed is a cons.