Alternative version of #2263 .

This modifies the desugaring for the cdot parser to apply eta-reduction to the resulting term if possible. So (· + ·) elaborates to HAdd.hAdd instead of fun x y => HAdd.hAdd x y.

This is complicated by the fact that metavariables generally capture all variables in scope, meaning that (· + ·) of unknown type elaborates to something like fun x y => @HAdd.hAdd (?m1 x y) (?m2 x y) x y, which is not an eta redex. To reliably eta reduce the expression, we introduce a new SyntheticMVarKind, similar to how coercions are handled. This is simpler (less code) and a bit more robust than #2263, but there are relatively few SyntheticMVarKinds so this might be considered a more disruptive change than simply adding another auxiliary term elaborator.