From cd70563b5bc2793aa1ad905309c2c9f00550603c Mon Sep 17 00:00:00 2001
From: Gardanta Spirito <guardspirit@protonmail.com>
Date: Tue, 15 Aug 2023 23:39:11 +0300
Subject: [PATCH] Preserve inner exists/forall (#62)

---
 src/Grace/Infer.hs                            | 20 +++++++++----------
 .../complex/preserve-inner-exists-input.ffg   |  4 ++++
 .../complex/preserve-inner-exists-output.ffg  |  1 +
 .../complex/preserve-inner-exists-type.ffg    |  1 +
 .../complex/preserve-inner-forall-input.ffg   |  4 ++++
 .../complex/preserve-inner-forall-output.ffg  |  1 +
 .../complex/preserve-inner-forall-type.ffg    |  1 +
 7 files changed, 22 insertions(+), 10 deletions(-)
 create mode 100644 tasty/data/complex/preserve-inner-exists-input.ffg
 create mode 100644 tasty/data/complex/preserve-inner-exists-output.ffg
 create mode 100644 tasty/data/complex/preserve-inner-exists-type.ffg
 create mode 100644 tasty/data/complex/preserve-inner-forall-input.ffg
 create mode 100644 tasty/data/complex/preserve-inner-forall-output.ffg
 create mode 100644 tasty/data/complex/preserve-inner-forall-type.ffg

diff --git a/src/Grace/Infer.hs b/src/Grace/Infer.hs
index df9445a..5db239d 100644
--- a/src/Grace/Infer.hs
+++ b/src/Grace/Infer.hs
@@ -313,6 +313,16 @@ subtype _A0 _B0 = do
         -- except with the arguments flipped.  Similarly, the <:∃L rule is
         -- basically the same as the <:∀R rule with the arguments flipped.
 
+        -- <:∃L
+        (Type.Exists{..}, _) -> do
+            scoped (Context.Variable domain name) do
+                subtype type_ _B0
+
+        -- <:∀R
+        (_, Type.Forall{..}) -> do
+            scoped (Context.Variable domain name) do
+                subtype _A0 type_
+
         -- <:∃R
         (_, Type.Exists{ domain = Domain.Type, .. }) -> do
             scopedUnsolvedType nameLocation \a ->
@@ -339,16 +349,6 @@ subtype _A0 _B0 = do
             scopedUnsolvedAlternatives \a -> do
                 subtype (Type.substituteAlternatives name 0 a type_) _B0
 
-        -- <:∃L
-        (Type.Exists{..}, _) -> do
-            scoped (Context.Variable domain name) do
-                subtype type_ _B0
-
-        -- <:∀R
-        (_, Type.Forall{..}) -> do
-            scoped (Context.Variable domain name) do
-                subtype _A0 type_
-
         (Type.Scalar{ scalar = s0 }, Type.Scalar{ scalar = s1 })
             | s0 == s1 -> do
                 return ()
diff --git a/tasty/data/complex/preserve-inner-exists-input.ffg b/tasty/data/complex/preserve-inner-exists-input.ffg
new file mode 100644
index 0000000..fa0d306
--- /dev/null
+++ b/tasty/data/complex/preserve-inner-exists-input.ffg
@@ -0,0 +1,4 @@
+let wrappedVal
+  : { wrapped : exists (a : Type). a }
+  = { wrapped : 0 }
+in wrappedVal : { wrapped: exists (a : Type). a }
diff --git a/tasty/data/complex/preserve-inner-exists-output.ffg b/tasty/data/complex/preserve-inner-exists-output.ffg
new file mode 100644
index 0000000..4ee0269
--- /dev/null
+++ b/tasty/data/complex/preserve-inner-exists-output.ffg
@@ -0,0 +1 @@
+{ "wrapped": 0 }
diff --git a/tasty/data/complex/preserve-inner-exists-type.ffg b/tasty/data/complex/preserve-inner-exists-type.ffg
new file mode 100644
index 0000000..886060b
--- /dev/null
+++ b/tasty/data/complex/preserve-inner-exists-type.ffg
@@ -0,0 +1 @@
+{ wrapped: exists (a : Type) . a }
diff --git a/tasty/data/complex/preserve-inner-forall-input.ffg b/tasty/data/complex/preserve-inner-forall-input.ffg
new file mode 100644
index 0000000..1d94cd9
--- /dev/null
+++ b/tasty/data/complex/preserve-inner-forall-input.ffg
@@ -0,0 +1,4 @@
+let wrappedId
+  : { wrapped : forall (a : Type). a -> a }
+  = { wrapped : \x -> x }
+in wrappedId : { wrapped: forall (a : Type). a -> a }
diff --git a/tasty/data/complex/preserve-inner-forall-output.ffg b/tasty/data/complex/preserve-inner-forall-output.ffg
new file mode 100644
index 0000000..0719988
--- /dev/null
+++ b/tasty/data/complex/preserve-inner-forall-output.ffg
@@ -0,0 +1 @@
+{ "wrapped": \x -> x }
diff --git a/tasty/data/complex/preserve-inner-forall-type.ffg b/tasty/data/complex/preserve-inner-forall-type.ffg
new file mode 100644
index 0000000..3289e9c
--- /dev/null
+++ b/tasty/data/complex/preserve-inner-forall-type.ffg
@@ -0,0 +1 @@
+{ wrapped: forall (a : Type) . a -> a }