(:-) a closed category?

[Zemyla]

It seems to be. There is an exponential, which is (:=>), and apply and uncurry combinators:

apply :: forall a b. (a :=> b, a) :- b
apply = Sub $ (Dict :: Dict b) \\ (ins :: a :- b)

uncurry :: forall a b c. (a :- (b :=> c)) -> ((a, b) :- c)
uncurry s = unmapDict $ \Dict -> (Dict :: Dict c) \\ ((ins :: b :- c) \\ s)

But there should also be a curry combinator:

curry :: forall a b c. ((a, b) :- c) -> (a :- (b :=> c))
curry = ???

And it seems like that can't be implemented without unsafe operations.

[Zemyla]

I just realized that :=> isn't the canonical exponential type, because it induces a functional dependency. There could be a type family, something like ==>, which is a constraint but doesn't have the same dependency.

[Icelandjack]

These things can be implemented with Simon's -XQuantifiedConstraints branch

[Icelandjack]

Is found here https://github.com/ghc/ghc/tree/wip/T2893, I made tickets for curry and uncurry