idris-1.2.0: test/error004/expected

FunErrTest.idr:35:12-18:
   |
35 | badCadr1 = cadr []
   |            ~~~~~~~
When checking right hand side of badCadr1 with expected type
        Int

When checking argument cons2 to function FunErrTest.cadr:
        Could not prove that [] has at least two elements.

FunErrTest.idr:38:12-19:
   |
38 | badCadr2 = cadr [1]
   |            ~~~~~~~~
When checking right hand side of badCadr2 with expected type
        Int

When checking argument cons2 to function FunErrTest.cadr:
        Could not prove that [] has at least two elements.