[stack] Motivations to embrace undecidable type systems

One motivation for this work was to broaden the range of functions
which can be investigated by looking at their type, which can be
useful to see their effect. Another was to allow the programmer to
provide additional constraints. I also hoped that the type would form
a basis for proving properties of any function, using denotation
provided by the programmer. I did not want the type system to restrict
which functions or algorithms could be considered. We should be free
to get a function working empirically, then prove its correctness.

And another was to use inheritance polymorphism, mix in native objects
from Java or C# and type their interfaces, and investigate uniqueness
types in concatenative languages. Perhaps an undecidable type system
is not really necessary for this. But I wanted a type system for
experimental programs that might be rejected by conventional type
systems.

I do not expect that there is any automated (unguided) procedure to
check, for instance, whether two type formulas are equivalent in this
system. Is this what decidable type inference means?