# Zulip Chat Archive

## Stream: new members

### Topic: Odd Typeclass Resolution Behavior

#### Lucas Silver (Feb 22 2023 at 19:51):

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 (Feb 22 2023 at 19:52):

`is_scaling x x`

doesn't tell Lean which `R`

to use

#### Eric Wieser (Feb 22 2023 at 19:53):

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 (Feb 22 2023 at 19:53):

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

#### Lucas Silver (Feb 22 2023 at 19:58):

Thanks!

Last updated: Dec 20 2023 at 11:08 UTC