Rerefined: Refinement types, again (refined rewrite)

Show and Tell
#1

refined is broken for GHC 9.8 (+ 9.10) due to pending dependency bound bumps, and I have some gripes with it (aeson dependency, Typeable constraints, no support for functor predicates, arbitrary overlapping terminology with my strongweak library). rerefined resolves these in less code with fewer dependencies.

Thanks to some design improvements we can get away with some neat tricks, like replacing the Weaken type class with a single type family for widening relational operations (see WidenRelOp and the other Predicate.Relational modules).

I had wanted to write this for a while, and once I saw the Typeable and GHC 9.8 issues I figured it was worthwhile. For anyone using refined, you should be able to switch if you like, but it’s lots of definition name changes and I haven’t finished checking coercion safety (you may be able to shoot yourself in the foot in new, fresh ways). I’d be keen to write a compatibility shim and/or a switching guide if there’s any interest at all.

/r/haskell post: https://www.reddit.com/r/haskell/comments/1cgwikh

7 Likes
#2

If it’s just bounds bumping that’s the problem then users of refined should file an issue with the Hackage Trustees.

EDIT: Well, it’s clearly not just bounds bumping, because rerefined has many other benefits, but I mean for those who do want to still use refined for whatever reason, that’s what they can do.

1 Like
#3

Thanks, I didn’t know about that Hackage trustees repo. To clarify, I don’t suggest refined users swap. I noted the likely experience you’d have if you wanted to swap, for whatever reason (e.g. if you are writing libraries using refined and want the same improvements I do).

1 Like