[Agda] another possible without-K problem

[Dan Licata]

Also, related to implementing higher inductives, but not to without-K: 
is there a way to turn off/defeat the unused arguments analysis that is
new in 2.3.2.1?  It breaks some of the things I'm doing: I want a
function with a "phantom" parameter, where different values of the
phantom parameter do not automatically get equated.  

Thanks!
-Dan