idris-0.9.11: test/error002/expected