Array access in transformations with arguments
In transformation with arguments, stuff defined with a notation cannot be reused if the notation is overloaded.
In Array63 module we have:
function () (a: array 'a) (i: int) : 'a = a.elts i
And an example is:
module Test use import array.Array use import mach.array.Array63 constant d: Array.array int constant e: Array63.array int goal a: e = 5 goal c: Array.() d 3 = 5 end
In the above, notation  cannot be used for array d as the notation  is used for Array63. In this example, it is not even possible to talk about Array.() in transformations.
The complete solution would be to accept qualified expressions in arguments of tactics: this may be difficult.
I think it's possible to disambiguate the mixfix notation as we do for infix (==^ ==^ etc). It would require to extend the parser a little so that "[ term ]", "[ ^ term ]", "[ ^ ^ term ]" are recognized (or any similar notation).