Weird error message saying "expected a pattern"

[emilyriehl]

I just submitted a draft pull request #132 in the sHoTT repository for the purposes of reporting a weird error message. At the end of the the propositions file there are four mathematically identical definitions of the same function, two of which compile, and two of which give errors. I'd love to understand what is going on.

[fizruk]

I've replied in the PR, but here's a duplicate:

It appears that two patterns are not allowed by Rzk, for now the suggestion is to introduce the two pairs separately:

- ( (a, p) (b, q) : total-type A P)
+ ( (a, p) : total-type A P)
+ ( (b, q) : total-type A P)

Originally posted by @fizruk in rzk-lang/sHoTT#132 (comment)