Allow WithModel to take subtypes of model_type

src/models/ModelInterface.jl

@@ -514,7 +514,7 @@ function make_alias_definitions(theory, theory_module, jltype_by_sort, model_typ
               args
             end
           else
-            [(gensym(:m), :($(TheoryInterface.WithModel){$model_type})); args]
+            [(gensym(:m), :($(TheoryInterface.WithModel){<:$model_type})); args]
           end
           argexprs = [Expr(:(::), p...) for p in args]
           overload = JuliaFunction(;
@@ -560,7 +560,7 @@ function qualify_function(fun::JuliaFunction, theory_module, model_type::Union{E
 
     m = gensym(:m)
     (
-      [Expr(:(::), m, Expr(:curly, TheoryInterface.WithModel, model_type)), args...],
+      [Expr(:(::), m, Expr(:curly, TheoryInterface.WithModel, Expr(:<:, model_type))), args...],
       Expr(:let, Expr(:(=), :model, :($m.model)), fun.impl)
     )
   else

test/models/ModelInterface.jl

@@ -195,5 +195,25 @@ end
 
 @test h(false) == false
 
+# Test models with abstract types 
+#################################
+
+""" 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
 
 end # module