Yeah, that seems right. I'd also believe you if you told me that the second arrow also needs to be linear, since I can't really give a good reason why it should

Yeah, that seems right. I'd also believe you if you told me that the second arrow also needs to be linear, since I can't really give a good reason why it should be one way or the other off the top of my head. I admittedly don't really have a great intuition for how to work with this machinery, since I haven't had a chance/excuse to actually play around with it, to be honest; I'm just going off of a SPJ talk on this stuff I watched many months ago, which I mostly understood at the time, and the paper associated with the GHC implementation, which I understood substantially less of.