From b31917527393e04c0cc64dee6b495a723909537e Mon Sep 17 00:00:00 2001
From: Kris Brown <kris@topos.institute>
Date: Sat, 7 Dec 2024 19:44:36 -0800
Subject: [PATCH 1/2] Remove Model, change migration

typecon too

allow subtyping in WithModel

Change how import works.

remove redundant Using Gatlab

.

.

fix docstrings

.
---
 src/models/ModelInterface.jl              | 193 ++++++++++++----------
 src/nonstdlib/models/Pushouts.jl          |   2 -
 src/stdlib/derivedmodels/DerivedModels.jl |   2 +-
 src/stdlib/models/arithmetic.jl           |   8 +-
 src/stdlib/models/finmatrices.jl          |   3 +-
 src/stdlib/models/finsets.jl              |   3 +-
 src/stdlib/models/gats.jl                 |   5 +-
 src/stdlib/models/nothings.jl             |   3 +-
 src/stdlib/models/op.jl                   |  13 +-
 src/stdlib/models/slicecategories.jl      |  12 +-
 src/syntax/GATs.jl                        |   2 +-
 src/syntax/TheoryInterface.jl             |  11 +-
 src/syntax/TheoryMaps.jl                  |   4 -
 src/syntax/gats/gat.jl                    |   2 +
 test/models/ModelInterface.jl             |  11 +-
 test/stdlib/FinMatrices.jl                |   5 +-
 test/stdlib/FinSets.jl                    |   2 +-
 test/stdlib/Nothings.jl                   |   2 +-
 test/stdlib/Op.jl                         |   1 -
 test/stdlib/SliceCategories.jl            |   2 +-
 20 files changed, 148 insertions(+), 138 deletions(-)

diff --git a/src/models/ModelInterface.jl b/src/models/ModelInterface.jl
index 08751991..64d1177e 100644
--- a/src/models/ModelInterface.jl
+++ b/src/models/ModelInterface.jl
@@ -1,25 +1,7 @@
-module ModelInterface
-
-export Model, implements, TypeCheckFail, SignatureMismatchError, 
-       @model, @instance, @withmodel, @fail, migrate_model
-
-using ...Syntax
-using ...Util.MetaUtils
-using ...Util.MetaUtils: JuliaFunctionSigNoWhere
-
-import ...Syntax.TheoryMaps: migrator 
-
-using MLStyle
-using DataStructures: DefaultDict, OrderedDict
 
 """
-`Model{Tup <: Tuple}`
-
-A Julia value with type `Model{Tuple{Ts...}}` represents a model of some
-part of the theory hierarchy, which uses the types in `Ts...` to implement
-the sorts.
-
-A model `m::Model{Tup}` is marked as implementing a `seg::GATSegment` iff
+Any Julia struct can be a model of a GAT. A model is marked as implementing a 
+`seg::GATSegment` iff
 
 `implements(m, ::Type{Val{gettag(seg)}}) == true`
 
@@ -57,11 +39,25 @@ to get away without providing the context when you are writing code that is not
 across models, and you know that, for instance, composition of FinFunctions does not
 need the domains and codomains of the FinFunctions explicitly supplied.
 
-A model `m::Model{Tup}` implements a theory iff it implements all of the GATSegments
+A model implements a theory iff it implements all of the GATSegments
 in the theory.
-
-Models are defined in TheoryInterface because reasons
 """
+module ModelInterface
+
+export implements, impl_type, TypeCheckFail, SignatureMismatchError, 
+       @model, @instance, @withmodel, @fail, migrate_model
+
+using ...Syntax
+using ...Util.MetaUtils
+using ...Util.MetaUtils: JuliaFunctionSigNoWhere
+
+import ...Syntax.TheoryMaps: migrator 
+using ...Syntax.TheoryMaps: dom, codom
+using ...Syntax.TheoryInterface: GAT_MODULE_LOOKUP
+
+using MLStyle
+using DataStructures: DefaultDict, OrderedDict
+
 
 """
 `ImplementationNotes`
@@ -75,20 +71,26 @@ struct ImplementationNotes
 end
 
 """
