
18 Sep
2023
18 Sep
'23
11:02 a.m.
On Mon, Sep 18, 2023 at 09:23:19AM -0400, Ryan Scott wrote:
Short answer: This is expected behavior, and it's unlikely that behavior will change any time soon.
Long answer: The key phrase in your original post is "the quantifier moved". [...] The reason why this restriction exists is because there is no type-level counterpart to `\ (@z)` in Core, which would be required for regeneralization at the kind level.
Aha, thank you, Ryan, for the helpful explanation. In that case I will continue to write data types specialised for each use case. That's not too painful in my particular application. Whenever I get stuck on this stuff I marvel at how wonderfully everything works out at the value level! Tom