[proposal]Make request parsing more robust

[Qiu233]

Currently the repl is parsing request json in a try-chain, which is very prone to errors.

For example, if we declare a new request:

structure CommandParse where
  env : Option Nat
  cmd : String
deriving ToJson, FromJson

and add it to the end of the chain, the function parse will never return CommandParse but always Command for cases meant to be CommandParse. This is because the parsing try of Command is preceding the CommandParse.

One workaround could be changing the field name cmd, so Command fails and CommandParse get its chance. But things would get messy rapidly as more requests are added.

It is interesting that this issue can be definitely solved with the aid of dependent types. The following is a simple example.

Proposal

structure StringLit (s : String) where
  val : String
  h : val = s

instance {s} : ToJson (StringLit s) where
  toJson _ := Json.str s

instance {s} : FromJson (StringLit s) where
  fromJson? json := do
    let x ← json.getStr?
    if h : x = s then
      return ⟨x, h⟩
    else
      throw s!"string literal mismatched, expected {s}, got {x}"

structure Request (type : String) where
  reqType : StringLit type

structure Command extends Request "run_command", CommandOptions where
  env : Option Nat
  cmd : String
deriving ToJson, FromJson

#eval toJson ({ reqType := ⟨"run_command", by rfl⟩, env := none, cmd := "", infotree := none : Command})

Here we make a new type StringLit to encode a String that is always some fixed value encoded in its type.
The type Request serves as the base type of all requests.
Whenever we declare a new request R, we just declare a structure R extending Request S for some string literal S. The automatically derived ToJson R and FromJson R ensure correctness of the field reqType, which disambiguates any two requests with different reqType.

Breaking changes

This will require the clients of REPL to modify their communication code.

If the proposal is acceptable, I would like to be assigned for it.