Consider internal usage of Resugarable Syntax principles for sugars

[eternaleye]

Justin Pombrio's thesis (PDF) on Resugarable Syntax has a number of desirable properties, from the perspective of a language designer using it as a tool without exposing its power to the user:

• The resulting sugars are
  • hygenic
  • type-safe
  • scope-safe
• The definitions of the sugars are separated from the language core
• User errors are reported in terms of the surface syntax, not the core

Chapter 6, Resugaring Types, defines the form of resugarable syntax with the strongest safety properties, and would seem to be a good fit; it'd enable the lambda syntax sugar to have a better story around errors, and also likely make it easier to implement arity shorthands. It'd also likely make adding other sugars, such as for Π types, Σ types, non-dependent pairs and sums, etc. easier.

I am intentionally not asking the further question of exposing such power to the user at this time :P