Odd Typeclass Resolution Behavior

Stream: new members

[Lucas Silver]

I am trying to use typeclasses to define a formalization and am running into a weird typeclass resolution error

I wrote the following code in which I introduce types with algebraic structure constraints using in a section using variables.

section
variables {R M : Type} [semiring R] [add_comm_group M] [module R M]

-- check if point in semiring is a unit
--def semiring.is_unit (r : R) : Prop
--  := ∃ s, (r s = 1 ∧ s * r = 1)

-- check if there is a unit to scale x by to get y
def is_scaling (x y : M) : Prop
  := (∃ r : Rˣ,  r • x = y)
lemma is_scaling_refl (x : M) : is_scaling x x
 := sorry

The lemma fails to typecheck giving a type error that indicates it does not know what add_comm_group instance to use on M

don't know how to synthesize placeholder
context:
M : Type,
_inst_2 : add_comm_group M,
x : M
⊢ Type

However, everything works when I stop using variables and explicitly quantify over the types and typeclasses in each definition.

def is_scaling' (R M : Type) [semiring R] [add_comm_group M] [module R M]
 (x y : M) : Prop
 := (∃ r : Rˣ, r • x = y)

-- is_scaling is an equivalence relation
lemma is_scaling_refl' (R M : Type) [semiring R] [add_comm_group M] [module R M] (x : M)
  : is_scaling' R M x x
  := sorry

I assume there is some subtle way in which I am using either the variables keyword or typeclasses incorrectly. Does anyone have any insights?

[Eric Wieser]

is_scaling x x doesn't tell Lean which R to use

[Eric Wieser]

You can make R explicit after you declare it:

variables {R M : Type} [semiring R] [add_comm_group M] [module R M]

variables (R)

-- check if there is a unit to scale x by to get y
def is_scaling (x y : M) : Prop
  := (∃ r : Rˣ,  r • x = y)
lemma is_scaling_refl (x : M) : is_scaling R x x
 := sorry

[Notification Bot]

This topic was moved here from #general > Odd Typeclass Resolution Behavior by Eric Wieser.

[Lucas Silver]

Thanks!