`strengthen` is not safe

nikita-volkov / refined

Refinement types with static checking

http://hackage.haskell.org/package/refined

MIT License

182 stars 31 forks source link

Closed raymond-h closed 3 years ago

raymond-h commented 3 years ago

strengthen allows you to fabricate refinements that are incorrect:

n = $$(refineTH @Positive 5)

n' :: Refined (Positive && Even) Integer
n' = strengthen n

n'' :: Refined Even Integer
n'' = andRight n'

print n''

Output:

n :: Refined Positive Integer
n' :: Refined (Positive && Even) Integer
n'' :: Refined Even Integer
Refined 5

Nothing is wrong with the Even predicate as it does correctly catch the error when not using strengthen.

This was tested with refined-0.6.1.

chessai commented 3 years ago

I could've sworn I fixed this already.

Fix incoming

chessai commented 3 years ago

corrected in efa5aaad04da2334f138d1ac70e342cc3a2d0975

chessai commented 3 years ago