Better test case for erasing holes

polarity-lang · Jan 5, 2025 · 22404b4 · 22404b4
1 parent bc374ba
commit 22404b4
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 6 deletions.
diff --git a/test/suites/success/038-erase-hole.ir.expected b/test/suites/success/038-erase-hole.ir.expected
@@ -1 +1,6 @@
-let foo { MkFoo(Unit) }
+use "../../../std/data/list.pol"
+use "../../../std/data/nat.pol"
+
+let foo(a) { Nil }
+
+let bar { foo(<ZST>) }
diff --git a/test/suites/success/038-erase-hole.pol b/test/suites/success/038-erase-hole.pol
@@ -1,7 +1,7 @@
-data Top { Unit }
+use "../../../std/data/list.pol"
+use "../../../std/data/nat.pol"
 
-data Foo(a : ?) {
-    MkFoo(a: Type, x: a): Foo(a)
-}
+-- | FIXME: At the moment, a is not erased.
+let foo(a: _) : List(a) { Nil(a) }
 
-let foo: Foo(Top) { MkFoo(Top, Unit) }
+let bar: List(Nat) { foo(Nat) }