Debugging procedure

Stream: mathlib4

[Patrick Massot]

As discussed last week, I found a really tricky lemma to port in the sphere eversion project. This is probably due to some not-so-nice instance, and I can prove the lemma. But I spend a lot of time on it and I still don't really understand the issue. My question is not really about this specific issue, it's about the debugging procedure. I'll paste the code below. This code works but it has two places that involve suffering. One is a rw that should be a simp only, and the other one is a rw that doesn't work but erw works (and of course simp only doesn't work). In Lean 3 the whole proof was a single simp only call. The question is: how do you debug this? In particular how can you get access to the part of the lemma that is not syntactically matching the goal, necessitating the erw?

/-
Copyright (c) 2022 Heather Macbeth. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Heather Macbeth

! This file was ported from Lean 3 source module to_mathlib.analysis.inner_product_space.cross_product
-/
import Mathlib.Analysis.InnerProductSpace.Dual
import Mathlib.Analysis.InnerProductSpace.Orientation


section meta_utils
open Lean PrettyPrinter Delaborator SubExpr

def withBetaReduced (d : Delab) : Delab := do
  let e' ← Core.betaReduce (← getExpr)
  withTheReader SubExpr (fun ctx => {ctx with expr := e'}) d

/-- Fail if the arity is less than `n`, and collect arguments if the arity is more than `n`. -/
partial def delabWithArity (n : Nat) (d : Delab) : Delab := do
  if (← getExpr).getAppNumArgs < n then
    failure
  else
    let rec loop (args : Array Term) : Delab := do
      if (← getExpr).getAppNumArgs > n then
        let arg ← withAppArg delab
        withAppFn <| loop (args.push arg)
      else
        let s ← d
        `($s $args*)
    loop #[]

/-- Delaborator for a coercion function of arity `arity` such that
the coerced value is at argument index `coeArg`. -/
def delabCoe (arity coeArg : Nat) : Delab := delabWithArity arity do
  let arg ← withNaryArg coeArg delab
  let ty ← withType <| withBetaReduced delab
  `((↑$arg : $ty))

namespace AnnotateFunLikecoe
/-- Display `FunLike.coe` with type ascriptions. -/
@[scoped delab app.FunLike.coe]
def delabFunLikeCoe : Delab := delabCoe 5 4
end AnnotateFunLikecoe
end meta_utils

/-! # The cross-product on an oriented real inner product space of dimension three -/

noncomputable section

open scoped RealInnerProductSpace

open FiniteDimensional

set_option synthInstance.checkSynthOrder false
attribute [local instance] fact_finiteDimensional_of_finrank_eq_succ
set_option synthInstance.checkSynthOrder true

variable (E : Type _) [NormedAddCommGroup E] [InnerProductSpace ℝ E]

/-- The identification of a finite-dimensional inner product space with its algebraic dual. -/
private def to_dual [FiniteDimensional ℝ E] : E ≃ₗ[ℝ] E →ₗ[ℝ] ℝ :=
  (InnerProductSpace.toDual ℝ E).toLinearEquiv ≪≫ₗ LinearMap.toContinuousLinearMap.symm

namespace Orientation

variable {E}
variable [Fact (finrank ℝ E = 3)] (ω : Orientation ℝ E (Fin 3))

/-- Linear map from `E` to `E →ₗ[ℝ] E` constructed from a 3-form `Ω` on `E` and an identification of
`E` with its dual.  Effectively, the Hodge star operation.  (Under appropriate hypotheses it turns
out that the image of this map is in `𝔰𝔬(E)`, the skew-symmetric operators, which can be identified
with `Λ²E`.) -/
def crossProduct : E →ₗ[ℝ] E →ₗ[ℝ] E := by
  let z : AlternatingMap ℝ E ℝ (Fin 0) ≃ₗ[ℝ] ℝ :=
    AlternatingMap.constLinearEquivOfIsEmpty.symm
  let y : AlternatingMap ℝ E ℝ (Fin 1) →ₗ[ℝ] E →ₗ[ℝ] ℝ :=
    LinearMap.llcomp ℝ E (AlternatingMap ℝ E ℝ (Fin 0)) ℝ z ∘ₗ AlternatingMap.curryLeftLinearMap
  let y' : AlternatingMap ℝ E ℝ (Fin 1) →ₗ[ℝ] E :=
    (LinearMap.llcomp ℝ (AlternatingMap ℝ E ℝ (Fin 1)) (E →ₗ[ℝ] ℝ) E (to_dual E).symm) y
  let u : AlternatingMap ℝ E ℝ (Fin 2) →ₗ[ℝ] E →ₗ[ℝ] E :=
    LinearMap.llcomp ℝ E (AlternatingMap ℝ E ℝ (Fin 1)) _ y' ∘ₗ AlternatingMap.curryLeftLinearMap
  exact u ∘ₗ AlternatingMap.curryLeftLinearMap (n := 2) ω.volumeForm

local infixl:100 "×₃" => ω.crossProduct

theorem crossProduct_apply_self (v : E) : v×₃v = 0 := by simp [crossProduct]

set_option quotPrecheck false in
notation "𝒜" => AlternatingMap ℝ E ℝ (Fin 0)

set_option quotPrecheck false in
notation "𝒜'" => AlternatingMap ℝ E ℝ (Fin (Nat.succ 0))

attribute [pp_dot] LinearEquiv.symm
open AnnotateFunLikecoe

-- Let's inspect `LinearMap.toContinuousLinearMap` and ways to build the `ContinuousSMul` instance
-- it requires. Feel free to skip to the theorem on first read.

#check (LinearMap.toContinuousLinearMap : (E →ₗ[ℝ] ℝ) → NormedSpace.Dual ℝ E)

#check (↑LinearMap.toContinuousLinearMap : (E →ₗ[ℝ] ℝ) → NormedSpace.Dual ℝ E)

#synth ContinuousSMul ℝ ℝ
#check to_dual.proof_11

example : to_dual.proof_11 = ContinuousMul.to_continuousSMul := rfl

#check @LinearMap.toContinuousLinearMap ℝ _ E _ _ _ _ _ ℝ _ _ _ _ to_dual.proof_11 _ _ _

lemma foo (φ : E →ₗ[ℝ] ℝ) (w: E) :
    (↑((LinearMap.toContinuousLinearMap : (E →ₗ[ℝ] ℝ) → NormedSpace.Dual ℝ E) φ) : E → ℝ) w =
    (↑φ : E → ℝ) w := by
  rfl

lemma bar (φ : E →ₗ[ℝ] ℝ) (w: E) : @FunLike.coe (NormedSpace.Dual ℝ E) E (fun _ ↦ ℝ) ContinuousMapClass.toFunLike
    (@LinearMap.toContinuousLinearMap ℝ _ E _ _ _ _ _ ℝ _ _ _ _ to_dual.proof_11 _ _ _ φ) w =
    (↑φ : E → ℝ) w := by
  rfl

--set_option pp.explicit true in
theorem inner_crossProduct_apply (u v w : E) : ⟪u×₃v, w⟫ = ω.volumeForm ![u, v, w] := by
  simp only [crossProduct]
  simp only [to_dual]
  simp only [LinearEquiv.trans_symm]
  simp only [LinearEquiv.symm_symm]
  simp only [LinearIsometryEquiv.toLinearEquiv_symm]
  simp only [AlternatingMap.curryLeftLinearMap_apply]
  simp only [LinearMap.coe_comp]
  simp only [Function.comp_apply]
  simp only [LinearMap.llcomp_apply]
  simp only [LinearEquiv.coe_coe]
  simp only [LinearEquiv.trans_apply]
  simp only [LinearIsometryEquiv.coe_toLinearEquiv]
  simp only [AlternatingMap.curryLeftLinearMap_apply]
  simp only [LinearMap.coe_comp]
   -- simp only [InnerProductSpace.toDual_symm_apply] fails
  rw [InnerProductSpace.toDual_symm_apply]
  set F' : 𝒜' → E →ₗ[ℝ] ℝ := (LinearMap.llcomp ℝ E 𝒜 ℝ ↑(AlternatingMap.constLinearEquivOfIsEmpty.symm : 𝒜 ≃ₗ[ℝ] ℝ)) ∘ AlternatingMap.curryLeftLinearMap
  set K := (AlternatingMap.curryLeft ((AlternatingMap.curryLeft (volumeForm ω)) u)) v
  -- rw [LinearMap.coe_toContinuousLinearMap' (F' K)] -- fails
  -- rw [bar (F' K) w] -- fails
  -- rw [foo (F' K) w] -- fails
  erw [bar (F' K) w]
  simp only [Function.comp_apply]
  simp only [LinearMap.llcomp_apply]
  simp only [LinearEquiv.coe_coe]
  simp only [AlternatingMap.constLinearEquivOfIsEmpty_symm_apply]
  simp only [Matrix.zero_empty]
  simp only [AlternatingMap.curryLeftLinearMap_apply]
  simp only [AlternatingMap.curryLeft_apply_apply]

[Eric Wieser]

Does making docs#NormedSpace.Dual reducible (to match docs#Module.Dual) fix the first simp only failure?

[Eric Wieser]

The (↑LinearMap.toContinuousLinearMap : (E →ₗ[ℝ] ℝ) → NormedSpace.Dual ℝ E) in the goal view looks pretty fishy to me

[Eric Wieser]

That's not really the type of the def, so my guess is that lean is getting confused about the difference between NormedSpace.Dual 𝕜 E and (E →L[𝕜] 𝕜)

[Kevin Buzzard]

Indeed, filling in a bunch of implicit variables gives the following error:

application type mismatch
  @InnerProductSpace.toDual_symm_apply ℝ E ?m.383599 ?m.383600 ?m.383601 ?m.383602 w
    (((↑((↑(LinearMap.llcomp ℝ E 𝒜 ℝ) : (𝒜 →ₗ[ℝ] ℝ) → (E →ₗ[ℝ] 𝒜) →ₗ[ℝ] E →ₗ[ℝ] ℝ) ?m.389716) :
            (E →ₗ[ℝ] 𝒜) → E →ₗ[ℝ] ℝ) ∘
        (↑AlternatingMap.curryLeftLinearMap : 𝒜' → E →ₗ[ℝ] 𝒜))
      ((↑(AlternatingMap.curryLeft
              ((↑(AlternatingMap.curryLeft (volumeForm ω)) : E → AlternatingMap ℝ E ℝ (Fin 2)) u)) :
          E → AlternatingMap ℝ E ℝ (Fin 1))
        v))
argument
  ((↑((↑(LinearMap.llcomp ℝ E 𝒜 ℝ) : (𝒜 →ₗ[ℝ] ℝ) → (E →ₗ[ℝ] 𝒜) →ₗ[ℝ] E →ₗ[ℝ] ℝ) ?m.389716) : (E →ₗ[ℝ] 𝒜) → E →ₗ[ℝ] ℝ) ∘
      (↑AlternatingMap.curryLeftLinearMap : 𝒜' → E →ₗ[ℝ] 𝒜))
    ((↑(AlternatingMap.curryLeft ((↑(AlternatingMap.curryLeft (volumeForm ω)) : E → AlternatingMap ℝ E ℝ (Fin 2)) u)) :
        E → AlternatingMap ℝ E ℝ (Fin 1))
      v)
has type
  E →ₗ[ℝ] ℝ : Type u_1
but is expected to have type
  NormedSpace.Dual ℝ E : Type u_1

[Eric Wieser]

(I realize this doesn't directly answer your question, but perhaps we could write a tactic to detect this kind of type issue)

[Kevin Buzzard]

attribute [reducible] NormedSpace.Dual -- invalid attribute 'reducible', declaration is in an imported module :cry:

So I have to mark it reducible at source and then recompile everything? :-( it's bed time!

[Eric Wieser]

Or better, change def to abbrev

[Eric Wieser]

But yes, make the change and a PR, and let CI try it while you sleep!

[Kevin Buzzard]

Analysis/InnerProductSpace/Dual.lean stops compiling and I don't know my way around this part of the library at all.

[Eric Wieser]

You also need to delete all the instances we copied

[Kevin Buzzard]

I'm afraid I don't have time to embark on this :-(

[Eric Wieser]

Me neither

[Matthew Ballard]

For the first, I think I would check for metadata in the expression with pp.raw (didn’t see it but the term is very large) and then trace.Meta.isDefEq and trace.Meta.synthInstance to see the difference in behavior between simp and rw. lean4#2461 seems to behave similarly.

I don’t have a better way to inspect an expensive rewrite than printing a giant term. It would good to have something more efficient, especially for the horror that is some parts of current AG library

[Matthew Ballard]

#6998 fixes the expensive rewrite but not the simp vs rw issue

[Matthew Ballard]

By making Dual reducible

[Patrick Massot]

Eric Wieser said:

(I realize this doesn't directly answer your question, but perhaps we could write a tactic to detect this kind of type issue)

On the contrary, this is exactly my question. I want a tools to debug those issues. As I wrote, I can work around this issue (the proof I posted does work), but I don want to regularly spend days on such issues.

[Eric Wieser]

Sorry, what I meant was "my previous message did not answer your question, but this parenthesized comment might"

[Kevin Buzzard]

Are we any nearer to understanding why simp fails but rw works?

[Eric Wieser]

Presumably simp is using stricter reducibility settings than rw

[Eric Wieser]

(and arguably, rw is in the wrong here and only erw should work)

[Patrick Massot]

Kevin, what was your algorithm to find the implicit variables you needed to fill?

[Eric Wieser]

Kevin's error message doesn't look relevant to me. It says:

has type
  E →ₗ[ℝ] ℝ : Type u_1
but is expected to have type
  NormedSpace.Dual ℝ E : Type u_1

but my claim was that Lean was getting confused about Dual and E →L[ℝ] ℝ (with L not ₗ)

[Eric Wieser]

Which is to say, it sounds like Kevin filled the implicit variables incorrectly

[Kevin Buzzard]

oh maybe. My algorithm was to uncomment the simp only line, click on and hover over the InnerProductSpace.toDual_symm_apply on that line, and then observe that in the messages and in the pop-up I had enough information to start filling in implicit variables, and then I just started adding stuff like simp only [InnerProductSpace.toDual_symm_apply (\k := \R)] etc. It was just five minutes before I was turning the computer off though so I could have made some errors.

[Patrick Massot]

Eric, I answered some of your questions at #6998

[Kevin Buzzard]

I'm on a 45 minute train journey and it's touch and go as to whether lake exe cache get will terminate before I arrive...

[Patrick Massot]

Matthew Ballard said:

For the first, I think I would check for metadata in the expression with pp.raw (didn’t see it but the term is very large) and then trace.Meta.isDefEq and trace.Meta.synthInstance to see the difference in behavior between simp and rw. lean4#2461 seems to behave similarly.

I don’t have a better way to inspect an expensive rewrite than printing a giant term. It would good to have something more efficient, especially for the horror that is some parts of current AG library

Does anyone understand the output with trace.Meta.isDefEq in the failing simp? It's full of things like:

❌ Prop =?= {R : Type} →
      [inst : Semiring R] →
        {M : Type u_1} →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : Module R M] →
              {N : Type} →
                [inst_3 : AddCommMonoid N] →
                  [inst_4 : Module R N] → {ι : Type} → FunLike (AlternatingMap R M N ι) (ι → M) fun x => N

There are dozens of variations on this unpromising theme, and then the trace ends with

❌ ?a =
      ?a =?= inner
        (↑(LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E))
          (↑LinearMap.toContinuousLinearMap
            ((↑(↑(LinearMap.llcomp ℝ E 𝒜 ℝ) ↑AlternatingMap.constLinearEquivOfIsEmpty.symm) ∘
                ↑AlternatingMap.curryLeftLinearMap)
              (↑(AlternatingMap.curryLeft (↑(AlternatingMap.curryLeft (Orientation.volumeForm ω)) u)) v))))
        w =
      ↑(Orientation.volumeForm ω) ![u, v, w]

[Patrick Massot]

For comparison, the rw does the usual start with lots of failing foo ?m.78876 =?= foo a but then it goes straight to the relevant quest

inner
      (↑(LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E))
        (↑LinearMap.toContinuousLinearMap
          ((↑(↑(LinearMap.llcomp ℝ E 𝒜 ℝ) ↑AlternatingMap.constLinearEquivOfIsEmpty.symm) ∘
              ↑AlternatingMap.curryLeftLinearMap)
            (↑(AlternatingMap.curryLeft (↑(AlternatingMap.curryLeft (Orientation.volumeForm ω)) u)) v))))
      w =?= inner (↑(LinearIsometryEquiv.symm (InnerProductSpace.toDual ?m.412649 ?m.412650)) ?m.412656) ?m.412655

[Patrick Massot]

In particular simp does not go far enough to try to synthesize any instance at all.

[Matthew Ballard]

Eric Wieser said:

Presumably simp is using stricter reducibility settings than rw

I thought these were the same defaults - they both only unfold things tagged with reducible. Am I wrong?

[Matthew Ballard]

Patrick Massot said:

Does anyone understand the output with trace.Meta.isDefEq in the failing simp?

I’ve seen this behavior where it wants to try to the unify the world with Propmost recently in Lean4#2461 and the related discussion.

I don’t understand it heuristically

[Eric Wieser]

Matthew Ballard said:

Eric Wieser said:

Presumably simp is using stricter reducibility settings than rw

I thought these were the same defaults - they both only unfold things tagged with reducible. Am I wrong?

I think unification is allowed to unfold further

[Matthew Ballard]

Sorry, can you expand when you get a chance?

[Patrick Massot]

Trying to investigate the second issue, I can type

import Mathlib.Analysis.InnerProductSpace.Dual
import Mathlib.Analysis.InnerProductSpace.Orientation

/-! # The cross-product on an oriented real inner product space of dimension three -/


noncomputable section

open scoped RealInnerProductSpace

open FiniteDimensional

set_option synthInstance.checkSynthOrder false
attribute [local instance] fact_finiteDimensional_of_finrank_eq_succ
set_option synthInstance.checkSynthOrder true

variable (E : Type _) [NormedAddCommGroup E] [InnerProductSpace ℝ E]

/-- The identification of a finite-dimensional inner product space with its algebraic dual. -/
private def to_dual [FiniteDimensional ℝ E] : E ≃ₗ[ℝ] E →ₗ[ℝ] ℝ :=
  (InnerProductSpace.toDual ℝ E).toLinearEquiv ≪≫ₗ LinearMap.toContinuousLinearMap.symm

namespace Orientation

variable {E}
variable [Fact (finrank ℝ E = 3)] (ω : Orientation ℝ E (Fin 3))

/-- Linear map from `E` to `E →ₗ[ℝ] E` constructed from a 3-form `Ω` on `E` and an identification of
`E` with its dual.  Effectively, the Hodge star operation.  (Under appropriate hypotheses it turns
out that the image of this map is in `𝔰𝔬(E)`, the skew-symmetric operators, which can be identified
with `Λ²E`.) -/
def crossProduct : E →ₗ[ℝ] E →ₗ[ℝ] E := by
  let z : AlternatingMap ℝ E ℝ (Fin 0) ≃ₗ[ℝ] ℝ :=
    AlternatingMap.constLinearEquivOfIsEmpty.symm
  let y : AlternatingMap ℝ E ℝ (Fin 1) →ₗ[ℝ] E →ₗ[ℝ] ℝ :=
    LinearMap.llcomp ℝ E (AlternatingMap ℝ E ℝ (Fin 0)) ℝ z ∘ₗ AlternatingMap.curryLeftLinearMap
  let y' : AlternatingMap ℝ E ℝ (Fin 1) →ₗ[ℝ] E :=
    (LinearMap.llcomp ℝ (AlternatingMap ℝ E ℝ (Fin 1)) (E →ₗ[ℝ] ℝ) E (to_dual E).symm) y
  let u : AlternatingMap ℝ E ℝ (Fin 2) →ₗ[ℝ] E →ₗ[ℝ] E :=
    LinearMap.llcomp ℝ E (AlternatingMap ℝ E ℝ (Fin 1)) _ y' ∘ₗ AlternatingMap.curryLeftLinearMap
  exact u ∘ₗ AlternatingMap.curryLeftLinearMap (n := 2) ω.volumeForm

local infixl:100 "×₃" => ω.crossProduct

theorem crossProduct_apply_self (v : E) : v×₃v = 0 := by simp [crossProduct]

set_option quotPrecheck false in
notation "𝒜" => AlternatingMap ℝ E ℝ (Fin 0)
set_option quotPrecheck false in
notation "𝒜'" => AlternatingMap ℝ E ℝ (Fin (Nat.succ 0))

attribute [pp_dot] LinearEquiv.symm

lemma bar (φ : E →ₗ[ℝ] ℝ) (w: E) : @FunLike.coe (NormedSpace.Dual ℝ E) E (fun _ ↦ ℝ) ContinuousMapClass.toFunLike
  (@LinearMap.toContinuousLinearMap ℝ _ E _ _ _ _ _ ℝ _ _ _ _ to_dual.proof_11 _ _ _ φ) w = (↑φ : E → ℝ) w := by
  rfl


theorem inner_crossProduct_apply (u v w : E) : ⟪u×₃v, w⟫ = ω.volumeForm ![u, v, w] := by
  simp only [crossProduct]
  simp only [to_dual]
  simp only [LinearEquiv.trans_symm]
  simp only [LinearEquiv.symm_symm]
  simp only [LinearIsometryEquiv.toLinearEquiv_symm]
  simp only [AlternatingMap.curryLeftLinearMap_apply]
  simp only [LinearMap.coe_comp]
  simp only [Function.comp_apply]
  simp only [LinearMap.llcomp_apply]
  simp only [LinearEquiv.coe_coe]
  simp only [LinearEquiv.trans_apply]
  simp only [LinearIsometryEquiv.coe_toLinearEquiv]
  simp only [AlternatingMap.curryLeftLinearMap_apply]
  simp only [LinearMap.coe_comp]
  rw [InnerProductSpace.toDual_symm_apply]
  set F' : 𝒜' → E →ₗ[ℝ] ℝ := (LinearMap.llcomp ℝ E 𝒜 ℝ ↑(AlternatingMap.constLinearEquivOfIsEmpty.symm : 𝒜 ≃ₗ[ℝ] ℝ)) ∘ AlternatingMap.curryLeftLinearMap
  set K := (AlternatingMap.curryLeft ((AlternatingMap.curryLeft (volumeForm ω)) u)) v
  have := bar (F' K) w
  trans F' K w
  · beta_reduce at this ⊢
    -- rw [this] -- fails
    set_option trace.Meta.isDefEq true in exact this
  sorry

But the isDefEq trace is showing nothing at all. I mean every line in the trace looks like a syntactic equality.

[Matthew Ballard]

Did you try it on branch#mrb/normed_dual_reducible to compare?

[Patrick Massot]

No, I'm actively avoiding doing this because I don't want to fix that proof, I want to understand how to debug the next 100 proofs that will fail in incomprehensible ways.

[Patrick Massot]

I guess part of what I want a version of convert that works up to syntactic equality, reporting any mismatch that would block rw.

[Matthew Ballard]

I meant to compare the traces and see if the difference is insightful in some way.

Is there a useful trace class for rewrite?

[Matthew Ballard]

I really only know print line debugging in general

[Jireh Loreaux]

@Patrick Massot I think you can do that with convert (config := {transparency := .reducible}) h, at least, #help tactic convert seems to suggest something like this

[Jireh Loreaux]

I'm not sure how helpful the error messages will be.

[Patrick Massot]

Jireh, nice try but it closes the goal without reporting anything.

[Patrick Massot]

Update: set_option trace.Meta.isDefEq true in rw [this] does report stuff about the failure. It starts with funny lines like

found messy fun a => ℝ =?= fun x => ℝ

but then at some point it gets to

[] ❌ NormedSpace.Dual ℝ E =?= E →L[ℝ] ℝ ▼
        [] ❌ NormedSpace.Dual =?= @ContinuousLinearMap
        [onFailure] ❌ NormedSpace.Dual ℝ E =?= E →L[ℝ] ℝ
        [onFailure] ❌ NormedSpace.Dual ℝ E =?= E →L[ℝ] ℝ

which indeed seems to be useful.

[Patrick Massot]

I'd be interested in learning what is messy about fun a => ℝ =?= fun x => ℝ.

[Jireh Loreaux]

Is messy something about mdata? I think someone recently found a bug in dsimp about mdata.

[Jireh Loreaux]

I'm just grasping at straws.

[Matthew Ballard]

Does grepping in core give any doc info?

[Patrick Massot]

The message about messy DefEq comes from here.

[Patrick Massot]

So it's printed because info.dependsOnHigherOrderOutParam || info.higherOrderOutParam.

[Eric Wieser]

Are the x and a the same time in that "messy" equality?

[Patrick Massot]

You mean the same type? Yes. This was also my first guess.

[Eric Wieser]

Patrick Massot said:

Eric, I answered some of your questions at #6998

I'm back at Lean and had a look at this (and left some more comments); something very nasty seems to be happening with typeclass inference, where somehow things in an unrelated part of the expression affect whether an instance is found

[Patrick Massot]

Should we still merge or do you want to get to the bottom of this?

[Eric Wieser]

I think we should add a TODO comment that references a new github issue, then merge

[Patrick Massot]

Ok, I delegated the PR.

[Eric Wieser]

I've made a thread with a not-mathlib-free mwe at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Typeclass.20search.20is.20affected.20by.20other.20subexpressions/near/389833387

[Patrick Massot]

What is the status of #6998 @Eric Wieser and @Matthew Ballard? I lost track.

[Eric Wieser]

It's waiting on the undergrad.yml fix, and also a tracking issue to be created for the noncomputable hack needed to keep down the maxrss performance metric.

[Matthew Ballard]

Sorry. I’ve been out of commission for a bit. Back at it soon.