Given any well-typed term, produce its type.

TODO: at present this function may throw errors; in particular, whenever encountering a Case_ or Superpose_ which is either empty or where all the branches fail. This is considered a bug (since all well-typed terms should be able to produce their types), however it only arises on programs which are (at least partially) undefined or (where defined) are the zero measure, so fixing this is a low priority. When working to correct this bug, it is strongly discouraged to try correcting it by adding singletons to the Case_ and Superpose_ constructors; since doing so will cause a lot of code to break (and therefore is not a lightweight change), as well as greatly increasing the memory cost for storing ASTs. It would be much better to consider whole programs as being something more than just the AST, thus when trying to get the type of subterms (which should be the only time we ever call this function) we should have access to some sort of context, or intern-table for type singletons, or whatever else makes something a whole program.

N.B., this is a bit of a hack in order to avoid using SingI or needing to memoize the types of everything. You should really avoid using this function if at all possible since it's very expensive.

This is the core of the Term-algebra for computing typeOf. It is exported because it is useful for constructing other Term-algebras for use with paraABT; namely, for callers who need singletons for every subterm while converting an ABT to something else (e.g., pretty printing).

The r type is whatever it is you're building up via paraABT. The first argument to getTermSing gives some way of projecting a singleton out of r (to avoid the need to map that projection over the term before calling getTermSing). You can then use the resulting singleton for constructing the overall r to be returned.

If this function returns Left, this is considered an error (see the description of typeOf). We pose things in this form (rather than throwing the error immediately) because it enables us to automatically recover from certain error situations.