Infer sharing and validity constraints for data constructors

[robertkleffner]

Currently, the programmer has to specify the sharing and validity constraints manually in constructor types for the compiler to get them right. For instance, instead of writing

rec data List a
    = Cons (List a) a --> (List a)
    | Nil --> (List a)

the programmer has to write

rec data List x
    = Cons {(List {a vd sd}) (vd & vl) (sd | sl)} {a v s} --> {(List {a (vd & v) (sl | s)}) (vd & v & vl & vr) (sd | sl | s | sr)}
    | Nil --> {(List {a v s}) (v & vr) (s | sr)}

Writing out the latter is tedious and easy to get wrong. But it's very pattern based and seems like it should be easy to automatically generate.

The concerns with automating this are:

1. Will it be polymorphic enough?
2. Will it be too polymorphic?
3. Can the programmer plug in some custom sharing attributes without breaking it?

[robertkleffner]

This was resolved, but the goal was reached via a different implementation method. Devs using Boba can still specify particular sharing constraints, and sharing constraints are fully specified by the type signature, not inferred. However, the written specification is now simpler.