Add support for type-checking declarations

[jespercockx]

Currently the type-checker can only type-check a single term, but eventually we would like to check whole declarations.

• For definitions, this boils down to checking the type signature + the body.
• For data types, this means checking the telescopes of parameters and indices, checking the telescope of arguments of each constructor, and checking that the indices are well-typed.