chore: refactor with new where syntax and auto-quantification

src/Lean/Data/Json/FromToJson.lean

@@ -36,11 +36,11 @@ instance : ToJson Int := ⟨fun n => Json.num n⟩
 instance : FromJson String := ⟨Json.getStr?⟩
 instance : ToJson String := ⟨fun s => s⟩
 
-instance {α : Type u} [FromJson α] : FromJson (Array α) := ⟨fun
+instance [FromJson α] : FromJson (Array α) := ⟨fun
   | Json.arr a => a.mapM fromJson?
   | _ => none⟩
 
-instance {α : Type u} [ToJson α] : ToJson (Array α) :=
+instance [ToJson α] : ToJson (Array α) :=
   ⟨fun a => Json.arr (a.map toJson)⟩
 
 namespace Json
@@ -54,13 +54,13 @@ instance : ToJson Structured := ⟨fun
   | Structured.arr a => arr a
   | Structured.obj o => obj o⟩
 
-def toStructured? {α : Type} [ToJson α] (v : α) : Option Structured :=
+def toStructured? [ToJson α] (v : α) : Option Structured :=
   fromJson? (toJson v)
 
 def getObjValAs? (j : Json) (α : Type u) [FromJson α] (k : String) : Option α :=
   (j.getObjVal? k).bind fromJson?
 
-def opt {α : Type u} [ToJson α] (k : String) : Option α → List (String × Json)
+def opt [ToJson α] (k : String) : Option α → List (String × Json)
   | some o => [⟨k, toJson o⟩]
   | none   => []
 

src/Lean/Data/Json/Parser.lean

@@ -34,7 +34,7 @@ partial def skipWs (it : String.Iterator) : String.Iterator :=
    it
 
 @[inline]
-protected def pure {α : Type} (a : α) : Quickparse α := fun it =>
+protected def pure (a : α) : Quickparse α := fun it =>
   success it a
 
 @[inline]
@@ -44,7 +44,7 @@ protected def bind {α β : Type} (f : Quickparse α) (g : α → Quickparse β)
   | error pos msg => error pos msg
 
 @[inline]
-def fail {α : Type} (msg : String) : Quickparse α := fun it =>
+def fail (msg : String) : Quickparse α := fun it =>
   error it msg
 
 @[inline]

src/Lean/Data/Json/Printer.lean

@@ -45,8 +45,6 @@ def renderString (s : String) : String :=
   "\"" ++ escape s ++ "\""
 
 section
-variables {α : Type}
-
 @[specialize]
 partial def render : Json → Format
   | null       => "null"

src/Lean/Data/JsonRpc.lean

@@ -38,8 +38,7 @@ inductive ErrorCode where
   | requestCancelled
   | contentModified
 
-instance : FromJson ErrorCode := ⟨fun j =>
-  match j with
+instance : FromJson ErrorCode := ⟨fun
   | num (-32700 : Int) => ErrorCode.parseError
   | num (-32600 : Int) => ErrorCode.invalidRequest
   | num (-32601 : Int) => ErrorCode.methodNotFound
@@ -53,8 +52,7 @@ instance : FromJson ErrorCode := ⟨fun j =>
   | num (-32801 : Int) => ErrorCode.contentModified
   | _  => none⟩
 
-instance : ToJson ErrorCode := ⟨fun e =>
-  match e with
+instance : ToJson ErrorCode := ⟨fun
   | ErrorCode.parseError           => (-32700 : Int)
   | ErrorCode.invalidRequest       => (-32600 : Int)
   | ErrorCode.methodNotFound       => (-32601 : Int)
@@ -213,19 +211,19 @@ def readNotificationAs (h : FS.Stream) (nBytes : Nat) (expectedMethod : String)
 def writeMessage (h : FS.Stream) (m : Message) : IO Unit :=
   h.writeJson (toJson m)
 
-def writeRequest {α : Type} [ToJson α] (h : FS.Stream) (id : RequestID) (method : String) (params : α) : IO Unit :=
+def writeRequest [ToJson α] (h : FS.Stream) (id : RequestID) (method : String) (params : α) : IO Unit :=
   h.writeMessage (Message.request id method (fromJson? (toJson params)))
 
