Projects like mathlib like to define projection functions with extra structure, for example one could imagine defining Multiset.card : Multiset α →+ Nat, which bundles the fact that Multiset.card (m1 + m2) = Multiset.card m1 + Multiset.card m2 for all m1 m2 : Multiset α. A problem though is that so far this has prevented dot notation from working: you can't write (m1 + m2).card = m1.card + m2.card.

With this PR, now you can. The way it works is that "LValue resolution" will apply CoeFun instances when trying to resolve which argument should receive the object of dot notation.

A contrived-yet-representative example:

structure Equiv (α β : Sort _) where
  toFun : α → β
  invFun : β → α

infixl:25 " ≃ " => Equiv

instance: CoeFun (α ≃ β) fun _ => α → β where
  coe := Equiv.toFun

structure Foo where
  n : Nat

def Foo.n' : Foo ≃ Nat := ⟨Foo.n, Foo.mk⟩

variable (f : Foo)
#check f.n'
-- Foo.n'.toFun f : Nat

Design note 1: While LValue resolution attempts to make use of named arguments when positional arguments cannot be used, when we apply CoeFun instances we disallow making use of named arguments. The rationale is that argument names for CoeFun instances tend to be random, which could lead dot notation randomly succeeding or failing. It is better to be uniform, and so it uniformly fails in this case.

Design note 2: There is a limitation in that this will not make use of the values of any of the provided arguments when synthesizing the CoeFun instances (see the tests for an example), since argument elaboration takes place after LValue resolution. However, we make sure that synthesis will fail rather than choose the wrong CoeFun instance.

Performance note: Such instances will be synthesized twice, once during LValue resolution, and again when applying arguments.

This also adds in a small optimization to the parameter list computation in LValue resolution so that it lazily reduces when a relevant parameter hasn't been found yet, rather than using forallTelescopeReducing. It also switches to using forallMetaTelescope to make sure the CoeFun synthesis will fail if multiple instances could apply.

Getting this to pretty print will be deferred to future work.

Closes #1910