Investigate constraining behaviour

[nsbgn]

Consider this:

    TypeSchema(lambda x, y, z: F(x, x) ** z[F(x, A)]).apply(F(A, A))

... does not yield F(A, A)

    TypeSchema(lambda x, y, z: F(x, x) ** z[F(x, x)]).apply(F(A, A))

does yield F(A, A).

The logic for unifying with constraints doesn't make full sense. Why would it be okay to unify with base types, but not with variables?

Also, we should make sure that the following works:

    TypeSchema(lambda x, y, z: F(x, y) ** z[F(x, A), F(y, A)]).apply(F(A, A))

[nsbgn]

A better way might be to explicitly indicate whether a subtype is acceptable, perhaps by having x[A, B] mean something different from x[+A, B] (where the + indicates that a subtype is accepted. Or perhaps automatically unfold concrete types in constraints to all their subtypes. I need to think through the ramifications.

[nsbgn]

Unfolding the concrete types seems the most workable. I would just need to register the subtypes of every base type operator and add a .subtypes() method on TypeInstances.

[nsbgn]

While the above is a good idea, it becomes complicated when coupled with intersection and union types (#79), since A.subtypes() should include A & B, and A & B & C, and... Though this might not be a problem since we can disregard them.

[nsbgn]

Plan of attack:

• Don't have special notation for subtypes and supertypes, nor unfold types into its super-/subtypes. Instead, assume that every type also stands for its subtypes, just as we do now. I think this is almost always what you want, so there's no point in increasing the number of checks we do.
• We now unify with the skeleton of the last remaining type in the constraint. Instead, we should unify with the entire type, excepting base types that have any subtypes and that are not already bound on the left hand side. In the latter case, we still consider the constraint satisfied and just put a new constraint on that one variable.
• In case there are multiple types in the constraint, but they all have the same type operator, we can already unify with that operator, in case that narrows down other constraints.

Start with tests.

[nsbgn]

We use x[A] to mean that 'once x is bound, we must check that it is subtype of A', and we use x[y,z] to mean that 'once we are sure that x can only possibly unify with one of the constraint options (y or z), we can perform that unification'. This mixes up ideas: If one of the options is bound before the final option unification is triggered, it has turned into a subtype guard and won't unify to a concrete type anymore. If it is bound after, then it has already unified so we immediately get a concrete type. Also, it is unclear what A[x] would mean: must we check that x is a supertype of A once it is bound, or can we immediately bind x>A?

All this does not amount to sane behaviour.

This is why we should only accept the second idea, and when we want to be able to express a subtype guard, we must be explicit about it. How is still up for debate.

(x[~Qlt]) >> x
(x[+Qlt]) >> x
(x < Qlt) >> x
(x[Sub(Qlt)]) >> x
(x[Qlt.sub()]) >> x

x <= Qlt is the most intuitive, but it would need reinterpretation of the < operator, and I don't know if we ever need to combine the two (e.g. x[A, Subtype(B)]).

[nsbgn]

Combining makes sense to do like so: (y < B) & x[A, y] or x[A, _ < B]