И то и другоеAgda а такжеИдрис эффективно запретить сопоставление с образцом значений типаType, Кажется, что Agda всегда совпадает в первом случае, в то время как Идрис просто выдает ошибку.

Итак, почему Typecase это плохо? Это нарушает последовательность? Я не смог найти много информации по теме.