Properly handling variance for arrays to avoid invalid subtyping.

6 files changed, 129 insertions, 75 deletions

diff --git a/stdlib/source/library/lux/data/collection/array.lux b/stdlib/source/library/lux/data/collection/array.lux
index 4a931cfae..eb0cf93b0 100644
--- a/stdlib/source/library/lux/data/collection/array.lux
+++ b/stdlib/source/library/lux/data/collection/array.lux
@@ -9,13 +9,18 @@
     [predicate {"+" Predicate}]]
    [data
     [collection
-     ["[0]" list]]]]]
+     ["[0]" list]]]
+   [type
+    [variance {"+"}]]]]
  ["!" \\unsafe])
 
 (def: .public type_name
   Text
   !.type)
 
+(type: .public Array'
+  !.Array')
+
 (type: .public Array
   !.Array)
 
@@ -24,73 +29,73 @@
   (|>> !.empty))
 
 (def: .public size
-  (All (_ a) (-> (Array a) Nat))
+  (All (_ r w) (-> (Array' r w) Nat))
   (|>> !.size))
 
 (def: .public (item index array)
-  (All (_ a)
-    (-> Nat (Array a) (Maybe a)))
+  (All (_ r w)
+    (-> Nat (Array' r w) (Maybe r)))
   (if (!.lacks? index array)
     {.#None}
     {.#Some (!.item index array)}))
 
 (def: .public (has! index value array)
-  (All (_ a)
-    (-> Nat a (Array a) (Array a)))
+  (All (_ r w)
+    (-> Nat w (Array' r w) (Array' r w)))
   (!.has! index value array))
 
 (def: .public (lacks! index array)
-  (All (_ a)
-    (-> Nat (Array a) (Array a)))
+  (All (_ r w)
+    (-> Nat (Array' r w) (Array' r w)))
   (!.lacks! index array))
 
 (def: .public (lacks? index array)
-  (All (_ a)
-    (-> Nat (Array a) Bit))
+  (All (_ r w)
+    (-> Nat (Array' r w) Bit))
   (!.lacks? index array))
 
 (def: .public (has? index array)
-  (All (_ a)
-    (-> Nat (Array a) Bit))
+  (All (_ r w)
+    (-> Nat (Array' r w) Bit))
   (!.has? index array))
 
 (def: .public (revised! index $ array)
-  (All (_ a)
-    (-> Nat (-> a a) (Array a) (Array a)))
+  (All (_ r w)
+    (-> Nat (-> r w) (Array' r w) (Array' r w)))
   (!.revised! index $ array))
 
 (def: .public (upsert! index default transform array)
-  (All (_ a)
-    (-> Nat a (-> a a) (Array a) (Array a)))
+  (All (_ r w)
+    (-> Nat r (-> r w) (Array' r w) (Array' r w)))
   (!.upsert! index default transform array))
 
 (def: .public (copy! length src_start src_array dest_start dest_array)
-  (All (_ a)
-    (-> Nat Nat (Array a) Nat (Array a)
-        (Array a)))
+  (All (_ r w)
+    (-> Nat Nat (Array' w Nothing) Nat (Array' r w)
+        (Array' r w)))
   (!.copy! length src_start src_array dest_start dest_array))
 
 (def: .public occupancy
-  (All (_ a) (-> (Array a) Nat))
+  (All (_ r w) (-> (Array' r w) Nat))
   (|>> !.occupancy))
 
 (def: .public vacancy
-  (All (_ a) (-> (Array a) Nat))
+  (All (_ r w) (-> (Array' r w) Nat))
   (|>> !.vacancy))
 
 (def: .public (only! ? it)
-  (All (_ a)
-    (-> (Predicate a) (Array a) (Array a)))
+  (All (_ r w)
+    (-> (Predicate r) (Array' r w) (Array' r w)))
   (!.only! ? it))
 
 (def: .public (example ? it)
-  (All (_ a)
-    (-> (Predicate a) (Array a) (Maybe a)))
+  (All (_ r w)
+    (-> (Predicate r) (Array' r w) (Maybe r)))
   (!.example ? it))
 
 (def: .public (example' ? it)
-  (All (_ a)
-    (-> (-> Nat a Bit) (Array a) (Maybe [Nat a])))
+  (All (_ r w)
+    (-> (-> Nat r Bit) (Array' r w) (Maybe [Nat r])))
   (!.example' ? it))
 
 (def: .public clone
@@ -102,11 +107,11 @@
   (|>> !.of_list))
 
 (def: .public (list default array)
-  (All (_ a) (-> (Maybe a) (Array a) (List a)))
+  (All (_ r w) (-> (Maybe r) (Array' r w) (List r)))
   (!.list default array))
 
 (implementation: .public (equivalence //)
-  (All (_ a) (-> (Equivalence a) (Equivalence (Array a))))
+  (All (_ r) (-> (Equivalence r) (Equivalence (Ex (_ w) (Array' r w)))))
   
   (def: (= left/* right/*)
     (!.= // left/* right/*)))
@@ -120,7 +125,7 @@
     (!.composite left/* right/*)))
 
 (implementation: .public mix
-  (Mix Array)
+  (Mix (All (_ r) (Array' r Nothing)))
   
   (def: (mix $ init it)
     (!.mix (function (_ index partial total)
@@ -134,17 +139,17 @@
   (def: (each $ input)
     (!.each $ input)))
 
-(def: .public (every? ? it)
-  (All (_ a)
-    (-> (Predicate a) (Predicate (Array a))))
-  (!.every? ? it))
+(template [<safe> <unsafe>]
+  [(def: .public (<safe> ? it)
+     (All (_ r w)
+       (-> (Predicate r) (Predicate (Array' r w))))
+     (<unsafe> ? it))]
 
-(def: .public (any? ? it)
-  (All (_ a)
-    (-> (Predicate a) (Predicate (Array a))))
-  (!.any? ? it))
+  [every? !.every?]
+  [any? !.any?]
+  )
 
 (def: .public (one ? it)
-  (All (_ a b)
-    (-> (-> a (Maybe b)) (Array a) (Maybe b)))
+  (All (_ r r' w)
+    (-> (-> r (Maybe r')) (Array' r w) (Maybe r')))
   (!.one ? it))
diff --git a/stdlib/source/library/lux/ffi.jvm.lux b/stdlib/source/library/lux/ffi.jvm.lux
index 2428f6bb2..2441cf387 100644
--- a/stdlib/source/library/lux/ffi.jvm.lux
+++ b/stdlib/source/library/lux/ffi.jvm.lux
@@ -382,8 +382,7 @@
                    (` {.#Primitive (~ (code.text (..reflection (jvm.array elementT)))) {.#End}})
                    
                    {.#None}
-                   (` {.#Primitive (~ (code.text array.type_name))
-                                   {.#Item (~ (value_type elementT)) {.#End}}}))]))
+                   (` ((~! array.Array) (~ (value_type elementT)))))]))
           ... else
           (undefined)
           )))
@@ -1691,8 +1690,9 @@
                     [jvm.double  "jvm array new double"]
                     [jvm.char    "jvm array new char"]))
               ... else
-              (in (list (` (.is (~ (value_type {#ManualPrM} (jvm.array type)))
-                                ("jvm array new object" (~ g!size))))))))))
+              (in (list (` (.as ((~! array.Array) (~ (value_type {#ManualPrM} type)))
+                                (.is (~ (value_type {#ManualPrM} (jvm.array type)))
+                                     ("jvm array new object" (~ g!size)))))))))))
 
 (exception: .public (cannot_convert_to_jvm_type [type .Type])
   (exception.report
@@ -1743,9 +1743,9 @@
 
                   (text#= array.type_name name)
                   (case params
-                    {.#Item elementLT {.#End}}
+                    {.#Item {.#Apply writeLT {.#Apply readLT _Mutable}} {.#End}}
                     (# meta.monad each jvm.array
-                       (lux_type->jvm_type context elementLT))
+                       (lux_type->jvm_type context readLT))
 
                     _
                     <failure>)
diff --git a/stdlib/source/library/lux/ffi.old.lux b/stdlib/source/library/lux/ffi.old.lux
index ce9e50959..32844a7d7 100644
--- a/stdlib/source/library/lux/ffi.old.lux
+++ b/stdlib/source/library/lux/ffi.old.lux
@@ -1727,5 +1727,5 @@
 (syntax: .public (type [type (..generic_type^ (list))])
   (in (list (..class_type {#ManualPrM} (list) type))))
 
-(template: .public (as type term)
+(template: .public (is type term)
   [(.as type term)])
diff --git a/stdlib/source/library/lux/target/jvm/reflection.lux b/stdlib/source/library/lux/target/jvm/reflection.lux
index 55b6a4185..4fe60fd37 100644
--- a/stdlib/source/library/lux/target/jvm/reflection.lux
+++ b/stdlib/source/library/lux/target/jvm/reflection.lux
@@ -183,8 +183,8 @@
         {.#Some reflection}
         ... TODO: Instead of having single lower/upper bounds, should
         ... allow for multiple ones.
-        (case [(array.read! 0 (java/lang/reflect/WildcardType::getLowerBounds reflection))
-               (array.read! 0 (java/lang/reflect/WildcardType::getUpperBounds reflection))]
+        (case [(array.item 0 (java/lang/reflect/WildcardType::getLowerBounds reflection))
+               (array.item 0 (java/lang/reflect/WildcardType::getUpperBounds reflection))]
           (^.template [<pattern> <kind>]
             [<pattern>
              (case (ffi.as java/lang/reflect/GenericArrayType bound)
diff --git a/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/jvm.lux b/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/jvm.lux
index 95915309c..6d7804b9a 100644
--- a/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/jvm.lux
+++ b/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/jvm.lux
@@ -65,7 +65,9 @@
    ["/[1]" // "_"
     [generation
      [jvm
-      ["[0]" runtime]]]
+      ["[0]" runtime]
+      ["[0]" function "_"
+       ["[1]" abstract]]]]
     ["/[1]" // "_"
      ["[0]" generation]
      ["[0]" directive]
@@ -387,6 +389,9 @@
             [(reflection.reflection reflection.char)    [box.char jvm.char]])
       (dictionary.of_list text.hash)))
 
+(template: (lux_array_type :read: :write:)
+  [{.#Primitive (static array.type_name) (list {.#Apply :write: {.#Apply :read: _Mutable}})}])
+
 (def: (jvm_type luxT)
   (-> .Type (Operation (Type Value)))
   (case luxT
@@ -401,7 +406,7 @@
       {.#None}
       (/////analysis.except ..non_jvm_type luxT))
 
-    (pattern {.#Primitive (static array.type_name) (list elemT)})
+    (pattern (lux_array_type elemT _))
     (phase#each jvm.array (jvm_type elemT))
 
     {.#Primitive class parametersT}
@@ -432,6 +437,9 @@
 
     {.#Ex _}
     (phase#in (jvm.class ..object_class (list)))
+
+    {.#Function _}
+    (phase#in function.class)
     
     _
     (/////analysis.except ..non_jvm_type luxT)))
@@ -467,13 +475,16 @@
     (case args
       (pattern (list arrayC))
       (<| typeA.with_var
-          (function (_ [@var :var:]))
+          (function (_ [@read :read:]))
+          typeA.with_var
+          (function (_ [@write :write:]))
           (do phase.monad
             [_ (typeA.inference ..int)
-             arrayA (<| (typeA.expecting (.type (array.Array :var:)))
+             arrayA (<| (typeA.expecting (.type (array.Array' :read: :write:)))
                         (analyse archive arrayC))
-             :var: (typeA.check (check.clean (list) :var:))
-             arrayJT (jvm_array_type (.type (array.Array :var:)))]
+             :read: (typeA.check (check.clean (list) :read:))
+             :write: (typeA.check (check.clean (list) :write:))
+             arrayJT (jvm_array_type (.type (array.Array' :read: :write:)))]
             (in {/////analysis.#Extension extension_name (list (/////analysis.text (..signature arrayJT))
                                                                arrayA)})))
 
@@ -520,8 +531,7 @@
 (def: (check_parameter objectT)
   (-> .Type (Operation (Type Parameter)))
   (case objectT
-    (pattern {.#Primitive (static array.type_name)
-                          (list elementT)})
+    (pattern (lux_array_type elementT _))
     (/////analysis.except ..non_parameter objectT)
     
     {.#Primitive name parameters}
@@ -573,6 +583,9 @@
       {.#None}
       (/////analysis.except ..non_parameter objectT))
 
+    {.#Function _}
+    (phase#in function.class)
+
     _
     (/////analysis.except ..non_parameter objectT)))
 
@@ -613,9 +626,8 @@
 
               ... else
               (phase#in (jvm.class name (list)))))
-    
-    (pattern {.#Primitive (static array.type_name)
-                          (list elementT)})
+
+    (pattern (lux_array_type elementT _))
     (|> elementT
         check_jvm
         (phase#each jvm.array))
@@ -701,15 +713,18 @@
     (case args
       (pattern (list idxC arrayC))
       (<| typeA.with_var
-          (function (_ [@var :var:]))
+          (function (_ [@read :read:]))
+          typeA.with_var
+          (function (_ [@write :write:]))
           (do phase.monad
-            [_ (typeA.inference :var:)
-             arrayA (<| (typeA.expecting (.type (array.Array :var:)))
+            [_ (typeA.inference :read:)
+             arrayA (<| (typeA.expecting (.type (array.Array' :read: :write:)))
                         (analyse archive arrayC))
-             :var: (typeA.check (check.clean (list) :var:))
-             arrayJT (jvm_array_type (.type (array.Array :var:)))
              idxA (<| (typeA.expecting ..int)
-                      (analyse archive idxC))]
+                      (analyse archive idxC))
+             :read: (typeA.check (check.clean (list) :read:))
+             :write: (typeA.check (check.clean (list) :write:))
+             arrayJT (jvm_array_type (.type (array.Array' :read: :write:)))]
             (in {/////analysis.#Extension extension_name (list (/////analysis.text (..signature arrayJT))
                                                                idxA
                                                                arrayA)})))
@@ -745,17 +760,20 @@
     (case args
       (pattern (list idxC valueC arrayC))
       (<| typeA.with_var
-          (function (_ [@var :var:]))
+          (function (_ [@read :read:]))
+          typeA.with_var
+          (function (_ [@write :write:]))
           (do phase.monad
-            [_ (typeA.inference (.type (array.Array :var:)))
-             arrayA (<| (typeA.expecting (.type (array.Array :var:)))
+            [_ (typeA.inference (.type (array.Array' :read: :write:)))
+             arrayA (<| (typeA.expecting (.type (array.Array' :read: :write:)))
                         (analyse archive arrayC))
-             :var: (typeA.check (check.clean (list) :var:))
-             arrayJT (jvm_array_type (.type (array.Array :var:)))
              idxA (<| (typeA.expecting ..int)
                       (analyse archive idxC))
-             valueA (<| (typeA.expecting :var:)
-                        (analyse archive valueC))]
+             valueA (<| (typeA.expecting :write:)
+                        (analyse archive valueC))
+             :read: (typeA.check (check.clean (list) :read:))
+             :write: (typeA.check (check.clean (list) :write:))
+             arrayJT (jvm_array_type (.type (array.Array' :read: :write:)))]
             (in {/////analysis.#Extension extension_name (list (/////analysis.text (..signature arrayJT))
                                                                idxA
                                                                valueA
diff --git a/stdlib/source/library/lux/type/variance.lux b/stdlib/source/library/lux/type/variance.lux
index 00d2d931e..93f80356a 100644
--- a/stdlib/source/library/lux/type/variance.lux
+++ b/stdlib/source/library/lux/type/variance.lux
@@ -1,6 +1,8 @@
 (.using
-  [library
-   [lux "*"]])
+ [library
+  [lux "*"
+   [meta
+    ["[0]" symbol]]]])
 
 (type: .public (Co it)
   (-> Any it))
@@ -10,3 +12,32 @@
 
 (type: .public (In it)
   (-> it it))
+
+(type: .public (Mutable r w)
+  (Primitive "#Mutable" [(-> w r)]))
+
+(template [<name> <type>]
+  [(template: .public (<name> it)
+     [((.is (.All (_ r w) <type>)
+            (.|>> .as_expected))
+       it)])]
+
+  [read (.-> (..Mutable r w) r)]
+  [write (.-> w (..Mutable r w))]
+  )
+
+(type: .public (Read_Only a)
+  (Mutable a Nothing))
+
+(type: .public (Write_Only a)
+  (Mutable Any a))
+
+(template [<name> <type>]
+  [(template: .public (<name> it)
+     [((.is (.All (_ r w) <type>)
+            (.|>>))
+       it)])]
+
+  [read_only (.-> (..Mutable r w) (..Read_Only r))]
+  [write_only (.-> (..Mutable r w) (..Write_Only w))]
+  )