That's super interesting. I wonder if you've tried optimizing for type-checking duration of a richly dependently typed program and gotten viscerally nicer code out of that.