Problem with array manipulation functions

[Pablo J. Pedemonte]

Hi!
I'm having some problems when trying to handle the array belonging
to this data structure:

:: VEBTree a = ManyVEB a a a .{VEBTree a} (VEBTree a)

I'd like (for sake of efficiency) to be able to write an insertion function
similar to this one:

insert :: *(VEBTree a) a -> *(VEBTree a)
insert (ManyVEB ru f l det res) i = 
  let!
    a = i / ru
    b = i mod ru
    (w,det1) = uselect det (toInt a)
    w1 = insert w b
    det2 = update det1 (toInt a) w1
 in ManyVEB ru f l det2 res

Thus, I need the array and their elements to be unique. But trying with this
dummy piece of code:

insertWasEmpty (ManyVEB ru f l det res) i = 
let!
    a = i / ru
    (w,det1) = uselect det (toInt a)
    det2 = update det1 (toInt a) (EmptyVEB a)
in ???

and compiling with the -lt option, I get the following types (getting rid of
type contexts):

??? = det1: 
insert :: u:(VEBTree a) a -> v:{VEBTree a}, [u <= v]   
??? = w:
insert :: .(VEBTree a) a -> VEBTree a

Here is the problem, I presume. The uselect function seems to nuke the
uniqueness of the array elements (Is this right?), and I need'em to be unique
for the recursive step of the insertion! .
Moving to the select function (i.e., trying with this piece of code):

let!
    a = i / ru
    w = uselect det (toInt a)
in ???

I get:
??? = det
insert:: u:(VEBTree .a) .b -> v:{w:VEBTree .a}, [u <= w, u <= v]
(This is what I want!)
??? = w
insertWasEmpty :: u:(VEBTree a) a -> u:VEBTree a
(this is also OK!)

But using select I can't update the array...
Why uselect doesn't annotate the e type with uniqueness attributes?
Is there a solution for my update/select problem?

Greetings and thanks in advance,
Pablo J. Pedemonte