## Stream: general

### Topic: Diamond in multiplicative nat

#### Eric Wieser (Jan 04 2022 at 15:54):

What's going on with this diamond, and why is dunfold enough to solve it?

import algebra.group.type_tags
import data.nat.basic

example :
@monoid.to_mul_one_class (multiplicative ℕ) (comm_monoid.to_monoid _) =
multiplicative.mul_one_class :=
rfl -- fails

example :
@monoid.to_mul_one_class (multiplicative ℕ) (comm_monoid.to_monoid _) =
multiplicative.mul_one_class :=
begin
dunfold has_one.one multiplicative.mul_one_class,
refl,  -- ok
end


#### Anne Baanen (Jan 04 2022 at 15:55):

Could you post a trace.type_context.is_def_eq_detail trace? I assume it's either something irreducible blocking unification, or is_def_eq going down the wrong path and committing to it.

Sure:

#### Eric Wieser (Jan 04 2022 at 16:04):

Interestingly I can fix it by adding one := 1 in a few places, but then the dunfold version breaks instead!

#### Anne Baanen (Jan 04 2022 at 16:08):

It's a bit weird that it gives up on 1 =?= 0 without delta-reducing, since both sides should be projections out of a known structure.

#### Eric Wieser (Jan 04 2022 at 16:12):

Yeah, it's very weird

#### Eric Wieser (Jan 04 2022 at 16:12):

I made #11240 to try out a fix, but maybe it's worth fixing a deeper problem here

#### Reid Barton (Jan 04 2022 at 16:30):

More minimized version, using the expression where whnf got stuck:

import algebra.group.type_tags
import data.nat.basic

set_option trace.type_context.is_def_eq_detail true
set_option pp.all true

#check (rfl : @has_one.one.{0} (multiplicative.{0} nat)
(@multiplicative.has_one.{0} nat

I can't see any irreducibility setting which would interfere with reducing the left hand side, so it looks like an elaborator bug. The left hand side does #reduce to nat.zero.