ocaml-gospel / gospel

A tool-agnostic formal specification language for OCaml.
https://ocaml-gospel.github.io/gospel
MIT License
128 stars 16 forks source link

Uncaught exception on mutually recursive ghost types #388

Closed n-osborne closed 1 month ago

n-osborne commented 8 months ago
$ cat > foo.mli << EOF
> (*@ type foo = A | B
>     and bar = C | D *)
> EOF
$ OCAMLRUNPARAM=b gospel check foo.mli
gospel: internal error, uncaught exception:
        File "src/uattr2spec.ml", line 136, characters 9-15: Assertion failed
        Raised at Gospel__Uattr2spec.ghost_spec in file "src/uattr2spec.ml", line 136, char
acters 9-21
        Called from Gospel__Uattr2spec.signature.(fun) in file "src/uattr2spec.ml", line 21
1, characters 16-55
        Called from Stdlib__List.map in file "list.ml", line 92, characters 20-23
        Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
        Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
        Called from Dune__exe__Check.run_file in file "bin/check.ml", line 42, characters 1
5-58
        Called from Dune__exe__Check.run.(fun) in file "bin/check.ml", line 66, characters 
33-53
        Called from Dune__exe__Cli.run_check in file "bin/cli.ml", line 59, characters 10-4
7
        Called from Cmdliner_term.app.(fun) in file "cmdliner_term.ml", line 24, characters
 19-24
        Called from Cmdliner_eval.run_parser in file "cmdliner_eval.ml", line 34, character
s 37-44

We need to decide whether Gospel should support mutually recursive types and either implement support or catch the exception with a proper error.