Возьмите функцию tail как в библиотеке списка:
tail : (l : List a) -> {auto ok : NonEmpty l} -> List a
tail [] {ok=IsNonEmpty} impossible
tail (x::xs) {ok=p} = xs
Теперь попробуйте заменить тип вывода эффективным вычислением:
randomIndex : (l : List a) -> {auto ok : NonEmpty l} -> Eff Nat [RND]
randomIndex [] {ok=IsNonEmpty} impossible
randomIndex (x::xs) {ok=p} = pure 0 -- whatever
И вы получите ошибку Clauses have differing numbers of arguments.
Это кажется неправильным. кто-нибудь знает, почему это произошло? Возможно ли это потому, что Eff является синонимом типа для некоторого типа функции?