Elab issues with index notation

[lecopivo]

I broke the element access notation again

variable {Cont Idx Elem} [IndexType Idx] [Indexed Cont Idx Elem]

variable (x y : Cont)

-- broken
#check Function.HasUncurry.uncurry fun i => x[i]
#check Function.HasUncurry.uncurry fun i j => (x[i],y[j])

-- works
#check Function.HasUncurry.uncurry fun i => (x[i] : Elem)
#check Function.HasUncurry.uncurry fun i j => ((x[i] : Elem),(y[j] : Elem))

Because the x[i] elaboration is postponed until the type of x[i] is known it causes failure to synthesize the instance in HasUncurry.

I'm thinking of going back to using GetElem.getElem instead of Indexed.get. Then the custom element access notation can be implemented just as a macro and the elaboration mess can be completely avoided.

[JamesGallicchio]

hm, this makes sense; for now I think I'll remove the notation. when I want it again I'll try copying the getElem elaborator to see what it does.