-`implements(m::Model, tag::ScopeTag) -> Union{ImplementationNotes, Nothing}`
+`implements(m::MyModel, tag::ScopeTag) -> Union{ImplementationNotes, Nothing}`
 
 If `m` implements the GATSegment referred to by `tag`, then return the
 corresponding implementation notes.
 """
 implements(m::Module, ::Type{Val{tag}}) where {tag} = nothing
 
-implements(m::Model, tag::ScopeTag) = implements(m, Val{tag})
+implements(m, tag::ScopeTag) = implements(m, Val{tag})
+
+impl_type(m, tag::ScopeTag) = impl_type(m, Val{tag})
 
-implements(m::Model, theory_module::Module) =
+impl_type(m, mod::Module, name::Symbol) = 
+  impl_type(m, gettag(ident(mod.Meta.theory; name)))
+
+
+implements(m, theory_module::Module) =
   all(!isnothing(implements(m, gettag(scope))) for scope in theory_module.Meta.theory.segments.scopes)
 
 struct TypeCheckFail <: Exception
-  model::Union{Model, Nothing}
+  model::Any
   theory::GAT
   type::Ident
   val::Any
@@ -108,7 +110,7 @@ end
 Usage:
 
 ```julia
-struct TypedFinSetC <: Model{Tuple{Vector{Int}, Vector{Int}}}
+struct TypedFinSetC
   ntypes::Int
 end
 
@@ -124,11 +126,18 @@ end
   codom(f::Vector{Int}; context) = context.codom
 end
 
-struct SliceCat{Ob, Hom, C <: Model{Tuple{Ob, Hom}}} <: Model{Tuple{Tuple{Ob, Hom}, Hom}}
-  c::C
+struct SliceC{ObT, HomT, C}
+  cat::C
+  over::ObT
+  function SliceC(cat::C, over) where C
+    implements(cat, ThCategory) || error("Bad cat $cat")
+    obtype = impl_type(cat, ThCategory, :Ob)
+    homtype = impl_type(cat, ThCategory, :Hom)
+    new{obtype, homtype, C}(cat, ThCategory.Ob[cat](over))
+  end
 end
 
-@instance ThCategory{Tuple{Ob, Hom}, Hom} [model::SliceCat{Ob, Hom, C}] where {Ob, Hom, C<:Model{Tuple{Ob, Hom}}} begin
+@instance ThCategory{Tuple{Ob, Hom}, Hom} [model::SliceCat{Ob, Hom, C}] where {Ob, Hom, C}}} begin
 end
 ```
 
@@ -210,10 +219,18 @@ function generate_instance(
     []
   end
 
+  impl_type_declarations = if isnothing(model_type) 
+    Expr[]
+  else 
+    map(collect(jltype_by_sort)) do (k, v)
+      impl_type_declaration(model_type, whereparams, k, v)
+    end
+  end
   docsink = gensym(:docsink)
 
   code = Expr(:block,
     [generate_function(f) for f in qualified_functions]...,
+    impl_type_declarations...,
     implements_declarations...,
     :(function $docsink end),
     :(Core.@__doc__ $docsink)
@@ -491,7 +508,9 @@ function mk_fun(f::AlgFunction, theory, mod, jltype_by_sort)
   args = map(zip(f.args, sortsignature(f))) do (i,s)
     Expr(:(::),nameof(f[i]),jltype_by_sort[s])
   end
-  impl = to_call_impl(f.value,theory, mod, false)
+  argnames = Vector{Symbol}(undef, length(getcontext(f)))
+  setindex!.(Ref(argnames), [nameof(f[i]) for i in f.args], getvalue.(f.args))
+  impl = to_call_impl(f.value,theory, mod, argnames, false)
   JuliaFunction(;name=name, args, impl)
 end
 
@@ -578,6 +597,17 @@ function qualify_function(fun::JuliaFunction, theory_module, model_type::Union{E
   )
 end
 
+function impl_type_declaration(model_type, whereparams, sort, jltype)
+  quote 
+    if !hasmethod($(GlobalRef(ModelInterface, :impl_type)), 
+      ($(model_type) where {$(whereparams...)}, Type{Val{$(gettag(getdecl(sort)))}}))
+      $(GlobalRef(ModelInterface, :impl_type))(
+          ::$(model_type), ::Type{Val{$(gettag(getdecl(sort)))}}
+        ) where {$(whereparams...)} = $(jltype)
+    end
+  end
+end
+
 function implements_declaration(model_type, scope, whereparams)
   notes = ImplementationNotes(nothing)
   quote
@@ -627,37 +657,35 @@ macro withmodel(model, subsexpr, body)
 end
 
 
+migrate_model(F::Module, m::Any, new_model_name=nothing) = 
+  migrate_model(F.MAP, m, new_model_name)
+
 """
