Zulip Chat Archive

Stream: general

Topic: typeclass in assumption not visible


view this post on Zulip 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

view this post on Zulip Reid Barton (Nov 23 2020 at 21:14):

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

view this post on Zulip Reid Barton (Nov 23 2020 at 21:16):

huh, apparently it does something

view this post on Zulip 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 _.

view this post on Zulip Reid Barton (Nov 23 2020 at 21:16):

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

view this post on Zulip Tomas Skrivan (Nov 23 2020 at 21:17):

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

view this post on Zulip 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

view this post on Zulip Reid Barton (Nov 23 2020 at 21:18):

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

view this post on Zulip Reid Barton (Nov 23 2020 at 21:18):

Then you will run into the problem with

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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 } ?

view this post on Zulip Reid Barton (Nov 23 2020 at 21:22):

No, you need to insert by exactI after the ,

view this post on Zulip Tomas Skrivan (Nov 23 2020 at 21:23):

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

view this post on Zulip 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.

view this post on Zulip Eric Wieser (Nov 23 2020 at 21:40):

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

view this post on Zulip 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 }

view this post on Zulip 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