Zulip Chat Archive

Stream: general

Topic: Structure instantiation


view this post on Zulip Markus Himmel (Jul 02 2020 at 09:21):

I had always assumed that for a structure with a single field, writing ⟨value⟩ is exactly equivalent to writing { field := value }. However, this seems not to be the case:

class foo :=
(a : true)

structure baz [foo] :=
(a : true)

-- Works
example : Π (x : foo), @baz x :=
λ x, { a := trivial }

/-
synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized

inferred
  x
-/
example : Π (x : foo), @baz x :=
λ x, trivial

Is this intended behavior or a bug?

view this post on Zulip Mario Carneiro (Jul 02 2020 at 09:22):

what is the type of the constructor?

view this post on Zulip Markus Himmel (Jul 02 2020 at 09:23):

I'm not sure what you mean

view this post on Zulip Mario Carneiro (Jul 02 2020 at 09:23):

#print baz.mk
-- constructor baz.mk : Π [_inst_1 : foo], true → baz

view this post on Zulip Mario Carneiro (Jul 02 2020 at 09:23):

The anonymous constructor is the same as bas.mk trivial

view this post on Zulip Mario Carneiro (Jul 02 2020 at 09:24):

so maybe the better question is why the structure literal version doesn't give an error

view this post on Zulip Mario Carneiro (Jul 02 2020 at 09:25):

If this was a regular function application, the error would be expected (although this synthesized vs unified instance error is notorious for being useless and obstructionist)

view this post on Zulip Mario Carneiro (Jul 02 2020 at 09:26):

I think @Gabriel Ebner made a change affecting this error in a recent version

view this post on Zulip Markus Himmel (Jul 02 2020 at 09:27):

I guess I'm being stupid, because I don't see what's wrong with either of the versions. Why is an error expected?

view this post on Zulip Gabriel Ebner (Jul 02 2020 at 09:28):

The error message has been unchanged since 3.2.0.

view this post on Zulip Mario Carneiro (Jul 02 2020 at 09:29):

When you use [foo], lean will use typeclass inference to infer the value of foo you want. But in this case you have also supplied a value for the foo argument manually in the statement using @baz x, and this doesn't match what typeclass inference finds (nothing in this case)

view this post on Zulip Markus Himmel (Jul 02 2020 at 09:33):

Aha, I thought using @ completely disables typeclass resolution.

view this post on Zulip Mario Carneiro (Jul 02 2020 at 09:33):

It does, at @baz, but not at baz.mk where you used the anonymous constructor

view this post on Zulip Markus Himmel (Jul 02 2020 at 09:33):

Oh, now I get it.

view this post on Zulip Mario Carneiro (Jul 02 2020 at 09:33):

If you use @baz.mk x trivial instead it should work

view this post on Zulip Mario Carneiro (Jul 02 2020 at 09:33):

I think the reason the error exists instead of doing the obvious thing and going with the version found by unification is that it is an elaboration order problem; typeclass inference happens before unification is complete, and so lean may have already committed to the version that typeclass inference found and then later finds out that this doesn't match with something else

view this post on Zulip Markus Himmel (Jul 02 2020 at 09:37):

Okay, but does that explain why ⟨⟩ vs. {} makes a difference?

view this post on Zulip Mario Carneiro (Jul 02 2020 at 09:38):

Structure literals are a pretty complicated part of the elaborator, so I'm not particularly surprised that the order is different

view this post on Zulip Mario Carneiro (Jul 02 2020 at 09:39):

If I had to guess, I would say that it first gets the expected type to find out what structure is needed, and unifies with the constructor in order to get all the arguments

view this post on Zulip Markus Himmel (Jul 02 2020 at 09:45):

Fair enough, thank you for looking into it


Last updated: May 14 2021 at 02:15 UTC