From cc441378e207271885fc06d3fe8bff5520bd165d Mon Sep 17 00:00:00 2001
From: Kris Brown <kris@topos.institute>
Date: Tue, 10 Dec 2024 01:13:42 -0800
Subject: [PATCH] Optional typed wrapper constructor where type parameters are
 provided

Weaken
---
 src/syntax/TheoryInterface.jl | 11 +++++++++++
 test/models/ModelInterface.jl |  2 ++
 2 files changed, 13 insertions(+)

diff --git a/src/syntax/TheoryInterface.jl b/src/syntax/TheoryInterface.jl
index faaa846..de69ab4 100644
--- a/src/syntax/TheoryInterface.jl
+++ b/src/syntax/TheoryInterface.jl
@@ -329,6 +329,9 @@ function wrapper(name::Symbol, t::GAT, mod)
       Xs = map(Ts) do s 
         :($(GlobalRef($(TheoryInterface), :impl_type))(x, $($(name)), $($(Meta.quot)(s))))
       end
+      XTs = map(zip(Ts,Xs)) do (T,X)
+        :($X <: $T || error("Mismatch $($($(Meta.quot)(T))): $($X) ⊄ $($T)"))
+      end
       esc(quote 
         # Catch any potential docs above the macro call
         const $(doctarget) = nothing
@@ -337,6 +340,14 @@ function wrapper(name::Symbol, t::GAT, mod)
         # Declare the wrapper struct
         struct $n{$(Ts...)} <: $abs
           val::Any
+          function $n{$(Ts...)}(x::Any) where {$(Ts...)}
+            $($(GlobalRef(TheoryInterface, :implements)))(x, $($name)) || error(
+              "Invalid $($($(name))) model: $x")
+            $(XTs...)
+            # CHECK THAT THE GIVEN PARAMETERS MATCH Xs
+            new{$(Ts...)}(x)
+          end
+
           function $n(x::Any)
             $($(GlobalRef(TheoryInterface, :implements)))(x, $($name)) || error(
               "Invalid $($($(name))) model: $x")
diff --git a/test/models/ModelInterface.jl b/test/models/ModelInterface.jl
index 733ff91..3e5e262 100644
--- a/test/models/ModelInterface.jl
+++ b/test/models/ModelInterface.jl
@@ -262,6 +262,8 @@ ThCategory.Meta.@wrapper Cat2 <: MyAbsType
 ThCategory.Meta.@typed_wrapper TCat
 
 c = TCat(FinSetC())
+@test c == TCat{Int,Vector{Int}}(FinSetC())
+@test_throws ErrorException TCat{Bool,Symbol}(FinSetC()) # Ob: Int ⊄ Bool
 @test c isa TCat{Int, Vector{Int}}
 @test id(c, 2) == [1,2]