Weird type class resolution behavior of subtype coercion

Stream: general

[Eric Wieser]

I'm surprised to find that only the first of these four instances works:

import algebra.free_algebra

open free_algebra

variables {R : Type*} [comm_semiring R] {X : Type*}

structure add_proof (C : free_algebra R X → Prop) : Prop :=
(add : Π {a b}, C a → C b → C (a + b))

def aux {C : free_algebra R X → Prop}  (p : add_proof C) := {value // C value}

variables {C : free_algebra R X → Prop} (p : add_proof C)

-- with a proof present, this works
instance ok : has_add (aux p) := ⟨λ a b, ⟨↑a + ↑b, p.add a.prop b.prop⟩⟩

-- without it fails to find `has_lift_t (aux p) (free_algebra R X)`
instance fail1 : has_add (aux p) := ⟨λ a b, ⟨↑a + ↑b, sorry⟩⟩

-- even with a type annotation
instance fail2 : has_add (aux p) := ⟨λ a b, ⟨(↑a + ↑b : free_algebra R X), sorry⟩⟩

-- or show, from
instance fail3 : has_add (aux p) := ⟨λ a b, ⟨show free_algebra R X, from ↑a + ↑b, sorry⟩⟩

[Reid Barton]

Since there is no instance for aux I guess the real question is why ok does work. I think the variables a b in λ a b, must be inferred as having type {value // C value} somehow, in order to make sense of a.prop and b.prop. In the other cases they would be inferred as having type aux p.

[Reid Barton]

I also didn't know subtype.prop existed.

[Eric Wieser]

docs#subtype.prop looks to be an alias for docs#subtype.property