Fix and improve contract generation optimization for static types (#2017

)

* Fix and improve static contract optimizations

This commit fixes a number of issues with the optimization of contract
generation from a static type annotation. It's been introduced to take
advantage of the guarantees of static typing to simplify the generated
contract and elide a number of useless checks at run-time.

However, this optimization was too agressive as implemented: it just
turned any non-function type in a positive position to `Dyn`. Indeed,
contracts in negative position must be kept around, because they check
what's come from the (potentially untyped) external world: the fact that
a function is statically typed doesn't ensure it'll be called with the
right arguments.

The first issue is that a negative contract can hide inside something
else than an arrow type. Typically, take `let functions: Array (Number
-> Number) in (std.array.at 0 functions) "a"`. The application is
untyped, and wrongly pass a string to a function of the array. However,
the current optimization code will turn this contract to just `Dyn` at
runtime and get rid of entirely, because there's an `Array _` in
positive position. This is only valid if `_` doesn't contain any arrow
type, which it does, in this example.

Another issue stems from the sealing/unsealing symmetry of polymorphic
row contracts. Take `let id : forall r. {foo : Number; r} -> {foo :
Number; r} = fun x => x in id {foo = 1, bar = 2}`. The current version
would return `{foo = 1}`, with the `bar` field missing. The issue is
that the second `{foo : Number; r}` is a record type in positive
position, which currently gets entirely elided, giving `forall r. {foo :
Number; r} -> Dyn` as an optimized contract. The argument contract seals
anything else than `foo` in the record's tail, but there's no dual
contract to unseal it anymore, such that it just becomes invisible.

This commit implements a more complicated strategy, but which is
hopefully correct. Instead of getting rid of type constructor in
positive positions, we try to simplify their content as well, and only
if the content is simplified down to `Dyn` (or `{; Dyn}` for record
rows, etc.), we get rid of the entire constructor. Otherwise, we try to
pay only for necessary checks. For example, `{foo : Number, bar : Number
-> Number}` now gets simplified to `{bar : Number -> Dyn; Dyn}` instead
of just `Dyn` before (which was incorrect).

The full simplification rules around polymorphic row contracts are a bit
intricate and are properly detailed in the documentation of the
corresponding methods.

* Add tests (wip)

* Add tests for type simplification, fix unveiled bug

* Apply suggestions from code review

Co-authored-by: jneem <[email protected]>

* Move back code comments to the right position

---------

Co-authored-by: jneem <[email protected]>

core/src/identifier.rs

@@ -33,6 +33,14 @@ impl Ident {
     pub fn into_label(self) -> String {
         self.label().to_owned()
     }
+
+    /// Create a new fresh identifier. This identifier is unique and is guaranteed not to collide
+    /// with any identifier defined before. Generated identifiers start with a special prefix that
+    /// can't be used by normal, user-defined identifiers.
+    pub fn fresh() -> Self {
+        increment!("Ident::fresh");
+        Self::new(format!("{}{}", GEN_PREFIX, GeneratedCounter::next()))
+    }
 }
 
 impl fmt::Display for Ident {
@@ -122,12 +130,9 @@ impl LocIdent {
         LocIdent { pos, ..self }
     }
 
-    /// Create a new fresh identifier. This identifier is unique and is guaranteed not to collide
-    /// with any identifier defined before. Generated identifiers start with a special prefix that
-    /// can't be used by normal, user-defined identifiers.
+    /// Create a fresh identifier with no position. See [Ident::fresh].
     pub fn fresh() -> Self {
-        increment!("LocIdent::fresh");
-        Self::new(format!("{}{}", GEN_PREFIX, GeneratedCounter::next()))
+        Ident::fresh().into()
     }
 
     /// Return the identifier without its position.

core/src/stdlib.rs

@@ -92,6 +92,7 @@ pub mod internals {
     generate_accessor!(record_contract);
     generate_accessor!(record_type);
     generate_accessor!(forall_record_tail);
+    generate_accessor!(forall_record_tail_excluded_only);
     generate_accessor!(dyn_tail);
     generate_accessor!(empty_tail);