[lmm]

> if I had more experience implementing dependently typed languages, then perhaps I would not find it so weird, as it really just makes type constructors similar to functions, which they would be in a fully dependently typed language.

Yeah. I was screaming for most of this piece, because this all seems like standard dependently-typed stuff, and ironically enough implementing full dependent types would probably end up being easier than trying to handle this one feature as a special case.