typeclass in assumption not visible

Stream: general

[Tomas Skrivan]

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]

I don't think this [_] is a real thing, is it?

[Reid Barton]

huh, apparently it does something

[Tomas Skrivan]

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]

Anyways, you have no instance involving ℝ so that seems to be the main problem

[Tomas Skrivan]

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

[Tomas Skrivan]

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]

OK, the other problem is that by exactI is needed here

[Reid Barton]

Then you will run into the problem with ℝ

[Tomas Skrivan]

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]

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]

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]

No, you need to insert by exactI after the ,

[Tomas Skrivan]

Ohh thank you! I have no clue what by exactI does but it works.

[Tomas Skrivan]

Ok documentation says Like 'exact', but uses all variables in the context for typeclass inference. Now it makes sense.

[Eric Wieser]

Does the example rely on [_], or is it fine with regular _ too?

[Tomas Skrivan]

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]

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