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 fo

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-phantom-types-d18ece7235e6 https://engineering.foursquare.com/going-rogue-part-2-phanto...