Isn't your associated type here more like a dependent record field/ existential that we can kinda expose?
Not quite. There is still a clear distinction between type and value level. You cannot refer to an AT on the value level or to a member value on the type level.
This does seem to veer into first class module territory. Especially wrt needing first class types in a fashion.
I think formally there is little difference between a powerful record system and a first-class module system. However, even in a non-dependent language a first class module could still expect a value argument. A record type couldn't do this without essentially making the language dependent on the way.
Have you had a chance to peruse the Andreas Rossberg 1ml paper on embedding first class modules into f omega that has been circulating? Perhaps there are ideas There that could be adapted. Especially since core is an augmented f omega
I haven't read it, sorry. My proposal should conform to the current core language, as it's mostly just a syntax transformation. The only new semantics would be defaults.