Improve type checking of recursive lets with a mix of binding annotations - #6221

This PR contains some type checking tweaks to handle some cases that were previously errors. The simplest example is

f x = g x x
g : a -> b -> a
g x y = f x

The issue with this is that the inferred type of f will not be general enough to satisfy the supplied signature for g when they are checked as a single group. The new approach partitions definitions into those that require inference vs. those that require checking, and generalizes the former before checking the latter.

However, just that change wouldn't allow e.g.

f x = g x x
g : a -> b ->{IO} a
g x y = f x

because g was still not completely closed. It actually got expanded to forall a b. a ->{g} b ->{IO} a, where g requires inference, and can't be split out. To fix this, I made the function that inserts these ability inference variables aware of how many lambda-bound variables there are, because only the last variable can have a non-empty ability list. This means that the signature above gets immediately completed to forall a b. a ->{} b ->{IO} a, which is closed, and can be split out.

I tried detecting the error situation (which could still happen in general) in the error recognizer, to give a more specific error message. However, it actually doesn't seem easy to do so. I think the actual error that happens is an attempt to solve an out-of-order variable in the context, but trying to test for that didn't seem to work. So, this PR merely increases the number of programs we can check, and doesn't give a better indication of what's going on in the odd cases. Perhaps I can revisit the error message in the future.