[padator]

Not sure you really need GADTs for the instruction set. A separate arg8 and arg16 ADT types would be enough, so you would have | Add8 of arg8 * arg8

[linoscope]

Hi, author here. Yeah, I thought the same and tried that too, but it failed due to the same reason mentioned in the "Problem with the definition using variants" section. Namely, the return value type of `read_arg` would not be uniquely determinable. We CAN define separate `read_arg8` for `read_arg16` for the `arg8` and `arg16` respectively, but I thought the GADT solution was more clean.