More probles with arrays

[Pablo J. Pedemonte]

Hi again!

Thanks to Martin Wierich's helpful suggestions, I was able to create
(unique?) arrays with unique elements. But unfortunately, I still have some
problems. If I define the VEBTree data type like this:

:: VEBTree u = EmptyVEB u
                   | OneVEB u u
	       | TwoVEB u u u
	       | ManyVEB u u u .{VEBTree u} (VEBTree u)

Then this dumb piece of code produces the following error message:

insertWasEmpty (ManyVEB ru f l det res) i = 
  let
     a = i / ru
     w = select det (toInt a)
     w1 = id w
     det1 = update det (toInt a) w1
in (ManyVEB ru f l det1 res, False)

"argument 1 of select ({})" attribute at the indicated position cannot be
coerced: {^ VEBTree a} |...
Why it's necessary to perform this kind of coercion? Maybe because the array
isn't unique?

If I put explicit uniqueness annotations, like this:

:: *VEBTree u = EmptyVEB u
                    | OneVEB u u
	        | TwoVEB u u u
	        | ManyVEB u u u *{VEBTree u} (VEBTree u)

then for the same piece of code I get this error message:
 "argument 1 of select ({})" * attribute required but not offered at the
indicated position: ^ {VEBTree a} |...
Again, why this happens? The data type definition declares the array as
a unique one, doesn't it?

So I'm really confused.
Maybe the data type is ill-annotated? Maybe I'm not handling the array
porperly? My intention is to have a unique array holding unique elements, and to
update destructively both of them.

Again, any kind of help or advice is more than welcome!
Thanks in advance,
Pablo Pedemonte