Bad error message when applying a function to too many arguments

[n-osborne]

Running the Gospel type-checker on a file foo.mli containing:

(*@ open Sequence *)

(*@ function f (s : 'a sequence) : integer = length empty empty *)

will display the following error message:

$ deq gospel check foo.mli 
File "foo.mli", line 3, characters 45-51:
3 | (*@ function f (s : 'a sequence) : integer = length empty empty *)
                                                 ^^^^^^
Error: This term has type integer but a term was expected of type
       'a657 sequence -> 'a658.

In contrast, running ocamlc on the corresponding foo.ml file containing:

let f x = List.length x x

will display the more informative messages:

λ ocamlc foo.ml 
File "foo.ml", line 1, characters 10-25:
1 | let f x = List.length x x
              ^^^^^^^^^^^^^^^
Error: The function List.length has type 'a list -> int
       It is applied to too many arguments
File "foo.ml", line 1, characters 24-25:
1 | let f x = List.length x x
                            ^
  This extra argument is not expected.