More on Tail Merging

In an earlier post I speculated that factoring out Cat combinators other than Dup would just be a matter of copy-and-paste (I used the euphemism boilerplate back then). It came to me as a shocking revelation that the Ωmega interpreter did not agree. It asserted that

type _d is equated to type _e

which is inacceptable. The error message was not exactly like this, but very similar. It took me some time to understand it. First I wrote an even shorter function than the one-liner that caused the error. It only happened when I recombined the two shortened If legs (that is, after removing a Print from each).
This piqued my curiosity and I made an excursion into Ωmega's interactive typecheck mode, just to discover that the two If legs ended with different stack configurations!

This put me over the top, and I could come up with an example immediately:

If [Push 42, Print] [Push True, Print]

is a case where the Print cannot be removed without violating the invariant that the exit stack configurations at both If legs must be the same. In this case the yes-leg would have an Int at TOS and the no-leg a Bool. Since I have to cater for the general case, the removal of a Print is unsound. Ωmega discovered this.

There are two lessons to be learned from this incident, namely:

1. If you see a mysterious error (message), simply provoke the same with a smaller program, and
2. Ωmega's error messages need to be improved in a way that somehow the piece of code is indicated that gives rise to the erroneous types.

In the meantime I have an idea how to find a way to remove that Print anyway. The key is abstract interpretation of the two If legs, to construct a proof that the stacks have the same shape immediately before the Print. Given this proof the typechecker can be persuaded to allow the recombination of the shortened legs. But to implement this idea there are many more hours to be spent hacking. It will surely be worth blogging about.