feat: updates to classes

Manual/Language/Classes/InstanceSynth.lean

@@ -49,64 +49,12 @@ The search for instance implicit arguments may make use of the implicit argument
 
 Instance implicit search begins with the type of the instance implicit parameter.
 This type must be the application of a type class to zero or more arguments; these argument values may be known or unknown when search begins.
-If an argument to a class is unknown, the search process will not instantiate it unless the corresponding parameter is marked as an "out" parameter, explicitly making it an output of the instance synthesis routine.
+If an argument to a class is unknown, the search process will not instantiate it unless the corresponding parameter is {ref "class-output-parameters"}[marked as an output parameter], explicitly making it an output of the instance synthesis routine.
 
 Search may succeed, fail, or get stuck; a stuck search may occur when an unknown argument value becoming known might enable progress to be made.
 Stuck searches may be re-invoked when the elaborator has discovered one of the previously-unknown implicit arguments.
 If this does not occur, stuck searches become failures.
 
-::::example "Out Parameters and Stuck Search"
-:::keepEnv
-This serialization framework provides a way to convert values to some underlying storage type:
-```lean
-class Serialize (input output : Type) where
-  ser : input → output
-export Serialize (ser)
-
-instance : Serialize Nat String where
-  ser n := toString n
-
-instance [Serialize α γ] [Serialize β γ] [Append γ] :
-    Serialize (α × β) γ where
-  ser
-    | (x, y) => ser x ++ ser y
-```
-
-In this example, the output type is unknown.
-```lean (error := true) (name := noOutputType)
-example := ser (2, 3)
-```
-Instance synthesis can't select the {lean}`Serialize Nat String` instance, and thus the {lean}`Append String` instance, because that would require instantiating the output type as {lean}`String`, so the search gets stuck:
-```leanOutput noOutputType
-typeclass instance problem is stuck, it is often due to metavariables
-  Serialize (Nat × Nat) ?m.16
-```
-One way to fix the problem is to supply an expected type:
-```lean
-example : String := ser (2, 3)
-```
-:::
-:::keepEnv
-The other is to make the output type into an output parameter:
-```lean
-class Serialize (input : Type) (output : outParam Type) where
-  ser : input → output
-export Serialize (ser)
-
-instance : Serialize Nat String where
-  ser n := toString n
-
-instance [Serialize α γ] [Serialize β γ] [Append γ] :
-    Serialize (α × β) γ where
-  ser
-    | (x, y) => ser x ++ ser y
-```
-Now, instance synthesis is free to select the {lean}`Serialize Nat String` instance, which solves the unknown implicit `output` parameter of {name}`ser`:
-```lean
-example := ser (2, 3)
-```
-:::
-::::
 
 # Candidate Instances
 
@@ -161,8 +109,16 @@ The local instance is selected instead of the global one:
 
 # Instance Parameters and Synthesis
 
-Parameters to instances may be explicit, implicit, or instance-implicit.
-If they are instance implicit, then they induce further instance searching, while explicit or implicit parameters must be solved by unification.
+The search process for instances is largely governed by class parameters.
+Type classes take a certain number of parameters, and instances are tried during the search when their choice of parameters is compatible with those in the class type for which the instance is being synthesized.
+Here, classes can be seen as relations between types, and instances as governing which types are related.
+An instance synthesis problem consists of instantiations of parameters to a class.
+
+Parameters are not limited to classes.
+Instances themselves may also take parameters, but the role of instances' parameters in instance synthesis is very different.
+Instances' parameters represent either variables that may be instantiated by instance synthesis or further synthesis work to be done before the instance can be used.
+In particular, parameters to instances may be explicit, implicit, or instance-implicit.
+If they are instance implicit, then they induce further recursive instance searching, while explicit or implicit parameters must be solved by unification.
 
 ::::keepEnv
 :::example "Implicit and Explicit Parameters to Instances"
@@ -186,9 +142,80 @@ In the output, both the explicit argument {lean}`Nat` and the implicit argument
 ::::
 
 # Output Parameters
