using etaExperiment

Stream: mathlib4

[Matthew Ballard]

What is the current guidance around enabling structure eta? It’s turned on in some files that have been merged. Are we just rolling with it?

[Matthew Ballard]

I’ve encountered people who think the current situation is hard no and some who think it’s hard yes. My personal understanding was: use it as a last resort to keep the port moving. Any clarification would be helpful. Thanks

[Eric Wieser]

I think if we want a rule against it it probably needs to be CI-enforced

[Eric Wieser]

(the rule might be just "must appear with a comment on the line above with a basic explanation of what alternatives didn't work)

[Matthew Ballard]

Perhaps some diagnostic information should be required to help with the final fix?

[Jireh Loreaux]

I thought Gabriel was pretty explicit about this being only for testing. The issue being, I think, that he may remove it from core whenever, at which point downstream uses would no longer be able to bump core.

[Matthew Ballard]

Is there value to keeping two copies - one with eta and one without (if possible)? Some statements get pretty brutal without it

[Eric Wieser]

@Gabriel Ebner did say that, but I think there might have been an ad-hoc decision to ignore it to allow porting more files.

[Eric Wieser]

at which point downstream uses would no longer be able to bump core.

RIght, at that point we can spend the effort to remove the uses of etaExperiment. But if we're very lucky the option will stop being needed anyway.

[Matthew Ballard]

Are we expecting some form of structure eta to be the final solution? If so, how confident are we in this?

[Eric Wieser]

I am of the opinion that new-style classes in the presense of diamonds are in the long run simply unusable without structure eta

[Eric Wieser]

In my opinion are options are:

1. Come up with ad-hoc and messy hacks during porting to avoid using etaExperiment. This isn't just a porting problem, end users of mathlib4 will run into the same pain as we do
2. Rework the algebra hierarchy to emulate the old-style classes we had in lean3. This is mechanical but tedious work, and there's no guarantee that it won't cause timeouts elsewhere
3. Tack on etaExperiment false and wait for Lean core to either help us by either adding shorthand for 2 or TC eta the default, or to force our hand.

[Matthew Ballard]

Personally, an upstream fix seems most reasonable as a long term solution. I don’t have any examples but it doesn’t seem unreasonable that the complexity of the algebra hierarchy could emerge naturally outside Mathlib, especially if Lean 4 becomes widely adopted as hoped.

[Matthew Ballard]

I should preface my opinions with: what do I know

[Ruben Van de Velde]

Also prefacing with "what do I know" :)

I suspect the most important benchmark for any solution will be "does this work for all of mathlib" - which we can only check once all of mathlib is ported. So right now I'd move forward with whatever gets us there fastest, and I think that's with applying the option where it helps

[Matthew Ballard]

The conclusion I got from the meeting today was "go ahead but don't go crazy". Anyone please feel free to correct me.

[Sebastian Ullrich]

There was the question of "what actually happens when etaExperiment makes things (much) slower?". Here is a (small part of a) diff from a random file

       [Meta.isDefEq] ❌ Preorder.mk (_ : ∀ (a : SignType), a ≤ a)
             (_ : ∀ (a b c : SignType), a ≤ b → b ≤ c → a ≤ c) =?= PartialOrder.toPreorder
