no synth rule for lambda

[ivoysey]

“why not have a synthesis rule for lambda that gives x the hole type and
synthesizes the type of the body?  What goes wrong?”

[ivoysey]

we said

This would be a valid extension of the calculus, but a more conventional
approach would be to introduce “half annotated” lambdas as described by
Chlipala et al. in their paper “Strict Bidirectional Type Checking” (TLDI
2005). We left these out for simplicity.```

[ivoysey]

related is this back-and-forth, where i think rev.D is a little unfamiliar with bidirectional systems

“lambdas are the only constructor in your theory with no synthesis rule
(even injections for sums have them)”

Correction: there is no type synthesis rule for injections. The synthetic
action rule for injections inserts an ascription, like the synthetic action
rule for lambdas.

[ivoysey]

there's some more extended commentary about this in the review text, too"

Section 2: Regarding the "construct lam x" action, at first I found it
rather annoying that introducing a lam also introduces an ascription, and
that lambda does not have a synthesis rule.  My best guess for this design
decision is that one should usually think of the lam and ascription
together as a single expression, rather than just marking the type of the
argument, but that in some contexts you can get away with not providing an
ascription because of the demands of the context (i.e. it's a syntactic
nicety to not provide a type for your lambda).  Is that the intent?
Otherwise lambdas are the only constructor in your theory with no synthesis
rule (even injections for sums have them).

[cyrus-]

I addressed this by saying "Type-annotated function definitions often arise as a single syntactic construct in full-scale languages like ML." I didn't explicitly talk about the alternative rule where \x.e synthesizes (||) -> (||) but that would fall out from a combined syntactic construct like that.