calc for linear equivs

Stream: general

[Oliver Nash]

Should I be able to use calc to construct a linear_equiv?

[Oliver Nash]

For example, should calc_linear_equiv work in the following:

import algebra.module.linear_map

variables (R M N P : Type*)
variables [semiring R]
variables [add_comm_monoid M] [module R M]
variables [add_comm_monoid N] [module R N]
variables [add_comm_monoid P] [module R P]

/-- Works. -/
def calc_equiv (e₁ : M ≃ N) (e₂ : N ≃ P) : M ≃ P :=
calc M ≃ N : e₁
   ... ≃ P : e₂

/- Fails with error:
type mismatch at application
  linear_equiv.trans
term
  M
has type
  Type u_2 : Type (u_2+1)
but is expected to have type
  module ?m_1 ?m_2 : Type (max ? ?)
-/
def calc_linear_equiv (e₁ : M ≃ₗ[R] N) (e₂ : N ≃ₗ[R] P) : M ≃ₗ[R] P :=
calc M ≃ₗ[R] N : e₁
   ... ≃ₗ[R] P : e₂

[Eric Wieser]

@[trans] only works on types with two arguments, I think. docs#equiv is therefore fine, but docs#linear_equiv has way too many. I imagine even mul_equiv is not an option here. Maybe comparing docs#equiv.trans and docs#linear_equiv.trans can help.

[Oliver Nash]

I see!

[Oliver Nash]

Does @[trans] do anything else or are many such decorators basically pointless then?

[Oliver Nash]

(Also, if anyone has a reference for this "two arguments" rule, I'd be grateful to receive it.)

[Eric Wieser]

My hunch is it's pointless...

[Eric Wieser]

The attribute also works for tactic#transitivity I think

[Eric Wieser]

But I expect it to fail in the same way

[Oliver Nash]

Right, thanks.

[Eric Wieser]

Here's a possible fix - replace the weird {module} binders with [module] in linear_equiv.trans

[Oliver Nash]

The supposition being that implicit, but not typeclass, arguments contribute to the magical "two arguments" count?

[Eric Wieser]

Well, or that my previous rationale was nonsense.

[Oliver Nash]

Very unlikely! I'm going to leave this alone though, I don't want this badly enough.