Zulip Chat Archive

Stream: general

Topic: Structure instantiation


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?

Mario Carneiro (Jul 02 2020 at 09:22):

what is the type of the constructor?

Markus Himmel (Jul 02 2020 at 09:23):

I'm not sure what you mean

Mario Carneiro (Jul 02 2020 at 09:23):

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

Mario Carneiro (Jul 02 2020 at 09:23):

The anonymous constructor is the same as bas.mk trivial

Mario Carneiro (Jul 02 2020 at 09:24):

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

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)

Mario Carneiro (Jul 02 2020 at 09:26):

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

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?

Gabriel Ebner (Jul 02 2020 at 09:28):

The error message has been unchanged since 3.2.0.

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)

Markus Himmel (Jul 02 2020 at 09:33):

Aha, I thought using @ completely disables typeclass resolution.

Mario Carneiro (Jul 02 2020 at 09:33):

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

Markus Himmel (Jul 02 2020 at 09:33):

Oh, now I get it.

Mario Carneiro (Jul 02 2020 at 09:33):

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

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

Markus Himmel (Jul 02 2020 at 09:37):

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

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

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

Markus Himmel (Jul 02 2020 at 09:45):

Fair enough, thank you for looking into it


Last updated: Dec 20 2023 at 11:08 UTC