To reduce the problem to a simpler (but useful) one: what would it take to be able to write a generic "compose" function (on function values) that would be polymorphic across at least Fn/FnMut/FnOnce? This is something that people already write the specific versions of; obviously the general version requires some form of HKT, but it's not clear (at least to me) what's blocking that.

When I've seen discussions of HKT in Rust it feels like there's an awkward circularity where if you talk about HKT people say the use cases aren't there, but if you talk about things that need HKT people say they can't be implemented because they need HKT. And I'm worried that the conversation about extending the type system has reached a place where adding ad-hoc special cases is seen as the "cautious" approach, when the result is a funny subset of a more general system that's both more complex and less powerful than biting the bullet and implementing the general system.

I am not an expert in this area, but the problem is that these things all have very different kinds of permissions, in a sense... I'm not sure what being polymorphic over ownership looks like.

I don't think that anyone who understands this stuff deeply denies that there's good use cases for HKT. There's just not a design, and we're not sure that one actually exists. And a general perception that GATs will give us most of the big benefits of HKT in a way that feels more Rust-like. That being said, there have been a few attempts at this. We'll see.

Being polymorphic over ownership is the most important problem Rust should be looking to solve, IMO: it would make a lot of other problems trivial. I don't necessarily think it's easy, but I do think it's tractable.

The choice to focus on GATs is exactly what I was thinking of. I think Rust will come to regret it, as it comes with most of the costs of full HKT but leads one into working with a limited subset that's not so theoretically well-founded, and I'm not convinced the forward-compatibility is as good as claimed (the semantics may extend to full HKT, but it pushes syntax in a direction that seems likely to make for a frustrating syntax for full HKT). I hope it ends up working out.

How are GATs any less theoretically well founded than HKT?

I can see how maybe working toward that would be a priority in a PLT research sense, but Rust isn't that kind of language anymore. (This is my own opinion and I'm not on the lang team, mind you.)

> How are GATs any less theoretically well founded than HKT?

I'm not aware of their having been studied to the same extent, so I don't have the same level of confidence that they are well-behaved. For example, is there a known algorithm for doing perfect type inference in the presence of GAT? What about when we add in subtyping, or higher-rank types? Maybe it's all going to be fine, but the further you stray from the path that's been trodden by PLT research, the more I'd worry about falling down a hole.

Gotcha. My understanding was that they were, but not my area of expertise.