units.has_scalar and polynomial.has_scalar diamond

Stream: general

[Eric Wieser]

So, the problem here is polynomial.smul, which is:

1. private, which means I can't link to it with docs#
2. Defined using a pattern match, which makes it not reduce when unapplied
3. irreducible, which means that typeclass search is unable to unfold it to see there is no diamond

If I replace it with

def smul {S : Type*} [monoid S] [distrib_mul_action S R] (s : S) (p : polynomial R) : polynomial R :=
of_finsupp (s • p.to_finsupp)

then the problem goes away.

@Sebastien Gouezel, you pushed for making this irreducible - what would be the impact of removing that attribute? The change to make polynomial a structure didn't cause any trouble here, only the irreducibility of the operations.

[Eric Wieser]

(I split this thread since the cause is very different, original thread here)

[Mario Carneiro]

You shouldn't have to unfold definitions (of non-instances) in order to prove that a diamond commutes. There are a lot of performance problems that arise when that becomes an option

[Mario Carneiro]

I'm not sure why it's private though

[Eric Wieser]

You can see where lean gets stuck here:

attribute [ext] has_scalar mul_action distrib_mul_action

example (R α : Type*) (β : α → Type*) [monoid R] [semiring α] [distrib_mul_action R α] :
  (units.distrib_mul_action : distrib_mul_action (units R) (polynomial α)) = polynomial.distrib_mul_action :=
begin
  -- note: this works around the pattern match opacity, but typeclass resolution does essentially only `ext : 3`
  ext u p : 5,
  dsimp [(•)],
  -- `polynomial.smul ↑u p = polynomial.smul u p`

  success_if_fail { refl },  -- fails, as `smul` is irreducible
  dunfold polynomial.smul, refl, -- succeeds
end

[Sebastien Gouezel]

The idea was to hide everything as much as possible, to make sure that people don't break the abstraction barrier and use the proper API. If it creates diamonds, though, I'm completely onboard with changing the definition.

[Eric Wieser]

I'll make a PR (edit: #8392)