Three Dollar Quill

I didn't think as hard about this as I might have liked, due to circumstances, but I believe that the semantics of my System Fω variant will break the generative/applicative distinction in 1ML. Fortunately, it's a simple fix in terms of changes to core code; the tricky bit is going to be rewriting the test helpers.

(The fix is "You know all of that fancy subtyping stuff? Don't do that.")

Before I touch anything, let's make sure I've got a handle on how all of this is supposed to work. Because now that I'm looking at this again, I think I might have thought about this wrong. What I need to do is, ignoring the semantics of my System Fω variant, figure out what 1ML "wants" to have happen with existential types.

I'm getting tired so I'm going to try to wrap things up, but my impression is that I should expect fundamentally incompatible return values from a pure function from a type to itself, and two invocations of an impure function from a type to itself. If this is right, then I just need to take some time to confirm that it works as expected/desired, and that it requires certain guarantees that my code doesn't currently provide. Anyway, tired, losing track of time.

Good night.