*** Case 1 (easy): we want to be able to write
[...]
*** Case 2 (easy):
Since these depend on HM-style generalization and our inference alg doesn't let us (yet) compute efficiently the set of "free" metavars, this is still not implemented. [ Aka: *too* easy. ]
*** Case 3: We could also allow
This one even less.
*** Case 4: now comes the tricky part.
[...]
*** Case 5: sinking deeper.
These should now work. I ended up doing it not in `let` but in the `lambda_->_` special form. So this should work even for cases where we need to pass an anonymous polymorphic function but want to just write "lambda x -> ..." and skip writing the additional "lambda t ≡> ... "wrappers.
K : (a : Type) ≡> a -> (b : Type) ≡> b -> a; K x y = x;
And yes, the new code also allows the above (tho currently, K is defined in pervasive.typer before we define multi-arg lambdas, so it can't be defined quite as above).
Stefan