Deserialize: nullary constructors cannot be numbers

[liyishuai]

Is it a bug or feature?

Instance Deserialize__unit : Deserialize unit :=
  Deser.match_con "unit type" [("204", tt)] [].

Goal (from_string "204" = inl
        (DeserError [ ]
           ("could not read type '" ++ "unit type" ++ "', " ++
            "unexpected atom (expected list or nullary constructor name)"))).
Proof. reflexivity. Qed.

[Lysxia]

I'd classify that as working as expected, but it might also be a good idea to generalize match_con a little. At the same time, the match_con stuff is really meant to be used in a very formulaic manner entirely derived from the type declaration. If you want to have any say in the encoding, you might want to just pattern-match on the S-expression directly in this definition.

[liyishuai]

Yea I can live with this feature, provided documentation.

[Lysxia]

Sadly, generalizing match_con to allow arbitrary atoms as constructor tags breaks the current API. I hoped coercions would smooth this out but they don't. We could have the generalized version as a separate function, but I still feel like this is a rather odd use case. Instead, I can add some documentation about defining parsers by manual pattern-matching.