Excited that "Is sized typing for Coq practical?", @ionchy's work, with Yufeng Li and me, has finally appeared in JFP:
https://doi.org/10.1017/S0956796822000120

In this work, we extended some past work on sized typing for CIC to Coq, extend Coq with sized typing with complete size inference, prove some stuff about size inference, study a set theoretic model, and analyze the performance of the implementation (which is bad).

You can find @ionchy's original summary on the bird site: https://twitter.com/ionathanch/status/1471220461509832704