ucsd-progsys
Have exact-data-cons propagate generated definitions
#2516 reports a problem that I think must be common.
Suppose we have a project with two files Lib.hs and Main.hs. Lib.hs requires --exact-data-cons, and so we enable the flag, or enable some other flag that implies --exact-data-cons too.
Verification of Lib.hs succeeds, but when Liquid Haskell tries to verify Main.hs, it fails when importing annotations from Lib.hs. The error message complains about unbound symbols like is$Lib.Val in Lib.hs, which had supposedly been successfully verified.
We can get verification of Main.hs to succeed by enabling --exact-data-cons again in Main.hs. However, there might be other data types in scope in Main.hs that do not tolerate the flag. And more important, we have to discover why there are missing symbols in a dependency.
Ideally, Liquid Haskell would arrange for the unbound symbols to be in scope in any module that imports Lib. This ticket is about exploring such approach.
Is there any reason why reflection is behind a flag? In principle it shouldn't be impactful performance wise as if you don't reflect any function you shouldn't get any new constraints
IIUC, you would like to fix this by enabling --reflection by default. Since --reflection enables --exact-data-cons, this would be equivalent to enabling --exact-data-cons in Main.hs. This is problematic for some data type definitions, apparently. There is some more discussion about it in #2292.
Do you have an actual example of those datatypes? I used datatypes with functions while having reflection in the SKILam.hs test
Actually, I don't. @ranjitjhala, I collected such a claim from #1284 and #2292. Do you think you could illustrate the limitations of --exactdc with an example?
Even if no such limitations existed, we would need to deal with the crashes of #2290 still.
I believe the isAdmit error was caused by the fact that the flag generates uninterpreted functions named isAdmit, while an interpreted function with that name had already been declared. This should already be resolved, as I removed the uninterpreted function when I disallowed refining the return types of constructors not written with prop.
Regarding the other errors I have no idea