The thing to notice here is that your function sum is defined on lists, which are inductively defined. Theoretically, the inductive definition of a list defines for every type T a term
match_list :: T -> (a -> [a] -> T) -> ([a] -> T)
satisfying the property
match_list s t  = s
match_list s t (x::xs) = (t x xs)
in addition, defining a ...