Sorry if this is a silly question: People, are you sure that Agda really needs parameterized modules? For example, Haskell has not such and still looks all right (except absence of dependent types). If they are replaced with classes and instances by records, then the implementors could save effort. Regards, Sergei.