Annotations are not checked for reflected functions that are marked as non-terminating

Consider the following code (link):

{-@ LIQUID "--reflection" @-}
{-@ LIQUID "--ple" @-}

data L a = Nil | Cons a (L a)

{-@ reflect listSum @-}
{-@ listSum :: L Nat -> Nat @-}
listSum :: L Int -> Int
listSum Nil = 0
listSum (Cons h t) = h + listSum t


{-@ lazy ones @-}
{-@ ones :: {l:L Nat | listSum l > 5} @-}
ones :: L Int
ones = Cons 1 ones

This code verifies without issues and if I replace listSum l > 5 by listSum l < 5 I get an error as expected (try). However, when I add the line {-@ reflect ones @-}, then no error is generated at all (example) With this it would be easy to introduce an inconsistency. However, I would like to safely reflect a non-terminating function such that I can use it in theorems and other annotations.

Note that the issue persists if I disable the termination checker for the whole file (link).

I also tested this with liquidhaskell-0.9.6.3 as well as the recent LiquidHaskell from github.