Apparently unhelpful instance resolution error

Stream: new members

[Iain Monro]

I'm trying to use unique_factorization_domain.to_gcd_domain to turn a unique_factorization_domain into a gcd_domain, but I'm getting a surprising error when I try to invoke it:

import ring_theory.unique_factorization_domain

namespace unique_factorization_domain

variables {R: Type} [integral_domain R] [unique_factorization_domain R] [normalization_domain R] [decidable_eq (associates R)]

example : gcd_domain R := to_gcd_domain R

end unique_factorization_domain

error: failed to synthesize type class instance for
R : Type,
_inst_1 : integral_domain R,
_inst_2 : unique_factorization_domain R,
_inst_3 : normalization_domain R,
_inst_4 : decidable_eq (associates R)
⊢ unique_factorization_domain R

Naturally I assume I'm making a basic mistake, but the error message is not really giving me any clues. Anyone able to point me in the right direction?

[Reid Barton]

Try turning on set_option pp.all true

[Iain Monro]

Ah, yes, that helps!

The problem was that to_gcd_domain wants a unique_factorization_domain whose integral_domain parameter has been constructed via normalization_domain.to_integral_domain from its normalization_domain, but I was just supplying one directly. Slightly odd that it cares, but I guess it makes sense if I think about if from the right direction. Removing [integral_domain R] and moving [normalization_domain R] before [unique_factorization_domain R] fixed it.

Thanks!