The first code block is incorrect. Match patterns like that only work when all the parameters to be matched on come after the colon. For example, the code block is equivalent to

    def length (α : Type) : List α -> Nat
    | List.nil => Nat.zero
    | List.cons y ys => Nat.succ (length α ys)