Even though there is a workaround #175, I suspect that dispatch isn't the best way to check this. I envision a solution like

implements(model::Any, theory::Union{Module,GAT}, x::Ident, types::Vector{Type})

E.g. implements(FinMatC{Int}(), ThCategory, compose, [Int, Matrix{Int}]) which the above function converts into a runtime check whether or not there is a method compose(::WithModel{FinSetC}, ::Matrix{Int}, ::Matrix{Int}).

We can then add sugar which takes a Symbol rather than an Ident(if this is not ambiguous) and uses [Any, Any,...] for the type vector if none is explicitly provided. And not providing a particular ident means the conjunction of checking all the idents in the theory.

This seems nicer than the current approach because

1. it avoids a proliferation of implements methods (for every model type + theory scope pair)
2. it gives you finer granularity to check if particular methods are implemented rather than only checking entire theories (or, at best, scopes)
3. it gives you the argument type granularity to see that FinMatC{Int}() implements compose(::Matrix{Int}, ::Matrix{Int}) but not compose(::Matrix{Float64}, ::Matrix{Float64}).