new structure elaboration

Stream: general

[Sébastien Gouëzel]

While bumping mathlib in Carleson, I encountered a weird behavior, probably due to the new structure elaboration, in which typeclass instances are not available when extending classes. I'm not sure this has already been reported @Kyle Miller, so here it is. MWE:

class myClass : Type 1 where
  X : Type

instance instLEmyClass (m : myClass) : LE m.X where
  le _ _ := True

class fails extends myClass where
  p (x y : X) : x ≤ y

class works extends myClass where
  p (x y : X) :
    letI : LE X := instLEmyClass _
    x ≤ y

The LE instance on m.X is not available when defining a class that extends myClass. This used to work on 4.18.

[Edward van de Meent]

i think that this already was mentioned in porting notes, and i seem to recall that those also mentioned that this is being worked on?

[Kyle Miller]

The reason this used to work is that when class fails was being elaborated, the local context right before elaborating the p field looks like

tomyClass : myClass
X : Type := toMyClass.X

and so (x y : X) is the same as (x y : tomyClass.X). Since the LE instance is on m.X, that would enable the instLEmyClass instance to be found for x ≤ y.

This is brittle; it only works for fields from so-called "subobject parents" (parents that happen to be embedded as the structure's constructor fields). For example, this breaks it:

class nClass where
  n : Nat

class myClass extends nClass where
  X : Type

instance instLEmyClass (m : myClass) : LE m.X where
  le _ _ := True

class fails extends nClass, myClass where
  p (x y : X) : x ≤ y -- failed to synthesize LE X

The issue is that the the field overlap causes myClass to not be represented as a subobject parent, and instead the new X field is represented as its own constructor field. The local context instead looks like

tonClass : nClass
n : Nat := nClass.n
X : Type

so given (x y : X), one no longer has any connection between X and myClass.

With the new structure elaborator, instead the local context in class fails looks like

X : Type
tomyClass : myClass := { X := X }

The relationship between fields and parents is inverted; fields are primary, and the parent projections are all let bindings. No details of which parents are subobject fields are exposed anymore. (Another benefit: all parents provide themselves as instances now, and they can all be referred to in field declarations.)

The cost is that some things that used to elaborate no longer elaborate (sorry), but I don't see how to reliably have instances for fields of parent classes apply in general.

That said, I think we have two reliable workarounds for your problem that should appear for the next release. They both involve allowing let bindings as fields.

Future workaround 1: I expect that this will be allowed syntax:

class works extends myClass where
  let instLE : LE X := instLEmyClass _
  p (x y : X) :
    x ≤ y

Future workaround 2: Same syntax, but you use it to define a fixed LE instance in the parent class

class myClass : Type 1 where
  X : Type
  let instLE : LE X := { le _ _ := true }

and then when class fails is being defined, this instance would be in the local context.

I hadn't planned on it, but a potential feature could be the ability to mark certain definitions to be turned into let bindings whenever a structure is extended. For example, imagine

class myClass : Type 1 where
  X : Type

@[structure_include_let]
instance myClass.instLE (m : myClass) : LE m.X where
  le _ _ := True

class fails extends myClass where
  p (x y : X) : x ≤ y

and then the local context when p is being elaborated could be

X : Type
tomyClass : myClass := { X := X }
instLE : LE X := myClass.instLE tomyClass

Other than these sorts of features (new let field syntax or a @[structure_include_let] attribute), I don't see how we could support the old behavior — and I believe the old behavior wasn't intended.

Let me know if this is a significant issue, or if there are more examples that we should address.

[Edward van de Meent]

let me try to rephrase those possible solutions to check my understanding.
Both solutions allows you to tell lean about instances to use when trying to make sense of the types of class fields.

• Workaround 1 allows you to do so when defining the class which needs the instance
• Workaround 2 allows you to do so when defining the parent class, telling lean "keep this in mind for any child class"
• Workaround 2b (the structure_include_let option) allows you to do so when defining an instance, telling lean "add this in mind while extending ?????"

I'm not sure i quite get when some instance could be applicable to some class definition. I'm having a hard time visualizing exactly what aspects of myClass.instLE tell lean what classes this should be added to as "let" binding.

[Edward van de Meent]

honestly i'm having a hard time writing down my question...
let me try an example:

class myClass : Type 1 where
  X : Type

class Foo : Type 1 where
  X : Type

@[structure_include_let]
instance Foo.instGroup (m : Foo) : Group m.X := sorry

@[structure_include_let]
instance myClass.instLE (m : myClass) [Group m.X]: LE m.X where
  le _ _ := True

class fails extends myClass , Foo where
  p (x y : X) : x ≤ y

How does lean realize that myClass.instLE and Foo.instGroup should be added as let-bindings here?

[Edward van de Meent]

or, well, how will/might lean do this when this is implemented...

[Kyle Miller]

To be clear, the features I'm proposing are not for instances per se, but they can be used to supply instances (since typeclass inference makes use of any instances introduced with let).

• Workaround 1: Yes, the let lets you introduce instances that are needed to define fields. This is the "obvious" use of the potential feature.
• Workaround 2: Yes, the idea would be that lets are remembered, and they might even be available as additional projections.
• Workaround 2b: Not quite. Recall that Lean lets you define new projections using generalized field notation. The idea here is that you could mark such definitions to be added as new let fields when a structure is being extended.

[Sébastien Gouëzel]

Any of the workarounds you propose looks good to me (in particular the structure_include_let one, because it means downstream users don't need to understand that something subtle is going on). To be honest, the local introduction of missing instances with letI is also not too painful. The most surprising fact to me was that it used to work, and then is stopped working, but the explanation you give is perfectly convincing.

In an ideal world, maybe there could be some error message tweaking in this kind of situation, that would explain a little bit to the user what could be going on?

[Kyle Miller]

@Edward van de Meent In your example of

class fails extends myClass, Foo where
  p (x y : X) : x ≤ y

the local context before elaborating p would be something like

X : Type
instLE : [Group X] -> LE X
instGroup : Group X

[Edward van de Meent]

my main question is basically how lean would know what argument is the right one to check for when extending...

[Edward van de Meent]

i guess lean could look at the result type of the instance, and then check which arguments it depends on, then all of those are marked as "parents to check for"?

[Edward van de Meent]

so when lean sees an instance like
(m:myClass) (f: Foo) : Module f.X m.X, lean figures out to only add this let binding to the context when a class extends both myClass and Foo?

[Kyle Miller]

Sébastien Gouëzel said:

(in particular the structure_include_let one, because it means downstream users don't need to understand that something subtle is going on)

I think this is even the simplest way to implement it, so all the better! (There are a couple complexities to allowing users to write such definitions themselves that I'll have to work through though.)

Sébastien Gouëzel said:

In an ideal world, maybe there could be some error message tweaking in this kind of situation, that would explain a little bit to the user what could be going on?

Yeah, though I can't think of much we can do... Maybe if there's an instance synthesis error, if it were possible to make custom errors, we could detect that one of the field local variables is in the class's type and say "by the way, instances about fields aren't available to child structures, though you might be able to make use of such instances by introducing them with let". More sophisticated, but less reliably, we could also try to replace field locals with projections of a parent and resynthesizing to figure out exactly which instances are missing.

[Kyle Miller]

@Edward van de Meent I think you're sort of getting ahead of me with the feature idea. I wasn't considering letting these depend on instances defined by other @[structure_include_let] declarations.

All I had in mind was that such declarations would use a similar mechanism as dot notation. It would look for the argument whose type is the namespace the declaration is within. Notice that instLE is a function in the local context I gave.

[Edward van de Meent]

right... i personally figured that that would be because the return type doesn't depend on it, so it would be fine to leave that argument unspecified in the let

[Edward van de Meent]

i guess that asking what the implementation is before it is written is sort of backwards

[Kyle Miller]

Sorry, I don't really know what you mean or what you're imagining @[structure_include_let] would do. What's the significance of dependence in the types?

[Edward van de Meent]

ehmmmm

[Edward van de Meent]

i guess that doesn't really matter here

[Edward van de Meent]

sorry for my confusing questions

[Kyle Miller]

Thanks for probing the design. There are still many details I'm not sure about, and it might not be good to make this attribute user-accessible in the end, we'll see.