## Stream: new members

### Topic: Replacing ℤ with a type argument breaks type class synthesis

#### Eric Wieser (Jul 03 2020 at 14:13):

Hi all,

I had some type class defined over (A : ℤ → Type u), but decided I wanted to be able to restrict it to (A : ℕ → Type u). To avoid losing the generality of the original statement, I changed the declaration to {ι : Type u} (A : ι → Type u). Unfortunately, this appears to break lean's ability to "synthesize type class instances".

The change in question can be seen at https://github.com/pygae/lean-ga/pull/6/files. The file is self-contained, and I've added comments to the lines causing me trouble. The file builds with no errors prior to this change.

I think the problem is something to do with my type class becoming a Pi-type, which prevents inference of its fields?

#### Reid Barton (Jul 03 2020 at 14:15):

The has_coe instance looks useless, btw

#### Reid Barton (Jul 03 2020 at 14:16):

(I mean instance has_coe (r s : ι) (h: r = s) : has_coe (A r) (A s), in case there are others)

#### Eric Wieser (Jul 03 2020 at 14:17):

It probably is - I was trying to solve a problem in another file where I couldn't equate terms of types A r and A (r + 0)

#### Reid Barton (Jul 03 2020 at 14:18):

There's no way to supply h.

#### Reid Barton (Jul 03 2020 at 14:18):

Anyways, I'm surprised if this worked before.

#### Eric Wieser (Jul 03 2020 at 14:19):

I suspect it just silently did nothing useful and I wasn't relying on it

#### Eric Wieser (Jul 03 2020 at 14:19):

But at any rate, after this change I now get complaints from lean

#### Reid Barton (Jul 03 2020 at 14:19):

I meant the file in general

#### Reid Barton (Jul 03 2020 at 14:19):

The fields of graded_module_components don't make good instances

#### Eric Wieser (Jul 03 2020 at 14:20):

Really I was trying to use graded_module_components  as a shorthand for specifying all the properties over and over again

#### Reid Barton (Jul 03 2020 at 14:20):

I think this doesn't work.

#### Eric Wieser (Jul 03 2020 at 14:21):

I assume your statement is a judgement on the attribute [instance] lines below

#### Eric Wieser (Jul 03 2020 at 14:21):

Which actually worked perfectly until I replaced ℤ with ι

#### Reid Barton (Jul 03 2020 at 14:21):

For example, you're adding a rule for add_comm_group that matches literally anything applied to anything

#### Reid Barton (Jul 03 2020 at 14:22):

It may work so far in your small file

#### Eric Wieser (Jul 03 2020 at 14:23):

I suppose the number of "anything"s it matches grew immensely upon replacing ℤ...

#### Eric Wieser (Jul 03 2020 at 14:23):

But won't it only match things for which local instances of graded_module_components exist?

#### Reid Barton (Jul 03 2020 at 14:23):

It will match anything and then go look for instances of graded_module_components

#### Reid Barton (Jul 03 2020 at 14:24):

It can't see the future.

#### Jalex Stark (Jul 03 2020 at 14:24):

(Reid is talking about the typeclass inference algorithm)

#### Reid Barton (Jul 03 2020 at 14:24):

Eric Wieser said:

I suppose the number of "anything"s it matches grew immensely upon replacing ℤ...

Yes, with the change now all the instances match anything applied to anything.

#### Reid Barton (Jul 03 2020 at 14:24):

Because anything could be 0.

#### Reid Barton (Jul 03 2020 at 14:26):

We do have instances like this but where the type isn't changing.

#### Eric Wieser (Jul 03 2020 at 14:26):

Could you point me to the builtin ones?

Builtin what?

#### Reid Barton (Jul 03 2020 at 14:27):

I mean, imagine instead of A 0 or A r you just have A.

#### Eric Wieser (Jul 03 2020 at 14:27):

Sorry, wrong word - when you say "We do have", I'm asking for the names of those ones

#### Reid Barton (Jul 03 2020 at 14:27):

That seems more okay.

#### Reid Barton (Jul 03 2020 at 14:27):

You could also set_option trace.class_instances true and try to figure out why it didn't apply the instances you expected.

#### Reid Barton (Jul 03 2020 at 14:28):

I don't know if they have names. I think there are some in the category theory library.

#### Reid Barton (Jul 03 2020 at 14:28):

Also extends on a class creates them automatically I think.

#### Utensil Song (Jul 03 2020 at 14:29):

Reid Barton said:

We do have instances like this but where the type isn't changing.

I don't get the part "where the type isn't changing".

#### Reid Barton (Jul 03 2020 at 14:29):

An instance that says: In order to get an instance of C for a type, you need an instance of D for the same type.

#### Utensil Song (Jul 03 2020 at 14:30):

Ah, that makes sense in the context of category theory.

#### Utensil Song (Jul 03 2020 at 14:32):

Reid Barton said:

(I mean instance has_coe (r s : ι) (h: r = s) : has_coe (A r) (A s), in case there are others)

@Eric Wieser What were you trying to have with this? I don't get it.

#### Eric Wieser (Jul 03 2020 at 14:33):

I was trying to have a coercion from A (r + 0) to A r if I had a local trivial proof that r = r + 0

#### Utensil Song (Jul 03 2020 at 14:33):

That seems to be not a coercion

#### Utensil Song (Jul 03 2020 at 14:34):

They're just equal

#### Eric Wieser (Jul 03 2020 at 14:36):

Well, the lean type system doesn't allow me to make statements arp0 = ar if ar : A r and arp0 : A (r + 0).
It was an attempt at doing something like @Kevin Buzzard's canonical_map  in https://gist.githubusercontent.com/kbuzzard/f5ee35457c5d257ceec58c66d7da0c38/raw/e7eefed8190b436f4b6f34ee3895931e43859997/cdga.lean, and looking for alternate spellings

#### Reid Barton (Jul 03 2020 at 14:37):

Are you sure it was r + 0 and not 0 + r?

#### Eric Wieser (Jul 03 2020 at 14:40):

No, I'm probably misremembering the details

#### Eric Wieser (Jul 03 2020 at 14:41):

That was a problem that I only got halfway through investigating before running into the titular issue of this thread.

#### Eric Wieser (Jul 03 2020 at 14:41):

Unfortunately, set_option trace.class_instances true is not giving me anythiing I can easily sift though

#### Eric Wieser (Jul 03 2020 at 14:56):

Perhaps I should instead be asking the question "Is attempting to bundle type classes together like this sensible?"

#### Scott Morrison (Jul 04 2020 at 05:13):

An example of an instance which matches "anything" (and hence is probably a bad idea) is

https://github.com/leanprover-community/mathlib/blob/master/src/category_theory/isomorphism.lean#L210

which allows typeclass inference to prove an isomorphism is an epimorphism.

#### Scott Morrison (Jul 04 2020 at 05:14):

(the combination of "inference" and "prove" in that sentence may be a bad sign...)

#### Reid Barton (Jul 04 2020 at 12:53):

But here again the thing (no longer a type) f doesn't change.

Last updated: May 08 2021 at 19:11 UTC