trouble with algebras

Stream: general

[Scott Morrison]

Any advice for resolving:

import data.polynomial

set_option pp.all true

example {R : Type} [comm_ring R] (r : R) : polynomial ℤ →+* R :=
(polynomial.aeval ℤ R r).to_ring_hom

/- fails with:
```
synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  @polynomial.algebra'.{0 0} int int.comm_semiring int (@comm_semiring.to_semiring.{0} int int.comm_semiring)
    (@algebra_int.{0} int int.ring)
inferred
  @polynomial.algebra'.{0 0} int int.comm_semiring int (@comm_semiring.to_semiring.{0} int int.comm_semiring)
    (@algebra.id.{0} int int.comm_semiring)
```
-/

[Scott Morrison]

I can get

example {R : Type} [comm_ring R] (r : R) : polynomial ℤ →+* R :=
(by convert (polynomial.aeval ℤ R r) : polynomial ℤ →ₐ[ℤ] R).to_ring_hom

by first providing the instance subsingleton (algebra ℤ R), but it's not an ideal solution.

[Scott Morrison]

Because this doesn't help if someone quite reasonably writes (polynomial.aeval ℤ R r).to_ring_hom...

[Scott Morrison]

(And the convert results in a completely unusable term...)

[Johan Commelin]

Hmm, frustrating. I wonder if it is in some way related to https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/splitting.20field.20timeout