revise existing tests to match #311 (subtype checking only for refere… #323

crusso · 2022-03-18T14:29:08Z

…nce types)

I think these tests are need to change in light of #311 (as verified by Motoko testing)

…nce types)

nomeata · 2022-03-18T14:47:40Z

I guess we should implement the new rules in Haskell and Rust to compare notes on these updated tests. (And we means me and Yan respectively)

crusso · 2022-03-18T17:11:04Z

The fact that no-one is confident about how this is meant to behave strikes me as slightly worrying ;->

nomeata · 2022-03-18T17:13:26Z

Just because it changes every few months doesn’t mean we are not confident? ;-)

crusso · 2022-04-09T20:14:35Z

@nomeata thanks for adjusting the tests to use a method name - most of my tests now pass but there's another bug I'll need to figure out on the motoko side (see below).

More pretty printing crap, I'm afraid. Should be possible to sort out (by me).

Output form a private branch (don't try this at home)

[nix-shell:~/clean/motoko]$ candid-tests -p "subtypes" -i ../../candid/test
Parsing construct.test.did ...
Parsing overshoot.test.did ...
Parsing prim.test.did ...
Parsing reference.test.did ...
Parsing subtypes.test.did ...
subtypes:35 null <: null ... ok (pass)
subtypes:37 bool <: bool ... ok (pass)
subtypes:39 nat <: nat ... ok (pass)
subtypes:41 int <: int ... ok (pass)
subtypes:45 nat <: int ... ok (pass)
subtypes:47 int </: nat ... ok (pass)
subtypes:49 nat </: nat8 ... ok (pass)
subtypes:51 nat8 </: nat ... ok (pass)
subtypes:55 nat <: opt bool ... ok (pass)
subtypes:57 opt bool <: opt bool ... ok (pass)
subtypes:59 bool <: opt bool ... ok (pass)
subtypes:61 µ opt <: opt opt nat ... ok (pass)
subtypes:65 record {} <: record {} ... ok (pass)
subtypes:67 record {} <: record { a : opt empty } ... ok (pass)
subtypes:69 record {} <: record { a : opt null } ... ok (pass)
subtypes:71 record {} <: record { a : reserved } ... ok (pass)
subtypes:73 record {} </: record { a : empty } ... ok (pass)
subtypes:75 record {} </: record { a : nat } ... ok (pass)
subtypes:77 record {} </: record { a : null } ... ok (pass)
subtypes:81 func () -> () <: func () -> () ... ok (pass)
subtypes:83 func () -> () <: func () -> (opt empty) ... ok (pass)
subtypes:85 func () -> () <: func () -> (opt null) ... ok (pass)
subtypes:87 func () -> () <: func () -> (reserved) ... ok (pass)
subtypes:89 func () -> () </: func () -> (empty) ... ok (pass)
subtypes:91 func () -> () </: func () -> (nat) ... ok (pass)
subtypes:93 func () -> () </: func () -> (null) ... ok (pass)
subtypes:97 func (opt empty) -> () <: func () -> () ... ok (pass)
subtypes:99 func (opt null) -> () <: func () -> () ... ok (pass)
subtypes:101 func (reserved) -> () <: func () -> () ... ok (pass)
subtypes:103 func (empty) -> () </: func () -> () ... ok (pass)
subtypes:105 func (nat) -> () </: func () -> () ... ok (pass)
subtypes:107 func (null) -> () </: func () -> () ... ok (pass)
subtypes:111 variant {} <: variant {} ... ok (pass)
subtypes:113 variant {} <: variant {0 : nat} ... ok (pass)
subtypes:115 variant {0 : nat} <: variant {0 : nat} ... ok (pass)
subtypes:117 variant {0 : bool} </: variant {0 : nat} ... ok (pass)
subtypes:119 variant {0 : bool} </: variant {1 : bool} ... ok (pass)
subtypes:124 (µ record) <: (µ record) ... not ok (cannot compile)
tmp.mo:5.216-5.231: type error [M0029], unbound type EmptyRecord__38

import Prim "mo:⛔";type EmptyRecord = {_0_ : EmptyRecord};
type EmptyVariant = {#_0_ : EmptyVariant};
type Vec = [Vec];

assert ((prim "deserialize" : Blob -> (?(shared () -> async EmptyRecord))) "\44\49\44\4C\02\6A\00\01\01\00\6C\01\00\01\01\00\01\01\00\01\6D" == (((?(actor "\61\61\61\61\61\2D\61\61" : actor { m : shared () -> async EmptyRecord__38 }).m)) : (?(shared () -> async EmptyRecord))))
subtypes:126 (µ record) </: empty ... ok (pass)
subtypes:128 empty <: (µ record) ... not ok (cannot compile)
tmp.mo:5.204-5.219: type error [M0029], unbound type EmptyRecord__41

import Prim "mo:⛔";type EmptyRecord = {_0_ : EmptyRecord};
type EmptyVariant = {#_0_ : EmptyVariant};
type Vec = [Vec];

assert ((prim "deserialize" : Blob -> (?(shared () -> async EmptyRecord))) "\44\49\44\4C\01\6A\00\01\6F\00\01\00\01\01\00\01\6D" == (((?(actor "\61\61\61\61\61\2D\61\61" : actor { m : shared () -> async EmptyRecord__41 }).m)) : (?(shared () -> async EmptyRecord))))
subtypes:130 (µ record) <: record {µ record} ... not ok (cannot compile)
tmp.mo:5.231-5.246: type error [M0029], unbound type EmptyRecord__43

import Prim "mo:⛔";type EmptyRecord = {_0_ : EmptyRecord};
type EmptyVariant = {#_0_ : EmptyVariant};
type Vec = [Vec];

assert ((prim "deserialize" : Blob -> (?(shared () -> async {_0_ : EmptyRecord}))) "\44\49\44\4C\02\6A\00\01\01\00\6C\01\00\01\01\00\01\01\00\01\6D" == (((?(actor "\61\61\61\61\61\2D\61\61" : actor { m : shared () -> async {_0_ : EmptyRecord__43} }).m)) : (?(shared () -> async {_0_ : EmptyRecord}))))
subtypes:132 record {µ record} <: (µ record) ... not ok (cannot compile)
tmp.mo:5.228-5.243: type error [M0029], unbound type EmptyRecord__45

import Prim "mo:⛔";type EmptyRecord = {_0_ : EmptyRecord};
type EmptyVariant = {#_0_ : EmptyVariant};
type Vec = [Vec];

assert ((prim "deserialize" : Blob -> (?(shared () -> async EmptyRecord))) "\44\49\44\4C\03\6A\00\01\01\00\6C\01\00\02\6C\01\00\02\01\00\01\01\00\01\6D" == (((?(actor "\61\61\61\61\61\2D\61\61" : actor { m : shared () -> async EmptyRecord__45 }).m)) : (?(shared () -> async EmptyRecord))))
subtypes:135 (µ variant) <: (µ variant) ... not ok (cannot compile)
tmp.mo:5.217-5.233: type error [M0029], unbound type EmptyVariant__43

import Prim "mo:⛔";type EmptyRecord = {_0_ : EmptyRecord};
type EmptyVariant = {#_0_ : EmptyVariant};
type Vec = [Vec];

assert ((prim "deserialize" : Blob -> (?(shared () -> async EmptyVariant))) "\44\49\44\4C\02\6A\00\01\01\00\6B\01\00\01\01\00\01\01\00\01\6D" == (((?(actor "\61\61\61\61\61\2D\61\61" : actor { m : shared () -> async EmptyVariant__43 }).m)) : (?(shared () -> async EmptyVariant))))
subtypes:137 (µ variant) </: empty ... ok (pass)
subtypes:139 empty <: (µ variant) ... not ok (cannot compile)
tmp.mo:5.205-5.221: type error [M0029], unbound type EmptyVariant__46

import Prim "mo:⛔";type EmptyRecord = {_0_ : EmptyRecord};
type EmptyVariant = {#_0_ : EmptyVariant};
type Vec = [Vec];

assert ((prim "deserialize" : Blob -> (?(shared () -> async EmptyVariant))) "\44\49\44\4C\01\6A\00\01\6F\00\01\00\01\01\00\01\6D" == (((?(actor "\61\61\61\61\61\2D\61\61" : actor { m : shared () -> async EmptyVariant__46 }).m)) : (?(shared () -> async EmptyVariant))))
subtypes:141 (µ variant) <: variant {µ variant} ... not ok (cannot compile)
tmp.mo:5.234-5.250: type error [M0029], unbound type EmptyVariant__48

import Prim "mo:⛔";type EmptyRecord = {_0_ : EmptyRecord};
type EmptyVariant = {#_0_ : EmptyVariant};
type Vec = [Vec];

assert ((prim "deserialize" : Blob -> (?(shared () -> async {#_0_ : EmptyVariant}))) "\44\49\44\4C\02\6A\00\01\01\00\6B\01\00\01\01\00\01\01\00\01\6D" == (((?(actor "\61\61\61\61\61\2D\61\61" : actor { m : shared () -> async {#_0_ : EmptyVariant__48} }).m)) : (?(shared () -> async {#_0_ : EmptyVariant}))))
subtypes:143 variant {µ variant} <: (µ variant) ... not ok (cannot compile)
tmp.mo:5.229-5.245: type error [M0029], unbound type EmptyVariant__50

import Prim "mo:⛔";type EmptyRecord = {_0_ : EmptyRecord};
type EmptyVariant = {#_0_ : EmptyVariant};
type Vec = [Vec];

assert ((prim "deserialize" : Blob -> (?(shared () -> async EmptyVariant))) "\44\49\44\4C\03\6A\00\01\01\00\6B\01\00\02\6B\01\00\02\01\00\01\01\00\01\6D" == (((?(actor "\61\61\61\61\61\2D\61\61" : actor { m : shared () -> async EmptyVariant__50 }).m)) : (?(shared () -> async EmptyVariant))))
subtypes:146 (µ vec) <: (µ vec) ... not ok (cannot compile)
tmp.mo:5.202-5.209: type error [M0029], unbound type Vec__48

import Prim "mo:⛔";type EmptyRecord = {_0_ : EmptyRecord};
type EmptyVariant = {#_0_ : EmptyVariant};
type Vec = [Vec];

assert ((prim "deserialize" : Blob -> (?(shared () -> async Vec))) "\44\49\44\4C\02\6A\00\01\01\00\6D\01\01\00\01\01\00\01\6D" == (((?(actor "\61\61\61\61\61\2D\61\61" : actor { m : shared () -> async Vec__48 }).m)) : (?(shared () -> async Vec))))
subtypes:148 (µ vec) </: empty ... ok (pass)
subtypes:150 empty <: (µ vec) ... not ok (cannot compile)
tmp.mo:5.196-5.203: type error [M0029], unbound type Vec__51

import Prim "mo:⛔";type EmptyRecord = {_0_ : EmptyRecord};
type EmptyVariant = {#_0_ : EmptyVariant};
type Vec = [Vec];

assert ((prim "deserialize" : Blob -> (?(shared () -> async Vec))) "\44\49\44\4C\01\6A\00\01\6F\00\01\00\01\01\00\01\6D" == (((?(actor "\61\61\61\61\61\2D\61\61" : actor { m : shared () -> async Vec__51 }).m)) : (?(shared () -> async Vec))))
subtypes:152 (µ vec) <: vec {µ vec} ... not ok (cannot compile)
tmp.mo:5.205-5.212: type error [M0029], unbound type Vec__53

import Prim "mo:⛔";type EmptyRecord = {_0_ : EmptyRecord};
type EmptyVariant = {#_0_ : EmptyVariant};
type Vec = [Vec];

assert ((prim "deserialize" : Blob -> (?(shared () -> async [Vec]))) "\44\49\44\4C\02\6A\00\01\01\00\6D\01\01\00\01\01\00\01\6D" == (((?(actor "\61\61\61\61\61\2D\61\61" : actor { m : shared () -> async [Vec__53] }).m)) : (?(shared () -> async [Vec]))))
subtypes:154 vec {µ vec} <: (µ vec) ... not ok (cannot compile)
tmp.mo:5.208-5.215: type error [M0029], unbound type Vec__55

import Prim "mo:⛔";type EmptyRecord = {_0_ : EmptyRecord};
type EmptyVariant = {#_0_ : EmptyVariant};
type Vec = [Vec];

assert ((prim "deserialize" : Blob -> (?(shared () -> async Vec))) "\44\49\44\4C\03\6A\00\01\01\00\6D\02\6D\02\01\00\01\01\00\01\6D" == (((?(actor "\61\61\61\61\61\2D\61\61" : actor { m : shared () -> async Vec__55 }).m)) : (?(shared () -> async Vec))))
subtypes:161 (future type) <: (opt empty) ... ok (pass)
subtypes:163 (future type) <: (nat) ... ok (pass)
410 tests:  356 skipped  42 ok  12 failed

Including LICENSE and a proper author/description/keywords. More could be added later but this fixes the requirements for open sourcing. Fixes dfinity#322 Co-authored-by: Kyle Peacock <kylpeacock@gmail.com>

test/construct.test.did

chenyan-dfinity · 2022-12-04T21:04:50Z

test/subtypes.test.did

+assert blob "DIDL\02\6a\00\01\01\00\6c\01\00\01\01\00\01\01\00\01m"
+   == "(null)" : (opt func () -> (empty)) "(µ record) </: empty";


Suggested change

assert blob "DIDL\02\6a\00\01\01\00\6c\01\00\01\01\00\01\01\00\01m"

== "(null)" : (opt func () -> (empty)) "(µ record) </: empty";

// assert blob "DIDL\02\6a\00\01\01\00\6c\01\00\01\01\00\01\01\00\01m"

// == "(null)" : (opt func () -> (empty)) "(µ record) </: empty";

I will comment out this test for now. It's a bit implementation dependent. In Rust, we replace µ record with empty after parsing the type table, so we actually get opt func instead of null.

Can you explain why? I don't quite follow.

In the Haskell code I think I too replace mu record with empty, but only after subtype checking?

I believe Motoko gets this right as spec'ed.

If we want to allow implementations to differ here we should say so explicitly in the spec. But I don't know if that's a good idea.

Could you introduce in the rust code a MuRecord type that you can replace it with, which does the job of preventing your code to run into these vicious cycles, while still having the right subtypes relations?

Hmm, but mu record <: mu (record opt), so you probably really can't throw away the structure before subtype checking.

Resolved offline. \mu record is shorthand for \mu t. record { 0 = t } which I agree is isomorphic to empty with least fixed points. Do you agree @nomeata or is it actually not safe to identify them in the type table, even if they are isomorphic.
My worry is that Motoko will still distinguish the types that Rust is conflating, which might lead to (obscure) trouble elsewhere.

It’s safe, I think, but it is not according to specification. If we go that route, it would be consistent to equate all other empty types as well (empty, {empty, empty} etc.), and it should be part of the spec. And I would guess that @rossberg doesn’t like it :-)

test/subtypes.test.did

Co-authored-by: Yan Chen <48968912+chenyan-dfinity@users.noreply.github.com>

revise existing tests to match #311 (subtype checking only for refere…

9b0e92e

…nce types)

crusso requested a review from chenyan-dfinity March 18, 2022 14:29

nomeata added 5 commits April 8, 2022 17:15

More test cases, new file for subtype tests

6976902

Many more tests

734b796

Tests about infinite types

135a26e

Use method name "m" to work around dfinity/motoko#1668

5e8c752

A few tests with future types

0889e28

crusso mentioned this pull request Nov 1, 2022

feat: candid subtype check dfinity/motoko#3171

Merged

8 tasks

chenyan-dfinity approved these changes Dec 4, 2022

View reviewed changes

chenyan-dfinity reviewed Dec 4, 2022

View reviewed changes

test/subtypes.test.did Outdated Show resolved Hide resolved

nomeata and others added 6 commits December 5, 2022 08:19

Update test/construct.test.did

9420864

Co-authored-by: Yan Chen <48968912+chenyan-dfinity@users.noreply.github.com>

Update test/subtypes.test.did

98ea8ed

Co-authored-by: Yan Chen <48968912+chenyan-dfinity@users.noreply.github.com>

Merge branch 'master' into claudio/candid-subtype-check

ad0dc5b

add "(µ record) <: (μ (record opt))"

086e43e

Merge branch 'master' into claudio/candid-subtype-check

d2b7b81

Merge branch 'master' into claudio/candid-subtype-check

96718cf

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

revise existing tests to match #311 (subtype checking only for refere… #323

revise existing tests to match #311 (subtype checking only for refere… #323

crusso commented Mar 18, 2022

nomeata commented Mar 18, 2022 •

edited

crusso commented Mar 18, 2022

nomeata commented Mar 18, 2022

crusso commented Apr 9, 2022 •

edited

chenyan-dfinity Dec 4, 2022

crusso Dec 4, 2022

nomeata Dec 5, 2022

crusso Dec 5, 2022

nomeata Dec 5, 2022 •

edited

		assert blob "DIDL\02\6a\00\01\01\00\6c\01\00\01\01\00\01\01\00\01m"
		== "(null)" : (opt func () -> (empty)) "(µ record) </: empty";

revise existing tests to match #311 (subtype checking only for refere… #323

Are you sure you want to change the base?

revise existing tests to match #311 (subtype checking only for refere… #323

Conversation

crusso commented Mar 18, 2022

nomeata commented Mar 18, 2022 • edited

crusso commented Mar 18, 2022

nomeata commented Mar 18, 2022

crusso commented Apr 9, 2022 • edited

chenyan-dfinity Dec 4, 2022

Choose a reason for hiding this comment

crusso Dec 4, 2022

Choose a reason for hiding this comment

nomeata Dec 5, 2022

Choose a reason for hiding this comment

crusso Dec 5, 2022

Choose a reason for hiding this comment

nomeata Dec 5, 2022 • edited

Choose a reason for hiding this comment

nomeata commented Mar 18, 2022 •

edited

crusso commented Apr 9, 2022 •

edited

nomeata Dec 5, 2022 •

edited