Unbound constructor error in Ortac-generated file

[Lucccyo]

Ortac generated a file that did not include the constructor of the type A I created in the gospel (it should do the same for type B).

(*@ type v = A of string | B of string *)

While running QCheckSTM tests on Ortac file, it fails with the following:

5 |     | Some v_1 -> (match v_1 with | A _ -> true | B _ -> false)
                                        ^^^
Error: Unbound constructor A

[n-osborne]

Thanks for raising this issue!

Indeed, we don't translate (yet) the ghost types. Translations should be relatively simple (mostly converting a Gospel.Tast.type_declaration into a Ppxlib.type_declaration)

There is though the question of where to store them between the moment we read the Gospel AST and the moment we generate the OCaml code. Maybe Ir is better than Config?

[n-osborne]

The scope of this issue is in fact a bit larger than I first thought.

Indeed, all the plugins could benefit from the support for Gospel ghost types translation.

This means that some modifications should be done in ortac-core:

There are mainly two modifications to bring to ortac-core

• Provide a translation from Gospel.Tast.type_declaration to Ppxlib.type_declaration
• Store constructors and destructors of the Gospel types in the Context.t (in a similar way that ghost functions are stored)

I'm not sure whether we have to handle name capture as Gospel type-checker may complain at an earlier stage.

Regarding the second item, we have to deal with

• variants that take a tuple as argument
• variants that take an inlined record as argument (though they seem buggy in Gospel)
• records' fields (destructors)
• records' functional constructor that is generated by Gospel and injected in the typed AST

Once these modifications are done, we should bring the change to ortac-qcheck-stm and to ortac-wrapper (otrac-monolith is based on ortac-wrapper so this will be free). This should be straightforward.

Testing-wise, the error sadly appears only when we try to compile the generated code.

A good way to make sure it is working is then to add a new example.

[n-osborne]

Closed by #228