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.