> If I understand correctly, generics here are “type agnostic” functions in a strongly typed language?

They are not.

They are applicable to a well-defined range of sets of input types, instead of a single specific type combination, and produce a well-defined output type for each input type combination.

> It seems strange to put in so much effort for type checking then only to throw it overboard by implementing something that ignores type.

Generics do not ignore types. That's kind of the whole point.