# Zulip Chat Archive

## Stream: new members

### Topic: Inferring associativity of composition

#### Yakov Pechersky (Jun 17 2020 at 18:34):

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 (Jun 18 2020 at 09:48):

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.

Last updated: Dec 20 2023 at 11:08 UTC