LIQUID.txt

Data.Text: 56 annotated, 32 unannotated (most don't have an obvious
spec that we can express)

Data.Text.Lazy: 62 annotated, 35 unannotated (most don't have an obvious
spec that we can express)


Verified modules:
- [ ] Data.Text
- [x] Data.Text.Array
- [x] Data.Text.Encoding
- [x] Data.Text.Foreign
- [x] Data.Text.Fusion
- [x] Data.Text.Fusion.Size
- [x] Data.Text.Internal
- [x] Data.Text.Lazy
- [x] Data.Text.Lazy.Builder
- [x] Data.Text.Lazy.Encoding
- [x] Data.Text.Lazy.Fusion
- [x] Data.Text.Lazy.Internal
- [x] Data.Text.Lazy.Search
- [x] Data.Text.Private
- [x] Data.Text.Search
- [x] Data.Text.Unsafe
- [x] Data.Text.UnsafeChar


FIXME: there's a strange issue where desugaring a guard results in a
       GHC.Prim.realWorld# value being passed around (but seemingly
       ignored). this value is refined to false and is subsequently
       laden with every refinement imaginable, which can make the
       "saving result" stage of fixpoint last hours.. it does not,
       however, seem to affect soundness, as i have consistently been
       able to convert guards to ifs, thereby removing the
       `realWorld#`s and falses with no effect on the safety
       judgment.

FIXME: another weird issue in Text.small.hs.fq.bk. a duplicate
       qualifier is mined and seems to cause a constraint to be unsat.

Other interesting modules:

Definitely not interesting:
- Data.Text.Encoding.* (deals with encodings and bytestrings)
- Data.Text.Encoding.Fusion.Common
- Data.Text.Fusion.CaseMapping
- Data.Text.Fusion.Common
- Data.Text.Fusion.Internal
- Data.Text.IO
- Data.Text.IO.Internal
- Data.Text.Lazy.Builder.**
- Data.Text.Lazy.Encoding.Fusion
- Data.Text.Lazy.IO
- Data.Text.Lazy.Read
- Data.Text.Read
- Data.Text.Unsafe.Base
- Data.Text.UnsafeShift
- Data.Text.Util (actually inlined this into Text and Text.Lazy)

Possible bug in Data.Text.Fusion.mapAccumL:

    > let f a c = (a, chr 65536)
    > mapAccumL f 0 (stream (pack "aaaaa"))

I believe this ought to return `(0,"\65536\65536\65536\65536\65536")`
but instead it returns `(0,"\65536\65536\x\65536\65536")` where `\x`
is a non-deterministic value. At the very least this breaks
referential transparency.

The issue comes due to the fact that `f` may be given a Char that fits
into a `Word16` but return one that requires 2. LiquidHaskell
complains that the call to `unsafeWrite` may index out-of-bounds, but
if we change `j` to depend on the Char returned by `f`, the complain
goes away, as does the non-determinism.

The non-determinism seems to come about as follows:
- mapAccumL calls `outer arr top z s i` (top == len arr) (i < top)
- suppose `i == top - 1`, meaning it is the last valid index into
  `arr`, but `f z x` returns a Char `c` that requires two slots.
- outer calls `unsafeWrite arr i c` indexing one step out-of-bounds,
  and then recursively calls `loop z' s' (i+d)` (i+d == top+1)
- outer allocates a new array, copies `top` bytes into the new array,
  but then recurs with `i' == i+d == top+1`, which leaves the array
  with a single junk byte. hence the nondeterminism