search

ucsd-progsys / liquid-fixpoint

Horn Clause Constraint Solving for Liquid Types
BSD 3-Clause "New" or "Revised" License
132 stars 59 forks source link

[cutsolver] Multiple Sorts #70

Closed BenjaminCosman closed 9 years ago

BenjaminCosman commented 9 years ago

See:

https://github.com/ucsd-progsys/liquid-fixpoint/blob/cutsolver/tests/todo/multiple-sorts.fq

The Ocaml solver accepts it while the Haskell solver rejects it. (It's an excerpt from the fq file that LH generates from https://github.com/ucsd-progsys/liquidhaskell/blob/master/tests/pos/tyvar.hs)

BenjaminCosman commented 9 years ago

Addressed by af4e59fc2354be7d690f389060aabae024bb55f6

ranjitjhala commented 9 years ago

Wow! Do the previously failing tests now pass?

On Jun 5, 2015, at 11:20 PM, bmcfluff notifications@github.com wrote:

Addressed by af4e59f

— Reply to this email directly or view it on GitHub.

BenjaminCosman commented 9 years ago

Yes On Sat, Jun 6, 2015 at 8:37 AM Ranjit Jhala notifications@github.com wrote:

Wow! Do the previously failing tests now pass?

On Jun 5, 2015, at 11:20 PM, bmcfluff notifications@github.com wrote:

Addressed by af4e59f

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHub https://github.com/ucsd-progsys/liquid-fixpoint/issues/70#issuecomment-109604587 .