This PR changes how generalized field notation ("dot notation") resolves the name of the function, adds a feature where terms such as `x.toString` can resolve as `toString x` as a last resort, and modifies the `Function` dot notation to always use the first explicit argument rather than the first function argument. The new rule is that if `x : S`, then `x.f` resolves the name `S.f` relative to the root namespace (hence it now responds to `export` and `open). Breaking change: aliases now resolve differently. Before, if `x : S`, and `S.f` is an alias for `S'.f`, then `x.f` would use `S'.f` and look for an argument of type `S'`. Now, it looks for an argument of type `S`, which is more generally useful behavior. Code making use of the old behavior should consider defining `S` or `S'` in terms of the other, since dot notation can unfold definitions during resolution.

This also fixes a bug in explicit field notation (`@x.f`) where `x` could be passed as the wrong argument.

Closes leanprover#3031