Branch: refined app typing

to-revisit/refined-app-typing

I implemented a refined App typing rule that checks if the LHS's type is already know to be a function, in order to directly constrain the argument and reuse the result type in this case. I even handle the case where the LHS is a splittable polymorphic function that can be distributed.

The idea was that it would allow avoiding the creation of "function result" type variables, which always seems like a win. The specific case I was looking at was how def Nil = Nil{} stupidly inferred type forall 'a {'a :> #Nil}. 'a, which led to pointless constraint handling in the presence of FCP.

Surprisingly, this didn't seem to lead to any significant improvements in the test suite. In fact, it led to a number of regressions in the simplicity of inferred recursive types! This is apparently because typing applications this way makes the types a bit less regular (the types at the top (term) level will look a bit simpler), which leads to knots being tied later...