Missing error message for unsupported types

[shym]

On:

val ret_obj : unit -> <bob:int>
(*@ o = ret_obj () *)

the typechecker fails with:

gospel: internal error, uncaught exception:
        File "src/typing.ml", line 108, characters 9-15: Assertion failed

because Typing.ty_of_core uses an assert false for all unsupported types. This should be fixed by adding a proper error message in Warnings.

[shubhamkumar13]

I was trying to re-create this issue : reproducible repo. ~And I was getting no errors with it, what am I doing wrong here :smiley_cat: ?~

I got an error, wasn't using the gospel cli :facepalm:

test_gospel on  main via 🐫 v4.13.1 (4.13.1+options) on ☁  (ap-southeast-2)
❯ gospel check bin/main.mli
gospel: internal error, uncaught exception:
        File "src/typing.ml", line 108, characters 9-15: Assertion failed

main.ml

class test_obj =
  object (_self)
    val mutable i = 1
    method bob = i
end

let ret_obj () = 
object
  val mutable i = 0
  method bob = i
end 

and respective .mli file

class test_obj :
    object
        val mutable i : int
        method bob : int
    end

val ret_obj : unit -> <bob:int>
(*@ o = ret_obj () *)

output

test_gospel on  main via 🐫 v4.13.1 (4.13.1+options) on ☁  (ap-southeast-2) took 3s
❯ dune build bin/main.exe

test_gospel on  main via 🐫 v4.13.1 (4.13.1+options) on ☁  (ap-southeast-2)
❯ dune exec bin/main.exe

Thanks!

[shubhamkumar13]

I might not be well versed in what the exact error should look like but I imagine this kind of error is an non-deterministic error, right?

The output can never depend on input, very similar to any function which has side effects we cannot determine what kind implementation is performed by the user and the int value returned can be anything similar to a read_line function

I am afraid I might be conceptually wrong about this, please let me know

[shym]

There is no non-determinism in the gospel tool. Maybe the command gospel check is misleading there: it performs type-checking. Actually checking the specifications is left for other tools. Said another way, encountering an object type (or any other unsupported type) will trigger the assert false reported in the error message.

[shubhamkumar13]

Thanks for the correction, I am not well versed with model checking but I am interested in it.

So according to your explanation the type checking matching leads to classify objects as an unsupported type which leads to pattern matching the error with _ -> assert false

The solution to this off the top of my head would be address the object type as a valid type in the typechecker and then add another error type constructor in warnings.ml -> type kind.

This would lead to a clearer type error. Am I on the right track here.

Btw thanks for the quick reply @shym :smile:

[shym]

The solution to this off the top of my head would be address the object type as a valid type in the typechecker and then add another error type constructor in warnings.ml -> type kind.

It depends on what you mean by “valid type”: we don’t want to bring support for objects in Gospel (that would be quite some work!), but just end up with a new error indeed.

[n-osborne]

Fixed by #406