Agda-2.3.2.2: test/fail/ShouldBeASort.err
ShouldBeASort.agda:5,7-33 Not in scope: ShouldBeASort-Never-Occurs at ShouldBeASort.agda:5,7-33 when scope checking ShouldBeASort-Never-Occurs
ShouldBeASort.agda:5,7-33 Not in scope: ShouldBeASort-Never-Occurs at ShouldBeASort.agda:5,7-33 when scope checking ShouldBeASort-Never-Occurs