Agda-2.3.2.2: test/fail/ClashingImport.err
ClashingImport.agda:3,5-34 Not in scope: TODO--Can't-make-this-happen! at ClashingImport.agda:3,5-34 when scope checking TODO--Can't-make-this-happen!
ClashingImport.agda:3,5-34 Not in scope: TODO--Can't-make-this-happen! at ClashingImport.agda:3,5-34 when scope checking TODO--Can't-make-this-happen!