[Remote API] Missing Type constructors?

[m-yac]

I noticed that there are a number of constructors missing in the toJSON instance for Type, namely:

• TCFloat, TCArray, TCAbstract
• PPrime, PEq, PLiteralLessThan, PFLiteral, PValidFloat

Is this just the result of people forgetting to update the RPC interface when a new constructor is added, or are there reasons why we don't implement these constructors? If it's the latter, is this documented somewhere?

Either way, perhaps we should modify the way we pattern match here to make sure that a warning is generated if a new constructor is added and this function is not updated. The TF case of this function does this, for example, and thus is forced to stay up-to-date.

[RyanGlScott]

Ouch, I didn't realize we were using catch-all patterns in that ToJSON instance. In that case, I suspect that these were overlooked simply because it wasn't obvious that the cases were missing. I agree that we should make these pattern matches total.

[m-yac]

Oh dear, looks like this is a larger issue – these same constructors also appear to be absent from the PP instance for Type. I'm going to review every case where we pattern match on a TCon now and make sure we use total pattern matches.

[yav]

@m-yac could you please do this on the functors-merge branch?

[yav]

Btw, what is the problem with the PP instance for Type?

[m-yac]

Well, I'm not sure, maybe there's nothing wrong with it, actually. I just noticed it's missing explicit cases for a number of constructors. For example, TCFloat is not simply text "Float" like Bit, Integer, etc., instead it's covered by the final catch-all case. Maybe that's fine, but seems like it's part of a larger pattern that could result in cases getting missed when new TCon constructors are added (as was the case in the remote API).

[yav]

TCFloat has parameters, so it can't be just text "Float". In fact, some more of the constructors could probably be covered by the "catch" all case, and only the ones that have special syntax (e.g., sequences) need a special case. This doesn't seem super important to fix though.

[m-yac]

That being said, I'm not exactly sure what the "right" way to make these pattern matches total is. Currently the common pattern is:

TCon (TC tc) ts ->
  case (tc,ts) of
    (TCNum n, [])       -> ...
    ...
    (TCFun,   [t1,t2])  -> ...
    (TCTuple _, fs)     -> ...
    (_, _)              -> ...{fallback}...

where each TC constructor always expects the same number of arguments, and we need to do some common error/fallback case if that number of arguments is wrong.

The most obvious way to make this pattern match total is to lift the fallback to each case, as in:

TCon (TC tc) ts ->
  case tc of
    TCNum n -> case ts of
      [] -> ...
      _ -> ...{fallback}...
    ...
    TCFun -> case ts of
      [t1,t2] -> ...
      _ -> ...{fallback}...
    TCTuple _ -> ...

but that's not very nice. Have either of you encountered a situation like this before? Perhaps there's some pattern synonym trickery to do to make this better?