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}

T.headLH は の呼び出しが安全ではないと考えているようです。しかし、私は長さのチェックをしていT.length t > 0ます！LH が検証に合格できるように、この問題を修正する正規の方法は何ですか? さらに興味深いのは、コードを書き直さずに LH のみを使用することです。