Problem Verifying ASCII.String

The following fails for reasons unknown:

import whiley.lang.ASCII

function f(ASCII.string str) -> (ASCII.string r):
    return str

This fails with an error message:

./test.wyal:3: type invariant not satisfied
assert "type invariant not satisfied":
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

The proof is:

 56. exists(whiley.lang.ASCII.string str).(((true) && ((str is !whiley.lang. () 
 57. exists(whiley.lang.ASCII.string str).(str is !whiley.lang.ASCII. (Simp 56) 
 51. str is !whiley.lang.ASCII.string                             (Exists-E 57) 
 67. !whiley.lang.ASCII.string(str)                                   (Is-I 51) 
 91. exists(int i:3).((((i:3 + 1) >= (0 + 1)) && ((|str| + 1) >= ( (Macro-I 67) 
 96. exists(int i:3).((i:3 >= 0) && (|str| >= (1 + i:3)) && !whiley.l (Simp 91) 
 95. (i:3 >= 0) && (|str| >= (1 + i:3)) && !whiley.lang.ASCII.cha (Exists-E 96) 
 92. i:3 >= 0                                                        (And-E 95) 
 94. |str| >= (1 + i:3)                                              (And-E 95) 
 89. !whiley.lang.ASCII.char(str[i:3])                               (And-E 95) 
 97. |str| >= 1                                                   (Ieq-I 94,92) 
 105. ((0 >= (str[i:3] + 1)) || (str[i:3] >= (255 + 1)))           (Macro-I 89) 
 111. (0 >= (1 + str[i:3])) || (str[i:3] >= 256)                     (Simp 105) 
┌──────────────────────────────────────────────────────────────────────────────┐
│ 107. 0 >= (1 + str[i:3])                                          (Or-E 111) │
├──────────────────────────────────────────────────────────────────────────────┤
│ 110. str[i:3] >= 256                                              (Or-E 111) │
└──────────────────────────────────────────────────────────────────────────────┘

However, if we inline the definitions of ASCII.string into the same file then it does verify.

Whiley / WhileyTheoremProver

Problem Verifying ASCII.String #123