haskell - 在 Liquid Haskell 中修复 Data.Text.head 错误的规范方法？

Question

我有代码：

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}

我不知道这是什么意思，似乎 LH 认为调用T.head是不安全的。但我检查了长度T.length t > 0！解决此问题的规范方法是什么，以便 LH 可以通过验证？更有趣的是无需重写代码，仅使用 LH。