Conclusion
The type-inference algorithm described here is not useful. BCI-nf terms are a very small and weak set of lambda-terms. However, it is somewhat unusual, and the idea that, in some sense, lambda-terms are "the same shape as" their types is interesting.