-def writeNotification {α : Type} [ToJson α] (h : FS.Stream) (method : String) (params : α) : IO Unit :=
+def writeNotification [ToJson α] (h : FS.Stream) (method : String) (params : α) : IO Unit :=
   h.writeMessage (Message.notification method (fromJson? (toJson params)))
 
-def writeResponse {α : Type} [ToJson α] (h : FS.Stream) (id : RequestID) (r : α) : IO Unit :=
+def writeResponse [ToJson α] (h : FS.Stream) (id : RequestID) (r : α) : IO Unit :=
   h.writeMessage (Message.response id (toJson r))
 
 def writeResponseError (h : FS.Stream) (id : RequestID) (code : ErrorCode) (message : String) : IO Unit :=
   h.writeMessage (Message.responseError id code message none)
 
-def writeResponseErrorWithData {α : Type} [ToJson α] (h : FS.Stream) (id : RequestID) (code : ErrorCode) (message : String) (data : α) : IO Unit :=
+def writeResponseErrorWithData [ToJson α] (h : FS.Stream) (id : RequestID) (code : ErrorCode) (message : String) (data : α) : IO Unit :=
   h.writeMessage (Message.responseError id code message (toJson data))
 
 end IO.FS.Stream

src/Lean/Data/Lsp/Basic.lean

@@ -18,7 +18,8 @@ namespace Lsp
 
 open Json
 
-structure CancelParams := (id : JsonRpc.RequestID)
+structure CancelParams where
+  id : JsonRpc.RequestID
 
 instance CancelParams.hasFromJson : FromJson CancelParams :=
   ⟨fun j => do
@@ -29,7 +30,6 @@ instance CancelParams.hasToJson : ToJson CancelParams :=
   ⟨fun o => mkObj $
     ⟨"id", toJson o.id⟩ :: []⟩
 
-
 abbrev DocumentUri := String
 
 /-- We adopt the convention that zero-based UTF-16 positions as sent by LSP clients

src/Lean/Data/Lsp/Communication.lean

@@ -65,19 +65,19 @@ def writeLspMessage (h : FS.Stream) (msg : Message) : IO Unit := do
   h.putStr (header ++ j)
   h.flush
 
-def writeLspRequest {α : Type} [ToJson α] (h : FS.Stream) (id : RequestID) (method : String) (params : α) : IO Unit :=
+def writeLspRequest [ToJson α] (h : FS.Stream) (id : RequestID) (method : String) (params : α) : IO Unit :=
   writeLspMessage h (Message.request id method (fromJson? (toJson params)))
 
-def writeLspNotification {α : Type} [ToJson α] (h : FS.Stream) (method : String) (r : α) : IO Unit :=
+def writeLspNotification [ToJson α] (h : FS.Stream) (method : String) (r : α) : IO Unit :=
   writeLspMessage h (Message.notification method (fromJson? (toJson r)))
 
-def writeLspResponse {α : Type} [ToJson α] (h : FS.Stream) (id : RequestID) (r : α) : IO Unit :=
+def writeLspResponse [ToJson α] (h : FS.Stream) (id : RequestID) (r : α) : IO Unit :=
   writeLspMessage h (Message.response id (toJson r))
 
 def writeLspResponseError (h : FS.Stream) (id : RequestID) (code : ErrorCode) (message : String) : IO Unit :=
   writeLspMessage h (Message.responseError id code message none)
 
-def writeLspResponseErrorWithData {α : Type} [ToJson α] (h : FS.Stream) (id : RequestID) (code : ErrorCode) (message : String) (data : α) : IO Unit :=
+def writeLspResponseErrorWithData [ToJson α] (h : FS.Stream) (id : RequestID) (code : ErrorCode) (message : String) (data : α) : IO Unit :=
   writeLspMessage h (Message.responseError id code message (toJson data))
 
 end Lsp

src/Lean/Server/AsyncList.lean

