RFC discussion: coercions don't fire with metavariables

Stream: lean4

[Floris van Doorn]

I'm planning to make the following RFC.

[Floris van Doorn]

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

import Lean

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, 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.

• 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)

---

[Floris van Doorn]

Do you think this would be a good feature to have?

[Floris van Doorn]

One question before I make this RFC: I thought we had similar issues with functions. However, I cannot reproduce it for functions now. Was I just imagining that (maybe remembering it from the Lean 3 days)?

import Lean

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

[Albus Dompeldorius]

I think I have encountered this situation here: #mathlib4 > Constructing morphisms in a cartesian closed category @ 💬

[Floris van Doorn]

I opened this as lean#7440