Coercion with polymorphic types

Stream: lean4

[Param Reddy]

From Functional programming in lean:

structure NonEmptyList (T : Type) : Type where
  head : T
  tail : List T
  deriving Repr

instance : Coe (NonEmptyList T) (List T) where
  coe
    | { head := x, tail := xs } => x :: xs

def idahoSpiders : NonEmptyList String := {
  head := "Banded Garden Spider",
  tail := [
    "Long-legged Sac Spider",
    "Wolf Spider",
    "Hobo Spider",
    "Cat-faced Spider"
  ]
}

#eval List.reverse idahoSpiders
#eval List.reverse (α := String) idahoSpiders

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

def nel1 : NonEmptyList Nat := [1, 2, 3]
def l1 := [1, 2, 3]
def nel2 : NonEmptyList Nat := l1

I get error for #eval List.reverse idahoSpiders where I did not apply α to be String to Polymorphic List.reverse.

application type mismatch
  List.reverse idahoSpiders
argument
  idahoSpiders
has type
  NonEmptyList String : Type
but is expected to have type
  List ?m.10443 : Type

Error goes away when I let lean know that (α := String). I am guessing coercion and unification happen in different phases? Or coersion happens only on fully qualified types? Can someone more familiar with the steps lean takes in type inference/coercion search throw more light on this?

This also makes statement This allows non-empty lists to be used with the entire List API. not as nice to work with as now i need to keep instantiating polymorphic APIs before coercion helps. Something I am missing which makes usage simpler?

Also in dependent coercion, def nel1 : NonEmptyList Nat := [1, 2, 3] works, but not def nel2 : NonEmptyList Nat := l1. I am guessing somehow the list value [1, 2, 3] is helping identify that dependent coercion can be used, but cant really figure out how and why?

[Matthew Fisher]

Hey! I just ran into the same dependent coercion that you found with nel1, l1 and nel2. I'm sure hoping someone can explain what is going on. That List.reverse example you found is bothersome too, and I'm curious about that one now as well.