Try type class synthesis as a fallback in type class specialization

Lean/Egg/Core/Gen/TcSpecs.lean

@@ -13,12 +13,17 @@ private partial def genSpecialization (rw : Rewrite) (dir : Direction) (missing
   while changed do
     changed := false
     for var in missing do
-      if let some inst ← findLocalDeclWithType? (← var.getType) then
-        var.assign (.fvar inst)
+      if let some inst ← instanceForType? (← var.getType) then
+        var.assign inst
         missing := missing.erase var
         changed := true
   let rw ← rw.instantiateMVars
   return if rw.validDirs.contains dir then rw else none
+where
+  instanceForType? (type : Expr) : MetaM (Option Expr) := do
+    if let some inst ← findLocalDeclWithType? type
+    then return (Expr.fvar inst)
+    else optional (synthInstance type)
 
 private def genTcSpecializationsForRw (rw : Rewrite) : MetaM Rewrites := do
   let missingOnLhs := rw.rhsMVars.tc.subtract rw.lhsMVars.tc

Lean/Egg/Tests/WIP.lean

@@ -54,3 +54,9 @@ example : True := by
 -- TODO: If we have a theorem like `(fun a b => a) x y = x`, it's only applicable in the forward
 --       direction. But once we β-reduce it, it's applicable in both directions. I think that can
 --       cause problems during reconstruction as we cannot reconstruct the assignment of `y`.
+
+
+
+-- TODO: Something about tc-specialization isn'T quite working yet.
+--       The first calc step in inv_eq_of_mul_eq_one_left should be doable with egg, but no tc-spec
+--       is generated.