Hipspec performs worse if there are missing type signatures

Open sergei-grechanik opened this issue 12 years ago • 1 comments

For example, hipspec cannot prove the prop from here unless the type signature for (++) is uncommented.

Judging by the *.mlw files, this is due to redundant apps. The bug seems to be introduced by the commit a63a8fe6264fcb27d4e6cec525d5e06d7677db8a

Dec 27 '13 18:12 sergei-grechanik

Thanks sergei-grechanik, I have had a similar problem before, yours differs by involving a polymorphic function. The culprit is simpFun in SimplifyRich, but I will have to tend to it later.

Dec 27 '13 19:12 danr