search

ucsd-progsys / liquid-fixpoint

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

Remove GHC-specific bits from liquid-fixpoint #668

Open facundominguez opened 9 months ago

facundominguez commented 9 months ago

At the moment the extensionality feature hardcodes the datatype definition of pairs.

Pairs are produced by liquidhaskell, but their definition is not made explicit in the fixpoint queries.

This GHC-specific definition should be removed from liquid-fixpoint (this part is easy).

Then liquidhaskell should define a type of pairs that liquid-fixpoint can handle. This will require some investigation to see if LH has a datatype representation of tuples and if so why it isn't appearing in fixpoint queries.