Nigel,
I am sorry if I have said something wrong in my posting. I agree that
the example I gave was insufficient to disprove soundness of Hope+C.
On the other hand, no example can *prove* soundness of a type system.
So, let me try a bit further. What happens if I extend your
example as follows [I can read Hope but writing it is another
matter, so forgive me if I stick to Haskell :-)]:
let unpack w = let Win x = w in x
same (x, y) = unpack x == unpack y
in
same (index (wl, 1), index (wl, 2))
Does that type? Looking at your typing rules I thought it would, but
please correct me if I am wrong.
-- Martin
