Structure instantiation

Stream: general

[Markus Himmel]

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]

what is the type of the constructor?

[Markus Himmel]

I'm not sure what you mean

[Mario Carneiro]

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

[Mario Carneiro]

The anonymous constructor is the same as bas.mk trivial

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Markus Himmel]

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]

The error message has been unchanged since 3.2.0.

[Mario Carneiro]

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]

Aha, I thought using @ completely disables typeclass resolution.

[Mario Carneiro]

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

[Markus Himmel]

Oh, now I get it.

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

Fair enough, thank you for looking into it