Properly handling variance for arrays to avoid invalid subtyping.

5 files changed, 77 insertions, 20 deletions

diff --git a/lux-bootstrapper/src/lux/analyser/proc/jvm.clj b/lux-bootstrapper/src/lux/analyser/proc/jvm.clj
index 38310e60c..0cfa8c873 100644
--- a/lux-bootstrapper/src/lux/analyser/proc/jvm.clj
+++ b/lux-bootstrapper/src/lux/analyser/proc/jvm.clj
@@ -206,7 +206,7 @@
 
     (&/$GenericArray param)
     (|do [=param (generic-class->type env param)]
-      (return (&/$Primitive &host-type/array-data-tag (&/|list =param))))
+      (return (&type/Array =param)))
 
     (&/$GenericWildcard _)
     (return (&/$ExQ &/$End (&/$Parameter 1)))
@@ -568,7 +568,7 @@
                    &&a-parser/parse-gclass)
           gtype-env &/get-type-env
           =gclass (&host-type/instance-gtype &type/existential gtype-env gclass)
-          :let [array-type (&/$Primitive &host-type/array-data-tag (&/|list =gclass))]
+          :let [array-type (&type/Array =gclass)]
           =length (&&/analyse-1 analyse length-type length)
           _ (&type/check exo-type array-type)
           _location &/location]
@@ -578,11 +578,14 @@
   (defn- analyse-jvm-aaload [analyse exo-type ?values]
     (|do [:let [(&/$Item array (&/$Item idx (&/$End))) ?values]
           =array (&&/analyse-1+ analyse array)
-          [arr-class arr-params] (ensure-object (&&/expr-type* =array))
+          array-type (&type/normal (&&/expr-type* =array))
+          [arr-class arr-params] (ensure-object array-type)
           _ (&/assert! (= &host-type/array-data-tag arr-class) (str "[Analyser Error] Expected array. Instead got: " arr-class))
-          :let [(&/$Item inner-arr-type (&/$End)) arr-params]
+          :let [(&/$Item mutable_type (&/$End)) arr-params
+                (&/$Primitive "#Mutable" (&/$Item type_variance (&/$End))) mutable_type
+                (&/$Function write_type read_type) type_variance]
           =idx (&&/analyse-1 analyse idx-type idx)
-          _ (&type/check exo-type inner-arr-type)
+          _ (&type/check exo-type read_type)
           _location &/location]
       (return (&/|list (&&/|meta exo-type _location
                                  (&&/$proc (&/T ["jvm" "aaload"]) (&/|list =array =idx) (&/|list)))))))
