It's not Agda, but you may be interested in this article by Foursquare about how they use Scala Phantom Types to ensure MongoDB queries are semantically well formed at compile time:

https://engineering.foursquare.com/going-rogue-part-2-phanto...