This is the part where my knowledge of type systems falls down, and where I'd go dig out my copy of Pierce's Types and Programming Languages if I knew which box it was in, because I know Pierce gets into the decidability of the simply typed lambda calculus and what you can do with it, but I don't remember much of that chapter. It's one of those books I need to read five or six times before I really understand it.