extending or inferring (PID / UFD) in a Lean class definition

Question

Why is mathlib's definition of UFD this:

class unique_factorization_domain (α : Type*) [integral_domain α] :=
(factors : α → multiset α)
(factors_prod : ∀{a : α}, a ≠ 0 → (factors a).prod ~ᵤ a)
(prime_factors : ∀{a : α}, a ≠ 0 → ∀x∈factors a, prime x)

(asking for the integral domain structure to be inferred by type class inference) but its definition of PID is this:

class principal_ideal_domain (α : Type*) extends integral_domain α :=
(principal : ∀ (S : ideal α), S.is_principal)

extending the integral domain structure? What is the difference? Does the old structure command have something to do with it?

Answer 1

My impression from the discussion on the Lean chat is that for subtle reasons related to type class inference it is probably better to extend the class, and so perhaps the definition of UFD needs to be refactored.