diff --git a/src/Lean/AddDecl.lean b/src/Lean/AddDecl.lean index e0352eeccd..8ce153734b 100644 --- a/src/Lean/AddDecl.lean +++ b/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 diff --git a/src/Lean/Elab/Deriving/Basic.lean b/src/Lean/Elab/Deriving/Basic.lean index 4d3854216a..3274d1773a 100644 --- a/src/Lean/Elab/Deriving/Basic.lean +++ b/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 diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index 8d971f11c2..0c369f54f2 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/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 diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 493eeb530c..de3dbacba0 100644 --- a/src/Lean/Parser/Command.lean +++ b/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 ") >> diff --git a/src/lake/Lake/Config/ConfigDecl.lean b/src/lake/Lake/Config/ConfigDecl.lean index 7d53ae3766..5a658a01c8 100644 --- a/src/lake/Lake/Config/ConfigDecl.lean +++ b/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) diff --git a/src/lake/Lake/Config/FacetConfig.lean b/src/lake/Lake/Config/FacetConfig.lean index 77a474f21e..8ec8607d49 100644 --- a/src/lake/Lake/Config/FacetConfig.lean +++ b/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 diff --git a/src/lake/Lake/Config/Script.lean b/src/lake/Lake/Config/Script.lean index f4fe9387d5..cac7cd6d42 100644 --- a/src/lake/Lake/Config/Script.lean +++ b/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 diff --git a/tests/lean/defInst.lean b/tests/lean/defInst.lean index c614d3528d..3d4b8a1d9f 100644 --- a/tests/lean/defInst.lean +++ b/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) diff --git a/tests/lean/defInst.lean.expected.out b/tests/lean/defInst.lean.expected.out index 24ffb629c5..f26ebc53bc 100644 --- a/tests/lean/defInst.lean.expected.out +++ b/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 diff --git a/tests/lean/run/derivingDelta.lean b/tests/lean/run/derivingDelta.lean new file mode 100644 index 0000000000..743c5db071 --- /dev/null +++ b/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