Implement ADT contracts (#1821)

* Update contract optimization for ADT

Before the introduction of ADT, enum types couldn't contain other type
components. Now they can, as in e.g. `[| 'Foo (String -> Number) |]`.
The optimizer is updated to recurse into those types as well.

* Proper contract for extended enum types (ADTs)

ADTs have been introduced (experimentally) in previous commits. In
practice, this means that the enum types have become more expressive,
where value can now be variant with an associated argument.

The contract derived from an enum type hasn't been updated yet, and
wasn't correctly handling more elaborate enums. This commit implements
the proper behavior for full enum types.

This commit doesn't change the previous status quo around polymorphic
enum types, in that it doesn't enforce parametricity at run-time. While
this is questionable, we are somehow stuck with this choice for now,
because suddenly enforcing parametricity would break
backward-compatibility, including the types of some functions from the
stdlib.

* Converts type annotations to contract annotations

Since optimization has been introduced, eliding some contract
application for type annotations, it's safer to use contract annotation
in test whenever we really want to check the behavior of contracts at
run-time.

While this change shouldn't make any difference right now, it's probably
more future-proof, if further optimizations one day elide those
contracts.

* Add tests for enum/adt contracts

* Format internals.ncl

* Apply suggestions from code review

Co-authored-by: Viktor Kleen <[email protected]>

* Remove trailing backtick in comment

---------

Co-authored-by: Viktor Kleen <[email protected]>

cli/tests/snapshot/inputs/errors/enum_contract_shape_mismatch.ncl

@@ -0,0 +1,3 @@
+# capture = 'stderr'
+# command = ['eval']
+(std.function.id | forall r. [| 'Foo Number, 'Bar String, 'Qux; r |] -> [| 'Foo Number, 'Bar String, 'Qux; r |]) 'Foo

cli/tests/snapshot/inputs/errors/enum_contract_shape_mismatch_rev.ncl

@@ -0,0 +1,3 @@
+# capture = 'stderr'
+# command = ['eval']
+(std.function.id | forall r. [| 'Foo, 'Bar String, 'Qux Dyn; r |] -> [| 'Foo, 'Bar String, 'Qux Dyn; r |]) ('Foo..(5))

cli/tests/snapshot/snapshots/snapshot__eval_stderr_enum_contract_shape_mismatch.ncl.snap

@@ -0,0 +1,29 @@
+---
+source: cli/tests/snapshot/main.rs
+expression: err
+---
+error: contract broken by the caller
+       shape mismatch for 'Foo
+  ┌─ [INPUTS_PATH]/errors/enum_contract_shape_mismatch.ncl:3:30
+  │
+3 │ (std.function.id | forall r. [| 'Foo Number, 'Bar String, 'Qux; r |] -> [| 'Foo Number, 'Bar String, 'Qux; r |]) 'Foo
+  │                              ---------------------------------------                                             ---- evaluated to this expression
+  │                              │                                                                                    
+  │                              expected type of the argument provided by the caller
+  │
+  = Found an enum with tag `'Foo` which is indeed part of the expected enum type
+  = However, their shape differs: one is an enum variant that carries an argument while the other is a bare enum tag
+
+note: 
+  ┌─ [INPUTS_PATH]/errors/enum_contract_shape_mismatch.ncl:3:1
+  │
+3 │ (std.function.id | forall r. [| 'Foo Number, 'Bar String, 'Qux; r |] -> [| 'Foo Number, 'Bar String, 'Qux; r |]) 'Foo
+  │ --------------------------------------------------------------------------------------------------------------------- (1) calling <func>
+
+note: 
+  ┌─ [INPUTS_PATH]/errors/enum_contract_shape_mismatch.ncl:3:2
+  │
+3 │ (std.function.id | forall r. [| 'Foo Number, 'Bar String, 'Qux; r |] -> [| 'Foo Number, 'Bar String, 'Qux; r |]) 'Foo
+  │  --------------- (2) calling <func>
+
+

cli/tests/snapshot/snapshots/snapshot__eval_stderr_enum_contract_shape_mismatch_rev.ncl.snap

@@ -0,0 +1,29 @@
+---
+source: cli/tests/snapshot/main.rs
+expression: err
+---
+error: contract broken by the caller
+       shape mismatch for 'Foo
+  ┌─ [INPUTS_PATH]/errors/enum_contract_shape_mismatch_rev.ncl:3:30
+  │
+3 │ (std.function.id | forall r. [| 'Foo, 'Bar String, 'Qux Dyn; r |] -> [| 'Foo, 'Bar String, 'Qux Dyn; r |]) ('Foo..(5))
+  │                              ------------------------------------                                          ----------- evaluated to this expression
+  │                              │                                                                              
+  │                              expected type of the argument provided by the caller
+  │
+  = Found an enum with tag `'Foo` which is indeed part of the expected enum type
+  = However, their shape differs: one is an enum variant that carries an argument while the other is a bare enum tag
+
+note: 
+  ┌─ [INPUTS_PATH]/errors/enum_contract_shape_mismatch_rev.ncl:3:1
+  │
+3 │ (std.function.id | forall r. [| 'Foo, 'Bar String, 'Qux Dyn; r |] -> [| 'Foo, 'Bar String, 'Qux Dyn; r |]) ('Foo..(5))
+  │ ---------------------------------------------------------------------------------------------------------------------- (1) calling <func>
+
+note: 
+  ┌─ [INPUTS_PATH]/errors/enum_contract_shape_mismatch_rev.ncl:3:2
+  │
+3 │ (std.function.id | forall r. [| 'Foo, 'Bar String, 'Qux Dyn; r |] -> [| 'Foo, 'Bar String, 'Qux Dyn; r |]) ('Foo..(5))
+  │  --------------- (2) calling <func>
+
+

core/src/eval/operation.rs

@@ -2300,7 +2300,7 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
                 let Term::Array(array, _) = t1 else {
                     return Err(mk_type_error!(
                         "label_with_notes",
-                        "Array String",
+                        "Array",
                         1,
                         t1.into(),
                         pos1

core/src/stdlib.rs

@@ -64,29 +64,41 @@ pub mod internals {
         mk_term::var("$dyn")
     }
 
+    // `enum` is a reserved keyword in rust
+    pub fn enumeration() -> RichTerm {
+        mk_term::var("$enum")
+    }
+
     generate_accessor!(num);
     generate_accessor!(bool);
     generate_accessor!(string);
+    generate_accessor!(fail);
+
     generate_accessor!(array);
     generate_accessor!(array_dyn);
+
     generate_accessor!(func);
     generate_accessor!(func_dom);
     generate_accessor!(func_codom);
     generate_accessor!(func_dyn);
+
     generate_accessor!(forall_var);
     generate_accessor!(forall);
-    generate_accessor!(fail);
-    generate_accessor!(enums);
+
     generate_accessor!(enum_fail);
+    generate_accessor!(enum_variant);
+    generate_accessor!(forall_enum_tail);
+
     generate_accessor!(record);
-    generate_accessor!(dict_type);
-    generate_accessor!(dict_contract);
-    generate_accessor!(dict_dyn);
     generate_accessor!(record_extend);
-    generate_accessor!(forall_tail);
+    generate_accessor!(forall_record_tail);
     generate_accessor!(dyn_tail);
     generate_accessor!(empty_tail);
-    generate_accessor!(enum_variant);
+
+    generate_accessor!(dict_type);
+    generate_accessor!(dict_contract);
+    generate_accessor!(dict_dyn);
+
     generate_accessor!(stdlib_contract_equal);
 
     generate_accessor!(rec_default);