Canonical way to fix error with Data.Text.head in Liquid Haskell?

Question

I have code:

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

When I run LH on it (stack exec liquid -- MyFile.hs) I get error:

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}

I am not sure what does it mean, seems that LH thinks the call of T.head is unsafe. But I have a check of the length with T.length t > 0! What is the canonical way to fix this problem, so LH could pass the verification? More interesting is without rewriting of the code, with LH only.