From be9b7d5150322fba45d0c9de60fd133e44b4faa5 Mon Sep 17 00:00:00 2001
From: Kris Brown <kris@topos.institute>
Date: Fri, 6 Dec 2024 19:17:33 -0800
Subject: [PATCH] Allow WithModel to take subtypes of model_type

---
 src/models/ModelInterface.jl  |  4 ++--
 test/models/ModelInterface.jl | 20 ++++++++++++++++++++
 2 files changed, 22 insertions(+), 2 deletions(-)

diff --git a/src/models/ModelInterface.jl b/src/models/ModelInterface.jl
index 4e9e0ec..0875199 100644
--- a/src/models/ModelInterface.jl
+++ b/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
diff --git a/test/models/ModelInterface.jl b/test/models/ModelInterface.jl
index e6fe937..5b16ed4 100644
--- a/test/models/ModelInterface.jl
+++ b/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