RFC: Coercions should fire with metavariables

Proposal

Coercions typically only fire when the target type is fully known, see the examples below.

import Lean

universe u

def Set (X : Type u) : Type u := X → Prop
def MySet (X : Type u) : Type u := { _s : X → Prop // True }

def MyProp {X : Type u} (_s : Set X) : Prop := True

instance {X} : Coe (MySet X) (Set X) where coe s := s.1
-- instance {X} : CoeOut  (MySet X) (Set X) where coe s := s.1
-- instance {X} : CoeHead (MySet X) (Set X) where coe s := s.1
-- instance {X} : CoeTail (MySet X) (Set X) where coe s := s.1

-- error
example {X} (s : MySet X) : MyProp s := sorry
-- works
example {X} (s : MySet X) : MyProp (X := X) s := sorry
-- works
example {X} (s : MySet X) : MyProp (s : Set X) := sorry

Note: the error remains even when Coe is replaced by CoeHead, CoeTail or CoeOut.

Back in the days of Lean 0.2, I believe that coercions did not rely on type-classes, and coercions would trigger as soon as the head of the target type was known, even if not all of the arguments are known. It would be nice if we could have something similar again.

This would be a big benefit in Mathlib, since we're often in situations where there should be enough information to fire a coercion, but Lean doesn't, because the target type is not fully known.

Note: this already works nicely for CoeFun.

import Lean

universe u v

def MyFunction (X : Type u) (Y : Type v) : Type (max u v) := { _f : X → Y // True }

def Injective {α β} (f : α → β) : Prop :=
  ∀ ⦃a₁ a₂⦄, f a₁ = f a₂ → a₁ = a₂

instance {X Y} : CoeFun (MyFunction X Y)  (fun _ ↦ X → Y) where
  coe s := s.1

-- this works nicely
example {X Y} (f : MyFunction X Y) : Injective f := sorry
-- this works nicely
example {X Y} (f : MyFunction X Y) {x y} : f x = y := sorry

• User Experience: This would be a huge benefit and it will be less often the case that the user has to specify the same information twice. There is a risk that users will write code with less explicit information, resulting in code where Lean has to work harder.
• Beneficiaries: Mathlib, Lean users generally
• Maintainability: This is a major new feature, and will likely require more code specific to coercions on top of the code for type-class inference.

Community Feedback

This comes up a lot, here are some examples: 1, 2, 3)

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Start by reproducing the Lean examples in the issue and inspect the coercion and type-class inference entry points involved in resolving the metavariable target. Done means ordinary coercions fire when the target head is known but its arguments are metavariables, while the existing CoeFun behavior and explicit-type examples remain valid.