Refined has the wrong role signature

nikita-volkov / refined

Refinement types with static checking

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

MIT License

183 stars 31 forks source link

Closed treeowl closed 6 years ago

treeowl commented 6 years ago

Currently, it says

type role Refined phantom representational

This means that I can use coerce to prove Q x given any P x whatsoever! I think you probably should write

type role Refined nominal nominal

Why should the second parameter be nominal? Consider the interaction between GreaterThan and Data.Ord.Down.

chessai commented 6 years ago

This makes sense. Yeah, I didn't consider interactions with Down at all. Thanks for pointing this out.