Allow implicit auto-params

[Kha]

This came up in context of #1647: an implicit auto-param could only be specified using a named argument of @

[digama0]

Also semi-implicit arguments make sense in conjunction with auto-params: f : {{x : A := by foo}} -> x = x -> True would not apply anything by default but f rfl would infer x using foo. The only combination that doesn't make sense is instance implicit with auto-param, and that's good because that's also the one that goes via different syntax because it is also the only one where you can omit the argument name.