Канонический способ исправить ошибку с Data.Text.head в Liquid Haskell? - PullRequest
Новая
       14

Канонический способ исправить ошибку с Data.Text.head в Liquid Haskell?

0 голосов
/ 03 июня 2019

У меня есть код: 

myfun c t = if c == '/' && T.length t > 0 && '/' == T.head t then t else T.singleton c <> t

Когда я запускаю LH на нем (stack exec liquid -- MyFile.hs), я получаю ошибку: 

Error: Liquid Type Mismatch

35 |           rmSlash c t = if c == '/' && T.length t >= 1 && '/' == T.head t then t else T.singleton c <> t
                                                                            ^

Inferred type
    VV : {v : Data.Text.Internal.Text | 0 <= tlen v
                                        && tlen v == stringlen v
                                        && v == t}

not a subtype of Required type
    VV : {VV : Data.Text.Internal.Text | 1 <= tlen VV}

In Context
    t : {t : Data.Text.Internal.Text | 0 <= tlen t
                                        && tlen t == stringlen t}

Я не уверен, что это значит, кажется, что ЛХ считает вызов T.head небезопасным. Но у меня есть проверка длины с T.length t > 0! Какой канонический способ решить эту проблему, чтобы LH мог пройти проверку? Более интересно без переписывания кода, только с LH.

...