Type-checker oversees fact about top-level type of case statement

[jurgenvinju]

Describe the bug

data Symbol = \int();
data Statement = \if();

data S = label(Statement x, int y);
data T = label(Symbol x, str y);

value f(S s) {
    switch (s) {
        case label(_, x) : return x;
    }

    return "";
}

The case label resolves to both the T and the S. In complex cases this leads to spurious static errors (happened in Clair), while there is no error. Because s is a S the case label constructor should resolve only to the label constructor of the S sort.

[jurgenvinju]

when I put label(Symbol _, _) the type-checker also misses errors, since that constructor it could never be.