Inferring associativity of composition

Stream: new members

[Yakov Pechersky]

I'm trying to understand how instances are inferred for composition of functions or linear maps. Why does the first example work, but the second one fails?

import data.real.basic
import data.matrix.basic
import linear_algebra.matrix

variables {n : Type*} [fintype n] [decidable_eq n] {R : Type*} [field R]

-- works
example (A : matrix n n R) (B : matrix n n R) (C : matrix n n R) :
        (A.to_lin.comp (B.to_lin.comp C.to_lin)) = ((A.to_lin.comp B.to_lin).comp C.to_lin) :=
(is_associative.assoc _ _ _).symm

-- does not work, cannot find instance for is_associative
example (A : matrix n n R) (B : matrix n n R) (C : matrix n n R) :
        (A.to_lin.comp (B.to_lin.comp C.to_lin)) = ((A.to_lin.comp B.to_lin).comp C.to_lin) :=
begin
  rw @is_associative.assoc _ linear_map.comp (by apply_instance) _ _ _,
  sorry,
end

[Anne Baanen]

From set_option trace.class_instances true, we can see that it derives is_associative from the monoid instance on linear_map, but that only works for specific linear maps, from a semimodule M to M itself. In the first example, the expected type gives the elaborator enough information to finish the typeclass search. Passing the term as an argument to rw doesn't give it an expected type, so there are not enough constraints to find the monoid instance. If you help the typeclass search by writing rw @is_associative.assoc (linear_map R (n → R) (n → R)) linear_map.comp (by apply_instance), it does have enough information to succeed.