@@ -590,12 +593,14 @@
   (defn- analyse-jvm-aastore [analyse exo-type ?values]
     (|do [:let [(&/$Item array (&/$Item idx (&/$Item elem (&/$End)))) ?values]
           =array (&&/analyse-1+ analyse array)
-          :let [array-type (&&/expr-type* =array)]
+          array-type (&type/normal (&&/expr-type* =array))
           [arr-class arr-params] (ensure-object array-type)
           _ (&/assert! (= &host-type/array-data-tag arr-class) (str "[Analyser Error] Expected array. Instead got: " arr-class))
-          :let [(&/$Item inner-arr-type (&/$End)) arr-params]
+          :let [(&/$Item mutable_type (&/$End)) arr-params
+                (&/$Primitive "#Mutable" (&/$Item type_variance (&/$End))) mutable_type
+                (&/$Function write_type read_type) type_variance]
           =idx (&&/analyse-1 analyse idx-type idx)
-          =elem (&&/analyse-1 analyse inner-arr-type elem)
+          =elem (&&/analyse-1 analyse write_type elem)
           _ (&type/check exo-type array-type)
           _location &/location]
       (return (&/|list (&&/|meta exo-type _location
diff --git a/lux-bootstrapper/src/lux/compiler/jvm/proc/host.clj b/lux-bootstrapper/src/lux/compiler/jvm/proc/host.clj
index a455be83a..619e4b6f9 100644
--- a/lux-bootstrapper/src/lux/compiler/jvm/proc/host.clj
+++ b/lux-bootstrapper/src/lux/compiler/jvm/proc/host.clj
@@ -777,7 +777,11 @@
               ;; (&/$End) special-args
               ]
         ^MethodVisitor *writer* &/get-writer
-        array-type (&host/->java-sig (&a/expr-type* ?array))
+        normal_array_type (&type/normal (&a/expr-type* ?array))
+        :let [(&/$Primitive "#Array" (&/$Item mutable_type (&/$End))) normal_array_type
+              (&/$Primitive "#Mutable" (&/$Item type_variance (&/$End))) mutable_type
+              (&/$Function write_type read_type) type_variance]
+        array-type (&host/->java-sig (&/$Primitive "#Array" (&/|list read_type)))
         _ (compile ?array)
         :let [_ (.visitTypeInsn *writer* Opcodes/CHECKCAST array-type)]
         _ (compile ?idx)
@@ -792,7 +796,11 @@
               ;; (&/$End) special-args
               ]
         ^MethodVisitor *writer* &/get-writer
-        array-type (&host/->java-sig (&a/expr-type* ?array))
+        normal_array_type (&type/normal (&a/expr-type* ?array))
+        :let [(&/$Primitive "#Array" (&/$Item mutable_type (&/$End))) normal_array_type
+              (&/$Primitive "#Mutable" (&/$Item type_variance (&/$End))) mutable_type
+              (&/$Function write_type read_type) type_variance]
+        array-type (&host/->java-sig (&/$Primitive "#Array" (&/|list write_type)))
         _ (compile ?array)
         :let [_ (.visitTypeInsn *writer* Opcodes/CHECKCAST array-type)]
         :let [_ (.visitInsn *writer* Opcodes/DUP)]
@@ -809,7 +817,15 @@
               ;; (&/$End) special-args
               ]
         ^MethodVisitor *writer* &/get-writer
-        array-type (&host/->java-sig (&a/expr-type* ?array))
+        normal_array_type (&type/normal (&a/expr-type* ?array))
+        array-type (|case normal_array_type
+                     (&/$Primitive ?name (&/$End))
+                     (&host/->java-sig normal_array_type)
+
+                     (&/$Primitive "#Array" (&/$Item mutable_type (&/$End)))
+                     (|let [(&/$Primitive "#Mutable" (&/$Item type_variance (&/$End))) mutable_type
+                            (&/$Function write_type read_type) type_variance]
+                       (&host/->java-sig (&/$Primitive "#Array" (&/|list read_type)))))
         _ (compile ?array)
         :let [_ (.visitTypeInsn *writer* Opcodes/CHECKCAST array-type)]
         :let [_ (doto *writer*
diff --git a/lux-bootstrapper/src/lux/host.clj b/lux-bootstrapper/src/lux/host.clj
index 7b114a772..0abba888a 100644
--- a/lux-bootstrapper/src/lux/host.clj
+++ b/lux-bootstrapper/src/lux/host.clj
@@ -42,13 +42,19 @@
 (def ->package ->module-class)
 
 (defn unfold-array
-  "(-> Type (, Int Type))"
+  "(-> Type [Nat Type])"
   [type]
   (|case type
-    (&/$Primitive "#Array" (&/$Item param (&/$End)))
+    (&/$Primitive "#Array" (&/$Item (&/$Primitive "#Mutable" (&/$Item (&/$Function _ param)
+                                                                      (&/$End)))
+                                    (&/$End)))
     (|let [[count inner] (unfold-array param)]
       (&/T [(inc count) inner]))
 
+    (&/$Primitive "#Array" (&/$Item param (&/$End)))
+    (|let [[count inner] (unfold-array param)]
+      (&/T [(inc count) inner]))
+    
     _
     (&/T [0 type])))
 
@@ -59,7 +65,8 @@
     [^objects type]
     (|case type
       (&/$Primitive ?name params)
-      (cond (= &host-type/array-data-tag ?name) (|do [:let [[level base] (unfold-array type)]
+      (cond (= &host-type/array-data-tag ?name) (|do [normal_type (&type/normal type)
+                                                      :let [[level base] (unfold-array normal_type)]
                                                       base-sig (|case base
                                                                  (&/$Primitive base-class _)
                                                                  (return (&host-generics/->type-signature base-class))
diff --git a/lux-bootstrapper/src/lux/type.clj b/lux-bootstrapper/src/lux/type.clj
index e1e229ce9..657eb3077 100644
--- a/lux-bootstrapper/src/lux/type.clj
+++ b/lux-bootstrapper/src/lux/type.clj
@@ -40,8 +40,7 @@
 (def Text (&/$Named (&/T [&/prelude "Text"]) (&/$Primitive "#Text" &/$End)))
 (def Ident (&/$Named (&/T [&/prelude "Ident"]) (&/$Product Text Text)))
 
-(defn Array [elemT]
-  (&/$Primitive "#Array" (&/|list elemT)))
+(def Array &&host/Array)
 
 (def Nothing
   (&/$Named (&/T [&/prelude "Nothing"])
@@ -924,3 +923,25 @@
 
     _
     (return type)))
+
+(defn normal
+  "(-> Type Type)"
+  [it]
+  (|case it
+    (&/$Named _ ?it)
+    (normal ?it)
+
+    (&/$Primitive ?name ?parameters)
+    (|do [=parameters (&/map% normal ?parameters)]
+      (return (&/$Primitive ?name =parameters)))
+
+    (&/$Apply ?parameter ?abstraction)
+    (|do [reification (apply-type ?abstraction ?parameter)]
+      (normal reification))
+
+    (&/$Var id)
+    (|do [referenced (deref id)]
+      (normal referenced))
+
+    _
+    (return it)))
diff --git a/lux-bootstrapper/src/lux/type/host.clj b/lux-bootstrapper/src/lux/type/host.clj
index 692062f50..0ea72c98f 100644
--- a/lux-bootstrapper/src/lux/type/host.clj
+++ b/lux-bootstrapper/src/lux/type/host.clj
@@ -64,7 +64,11 @@
                     (&/$Parameter 1))))
 
 ;; [Exports]
+(def mutable-data-tag "#Mutable")
 (def array-data-tag "#Array")
+(defn Array [item]
+  (&/$Primitive array-data-tag (&/|list (&/$Primitive mutable-data-tag (&/|list (&/$Function item item))))))
+
 (def null-data-tag "#Null")
 (def i64-data-tag "#I64")
 (def nat-data-tag "#Nat")
@@ -135,7 +139,7 @@
           (let [base (or arr-obase simple-base (jprim->lprim arr-pbase))]
             (if (.equals "void" base)
               Any
-              (reduce (fn [inner _] (&/$Primitive array-data-tag (&/|list inner)))
+              (reduce (fn [inner _] (Array inner))
                       (&/$Primitive base (try (-> (Class/forName base) .getTypeParameters
                                                   seq count (repeat (&/$Primitive "java.lang.Object" &/$End))
                                                   &/->list)
@@ -152,7 +156,7 @@
 
         (instance? GenericArrayType refl-type)
         (|do [inner-type (instance-param existential matchings (.getGenericComponentType ^GenericArrayType refl-type))]
-          (return (&/$Primitive array-data-tag (&/|list inner-type))))
+          (return (Array inner-type)))
         
         (instance? ParameterizedType refl-type)
         (|do [:let [refl-type* ^ParameterizedType refl-type]
@@ -183,7 +187,11 @@
           (if (type= Any class-type)
             "V"
             (|case class-type
-              (&/$Primitive "#Array" (&/$Item (&/$Primitive class-name _) (&/$End)))
+              (&/$Primitive "#Array"
+                            (&/$Item (&/$Primitive "#Mutable"
+                                                   (&/$Item (&/$Function _ (&/$Primitive class-name _))
+                                                            (&/$End)))
+                                     (&/$End)))
               (str "[" (&host-generics/->type-signature class-name))
 
               (&/$Primitive class-name _)
@@ -211,7 +219,7 @@
   (|case gtype
     (&/$GenericArray component-type)
     (|do [inner-type (instance-gtype existential matchings component-type)]
-      (return (&/$Primitive array-data-tag (&/|list inner-type))))
+      (return (Array inner-type)))
     
     (&/$GenericClass type-name type-params)
     ;; When referring to type-parameters during class or method