SuchThat is a purely generic programming language under active development. Focusing on type checking issues of generic programming we explain the requirements of a type system for a generic language and give a rationale for the SuchThat type system. We illustrate the challenge of type checking parameterized and attributed structures with examples from computer algebra, and present the implication calculus as a formalism that models well the instantiation of generic algorithms.