allow linear usage by using all fields

[tjhance]

This would be nice to have, but it's probably complicated, and would likely require a more comprehensive proposal than is here.

It would be nice if I could "use" a linear datatype variable by using all of its fields without having to explicitly destruct it.

Here's a very simple example, with a single-constructor datatype:

linear datatype Foo = Foo(linear a: Bar, linear b: Bar)

method destroy_foo(linear foo: Foo)
{
  destroy_bar(foo.a);
  destroy_bar(foo.b);
}

Support this for a multiple-constructor datatype would be a far more advanced proposal. To see why it's hard, consider this example:

linear datatype Option<V> = Some(linear value: V) | None
method destroy_opt(linear opt: Option<Bar>)
{
  if opt.Some? {
    destroy_bar(opt.value);
  } else {
  }
}

The linear typechecker would need to infer that the None constructor is used implicitly in the else branch, and create a proof obligation that opt.None? is used in the else branch. However, I don't think this feature would be impossible.