Clauses have differing numbers of arguments (when mixing impossible pattern and effects)

Take the function tail as in the list library:

tail : (l : List a) -> {auto ok : NonEmpty l} -> List a
tail []      {ok=IsNonEmpty} impossible
tail (x::xs) {ok=p} = xs

Now try to replace the output type with an effectful computation:

randomIndex : (l : List a) -> {auto ok : NonEmpty l} -> Eff Nat [RND]
randomIndex []      {ok=IsNonEmpty} impossible
randomIndex (x::xs) {ok=p} = pure 0 -- whatever

And you get the error Clauses have differing numbers of arguments.

This seems wrong. Does anyone know why this happens? Is it possibly because Eff is a type synonym for some function type?