I asked about this in /r/dependent_types yesterday. Apparently there's already a fair bit or research going on in this area. See the links: https://www.reddit.com/r/dependent_types/comments/49z1uc/usi...