-Given a Theory Morphism T->U and a model Mᵤ which implements U,
-obtain a model Mₜ which wraps Mᵤ and is a model of T.
+Given a theory map A -> B, construct a new struct type which wraps a model of
+theory B and is itself a model of theory A. The name of the struct can be
+optionally given, otherwise it is gensym'd. The resulting expression is an
+instance of that struct type.
 
 Future work: There is some subtlety in how accessor functions should be handled.
 TODO: The new instance methods do not yet handle the `context` keyword argument.
 """
-function migrator(tmap, dom_module, codom_module, dom_theory, codom_theory)
-
-  # Symbols
-  migrator_name = :Migrator # TODO do we need to gensym?
-  _x = gensym("val")
-
-  # Map CODOM sorts to whereparam symbols
-  whereparamdict = OrderedDict(s=>gensym(s.head.name) for s in sorts(codom_theory))
-  # New model is parameterized by these types
-  whereparams = collect(values(whereparamdict))
-  # Julia types of domain sorts determined by theorymap 
+function migrate_model(F::AbsTheoryMap, m::Any, new_model_name::Union{Nothing,Symbol}=nothing)
+  new_model_name = isnothing(new_model_name) ? gensym(:Migrated) : new_model_name
+  dom_theory = dom(F)
+  codom_theory = codom(F)
+  dom_module = GAT_MODULE_LOOKUP[gettag(dom_theory)]
+  codom_module = GAT_MODULE_LOOKUP[gettag(codom_theory)]
+
+  # Expressions which evaluate to the correct Julia type
   jltype_by_sort = Dict(map(sorts(dom_theory)) do v
-    v => whereparamdict[AlgSort(tmap(v.method).val)]
+    v => :(impl_type($m, gettag(getdecl(AlgSort($F($v.method).val)))))
   end)
 
-  whereparams2 = map(sorts(dom_theory)) do v
-    whereparamdict[AlgSort(tmap(v.method).val)]
-  end
+  _x = gensym("val")
 
-  # Create input for instance_code
-  ################################
   accessor_funs = JuliaFunction[] # added to during typecon_funs loop
 
-  typecon_funs = map(collect(typemap(tmap))) do (x, fx)
+  typecon_funs = map(collect(typemap(F))) do (x, fx)
     typecon = getvalue(dom_theory[x])
 
     # Accessors
@@ -692,36 +720,37 @@ function migrator(tmap, dom_module, codom_module, dom_theory, codom_theory)
     args = [:($k::$(v)) for (k, v) in zip(argnames, sig.types)]
     
     return_type = first(sig.types)
+    argnames′ = Array{Symbol}(undef, length(getcontext(typecon)))
+    setindex!.(Ref(argnames′), argnames[2:end], getvalue.(typecon.args))
 
-    impls = to_call_impl.(codom_body.args, Ref(codom_theory), Ref(codom_module), true)
+    impls = to_call_impl.(codom_body.args, Ref(codom_theory), Ref(codom_module), 
+                          Ref(argnames′), true)
     impl = Expr(:call, Expr(:ref, :($codom_module.$fxname), 
                             :(model.model)), _x, impls...)
-
     JuliaFunction(;name, args, return_type, impl)
   end
 
-  # Term constructors
-  #------------------
-  termcon_funs = map(collect(termmap(tmap))) do (x, fx)
+
+  termcon_funs = map(collect(termmap(F))) do (x, fx)
     termcon = getvalue(dom_theory[x])
     sig = julia_signature(dom_theory, x, jltype_by_sort)
 
     name = nameof(termcon.declaration)
     return_type = jltype_by_sort[AlgSort(termcon.type)]
-    args = [:($k::$v) for (k, v) in zip(nameof.(argsof(termcon)), sig.types)]
-    impl = to_call_impl(fx.val, codom_theory, codom_module, true)
+    argnames = nameof.(argsof(termcon))
+    argnames′ = Array{Symbol}(undef, length(getcontext(termcon)))
+    setindex!.(Ref(argnames′), argnames, getvalue.(termcon.args))
+    args = [:($k::$v) for (k, v) in zip(argnames, sig.types)]
+    impl = to_call_impl(fx.val, codom_theory, codom_module, argnames′, true)
 
     JuliaFunction(;name, args, return_type, impl)
   end
-
-
-  # Generate instance code 
   instance_code = generate_instance(
     dom_theory,
     dom_module,
     jltype_by_sort,
-    Expr(:curly, migrator_name, whereparams...),
-    whereparams,
+    new_model_name,
+    [],
     Expr(:block, generate_function.([typecon_funs...,
                                      termcon_funs..., 
                                      accessor_funs...
@@ -729,46 +758,32 @@ function migrator(tmap, dom_module, codom_module, dom_theory, codom_theory)
     typecheck=true, escape=false
   )
 
-  tup_params = Expr(:curly, :Tuple, whereparams...)
-  tup_params2 = Expr(:curly, :Tuple, whereparams2...)
-
-  model_expr = Expr(
-    :curly,
-    GlobalRef(Syntax.TheoryInterface, :Model),
-    tup_params2 # Types associated with *domain* sorts
-  )
-
-  # The second whereparams needs to be reordered by the sorts of the DOM theory
-  quote
-    struct Migrator{$(whereparams...)} <: $model_expr
-      model ::  $(GlobalRef(ModelInterface, :Model)){$tup_params}
-      function Migrator(model:: $(GlobalRef(ModelInterface, :Model)){$tup_params}) where {$(whereparams...)}
-        $(GlobalRef(ModelInterface, :implements))(model, $codom_module) || error("Cannot migrate model $model")
-        new{$(whereparams...)}(model)
-      end
+  eval(quote 
+    struct $new_model_name 
+      model::Any
     end
-
-    $(instance_code.args...)
-  end
+    $instance_code
+    $new_model_name($m)
+  end)
 end
 
 """
 Compile an AlgTerm into a Julia call Expr where termcons (e.g. `f`) are
 interpreted as `mod.f[model.model](...)`.
 """
-function to_call_impl(t::AlgTerm, theory::GAT, mod::Union{Symbol,Module}, migrate::Bool)
+function to_call_impl(t::AlgTerm, theory::GAT, mod::Union{Symbol,Module}, argnames::Vector{Symbol}, migrate::Bool)
   b = bodyof(t)
   if GATs.isvariable(t)
-    nameof(b)
+    argnames[getvalue(getlid(b))]
   elseif  GATs.isdot(t)
-    impl = to_call_impl(b.body, theory, mod, migrate)
+    impl = to_call_impl(b.body, theory, mod, argnames, migrate)
     if isnamed(b.head)
       Expr(:., impl, QuoteNode(nameof(b.head)))
     else 
       Expr(:ref, impl, getlid(b.head).val)
     end
   else
-    args = to_call_impl.(argsof(b), Ref(theory), Ref(mod), migrate)
+    args = to_call_impl.(argsof(b), Ref(theory), Ref(mod), Ref(argnames), migrate)
     name = nameof(headof(b))
     newhead = if name ∈ nameof.(structs(theory))
       Expr(:., :($mod), QuoteNode(name))
@@ -786,6 +801,4 @@ function to_call_accessor(t::AlgTerm, x::Symbol, mod::Module)
   Expr(:call, Expr(:ref, :($mod.$(nameof(headof(b)))), :(model.model)), rest)
 end
 
-migrate_model(theorymap::Module, m::Model) = theorymap.Migrator(m)
-
 end # module
diff --git a/src/nonstdlib/models/Pushouts.jl b/src/nonstdlib/models/Pushouts.jl
index 5c9def88..33fb6376 100644
--- a/src/nonstdlib/models/Pushouts.jl
+++ b/src/nonstdlib/models/Pushouts.jl
@@ -2,8 +2,6 @@ using DataStructures, StructEquality
 
 export PushoutInt
 
-using GATlab
-
 """Data required to specify a pushout. No fancy caching."""
 @struct_hash_equal struct PushoutInt
   ob::Int
diff --git a/src/stdlib/derivedmodels/DerivedModels.jl b/src/stdlib/derivedmodels/DerivedModels.jl
index a75674ba..5287ebc2 100644
--- a/src/stdlib/derivedmodels/DerivedModels.jl
+++ b/src/stdlib/derivedmodels/DerivedModels.jl
@@ -6,7 +6,7 @@ using ...StdTheoryMaps
 using ...StdModels
 
 # Given a model of a category C, we can derive a model of Cᵒᵖ.
-OpFinSetC = migrate_model(OpCat, FinSetC())
+OpFinSetC = migrate_model(OpCat, FinSetC(), :OpFinSetCat)
 
 # Interpret `e` as `0` and `⋅` as `+`.
 IntMonoid = migrate_model(NatPlusMonoid, IntNatPlus())
diff --git a/src/stdlib/models/arithmetic.jl b/src/stdlib/models/arithmetic.jl
index 76c53a17..9e5c0e04 100644
--- a/src/stdlib/models/arithmetic.jl
+++ b/src/stdlib/models/arithmetic.jl
@@ -3,14 +3,14 @@ export IntNat, IntNatPlus, IntPreorder, ZRing, BoolRing
 using ...Models
 using ..StdTheories
 
-struct IntNat <: Model{Tuple{Int}} end
+struct IntNat end
 
 @instance ThNat{Int} [model::IntNat] begin
   Z() = 0
   S(n::Int) = n + 1
 end
 
-struct IntNatPlus <: Model{Tuple{Int}} end
+struct IntNatPlus end
 
 @instance ThNatPlus{Int} [model::IntNatPlus] begin
   Z() = 0
@@ -18,7 +18,7 @@ struct IntNatPlus <: Model{Tuple{Int}} end
   +(x::Int, y::Int) = x + y
 end
 
-struct IntPreorder <: Model{Tuple{Int, Tuple{Int,Int}}} end
+struct IntPreorder end
 
 @instance ThPreorder{Int, Tuple{Int,Int}} [model::IntPreorder] begin
   Leq(ab::Tuple{Int,Int}, a::Int, b::Int) = a ≤ b ? ab : @fail "$(ab[1]) ≰ $(ab[2])"
@@ -30,7 +30,7 @@ struct IntPreorder <: Model{Tuple{Int, Tuple{Int,Int}}} end
   end
 end
 
-struct ZRing <: Model{Tuple{Int}} end
+struct ZRing end
 
 @instance ThRing{Int} [model::ZRing] begin
   zero() = 0
diff --git a/src/stdlib/models/finmatrices.jl b/src/stdlib/models/finmatrices.jl
index 35051d07..1d8d380a 100644
--- a/src/stdlib/models/finmatrices.jl
+++ b/src/stdlib/models/finmatrices.jl
@@ -3,8 +3,7 @@ export FinMatC
 using ...Models
 using ..StdTheories
 
-struct FinMatC{T<:Number} <: Model{Tuple{T}}
-end
+struct FinMatC{T <: Number} end
 
 @instance ThCategory{Int, Matrix{T}} [model::FinMatC{T}] where {T} begin
   Ob(n::Int) = n >= 0 ? n : @fail "expected nonnegative integer"
diff --git a/src/stdlib/models/finsets.jl b/src/stdlib/models/finsets.jl
index 2820eb92..eb2f1905 100644
--- a/src/stdlib/models/finsets.jl
+++ b/src/stdlib/models/finsets.jl
@@ -3,8 +3,7 @@ export FinSetC
 using ...Models
 using ..StdTheories
 
-struct FinSetC <: Model{Tuple{Int, Vector{Int}}}
-end
+struct FinSetC end
 
 @instance ThCategory{Int, Vector{Int}} [model::FinSetC] begin
   Ob(x::Int) = x >= 0 ? x : @fail "expected nonnegative integer"
diff --git a/src/stdlib/models/gats.jl b/src/stdlib/models/gats.jl
index 8d6cc87e..db2ed9a0 100644
--- a/src/stdlib/models/gats.jl
+++ b/src/stdlib/models/gats.jl
@@ -4,10 +4,7 @@ using ...Models
 using ...Syntax
 using ..StdTheories
 
-using GATlab, GATlab.Models
-
-struct GATC <: Model{Tuple{GAT, AbsTheoryMap}}
-end
+struct GATC end
 
 @instance ThCategory{GAT, AbsTheoryMap} [model::GATC] begin
   id(x::GAT) = IdTheoryMap(x)
diff --git a/src/stdlib/models/nothings.jl b/src/stdlib/models/nothings.jl
index 3a7fac67..90d851af 100644
--- a/src/stdlib/models/nothings.jl
+++ b/src/stdlib/models/nothings.jl
@@ -2,8 +2,7 @@ export NothingC
 
 using ...Models, ..StdTheories
 
-struct NothingC <: Model{Tuple{Nothing, Nothing}}
-end
+struct NothingC end
 
 @instance ThCategory{Nothing, Nothing} [model::NothingC] begin
   Ob(::Nothing) = nothing
diff --git a/src/stdlib/models/op.jl b/src/stdlib/models/op.jl
index e0e346f9..2d973a34 100644
--- a/src/stdlib/models/op.jl
+++ b/src/stdlib/models/op.jl
@@ -10,8 +10,17 @@ using ...Models
 using ..StdTheories
 using StructEquality
 
-@struct_hash_equal struct OpC{ObT, HomT, C<:Model{Tuple{ObT, HomT}}} <: Model{Tuple{ObT, HomT}}
-  cat::C
+# TODO when we implement custom structs for models of a particular theory, we 
+# can use that rather than a generic "C" for which we then have to check 
+# whether it implements the theory.
+
+@struct_hash_equal struct OpC{ObT, HomT, C}
+  cat::C 
+  function OpC(c::C) where C 
+    obtype = impl_type(c, ThCategory, :Ob)
+    homtype = impl_type(c, ThCategory, :Hom)
+    implements(c, ThCategory) ? new{obtype, homtype, C}(c) : error("bad")
+  end
 end
 
 op(c) = OpC(c)
diff --git a/src/stdlib/models/slicecategories.jl b/src/stdlib/models/slicecategories.jl
index 923ab998..701d172e 100644
--- a/src/stdlib/models/slicecategories.jl
+++ b/src/stdlib/models/slicecategories.jl
@@ -9,13 +9,15 @@ using StructEquality
   hom::HomT
 end
 
-@struct_hash_equal struct SliceC{ObT, HomT, C<:Model{Tuple{ObT, HomT}}} <: Model{Tuple{SliceOb{ObT, HomT}, HomT}}
+@struct_hash_equal struct SliceC{ObT, HomT, C}
   cat::C
   over::ObT
-  # function SliceC(cat, over)
-  #   implements(cat, ThCategory)
-  #   new(cat, Ob[cat](over))
-  # end
+  function SliceC(cat::C, over) where C
+    implements(cat, ThCategory) || error("Bad cat $cat")
+    obtype = impl_type(cat, ThCategory, :Ob)
+    homtype = impl_type(cat, ThCategory, :Hom)
+    new{obtype, homtype, C}(cat, ThCategory.Ob[cat](over))
+  end
 end
 
 using .ThCategory
diff --git a/src/syntax/GATs.jl b/src/syntax/GATs.jl
index 19326a16..e2c54d3c 100644
--- a/src/syntax/GATs.jl
+++ b/src/syntax/GATs.jl
@@ -14,7 +14,7 @@ export Constant, AlgTerm, AlgType, AlgAST,
 using ..Scopes
 import ..ExprInterop: fromexpr, toexpr
 
-import ..Scopes: retag, rename, reident
+import ..Scopes: retag, rename, reident, gettag
 
 import AlgebraicInterfaces: equations
 
diff --git a/src/syntax/TheoryInterface.jl b/src/syntax/TheoryInterface.jl
index 8de48c6c..6ceea774 100644
--- a/src/syntax/TheoryInterface.jl
+++ b/src/syntax/TheoryInterface.jl
@@ -1,14 +1,11 @@
 module TheoryInterface
-export @theory, @signature, Model, invoke_term
+export @theory, @signature, invoke_term
 
 using ..Scopes, ..GATs, ..ExprInterop, GATlab.Util
-# using GATlab.Util
 
 using MLStyle, StructEquality, Markdown
 
-abstract type Model{Tup <: Tuple} end
-
-@struct_hash_equal struct WithModel{M <: Model}
+@struct_hash_equal struct WithModel{M}
   model::M
 end
 
@@ -191,8 +188,8 @@ function juliadeclaration(name::Symbol)
   quote
     function $name end
 
-    if Base.isempty(Base.methods(Base.getindex, [typeof($name), $(GlobalRef(TheoryInterface, :Model))]))
-      function Base.getindex(::typeof($name), m::$(GlobalRef(TheoryInterface, :Model)))
+    if Base.isempty(Base.methods(Base.getindex, [typeof($name), Any]))
+      function Base.getindex(::typeof($name), m::Any) 
         (args...; context=nothing) -> $name($(GlobalRef(TheoryInterface, :WithModel))(m), args...; context)
       end
     end
diff --git a/src/syntax/TheoryMaps.jl b/src/syntax/TheoryMaps.jl
index fae0f915..4364dfef 100644
--- a/src/syntax/TheoryMaps.jl
+++ b/src/syntax/TheoryMaps.jl
@@ -402,8 +402,6 @@ macro theorymap(head, body)
   codom = macroexpand(__module__, :($codomname.Meta.@theory))
   tmap = fromexpr(dom, codom, body, TheoryMap)
 
-  mig = migrator(tmap, dommod, codommod, dom, codom)
-
   esc(
     Expr(
       :toplevel,
@@ -413,8 +411,6 @@ macro theorymap(head, body)
           macro map() $tmap end
           macro dom() $dommod end
           macro codom() $codommod end
-
-          $mig
         end
       ),
       :(Core.@__doc__ $(name)),
diff --git a/src/syntax/gats/gat.jl b/src/syntax/gats/gat.jl
index eb6841a6..ed5eee0b 100644
--- a/src/syntax/gats/gat.jl
+++ b/src/syntax/gats/gat.jl
@@ -379,3 +379,5 @@ end
 
 """Get all structs in a theory"""
 structs(t::GAT) = AlgStruct[getvalue(t[methodof(s)]) for s in struct_sorts(t)]
+
+gettag(T::GAT) = gettag(T.segments.scopes[end])
diff --git a/test/models/ModelInterface.jl b/test/models/ModelInterface.jl
index 5b16ed45..1e01eeea 100644
--- a/test/models/ModelInterface.jl
+++ b/test/models/ModelInterface.jl
@@ -1,11 +1,8 @@
 module TestModelInterface 
 
-using GATlab
-using Test
-using StructEquality
+using GATlab, Test, StructEquality
 
-@struct_hash_equal struct FinSetC <: Model{Tuple{Int, Vector{Int}}}
-end
+@struct_hash_equal struct FinSetC end
 
 @instance ThCategory{Int, Vector{Int}} [model::FinSetC] begin
   # check f is Hom: n -> m
@@ -58,7 +55,7 @@ end
 @test implements(FinSetC(), ThCategory)
 
 # Todo: get things working where Ob and Hom are the same type (i.e. binding dict not monic)
-struct TypedFinSetC <: Model{Tuple{Vector{Int}, Vector{Int}}}
+struct TypedFinSetC
   ntypes::Int
 end
 
@@ -199,7 +196,7 @@ end
 #################################
  
 """ Assume this implements Base.iterate """
-abstract type MyAbsIter{V} <: Model{Tuple{V}} end
+abstract type MyAbsIter{V} end
 
 struct MyVect{V} <: MyAbsIter{V}
   v::Vector{V}
diff --git a/test/stdlib/FinMatrices.jl b/test/stdlib/FinMatrices.jl
index 4bce8cce..c1376bd1 100644
--- a/test/stdlib/FinMatrices.jl
+++ b/test/stdlib/FinMatrices.jl
@@ -20,4 +20,7 @@ using .ThCategory
 
 end
 
-end
+# Test that `impl_type` is sensitive to the `where` parameters
+@test impl_type(FinMatC{Float64}(), ThCategory, :Hom) == Matrix{Float64}
+
+end # module
diff --git a/test/stdlib/FinSets.jl b/test/stdlib/FinSets.jl
index 7887388e..fd81b07b 100644
--- a/test/stdlib/FinSets.jl
+++ b/test/stdlib/FinSets.jl
@@ -16,4 +16,4 @@ using .ThCategory
   @test codom([5]; context=(codom=10,)) == 10
 end
 
-end
+end # module
diff --git a/test/stdlib/Nothings.jl b/test/stdlib/Nothings.jl
index 2cae9977..a199bc00 100644
--- a/test/stdlib/Nothings.jl
+++ b/test/stdlib/Nothings.jl
@@ -13,4 +13,4 @@ using .ThCategory
   @test isnothing(compose(nothing, nothing))
 end
 
-end
+end # module
diff --git a/test/stdlib/Op.jl b/test/stdlib/Op.jl
index b0e698f2..905dab0b 100644
--- a/test/stdlib/Op.jl
+++ b/test/stdlib/Op.jl
@@ -35,5 +35,4 @@ end
   @test codom([5]) == 1
 end
 
-
 end # module
diff --git a/test/stdlib/SliceCategories.jl b/test/stdlib/SliceCategories.jl
index 046b706d..f428f836 100644
--- a/test/stdlib/SliceCategories.jl
+++ b/test/stdlib/SliceCategories.jl
@@ -2,7 +2,7 @@ module TestSliceCategories
 
 using GATlab, Test
 
-const C = SliceC{Int, Vector{Int}, FinSetC}(FinSetC(), 4)
+const C = SliceC(FinSetC(), 4)
 const MkOb = SliceOb{Int, Vector{Int}}
 
 using .ThCategory

From 86e6d51a71cc5f471bf4b575ca9a21dfe5bab199 Mon Sep 17 00:00:00 2001
From: Kris Brown <kris@topos.institute>
Date: Tue, 10 Dec 2024 15:59:22 -0800
Subject: [PATCH 2/2] Migrate models with theorymap modules, not theorymaps

---
 src/models/ModelInterface.jl | 17 +++++++++--------
 1 file changed, 9 insertions(+), 8 deletions(-)

diff --git a/src/models/ModelInterface.jl b/src/models/ModelInterface.jl
index 64d1177e..a31021b1 100644
--- a/src/models/ModelInterface.jl
+++ b/src/models/ModelInterface.jl
@@ -656,9 +656,9 @@ macro withmodel(model, subsexpr, body)
   )
 end
 
-
-migrate_model(F::Module, m::Any, new_model_name=nothing) = 
-  migrate_model(F.MAP, m, new_model_name)
+# Until GAT_MODULE_LOOKUP is debugged, we can only migrate with the Module
+# migrate_model(F::Module, m::Any, new_model_name=nothing) = 
+#   migrate_model(F.MAP, m, new_model_name)
 
 """
 Given a theory map A -> B, construct a new struct type which wraps a model of
