Is it possible to compute a more precise type?

[PaulKlint]

Consider the following program (non-sensical since it will trow an exception for the missing key 3):

value main(list[value] args) {
    matched = ();
    return matched[3] == 10;
}

This program is accepted by the type checker but the type assigned to matched[3] is void.
I handle this case in the compiler by falling back to the general equal primitive rather than using the more efficient int_equal_int.

Question: it seems that the type checker could infer that matched has type map[int,int] based on its use. Would that be hard to add or does it require a complete pass of backward propagating type information?

[mahills]

I'm checking this, I'm actually surprised that it type checks without giving an error.

[mahills]

I suspect I may have something in there to handle this as a special case, since normally having something like matched[3] with domain type void would be an error. It does type check.

To the bigger question, I think inferring that the type is map[int,int] would be a bad idea. The only situation where this would be necessary is when the type is actually map[void,void], which occurs when we have an explicit assignment of () into the map, and when nothing else has been assigned into it (or it would have a concrete or inferred type). This would be adding another special case for void maps, and I'm not convinced that the type is even correct, since indexing into a void map for a comparison operation seems like it should be disallowed. Again, I'm surprised this isn't being treated by the checker as an actual violation.

[jurgenvinju]

Just to avoid any confusion: more precise than void it doesn't get... it's the most precise type we have.

I agree with Mark, the question is why it type checks at all since int is not a sub-type of void

[PaulKlint]

I agree that probably the most surprising observation is that this code passes the type checker,
Once this has been clarified I will remove the special case code in the compiler to handle this.

[mahills]

I'm currently not using subtype to check this but am instead using comparable, which just means that one is a subtype of the other (here, void is a subtype of int so it passes). I'm assuming there is some good reason why I'm doing so, but I don't remember what that was :(

I guess I can tighten the checks up and see what fails...