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

Type-checker fails with an assert false on extensible type #405

Open n-osborne opened 6 months ago

n-osborne commented 6 months ago
$ cat > foo.mli << EOF
> type t = ..
> EOF
$ gospel check foo.mli
gospel: internal error, uncaught exception:
        File "src/typing.ml", line 710, characters 22-28: Assertion failed

It is easy enough to handle the failling case (I already have a draft fix). There is the question though of whether we support specifications for this kind of types?