search

nikita-volkov / refined

Refinement types with static checking
http://hackage.haskell.org/package/refined
MIT License
183 stars 31 forks source link

move `Typeable` constraint on predicate kind to class #98

Closed raehik closed 2 weeks ago

raehik commented 1 year ago

An earlier change #83 enabled using non-Type-kinded predicates. To support this, Predicate (p :: k) x instances were changed to explicitly include a Typeable k constraint. Every instance that wishes to support non-Type-kinded predicates (e.g. further predicate operators like And, Not) must add this constraint.

This PR moves the Typeable k constraint to the class definition. (Note that Typeable p was already present.) We remove lots of newly spurious Typeable constraints. We also fix an oversight in the instances for binary predicate operators, where the kind of predicates l and r were arbitrarily required to be the same kind k. Thanks to this change, we can remove the explicit kind quantifying and let GHC correctly infer l :: k1, r :: k2.

Due to GHC's rules on inferring type variable order, validate becomes awkward to use with TypeApplications. validate' provides original behaviour. Potential discussion there.

This might break certain custom predicate operator instances, but I'm not sure.

raehik commented 1 year ago

A potential discussion on design:

validate' :: forall {k} ... is really the preferred external function signature. It would be nicer to switch the names of validate and validate'. However, it would break certain custom Predicate instances. In the first place validate is a fairly internal function, so I figured there wasn't a good enough reason to switch.

chessai commented 1 year ago

The type ordering is unfortunate. This looks good to me. Having both validate and validate' makes me sad, but like you said, it's mostly internal. The docs should definitely mention this issue though.

raehik commented 1 year ago

I clarified the validate' situation so there should be no confusion.

raehik commented 1 year ago

@chessai any further thoughts on this PR? I'm using it in 2 projects without issue (though it is more of a library concern than user-facing)

raehik commented 7 months ago

This is fairly ready to merge, but I'm loathe to push it forwards as I'd prefer to remove Typeable constraints from combinator predicates altogether. I've already done this in rerefined. See #101 for an overview of the changes required.