+        [Meta.isDefEq] ✅ Preorder SignType =?= Preorder SignType
+        [Meta.isDefEq] ❌ Preorder.toLE =?= { le := fun x x_1 => x ≤ x_1 }
+          [Meta.isDefEq] ✅ LE SignType =?= LE SignType
+          [Meta.isDefEq] ❌ LE.le =?= fun x x_1 => x ≤ x_1
+            [Meta.isDefEq] ❌ fun x x_1 => x ≤ x_1 =?= fun a => LE.le a
+              [Meta.isDefEq] ✅ SignType =?= SignType
+              [Meta.isDefEq] ❌ fun x => x✝ ≤ x =?= LE.le x✝
+                [Meta.isDefEq] ❌ fun x => x✝ ≤ x =?= fun a => x✝ ≤ a
+                  [Meta.isDefEq] ✅ SignType =?= SignType
+                  [Meta.isDefEq] ❌ x✝¹ ≤ x✝ =?= x✝¹ ≤ x✝
+                    [Meta.isDefEq] ✅ x✝¹ =?= x✝¹
+                    [Meta.isDefEq] ✅ x✝ =?= x✝
+                    [Meta.isDefEq] ✅ SignType =?= SignType
+                    [Meta.isDefEq] ❌ SignType.instLESignType =?= Preorder.toLE
+                      [Meta.isDefEq] ❌ { le := SignType.Le } =?= Preorder.toLE
+                        [Meta.isDefEq] ✅ LE SignType =?= LE SignType
+                        [Meta.isDefEq] ❌ LE.le =?= SignType.Le
+                          [Meta.isDefEq] ❌ Preorder.toLE.1 =?= SignType.Le
+                            [Meta.isDefEq.onFailure] ❌ Preorder.toLE.1 =?= SignType.Le
+                              [Meta.isDefEq.stuckMVar] found stuck MVar ?m.16205 : LinearOrder SignType
+                        [Meta.isDefEq] ❌ { le := SignType.Le } =?= PartialOrder.toPreorder.1
+                          [Meta.isDefEq] ✅ LE SignType =?= LE SignType
+                          [Meta.isDefEq] ❌ LE.le =?= SignType.Le
+                            [Meta.isDefEq] ❌ PartialOrder.toPreorder.1.1 =?= SignType.Le
+                              [Meta.isDefEq.onFailure] ❌ PartialOrder.toPreorder.1.1 =?= SignType.Le
+                                [Meta.isDefEq.stuckMVar] found stuck MVar ?m.16205 : LinearOrder SignType
+                          [Meta.isDefEq.onFailure] ❌ { le := SignType.Le } =?= PartialOrder.toPreorder.1
+                            [Meta.isDefEq.stuckMVar] found stuck MVar ?m.16205 : LinearOrder SignType
+                    [Meta.isDefEq] ❌ SignType.instLESignType.1 x✝¹ x✝ =?= Preorder.toLE.1 x✝¹ x✝
+                      [Meta.isDefEq] ❌ SignType.Le x✝¹ x✝ =?= Preorder.toLE.1 x✝¹ x✝
+                        [Meta.isDefEq] ❌ SignType.Le =?= Preorder.toLE.1
+                          [Meta.isDefEq.onFailure] ❌ SignType.Le =?= Preorder.toLE.1
+                            [Meta.isDefEq.stuckMVar] found stuck MVar ?m.16205 : LinearOrder SignType
+                        [Meta.isDefEq.onFailure] ❌ SignType.Le x✝¹ x✝ =?= Preorder.toLE.1 x✝¹ x✝
+                          [Meta.isDefEq.stuckMVar] found stuck MVar ?m.16205 : LinearOrder SignType
+                        [Meta.isDefEq.onFailure] ❌ SignType.Le x✝¹ x✝ =?= Preorder.toLE.1 x✝¹ x✝
+                          [Meta.isDefEq.stuckMVar] found stuck MVar ?m.16205 : LinearOrder SignType
+          [Meta.isDefEq] ❌ PartialOrder.toPreorder.1 =?= { le := fun x x_1 => x ≤ x_1 }
+            [Meta.isDefEq] ✅ LE SignType =?= LE SignType
+            [Meta.isDefEq] ❌ LE.le =?= fun x x_1 => x ≤ x_1
+              [Meta.isDefEq] ❌ fun x x_1 => x ≤ x_1 =?= fun a => LE.le a
+                [Meta.isDefEq] ✅ SignType =?= SignType
+                [Meta.isDefEq] ❌ fun x => x✝ ≤ x =?= LE.le x✝
+                  [Meta.isDefEq] ❌ fun x => x✝ ≤ x =?= fun a => x✝ ≤ a
+                    [Meta.isDefEq] ✅ SignType =?= SignType
+                    [Meta.isDefEq] ❌ x✝¹ ≤ x✝ =?= x✝¹ ≤ x✝
+                      [Meta.isDefEq] ✅ x✝¹ =?= x✝¹
+                      [Meta.isDefEq] ✅ x✝ =?= x✝
+                      [Meta.isDefEq] ✅ SignType =?= SignType
+                      [Meta.isDefEq] ❌ SignType.instLESignType =?= PartialOrder.toPreorder.1
+                        [Meta.isDefEq] ❌ { le := SignType.Le } =?= PartialOrder.toPreorder.1
+                          [Meta.isDefEq] ✅ LE SignType =?= LE SignType
+                          [Meta.isDefEq] ❌ LE.le =?= SignType.Le
+                            [Meta.isDefEq] ❌ PartialOrder.toPreorder.1.1 =?= SignType.Le
+                              [Meta.isDefEq.onFailure] ❌ PartialOrder.toPreorder.1.1 =?= SignType.Le
+                                [Meta.isDefEq.stuckMVar] found stuck MVar ?m.16205 : LinearOrder SignType
+                          [Meta.isDefEq.onFailure] ❌ { le := SignType.Le } =?= PartialOrder.toPreorder.1
+                            [Meta.isDefEq.stuckMVar] found stuck MVar ?m.16205 : LinearOrder SignType
+                      [Meta.isDefEq] ❌ SignType.instLESignType.1 x✝¹ x✝ =?= PartialOrder.toPreorder.1.1 x✝¹ x✝
+                        [Meta.isDefEq] ❌ SignType.Le x✝¹ x✝ =?= PartialOrder.toPreorder.1.1 x✝¹ x✝
+                          [Meta.isDefEq] ❌ SignType.Le =?= PartialOrder.toPreorder.1.1
+                            [Meta.isDefEq.onFailure] ❌ SignType.Le =?= PartialOrder.toPreorder.1.1
+                              [Meta.isDefEq.stuckMVar] found stuck MVar ?m.16205 : LinearOrder SignType
+                          [Meta.isDefEq.onFailure] ❌ SignType.Le x✝¹ x✝ =?= PartialOrder.toPreorder.1.1 x✝¹ x✝
+                            [Meta.isDefEq.stuckMVar] found stuck MVar ?m.16205 : LinearOrder SignType
+                          [Meta.isDefEq.onFailure] ❌ SignType.Le x✝¹ x✝ =?= PartialOrder.toPreorder.1.1 x✝¹ x✝
+                            [Meta.isDefEq.stuckMVar] found stuck MVar ?m.16205 : LinearOrder SignType
+            [Meta.isDefEq.onFailure] ❌ PartialOrder.toPreorder.1 =?= { le := fun x x_1 => x ≤ x_1 }
+              [Meta.isDefEq.stuckMVar] found stuck MVar ?m.16205 : LinearOrder SignType
         [Meta.isDefEq] ❌ Preorder.mk (_ : ∀ (a : SignType), a ≤ a)
               (_ : ∀ (a b c : SignType), a ≤ b → b ≤ c → a ≤ c) =?= LinearOrder.toPartialOrder.1

Basically, it looks like class eta allows us to make much more progress on a unification problem like Foo.mk ... =?= Bar.toFoo ?instBar that is ultimately not solvable because there is no such ?instBar instance