idris-0.9.17: test/reg051-disabled/expected