From d9093178ba495a3ab9018d8f69354086c924b006 Mon Sep 17 00:00:00 2001 From: Patrick Oscar Boykin Date: Mon, 20 Nov 2023 09:29:41 -1000 Subject: [PATCH] add test using existentials in pattern matching --- .../org/bykn/bosatsu/EvaluationTest.scala | 25 +++++++++++++++++++ 1 file changed, 25 insertions(+) diff --git a/core/src/test/scala/org/bykn/bosatsu/EvaluationTest.scala b/core/src/test/scala/org/bykn/bosatsu/EvaluationTest.scala index fffef5c27..4c0cc9af4 100644 --- a/core/src/test/scala/org/bykn/bosatsu/EvaluationTest.scala +++ b/core/src/test/scala/org/bykn/bosatsu/EvaluationTest.scala @@ -3179,6 +3179,31 @@ res = match empty: case [_, *_]: 1 test = Assertion(res matches 0, "one") +"""), "Foo", 1) + + } + + test("existential quantification in a match") { + runBosatsuTest(List(""" +package Foo + +enum FreeF[a]: + Pure(a: a) + Mapped(tup: exists b. (FreeF[b], b -> a)) + +def pure(a: a) -> FreeF[a]: Pure(a) +def map[a, b](f: FreeF[a], fn: a -> b) -> FreeF[b]: + tup: exists x. (FreeF[x], x -> b) = (f, fn) + Mapped(tup) + +def run[a](fa: FreeF[a]) -> a: + recur fa: + case Pure(a): a + case Mapped((prev, fn)): + fn(run(prev)) + +res = run(pure(0).map(x -> x.add(1))) +test = Assertion(res matches 1, "one") """), "Foo", 1) }