Don't generate tc proj rewrites which only reduce to Expr.proj

Lean/Egg/Core/Gen/TcProjs.lean

@@ -5,27 +5,29 @@ open Lean Meta
 
 namespace Egg
 
--- We expect the `args` to contain `numParams + 1` elements where the `numParams + 1`th argument is
--- the typeclass instance argument for `const`. Also, not arguments can contain loos bvars and the
--- final argument (the typeclass instance) can not be an mvar.
-structure TcProj where
-  const : Name
-  lvls  : List Level
-  args  : Array Expr
-  deriving BEq, Hashable
+abbrev TcProj := Expr
 
-abbrev TcProjIndex := HashMap TcProj Source
+private def TcProj.mk (const : Name) (args : Array Expr) (lvls : List Level) : TcProj :=
+  mkAppN (.const const lvls) args
 
 private def TcProj.reductionRewrite? (proj : TcProj) (src : Source) (beta eta : Bool) :
     MetaM (Option Rewrite) := do
-  let app := mkAppN (.const proj.const proj.lvls) proj.args
-  let reduced ← withReducibleAndInstances do reduceAll app
-  if app == reduced then return none
-  let eq ← mkEq app reduced
-  let proof ← mkEqRefl app
-  let some rw ← Rewrite.from? proof eq src beta eta | throwError "egg: internal error in 'TcProj.reductionRewrite'"
+  let reduced ← withReducibleAndInstances do reduceAll proj
+  -- Sometimes the only reduction performed by `reduceAll` is to replace a application of a type
+  -- class projection with its corresponding `Expr.proj` expression. In that case, no real reduction
+  -- has been performed for our purposes. To catch these cases, we normalize `reduced` (which
+  -- expands `Expr.proj`s) *before* checking for equality with `proj`, and in return *don't*
+  -- normalize again in `Rewrite.from?`.
+  let reducedNorm ← Egg.normalize reduced beta eta
+  if proj == reducedNorm then return none
+  let eq ← mkEq proj reducedNorm
+  let proof ← mkEqRefl proj
+  let some rw ← Rewrite.from? proof eq src beta eta (normalize := false)
+    | throwError "egg: internal error in 'TcProj.reductionRewrite?'"
   return rw
 
+abbrev TcProjIndex := HashMap TcProj Source
+
 private structure State where
   projs   : TcProjIndex    := ∅
   args    : Array Expr     := #[]
@@ -53,7 +55,7 @@ where
     unless info.fromClass && s.args.size > info.numParams do return s
     let args := s.args[:info.numParams + 1].toArray
     if args.back.isMVar || args.any (·.hasLooseBVars) then return s
-    let proj : TcProj := { const, lvls, args }
+    let proj := TcProj.mk const args lvls
     if s.covers proj
     then return s
     else return { s with projs := s.projs.insert proj (.tcProj src side? s.pos) }

Lean/Egg/Core/Rewrites.lean

@@ -26,12 +26,10 @@ structure _root_.Egg.Rewrite extends Congr where
 --
 -- Note: We must instantiate mvars of the rewrite's type. For an example that breaks otherwise, cf.
 --       https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Different.20elab.20results
---
--- TODO: We should probably only β- and η-reduce during normalization if the corresponding
---       configuration options are enabled.
-def from? (proof : Expr) (type : Expr) (src : Source) (beta eta : Bool) : MetaM (Option Rewrite) := do
+def from? (proof : Expr) (type : Expr) (src : Source) (beta eta : Bool) (normalize := true) :
+    MetaM (Option Rewrite) := do
   let mut (args, _, type) ← forallMetaTelescope (← instantiateMVars type)
-  type ← normalize type beta eta
+  type ← if normalize then Egg.normalize type beta eta else pure type
   let proof := mkAppN proof args
   let some cgr ← Congr.from? type | return none
   let lhsMVars ← MVars.collect cgr.lhs

Lean/Egg/Tactic/Trace.lean

@@ -19,7 +19,7 @@ nonrec def MVars.format (mvars : MVars) : MetaM Format := do
   let expr := format <| ← mvars.expr.toList.mapM (ppExpr <| Expr.mvar ·)
   let tc   := format <| ← mvars.tc.toList.mapM   (ppExpr <| Expr.mvar ·)
   let lvl  := format <|   mvars.lvl.toList.map   (Level.mvar ·)
-  return "expr: " ++ expr ++ "\n" ++ "class: " ++ tc ++ "\n" ++ "level: " ++ lvl
+  return "expr:  " ++ expr ++ "\n" ++ "class: " ++ tc ++ "\n" ++ "level: " ++ lvl
 
 def Directions.format : Directions → Format
   | .none     => "∅"