Weird difference between class and structure

Stream: new members

[Yicheng Tao]

Any ideas about the following situation?

structure Point where
  x : Nat
  y : Nat

structure Point3D extends Point where
  z : Nat

def p : Point3D := ⟨⟨1, 2⟩, 3⟩  -- success

class Point where
  x : Nat
  y : Nat

structure Point3D extends Point where
  z : Nat

def p : Point3D := ⟨⟨1, 2⟩, 3⟩ -- success

structure Point where
  x : Nat
  y : Nat

class Point3D extends Point where
  z : Nat

def p : Point3D := ⟨⟨1, 2⟩, 3⟩ -- success

class Point where
  x : Nat
  y : Nat

class Point3D extends Point where
  z : Nat

def p : Point3D := ⟨⟨1, 2⟩, 3⟩ -- fail

Why two class fail here.

[Yicheng Tao]

The answer is when Point and Point3D are both class, the arguments of Point3D.mk will take an implicit argument toPoint, which cause the angle constructor fails.

[Yicheng Tao]

When the parent is a structure, it can not perform instance search, so it will be an explicit argument. When the child is a structure, I think it's because structure is designed to be data-carrying. Searching for an instance to fill in is not expected.
That's my understanding.

[Kyle Miller]

In the failing case, checking the type of the constructor makes it clear what's going on:

#check Point3D.mk
/-
Point3D.mk [toPoint : Point] (z : Nat) : Point3D
-/

When defining a class, parents that are classes (that are represented as "subobjects") yield instance implicit arguments. (Subobject representation occurs for parents whose fields don't overlap with the fields of any parent before it.)

This is an implementation detail though. For structures you're expected to use "structure instance notation":

def p : Point3D := { x := 1, y := 2, z := 3 }

You can also do

def p : Point3D := { toPoint := { x := 1, y := 2}, z := 3 }

[Kyle Miller]

(This doesn't have to do with the notion of data-carrying. The same rules apply for Prop-valued structures/classes.)

[Yicheng Tao]

But things are strange for a structure with a class parent, where the argument is (toPoint : Point) instead of [toPoint : Point].

[Yicheng Tao]

I mean, what makes it an instance implicit argument? And what makes it not? If the second case fails it would make much more sense.

[Kyle Miller]

In the second case, you're defining a structure rather than a class, which according to the rule doesn't create instance implicit arguments for the constructor.