Typeclass inference cannot find is_scalar_tower.left

Stream: general

[Eric Wieser]

mwe:

import algebra.module.basic

variables {R M : Type*} [semiring R] [add_comm_monoid M] [semimodule R M]

instance test1 : is_scalar_tower R R M := mul_action.is_scalar_tower.left _ -- ok
instance test2 : is_scalar_tower R R M := infer_instance  -- fails

docs#mul_action.is_scalar_tower.left is an instance, so why can't lean find it for me?

[Eric Wieser]

Maybe this is because is_scalar_tower.left depends on docs#mul_action.regular which isn't registered as an instance by default

[Kenny Lau]

What is the error?

[Kenny Lau]

Is it because infer_instance doesn't work for Prop

[Kevin Buzzard]

by apply_instance works

[Kevin Buzzard]

infer_instance : Π {α : Type u} [i : α], α

indeed Type u not Sort u, for some reason.

[Eric Wieser]

Is docs#infer_instance part of core?

[Eric Wieser]

Added in https://github.com/leanprover-community/lean/commit/f487989470d9e0c116a213a11c0f2ccc102c66fc

[Eric Wieser]

let's find out if there is a reason: leanprover-community/lean#506