instance lookup on function types

Stream: general

[Eric Wieser]

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]

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]

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]

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]

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]

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