В Идрисе один из базовых типов - String, внутри представленный как null-terminated C string. Знаете, как узнать длину такой строки? Сконвертить в список Char'ов, а потом посчитать его длину. А все потому, что хоть в рантайме идриса и есть нормальная функция вычисления длины (по-хорошему ее вообще стоило бы хранить, а не вычислять), в стандартную библиотеку ее забыли экспортнуть. У них там в академии своя атмосфера.