experiment: approximate stable as shared types in view queries

[crusso]

Builds on #5796

#5796 requires the result of a generated view query to be shared, omitting viewers for stable vars that contain non-shared mutable data.

This PR relaxes that restriction by requiring them to just be stable and, if non-shared, coercing them to the nearest shared supertype by (recursively) erasing mutable fields and promoting mutable arrays to Any.
The type approximation is done by Type.shared_of_stable which returns a shared supertype of a given stable type.
The value of stable type can always be directly cast to the shared type via a no-cost upcast (subsumption).

This means a stable variable will always be displayed in some form, degrading to just Any in the worst case, but typically more informative than that.

NB. It would be nice if we could approximate a mutable object field by a field of type Any, but that's not allowed by subtyping at the moment. Instead, we just drop the field.

For example, with a simple .viewer for mutable arrays,
the following (mixed) stable var signature:

.most

// Version: 1.0.0
type List<T> = ?(T, List<T>);
actor {
  stable array : [var (Nat, Text)];
  stable array_of_non_shared : [var {var a : {#A}; b : {#B}; c : [var {#C}]}];
  stable motoko_xxx : {#motoko_xxx};
  stable non_shared_array : [[var Nat]];
  stable override : {#override};
  stable some_list : ?(Nat, List<Nat>);
  stable some_mutable_record : {var a : Nat; b : Nat; c : [var Nat]};
  stable some_non_shared_list :
    ?({var a : Nat; b : Text}, List<{var a : Nat; b : Text}>);
  stable some_record : {a : Nat; b : Text; c : Bool};
  stable var some_variant : {#node : ({#leaf}, Nat, {#leaf})}
};

produces:

type List__1 = 
 opt record {
       nat;
       List__1;
     };
type List = 
 opt record {
       record {b: text;};
       List;
     };
service : {
  __array: (start: nat, count: nat) -> (vec record {
                                              nat;
                                              text;
                                            }) query;
  __array_of_non_shared: (start: nat, count: nat) ->
   (vec record {
          b: variant {B;};
          c: reserved;
        }) query;
  __non_shared_array: () -> (vec reserved) query;
  __override: () -> (text) query;
  __some_list: () -> (opt record {
                            nat;
                            List__1;
                          }) query;
  __some_mutable_record: () -> (record {
                                  b: nat;
                                  c: reserved;
                                }) query;
  __some_non_shared_list: () -> (opt record {
                                       record {b: text;};
                                       List;
                                     }) query;
  __some_record: () -> (record {
                          a: nat;
                          b: text;
                          c: bool;
                        }) query;
  __some_variant: () ->
   (variant {node: record {
                     variant {leaf;};
                     nat;
                     variant {leaf;};
                   };}) query;
  go: () -> ();
}

[github-actions]

Comparing from 3d4bf0f to 678e537:
The produced WebAssembly code seems to be completely unchanged.
In terms of gas, no changes are observed in 5 tests.
In terms of size, no changes are observed in 5 tests.

[christoph-dfinity]

I'm a bit worried about this, as it might give the indication that data is missing. For example, since we don't have a view function for core/PriorityQueue at the moment, and its definition is:

  public type PriorityQueue<T> = {
    heap : List<T>
  }
  // with
  public type List<T> = {
    var blocks : [var [var ?T]];
    var blockIndex : Nat;
    var elementIndex : Nat
  };

You'd get record { heap : record { } } by the approximation, which looks a lot like no data.

I'm surprise by the __array_of_non_shared example in your description:

  __array_of_non_shared: (start: nat, count: nat) ->
   (vec record {
          b: variant {B;};
          c: reserved;
        }) query;

shouldn't that be vec reserved according to "... and promoting mutable arrays to Any"?

[crusso]

I'm a bit worried about this, as it might give the indication that data is missing. For example, since we don't have a view function for core/PriorityQueue at the moment, and its definition is:

  public type PriorityQueue<T> = {
    heap : List<T>
  }
  // with
  public type List<T> = {
    var blocks : [var [var ?T]];
    var blockIndex : Nat;
    var elementIndex : Nat
  };

You'd get record { heap : record { } } by the approximation, which looks a lot like no data.

Yeah, that's probably true. I was hoping to have approximation:

record { heap :  { record { blocks : Any; blockIndex : Any; elementIndex : Any }}

With the Any indication approximation.

However, Motoko subtyping doesn't allow { var f : T } <: { f : Any }, which would be required for that (if it's even sound).
Our current representation probably allows that, since a mutable field is just an immutable field holding a ref cell, but still requires a change to subtyping.

I guess another alternative might be to make the approximation apparent in the type of the generated query:

__non_shared_array: () -> (variant { approximately : vec reserved }) query;

(so we wrap an approximately on the outside of query result, for clarity).

I'm surprise by the __array_of_non_shared example in your description:

  __array_of_non_shared: (start: nat, count: nat) ->
   (vec record {
          b: variant {B;};
          c: reserved;
        }) query;

shouldn't that be vec reserved according to "... and promoting mutable arrays to Any"?

The code actually defines a view for mutable arrays.

  stable array_of_non_shared : [var {var a : {#A}; b : {#B}; c : [var {#C}]}];

The view returns an immutable sub-array of the mutable array, so it is just approximating the contents of the mutable array (dropping mutable a, keeping b and approximating c)