Can't find algebra instance

Stream: maths

[Adam Topaz]

Can someone explain what's going on here?

import linear_algebra.tensor_algebra
import algebra.category.Algebra.basic

variables {R : Type*} [comm_ring R]

example {M : Module R} : algebra R (tensor_algebra R M) := by apply_instance -- WORKS

def free_of_module : Module R ⥤ Algebra R :=
{ obj := λ M,
  { carrier := tensor_algebra R M,
    is_ring := algebra.semiring_to_ring R,
    is_algebra := by apply_instance }, -- FAILS
  map := sorry,
  map_id' := sorry,
  map_comp' := sorry }

[Adam Topaz]

Note that algebra.semiring_to_ring also requires the algebra instance, so the fact that the is_ring field works adds to the strangeness...

[Reid Barton]

Possibly related to https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/algebra.2Esemiring_to_ring.20breaks.20semimodule.20typeclass.20lookup/near/212584556

[Adam Topaz]

Okay, if I cheat and use local attribute [reducible] tensor_algebra then lean is indeed happy.

[Adam Topaz]

The algebra instance for the tensor algebra is obtained by a derive declaration. Is it possible there's some conflict with the fact that it's also tagged irreducible?

[Adam Topaz]

Did that conversation ever lead to a satisfactory conclusion @Eric Wieser @Reid Barton ?

[Reid Barton]

nope, still a mystery

[Adam Topaz]

I'll just cheat with reducibility for now then.

[Adam Topaz]

Okay, I have the algebra/module adjunction here:
https://github.com/leanprover-community/mathlib/compare/tensor_algebra_adjunction
But this involves cheating with semireducibility :(