GATlab does a trick where it converts a (literally) indexed function, e.g. compose[myCat](f,g), into something Julia can dispatch on: compose(WithModel{MyCat}(myCat), f, g). This latter method is programmatically generated by @instance, but this generated method expects (TheoryInterface.WithModel){$model_type}. This is too strict: rather it ought accept (TheoryInterface.WithModel){<:$model_type}. For example, if model_type is an abstract type, then any particular model one passes will only be a subtype, not an exact match. See below for an example:

""" Assume this implements Base.iterate """
abstract type MyAbsIter{V} <: Model{Tuple{V}} end

struct MyVect{V} <: MyAbsIter{V}
  v::Vector{V}
end

Base.iterate(m::MyVect, i...) = iterate(m.v, i...)

@instance ThSet{V} [model::MyAbsIter{V}] where V begin 
  default(v::V) = v ∈ model ? v : @fail "Bad $v not in $model"
end

@test implements(MyVect([1,2,3]), ThSet)

# this will fail unless WithModel accepts subtypes
@test ThSet.default[MyVect([1,2,3])](1) == 1