## 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_4 : semimodule R U,
_inst_5 : semimodule R V,
f : U → V
failed to synthesize type class instance for
R U V : Type,
_inst_1 : semiring R,
_inst_4 : semimodule R U,
_inst_5 : semimodule R V,
f : U → V


#### 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_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_4 : semimodule R U,
_inst_5 : semimodule R V,
f : U → V
failed to synthesize type class instance for
R U V : Type,
_inst_1 : semiring R,
_inst_4 : semimodule R U,
_inst_5 : semimodule R V,
f : U → V


#### 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