+%%%
+tag := "class-output-parameters"
+%%%
+
+By default, the parameters of a type class are considered to be _inputs_ to the search process.
+If the parameters are not known, then the search process gets stuck, because choosing an instance would require the parameters to have values that match those in the instance.
+In some cases, the choice of one parameter should cause an automatic choice of another; for example, the overloaded membership predicate type class {name}`Membership` treats the type of elements of a data structure as an output, so that the type of element can be determined by the type of data structure at a use site, instead of requiring that there be sufficient type annotations to determine both types prior to starting instance synthesis.
+
+```signature (show := false)
+-- Test the above claim
+Membership.{u, v} (α : outParam (Type u)) (γ : Type v) : Type (max u v)
+```
+
+Type class parameters can be declared as outputs by wrapping their types in the {name}`outParam` {tech}[gadget].
+When a class parameter is an output, instance synthesis will not require that it be known.
+If it is unknown, and a candidate instance matches the input parameters, then that instance is selected; the instance's assignment of the output parameter becomes its value.
+If it is known, then only instances that match the already-known value are considered.
 
 {docstring outParam}
 
+
+::::example "Output Parameters and Stuck Search"
+:::keepEnv
+This serialization framework provides a way to convert values to some underlying storage type:
+```lean
+class Serialize (input output : Type) where
+  ser : input → output
+export Serialize (ser)
+
+instance : Serialize Nat String where
+  ser n := toString n
+
+instance [Serialize α γ] [Serialize β γ] [Append γ] :
+    Serialize (α × β) γ where
+  ser
+    | (x, y) => ser x ++ ser y
+```
+
+In this example, the output type is unknown.
+```lean (error := true) (name := noOutputType)
+example := ser (2, 3)
+```
+Instance synthesis can't select the {lean}`Serialize Nat String` instance, and thus the {lean}`Append String` instance, because that would require instantiating the output type as {lean}`String`, so the search gets stuck:
+```leanOutput noOutputType
+typeclass instance problem is stuck, it is often due to metavariables
+  Serialize (Nat × Nat) ?m.16
+```
+One way to fix the problem is to supply an expected type:
+```lean
+example : String := ser (2, 3)
+```
+:::
+:::keepEnv
+The other is to make the output type into an output parameter:
+```lean
+class Serialize (input : Type) (output : outParam Type) where
+  ser : input → output
+export Serialize (ser)
+
+instance : Serialize Nat String where
+  ser n := toString n
+
+instance [Serialize α γ] [Serialize β γ] [Append γ] :
+    Serialize (α × β) γ where
+  ser
+    | (x, y) => ser x ++ ser y
+```
+Now, instance synthesis is free to select the {lean}`Serialize Nat String` instance, which solves the unknown implicit `output` parameter of {name}`ser`:
+```lean
+example := ser (2, 3)
+```
+:::
+::::
+
 {docstring semiOutParam}
 
 

Manual/Meta/Lean.lean

@@ -303,10 +303,18 @@ def Block.signature : Block where
 declare_syntax_cat signature_spec
 syntax ("def" <|> "theorem")? declId declSig : signature_spec
 
+structure SignatureConfig where
+  «show» : Bool := true
+
+def SignatureConfig.parse [Monad m] [MonadError m] [MonadLiftT CoreM m] : ArgParse m SignatureConfig :=
+  SignatureConfig.mk <$>
+    ((·.getD true) <$> .named `show .bool true)
+
+
 @[code_block_expander signature]
 def signature : CodeBlockExpander
   | args, str => do
-    ArgParse.done.run args
+    let {«show»} ← SignatureConfig.parse.run args
     let altStr ← parserInputString str
 
     match Parser.runParserCategory (← getEnv) `signature_spec altStr (← getFileName) with
@@ -325,7 +333,10 @@ def signature : CodeBlockExpander
       let ((hls, _, _, _), st') ← ((SubVerso.Examples.checkSignature name sig).run cmdCtx).run cmdState
       setInfoState st'.infoState
 
-      pure #[← `(Block.other {Block.signature with data := ToJson.toJson $(quote (Highlighted.seq hls))} #[Block.code $(quote str.getString)])]
+      if «show» then
+        pure #[← `(Block.other {Block.signature with data := ToJson.toJson $(quote (Highlighted.seq hls))} #[Block.code $(quote str.getString)])]
+      else
+        pure #[]
 
 @[block_extension signature]
 def signature.descr : BlockDescr where