coe_trans

Stream: general

[Kenny Lau]

instance coe_trans {a : Sort u₁} {b : Sort u₂} {c : Sort u₃} [has_coe_t b c] [has_coe a b] : has_coe_t a c

[Kenny Lau]

why doesn't this instance cause loops in typeclass search?

[Floris van Doorn]

When looking for has_coe_t a c it first looks for instances for has_coe a ?m (which should only be a finite list, if you know a) and then looks for has_coe_t b c so as long as we restrict the has_coe instances enough (no cycles, adherence to this library note: https://leanprover-community.github.io/mathlib_docs/notes.html#use%20has_coe_t) there should not be a loop.

[Floris van Doorn]

(instance arguments are filled in from right-to-left, to speed-up the search for classes like algebra R A).

[Johan Commelin]

But the trouble with algebra_trans would come from the identity algebra R R... that would cause loops anyway )-;

[Kenny Lau]

@Johan Commelin we can avoid that by having algebra_t R R

[Kenny Lau]

you won't ever have algebra R R to cause the loop

[Johan Commelin]

Aah, and you are saying that we should only ever use algebra_t?
But aren't we still going to run into non-defeq diamonds?

[Johan Commelin]

Like, I compose the algebra instance int -> rat with rat -> real, and this will not be defeq to int -> real.

[Johan Commelin]

That's why I think we should have a typeclass like tower or commutes that expresses the provable equality of these instances.

[Kenny Lau]

fair