chore: remove unused deriving handler argument syntax (#5265)

As far as I can tell, the ability to pass a structure instance to a
deriving handler is not actually used in practice. It didn't seem to be
used in the test suite, at least.

Do we want to remove this, or do we want to use and document it? This PR
removes it, but that's not something I feel strongly about - but seeing
if it breaks Mathlib is a useful data point.

src/Lean/Elab/BuiltinEvalCommand.lean

@@ -137,7 +137,7 @@ private def mkFormat (e : Expr) : MetaM Expr := do
       if let .const name _ := (← whnf (← inferType e)).getAppFn then
         try
           trace[Elab.eval] "Attempting to derive a 'Repr' instance for '{.ofConstName name}'"
-          liftCommandElabM do applyDerivingHandlers ``Repr #[name] none
+          liftCommandElabM do applyDerivingHandlers ``Repr #[name]
           resetSynthInstanceCache
           return ← mkRepr e
         catch ex =>

src/Lean/Elab/Deriving/Basic.lean

@@ -63,7 +63,10 @@ def processDefDeriving (className : Name) (declName : Name) : TermElabM Bool :=
 
 end Term
 
-def DerivingHandler := (typeNames : Array Name) → (args? : Option (TSyntax ``Parser.Term.structInst)) → CommandElabM Bool
+def DerivingHandler := (typeNames : Array Name) → CommandElabM Bool
+
+/-- Deprecated - `DerivingHandler` no longer assumes arguments -/
+@[deprecated DerivingHandler (since := "2024-09-09")]
 def DerivingHandlerNoArgs := (typeNames : Array Name) → CommandElabM Bool
 
 builtin_initialize derivingHandlersRef : IO.Ref (NameMap (List DerivingHandler)) ← IO.mkRef {}
@@ -73,25 +76,21 @@ as well as the syntax of a `with` argument, if present.
 
 For example, `deriving instance Foo with fooArgs for Bar, Baz` invokes
 ``fooHandler #[`Bar, `Baz] `(fooArgs)``. -/
-def registerDerivingHandlerWithArgs (className : Name) (handler : DerivingHandler) : IO Unit := do
+def registerDerivingHandler (className : Name) (handler : DerivingHandler) : IO Unit := do
   unless (← initializing) do
     throw (IO.userError "failed to register deriving handler, it can only be registered during initialization")
   derivingHandlersRef.modify fun m => match m.find? className with
     | some handlers => m.insert className (handler :: handlers)
     | none => m.insert className [handler]
 
-/-- Like `registerBuiltinDerivingHandlerWithArgs` but ignoring any `with` argument. -/
-def registerDerivingHandler (className : Name) (handler : DerivingHandlerNoArgs) : IO Unit := do
-  registerDerivingHandlerWithArgs className fun typeNames _ => handler typeNames
-
 def defaultHandler (className : Name) (typeNames : Array Name) : CommandElabM Unit := do
   throwError "default handlers have not been implemented yet, class: '{className}' types: {typeNames}"
 
-def applyDerivingHandlers (className : Name) (typeNames : Array Name) (args? : Option (TSyntax ``Parser.Term.structInst)) : CommandElabM Unit := do
+def applyDerivingHandlers (className : Name) (typeNames : Array Name) : CommandElabM Unit := do
   match (← derivingHandlersRef.get).find? className with
   | some handlers =>
     for handler in handlers do
-      if (← handler typeNames args?) then
+      if (← handler typeNames) then
         return ()
     defaultHandler className typeNames
   | none => defaultHandler className typeNames
@@ -101,37 +100,36 @@ private def tryApplyDefHandler (className : Name) (declName : Name) : CommandEla
     Term.processDefDeriving className declName
 
 @[builtin_command_elab «deriving»] def elabDeriving : CommandElab
-  | `(deriving instance $[$classes $[with $argss?]?],* for $[$declNames],*) => do
+  | `(deriving instance $[$classes],* for $[$declNames],*) => do
      let declNames ← liftCoreM <| declNames.mapM realizeGlobalConstNoOverloadWithInfo
-     for cls in classes, args? in argss? do
+     for cls in classes do
        try
          let className ← liftCoreM <| realizeGlobalConstNoOverloadWithInfo cls
          withRef cls do
-           if declNames.size == 1 && args?.isNone then
+           if declNames.size == 1 then
              if (← tryApplyDefHandler className declNames[0]!) then
                return ()
-           applyDerivingHandlers className declNames args?
+           applyDerivingHandlers className declNames
        catch ex =>
          logException ex
   | _ => throwUnsupportedSyntax
 
 structure DerivingClassView where
   ref : Syntax
   className : Name
-  args? : Option (TSyntax ``Parser.Term.structInst)
 
 def getOptDerivingClasses (optDeriving : Syntax) : CoreM (Array DerivingClassView) := do
   match optDeriving with
-  | `(Parser.Command.optDeriving| deriving $[$classes $[with $argss?]?],*) =>
+  | `(Parser.Command.optDeriving| deriving $[$classes],*) =>
     let mut ret := #[]
-    for cls in classes, args? in argss? do
+    for cls in classes do
       let className ← realizeGlobalConstNoOverloadWithInfo cls
-      ret := ret.push { ref := cls, className := className, args? }
+      ret := ret.push { ref := cls, className := className }
     return ret
   | _ => return #[]
 
 def DerivingClassView.applyHandlers (view : DerivingClassView) (declNames : Array Name) : CommandElabM Unit :=
-  withRef view.ref do applyDerivingHandlers view.className declNames view.args?
+  withRef view.ref do applyDerivingHandlers view.className declNames
 
 builtin_initialize
   registerTraceClass `Elab.Deriving

src/Lean/Parser/Command.lean

@@ -173,7 +173,7 @@ def «example»        := leading_parser
 def ctor             := leading_parser
   atomic (optional docComment >> "\n| ") >>
   ppGroup (declModifiers true >> rawIdent >> optDeclSig)
-def derivingClasses  := sepBy1 (group (ident >> optional (" with " >> ppIndent Term.structInst))) ", "
+def derivingClasses  := sepBy1 ident ", "
 def optDeriving      := leading_parser
   optional (ppLine >> atomic ("deriving " >> notSymbol "instance") >> derivingClasses)
 def computedField    := leading_parser

stage0/src/stdlib_flags.h

@@ -8,7 +8,7 @@ options get_default_options() {
     // switch to `true` for ABI-breaking changes affecting meta code
     opts = opts.update({"interpreter", "prefer_native"}, false);
     // switch to `true` for changing built-in parsers used in quotations
-    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false);
+    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, true);
     // toggling `parseQuotWithCurrentStage` may also require toggling the following option if macros/syntax
     // with custom precheck hooks were affected
     opts = opts.update({"quotPrecheck"}, true);