Adding documentation for subtyping (#1990)

* Add subsumption rule between Record/Dictionary

* Remove commented code

* Remove clone in pattern match, replaced fold by a for loop, take into account TailUnifVar and TailConstant

* Update & add comments

* Add integration tests

* add test with chaining std function on records

* add manual documentation for record/dictionary subtyping

* Modify manual

* Changing contract to typing

* Update core/tests/integration/inputs/typecheck/chaining_dictionary_function_record_dictionary_subtyping.ncl

Co-authored-by: Yann Hamdaoui <[email protected]>

* Update doc/manual/typing.md

Co-authored-by: Yann Hamdaoui <[email protected]>

* Fix test

* Add motivation

* Fix code example

* Add Array/Array and Dictionary/Dictionary subtyping documentation

* Fix code (does not fix TypecheckError)

* Fix code examples (does fix errors)

* Fix subsumption

* Fix subsumption

* Improve the manual section on subtyping

* Add generic example to work around function subsumption

* Update doc/manual/typing.md

* Update doc/manual/typing.md

* Fix format problem

* Update doc/manual/typing.md

---------

Co-authored-by: Yann Hamdaoui <[email protected]>
Co-authored-by: Yann Hamdaoui <[email protected]>

core/benches/nixpkgs/lists.ncl

@@ -525,9 +525,8 @@
             @ (toporest | { result : Array Dyn }).result
         } : { _ : Array Dyn },
 
-  #TODO: can it be statically typed?
   sort
-    | forall a. (a -> a -> Bool) -> Array a -> Array a
+    : forall a. (a -> a -> Bool) -> Array a -> Array a
     | doc m%"
       Sort a list based on a comparator function which compares two
      elements and returns true if the first argument is strictly below

core/src/typecheck/mod.rs

@@ -2383,6 +2383,7 @@ pub fn subsumption(
     checked: UnifType,
 ) -> Result<(), UnifError> {
     let inferred_inst = instantiate_foralls(state, &mut ctxt, inferred, ForallInst::UnifVar);
+    let checked = checked.into_root(state.table);
     match (inferred_inst, checked) {
         (
             UnifType::Concrete {

core/tests/integration/inputs/typecheck/chaining_dictionary_function_record_dictionary_subtyping.ncl

@@ -0,0 +1,8 @@
+# test.type = 'error'
+# [test.metadata]
+# error = 'EvalError::BlameError'
+let x = {foo = 1, bar = 2} in
+let y = std.record.insert "baz" 5 x in
+let _ = std.record.get "foo" y in
+let z = std.record.remove "foo" y in
+std.record.get "foo" z

doc/manual/typing.md

@@ -255,6 +255,90 @@ The following type constructors are available:
   }
   ```
 
+### Subtyping
+
+While distinct types are usually incompatible, some types might actually be
+safely converted to some other types. For example, `{foo = 5}` is inferred to
+have type `{foo : Number}` by default, but is also a valid value of type `{_ :
+Number}`. The latter type is less precise, but might be required for dynamic
+dictionary operations such as `std.record.insert`:
+
+```nickel
+let extended : { _ : Number } =
+  let initial : { foo : Number } = { foo = 5 } in
+  std.record.insert "bar" 5 initial in
+extended
+```
+
+In this example, there is a silent conversion from `{foo : Number}` to `{_ :
+Number}`. This is safe because `foo` is of type `Number`, and it's the only
+field, which means that a value of type `{foo : Number}` is effectively
+dictionary of numbers. In the typing jargon, `{foo : Number}` is said to be a
+*subtype* of `{_ : Number}`. We will write `T <: U` to say that `T` is a subtype
+of `U`: whenever a value of type `U` is expected, we can use a value of type `T`
+as well.
+
+Currently, Nickel supports the following subtyping rule which generalizes the
+example above:
+
+- **Record/Dictionary** subtyping :
+  `{ field1 : T1, ..., fieldn : Tn } <: { _ : T }` if for each `i`, `Ti <: T`
+  That is, a record type is a subtype of a dictionary type if the type of each
+  field is a subtype of the type of dictionary elements.
+
+  Example:
+
+  ```nickel
+  let occurrences : {a : Number, b : Number, c : Number} = {a = 1, b = 3, c = 0} in
+  std.record.map (fun char count => count + 1) occurrences : {_ : Number}
+  ```
+
+Subtyping extends to type constructors in the following way:
+
+- **Equality** : a type is trivially a subtype of itself, that is `T <: T`.
+- **Array**: `Array T <: Array U` if `T <: U`.
+
+  Example:
+
+  ```nickel
+  let block : _ =
+      let array_of_records : Array {a : Number} = [{a = 5}] in
+      let inject_b : Array {_ : Number} -> Array {_ : Number} =
+          std.array.map (fun a => std.record.insert "b" 5 a)
+      in
+
+      inject_b array_of_records
+  in block
+  ```
+
+  Here, `Array {a : Number}` is accepted where `Array {_ : Number}` is expected,
+  because `{a : Number} <: { _ : Number }`.
+- **Dictionary**: similarly, `{ _ : T } <: { _ : U }` if `T <: U`.
+
+  Example:
+
+  ```nickel
+  let block : _ =
+    let dict_of_records : { _ : {a : Number}} = {r = {a = 5}} in
+    let inject_b : { _ : {_ : Number}} -> { _ : {_ : Number}}
+      = std.record.map (fun _ x => std.record.insert "b" 5 x)
+    in
+
+    inject_b dict_of_records in
+  block
+  ```
+
+  Here, `{_ : {a : Number}}` is accepted where `{_ : {_ : Number}}` is expected,
+  because `{a : Number} <: { _ : Number }`.
+
+**Remark**: if you've used languages with subtyping before, you might expect the
+presence of a rule for function types, namely that `T -> U <: S -> V` if `S <:
+T` and `U <: V`. This is not the case in Nickel, for various technical reasons.
+However, you can work around this limitation by expanding a given function:
+If `f` has type `T -> U`, but a value of type `S -> V` is required,
+use `fun x => f x` instead, which has the same runtime behavior
+but isn't typed in the same way.
+
 ### Polymorphism
 
 #### Type polymorphism