Zulip Chat Archive

Stream: new members

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


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

view this post on Zulip Reid Barton (Jul 03 2020 at 14:15):

The has_coe instance looks useless, btw

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

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

view this post on Zulip Reid Barton (Jul 03 2020 at 14:18):

There's no way to supply h.

view this post on Zulip Reid Barton (Jul 03 2020 at 14:18):

Anyways, I'm surprised if this worked before.

view this post on Zulip Eric Wieser (Jul 03 2020 at 14:19):

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

view this post on Zulip Eric Wieser (Jul 03 2020 at 14:19):

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

view this post on Zulip Reid Barton (Jul 03 2020 at 14:19):

I meant the file in general

view this post on Zulip Reid Barton (Jul 03 2020 at 14:19):

The fields of graded_module_components don't make good instances

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

view this post on Zulip Reid Barton (Jul 03 2020 at 14:20):

I think this doesn't work.

view this post on Zulip Eric Wieser (Jul 03 2020 at 14:21):

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

view this post on Zulip Eric Wieser (Jul 03 2020 at 14:21):

Which actually worked perfectly until I replaced with ι

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

view this post on Zulip Reid Barton (Jul 03 2020 at 14:22):

It may work so far in your small file

view this post on Zulip Eric Wieser (Jul 03 2020 at 14:23):

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

view this post on Zulip Eric Wieser (Jul 03 2020 at 14:23):

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

view this post on Zulip Reid Barton (Jul 03 2020 at 14:23):

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

view this post on Zulip Reid Barton (Jul 03 2020 at 14:24):

It can't see the future.

view this post on Zulip Jalex Stark (Jul 03 2020 at 14:24):

(Reid is talking about the typeclass inference algorithm)

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

view this post on Zulip Reid Barton (Jul 03 2020 at 14:24):

Because anything could be 0.

view this post on Zulip Reid Barton (Jul 03 2020 at 14:26):

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

view this post on Zulip Eric Wieser (Jul 03 2020 at 14:26):

Could you point me to the builtin ones?

view this post on Zulip Reid Barton (Jul 03 2020 at 14:26):

Builtin what?

view this post on Zulip Reid Barton (Jul 03 2020 at 14:27):

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

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

view this post on Zulip Reid Barton (Jul 03 2020 at 14:27):

That seems more okay.

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

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

view this post on Zulip Reid Barton (Jul 03 2020 at 14:28):

Also extends on a class creates them automatically I think.

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

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

view this post on Zulip Utensil Song (Jul 03 2020 at 14:30):

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

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

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

view this post on Zulip Utensil Song (Jul 03 2020 at 14:33):

That seems to be not a coercion

view this post on Zulip Utensil Song (Jul 03 2020 at 14:34):

They're just equal

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

view this post on Zulip Reid Barton (Jul 03 2020 at 14:37):

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

view this post on Zulip Eric Wieser (Jul 03 2020 at 14:40):

No, I'm probably misremembering the details

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

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

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

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

view this post on Zulip Scott Morrison (Jul 04 2020 at 05:14):

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

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