Allow combining inductives + records?

[mtzguido]

Would it make sense to allow type declarations such as this?

type t =
    | A of { x : int; y : bool }
    | B of { z : nat }

Then one can do:

let t = A ({ x = 2; y = true })

let _ = match t with
        | A ({ x = x }) -> assert (x == 2)
        | _ -> assert False

and have code that is robust in the face of adding fields to either case. One can work around it by using a proxy for the records, like this:

type p1 = { x : int; y : bool }
type p2 = { z : nat }
type t =
    | A of p1
    | B of p2

With this definition, the code above typechecks just fine, so it doesn't seem like a lot of work is needed.

My particular desire for this comes from the term_view and sigelt_view types in Meta-F*. Adding a field to one of the data constructors requires changing a bunch of places to ignore it.

[typesAreSpaces]

I have a similar question, but simpler. I don't understand why the following code doesn't work: val f : {fst : int; snd: int} -> Tot int

It seems that a proxy is needed, the following works: type int_pair = {fst : int; snd : int} val f : int_pair -> Tot int

[typesAreSpaces]

After reading the discussion in #1184 , now I understand the internals of record types and what do they desugar to. Your question is interesting because it hints that 'adding more sugar' might solve the problem, perhaps using an internal table to keep track 'of all the sugar added' might be needed to avoid repetitions. I'm new using FStar, I really like it!