Coercions on subtypes

Stream: general

[Eric Wieser]

Are the has_coes in this message safe? Are they sensible? Would they make sense in mathlib?

Eric Wieser said:

This seems to work:

import data.set.basic

instance coe_left_inter {X : Type*} {A B : set X} : has_coe ↥(A ∩ B) ↥A := ⟨ λ x, ⟨x.1, set.inter_subset_left _ _ x.2⟩ ⟩
instance coe_right_inter {X : Type*} {A B : set X} : has_coe ↥(A ∩ B) ↥B := ⟨ λ x, ⟨x.1, set.inter_subset_right _ _ x.2⟩ ⟩

example {X Y : Type*} {A B : set X} (f : A → Y) (g: B → Y) (h : ∀ x : A ∩ B, f x = g x) : sorry  := sorry

[Kenny Lau]

nooo u can't just make every function a coercion

[Reid Barton]

As far as coercions go they seem pretty safe/sensible to me, since the type gets smaller and you're not generally likely to have terms of A ∩ B in the first place. Also, the instances are defeq to each other when A and B are.

[Eric Wieser]

since the type gets smaller

Does that then mean that has_coe ↥A ↥(A ∪ B) would _not_ be sensible / safe?

[Reid Barton]

it's definitely scarier

[Kenny Lau]

I thought the former would be scarier

[Mario Carneiro]

please no. The typeclass problem for coercion already includes a ton of random garbage

[Reid Barton]

Maybe I have the wrong mental model for how coercion instance search works? I thought it was basically directed by the actual type of the thing being coerced, and then recursive on the result of the has_coe. So instances like these are basically working by structural recursion, and won't match anything that's not of the form A ∩ B.

[Rob Lewis]

I think weird coercions are a great way to get people totally lost about what they're writing, and this is a coercion from a coercion to a coercion. Regardless of whether type class inference will get confused, people will get confused.

[Reid Barton]

I'm not trying to argue for the coercion, I just don't see why it would be particularly problematic (I also don't find this confusing because coercing a set to a subtype is super common, but YMMV).

[Eric Wieser]

Would these be sensible as has_lift instead of has_coe?

[Utensil Song]

Eric Wieser said:

since the type gets smaller

Does that then mean that has_coe ↥A ↥(A ∪ B) would _not_ be sensible / safe?

Does it even work?

[Utensil Song]

{X Y : Type*} {A B : set X} (f : A → Y) (g: B → Y) (h : ∀ x : A ∩ B, f x = g x) is playing an even more dangerous game.

[Utensil Song]

For an x ∈ A ∩ B, its type should be X. Writing x : A ∩ B is nowhere near what you meant to express.

Same for f and g, they are not mapping the members of A and B to Y, so they are also not expressing functions that have a domain.

[Eric Wieser]

Writing x : A ∩ B is nowhere near what you meant to express.

It's not far off - it's identical to {x : {x' : X // x' ∈ A ∩ B}) which is not that different from saying(x : X) (h : x ∈ A ∩ B)

[Eric Wieser]

they are not mapping the members of A and B to Y

I'm confused by your statement - that's exactly what they're doing - they're partial functions over X that only accept members of A and B.

[Utensil Song]

Oh, I didn't recognize them as identical until I saw

/-- Coercion from a set to the corresponding subtype. -/
instance {α : Type*} : has_coe_to_sort (set α) := ⟨_, λ s, {x // x ∈ s}⟩