feat: Better handling of unused args in typeclass resolution

src/Lean/Meta/SynthInstance.lean

@@ -138,6 +138,36 @@ partial def normExpr (e : Expr) : M Expr := do
 
 end MkTableKey
 
+def removeUnusedArguments (mctx : MetavarContext) (mvar : Expr) : MetaM (Option (Prod Expr Expr)) :=
+withMCtx mctx do
+let E <- inferType mvar
+let E <- instantiateMVars E
+match E with
+  | Expr.forallE .. => forallTelescope E fun xs b => do
+    -- if (b.getAppFn.constName! == `SciLean.IsSmooth) ∨ (b.getAppFn.constName! == `SciLean.IsLin) then
+      let mut ys : List Expr := []
+      for x in xs do
+        if (b.containsFVar x.fvarId!) then
+          ys := ys.concat x
+
+      if xs.size != ys.length then
+        let E' ← mkForallFVars ys.toArray b
+
+        -- Creates transformer that takes (e' : E') and produces (e : E)
+        let fvarId <- mkFreshFVarId
+        let lctx := (<- getLCtx).mkLocalDecl fvarId `redf E'
+        let fvar := mkFVar fvarId
+        let transformer <-
+          withLCtx lctx #[] do
+            mkLambdaFVars (fvar::xs.toList).toArray (mkAppN fvar ys.toArray)
+        some (E', transformer)
+      else
+        none
+    -- else
+    --   none
+  | _ => none
+
+
 /- Remark: `mkTableKey` assumes `e` does not contain assigned metavariables. -/
 def mkTableKey (mctx : MetavarContext) (e : Expr) : Expr :=
   MkTableKey.normExpr e mctx |>.run' {}
@@ -432,7 +462,34 @@ def consume (cNode : ConsumerNode) : SynthM Unit :=
      let key ← mkTableKeyFor cNode.mctx mvar
      let entry? ← findEntry? key
      match entry? with
-     | none       => newSubgoal cNode.mctx key mvar waiter
+     | none       => do
+       match (<- removeUnusedArguments cNode.mctx mvar) with
+       | none => newSubgoal cNode.mctx key mvar waiter
+       | some (M', trans) =>
+         let key' <- mkTableKey cNode.mctx M'
+         let entry'? <- findEntry? key'
+         match entry'? with
+         | none => do
+           let (mctx', mvar') <-
+             withMCtx cNode.mctx do
+               let mvar' <- mkFreshExprMVar M'
+               (<- getMCtx, mvar')
+           newSubgoal mctx' key' mvar' (Waiter.consumerNode {cNode with mctx := mctx', subgoals := mvar'::cNode.subgoals })
+         | some entry' => do
+
+           let answers' ← entry'.answers.mapM 
+             λ a => 
+               withMCtx cNode.mctx do
+                 let answr ← instantiateMVars a.result.expr
+                 let trAnswr ← whnf (mkApp trans answr)
+                 let trAnswrType ← inferType trAnswr
+                 { a with result := {a.result with expr := trAnswr},
+                          resultType := trAnswrType }
+
+           modify fun s =>
+           { s with
+             resumeStack  := answers'.foldl (fun s answer => s.push (cNode, answer)) s.resumeStack,
+             tableEntries := s.tableEntries.insert key' { entry' with waiters := entry'.waiters.push waiter } }
      | some entry => modify fun s =>
        { s with
          resumeStack  := entry.answers.foldl (fun s answer => s.push (cNode, answer)) s.resumeStack,