search

informalsystems / quint

An executable specification language with delightful tooling based on the temporal logic of actions (TLA)
Apache License 2.0
782 stars 31 forks source link

Improve type checking error for sum-type constructors and eliminators #1231

Open shonfeder opened 10 months ago

shonfeder commented 10 months ago

Currently, the constraint system etc. doesn't let us produce very friendly or informative error messages: it's all in terms of unification failures of rows. We need a way to guide or decorate the constraint checker with error messages on constraint failures.

romac commented 10 months ago

Maybe check out this paper which was published at OOPSLA '23:

Getting into the Flow: Towards Better Type Error Messages for Constraint-Based Type Inference https://dl.acm.org/doi/10.1145/3622812 (PDF)

I don't know if the technique described there is directly applicable to the Quint type checker but perhaps it'll yield some inspiration towards a solution.

shonfeder commented 10 months ago

Thanks for the pointer, @romac !