Thanks for the Simplicity reference, hadn't seen that yet. Seems like it builds on the implicit calculus [1], which applies more generally to any lambda calculus than in the Scala context.

[1] http://homepages.inf.ed.ac.uk/wadler/papers/implicits/implic...