add test

anoma · Oct 1, 2024 · 9e47481 · 9e47481
1 parent 3899c9b
commit 9e47481
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 0 deletions.
diff --git a/test/Typecheck/NegativeNew.hs b/test/Typecheck/NegativeNew.hs
@@ -98,6 +98,13 @@ arityTests =
       $ \case
         ErrExpectedFunctionType {} -> Nothing
         _ -> wrongError,
+    negTest
+      "Implicit name argument without name"
+      $(mkRelDir "Internal")
+      $(mkRelFile "issue3074.juvix")
+      $ \case
+        ErrUnsolvedMeta {} -> Nothing
+        _ -> wrongError,
     negArityTest
       "Expected explicit pattern"
       $(mkRelDir "Internal")

diff --git a/tests/negative/Internal/issue3074.juvix b/tests/negative/Internal/issue3074.juvix
@@ -0,0 +1,7 @@
+module issue3074;
+
+type T := mkT;
+
+fun {_ : T} : {A : Type} -> T := mkT;
+
+x : T := fun@{A := T};