It seems desirable to be able to talk about required fundeps for a given polymorphic constraint (when constraint kinds are implemented).
This would make it possible to do higher-order programming at the type-level, consider the example:
class Map
(f :: (a :: Nat) -> (b :: Nat) -> Constraint | a -> b) -- <- here
(xs :: List Nat)
(out :: List Nat)
| f xs -> out
If some sort of coverage condition were to be implemented for functional dependencies, this extension would make it possible for more instances to be accepted.
An important question raised by @LiamGoodacre is how to deal with requiring a -> b, but being given a -> b c, etc. I think these should be possible to work out in general by computing the transitive closure of the given dependencies and checking the required one is a member of that set -- but it needs more thought.
It seems desirable to be able to talk about required fundeps for a given polymorphic constraint (when constraint kinds are implemented).
This would make it possible to do higher-order programming at the type-level, consider the example:
If some sort of coverage condition were to be implemented for functional dependencies, this extension would make it possible for more instances to be accepted.
An important question raised by @LiamGoodacre is how to deal with requiring
a -> b, but being givena -> b c, etc. I think these should be possible to work out in general by computing the transitive closure of the given dependencies and checking the required one is a member of that set -- but it needs more thought.