# Zulip Chat Archive

## Stream: new members

### Topic: Apparently unhelpful instance resolution error

#### Iain Monro (Aug 13 2020 at 12:54):

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

Try turning on `set_option pp.all true`

#### Iain Monro (Aug 13 2020 at 13:16):

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!

Last updated: Dec 20 2023 at 11:08 UTC