Hello Danny, and thank you! That is clearly a nice work around even though it may require to introduce unnecessary module signatures for the only purpose of composing module implementations. Cheers, Le jeu. 29 nov. 2018 à 10:02, Danny Gratzer a écrit : > Hello, > > Perhaps I'm overlooking something but replacing > > include BI > > with > > include (BI : B with type t := t) > > seems like a reasonable fix to me. > > Danny > -- Yann Régis-Gianas