[RFC] use expected type in apply

Description

I would like to be able to use expected type dot notation with the apply tactic, i.e. apply .blah will use the expected type of the goal to resolve the prefix of .blah

For example in the following code refine resolves .t_of to Foo.prop.t_of but apply does not.

axiom Foo : Type
axiom Foo.prop : Foo → Prop
axiom Foo.t : Foo → Foo 
axiom Foo.prop.t_of {l : Foo} (h : l.prop) : (t l).prop
open Foo

axiom a : Foo
example : prop (t a) := by
  refine .t_of ?_
  sorry
example : prop (t a) := by
  apply .t_of -- invalid dotted identifier notation, expected type is not of the form (... → C ...) where C is a constant
  sorry

Implementation

I believe implementing this would be relatively simple. elabTermForApply and resolveId? could take an optional expectedType? argument, which could then be passed on to resolveName, I do not know yet what other consequences this would have.

I would be happy to work on this and test that it doesn't break existing code anywhere if it is a desired feature

Start by tracing elabTermForApply and resolveId? through resolveName, using the issue's apply .t_of and refine examples as the behavioral guide. Determine how the expected type should flow into dotted-name resolution, then verify that apply .t_of resolves Foo.prop.t_of and that existing behavior remains intact.