Lone foralls should be allowed on both sides of subtyping. (allow `⋯ <: ∀ Y. ⋯`)

[paulstansifer]

This comes up when implementing a function application macro and trying to use it on a function with a generic type, so this is blocking making any good example languages.

But a simpler example is this: ∀T. *[a: Int b: T]* should be a subtype (or maybe a supertype? I can never get this straight) of *[a: Int b: ∀T. T]*. (In fact, in this case the types are equal, but they should at least compare in some direction.)

[paulstansifer]

Implementation... ugh, this seems tricky. We don't want to accidentally make *[b: Int]* a subtype of *[b: ∀T. T]* (or maybe I have that backwards). The point is that the underdetermined types on the RHS need to be "inside" the underdetermined types on the RHS (in fact, this should replace the current system where, when we ask whether ∀A B C . ??? <: ∀ X Y Z . ???, we just match up the variables in question).

This seems like perhaps another argument in favor of doing the normal thing that real languages do with generic types.

[paulstansifer]

Actually, I think that we have the exact same problem if we do the "normal" thing: we'd effectively be moving all of the ∀s up to the top, but we'd still need to figure out whether a particular specialization is valid or not.

• Seq<Int> <: ∀T. Seq<T> (but not vice versa!)
• ∀S. Seq<S> <: ∀T. Seq<T>
• ∀S. Seq<*[S S]*> <: ∀T. Seq<T> (but not vice versa!) ... T = *[S S]*. Is the rule that underdetermined names on the LHS must remain underdetermined, but names on the RHS can be assigned? Is it that simple? (but still maybe hard to implement)

[paulstansifer]

I wonder if the subtyping system is much too complicated. According to page 222 of https://www.cs.cmu.edu/~rwh/pfpl/2nded.pdf, the subtyping rule for foralls is really simple. Now, this particular problem (and the broader feature where Seq<Int> <: ∀T. Seq<T> without requiring some syntax for "hey, let's explicitly specify a type here") isn't covered, but maybe it's not too hard?

We could have

• Every time you hit a ∀, map the variable to some "underdetermined" special type (starts out as an empty set, no interior mutability required).
• Every time you compare an underdetermined variable to something, accumulate a new constraint in the underdetermined set. This can go in both directions, so I guess each set element has a "sign" indicating which direction subtyping should go.
• At the end of subtyping, we reconcile the underdetermined variables. If you have X <: T0, X <: T1, and X :> T2, there's probably some principled constraint-solving approach, but, for our purposes, I think it's easier to just try T0, T1, and T2 and see if one of them satisfies all the other constraints.