ML's module language has subtyping. Given any module signature, you can obtain a supersignature by forgetting any of the following: (0) The presence of a value

ML's module language has subtyping. Given any module signature, you can obtain a supersignature by forgetting any of the following: (0) The presence of a value component. (1) The presence of a type component. (2) The concrete definition of a type component, while still remembering its presence. I am not sure you can do this in Idris, other than manually shuffling data between multiple dependent record types. Which is rather inconvenient: If you have a module with 20 components, the last thing you want to do is manually shift 15 of them to another module. Also, unlike vanilla Haskell (no extensions) type classes, which can only have a single type parameter, ML modules can have more than one type component.