From 7e81a46f577f2a2bb3e4773db0e650af40948b9f Mon Sep 17 00:00:00 2001
From: Owen Lynch <root@owenlynch.org>
Date: Tue, 2 Jul 2024 18:42:01 -0700
Subject: [PATCH] more coverage for algclosure

---
 src/syntax/GATs.jl          |  3 ++-
 src/syntax/gats/closures.jl |  6 ++++--
 test/syntax/GATs.jl         | 12 +++++++++++-
 3 files changed, 17 insertions(+), 4 deletions(-)

diff --git a/src/syntax/GATs.jl b/src/syntax/GATs.jl
index c05bb34..25447be 100644
--- a/src/syntax/GATs.jl
+++ b/src/syntax/GATs.jl
@@ -9,7 +9,8 @@ export Constant, AlgTerm, AlgType, AlgAST,
   termcons,typecons, accessors, structs, primitive_sorts, struct_sorts,
   equations, build_infer_expr, compile, sortcheck, allnames, sorts, sortname,
   InCtx, TermInCtx, TypeInCtx, headof, argsof, methodof, bodyof, argcontext,
-  infer_type
+  infer_type,
+  tcompose
 
 using ..Scopes
 import ..ExprInterop: fromexpr, toexpr
diff --git a/src/syntax/gats/closures.jl b/src/syntax/gats/closures.jl
index 366cc40..bf30076 100644
--- a/src/syntax/gats/closures.jl
+++ b/src/syntax/gats/closures.jl
@@ -115,8 +115,10 @@ function tcompose(fs::Dtry{AlgClosure}, argnames::Vector{Symbol})
 end
 
 function (f::AlgClosure)(argvals::Any...)
-  if length(f.methods) > 1 && any(!(x isa AlgTerm) for x in argvals)
-    error("cannot infer type of non-AlgTerm value $x")
+  for x in argvals
+    if !(x isa AlgTerm)
+      error("cannot infer type of non-AlgTerm value $x")
+    end
   end
   sorts = AlgSort[sortcheck.(Ref(f.theory), argvals)...]
   if !haskey(f.methods, sorts)
diff --git a/test/syntax/GATs.jl b/test/syntax/GATs.jl
index 00b930b..6bd240d 100644
--- a/test/syntax/GATs.jl
+++ b/test/syntax/GATs.jl
@@ -157,6 +157,8 @@ end
   id_span(x) := Span(x, id(x),id(x)) ⊣ [x::Ob]
 end
 
+@test Base.isempty(GAT(:_EMPTY))
+
 # Dtrys
 
 tuplescope = fromexpr(ThMonoid.Meta.theory, :([x::(a::(s,t),b)]), TypeScope)
@@ -165,6 +167,14 @@ tuplescope = fromexpr(ThMonoid.Meta.theory, :([x::(a::(s,t),b)]), TypeScope)
   x * y + x * x
 end
 
-@test Base.isempty(GAT(:_EMPTY))
+@test only(f.methods)[2](1, 2) isa AlgTerm
+@test_throws ErrorException f(1, 2)
+@test_throws ErrorException f()
+
+@test sprint(show, f) isa String
+
+@test tcompose(
+    Dtrys.node(:a => Dtrys.leaf(f), :b => Dtrys.leaf(f)), [:x, :y]
+  ) isa AlgClosure
 
 end # module