- Added a rule that Void is a subtype of every other type.

- Added the type-checking rules for existential quantification (ExQ).
- Fixed one of the rules for type-checking universal quantification (UnivQ).

3 files changed, 42 insertions, 33 deletions

diff --git a/source/lux/data/list.lux b/source/lux/data/list.lux
index 7b9d4a60b..563282f32 100644
--- a/source/lux/data/list.lux
+++ b/source/lux/data/list.lux
@@ -190,7 +190,7 @@
     (#;Cons [x (#;Cons [sep (interpose sep xs')])])))
 
 (def #export (size list)
-  (-> List Int)
+  (All [a] (-> (List a) Int))
   (foldL (lambda [acc _] (i:+ 1 acc)) 0 list))
 
 (do-template [<name> <init> <op>]
diff --git a/src/lux/analyser.clj b/src/lux/analyser.clj
index 4e1093cec..c02ba03d0 100644
--- a/src/lux/analyser.clj
+++ b/src/lux/analyser.clj
@@ -68,7 +68,7 @@
       (&&lux/analyse-variant analyser (&/V &/$Right exo-type) idx values)
       )))
 
-(defn ^:private aba8 [analyse eval! compile-module compile-token exo-type token]
+(defn ^:private aba10 [analyse eval! compile-module compile-token exo-type token]
   (|case token
     ;; Arrays
     (&/$FormS (&/$Cons [_ (&/$SymbolS _ "_jvm_znewarray")] (&/$Cons ?length (&/$Nil))))
@@ -116,6 +116,12 @@
     (&/$FormS (&/$Cons [_ (&/$SymbolS _ "_jvm_laload")] (&/$Cons ?array (&/$Cons ?idx (&/$Nil)))))
     (&&host/analyse-jvm-laload analyse exo-type ?array ?idx)
 
+    _
+    (assert false (str "Unknown syntax: " (prn-str (&/show-ast (&&/|meta (&/T "" -1 -1) token)))))))
+
+(defn ^:private aba9 [analyse eval! compile-module compile-token exo-type token]
+  (|case token
+    ;; Arrays
     (&/$FormS (&/$Cons [_ (&/$SymbolS _ "_jvm_fnewarray")] (&/$Cons [_ (&/$SymbolS _ ?class)] (&/$Cons ?length (&/$Nil)))))
     (&&host/analyse-jvm-fnewarray analyse exo-type ?length)
     
@@ -143,6 +149,12 @@
     (&/$FormS (&/$Cons [_ (&/$SymbolS _ "_jvm_caload")] (&/$Cons ?array (&/$Cons ?idx (&/$Nil)))))
     (&&host/analyse-jvm-caload analyse exo-type ?array ?idx)
 
+    _
+    (aba10 analyse eval! compile-module compile-token exo-type token)))
+
+(defn ^:private aba8 [analyse eval! compile-module compile-token exo-type token]
+  (|case token
+    ;; Arrays
     (&/$FormS (&/$Cons [_ (&/$SymbolS _ "_jvm_anewarray")] (&/$Cons [_ (&/$TextS ?class)] (&/$Cons ?length (&/$Nil)))))
     (&&host/analyse-jvm-anewarray analyse exo-type ?class ?length)
 
@@ -156,8 +168,7 @@
     (&&host/analyse-jvm-arraylength analyse exo-type ?array)
 
     _
-    (do (prn 'aba8 (&/adt->text token))
-      (assert false (str "Unknown syntax: " (prn-str (&/show-ast (&&/|meta (&/T "" -1 -1) token))))))))
+    (aba9 analyse eval! compile-module compile-token exo-type token)))
 
 (defn ^:private aba7 [analyse eval! compile-module compile-token exo-type token]
   (|case token
diff --git a/src/lux/type.clj b/src/lux/type.clj
index 7eae7e181..ed0dd8898 100644
--- a/src/lux/type.clj
+++ b/src/lux/type.clj
@@ -638,10 +638,13 @@
         (check* class-loader fixpoints invariant?? expected actual*))
 
       [(&/$UnivQ _) _]
-      (with-var
-        (fn [$arg]
-          (|do [expected* (apply-type expected $arg)]
-            (check* class-loader fixpoints invariant?? expected* actual))))
+      (|do [$arg existential
+            expected* (apply-type expected $arg)]
+        (check* class-loader fixpoints invariant?? expected* actual))
+      ;; (with-var
+      ;;   (fn [$arg]
+      ;;     (|do [expected* (apply-type expected $arg)]
+      ;;       (check* class-loader fixpoints invariant?? expected* actual))))
 
       [_ (&/$UnivQ _)]
       (with-var
@@ -649,6 +652,23 @@
           (|do [actual* (apply-type actual $arg)]
             (check* class-loader fixpoints invariant?? expected actual*))))
 
+      [(&/$ExQ e!env e!def) _]
+      (with-var
+        (fn [$arg]
+          (|let [expected* (beta-reduce (->> e!env
+                                             (&/Cons$ expected)
+                                             (&/Cons$ $arg))
+                                        e!def)]
+            (check* class-loader fixpoints invariant?? expected* actual))))
+
+      [_ (&/$ExQ a!env a!def)]
+      (|do [$arg existential]
+        (|let [actual* (beta-reduce (->> a!env
+                                         (&/Cons$ expected)
+                                         (&/Cons$ $arg))
+                                    a!def)]
+          (check* class-loader fixpoints invariant?? expected actual*)))
+
       [(&/$DataT e!data) (&/$DataT a!data)]
       (&&host/check-host-types (partial check* class-loader fixpoints true)
                                check-error
@@ -658,31 +678,6 @@
                                invariant??
                                e!data
                                a!data)
-      ;; [(&/$DataT e!name e!params) (&/$DataT a!name a!params)]
-      ;; (cond (= "#Null" a!name)
-      ;;       (if (not (&&host/primitive-type? e!name))
-      ;;         (return (&/T fixpoints nil))
-      ;;         (fail (check-error expected actual)))
-
-      ;;       (= "#Null" e!name)
-      ;;       (if (= "#Null" a!name)
-      ;;         (return (&/T fixpoints nil))
-      ;;         (fail (check-error expected actual)))
-
-      ;;       :else
-      ;;       (let [e!name (&&host/as-obj e!name)
-      ;;             a!name (&&host/as-obj a!name)]
-      ;;         (cond (and (.equals ^Object e!name a!name)
-      ;;                    (= (&/|length e!params) (&/|length a!params)))
-      ;;               (|do [_ (&/map2% (partial check* class-loader fixpoints true) e!params a!params)]
-      ;;                 (return (&/T fixpoints nil)))
-
-      ;;               (not invariant??)
-      ;;               (|do [actual* (&&host/->super-type existential class-loader e!name a!name a!params)]
-      ;;                 (check* class-loader fixpoints invariant?? expected actual*))
-
-      ;;               :else
-      ;;               (fail (str "[Type Error] Names don't match: " e!name " =/= " a!name)))))
 
       [(&/$LambdaT eI eO) (&/$LambdaT aI aO)]
       (|do [[fixpoints* _] (check* class-loader fixpoints invariant?? aI eI)]
@@ -696,6 +691,9 @@
                                  e!members a!members)]
         (return (&/T fixpoints* nil)))
       
+      [_ (&/$VariantT (&/$Nil))]
+      (return (&/T fixpoints nil))
+
       [(&/$VariantT e!cases) (&/$VariantT a!cases)]
       (|do [fixpoints* (&/fold2% (fn [fp e a]
                                    (|do [[fp* _] (check* class-loader fp invariant?? e a)]