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

The typechecker fails with an exception on functor applications #338

Closed shym closed 4 months ago

shym commented 1 year ago

On:

val tricky : Set.Make(Int).t -> bool

the typechecker fails with:

gospel: internal error, uncaught exception:
        Invalid_argument("Ppxlib.Longident.flatten")
        Raised at Stdlib.invalid_arg in file "stdlib.ml", line 30, characters 20-45
        Called from Ppxlib__Longident.flatten_exn in file "src/longident.ml" (inlined), line 34, characters 22-33
        Called from Gospel__Typing.ty_of_core in file "src/typing.ml", line 101, characters 39-70
        Called from Gospel__Typing.val_parse_core_type in file "src/typing.ml", line 766, characters 8-25
        Called from Gospel__Typing.process_val in file "src/typing.ml", line 964, characters 18-49
        Called from Gospel__Typing.process_sig_item.process_sig_item in file "src/typing.ml", line 1329, characters 31-67
        Called from Gospel__Typing.process_sig_item in file "src/typing.ml", line 1361, characters 23-51
        Called from Gospel__Typing.type_sig_item in file "src/typing.ml", line 1366, characters 15-49
shym commented 1 year ago

Proposal of fix: