Since insertvalue and extractvalue for arrays and records require a constant index argument - how about turning this index into a type number and add a (index :<: dimension) constraint? Or should we have two functions, one with Int index and one of type number index?