Support arbitrary generalization points

[jgbm]

The following is rejected by type inference:

import Ro.Base, Data.Tuple

foo' : Pi { 'a := forall a b c. (a -> b) -> Pair a c -> Pair b c, 'b := Unit }
foo' = (#'a := first, #'b := tt)

Confusingly, on the other hand, this is accepted:

foo : Pi { 'a := forall a b c. (a -> b) -> Pair a c -> Pair b c }
foo = #'a := first

The key difference is that the former expands to an application of append, and so the polymorphic type signatures doesn't get pushed down to the binding. On the other hand, in the latter, the polymorphic type signature does get pushed down, and so this lets type inference figure out that it should instantiate and regeneralize first.