Yeah IIRC width subtyping for modules was the only thing they didn't have complete inference for if you didn't use large types, so this is a huge win. Though I

Yeah IIRC width subtyping for modules was the only thing they didn't have complete inference for if you didn't use large types, so this is a huge win. Though I'm nearing the end of the thesis and I'm afraid there may be some things about 1ML that don't jive with this (1ML elaborate to full Fω and gives you explicit access to existentials and higher kinds, which are possibly difficult to unify with the work here).