-
Notifications
You must be signed in to change notification settings - Fork 16
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Missing error message for unsupported types #340
Comments
I was trying to re-create this issue : reproducible repo. I got an error, wasn't using the gospel cli 🤦 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
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! |
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 I am afraid I might be conceptually wrong about this, please let me know |
There is no non-determinism in the |
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 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 This would lead to a clearer type error. Am I on the right track here. Btw thanks for the quick reply @shym 😄 |
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. |
Fixed by #406 |
On:
the typechecker fails with:
because
Typing.ty_of_core
uses anassert false
for all unsupported types.This should be fixed by adding a proper error message in
Warnings
.The text was updated successfully, but these errors were encountered: