totality022.idr:7:20-29:
  |
7 | f _ [] (RSnoc _ _) impossible -- = ?wat
  |                    ~~~~~~~~~~
f _ [] (RSnoc _ _) is a valid case