@@ -13,16 +13,13 @@ universes u v
 /-- An async IO list is like a lazy list but instead of being *unevaluated* `Thunk`s,
 lazy tails are `Task`s *being evaluated asynchronously*. A tail can signal the end
 of computation (successful or due to a failure) with a terminating value of type `ε`. -/
-inductive AsyncList (ε : Type u) (α : Type v) :=
+inductive AsyncList (ε : Type u) (α : Type v) where
   | cons (hd : α) (tl : AsyncList ε α)
   | asyncCons (hd : α) (tl : Task $ Except ε $ AsyncList ε α)
   | nil
 
 namespace AsyncList
 
--- TODO(WN): IO doesn't like universes :(
-variables {ε : Type} {α : Type}
-
 instance asyncListInhabited : Inhabited (AsyncList ε α) := ⟨nil⟩
 
 -- TODO(WN): tail-recursion without forcing sync?

src/Lean/Server/FileWorker.lean

@@ -55,7 +55,7 @@ private def sendDiagnostics (h : FS.Stream) (uri : DocumentUri) (version : Nat)
 private def logSnapContent (s : Snapshot) (text : FileMap) : IO Unit :=
   IO.eprintln $ "`" ++ text.source.extract s.beginPos (s.endPos-1) ++ "`"
 
-inductive TaskError :=
+inductive TaskError where
   | aborted
   | eof
   | ioError (e : IO.Error)
