add test

anoma · May 4, 2023 · e55357e · e55357e
1 parent 8ae1d3a
commit e55357e
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 0 deletions.
diff --git a/test/Typecheck/Positive.hs b/test/Typecheck/Positive.hs
@@ -202,6 +202,10 @@ tests =
       "Mutual inference inside let"
       $(mkRelDir ".")
       $(mkRelFile "MutualLet.juvix"),
+    posTest
+      "id application in type"
+      $(mkRelDir ".")
+      $(mkRelFile "IdInType.juvix"),
     posTest
       "Nested pattern match with type variables"
       $(mkRelDir ".")

diff --git a/tests/positive/IdInType.juvix b/tests/positive/IdInType.juvix
@@ -0,0 +1,10 @@
+module IdInType;
+
+type Unit :=
+  | unit : Unit;
+
+id : {a : Type} -> a -> a;
+id a := a;
+
+f : id Unit -> Unit;
+f _ := unit;