[Agda] emptiness checking with strings

[Dan Licata]

Hi everyone,

Given the usual equality type Id M N and the empty type Void, I'd like
to write a function

contra : Id "nat" "exp" -> Void
contra ()

However, the emptiness checker doesn't notice that this type is
uninhabited (like it would if "nat" and "exp" were two different
constructors of a datatype).  

Does anyone know a workaround?  Also, would it be hard to catch this
case (i.e., treat string literals as constructors), or is this just a
feature that's not implemented yet?

Thanks!
-Dan