Thanks for the link, it looks just like what I was after! I've been reading through the paper and it looks really nice. It seems to rely on dependent records,

Thanks for the link, it looks just like what I was after! I've been reading through the paper and it looks really nice. It seems to rely on dependent records, which I assumed might be the case; but it claims the dependency is "benign" and elaborates-way when translated to System-F (I haven't reached that part yet); so it does seem to have found the right "trick" (i.e. a tractable subset of dependent types which enables modules, without losing too much inference or devolving into a game of prove-the-lemma). Incidentally, it's also a nice use of "first class types" which isn't (fully) dependently-typed. It irks me when I read blog posts about e.g. Agda or Idris, which describe first-class types (i.e. no stratification, passing types in and out of functions, etc.) but call that "dependent types"; then don't mention the actual "dependent" part (type signatures which bind values to names, which can be referenced "later on" in the type).