Open paulstansifer opened 3 years ago
Okay, the problem with forall T. T<Int>
is that it doesn't have kind annotations (and we don't have a kind-checker yet (#3)). So I think we can get away with just modifying forall
. So it's syntax time!
forall co X contra Y in Z . ...
forall +X -Y =Z . ...
forall_co X . forall_contra Y . forall_inv Z . ...
...and, should the annotations be allowed to be omitted (meaning covariance)?
Currently
Cell<Int>
is a subtype offorall T . Cell<T>
. That's okay. But alsoCell<Sequence<Int>>
is a subtype ofCell<forall T . Sequence<T>>
. That's bad, because you can't actually put a generic sequence into aCell
that wants a sequence ofInt
s!I think that a solution looks like this:
ExtraInfo
for type comparison tostd::cmd::Ordering
(bonus: an easier way to reverse subtyping than swapping the mainAst
and the context), and ... use it somehow. Do we need to look it up in every subtyping judgment? (a lot of them areLiteralLike
, fortunately)forall T. T<Int>
? Maybe we want three different versions offorall
and three different versions of<...>
? Ugh!So, this might be (part of the) reason why "normal" MLs don't have an explicit
forall
type (and, I guess, insist thatA
be defined if you writeA<B>
): that way you can infer co/contra/in-variance and not have to make a big deal about it. So maybe we should do the normal thing.