Incorrect universe error

[palmskog]

I have a recursive function using a non-trivial measure that has been successfully defined before using a functional and well_founded_induction_type, that I've translated to Equations. However, I get the following error after proving all obligations:

Error: Anomaly "Incorrect universe max(Set, Top.2106) declared for inductive type, inferred level is max(Set, Top.518, Top.2106)."

This is without using universe polymorphism in any way, no fancy types, just plain lists.

I'm using Coq 8.9.1 and Equations 1.2.

It's very hard to minimize this example, so I've just made the whole thing available as a self-contained gist. The anomaly shows up at the last Qed.

The background is that the function is a regular expression matcher as defined in this paper.

[palmskog]

Instantiating my section Type variable to something in Set (in this case ascii) did not seem to help, but at least gave a more intelligible error message:

Error: Anomaly "Incorrect universe Set declared for inductive type, inferred level is max(Set, Top.1)."

However, I managed to get the parameterized equation to pass by manually annotating the type of everything I could with Type, see this new gist.