Motoko compiler feature?

Hi,

So I’ve been playing with this piece of code: Motoko Playground - DFINITY

So based on this 2 struct types:

public type Parent = {
 name: Text;
 description: Text;
 extraValue : ?Text;
};
public type Child = {
 extraValue : ?Text;
};

So I’m not sure if this is a bug or a feature, but should this be allowed?
validate = func (e: Parent: Child ) this works and the compiler doesn’t complain about it.

Parent struct has to contain same identical values like Child in order for this to compile eg: extraValue but the optional ? doesn’t seem to be make a difference tho.

This was found by accident and tbh it would be a great way to enforce struct inheritance if it was meant that way?

2 Likes

Maybe I’m misunderstanding but that looks like a serious bug to me.

The compiler correctly rejects this similar example:

[nix-shell:~/motoko/test/run]$ more bug.mo

type Child = { foo: Nat };
type Parent = { foo: Nat; bar: Bool};

func f ( x : Parent : Child) : Bool { x.bar };

let ohoh = f( { foo = 1 } );

[nix-shell:~/motoko/test/run]$ moc bug.mo
bug.mo:5.10-5.20: type error [M0117], pattern of type
  Parent = {bar : Bool; foo : Nat}
cannot consume expected type
  {foo : Nat}

It should reject it, otherwise ohoh would attempt access a missing field.

1 Like

Your playground example should also be rejected (but isn’t) so I think there is a bug and will investigate.

Thanks very much for reporting this!

1 Like

Hi @claudio, yes, in a normal scenario I’m getting a compiler rejection.

But in that particular case it’s working and it shouldn’t.

No worries and please do share your finds.

Actually, I think this may not be a bug per se but a subtle consequence of the type checker having more information to hand in one situation than another. @rossberg will take a look once he has the time, but I don’t think there’s a type unsoundness here (just weird typing behaviour).

Actually, this is working as intended. But the explanation is a bit complicated.

First, note that the argument of a function is defined by a pattern, and patterns work backwards from expressions: an expression constructs a value inside-out, whereas a pattern deconstructs a value outside-in. One consequence is that the subtyping requirements for type annotations in patterns work in the opposite direction from expressions, i.e., the annotation has to be a subtype of the pattern it annotates (which makes it a supertype of the scrutinee).

Another way to understand this is that patterns are contra-variant, as they can only occur in negative position. This can perhaps be best seen via an example. Consider:

type A = {a : Nat};
type B = {a : Nat; b : Nat};
type C = {a : Nat; b : Nat; c : Nat};

Now, a function can be written with an outer type annotation:

(func (x) { x }) : (B -> B)

I can duplicate the type information inside the function:

(func (x : B) { x : B }) : (B -> B)

Due to subtyping, the outer annotation can also refine the type, in the usual co/contra-variant manner:

(func (x : B) { x : B }) : (C -> A)

Now, we can also pull in the extra annotation into the function:

(func ((x : B) : C) { (x : B) : A }) : (C -> A)

and this all type-checks consistently. Note how the subtyping order in the pattern is opposite that in the expression.

The other direction, where the inner type is smaller than the outer, is rejected:

// ill-typed
(func (x : C : B) { x : B : A }) : (B -> A)

Allowing this direction, with the expected meaning, would be unsound, as @claudio’s example shows.

Now, given that, the next question then is: what is the type of x in such a case? It turns out that the typing rules propagates the outer subtype (i.e., C), not the inner supertype (B). This has to do with coverage checking. If we allowed to “forget” the more precise type of the scrutinee on the way into the pattern, then we would allow weird things, especially in a switch:

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

This would break coverage checking, at least as it works now, since it depends on precise type information.

Hence, if there are two types feeding into a pattern, the typing rules pick the smaller one to propagate inwards.

Now, this has the weird effect that the following actually becomes okay:

(func (((x : C) : B) : C) { (x : B) : A }) : (C -> A)

The reason is that the we start with the outer C, then see B but keep propagating the smaller C inwards, and so, the inner C is not in conflict. That is essentially the situation from the playground example (where there are three type annotations, though the outermost one is on the outer function’s return type in that case).

In fact, that behaviour allows even odder examples:

type D = {c : Nat};
(func (((x : D) : B) : C) { (x : B) : A }) : (C -> A)

That type-checks fine as well, because both B and D are supertypes of C, although they are unrelated.

I wouldn’t defend this behaviour on semantic grounds. It merely was simpler. The alternative would be to propagate the supertype, and thereby have typing allow an example like case ((-1 : Int) : Nat), but have coverage checking do its own type propagation, figuring out that -1 is a redundant pattern. Conceptually, that would be nicer, and I’d be open to changing it, but it would be a substantial complication to coverage checking (both in terms of specification and implementation).

4 Likes

Nice explanation, but it still makes me nervous.

I couldn’t let this rest and went ahead and actually implemented this change. So the surprising examples should be illegal in the next Motoko release (while some others become legal).

2 Likes

Hi @rossberg and @claudio

Thanks for looking into this and thanks for the amazing explanation. I do understand it might not be a critical bug but at first sight it might be weird and confusing, I mean look at javascript after all this years and we still get WAT (skip to 1:24) Wat

while some others become legal could you expand a bit on this?

Thanks

while some others become legal could you expand a bit on this?

The description of Tighten typing rules for type annotations in patterns by rossberg · Pull Request #2860 · dfinity/motoko · GitHub
gives an example and there may be more in the tests.

I see now,

switch (n : Nat) { case (-1 : Int : Nat) {...} }; So basically the effect of this is none except the compiler won’t complain now.

It will warn you that the pattern is never matched, but it won’t reject the code ( in this example).

Before:

> let n = 0;
> switch (n : Nat) { case (-1 : Int : Nat) {}};                 
stdin:1.26-1.28: type error [M0050], literal of type
  Int
does not have expected type
  Nat

After:

> let n = 0;
let n : Nat = 0
> switch (n : Nat) { case (-1 : Int : Nat) {}};                 
stdin:2.26-2.28: warning [M0146], this pattern is never matched
stdin:2.1-2.45: warning [M0145], this switch of type
  Nat
does not cover value
  0 or 1 or _
> stdin:2.20-2.44: execution error, switch value 0 does not match any case

It now rejects out cases like

func (x : Nat : Int : Nat) {...}

where a type shrinks again. Your playground example was a variation of that, except that in your case, the outermost type annotation was propagated from the enclosing function’s return type. Simplifying a bit, yours was like:

func f() : {g : Nat -> ()} {
  {g = func(x : Nat : Int) {}}
};

which had a similar effect before, because the knowledge from f’s return type is propagated all the way into the inner function. It now is rejected as well.