add test

anoma · Oct 1, 2024 · 165f748 · 165f748
1 parent 317af4a
commit 165f748
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 0 deletions.
diff --git a/test/Typecheck/Negative.hs b/test/Typecheck/Negative.hs
@@ -265,6 +265,13 @@ tests =
       $(mkRelFile "Main.juvix")
       $ \case
         ErrWrongType {} -> Nothing
+        _ -> wrongError,
+    negTest
+      "Implicit name argument without name"
+      $(mkRelDir "Internal")
+      $(mkRelFile "issue3074.juvix")
+      $ \case
+        ErrUnsolvedMeta {} -> Nothing
         _ -> wrongError
   ]
 

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};