In GATlab's present design, one declares a struct to be a possible model (e.g. for ThCategory) by saying struct SetCat <: Model{Tuple{AbstractSet, SetFunction}} and then putting all the methods in an @instance block somewhere.

This prevents one from saying SetCat is a model of some other theory (unless we're lucky and they have semantically the same type constructors in the same order). This feels really limiting. The example this is coming up in is we have ThCategoryWithTerminal <: ThCategory which adds another type constructor. It would be great to say "by the way, SetCat is not merely a category, but it also has this additional structure which I can make explicit by:

@instance ThCategoryWithTerminal{AbstractSet, SetFunction, TerminalLimit} [model::SetCat] begin
  @import id, compose
  terminal()::TerminalLimit = ...
  delete(T::TerminalLimit, x::AbstractSet)::SetFunction = ...
end

But SetCat is not a Model{Tuple{AbstractSet, SetFunction, TerminalLimit}} - that is fixed! It seems like there will be a huge proliferation of structs and names if the same struct can't be a model of two different theories (which happen to have different type constructors).

This also addresses an issue of repetitiveness of type parameters: one first declares a model subtypes Model{Tuple{A,B,C,...}} and then has to write @instance MyTheory{A,B,C,...}.