diff --git a/src/models/ModelInterface.jl b/src/models/ModelInterface.jl
index 7ad28fb..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
@@ -649,6 +649,10 @@ function migrator(tmap, dom_module, codom_module, dom_theory, codom_theory)
     v => whereparamdict[AlgSort(tmap(v.method).val)]
   end)
 
+  whereparams2 = map(sorts(dom_theory)) do v
+    whereparamdict[AlgSort(tmap(v.method).val)]
+  end
+
   # Create input for instance_code
   ################################
   accessor_funs = JuliaFunction[] # added to during typecon_funs loop
@@ -726,11 +730,12 @@ function migrator(tmap, dom_module, codom_module, dom_theory, codom_theory)
   )
 
   tup_params = Expr(:curly, :Tuple, whereparams...)
+  tup_params2 = Expr(:curly, :Tuple, whereparams2...)
 
   model_expr = Expr(
     :curly,
     GlobalRef(Syntax.TheoryInterface, :Model),
-    tup_params
+    tup_params2 # Types associated with *domain* sorts
   )
 
   # The second whereparams needs to be reordered by the sorts of the DOM theory
diff --git a/test/Project.toml b/test/Project.toml
index 52861d4..1f56bf8 100644
--- a/test/Project.toml
+++ b/test/Project.toml
@@ -1,4 +1,5 @@
 [deps]
+GATlab = "f0ffcf3b-d13a-433e-917c-cc44ccf5ead2"
 Markdown = "d6f4376e-aef5-505a-96c1-9c027394607a"
 StructEquality = "6ec83bb0-ed9f-11e9-3b4c-2b04cb4e219c"
 Test = "8dfed614-e22c-5e08-85e1-65c5234f0b40"
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