I should say a little about this maybe
So there's some existing theory for sized types for CIC, which is the theory that Coq is based on, and I've extended it to cover a bit more of Gallina, which is Coq's specification language
Sized types are used for checking things like termination in Coq, in lieu of syntax-based guard predicates
I've implemented it in Coq's kernel here: https://github.com/ionathanch/coq/tree/dev
Still a bit buggy (not all of the stdlibs compiles) but examples work! (see README.v)
@nonphatic The abstract looks super interesting! 😀 I did something about this kind of problem a while ago, but it wasn't as general/practical as you announce it to be. Then Paco came along, making most people saying that it was all done… but you went further! 😀 I'm adding it to my reading list 😊 Thanks for sharing!