fix: support non-type params in RpcEncoding

src/Lean/Server/Rpc/Deriving.lean

@@ -216,12 +216,15 @@ private def deriveInstance (typeName : Name) : CommandElabM Bool := do
 
       for param in params do
         let paramNm := (← getFVarLocalDecl param).userName
-        paramBinders := paramBinders.push (← `(bracketedBinder| ($(mkIdent paramNm))))
+        let ty ← PrettyPrinter.delab (← inferType param)
+        paramBinders := paramBinders.push (← `(bracketedBinder| ($(mkIdent paramNm) : $ty)))
+        let packet := mkIdent (← mkFreshUserName (paramNm.appendAfter "Packet"))
         -- only look for encodings for `Type` parameters
         if (← inferType param).isType then
-          let packet := mkIdent (← mkFreshUserName (paramNm.appendAfter "Packet"))
           packetParamBinders := packetParamBinders.push (← `(bracketedBinder| ($packet : Type)))
           encInstBinders := encInstBinders.push (← `(bracketedBinder| [RpcEncoding $(mkIdent paramNm) $packet]))
+        else
+          packetParamBinders := packetParamBinders.push paramBinders.back --(← `(bracketedBinder| ($packet : $ty)))
 
       return (paramBinders, packetParamBinders, encInstBinders)
 

tests/lean/derivingRpcEncoding.lean

@@ -89,3 +89,10 @@ inductive FooNested (α : Type) where
 #print FooNested.RpcEncodingPacket
 #check @FooNested.RpcEncodingPacket.a
 #eval test (FooNested BazInductive) (.a default #[default])
+
+inductive FooParam (n : Nat) where
+  | a : Nat → FooParam n
+  deriving RpcEncoding, Inhabited
+
+#check instRpcEncodingFooParamRpcEncodingPacket
+#eval test (FooParam 10) (.a 42)

tests/lean/derivingRpcEncoding.lean.expected.out

@@ -39,3 +39,5 @@ FooNested.RpcEncodingPacket.a : {αPacket : Type} →
 @FooNested.RpcEncodingPacket.a : {αPacket : Type} →
   αPacket → Array (FooNested.RpcEncodingPacket αPacket) → FooNested.RpcEncodingPacket αPacket
 ok: {"a": [{"baz": []}, [{"a": [{"baz": []}, []]}]]}
+instRpcEncodingFooParamRpcEncodingPacket : (n : Nat) → RpcEncoding (FooParam n) (FooParam.RpcEncodingPacket n)
+ok: {"a": 42}