# Zulip Chat Archive

## Stream: general

### Topic: typeclass in assumption not visible

#### Tomas Skrivan (Nov 23 2020 at 21:12):

I'm having trouble with typeclasses when an instance is clearly in assumptions but is still fails to be synthesized. Minimal working example:

```
import algebra.module.linear_map
import data.real.basic
class C :=
{prop (R : Type) {U : Type} {V : Type} [semiring R] [add_comm_monoid U] [add_comm_monoid V] [semimodule R U] [semimodule R V] (f : U → V) : Prop}
instance inst : C := {prop := λ R U V [_] [_] [_] [_] [_] f, is_linear_map R f }
```

`is_linear_map`

has trouble finding an instance of `add_comm_monoid`

and `semimodule`

. What is going wrong here?

edit: Previously there was ` is_linear_map ℝ f`

instead of `is_linear_map R f`

#### Reid Barton (Nov 23 2020 at 21:14):

I don't think this `[_]`

is a real thing, is it?

#### Reid Barton (Nov 23 2020 at 21:16):

huh, apparently it does something

#### Tomas Skrivan (Nov 23 2020 at 21:16):

Well, I thought it might help because those instances actually get named as `_inst_#`

if you write `[_]`

instead of `_`

. But it does not work neither with `[_]`

or `_`

.

#### Reid Barton (Nov 23 2020 at 21:16):

Anyways, you have no instance involving `ℝ`

so that seems to be the main problem

#### Tomas Skrivan (Nov 23 2020 at 21:17):

Those are real numbers and there is definitely an instance of `semiring R`

.

#### Tomas Skrivan (Nov 23 2020 at 21:18):

My error looks like this:

```
failed to synthesize type class instance for
R U V : Type,
_inst_1 : semiring R,
_inst_2 : add_comm_monoid U,
_inst_3 : add_comm_monoid V,
_inst_4 : semimodule R U,
_inst_5 : semimodule R V,
f : U → V
⊢ add_comm_monoid V
failed to synthesize type class instance for
R U V : Type,
_inst_1 : semiring R,
_inst_2 : add_comm_monoid U,
_inst_3 : add_comm_monoid V,
_inst_4 : semimodule R U,
_inst_5 : semimodule R V,
f : U → V
⊢ add_comm_monoid U
```

#### Reid Barton (Nov 23 2020 at 21:18):

OK, the other problem is that `by exactI`

is needed here

#### Reid Barton (Nov 23 2020 at 21:18):

Then you will run into the problem with `ℝ`

#### Tomas Skrivan (Nov 23 2020 at 21:20):

Ohh sorry, I have messed up, There should be `is_linear_map R f`

instead of `is_linear_map ℝ f`

. And I get an error

```
failed to synthesize type class instance for
R U V : Type,
_inst_1 : semiring R,
_inst_2 : add_comm_monoid U,
_inst_3 : add_comm_monoid V,
_inst_4 : semimodule R U,
_inst_5 : semimodule R V,
f : U → V
⊢ semiring R
failed to synthesize type class instance for
R U V : Type,
_inst_1 : semiring R,
_inst_2 : add_comm_monoid U,
_inst_3 : add_comm_monoid V,
_inst_4 : semimodule R U,
_inst_5 : semimodule R V,
f : U → V
⊢ add_comm_monoid V
failed to synthesize type class instance for
R U V : Type,
_inst_1 : semiring R,
_inst_2 : add_comm_monoid U,
_inst_3 : add_comm_monoid V,
_inst_4 : semimodule R U,
_inst_5 : semimodule R V,
f : U → V
⊢ add_comm_monoid U
```

#### Kevin Buzzard (Nov 23 2020 at 21:20):

The type class inference system doesn't look at what's in your local context, it only knows about instances if they show up before the colon

#### Tomas Skrivan (Nov 23 2020 at 21:22):

So do I have to spell out all those instances manually in `instance inst : C := {prop := λ R U V [_] [_] [_] [_] [_] f, is_linear_map R f }`

?

#### Reid Barton (Nov 23 2020 at 21:22):

No, you need to insert `by exactI`

after the `,`

#### Tomas Skrivan (Nov 23 2020 at 21:23):

Ohh thank you! I have no clue what `by exactI`

does but it works.

#### Tomas Skrivan (Nov 23 2020 at 21:24):

Ok documentation says `Like 'exact', but uses all variables in the context for typeclass inference.`

Now it makes sense.

#### Eric Wieser (Nov 23 2020 at 21:40):

Does the example rely on `[_]`

, or is it fine with regular `_`

too?

#### Tomas Skrivan (Nov 23 2020 at 21:57):

It does not matter if `[_]`

or `_`

is used, the important bit is `by exactI`

i.e. it works when the last line is

```
instance inst : C := {prop := λ R U V _ _ _ _ _ f, by exactI is_linear_map R f }
```

#### Kevin Buzzard (Nov 23 2020 at 22:09):

That's a relief, because before this thread I'm not sure anyone had ever seen `[_]`

before.

Last updated: May 08 2021 at 19:11 UTC