@@ -669,12 +669,13 @@ instance of that struct type.
 Future work: There is some subtlety in how accessor functions should be handled.
 TODO: The new instance methods do not yet handle the `context` keyword argument.
 """
-function migrate_model(F::AbsTheoryMap, m::Any, new_model_name::Union{Nothing,Symbol}=nothing)
+function migrate_model(FM::Module, m::Any, new_model_name::Union{Nothing,Symbol}=nothing)
   new_model_name = isnothing(new_model_name) ? gensym(:Migrated) : new_model_name
-  dom_theory = dom(F)
-  codom_theory = codom(F)
-  dom_module = GAT_MODULE_LOOKUP[gettag(dom_theory)]
-  codom_module = GAT_MODULE_LOOKUP[gettag(codom_theory)]
+  F = FM.MAP
+  dom_module =  macroexpand(FM, :($FM.@dom)) #GAT_MODULE_LOOKUP[gettag(dom_theory)]
+  codom_module = macroexpand(FM, :($FM.@codom)) #GAT_MODULE_LOOKUP[gettag(codom_theory)]
+  dom_theory = dom_module.Meta.theory #dom(F)
+  codom_theory = codom_module.Meta.theory #codom(F)
 
   # Expressions which evaluate to the correct Julia type
   jltype_by_sort = Dict(map(sorts(dom_theory)) do v