ShouldBeASort.agda:5,7-33
Not in scope:
  ShouldBeASort-Never-Occurs
  at ShouldBeASort.agda:5,7-33
when scope checking ShouldBeASort-Never-Occurs