Properly handling variance for arrays to avoid invalid subtyping.

7 files changed, 178 insertions, 122 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))]
+  )
diff --git a/stdlib/source/unsafe/lux/data/collection/array.lux b/stdlib/source/unsafe/lux/data/collection/array.lux
index e66d3ca3b..0a44efcf8 100644
--- a/stdlib/source/unsafe/lux/data/collection/array.lux
+++ b/stdlib/source/unsafe/lux/data/collection/array.lux
@@ -6,17 +6,23 @@
     ["[0]" functor]]
    [data
     [collection
-     ["[0]" list]]]]])
+     ["[0]" list]]]
+   [type
+    ["[0]" variance]]]])
 
 (def: .public type
   "#Array")
 
-(type: .public (Array a)
-  {.#Primitive ..type {.#Item a {.#End}}})
+(template [<item> <array>]
+  [(type: .public <array>
+     {.#Primitive ..type {.#Item <item> {.#End}}})]
+
+  [(variance.Mutable r w) (Array' r w)]
+  [(variance.Mutable a a) (Array a)]
+  )
 
 (with_expansions [<index_type> (.Primitive "java.lang.Long")
-                  <elem_type> (.Primitive "java.lang.Object")
-                  <array_type> (.type (..Array <elem_type>))]
+                  <item_type> (.Primitive "java.lang.Object")]
   (for @.jvm (template: (jvm_int value)
                [(.|> value
                      (.as <index_type>)
@@ -33,7 +39,7 @@
                        (~~ (.static @.jvm))
                        (|> (~~ (..jvm_int size))
                            "jvm array new object"
-                           (.is <array_type>)
+                           (.is (..Array <item_type>))
                            .as_expected)
 
                        (~~ (.static @.js)) ("js array new" size)
@@ -45,14 +51,13 @@
           <size>)]))
 
   (`` (template: .public (size <array>)
-        [((.is (.All (_ a) (.-> (..Array a) .Nat))
+        [((.is (.All (_ r w) (.-> (..Array' r w) .Nat))
                (.function (size array)
                  (.for (~~ (.static @.old))
                        ("jvm arraylength" array)
 
                        (~~ (.static @.jvm))
                        (.|> array
-                            (.as <array_type>)
                             "jvm array length object"
                             "jvm conversion int-to-long"
                             "jvm object cast"
@@ -71,8 +76,8 @@
     [(<null?> (<read!> index array))])
 
   (`` (template: .public (lacks? <index> <array>)
-        [((.is (.All (_ a)
-                 (.-> .Nat (..Array a) .Bit))
+        [((.is (.All (_ r w)
+                 (.-> .Nat (..Array' r w) .Bit))
                (.function (lacks? index array)
                  (.let [size (..size array)]
                    (.if ("lux i64 <" (.int size) (.int index))
@@ -81,7 +86,6 @@
 
                            (~~ (.static @.jvm))
                            (.|> array
-                                (.as <array_type>)
                                 ("jvm array read object" (~~ (jvm_int index)))
                                 "jvm object null?")
 
@@ -98,15 +102,14 @@
     [(.not (..lacks? index array))])
 
   (`` (template: .public (item <index> <array>)
-        [((.is (.All (_ a)
-                 (.-> .Nat (..Array a) a))
+        [((.is (.All (_ r w)
+                 (.-> .Nat (..Array' r w) r))
                (.function (item index array)
                  (.for (~~ (.static @.old))
                        ("jvm aaload" array index)
 
                        (~~ (.static @.jvm))
                        (.|> array
-                            (.as <array_type>)
                             ("jvm array read object" (~~ (jvm_int index)))
                             .as_expected)
 
@@ -119,16 +122,15 @@
           <index> <array>)]))
 
   (`` (template: .public (has! <index> <value> <array>)
-        [((.is (.All (_ a)
-                 (.-> .Nat a (..Array a) (..Array a)))
+        [((.is (.All (_ r w)
+                 (.-> .Nat w (..Array' r w) (..Array' r w)))
                (.function (has! index value array)
                  (.for (~~ (.static @.old))
                        ("jvm aastore" array index value)
 
                        (~~ (.static @.jvm))
                        (.|> array
-                            (.as <array_type>)
-                            ("jvm array write object" (~~ (jvm_int index)) (.as <elem_type> value))
+                            ("jvm array write object" (~~ (jvm_int index)) value)
                             .as_expected)
 
                        (~~ (.static @.js)) ("js array write" index value array)
@@ -140,8 +142,8 @@
           <index> <value> <array>)]))
 
   (`` (template: .public (lacks! <index> <array>)
-        [((.is (.All (_ a)
-                 (.-> .Nat (..Array a) (..Array a)))
+        [((.is (.All (_ r w)
+                 (.-> .Nat (..Array' r w) (..Array' r w)))
                (.function (lacks! index array)
                  (.let [size (..size array)]
                    (.if ("lux i64 <" (.int size) (.int index))
@@ -149,7 +151,7 @@
                            (..has! index (.as_expected ("jvm object null")) array)
                            
                            (~~ (.static @.jvm))
-                           (..has! index (.as_expected (is <elem_type> ("jvm object null"))) array)
+                           (..has! index (.as_expected (is <item_type> ("jvm object null"))) array)
 
                            (~~ (.static @.js)) ("js array delete" index array)
                            (~~ (.static @.python)) ("python array delete" index array)
@@ -162,8 +164,8 @@
   )
 
 (template: .public (revised! <index> <$> <array>)
-  [((.is (.All (_ a)
-           (.-> .Nat (.-> a a) (..Array a) (..Array a)))
+  [((.is (.All (_ r w)
+           (.-> .Nat (.-> r w) (..Array' r w) (..Array' r w)))
          (.function (revised! index $ array)
            (.if (..lacks? index array)
              array
@@ -171,8 +173,8 @@
     <index> <$> <array>)])
 
 (template: .public (upsert! <index> <default> <$> <array>)
-  [((.is (.All (_ a)
-           (.-> .Nat a (.-> a a) (..Array a) (..Array a)))
+  [((.is (.All (_ r w)
+           (.-> .Nat r (.-> r w) (..Array' r w) (..Array' r w)))
          (.function (upsert! index default $ array)
            (..has! index
                    ($ (.if (..lacks? index array)
@@ -182,9 +184,9 @@
     <index> <default> <$> <array>)])
 
 (template: .public (copy! <length> <src_start> <src_array> <dest_start> <dest_array>)
-  [((.is (.All (_ a)
-           (.-> .Nat .Nat (..Array a) .Nat (..Array a)
-                (..Array a)))
+  [((.is (.All (_ r w)
+           (.-> .Nat .Nat (..Array' w .Nothing) .Nat (..Array' r w)
+                (..Array' r w)))
          (.function (copy! length src_start src_array dest_start dest_array)
            (.loop (again [offset 0])
              (.if ("lux i64 <" (.int length) (.int offset))
@@ -200,7 +202,7 @@
 
 (template [<name> <when_lacks> <when_has>]
   [(template: .public (<name> <array>)
-     [((.is (.All (_ a) (.-> (..Array a) .Nat))
+     [((.is (.All (_ r w) (.-> (..Array' r w) .Nat))
             (.function (occupancy array)
               (.let [size (..size array)]
                 (.loop (again [index 0
@@ -217,8 +219,8 @@
   )
 
 (template: .public (only! <?> <it>)
-  [((.is (.All (_ a)
-           (.-> (.-> a .Bit) (..Array a) (..Array a)))
+  [((.is (.All (_ r w)
+           (.-> (.-> r .Bit) (..Array' r w) (..Array' r w)))
          (.function (only! ? it)
            (.let [size (..size it)]
              (.loop (again [index 0])
@@ -235,8 +237,8 @@
 
 (template [<name> <predicate> <test> <type> <term>]
   [(template: .public (<name> <?> <it>)
-     [((.is (.All (_ a)
-              (.-> <predicate> (..Array a) (.Maybe <type>)))
+     [((.is (.All (_ r w)
+              (.-> <predicate> (..Array' r w) (.Maybe <type>)))
             (.function (<name> ? it)
               (.let [size (..size it)]
                 (.loop (again [index 0])
@@ -250,8 +252,8 @@
                     {.#None})))))
        <?> <it>)])]
 
-  [example (.-> a .Bit) (? it) a it]
-  [example' (.-> Nat a .Bit) (? index it) [Nat a] [index it]]
+  [example (.-> r .Bit) (? it) r it]
+  [example' (.-> Nat r .Bit) (? index it) [Nat r] [index it]]
   )
 
 (template: .public (clone <it>)
@@ -283,7 +285,7 @@
   (-- 0))
 
 (`` (template: (list|-default <empty> <array>)
-      [((.is (.All (_ a) (.-> (.List a) (..Array a) (.List a)))
+      [((.is (.All (_ r w) (.-> (.List r) (..Array' r w) (.List r)))
              (.function (list|-default empty array)
                (.loop (again [index ("lux i64 -" 1 (..size array))
                               output empty])
@@ -296,7 +298,7 @@
         <empty> <array>)]))
 
 (`` (template: (list|+default <default> <array>)
-      [((.is (.All (_ a) (.-> a (..Array a) (.List a)))
+      [((.is (.All (_ r w) (.-> r (..Array' r w) (.List r)))
              (.function (list|+default default array)
                (.loop (again [index ("lux i64 -" 1 (..size array))
                               output (`` (.is (.List (~~ (.these (~~ (.type_of default)))))
@@ -311,7 +313,7 @@
         <default> <array>)]))
 
 (`` (template: .public (list <default> <array>)
-      [((.is (.All (_ a) (.-> (.Maybe a) (..Array a) (.List a)))
+      [((.is (.All (_ r w) (.-> (.Maybe r) (..Array' r w) (.List r)))
              (.function (list default array)
                (.case default
                  {.#Some default}
@@ -322,7 +324,7 @@
         <default> <array>)]))
 
 (template: .public (= <//#=> <left/*> <right/*>)
-  [((.is (.All (_ a) (.-> (.-> a a .Bit) (..Array a) (..Array a) .Bit))
+  [((.is (.All (_ r w0 w1) (.-> (.-> r r .Bit) (..Array' r w0) (..Array' r w1) .Bit))
          (.function (= //#= left/* right/*)
            (.let [size (..size left/*)]
              (.and ("lux i64 =" (..size right/*) size)
@@ -339,7 +341,7 @@
     <//#=> <left/*> <right/*>)])
 
 (template: .public (composite <left/*> <right/*>)
-  [((.is (.All (_ a) (.-> (..Array a) (..Array a) (..Array a)))
+  [((.is (.All (_ a) (.-> (..Array' a .Nothing) (..Array' a .Nothing) (..Array a)))
          (.function (composite left/* right/*)
            (.let [|left| (..size left/*)
                   |right| (..size right/*)]
@@ -349,8 +351,8 @@
     <left/*> <right/*>)])
 
 (template: .public (mix <$> <init> <it>)
-  [((.is (.All (_ a b)
-           (.-> (.-> Nat b a a) a (..Array b) a))
+  [((.is (.All (_ r w s)
+           (.-> (.-> Nat r s s) s (..Array' r w) s))
          (.function (mix $ init it)
            (.let [size (..size it)]
              (.loop (again [index 0
@@ -373,9 +375,9 @@
 
 (template [<name> <init> <op>]
   [(template: .public (<name> <?> <it>)
-     [((.is (.All (_ a)
-              (.-> (.-> a .Bit)
-                   (.-> (..Array a) .Bit)))
+     [((.is (.All (_ r w)
+              (.-> (.-> r .Bit)
+                   (.-> (..Array' r w) .Bit)))
             (.function (<name> ? it)
               (.let [size (..size it)]
                 (.loop (again [index 0])
@@ -392,8 +394,8 @@
   )
 
 (template: .public (one <?> <it>)
-  [((.is (.All (_ a b)
-           (.-> (.-> a (.Maybe b)) (..Array a) (.Maybe b)))
+  [((.is (.All (_ r r' w)
+           (.-> (.-> r (.Maybe r')) (..Array' r w) (.Maybe r')))
          (.function (one ? it)
            (.let [size (..size it)]
              (.loop (again [index 0])