Hey, this thread popped up as I was embarking on some travel, but now that I had a chance to read it, I just want to "+1" the solution you landed on! I'm not sure I liked the idea of a magic vs. literal equals in definitions (or is it 'cooked' vs. 'raw')? But having a 'λ' that adds extra 'Λ' as needed seems flexible and reasonable.
CL
Stefan Monnier monnier@IRO.UMontreal.CA writes:
*** 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
Typer mailing list Typer@iro.umontreal.ca https://webmail.iro.umontreal.ca/mailman/listinfo/typer