# Zulip Chat Archive

## Stream: general

### Topic: instance lookup on function types

#### Eric Wieser (Oct 31 2021 at 11:49):

Something weird seems to be going on here:

```
import group_theory.group_action.basic
import algebra.module.opposites
import algebra.module.prod
open opposite
variables {R M : Type*}
lemma op_smul_eq_smul [monoid R] [mul_action R M] [mul_action Rᵒᵖ M]
[is_scalar_tower Rᵒᵖ R M] (r : R) (m : M) :
op r • m = r • m :=
by rw [←one_smul R m, ←smul_assoc (op r) (1 : R) m, op_smul_eq_mul, smul_smul, one_mul, mul_one]
instance comm_semigroup.op_is_scalar_tower [comm_semigroup R] : is_scalar_tower Rᵒᵖ R R :=
⟨λ a b c, opposite.rec (by exact λ a', mul_right_comm b a' c) a⟩
-- and now bad things happen
-- fails without this
instance comm_monoid.op_is_scalar_tower [comm_monoid R] :
is_scalar_tower Rᵒᵖ R R := comm_semigroup.op_is_scalar_tower
example [comm_monoid R] (r : R) (m : fin 3 → R) : op r • m = r • m := op_smul_eq_smul _ _
-- fails without this
instance comm_monoid_with_zero.op_is_scalar_tower [comm_monoid_with_zero R] :
is_scalar_tower Rᵒᵖ R R := comm_semigroup.op_is_scalar_tower
example [comm_monoid_with_zero R] (r : R) (m : fin 3 → R) : op r • m = r • m := op_smul_eq_smul _ _
-- fails without this
instance comm_semiring.op_is_scalar_tower [comm_semiring R] :
is_scalar_tower Rᵒᵖ R R := comm_semigroup.op_is_scalar_tower
example [comm_semiring R] (r : R) (m : fin 3 → R) : op r • m = r • m := op_smul_eq_smul _ _
-- fails without this
instance comm_ring.op_is_scalar_tower {R} [comm_ring R] : is_scalar_tower Rᵒᵖ R R := comm_semigroup.op_is_scalar_tower
example [comm_ring R] (r : R) (m : fin 3 → R) : op r • m = r • m := op_smul_eq_smul _ _
```

I feel like I shouldn't have to copy the same instance over and over again for every algebraic structure, especially as each can be proved from the previous. Somehow typeclass search is not willing to relax `comm_ring`

to `comm_semigroup`

when searching for the `is_scalar_tower`

instance

#### Kevin Buzzard (Oct 31 2021 at 12:57):

This sort of thing is easier to for the Lean 3 gurus to debug if you have some mathlib-free example and it always saddens me a bit that when obscure stuff like this happens that we can't just press a button and get a mwe without any mathlib imports.

#### Kevin Buzzard (Oct 31 2021 at 12:58):

In the past I have spent hours manually creating such examples on the basis that if I want people like Gabriel's help then I should do the work that I can do myself to try and make his life easier. Of course I am sufficiently ignorant about how typeclass inference works to not actually be sure that a mathlib-free example really would make his life easier anyway in this case.

#### Kevin Buzzard (Oct 31 2021 at 13:16):

I guess a mathlib-free example would make the trace much easier to read. My understanding of the output of `set_option trace.class_instances true`

is that it in the first failure (without the manual addition of the instance) Lean finds instances for `monoid R`

and `has_scalar Rᵒᵖ (fin 3 → R)`

and `has_scalar R (fin 3 → R)`

and `mul_action Rᵒᵖ (fin 3 → R) `

and `mul_action R (fin 3 → R)`

but then gets stuck on `is_scalar_tower Rᵒᵖ R (fin 3 → R)`

(i.e. it "proves" that it can't find this term, whatever that means in the context of type class inference)

#### Kevin Buzzard (Oct 31 2021 at 13:21):

so there's a slightly more minimal failure:

```
...
instance comm_semigroup.op_is_scalar_tower [comm_semigroup R] : is_scalar_tower Rᵒᵖ R R :=
⟨λ a b c, opposite.rec (by exact λ a', mul_right_comm b a' c) a⟩
-- example fails without this
instance comm_monoid.op_is_scalar_tower [comm_monoid R] :
is_scalar_tower Rᵒᵖ R R := infer_instance
example [comm_monoid R] : is_scalar_tower Rᵒᵖ R (fin 3 → R) := infer_instance
```

#### Kevin Buzzard (Oct 31 2021 at 13:22):

this is a proof that typeclass inference could have worked, but didn't.

Last updated: Aug 03 2023 at 10:10 UTC