My original implementation is in Python and I documented a bit of research and implementation of type inference here: "The Blissful Elegance of Typing Joy" http://joypy.osdn.io/notebooks/Types.html The “Type Inference in Stack-Based Programming Languages” talk given by Rob Kleffner informed it. I don't recall now whether I read his thesis but it's likely. I probably couldn't wrap my head around it either.

For typing combinators (Joy's higher-order functions) I tried making a hybrid inferencer and interpreter that just evaluated them and it worked. (Incidentally that's what drove home to me the categorical nature of Joy. When I read Conal Elliott's "Compiling to Categories" I recognized what I had done.) In Joy the higher order combinators "don't care" if they are working on e.g. values or types. In other words they only care about the shape or structure (structural typing) of the data on the stack.

When I wrote the interpreter in Prolog and then wrote the inferencer in Prolog I noticed they were the same code, so I deleted one of them. In Prolog, you can pass a stack and compute values or pass logic variables and it will tell you what kind of stack a given expression expects/generates. If you implement math ops with CLP(FD) you get a nice constraint compiler that get generate new Prolog implementations of Joy expressions. Sick, eh?

In both Prolog and Python I haven't yet closed the loop for recursive combinators. Meaning the type inferencer generates the base-case and then the case for recurring once, then twice, and so on. I know the answer is some simple application of fixed-point theory or something, but I'm an idiot, and I've been working on other aspects (because I'm sure the solution is like decades old in the "compiling FP languages" literature. "Somebody else has had this problem.")

In any event, I don't think I'll have to figure it out, because I just found out that the next steps I was going to take have already been done by the "Seven Sketches" folks and then some: https://news.ycombinator.com/item?id=20376325

I'm pretty sure most of that stuff would make great Joy combinators. And something in there would be the way to deal with e.g. genrec and x combinators.