ucsd-progsys / liquidhaskell

Liquid Types For Haskell

BSD 3-Clause "New" or "Revised" License

1.2k stars 139 forks source link

Fix crashes and obscure errors in tests when enabling --exact-data-cons #2292

Open facundominguez opened 5 months ago

facundominguez commented 5 months ago

2290 tried enabling `--exact-data-cons` by default, but this causes many tests to fail with crashes and error messages that are hard to relate to the flag. While the feature could still be disabled in the tests, we don't want users to be confronted with the problem of discovering how to get rid of such errors.

This issue is about improving those error messages.

Earlier discussion on enabling --exactdc by default can be found in https://github.com/ucsd-progsys/liquidhaskell/issues/1284.

ranjitjhala commented 5 months ago

I agree - “exact” should be the default. The trouble is that some things cannot be translated to SMT eg if you have function types in the data definition.. while others can… eg plain Lists …

facundominguez commented 1 month ago

eg if you have function types in the data definition..

IIRC, functions are replaced with integers to describe higher order functions to the SMT solver. Could we hope to do the same with data constructors?