feat: make delta deriving more robust and handle binders (#9800)

This PR improves the delta deriving handler, giving it the ability to
process definitions with binders, as well as the ability to recursively
unfold definitions. Furthermore, delta deriving now tries all explicit
non-out-param arguments to a class, and it can handle "mixin" instance
arguments. The `deriving` syntax has been changed to accept general
terms, which makes it possible to derive specific instances with for
example `deriving OfNat _ 1` or `deriving Module R`. The class is
allowed to be a pi type, to add additional hypotheses; here is a Mathlib
example:
```lean
def Sym (α : Type*) (n : ℕ) :=
  { s : Multiset α // Multiset.card s = n }
deriving [DecidableEq α] → DecidableEq _
```
This underscore stands for where `Sym α n` may be inserted, which is
necessary when `→` is used. The `deriving instance` command can refer to
scoped variables when delta deriving as well. Breaking change: the
derived instance's name uses the `instance` command's name generator,
and the new instance is added to the current namespace.

This closes
[mathlib4#380](https://github.com/leanprover-community/mathlib4/issues/380).

src/Lean/AddDecl.lean

@@ -177,8 +177,8 @@ where
       catch _ => pure ()
 
 
-def addAndCompile (decl : Declaration) : CoreM Unit := do
+def addAndCompile (decl : Declaration) (logCompileErrors : Bool := true) : CoreM Unit := do
   addDecl decl
-  compileDecl decl
+  compileDecl decl (logErrors := logCompileErrors)
 
 end Lean

src/Lean/Elab/Deriving/Basic.lean

@@ -6,8 +6,10 @@ Authors: Leonardo de Moura, Wojciech Nawrocki
 module
 
 prelude
+public import Lean.Elab.App
 public import Lean.Elab.Command
 public import Lean.Elab.DeclarationRange
+public import Lean.Elab.DeclNameGen
 public meta import Lean.Parser.Command
 
 public section
@@ -18,53 +20,189 @@ open Command
 namespace Term
 open Meta
 
-/-- Result for `mkInst?` -/
-structure MkInstResult where
-  instVal   : Expr
-  instType  : Expr
-  outParams : Array Expr := #[]
+/-- Result for `mkInst` -/
+private structure MkInstResult where
+  instType   : Expr
+  instVal    : Expr
+
+private def throwDeltaDeriveFailure (className declName : Name) (msg? : Option MessageData) (suffix : MessageData := "") : MetaM α :=
+  let suffix := if let some msg := msg? then m!", {msg}{suffix}" else m!".{suffix}"
+  throwError "Failed to delta derive `{.ofConstName className}` instance for `{.ofConstName declName}`{suffix}"
 
 /--
-  Construct an instance for `className out₁ ... outₙ type`.
-  The method support classes with a prefix of `outParam`s (e.g. `MonadReader`). -/
-private partial def mkInst? (className : Name) (type : Expr) : MetaM (Option MkInstResult) := do
-  let rec go? (instType instTypeType : Expr) (outParams : Array Expr) : MetaM (Option MkInstResult) := do
-    let instTypeType ← whnfD instTypeType
-    unless instTypeType.isForall do
-      return none
-    let d := instTypeType.bindingDomain!
-    if d.isOutParam then
-      let mvar ← mkFreshExprMVar d
-      go? (mkApp instType mvar) (instTypeType.bindingBody!.instantiate1 mvar) (outParams.push mvar)
-    else
-      unless (← isDefEqGuarded (← inferType type) d) do
-        return none
-      let instType ← instantiateMVars (mkApp instType type)
-      let instVal ← synthInstance instType
-      return some { instVal, instType, outParams }
-  let instType ← mkConstWithFreshMVarLevels className
-  go? instType (← inferType instType) #[]
+Constructs an instance of the class `classExpr` by figuring out the correct position to insert `val`
+to create a type `className ... val ...` such that there is already an instance for it.
+The `declVal` argument is the value to use in place of `val` when creating the new instance.
 
-def processDefDeriving (className : Name) (declName : Name) : TermElabM Bool := do
-  try
-    let ConstantInfo.defnInfo info ← getConstInfo declName | return false
-    let some result ← mkInst? className info.value | return false
-    let instTypeNew := mkApp result.instType.appFn! (Lean.mkConst declName (info.levelParams.map mkLevelParam))
-    Meta.check instTypeNew
-    let instName ← liftMacroM <| mkUnusedBaseName (declName.appendBefore "inst" |>.appendAfter className.getString!)
-    addAndCompile <| Declaration.defnDecl {
-      name        := instName
-      levelParams := info.levelParams
-      type        := (← instantiateMVars instTypeNew)
-      value       := (← instantiateMVars result.instVal)
-      hints       := info.hints
-      safety      := info.safety
-    }
-    addInstance instName AttributeKind.global (eval_prio default)
-    addDeclarationRangesFromSyntax instName (← getRef)
-    return true
-  catch _ =>
-    return false
+Heuristics:
+- `val` must not use an outParam.
+- `val` should use an explicit parameter, or a parameter that has already been given a value.
+- If there are multiple explicit parameters, we try each possibility.
+- If the class has instance arguments, we require that they be synthesizable while synthesizing this instance.
+  While we could allow synthesis failure and abstract such instances,
+  we leave such conditional instances to be defined by users.
+- If this all fails and `val` is a constant application, we try unfolding it once and try again.
+
+For example, when deriving `MonadReader (ρ : outParam (Type u)) (m : Type u → Type v)`,
+we will skip `ρ` and try using `m`.
+
+Note that we try synthesizing instances even if there are still metavariables in the type.
+If that succeeds, then one can abstract those metavariables and create a parameterized instance.
+The abstraction is not done by this function.
+
+Expects to be run with an empty message log.
+-/
+private partial def mkInst (classExpr : Expr) (declName : Name) (declVal val : Expr) : TermElabM MkInstResult := do
+  let classExpr ← whnfCore classExpr
+  let cls := classExpr.getAppFn
+  let (xs, bis, _) ← forallMetaTelescopeReducing (← inferType cls)
+  for x in xs, y in classExpr.getAppArgs do
+    x.mvarId!.assign y
+  let classExpr := mkAppN cls xs
+  let some className ← isClass? classExpr
+    | throwError "Failed to delta derive instance for `{.ofConstName declName}`, not a class:{indentExpr classExpr}"
+  let mut instMVars := #[]
+  for x in xs, bi in bis do
+    if !(← x.mvarId!.isAssigned) then
+      -- Assumption: assigned inst implicits are already either solved or registered as synthetic
+      if bi.isInstImplicit then
+        x.mvarId!.setKind .synthetic
+        instMVars := instMVars.push x.mvarId!
+  let instVal ← mkFreshExprMVar classExpr (kind := .synthetic)
+  instMVars := instMVars.push instVal.mvarId!
+  let rec go (val : Expr) : TermElabM MkInstResult := do
+    let val ← whnfCore val
+    trace[Elab.Deriving] "Looking for arguments to `{classExpr}` that can be used for the value{indentExpr val}"
+    -- Save the metacontext so that we can try each option in turn
+    let state ← saveState
+    let valTy ← inferType val
+    let mut anyDefEqSuccess := false
+    let mut messages : MessageLog := {}
+    for x in xs, bi in bis, i in 0...xs.size do
+      unless bi.isExplicit do
+        continue
+      let decl ← x.mvarId!.getDecl
+      if decl.type.isOutParam then
+        continue
+      unless ← isMVarApp x do
+        /-
+        This is an argument supplied by the user, and it's not a `_`.
+        This is to avoid counterintuitive behavior, like in the following example.
+        Because `MyNat` unifies with `Nat`, it would otherwise generate an `HAdd MyNat Nat Nat` instance.
+        Instead it generates an `HAdd Nat MyNat Nat` instance.
+        ```
+        def MyNat := Nat
+        deriving instance HAdd Nat for MyNat
+        ```
+        Likely neither of these is the intended result, but the second is more justifiable.
+        It's possible to have it return `MyNat` using `deriving instance HAdd Nat _ MyNat for MyNat`.
+        -/
+        continue
+      unless ← isDefEqGuarded decl.type valTy <&&> isDefEqGuarded x val do
+        restoreState state
+        continue
+      anyDefEqSuccess := true
+      trace[Elab.Deriving] "Argument {i} gives option{indentExpr classExpr}"
+      try
+        -- Finish elaboration
+        synthesizeAppInstMVars instMVars classExpr
+        Term.synthesizeSyntheticMVarsNoPostponing
+      catch ex =>
+        trace[Elab.Deriving] "Option for argument {i} failed"
+        logException ex
+        messages := messages ++ (← Core.getMessageLog)
+        restoreState state
+        continue
+      if (← MonadLog.hasErrors) then
+        -- Sometimes elaboration only logs errors
+        trace[Elab.Deriving] "Option for argument {i} failed, logged errors"
+        messages := messages ++ (← Core.getMessageLog)
+        restoreState state
+        continue
+      -- Success
+      trace[Elab.Deriving] "Argument {i} option succeeded{indentExpr classExpr}"
+      -- Create the type for the declaration itself.
+      let xs' := xs.set! i declVal
+      let instType := mkAppN cls xs'
+      return { instType, instVal }
+    try
+      if let some val' ← unfoldDefinition? val then
+        return ← withTraceNode `Elab.Deriving (fun _ => return m!"Unfolded value to {val'}") <| go val'
+    catch ex =>
+      if !messages.hasErrors then
+        throw ex
+      Core.resetMessageLog
+    if !anyDefEqSuccess then
+      throwDeltaDeriveFailure className declName (m!"the class has no explicit non-out-param parameters where\
+        {indentExpr declVal}\n\
+        can be inserted.")
+    else
+      Core.setMessageLog (messages ++ (← Core.getMessageLog))
+      throwDeltaDeriveFailure className declName none
+        (.note m!"Delta deriving tries the following strategies: \
+            (1) inserting the definition into each explicit non-out-param parameter of a class and \
+            (2) unfolding definitions further.")
+  go val
+
+/--
+Delta deriving handler. Creates an instance of class `classStx` for `decl`.
+The elaborated class expression may be underapplied (e.g. `Decidable` instead of `Decidable _`),
+and may be `decl`.
+If unfolding `decl` results in an underapplied lambda, then this enters the body of the lambda.
+We prevent `classStx` from referring to these local variables; instead it's expected that one uses section variables.
+
+This function can handle being run from within a nontrivial local context,
+and it uses `mkValueTypeClosure` to construct the final instance.
+-/
+def processDefDeriving (classStx : Syntax) (decl : Expr) : TermElabM Unit := do
+  let decl ← whnfCore decl
+  let .const declName _ := decl.getAppFn
+    | throwError "Failed to delta derive instance, expecting a term of the form `C ...` where `C` is a constant, given{indentExpr decl}"
+  -- When the definition is private, the deriving handler will need access to the private scope,
+  -- and we make sure to put the instance in the private scope.
+  withoutExporting (when := isPrivateName declName) do
+  let ConstantInfo.defnInfo info ← getConstInfo declName
+    | throwError "Failed to delta derive instance, `{declName}` is not a definition."
+  let value := info.value.beta decl.getAppArgs
+  let result : Closure.MkValueTypeClosureResult ←
+    -- Assumption: users intend delta deriving to apply to the body of a definition, even if in the source code
+    -- the function is written as a lambda expression.
+    -- Furthermore, we don't use `forallTelescope` because users want to derive instances for monads.
+    lambdaTelescope value fun xs value => withoutErrToSorry do
+      let decl := mkAppN decl xs
+      -- Make these local variables inaccessible.
+      let lctx ← xs.foldlM (init := ← getLCtx) fun lctx x => do
+        pure <| lctx.setUserName x.fvarId! (← mkFreshUserName <| (lctx.find? x.fvarId!).get!.userName)
+      withLCtx' lctx do
+        let msgLog ← Core.getMessageLog
+        Core.resetMessageLog
+        try
+          -- We need to elaborate the class within this context to ensure metavariables can unify with `xs`.
+          let classExpr ← elabTerm classStx none
+          synthesizeSyntheticMVars (postpone := .partial)
+          if (← MonadLog.hasErrors) then
+            throwAbortTerm
+          -- We allow `classExpr` to be a pi type, to support giving more hypotheses to the derived instance.
+          -- (Possibly `classExpr` is not a type due to being underapplied, but `forallTelescopeReducing` tolerates this.)
+          -- We don't reduce because of abbreviations such as `DecidableEq`
+          forallTelescope classExpr fun _ classExpr => do
+            let result ← mkInst classExpr declName decl value
+            Closure.mkValueTypeClosure result.instType result.instVal (zetaDelta := true)
+        finally
+          Core.setMessageLog (msgLog ++ (← Core.getMessageLog))
+  let env ← getEnv
+  let mut instName := (← getCurrNamespace) ++ (← NameGen.mkBaseNameWithSuffix "inst" result.type)
+  -- We don't have a facility to let users override derived names, so make an unused name if needed.
+  instName ← liftMacroM <| mkUnusedBaseName instName
+  -- Make the instance private if the declaration is private.
+  if isPrivateName declName then
+    instName := mkPrivateName env instName
+  let hints := ReducibilityHints.regular (getMaxHeight env result.value + 1)
+  let decl ← mkDefinitionValInferringUnsafe instName result.levelParams.toList result.type result.value hints
+  addAndCompile (logCompileErrors := !(← read).isNoncomputableSection) <| Declaration.defnDecl decl
+  trace[Elab.Deriving] "Derived instance `{.ofConstName instName}`"
+  addInstance instName AttributeKind.global (eval_prio default)
+  addDeclarationRangesFromSyntax instName (← getRef)
 
 end Term
 
@@ -85,39 +223,60 @@ def registerDerivingHandler (className : Name) (handler : DerivingHandler) : IO
     | some handlers => m.insert className (handler :: handlers)
     | none => m.insert className [handler]
 
-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) : CommandElabM Unit := do
   -- When any of the types are private, the deriving handler will need access to the private scope
   -- (and should also make sure to put its outputs in the private scope).
   withoutExporting (when := typeNames.any isPrivateName) do
-  withTraceNode `Elab.Deriving (fun _ => return m!"running deriving handlers for '{className}'") do
+  withTraceNode `Elab.Deriving (fun _ => return m!"running deriving handlers for `{.ofConstName className}`") do
     match (← derivingHandlersRef.get).find? className with
     | some handlers =>
       for handler in handlers do
         if (← handler typeNames) then
           return ()
-      defaultHandler className typeNames
-    | none => defaultHandler className typeNames
+      throwError "None of the deriving handlers for class `{.ofConstName className}` applied to \
+        {.andList <| typeNames.toList.map (m!"`{.ofConstName ·}`")}"
+    | none => throwError "No deriving handlers have been implemented for class `{.ofConstName className}`"
 
-private def tryApplyDefHandler (className : Name) (declName : Name) : CommandElabM Bool :=
-  liftTermElabM do
-    Term.processDefDeriving className declName
+private def applyDefHandler (classStx : Syntax) (declExpr : Expr) : TermElabM Unit :=
+  withTraceNode `Elab.Deriving (fun _ => return m!"running delta deriving handler for `{classStx}` and definition `{declExpr}`") do
+    Term.processDefDeriving classStx declExpr
+
+private def elabDefDeriving (classes decls : Array Syntax) :
+    CommandElabM Unit := runTermElabM fun _ => do
+  for decl in decls do
+    withRef decl <| withLogging do
+      let declExpr ←
+        if decl.isIdent then
+          let declName ← realizeGlobalConstNoOverload decl
+          let info ← getConstInfo declName
+          unless info.isDefinition do
+            throwError (m!"Declaration `{.ofConstName declName}` is not a definition."
+              ++ .note m!"When any declaration is a definition, this command goes into delta deriving mode, \
+                    which applies only to definitions. \
+                    Delta deriving unfolds definitions and infers pre-existing instances.")
+          -- Use the declaration's level parameters, to ensure the instance is fully universe polymorphic
+          mkConstWithLevelParams declName
+        else
+          Term.elabTermAndSynthesize decl none
+      for classStx in classes do
+        withLogging <| applyDefHandler classStx declExpr
 
 @[builtin_command_elab «deriving»] def elabDeriving : CommandElab
-  | `(deriving instance $[$classes],* for $[$declNames],*) => do
-     let declNames ← liftCoreM <| declNames.mapM realizeGlobalConstNoOverloadWithInfo
-     for cls in classes do
-       try
-         let className ← liftCoreM <| realizeGlobalConstNoOverloadWithInfo cls
-         withRef cls do
-           if declNames.size == 1 then
-             if (← tryApplyDefHandler className declNames[0]!) then
-               return ()
-           applyDerivingHandlers className declNames
-       catch ex =>
-         logException ex
+  | `(deriving instance $[$classes],* for $[$decls],*) => do
+    let decls : Array Syntax := decls
+    if decls.all Syntax.isIdent then
+      let declNames ← liftCoreM <| decls.mapM (realizeGlobalConstNoOverloadWithInfo ·)
+      -- If any of the declarations are definitions, then we commit to delta deriving.
+      let infos ← declNames.mapM getConstInfo
+      if infos.any (·.isDefinition) then
+        elabDefDeriving classes decls
+      else
+        -- Otherwise, we commit to using deriving handlers.
+        let classNames ← liftCoreM <| classes.mapM (realizeGlobalConstNoOverloadWithInfo ·)
+        for className in classNames, classIdent in classes do
+          withRef classIdent <| withLogging <| applyDerivingHandlers className declNames
+    else
+      elabDefDeriving classes decls
   | _ => throwUnsupportedSyntax
 
 structure DerivingClassView where

src/Lean/Elab/MutualDef.lean

@@ -1303,12 +1303,24 @@ where
       addPreDefinitions preDefs
   processDeriving (headers : Array DefViewElabHeader) := do
     for header in headers, view in views do
-      if let some classNamesStx := view.deriving? then
-        for classNameStx in classNamesStx do
-          let className ← realizeGlobalConstNoOverload classNameStx
-          withRef classNameStx do
-            unless (← processDefDeriving className header.declName) do
-              throwError "failed to synthesize instance '{className}' for '{header.declName}'"
+      if let some classStxs := view.deriving? then
+        for classStx in classStxs do
+          withRef classStx <| withLogging <| withLCtx {} {} do
+            /-
+            Assumption: users intend delta deriving to apply to the body of a definition, even if in the source code
+            the function is written as a lambda expression.
+            Furthermore, we don't use `forallTelescope` because users want to derive instances for monads.
+
+            We enter the local context of this body, which is where `classStx` will be elaborated.
+
+            Small complication: we don't know the correlation between the section variables
+            and the parameters in the declaration, so for now we do not allow `classStx`
+            to refer to section variables that were not included.
+            -/
+            let info ← getConstInfo header.declName
+            lambdaTelescope info.value! fun xs _ => do
+              let decl := mkAppN (.const header.declName (info.levelParams.map mkLevelParam)) xs
+              processDefDeriving classStx decl
 
 /--
 Logs a snapshot task that waits for the entire snapshot tree in `defsParsedSnap` and then logs a

src/Lean/Parser/Command.lean

@@ -161,7 +161,7 @@ def whereStructInst  := leading_parser
 def «abbrev»         := leading_parser
   "abbrev " >> declId >> ppIndent optDeclSig >> declVal
 def optDefDeriving   :=
-  optional (ppDedent ppLine >> atomic ("deriving " >> notSymbol "instance") >> sepBy1 ident ", ")
+  optional (ppDedent ppLine >> atomic ("deriving " >> notSymbol "instance") >> sepBy1 termParser ", ")
 def definition     := leading_parser
   "def " >> recover declId skipUntilWsOrDelim >> ppIndent optDeclSig >> declVal >> optDefDeriving
 def «theorem»        := leading_parser
@@ -181,7 +181,7 @@ def «example»        := leading_parser
 def ctor             := leading_parser
   atomic (optional docComment >> "\n| ") >>
   ppGroup (declModifiers true >> rawIdent >> optDeclSig)
-def derivingClasses  := sepBy1 ident ", "
+def derivingClasses  := sepBy1 (withForbidden "for" termParser) ", "
 def optDeriving      := leading_parser
   optional (ppLine >> atomic ("deriving " >> notSymbol "instance") >> derivingClasses)
 def computedField    := leading_parser
@@ -253,7 +253,7 @@ def «structure»          := leading_parser
   («abbrev» <|> definition <|> «theorem» <|> «opaque» <|> «instance» <|> «axiom» <|> «example» <|>
    «inductive» <|> classInductive <|> «structure»)
 @[builtin_command_parser] def «deriving»     := leading_parser
-  "deriving " >> "instance " >> derivingClasses >> " for " >> sepBy1 (recover ident skip) ", "
+  "deriving " >> "instance " >> derivingClasses >> " for " >> sepBy1 (recover termParser skip) ", "
 def sectionHeader := leading_parser
   optional ("@[" >> nonReservedSymbol "expose" >> "] ") >>
   optional ("public ") >>

src/lake/Lake/Config/ConfigDecl.lean

@@ -126,6 +126,7 @@ abbrev InputFileDecl := KConfigDecl InputFile.configKind
 /-- A inpurt directory declaration from a configuration written in Lean. -/
 abbrev InputDirDecl := KConfigDecl InputDir.configKind
 
-deriving instance TypeName for
-  LeanLibDecl, LeanExeDecl,
-  InputFileDecl, InputDirDecl
+instance : TypeName LeanLibDecl := unsafe (.mk _ ``LeanLibDecl)
+instance : TypeName LeanExeDecl := unsafe (.mk _ ``LeanExeDecl)
+instance : TypeName InputFileDecl := unsafe (.mk _ ``InputFileDecl)
+instance : TypeName InputDirDecl := unsafe (.mk _ ``InputDirDecl)

src/lake/Lake/Config/FacetConfig.lean

@@ -87,8 +87,9 @@ abbrev LibraryFacetConfig := KFacetConfig LeanLib.facetKind
 /-- A library facet declaration from a configuration file. -/
 abbrev LibraryFacetDecl := NamedConfigDecl LibraryFacetConfig
 
-deriving instance TypeName for
-  ModuleFacetDecl, PackageFacetDecl, LibraryFacetDecl
+instance : TypeName ModuleFacetDecl := unsafe (.mk _ ``ModuleFacetDecl)
+instance : TypeName PackageFacetDecl := unsafe (.mk _ ``PackageFacetDecl)
+instance : TypeName LibraryFacetDecl := unsafe (.mk _ ``LibraryFacetDecl)
 
 /-- A library facet's declarative configuration. -/
 abbrev LeanLibFacetConfig := LibraryFacetConfig

src/lake/Lake/Config/Script.lean

@@ -22,7 +22,7 @@ also equipped with information about the Lake configuration.
 -/
 abbrev ScriptFn := (args : List String) → ScriptM ExitCode
 
-deriving instance TypeName for ScriptFn
+instance : TypeName ScriptFn := unsafe (.mk _ ``ScriptFn)
 
 /--
 A package `Script` is a `ScriptFn` definition that is

tests/lean/defInst.lean

@@ -28,7 +28,7 @@ def mkBoo (s : String) : Boo :=
 def M := ReaderT String (StateT Nat IO)
   deriving Monad, MonadState, MonadReader
 
-#print instMMonad
+#print instMonadM
 
 def action : M Unit := do
   modify (· + 1)

tests/lean/defInst.lean.expected.out

@@ -10,5 +10,5 @@ fun x y => x == y : Foo → Foo → Bool
 false
 true
 true
-def instMMonad : Monad M :=
+def instMonadM : Monad M :=
 ReaderT.instMonad

tests/lean/run/derivingDelta.lean

@@ -0,0 +1,321 @@
+/-!
+# Tests for delta deriving of instances for definitions
+
+In this file we test both `deriving` clauses on definitions and `deriving instance` commands.
+-/
+
+/-!
+Simple definition, body has instance immediately.
+-/
+def P1 : Prop := 1 = 1
+deriving Decidable
+
+def P1' : Prop := 1 = 1
+deriving instance Decidable for P1'
+
+/-!
+Derived instances go into the current namespace at the point of derivation.
+-/
+def MyLib.MyUnit := Unit
+deriving Inhabited
+deriving instance Nonempty for MyLib.MyUnit
+
+/-- info: MyLib.instInhabitedMyUnit -/
+#guard_msgs in #synth Inhabited MyLib.MyUnit
+/-- info: instNonemptyMyUnit -/
+#guard_msgs in #synth Nonempty MyLib.MyUnit
+
+/-!
+Parameterized instance, deriving goes underneath `fun x y => ...`
+-/
+def Rel (x y : Nat) : Prop := x = y
+deriving Decidable
+
+def Rel' (x y : Nat) : Prop := x = y
+deriving instance Decidable for Rel'
+
+/-!
+Another parameterized instance.
+-/
+def MyFin (n : Nat) : Type := Fin n
+deriving DecidableEq
+
+/-!
+Multiple unfolding
+-/
+def MyFin' (n : Nat) : Type := MyFin (n + 1)
+deriving Inhabited
+
+/-!
+Outparam support. Skips outparams.
+-/
+def IOReader (α : Type) := ReaderT α IO
+deriving MonadReader
+
+def MyList (α : Type) := List α
+deriving Membership
+
+/-!
+Allows metavariables in the class. These get abstracted.
+-/
+def MyNat := Nat
+deriving OfNat
+
+/--
+info: def instOfNatMyNat : (_x_1 : Nat) → OfNat MyNat _x_1 :=
+fun _x_1 => instOfNatNat _x_1
+-/
+#guard_msgs in #print instOfNatMyNat
+
+/-!
+Explicit parameterization
+-/
+deriving instance (n : Nat) → OfNat _ n for MyNat
+/--
+info: def instOfNatMyNat_1 : (n : Nat) → OfNat MyNat n :=
+fun n => instOfNatNat n
+-/
+#guard_msgs in #print instOfNatMyNat_1
+
+/-!
+Explicit parameterization using section variables
+-/
+section
+variable (m : Nat)
+deriving instance OfNat _ m for MyNat
+end
+/--
+info: def instOfNatMyNat_2 : (m : Nat) → OfNat MyNat m :=
+fun m => instOfNatNat m
+-/
+#guard_msgs in #print instOfNatMyNat_2
+
+/-!
+Can synthesize specific OfNat instances.
+-/
+def MyNat' := Nat
+deriving OfNat _ 1
+
+deriving instance OfNat _ 2 for MyNat'
+
+/-- info: instOfNatMyNat'OfNatNat -/
+#guard_msgs in #synth OfNat MyNat' 1
+/-- info: instOfNatMyNat'OfNatNat_1 -/
+#guard_msgs in #synth OfNat MyNat' 2
+/--
+error: failed to synthesize
+  OfNat MyNat' 3
+
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+-/
+#guard_msgs in #synth OfNat MyNat' 3
+
+/-!
+Don't unify with nontrivial arguments supplied by the user.
+Without the nontriviality check, would get `instHAddMyNatNat : HAdd MyNat Nat Nat`.
+-/
+deriving instance HAdd Nat for MyNat
+/-- info: instHAddNatMyNat : HAdd Nat MyNat Nat -/
+#guard_msgs in #check instHAddNatMyNat
+
+deriving instance HAdd _ Nat for MyNat
+/-- info: instHAddMyNatNat : HAdd MyNat Nat Nat -/
+#guard_msgs in #check instHAddMyNatNat
+
+/-!
+"Mixin" instances
+-/
+class C1 {α : Sort _} [DecidableEq α] (β : α → Type _)
+instance : C1 Fin := {}
+
+def MyFin'' := Fin
+deriving C1
+
+/--
+info: def instC1NatMyFin'' : @C1 Nat instDecidableEqNat MyFin'' :=
+instC1NatFin
+-/
+#guard_msgs in set_option pp.explicit true in #print instC1NatMyFin''
+
+/-!
+Can catch mixin failure
+-/
+instance (inst : DecidableEq (Type _)) : C1 List := {}
+
+/--
+error: failed to synthesize
+  DecidableEq (Type u_1)
+
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+---
+error: Failed to delta derive `C1` instance for `MyList'`.
+
+Note: Delta deriving tries the following strategies: (1) inserting the definition into each explicit non-out-param parameter of a class and (2) unfolding definitions further.
+-/
+#guard_msgs in
+def MyList' := List
+deriving C1
+
+/-!
+Can use explicit argument that's not the first.
+-/
+class OfNat' (n : Nat) (α : Type) where
+instance (n : Nat) : OfNat' n Int := {}
+def MyInt := Int
+deriving OfNat', OfNat
+/--
+info: def instOfNat'MyInt : (_x_1 : Nat) → OfNat' _x_1 MyInt :=
+fun _x_1 => instOfNat'Int _x_1
+-/
+#guard_msgs in #print instOfNat'MyInt
+/--
+info: def instOfNatMyInt : (_x_1 : Nat) → OfNat MyInt _x_1 :=
+fun _x_1 => instOfNat
+-/
+#guard_msgs in #print instOfNatMyInt
+
+/-!
+Deriving `Module` over different base rings.
+-/
+class Semiring (R : Type _) where
+class Module (R : Type _) [Semiring R] (α : Type _) where
+instance : Semiring Nat := {}
+instance : Semiring Int := {}
+opaque V : Type
+instance : Module Nat V := {}
+instance : Module Int V := {}
+
+def W := V
+deriving Module Nat, Module Int
+
+/-- info: instModuleNatW -/
+#guard_msgs in #synth Module Nat W
+/-- info: instModuleIntW -/
+#guard_msgs in #synth Module Int W
+
+/-!
+Deriving and making use of binders.
+-/
+instance (R : Type _) [Semiring R] : Module R R := {}
+def NewRing (R : Type _) [Semiring R] := R
+deriving Module R
+
+/--
+info: def instModuleNewRing.{u_1} : (R : Type u_1) → [inst : Semiring R] → Module R (NewRing R) :=
+fun R [Semiring R] => instModule R
+-/
+#guard_msgs in #print instModuleNewRing
+
+/-!
+`deriving instance` cannot make use of the definition's parameter names (they're introduced hygienically)
+-/
+/-- error: Unknown identifier `R` -/
+#guard_msgs in deriving instance Module R for NewRing
+
+/-!
+Can make use of section variables when using the `deriving instance` command.
+-/
+section
+variable (R : Type _) [Semiring R]
+def NewRing' (R : Type _) := R
+deriving instance Module R for NewRing' R
+
+/--
+info: def instModuleNewRing'.{u_1} : (R : Type u_1) → [inst : Semiring R] → Module R (NewRing' R) :=
+fun R [Semiring R] => instModule R
+-/
+#guard_msgs in #print instModuleNewRing'
+end
+
+/-!
+Multiple options, one works due to dependent types.
+-/
+class C2 (α : Sort _) (β : α) where
+instance : C2 Type Prop := {}
+-- set_option trace.Elab.Deriving true
+def Prop' := Prop
+deriving C2
+/--
+info: def instC2TypeProp' : C2 Type Prop' :=
+instC2TypeProp
+-/
+#guard_msgs in #print instC2TypeProp'
+
+/-!
+Error to mix both inductives and defs in the same `deriving instance` command.
+Rationale: none of the deriving handlers for inductives unfold definitions,
+so it is clearer if we make `deriving instance` have two distinct modes.
+-/
+inductive I1 | mk
+def D1 := Unit
+/--
+error: Declaration `I1` is not a definition.
+
+Note: When any declaration is a definition, this command goes into delta deriving mode, which applies only to definitions. Delta deriving unfolds definitions and infers pre-existing instances.
+-/
+#guard_msgs in deriving instance Inhabited for I1, D1
+deriving instance Inhabited for D1
+
+/-!
+No such class
+-/
+/-- error: Unknown identifier `NotAClass` -/
+#guard_msgs in deriving instance NotAClass for D1
+
+/-!
+Not a class
+-/
+/--
+error: Failed to delta derive instance for `D1`, not a class:
+  Nat
+-/
+#guard_msgs in deriving instance Nat for D1
+
+/-!
+No such definition
+-/
+/-- error: Unknown constant `NotADefinition` -/
+#guard_msgs in deriving instance Inhabited for NotADefinition
+
+/-!
+Delta deriving fails due to synthesis failure.
+-/
+/--
+error: failed to synthesize
+  Inhabited (Fin n)
+
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+---
+error: Failed to delta derive `Inhabited` instance for `D2`.
+
+Note: Delta deriving tries the following strategies: (1) inserting the definition into each explicit non-out-param parameter of a class and (2) unfolding definitions further.
+-/
+#guard_msgs in
+def D2 (n : Nat) := Fin n
+deriving Inhabited
+
+/--
+error: failed to synthesize
+  Inhabited (D2 n)
+
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+---
+error: Failed to delta derive `Inhabited` instance for `D2'`.
+
+Note: Delta deriving tries the following strategies: (1) inserting the definition into each explicit non-out-param parameter of a class and (2) unfolding definitions further.
+-/
+#guard_msgs in
+def D2' (n : Nat) := D2 n
+deriving Inhabited
+
+/-!
+Delta deriving fails due to no way to construct the class type.
+-/
+/--
+error: Failed to delta derive `Decidable` instance for `D3`, the class has no explicit non-out-param parameters where
+  D3
+can be inserted.
+-/
+#guard_msgs in
+def D3 := Bool
+deriving Decidable