@@ -93,13 +93,13 @@ def unfoldCmdSnaps (h : FS.Stream) (uri : DocumentUri) (version : Nat) (contents
 /-- A document editable in the sense that we track the environment
 and parser state after each command so that edits can be applied
 without recompiling code appearing earlier in the file. -/
-structure EditableDocument :=
-  (version : Nat)
-  (text : FileMap)
+structure EditableDocument where
+  version : Nat
+  text : FileMap
   /- The first snapshot is that after the header. -/
-  (headerSnap : Snapshot)
+  headerSnap : Snapshot
   /- Subsequent snapshots occur after each command. -/
-  (cmdSnaps : AsyncList TaskError Snapshot)
+  cmdSnaps : AsyncList TaskError Snapshot
 
 namespace EditableDocument
 
@@ -153,10 +153,10 @@ open JsonRpc
 
 abbrev PendingRequestMap := RBMap RequestID (Task (Except IO.Error Unit)) (fun a b => Decidable.decide (a < b))
 
-structure ServerContext :=
-  (hIn hOut : FS.Stream)
-  (docRef : IO.Ref EditableDocument)
-  (pendingRequestsRef : IO.Ref PendingRequestMap)
+structure ServerContext where
+  hIn hOut : FS.Stream
+  docRef : IO.Ref EditableDocument
+  pendingRequestsRef : IO.Ref PendingRequestMap
 
 abbrev ServerM := ReaderT ServerContext IO
 
@@ -217,7 +217,7 @@ def handleNotification (method : String) (params : Json) : ServerM Unit := do
   | "$/cancelRequest"        => handle CancelParams handleCancelRequest
   | _                        => throwServerError $ "Got unsupported notification method: " ++ method
 
-def queueRequest {α : Type} (id : RequestID) (handler : α → EditableDocument → IO Unit) (params : α)
+def queueRequest (id : RequestID) (handler : α → EditableDocument → IO Unit) (params : α)
 : ServerM Unit := do
   let requestTask ← asTask (handler params (←getDocument))
   updatePendingRequests (fun pendingRequests => pendingRequests.insert id requestTask)

src/Lean/Server/Utils.lean

@@ -9,7 +9,7 @@ import Lean.Data.Lsp
 
 namespace IO
 
-def throwServerError {α : Type} (err : String) : IO α :=
+def throwServerError (err : String) : IO α :=
   throw (userError err)
 
 namespace FS
@@ -107,7 +107,6 @@ end Lean
 namespace List
 
 universe u
-variable {α : Type u}
 
 def takeWhile (p : α → Bool) : List α → List α
   | []       => []

src/Lean/Server/Watchdog.lean

@@ -67,10 +67,10 @@ open Lsp
 open JsonRpc
 open System.FilePath
 
-structure OpenDocument :=
-  (version : Nat)
-  (text : FileMap)
-  (headerAst : Syntax)
+structure OpenDocument where
+  version : Nat
+  text : FileMap
+  headerAst : Syntax
 
 def workerCfg : Process.StdioConfig :=
   { stdin  := Process.Stdio.piped,
@@ -80,11 +80,11 @@ def workerCfg : Process.StdioConfig :=
     stderr := Process.Stdio.null }
 
 -- Events that a forwarding task of a worker signals to the main task
-inductive WorkerEvent :=
+inductive WorkerEvent where
   | terminated
   | crashed (e : IO.Error)
 
-inductive WorkerState :=
+inductive WorkerState where
   -- The watchdog can detect a crashed file worker in two places: When trying to send a message to the file worker
   -- and when reading a request reply.
   -- In the latter case, the forwarding task terminates and delegates a `crashed` event to the main task.
@@ -97,13 +97,13 @@ inductive WorkerState :=
 
 abbrev PendingRequestMap := RBMap RequestID JsonRpc.Message (fun a b => Decidable.decide (a < b))
 
-structure FileWorker :=
-  (doc : OpenDocument)
-  (proc : Process.Child workerCfg)
-  (commTask : Task WorkerEvent)
-  (state : WorkerState)
+structure FileWorker where
+  doc : OpenDocument
+  proc : Process.Child workerCfg
+  commTask : Task WorkerEvent
+  state : WorkerState
   -- NOTE: this should not be mutated outside of namespace FileWorker
-  (pendingRequestsRef : IO.Ref PendingRequestMap)
+  pendingRequestsRef : IO.Ref PendingRequestMap
 
 namespace FileWorker
 
@@ -124,10 +124,10 @@ def readMessage (fw : FileWorker) : IO JsonRpc.Message := do
 def writeMessage (fw : FileWorker) (msg : JsonRpc.Message) : IO Unit :=
   writeLspMessage fw.stdin msg
 
-def writeNotification {α : Type} [ToJson α] (fw : FileWorker) (method : String) (param : α) : IO Unit :=
+def writeNotification [ToJson α] (fw : FileWorker) (method : String) (param : α) : IO Unit :=
   writeLspNotification fw.stdin method param
 
-def writeRequest {α : Type} [ToJson α] (fw : FileWorker) (id : RequestID) (method : String) (param : α) : IO Unit := do
+def writeRequest [ToJson α] (fw : FileWorker) (id : RequestID) (method : String) (param : α) : IO Unit := do
   writeLspRequest fw.stdin id method param
   fw.pendingRequestsRef.modify $ fun pendingRequests =>
     pendingRequests.insert id (Message.request id method (Json.toStructured? param))
@@ -140,13 +140,13 @@ end FileWorker
 
 abbrev FileWorkerMap := RBMap DocumentUri FileWorker (fun a b => Decidable.decide (a < b))
 
-structure ServerContext :=
-  (hIn hOut : FS.Stream)
-  (hLog : FS.Stream)
-  (fileWorkersRef : IO.Ref FileWorkerMap)
+structure ServerContext where
+  hIn hOut : FS.Stream
+  hLog : FS.Stream
+  fileWorkersRef : IO.Ref FileWorkerMap
   /- We store these to pass them to workers. -/
-  (initParams : InitializeParams)
-  (workerPath : String)
+  initParams : InitializeParams
+  workerPath : String
 
 abbrev ServerM := ReaderT ServerContext IO
 
@@ -339,7 +339,7 @@ def shutdown : ServerM Unit := do
   fileWorkers.forM (fun id _ => terminateFileWorker id)
   fileWorkers.forM (fun _ fw => do let _ ← IO.wait fw.commTask)
 
-inductive ServerEvent :=
+inductive ServerEvent where
   | WorkerEvent (uri : DocumentUri) (fw : FileWorker) (ev : WorkerEvent)
   | ClientMsg (msg : JsonRpc.Message)
   | ClientError (e : IO.Error)