Preserve inner exists/forall (#62)

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 ()

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 }

tasty/data/complex/preserve-inner-exists-output.ffg

@@ -0,0 +1 @@
+{ "wrapped": 0 }

tasty/data/complex/preserve-inner-exists-type.ffg

@@ -0,0 +1 @@
+{ wrapped: exists (a : Type) . a }

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 }

tasty/data/complex/preserve-inner-forall-output.ffg

@@ -0,0 +1 @@
+{ "wrapped": \x -> x }

tasty/data/complex/preserve-inner-forall-type.ffg

@@ -0,0 +1 @@
+{ wrapped: forall (a : Type) . a -> a }