Inlined records as variant's argument are seen as unnamed tuples

[n-osborne]

In the following example, Gospel type-checker only complains when the record syntax is used. We would have expected the other way around.

$ cat > foo.mli << EOF
> (*@ type m = A of { b : bool; i : integer } *)
> 
> type t
> (*@ mutable model m : m *)
> 
> val create : unit -> t
> (*@ t = create ()
>     ensures t.m = A (true, 42) *)
> 
> val f : t -> bool
> (*@ b = f t
>     ensures b = match t.m with | A (b,_) -> b *)
> 
> val g : t -> bool
> (*@ b = g t
>     ensures b = match t.m with | A x -> x.b  *)
> EOF
$ gospel check foo.mli
File "foo.mli", line 16, characters 33-36:
16 |     ensures b = match t.m with | A x -> x.b  *)
                                      ^^^
Error: The constructor A expects 2 argument(s)
       but is applied to 1 argument(s) here.

We also have an error when we deconstruct the record in the pattern:

$ cat > foo.mli << EOF
> (*@ type m = A of { b : bool; i : integer } *)
> 
> type t
> (*@ mutable model m : m *)
> 
> val g : t -> bool
> (*@ b = g t
>     ensures b = match t.m with | A x -> x.b  *)
> EOF
$ gospel check foo.mli
File "foo.mli", line 8, characters 37-38:
8 |     ensures b = match t.m with | A { b; i } -> b  *)
                                         ^
Error: Symbol b not found in scope
       (see "Symbols in scope" documentation page).

This is not the case when we use a named record type:

$ cat > foo.mli << EOF
> (*@ type r = { b : bool; i : integer } *)
> (*@ type m = A of r *)
> 
> type t
> (*@ mutable model m : m *)
> 
> val create : unit -> t
> (*@ t = create ()
>     ensures t.m = A { b = true; i = 42 } *)
> 
> val f : t -> bool
> (*@ b = f t
>     ensures b = match t.m with | A {b; i} -> b *)
> 
> val g : t -> bool
> (*@ b = g t
>     ensures b = match t.m with | A x -> x.b  *)
$ gospel check foo.mli

I believe we can either fix this or decide that we don't really want inlined records (even if it means adding them back later if we happen to miss them). The rational for removing them is that they are not a key feature of a specification language and we talk about simplifying Gospel type-checker berfore adding new logical features.

What do you think?

[n-osborne]

I believe that this may come from the fact that internal representations for plain record and inlined record are different while typing pattern on records doesn't differentiate.

Plain records are represented with Tast.rec_declaration which contains a lsymbol for a generated contructor and a list of lsymbol label_declarations for the field, while inlined record are represented by a list of (Ident.t * ty) label_declarations.

I have to confess I don't really understand the need for the generated constructor (constr#type_name) for the plain record. But if we remove it, we can harmonize the way records (plain and inlined) are represented and this should at least bring us closer to a fix to this issue.

One other thing that should be done when removing the generated constructor for plain records is to add a Prec to Tterm.pattern_node.