Constructor checking mode

[andrejbauer]

This PR implements the checking mode for arguments of TT formers.

Implementing it also shows how we need to fix the infer/checking algorithm. Traditionally, we have

• infer mode, which calculates the type of a term
• check mode, which checks that a term has a given type

Because we have four judgement forms, we shall instead have:

• infer mode, which calculates a judgement
• check mode, which checks that a judgement has the required boundary

So in fact there will be four possible ways to check against. Consequently, we need to introduce boundaries into the absract syntax, namely in the form of patterns on handlers.