why this code fails?

Stream: lean4

[Asei Inoue]

structure NonEmptyList (α : Type) : Type where
  head : α
  tail : List α

variable {α : Type}

instance {x : α} {xs : List α} : CoeDep (List α) (x :: xs) (NonEmptyList α) where
  coe := {head := x, tail := xs}


/-
application type mismatch
  [1, 2].head
argument
  [1, 2]
has type
  List Nat : Type
but is expected to have type
  NonEmptyList ?m.435 : Type
-/
#check NonEmptyList.head [1, 2]

[Floris van Doorn]

Look at the precise type of docs#List.head

[Floris van Doorn]

#check NonEmptyList.head ([1, 2] : NonEmptyList Nat) does work.

[Floris van Doorn]

Do does #check NonEmptyList.head (α := Nat) [1, 2]

[Floris van Doorn]

I expect that CoeDep instances only work if the exact expected type is known. In your case, you only know it's NonEmptyList _, not NonEmptyList Nat

[Floris van Doorn]

Note: I wrote my first message because the error message is confusing. The [1, 2].head in the error message looks like List.head [1, 2].
(lean4#4670)

[Asei Inoue]

@Floris van Doorn Thank you!!

#check NonEmptyList.head (α := Nat) [1, 2]

[Asei Inoue]

(deleted)