Turns out something is still very broken. I never fully grokked how the locally-nameless representation works and I've been pretty sloppy about type simplification. But the picture is slowly coming together.