Typechecking bug in higher order Gospel functions

[mrjazzybread]

As I was updating the Gospel standard library, I came across a strange bug in the Gospel typechecker

If I create a function like

(*@ function f (f : int -> 'a) : 'a *)

Then write an axiom

(*@ axiom fail : forall x. f (fun _ -> x) = x *)

It fails with the following cryptic error

gospel: internal error, uncaught exception:
        Gospel.Ttypes.TypeMismatch(_, _)

However, the following axiom is typechecked correctly

(*@ axiom fail : forall x : 'a. f (fun _ -> x) = x *)

[n-osborne]

Thanks for reporting this.

What would be the expected behaviour in your opinion? Should the axiom be accepted or should the type-checker should fail with a proper error message?

Apparently, the uncaught exception is raised in Ttypes.ty_match.

Failing with a proper error message can simply be achieved by using the Warning mechanism.
If we want that example to be accepted by the type-checker, we are lacking a bit of type inference I guess.

Note that the following example is produced using the last released version of Gospel. Line numbers are expected to be different with main.

$ cat > foo.mli <<EOF
> (*@ function f (g : int -> 'a) : 'a *)
> (*@ axiom fail : forall x. f (fun _ -> x) = x *)
> EOF
$ OCAMLRUNPARAM=b gospel check foo.mli
gospel: internal error, uncaught exception:
        Gospel.Ttypes.TypeMismatch(_, _)
        Raised at Gospel__Ttypes.ty_match in file "src/ttypes.ml", line 171, characters 15-58
        Called from Gospel__Tterm_helper.t_app in file "src/tterm_helper.ml", line 148, characters 10-34
        Called from Gospel__Dterm.term in file "src/dterm.ml", line 340, characters 10-54
        Called from Gospel__Dterm.term_node in file "src/dterm.ml", line 365, characters 17-37
        Called from Gospel__Dterm.term in file "src/dterm.ml", line 340, characters 10-54
        Called from Gospel__Dterm.term_node in file "src/dterm.ml", line 396, characters 14-30
        Called from Gospel__Dterm.term in file "src/dterm.ml", line 340, characters 10-54
        Called from Gospel__Dterm.fmla in file "src/dterm.ml" (inlined), line 431, characters 18-34
        Called from Gospel__Typing.fmla in file "src/typing.ml", line 544, characters 11-22
        Called from Gospel__Typing.process_axiom in file "src/typing.ml", line 1094, characters 10-58
        Called from Gospel__Typing.process_sig_item.process_sig_item in file "src/typing.ml", line 1359, characters 32-64
        Called from Gospel__Typing.process_sig_item.process_and_import in file "src/typing.ml", line 1367, characters 8-31
        Called from Gospel__Typing.process_sig_item in file "src/typing.ml", line 1376, characters 23-51
        Called from Gospel__Typing.type_sig_item in file "src/typing.ml" (inlined), line 1381, characters 15-49
        Called from Dune__exe__Check.type_check in file "bin/check.ml", line 29, characters 26-53
        Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34
        Called from Dune__exe__Check.run_file in file "bin/check.ml", line 52, characters 8-45
        Called from Dune__exe__Check.run.(fun) in file "bin/check.ml", line 71, characters 33-53
        Called from Dune__exe__Cli.run_check in file "bin/cli.ml", line 53, characters 10-47
        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 35, characters 37-44

[mrjazzybread]

Both should be accepted I think, I don't think there is a good reason for this behavior. I tried to pinpoint the error and I think it's because the type that is inferred for (f (fun _ -> x)) is not the same as x, but I am not sure why. I think the problem is in the gen_app function but it is very hard to debug because I don't really get what it does :|