This is needed for nice kind/type checking error messages. In some cases the type checker knows the exact type that an expression has to have for type checking to succeed (see any of checkTypeM functions and its usages), which is what ExpectedExact is suitable for. In other cases the type checker only cares about the shape of the inferred type, e.g. the type checker knows that the type of a function has to be dom -> cod for type checking to succeed, but it doesn't yet care what dom and cod exactly are. Which is what ExpectedShape is useful for as it allows one to specify the shape of an expected type with some existential variables in it when it's impossible to provide an exact type.

We cannot do a correct translation to or from de Bruijn indices if the program is not well-scoped. So we throw an error in such a case.