Type abstraction issue with mattern matching

[crusso]

[nix-shell:~/motoko/rts]$ rlwrap moc
Motoko compiler (revision 0.4.6-36-g920c0c711)
> switch 0 { case (x:Nat) x};
0 : Nat
> switch 0 { case (x:Int) x};
0 : Nat
> switch {x = 1} { case (x:{}) x};
{x = 1} : {x : Nat}
> 

This looks really wrong to me. I'd expect the types to be Nat, Int, {}. Or have I totally lost the plot?

[crusso]

I believe the bug is here: typing.ml

  | AnnotP (pat1, typ) ->
    let t' = check_typ env typ in
    if not (T.sub t t') then
      error env pat.at
        "pattern of type\n  %s\ncannot consume expected type\n  %s"
        (T.string_of_typ_expand t')
        (T.string_of_typ_expand t);
    check_pat env t pat1 <---- BUG t should be t'

But perhaps I'm totally mis-appreciating the subtleties of subtyping.

[rossberg]

That is expected behaviour. Type annotations in patterns do not constrain, merely check. I remember dabbling with that for a while. The coverage check would not work otherwise, because it depends on the precise type for each sub pattern.

[crusso]

Ok, if you say so, but it seems very odd.

[crusso]

Guess I'll abandon my fix.

[rossberg]

I agree it's somewhat counter-intuitive. If you can come up with a consistent definition of coverage under different typing rules then I'm all ears. Try changing the above line and see what tests break.

[rossberg]

Because the outermost type annotation in lets is treated specially and rewritten to the RHS.

I know, it's hacky. Maybe there is a more coherent solution that I wasn't able to find.

[crusso]

But then why do we have:

[nix-shell:~/motoko/src]$ rlwrap moc Motoko compiler (revision 0.4.6-39-ga82698642)

> let x : Int = 0;
let x : Int = 0
> x;
0 : Int
> let r : {} = { f = 1};
let r : {} = {f = 1}
> r;
{f = 1} : {}
> 

I would expect x and r to have RHS types Nat and { f : Nat }. Is there something else going on? Maybe the use of type declaration for recursion is losing the info here?

[rossberg]

Interesting, my reply arrived 10 minutes before the post it is replying to. :-o A glitch in the matrix?

[crusso]

Not the matrix, probably more to do with me using a VM and Windows and cut'n'paste not working when I want it to.

[crusso]

I'll downgrade from bug to curiousity, in case we want to revisit.

[crusso]

See PR #2154 for ramifications of "fixing" this.

[rossberg]

Well, I saw your post as mail immediately, so the problem cannot have been on your end.

Some of the details are coming back to me. One problem is that allowing type annotations in patterns to "forget" information would naturally imply the validity of things like

switch (x : Nat) {
  case (-1 : Int) {}
}

which is rather dubious. And moreover, it would be odd if this was allowed but it did not type-check without the annotation. This would also cause issues with the coverage checker, which currently relies on the notion of "span" for certain types. The similar

switch (x : {#a}) {
  case (#b : {#a; #b})
}

would likely fail to warn about both the #b being unreachable and the pattern not being exhaustive. Other cases might even crash the checker, e.g., if the number of enumerated constructors exceeds the expected span.

I'm sure there are ways around this, but AFAICS, they would all involve propagating the precise type information in addition to the other one, a duplication that seems dubious.

[crusso]

Ok, that makes sense. Let's just park it for now but keep the issue in case we want to revisit.