Previously, the first return statement found within a method or block was assumed to determine the return type of that method or block. There was no attempt to unify that type with the constraints provided by other return statements. Furthermore, return statements within conditionals were not taken into account. Now, all the types of return statements (including those embedded in conditionals) are collected; type inference is the catamorphism of unification over constraint-gathering. That is, for differing types T and T', the closest type that allows both T and T' is chosen; this operation is folded over the gathered types, yielding the most specific return type possible for the given constraints. The unification rules are not very smart yet. This will need to improve. Furthermore, when unification is impossible, |error| is used. If this becomes a thing that can ever happen in real code (so far, it is not possible, since there is no instance in which a |VoidType| is inferred as a constraint), we will need to make type checking into its own phase with some sort of State Monad, perhaps, in order to provide context for the type error. I'm going to avoid this for now.
I had to change the architecture of the message expression AST. It's superior, in that message chains are now produced using the chainl1 combinator. There's a separate anamorphism in which left-factored message expressions (Receiver,[Message]) are built up into a recursive structure that allows different kinds of expressions (messages, invocations, binary operations) to be nested in any order.