It seems broken on Agda.
If it's not, wider sample tests needed, because error messages are unhelpful and doesn't give any idea on which samples it's failing.

I'm not sure that cata translations like this should exists.

This cata teaches to write partial functions in cases in which it is not nessesary.
Strongly unrecommend.

It's not haskell way :|

I tried to add it to the 'real' test case (not the sample test), dunno if it'll work.

You mean in the tests?

Can you force
{-# OPTIONS_GHC -Wincomplete-patterns -Werror=incomplete-patterns #-}
?
It would ban solutions like this. In previous catas too.

Add -Wincomplete-patterns, -Werror=incomplete-patterns GHC flags.
It will make some unfair tricks unavailable.

I found why is this happening.
Thats because pattern-matching is non-exhaustive.
So this tricky way of solving this cata can be removed by adding those GHC flags: -Wincomplete-patterns, -Werror=incomplete-patterns

I very liked this and previous katas!

I spend whole day on this kata and thought my brain will burn in fire :D

Thanks for this great experience and feelings that i got when tried to solve this kata!

Hope to see more katas like this one!