## Stream: general

### Topic: Coercions on subtypes

#### Eric Wieser (Aug 13 2020 at 17:38):

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 (Aug 13 2020 at 17:39):

nooo u can't just make every function a coercion

#### Reid Barton (Aug 13 2020 at 17:40):

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 (Aug 13 2020 at 17:44):

since the type gets smaller

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

#### Reid Barton (Aug 13 2020 at 17:45):

it's definitely scarier

#### Kenny Lau (Aug 13 2020 at 17:46):

I thought the former would be scarier

#### Mario Carneiro (Aug 13 2020 at 18:14):

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

#### Reid Barton (Aug 13 2020 at 18:41):

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 (Aug 13 2020 at 18:50):

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 (Aug 13 2020 at 18:52):

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 (Aug 13 2020 at 19:09):

Would these be sensible as has_lift instead of has_coe?

#### Utensil Song (Aug 14 2020 at 12:15):

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 (Aug 14 2020 at 13:19):

{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 (Aug 14 2020 at 13:30):

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 (Aug 14 2020 at 14:37):

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 (Aug 14 2020 at 14:39):

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 (Aug 14 2020 at 15:40):

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}⟩


Last updated: May 14 2021 at 05:20 UTC