diff --git a/Cargo.lock b/Cargo.lock index c5cac5a0..093424fe 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -7,7 +7,7 @@ name = "a-mir-formality" version = "0.1.0" dependencies = [ "anyhow", - "clap 4.3.19", + "clap", "expect-test", "formality-check", "formality-core", @@ -18,24 +18,8 @@ dependencies = [ "formality-types", "pretty_assertions", "tracing", - "ui_test", ] -[[package]] -name = "addr2line" -version = "0.20.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f4fa78e18c64fce05e902adecd7a5eed15a5e0a3439f7b0e169f0252214865e3" -dependencies = [ - "gimli", -] - -[[package]] -name = "adler" -version = "1.0.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f26201604c87b1e01bd3d98f8d5d9a8fcbb815e8cedb41ffccbeb4bf593a35fe" - [[package]] name = "aho-corasick" version = "1.1.2" @@ -90,7 +74,7 @@ version = "1.0.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "5ca11d4be1bab0c8bc8734a9aa7bf4ee8316d462a08c6ac5052f888fef5b494b" dependencies = [ - "windows-sys 0.48.0", + "windows-sys", ] [[package]] @@ -100,7 +84,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "180abfa45703aebe0093f79badacc01b8fd4ea2e35118747e5811127f926e188" dependencies = [ "anstyle", - "windows-sys 0.48.0", + "windows-sys", ] [[package]] @@ -120,76 +104,12 @@ dependencies = [ "winapi", ] -[[package]] -name = "backtrace" -version = "0.3.68" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4319208da049c43661739c5fade2ba182f09d1dc2299b32298d3a31692b17e12" -dependencies = [ - "addr2line", - "cc", - "cfg-if", - "libc", - "miniz_oxide", - "object", - "rustc-demangle", -] - -[[package]] -name = "bitflags" -version = "1.3.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a" - [[package]] name = "bitflags" version = "2.3.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "630be753d4e58660abd17930c71b647fe46c27ea6b63cc59e1e3851406972e42" -[[package]] -name = "bstr" -version = "1.6.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6798148dccfbff0fae41c7574d2fa8f1ef3492fba0face179de5d8d447d67b05" -dependencies = [ - "memchr", - "regex-automata 0.3.3", - "serde", -] - -[[package]] -name = "camino" -version = "1.1.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c59e92b5a388f549b863a7bea62612c09f24c8393560709a54558a9abdfb3b9c" -dependencies = [ - "serde", -] - -[[package]] -name = "cargo-platform" -version = "0.1.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2cfa25e60aea747ec7e1124f238816749faa93759c6ff5b31f1ccdda137f4479" -dependencies = [ - "serde", -] - -[[package]] -name = "cargo_metadata" -version = "0.15.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "eee4243f1f26fc7a42710e7439c149e2b10b05472f88090acce52632f231a73a" -dependencies = [ - "camino", - "cargo-platform", - "semver", - "serde", - "serde_json", - "thiserror", -] - [[package]] name = "cc" version = "1.0.79" @@ -202,21 +122,6 @@ version = "1.0.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" -[[package]] -name = "clap" -version = "2.34.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a0610544180c38b88101fecf2dd634b174a62eef6946f84dfc6a7127512b381c" -dependencies = [ - "ansi_term", - "atty", - "bitflags 1.3.2", - "strsim 0.8.0", - "textwrap", - "unicode-width", - "vec_map", -] - [[package]] name = "clap" version = "4.3.19" @@ -237,7 +142,7 @@ dependencies = [ "anstream", "anstyle", "clap_lex", - "strsim 0.10.0", + "strsim", ] [[package]] @@ -246,7 +151,7 @@ version = "4.3.12" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "54a9bb5758fc5dfe728d1019941681eccaf0cf8a4189b692a0ee2f2ecf90a050" dependencies = [ - "heck 0.4.0", + "heck", "proc-macro2", "quote", "syn 2.0.27", @@ -258,69 +163,12 @@ version = "0.5.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "2da6da31387c7e4ef160ffab6d5e7f00c42626fe39aea70a7b0f1773f7dd6c1b" -[[package]] -name = "color-eyre" -version = "0.6.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5a667583cca8c4f8436db8de46ea8233c42a7d9ae424a82d338f2e4675229204" -dependencies = [ - "backtrace", - "color-spantrace", - "eyre", - "indenter", - "once_cell", - "owo-colors", - "tracing-error", -] - -[[package]] -name = "color-spantrace" -version = "0.2.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1ba75b3d9449ecdccb27ecbc479fdc0b87fa2dd43d2f8298f9bf0e59aacc8dce" -dependencies = [ - "once_cell", - "owo-colors", - "tracing-core", - "tracing-error", -] - [[package]] name = "colorchoice" version = "1.0.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "acbf1af155f9b9ef647e42cdc158db4b64a1b61f743629225fde6f3e0be2a7c7" -[[package]] -name = "colored" -version = "2.0.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2674ec482fbc38012cf31e6c42ba0177b431a0cb6f15fe40efa5aab1bda516f6" -dependencies = [ - "is-terminal", - "lazy_static", - "windows-sys 0.48.0", -] - -[[package]] -name = "comma" -version = "1.0.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "55b672471b4e9f9e95499ea597ff64941a309b2cdbffcc46f2cc5e2d971fd335" - -[[package]] -name = "console" -version = "0.15.7" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c926e00cc70edefdc64d3a5ff31cc65bb97a3460097762bd23afb4d8145fccf8" -dependencies = [ - "encode_unicode 0.3.6", - "lazy_static", - "libc", - "unicode-width", - "windows-sys 0.45.0", -] - [[package]] name = "contracts" version = "0.6.3" @@ -341,46 +189,6 @@ dependencies = [ "unicode-segmentation", ] -[[package]] -name = "crossbeam-channel" -version = "0.5.8" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a33c2bf77f2df06183c3aa30d1e96c0695a313d4f9c453cc3762a6db39f99200" -dependencies = [ - "cfg-if", - "crossbeam-utils", -] - -[[package]] -name = "crossbeam-utils" -version = "0.8.16" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5a22b2d63d4d1dc0b7f1b6b2747dd0088008a9be28b6ddf0b1e7d335e3037294" -dependencies = [ - "cfg-if", -] - -[[package]] -name = "csv" -version = "1.2.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "626ae34994d3d8d668f4269922248239db4ae42d538b14c398b74a52208e8086" -dependencies = [ - "csv-core", - "itoa", - "ryu", - "serde", -] - -[[package]] -name = "csv-core" -version = "0.1.10" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2b2466559f260f48ad25fe6317b3c8dac77b5bdb5763ac7d9d6103530663bc90" -dependencies = [ - "memchr", -] - [[package]] name = "ctor" version = "0.1.23" @@ -408,57 +216,18 @@ version = "0.1.13" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "56254986775e3233ffa9c4d7d3faaf6d36a2c09d30b20687e9f88bc8bafc16c8" -[[package]] -name = "dirs-next" -version = "2.0.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b98cf8ebf19c3d1b223e151f99a4f9f0690dca41414773390fc824184ac833e1" -dependencies = [ - "cfg-if", - "dirs-sys-next", -] - -[[package]] -name = "dirs-sys-next" -version = "0.1.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4ebda144c4fe02d1f7ea1a7d9641b6fc6b580adcfa024ae48797ecdeb6825b4d" -dependencies = [ - "libc", - "redox_users", - "winapi", -] - [[package]] name = "dissimilar" version = "1.0.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "8c97b9233581d84b8e1e689cdd3a47b6f69770084fc246e86a7f78b0d9c1d4a5" -[[package]] -name = "distance" -version = "0.4.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6d9d8664cf849d7d0f3114a3a387d2f5e4303176d746d5a951aaddc66dfe9240" - [[package]] name = "either" version = "1.9.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "a26ae43d7bcc3b814de94796a5e736d4029efb0ee900c12e2d54c993ad1a1e07" -[[package]] -name = "encode_unicode" -version = "0.3.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a357d28ed41a50f9c765dbfe56cbc04a64e53e5fc58ba79fbc34c10ef3df831f" - -[[package]] -name = "encode_unicode" -version = "1.0.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "34aa73646ffb006b8f5147f3dc182bd4bcb190227ce861fc4a4844bf8e3cb2c0" - [[package]] name = "env_logger" version = "0.10.0" @@ -480,7 +249,7 @@ checksum = "4bcfec3a70f97c962c307b2d2c56e358cf1d00b558d74262b5f929ee8cc7e73a" dependencies = [ "errno-dragonfly", "libc", - "windows-sys 0.48.0", + "windows-sys", ] [[package]] @@ -495,9 +264,9 @@ dependencies = [ [[package]] name = "expect-test" -version = "1.4.1" +version = "1.5.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "30d9eafeadd538e68fb28016364c9732d78e420b9ff8853fa5e4058861e9f8d3" +checksum = "9e0be0a561335815e06dab7c62e50353134c796e7a6155402a64bcff66b6a5e0" dependencies = [ "dissimilar", "once_cell", @@ -514,22 +283,6 @@ dependencies = [ "syn 1.0.102", ] -[[package]] -name = "eyre" -version = "0.6.8" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4c2b6b5a29c02cdc822728b7d7b8ae1bab3e3b05d44522770ddd49722eeac7eb" -dependencies = [ - "indenter", - "once_cell", -] - -[[package]] -name = "fastrand" -version = "2.0.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6999dc1837253364c2ebb0704ba97994bd874e8f195d665c50b7548f6ea92764" - [[package]] name = "final_fn" version = "0.1.0" @@ -645,32 +398,6 @@ dependencies = [ "tracing", ] -[[package]] -name = "getrandom" -version = "0.2.10" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "be4136b2a15dd319360be1c07d9933517ccf0be8f16bf62a3bee4f0d618df427" -dependencies = [ - "cfg-if", - "libc", - "wasi", -] - -[[package]] -name = "gimli" -version = "0.27.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b6c80984affa11d98d1b88b66ac8853f143217b399d3c74116778ff8fdb4ed2e" - -[[package]] -name = "heck" -version = "0.3.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6d621efb26863f0e9924c6ac577e8275e5e6b77455db64ffa6c65c904e9e132c" -dependencies = [ - "unicode-segmentation", -] - [[package]] name = "heck" version = "0.4.0" @@ -698,34 +425,6 @@ version = "2.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9a3a5bfb195931eeb336b2a7b4d761daec841b97f947d34394601737a7bba5e4" -[[package]] -name = "indenter" -version = "0.3.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ce23b50ad8242c51a442f3ff322d56b02f08852c77e4c0b4d3fd684abc89c683" - -[[package]] -name = "indicatif" -version = "0.17.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8ff8cc23a7393a397ed1d7f56e6365cba772aba9f9912ab968b03043c395d057" -dependencies = [ - "console", - "instant", - "number_prefix", - "portable-atomic", - "unicode-width", -] - -[[package]] -name = "instant" -version = "0.1.12" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7a5bbe824c507c5da5956355e86a746d82e0e1464f65d862cc5e71da70e94b2c" -dependencies = [ - "cfg-if", -] - [[package]] name = "is-terminal" version = "0.4.9" @@ -734,7 +433,7 @@ checksum = "cb0889898416213fab133e1d33a0e5858a48177452750691bde3666d0fdbaf8b" dependencies = [ "hermit-abi 0.3.2", "rustix", - "windows-sys 0.48.0", + "windows-sys", ] [[package]] @@ -755,12 +454,6 @@ dependencies = [ "either", ] -[[package]] -name = "itoa" -version = "1.0.9" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "af150ab688ff2122fcef229be89cb50dd66af9e01a4ff320cc137eecc9bacc38" - [[package]] name = "lazy_static" version = "1.4.0" @@ -803,30 +496,6 @@ version = "2.7.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "523dc4f511e55ab87b694dc30d0f820d60906ef06413f93d4d7a1385599cc149" -[[package]] -name = "miniz_oxide" -version = "0.7.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e7810e0be55b428ada41041c41f32c9f1a42817901b4ccf45fa3d4b6561e74c7" -dependencies = [ - "adler", -] - -[[package]] -name = "number_prefix" -version = "0.4.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "830b246a0e5f20af87141b25c173cd1b609bd7779a4617d6ec582abaf90870f3" - -[[package]] -name = "object" -version = "0.31.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8bda667d9f2b5051b8833f59f3bf748b28ef54f850f4fcb389a252aa383866d1" -dependencies = [ - "memchr", -] - [[package]] name = "once_cell" version = "1.15.0" @@ -842,33 +511,12 @@ dependencies = [ "winapi", ] -[[package]] -name = "owo-colors" -version = "3.5.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c1b04fb49957986fdce4d6ee7a65027d55d4b6d2265e5848bbb507b58ccfdb6f" - -[[package]] -name = "pad" -version = "0.1.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d2ad9b889f1b12e0b9ee24db044b5129150d5eada288edc800f789928dc8c0e3" -dependencies = [ - "unicode-width", -] - [[package]] name = "pin-project-lite" version = "0.2.9" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "e0a7ae3ac2f1173085d398531c705756c94a4c56843785df85a60c1a0afac116" -[[package]] -name = "portable-atomic" -version = "1.4.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "edc55135a600d700580e406b4de0d59cb9ad25e344a3a091a97ded2622ec4ec6" - [[package]] name = "pretty_assertions" version = "1.3.0" @@ -881,56 +529,6 @@ dependencies = [ "yansi", ] -[[package]] -name = "prettydiff" -version = "0.6.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8ff1fec61082821f8236cf6c0c14e8172b62ce8a72a0eedc30d3b247bb68dc11" -dependencies = [ - "ansi_term", - "pad", - "prettytable-rs", - "structopt", -] - -[[package]] -name = "prettytable-rs" -version = "0.10.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "eea25e07510aa6ab6547308ebe3c036016d162b8da920dbb079e3ba8acf3d95a" -dependencies = [ - "csv", - "encode_unicode 1.0.0", - "is-terminal", - "lazy_static", - "term", - "unicode-width", -] - -[[package]] -name = "proc-macro-error" -version = "1.0.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "da25490ff9892aab3fcf7c36f08cfb902dd3e71ca0f9f9517bea02a73a5ce38c" -dependencies = [ - "proc-macro-error-attr", - "proc-macro2", - "quote", - "syn 1.0.102", - "version_check", -] - -[[package]] -name = "proc-macro-error-attr" -version = "1.0.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a1be40180e52ecc98ad80b184934baf3d0d29f979574e439af5a55274b35f869" -dependencies = [ - "proc-macro2", - "quote", - "version_check", -] - [[package]] name = "proc-macro2" version = "1.0.66" @@ -958,35 +556,6 @@ dependencies = [ "proc-macro2", ] -[[package]] -name = "redox_syscall" -version = "0.2.16" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fb5a58c1855b4b6819d59012155603f0b22ad30cad752600aadfcb695265519a" -dependencies = [ - "bitflags 1.3.2", -] - -[[package]] -name = "redox_syscall" -version = "0.3.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "567664f262709473930a4bf9e51bf2ebf3348f2e748ccc50dea20646858f8f29" -dependencies = [ - "bitflags 1.3.2", -] - -[[package]] -name = "redox_users" -version = "0.4.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b033d837a7cf162d7993aded9304e30a83213c648b6e389db233191f891e5c2b" -dependencies = [ - "getrandom", - "redox_syscall 0.2.16", - "thiserror", -] - [[package]] name = "regex" version = "1.10.2" @@ -1008,12 +577,6 @@ dependencies = [ "regex-syntax 0.6.27", ] -[[package]] -name = "regex-automata" -version = "0.3.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "39354c10dd07468c2e73926b23bb9c2caca74c5501e38a35da70406f1d923310" - [[package]] name = "regex-automata" version = "0.4.3" @@ -1037,96 +600,17 @@ version = "0.8.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "c08c74e62047bb2de4ff487b251e4a92e24f48745648451635cec7d591162d9f" -[[package]] -name = "rustc-demangle" -version = "0.1.23" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d626bb9dae77e28219937af045c257c28bfd3f69333c512553507f5f9798cb76" - -[[package]] -name = "rustc_version" -version = "0.4.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "bfa0f585226d2e68097d4f95d113b15b83a82e819ab25717ec0590d9584ef366" -dependencies = [ - "semver", -] - -[[package]] -name = "rustfix" -version = "0.6.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ecd2853d9e26988467753bd9912c3a126f642d05d229a4b53f5752ee36c56481" -dependencies = [ - "anyhow", - "log", - "serde", - "serde_json", -] - [[package]] name = "rustix" version = "0.38.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0a962918ea88d644592894bc6dc55acc6c0956488adcebbfb6e273506b7fd6e5" dependencies = [ - "bitflags 2.3.3", + "bitflags", "errno", "libc", "linux-raw-sys", - "windows-sys 0.48.0", -] - -[[package]] -name = "rustversion" -version = "1.0.14" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7ffc183a10b4478d04cbbbfc96d0873219d962dd5accaff2ffbd4ceb7df837f4" - -[[package]] -name = "ryu" -version = "1.0.15" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1ad4cc8da4ef723ed60bced201181d83791ad433213d8c24efffda1eec85d741" - -[[package]] -name = "semver" -version = "1.0.18" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b0293b4b29daaf487284529cc2f5675b8e57c61f70167ba415a463651fd6a918" -dependencies = [ - "serde", -] - -[[package]] -name = "serde" -version = "1.0.147" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d193d69bae983fc11a79df82342761dfbf28a99fc8d203dca4c3c1b590948965" -dependencies = [ - "serde_derive", -] - -[[package]] -name = "serde_derive" -version = "1.0.147" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4f1d362ca8fc9c3e3a7484440752472d68a6caa98f1ab81d99b5dfe517cec852" -dependencies = [ - "proc-macro2", - "quote", - "syn 1.0.102", -] - -[[package]] -name = "serde_json" -version = "1.0.99" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "46266871c240a00b8f503b877622fe33430b3c7d963bdc0f2adc511e54a1eae3" -dependencies = [ - "itoa", - "ryu", - "serde", + "windows-sys", ] [[package]] @@ -1151,42 +635,12 @@ dependencies = [ "winapi", ] -[[package]] -name = "strsim" -version = "0.8.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8ea5119cdb4c55b55d432abb513a0429384878c15dde60cc77b1c99de1a95a6a" - [[package]] name = "strsim" version = "0.10.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "73473c0e59e6d5812c5dfe2a064a6444949f089e20eec9a2e5506596494e4623" -[[package]] -name = "structopt" -version = "0.3.26" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0c6b5c64445ba8094a6ab0c3cd2ad323e07171012d9c98b0b15651daf1787a10" -dependencies = [ - "clap 2.34.0", - "lazy_static", - "structopt-derive", -] - -[[package]] -name = "structopt-derive" -version = "0.4.18" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "dcb5ae327f9cc13b68763b5749770cb9e048a99bd9dfdfa58d0cf05d5f64afe0" -dependencies = [ - "heck 0.3.3", - "proc-macro-error", - "proc-macro2", - "quote", - "syn 1.0.102", -] - [[package]] name = "syn" version = "1.0.102" @@ -1221,30 +675,6 @@ dependencies = [ "unicode-xid", ] -[[package]] -name = "tempfile" -version = "3.7.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5486094ee78b2e5038a6382ed7645bc084dc2ec433426ca4c3cb61e2007b8998" -dependencies = [ - "cfg-if", - "fastrand", - "redox_syscall 0.3.5", - "rustix", - "windows-sys 0.48.0", -] - -[[package]] -name = "term" -version = "0.7.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c59df8ac95d96ff9bede18eb7300b0fda5e5d8d90960e76f8e14ae765eedbf1f" -dependencies = [ - "dirs-next", - "rustversion", - "winapi", -] - [[package]] name = "termcolor" version = "1.1.3" @@ -1254,35 +684,6 @@ dependencies = [ "winapi-util", ] -[[package]] -name = "textwrap" -version = "0.11.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d326610f408c7a4eb6f51c37c330e496b08506c9457c9d34287ecc38809fb060" -dependencies = [ - "unicode-width", -] - -[[package]] -name = "thiserror" -version = "1.0.39" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a5ab016db510546d856297882807df8da66a16fb8c4101cb8b30054b0d5b2d9c" -dependencies = [ - "thiserror-impl", -] - -[[package]] -name = "thiserror-impl" -version = "1.0.39" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5420d42e90af0c38c3290abcca25b9b3bdf379fc9f55c528f53a269d9c9a267e" -dependencies = [ - "proc-macro2", - "quote", - "syn 1.0.102", -] - [[package]] name = "thread_local" version = "1.1.4" @@ -1324,16 +725,6 @@ dependencies = [ "valuable", ] -[[package]] -name = "tracing-error" -version = "0.2.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d686ec1c0f384b1277f097b2f279a2ecc11afe8c133c1aabf036a27cb4cd206e" -dependencies = [ - "tracing", - "tracing-subscriber", -] - [[package]] name = "tracing-log" version = "0.1.3" @@ -1373,33 +764,6 @@ dependencies = [ "tracing-subscriber", ] -[[package]] -name = "ui_test" -version = "0.12.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5cee90fef5a3d0887b7b16651c23d2fcd91b2636dad26c9e839e75f2df2789e0" -dependencies = [ - "anyhow", - "bstr", - "cargo-platform", - "cargo_metadata", - "clap 4.3.19", - "color-eyre", - "colored", - "comma", - "crossbeam-channel", - "distance", - "indicatif", - "lazy_static", - "prettydiff", - "regex", - "rustc_version", - "rustfix", - "serde", - "serde_json", - "tempfile", -] - [[package]] name = "unicode-ident" version = "1.0.4" @@ -1412,12 +776,6 @@ version = "1.10.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0fdbf052a0783de01e944a6ce7a8cb939e295b1e7be835a1112c3b9a7f047a5a" -[[package]] -name = "unicode-width" -version = "0.1.10" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c0edd1e5b14653f783770bce4a4dabb4a5108a5370a5f5d8cfe8710c361f6c8b" - [[package]] name = "unicode-xid" version = "0.2.4" @@ -1436,24 +794,6 @@ version = "0.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "830b7e5d4d90034032940e4ace0d9a9a057e7a45cd94e6c007832e39edb82f6d" -[[package]] -name = "vec_map" -version = "0.8.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f1bddf1187be692e79c5ffeab891132dfb0f236ed36a43c7ed39f1165ee20191" - -[[package]] -name = "version_check" -version = "0.9.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "49874b5167b65d7193b8aba1567f5c7d93d001cafc34600cee003eda787e483f" - -[[package]] -name = "wasi" -version = "0.11.0+wasi-snapshot-preview1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9c8d87e72b64a3b4db28d11ce29237c246188f4f51057d65a7eab63b7987e423" - [[package]] name = "winapi" version = "0.3.9" @@ -1485,37 +825,13 @@ version = "0.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f" -[[package]] -name = "windows-sys" -version = "0.45.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "75283be5efb2831d37ea142365f009c02ec203cd29a3ebecbc093d52315b66d0" -dependencies = [ - "windows-targets 0.42.2", -] - [[package]] name = "windows-sys" version = "0.48.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "677d2418bec65e3338edb076e806bc1ec15693c5d0104683f2efe857f61056a9" dependencies = [ - "windows-targets 0.48.1", -] - -[[package]] -name = "windows-targets" -version = "0.42.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8e5180c00cd44c9b1c88adb3693291f1cd93605ded80c250a75d472756b4d071" -dependencies = [ - "windows_aarch64_gnullvm 0.42.2", - "windows_aarch64_msvc 0.42.2", - "windows_i686_gnu 0.42.2", - "windows_i686_msvc 0.42.2", - "windows_x86_64_gnu 0.42.2", - "windows_x86_64_gnullvm 0.42.2", - "windows_x86_64_msvc 0.42.2", + "windows-targets", ] [[package]] @@ -1524,93 +840,51 @@ version = "0.48.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "05d4b17490f70499f20b9e791dcf6a299785ce8af4d709018206dc5b4953e95f" dependencies = [ - "windows_aarch64_gnullvm 0.48.0", - "windows_aarch64_msvc 0.48.0", - "windows_i686_gnu 0.48.0", - "windows_i686_msvc 0.48.0", - "windows_x86_64_gnu 0.48.0", - "windows_x86_64_gnullvm 0.48.0", - "windows_x86_64_msvc 0.48.0", + "windows_aarch64_gnullvm", + "windows_aarch64_msvc", + "windows_i686_gnu", + "windows_i686_msvc", + "windows_x86_64_gnu", + "windows_x86_64_gnullvm", + "windows_x86_64_msvc", ] -[[package]] -name = "windows_aarch64_gnullvm" -version = "0.42.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "597a5118570b68bc08d8d59125332c54f1ba9d9adeedeef5b99b02ba2b0698f8" - [[package]] name = "windows_aarch64_gnullvm" version = "0.48.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "91ae572e1b79dba883e0d315474df7305d12f569b400fcf90581b06062f7e1bc" -[[package]] -name = "windows_aarch64_msvc" -version = "0.42.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e08e8864a60f06ef0d0ff4ba04124db8b0fb3be5776a5cd47641e942e58c4d43" - [[package]] name = "windows_aarch64_msvc" version = "0.48.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b2ef27e0d7bdfcfc7b868b317c1d32c641a6fe4629c171b8928c7b08d98d7cf3" -[[package]] -name = "windows_i686_gnu" -version = "0.42.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c61d927d8da41da96a81f029489353e68739737d3beca43145c8afec9a31a84f" - [[package]] name = "windows_i686_gnu" version = "0.48.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "622a1962a7db830d6fd0a69683c80a18fda201879f0f447f065a3b7467daa241" -[[package]] -name = "windows_i686_msvc" -version = "0.42.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "44d840b6ec649f480a41c8d80f9c65108b92d89345dd94027bfe06ac444d1060" - [[package]] name = "windows_i686_msvc" version = "0.48.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "4542c6e364ce21bf45d69fdd2a8e455fa38d316158cfd43b3ac1c5b1b19f8e00" -[[package]] -name = "windows_x86_64_gnu" -version = "0.42.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8de912b8b8feb55c064867cf047dda097f92d51efad5b491dfb98f6bbb70cb36" - [[package]] name = "windows_x86_64_gnu" version = "0.48.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "ca2b8a661f7628cbd23440e50b05d705db3686f894fc9580820623656af974b1" -[[package]] -name = "windows_x86_64_gnullvm" -version = "0.42.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "26d41b46a36d453748aedef1486d5c7a85db22e56aff34643984ea85514e94a3" - [[package]] name = "windows_x86_64_gnullvm" version = "0.48.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "7896dbc1f41e08872e9d5e8f8baa8fdd2677f29468c4e156210174edc7f7b953" -[[package]] -name = "windows_x86_64_msvc" -version = "0.42.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9aec5da331524158c6d1a4ac0ab1541149c0b9505fde06423b02f5ef0106b9f0" - [[package]] name = "windows_x86_64_msvc" version = "0.48.0" diff --git a/Cargo.toml b/Cargo.toml index f6571d0c..0c07551d 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -30,7 +30,7 @@ formality-check = { version = "0.1.0", path = "crates/formality-check" } formality-prove = { version = "0.1.0", path = "crates/formality-prove" } formality-core = { version = "0.1.0", path = "crates/formality-core" } formality-smir = { version = "0.1.0", path = "crates/formality-smir" } -ui_test = "0.12" +expect-test = "1.4.0" [workspace] members = [ @@ -42,7 +42,3 @@ members = [ "crates/formality-prove", "crates/formality-smir", ] - -[[test]] -name = "ui" -harness = false diff --git a/crates/formality-check/src/coherence.rs b/crates/formality-check/src/coherence.rs index 5f9abfd5..7f679a9a 100644 --- a/crates/formality-check/src/coherence.rs +++ b/crates/formality-check/src/coherence.rs @@ -24,7 +24,9 @@ impl Check<'_> { self.orphan_check_neg(impl_a)?; } - // check for duplicate impls in the current crate + // check for duplicate impls in the current crate; + // the cartesian product below would otherwise consider every impl I + // as overlapping with itself. for (impl_a, i) in current_crate_impls.iter().zip(0..) { if current_crate_impls[i + 1..].contains(impl_a) { bail!("duplicate impl in current crate: {:?}", impl_a) diff --git a/crates/formality-check/src/lib.rs b/crates/formality-check/src/lib.rs index e3236b2c..1e284e40 100644 --- a/crates/formality-check/src/lib.rs +++ b/crates/formality-check/src/lib.rs @@ -107,6 +107,7 @@ impl Check<'_> { bail!("failed to prove {goal:?} given {assumptions:?}, got {cs:?}") } + #[tracing::instrument(level = "Debug", skip(self, assumptions, goal))] fn prove_not_goal( &self, env: &Env, @@ -116,6 +117,9 @@ impl Check<'_> { let goal: Wcs = goal.to_wcs(); let assumptions: Wcs = assumptions.to_wcs(); + tracing::debug!("assumptions = {assumptions:?}"); + tracing::debug!("goal = {goal:?}"); + assert!(env.only_universal_variables()); assert!(env.encloses((&assumptions, &goal))); @@ -146,10 +150,16 @@ impl Check<'_> { &existential_goal, ); - if !cs.is_proven() { - return Ok(()); + match cs.into_set() { + Ok(proofs) => { + bail!( + "failed to disprove\n {goal:?}\ngiven\n {assumptions:?}\ngot\n{proofs:?}" + ) + } + Err(err) => { + tracing::debug!("Proved not goal, error = {err}"); + return Ok(()); + } } - - bail!("failed to disprove\n {goal:?}\ngiven\n {assumptions:?}\ngot\n{cs:?}") } } diff --git a/crates/formality-core/src/judgment/proven_set.rs b/crates/formality-core/src/judgment/proven_set.rs index 8b2c2a71..aba06d94 100644 --- a/crates/formality-core/src/judgment/proven_set.rs +++ b/crates/formality-core/src/judgment/proven_set.rs @@ -91,7 +91,7 @@ impl ProvenSet { } } - /// Convert to a non-empty set of proven results (if ok) or an error (otherwise). + /// Iterate through all solutions. pub fn iter<'a>(&'a self) -> Box + 'a> { match &self.data { Data::Failure(_) => Box::new(std::iter::empty()), diff --git a/crates/formality-core/src/test_util.rs b/crates/formality-core/src/test_util.rs index c361a28b..c7a401ed 100644 --- a/crates/formality-core/src/test_util.rs +++ b/crates/formality-core/src/test_util.rs @@ -50,9 +50,15 @@ pub trait ResultTestExt { /// Given a `Fallible` value, assert that its debug representation matches the expected value. /// If the result is an error it is propagated through to the return value. fn assert_ok(self, expect: expect_test::Expect); + /// Given a `Fallible` value, assert that it is an error with the given string (after normalization). /// Returns `Ok(())` if the assertion succeeds, or panics if the assertion fails. fn assert_err(self, expect: expect_test::Expect); + + /// Given a `Fallible` value, assert that it is an error with the given string (after normalization). + /// Also assert that each of the strings in `must_have` appears somewhere within. + /// Returns `Ok(())` if the assertion succeeds, or panics if the assertion fails. + fn assert_has_err(self, expect: expect_test::Expect, must_have: &[&str]); } impl ResultTestExt for Result @@ -74,10 +80,21 @@ where #[track_caller] fn assert_err(self, expect: expect_test::Expect) { + self.assert_has_err(expect, &[]); + } + + #[track_caller] + fn assert_has_err(self, expect: expect_test::Expect, must_have: &[&str]) { match self { Ok(v) => panic!("expected `Err`, got `Ok`: {v:?}"), Err(e) => { - expect.assert_eq(&normalize_paths(format!("{e:?}"))); + let output = normalize_paths(format!("{e:?}")); + + expect.assert_eq(&output); + + for s in must_have { + assert!(output.contains(s), "did not find {s:?} in the output"); + } } } } diff --git a/crates/formality-prove/src/prove/combinators.rs b/crates/formality-prove/src/prove/combinators.rs index ed2ca6d8..e3ccf8b6 100644 --- a/crates/formality-prove/src/prove/combinators.rs +++ b/crates/formality-prove/src/prove/combinators.rs @@ -1,5 +1,5 @@ use crate::decls::Decls; -use formality_core::{ProvenSet, Upcast}; +use formality_core::ProvenSet; use formality_types::rust::Term; use super::{Constraints, Env}; @@ -20,7 +20,7 @@ where assert_eq!(a.len(), b.len()); if a.is_empty() && b.is_empty() { - return ProvenSet::singleton(Constraints::none(env.upcast())); + return ProvenSet::singleton(Constraints::none(env)); } let a0 = a.remove(0); @@ -45,7 +45,7 @@ where C: Term, { if a.is_empty() { - return ProvenSet::singleton(Constraints::none(env.upcast())); + return ProvenSet::singleton(Constraints::none(env)); } let a0 = a[0].clone(); diff --git a/crates/formality-prove/src/prove/constraints.rs b/crates/formality-prove/src/prove/constraints.rs index 726b5a20..42f7cb3b 100644 --- a/crates/formality-prove/src/prove/constraints.rs +++ b/crates/formality-prove/src/prove/constraints.rs @@ -25,7 +25,7 @@ where } impl Constraints { - pub fn none(env: Env) -> Self { + pub fn none(env: impl Upcast) -> Self { let v: Vec<(Variable, Parameter)> = vec![]; Self::from(env, v) } @@ -42,9 +42,10 @@ impl Constraints { } pub fn from( - env: Env, + env: impl Upcast, iter: impl IntoIterator, impl Upcast)>, ) -> Self { + let env = env.upcast(); let substitution: Substitution = iter.into_iter().collect(); assert!(env.encloses(substitution.range())); assert!(env.encloses(substitution.domain())); @@ -72,7 +73,7 @@ impl Constraints { } } - /// Given constraings from solving the subparts of `(A /\ B)`, yield combined constraints. + /// Given constraints from solving the subparts of `(A /\ B)`, yield combined constraints. /// /// # Parameters /// diff --git a/crates/formality-prove/src/prove/is_local.rs b/crates/formality-prove/src/prove/is_local.rs index 22636d20..e9aab047 100644 --- a/crates/formality-prove/src/prove/is_local.rs +++ b/crates/formality-prove/src/prove/is_local.rs @@ -1,6 +1,6 @@ -use formality_core::{judgment_fn, set, Set}; +use formality_core::{judgment_fn, ProvenSet, Upcast}; use formality_types::grammar::{ - Lt, Parameter, RigidName, RigidTy, TraitRef, TyData, Variable, Wcs, + AliasTy, BoundVar, Lt, Parameter, RigidName, RigidTy, TraitRef, TyData, Variable, Wcs, }; use crate::{ @@ -37,24 +37,166 @@ use crate::{ // `Vec` is not. `LocalType` is local. Type aliases and trait // aliases do not affect locality. -/// True if `goal` may be remote. This is -pub fn may_be_remote(decls: Decls, env: Env, assumptions: Wcs, goal: TraitRef) -> Set { +judgment_fn! { + /// True if `goal` may be implemented in a crate that is not the current one. + /// This could be a downstream crate that we cannot see, or it could be a future + /// (semver-compatible) version of an upstream crate. + /// + /// Note that per RFC #2451, upstream crates are not permitted to add blanket impls + /// and so new upstream impls for local types cannot be added. + pub fn may_be_remote( + decls: Decls, + env: Env, + assumptions: Wcs, + goal: TraitRef, + ) => () { + debug(assumptions, goal, decls, env) + + ( + (may_be_downstream_trait_ref(decls, env, assumptions, goal) => ()) + --- ("may be defined downstream") + (may_be_remote(decls, env, assumptions, goal) => ()) + ) + + ( + // In principle this rule could be removed and preserve soundness, + // but then we would accept code that is very prone to semver failures. + (may_not_be_provable(is_local_trait_ref(decls, env, assumptions, goal)) => ()) + --- ("may be added by upstream in a minor release") + (may_be_remote(decls, env, assumptions, goal) => ()) + ) + } +} + +judgment_fn! { + /// True if an impl defining this trait-reference could appear in a downstream crate. + fn may_be_downstream_trait_ref( + decls: Decls, + env: Env, + assumptions: Wcs, + goal: TraitRef, + ) => () { + debug(goal, assumptions, env, decls) + + ( + // There may be a downstream parameter at position i... + (&goal.parameters => p) + (may_be_downstream_parameter(&decls, &env, &assumptions, p) => ()) + --- ("may_be_downstream_trait_ref") + (may_be_downstream_trait_ref(decls, env, assumptions, goal) => ()) + ) + } +} + +judgment_fn! { + fn may_be_downstream_parameter( + decls: Decls, + env: Env, + assumptions: Wcs, + parameter: Parameter, + ) => () { + debug(parameter, assumptions, env, decls) + + ( + // existential variables *could* be inferred to downstream types; depends on the substitution + // we ultimately have. + --- ("type variable") + (may_be_downstream_parameter(_decls, _env, _assumptions, TyData::Variable(Variable::ExistentialVar(_))) => ()) + ) + + // If we can normalize `goal` to something else, and that normalized + // form may be downstream. + ( + // (a) there is some parameter in the alias that may be downstream + (parameters.iter() => p) + (if may_contain_downstream_type(&decls, &env, &assumptions, p)) + + // (b) the alias cannot be normalized to something that may not be downstream + (may_not_be_provable(normalizes_to_not_downstream(&decls, &env, &assumptions, AliasTy { name: name.clone(), parameters: parameters.clone() })) => ()) + --- ("via normalize") + (may_be_downstream_parameter(decls, env, assumptions, AliasTy { name, parameters }) => ()) + ) + } +} + +fn may_contain_downstream_type( + decls: &Decls, + env: &Env, + assumptions: &Wcs, + parameter: impl Upcast, +) -> bool { assert!(env.is_in_coherence_mode()); + let parameter = parameter.upcast(); - let c = is_local_trait_ref(decls, &env, assumptions, goal); + let Parameter::Ty(ty) = parameter else { + return false; + }; - if !c.is_proven() { - // Cannot possibly be local, so always remote. - return set![Constraints::none(env)]; + match ty.data() { + TyData::RigidTy(RigidTy { + name: _, + parameters, + }) => parameters + .iter() + .any(|p| may_contain_downstream_type(decls, env, assumptions, p)), + TyData::AliasTy(_) => prove_normalize(decls, env, assumptions, ty) + .iter() + .any(|(c, p)| { + let assumptions = c.substitution().apply(assumptions); + may_contain_downstream_type(decls, env, &assumptions, p) + }), + TyData::PredicateTy(p) => match p { + formality_types::grammar::PredicateTy::ForAll(binder) => { + let (_, ty) = binder.open(); + may_contain_downstream_type(decls, env, assumptions, ty) + } + }, + TyData::Variable(v) => match v { + Variable::ExistentialVar(_) => true, + Variable::UniversalVar(_) => panic!("universals are unexpected"), + Variable::BoundVar(BoundVar { + debruijn, + var_index: _, + kind: _, + }) => { + assert!(debruijn.is_none(), "must have been opened on the way down"); + true + } + }, } +} - if c.iter().any(Constraints::unconditionally_true) { - // If this is unconditionally known to be local, then it is never remote. - return set![]; +fn may_not_be_provable(op: ProvenSet) -> ProvenSet<()> { + if let Some(constraints) = op + .iter() + .find(|constraints| constraints.unconditionally_true()) + { + ProvenSet::failed( + "may_not_be_provable", + format!("found a solution {constraints:?}"), + ) + } else { + ProvenSet::singleton(()) } +} - // Otherwise it is ambiguous - set![Constraints::none(env).ambiguous()] +judgment_fn! { + fn normalizes_to_not_downstream( + decls: Decls, + env: Env, + assumptions: Wcs, + parameter: Parameter, + ) => Constraints { + debug(parameter, assumptions, env, decls) + + ( + (prove_normalize(&decls, &env, &assumptions, parameter) => (c1, parameter)) + (let assumptions = c1.substitution().apply(&assumptions)) + (is_not_downstream(&decls, &env, assumptions, parameter) => c2) + --- ("ambiguous") + (normalizes_to_not_downstream(decls, env, assumptions, parameter) => c1.seq(c2)) + ) + } } judgment_fn! { @@ -73,11 +215,14 @@ judgment_fn! { ) ( + // There is a local parameter at position i... (0 .. goal.parameters.len() => i) (is_local_parameter(&decls, &env, &assumptions, &goal.parameters[i]) => c1) + + // ...and in positions 0..i, there are no downstream parameters. (let assumptions = c1.substitution().apply(&assumptions)) (let goal = c1.substitution().apply(&goal)) - (for_all(&decls, &env, &assumptions, &goal.parameters[..i], ¬_downstream) => c2) + (for_all(&decls, &env, &assumptions, &goal.parameters[..i], &is_not_downstream) => c2) --- ("local parameter") (is_local_trait_ref(decls, env, assumptions, goal) => c1.seq(c2)) ) @@ -85,14 +230,14 @@ judgment_fn! { } judgment_fn! { - /// "not_downstream(..., P)" means that `P` cannot be instantiated with a type from + /// `is_not_downstream(..., P)` means that `P` cannot be instantiated with a type from /// a downstream crate (i.e., a crate that has us as a dependency). /// /// NB. Since RFC 2451, the judgment applies to the outermost type only. In other words, /// the judgment holds for (e.g.) `Vec`, which could be instantiated /// with something like `Vec`, but that is not considered downstream /// as the outermost type (`Vec`) is upstream. - fn not_downstream( + fn is_not_downstream( decls: Decls, env: Env, assumptions: Wcs, @@ -104,20 +249,20 @@ judgment_fn! { // Since https://rust-lang.github.io/rfcs/2451-re-rebalancing-coherence.html, // any rigid type is adequate. --- ("rigid") - (not_downstream(_decls, env, _assumptions, RigidTy { .. }) => Constraints::none(env)) + (is_not_downstream(_decls, env, _assumptions, RigidTy { .. }) => Constraints::none(env)) ) ( // Lifetimes are not relevant. --- ("lifetime") - (not_downstream(_decls, env, _assumptions, _l: Lt) => Constraints::none(env)) + (is_not_downstream(_decls, env, _assumptions, _l: Lt) => Constraints::none(env)) ) ( // existential variables *could* be inferred to downstream types; depends on the substitution // we ultimately have. --- ("type variable") - (not_downstream(_decls, env, _assumptions, TyData::Variable(Variable::ExistentialVar(_))) => Constraints::none(env).ambiguous()) + (is_not_downstream(_decls, env, _assumptions, TyData::Variable(Variable::ExistentialVar(_))) => Constraints::none(env).ambiguous()) ) } } diff --git a/crates/formality-prove/src/prove/prove_eq.rs b/crates/formality-prove/src/prove/prove_eq.rs index fe991476..23c9d6e0 100644 --- a/crates/formality-prove/src/prove/prove_eq.rs +++ b/crates/formality-prove/src/prove/prove_eq.rs @@ -165,7 +165,7 @@ fn equate_variable( // For each universal variable that we replaced with an existential variable // above, we now have to prove that goal. e.g., if we had `X = Vec`, we would replace `!Y` with `?Z` // (where `?Z` is in a lower universe than `X`), but now we must prove that `!Y = ?Z` - // (this may be posible due to assumptions). + // (this may be possible due to assumptions). let goals: Wcs = universe_subst .iter() .filter(|(v, _)| v.is_a::()) diff --git a/crates/formality-prove/src/prove/prove_wc.rs b/crates/formality-prove/src/prove/prove_wc.rs index 3d63afdf..f51e55cb 100644 --- a/crates/formality-prove/src/prove/prove_wc.rs +++ b/crates/formality-prove/src/prove/prove_wc.rs @@ -61,9 +61,9 @@ judgment_fn! { ( (if env.is_in_coherence_mode())! - (may_be_remote(decls, env, assumptions, trait_ref) => c) + (may_be_remote(decls, &env, assumptions, trait_ref) => ()) ----------------------------- ("coherence / remote impl") - (prove_wc(decls, env, assumptions, Predicate::IsImplemented(trait_ref)) => c.ambiguous()) + (prove_wc(decls, env, assumptions, Predicate::IsImplemented(trait_ref)) => Constraints::none(&env).ambiguous()) ) ( diff --git a/crates/formality-types/src/grammar/formulas.rs b/crates/formality-types/src/grammar/formulas.rs index 68f199dc..a750f806 100644 --- a/crates/formality-types/src/grammar/formulas.rs +++ b/crates/formality-types/src/grammar/formulas.rs @@ -31,6 +31,14 @@ pub enum Predicate { #[grammar(@WellFormedTraitRef($v0))] WellFormedTraitRef(TraitRef), + /// A trait-ref **is local** if the local crate could legally implement it for all + /// possible instantiations of the variables within. + /// + /// Example: + /// + /// * `T: SomeLocalTrait` is local for all `T` since the local crate could create a blanket impl + /// * `LocalType: SomeRemoteTrait` is local + /// * `RemoteType: SomeRemoteTrait` is not local #[grammar(@IsLocal($v0))] IsLocal(TraitRef), @@ -149,6 +157,8 @@ impl TraitRef { Predicate::WellFormedTraitRef(self.clone()) } + /// A trait-ref **is local** if the local crate could legally implement it + /// (and not via a blanket impl). pub fn is_local(&self) -> Predicate { Predicate::IsLocal(self.clone()) } @@ -205,10 +215,10 @@ impl TraitId { /// We need a better name for this lol. #[term] pub enum PR { - #[cast] - Predicate(Predicate), #[cast] Relation(Relation), + #[cast] + Predicate(Predicate), } impl PR { diff --git a/src/lib.rs b/src/lib.rs index 491d3bdd..1442d53b 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -7,6 +7,9 @@ use formality_prove::{test_util::TestAssertion, Constraints}; use formality_rust::grammar::Program; use formality_types::rust::try_term; +#[cfg(test)] +mod test; + #[derive(Parser, Debug)] #[command(author, version, about, long_about = None)] struct Args { @@ -40,6 +43,22 @@ pub fn main() -> anyhow::Result<()> { check_all_crates(&program) } +#[macro_export] +macro_rules! assert_ok { + ($input:tt $expect:expr) => {{ + use formality_core::test_util::ResultTestExt; + $crate::test_program_ok(stringify!($input)).assert_ok($expect); + }}; +} + +#[macro_export] +macro_rules! assert_err { + ($input:tt [$($must_have:expr,)*] $expect:expr) => {{ + use formality_core::test_util::ResultTestExt; + $crate::test_program_ok(stringify!($input)).assert_has_err($expect, &[$($must_have,)*]); + }}; +} + pub fn test_program_ok(input: &str) -> anyhow::Result<()> { let program: Program = try_term(input)?; check_all_crates(&program) diff --git a/src/test/coherence_orphan.rs b/src/test/coherence_orphan.rs new file mode 100644 index 00000000..a672dda1 --- /dev/null +++ b/src/test/coherence_orphan.rs @@ -0,0 +1,257 @@ +#![allow(non_snake_case)] + +#[test] +fn neg_CoreTrait_for_CoreStruct_in_Foo() { + crate::assert_err!( + [ + crate core { + trait CoreTrait {} + struct CoreStruct {} + }, + crate foo { + impl !CoreTrait for CoreStruct {} + } + ] + + [ /* TODO */ ] + + expect_test::expect![[r#" + orphan_check_neg(impl ! CoreTrait for CoreStruct {}) + + Caused by: + judgment `prove_wc_list { goal: {@ IsLocal(CoreTrait(CoreStruct))}, assumptions: {}, env: Env { variables: [], coherence_mode: true }, decls: decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: @ IsLocal(CoreTrait(CoreStruct)), assumptions: {}, env: Env { variables: [], coherence_mode: true }, decls: decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): + the rule "trait ref is local" failed at step #0 (src/file.rs:LL:CC) because + judgment `is_local_trait_ref { goal: CoreTrait(CoreStruct), assumptions: {}, env: Env { variables: [], coherence_mode: true }, decls: decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): + the rule "local parameter" failed at step #1 (src/file.rs:LL:CC) because + judgment `is_local_parameter { goal: CoreStruct, assumptions: {}, env: Env { variables: [], coherence_mode: true }, decls: decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): + the rule "fundamental rigid type" failed at step #0 (src/file.rs:LL:CC) because + condition evaluted to false: `is_fundamental(&decls, &name)` + &decls = decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], {}, {}) + &name = (adt CoreStruct) + the rule "local rigid type" failed at step #0 (src/file.rs:LL:CC) because + condition evaluted to false: `decls.is_local_adt_id(&a)` + decls = decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], {}, {}) + &a = CoreStruct + the rule "local trait" failed at step #0 (src/file.rs:LL:CC) because + condition evaluted to false: `decls.is_local_trait_id(&goal.trait_id)` + decls = decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], {}, {}) + &goal.trait_id = CoreTrait"#]] + ) +} + +#[test] +fn mirror_CoreStruct() { + crate::assert_err!( + [ + crate core { + trait CoreTrait {} + struct CoreStruct {} + + trait Mirror { + type Assoc : []; + } + + impl Mirror for T { + type Assoc = T; + } + }, + crate foo { + impl CoreTrait for ::Assoc {} + } + ] + + [ /* TODO */ ] + + expect_test::expect![[r#" + orphan_check(impl CoreTrait for ::Assoc { }) + + Caused by: + judgment `prove_wc_list { goal: {@ IsLocal(CoreTrait(::Assoc))}, assumptions: {}, env: Env { variables: [], coherence_mode: true }, decls: decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: @ IsLocal(CoreTrait(::Assoc)), assumptions: {}, env: Env { variables: [], coherence_mode: true }, decls: decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): + the rule "trait ref is local" failed at step #0 (src/file.rs:LL:CC) because + judgment `is_local_trait_ref { goal: CoreTrait(::Assoc), assumptions: {}, env: Env { variables: [], coherence_mode: true }, decls: decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): + the rule "local parameter" failed at step #1 (src/file.rs:LL:CC) because + judgment `is_local_parameter { goal: ::Assoc, assumptions: {}, env: Env { variables: [], coherence_mode: true }, decls: decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): + the rule "local parameter" failed at step #3 (src/file.rs:LL:CC) because + judgment `is_local_parameter { goal: CoreStruct, assumptions: {}, env: Env { variables: [], coherence_mode: true }, decls: decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): + the rule "fundamental rigid type" failed at step #0 (src/file.rs:LL:CC) because + condition evaluted to false: `is_fundamental(&decls, &name)` + &decls = decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], {}, {}) + &name = (adt CoreStruct) + the rule "local rigid type" failed at step #0 (src/file.rs:LL:CC) because + condition evaluted to false: `decls.is_local_adt_id(&a)` + decls = decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], {}, {}) + &a = CoreStruct + the rule "local trait" failed at step #0 (src/file.rs:LL:CC) because + condition evaluted to false: `decls.is_local_trait_id(&goal.trait_id)` + decls = decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], {}, {}) + &goal.trait_id = CoreTrait"#]] + ) +} + +#[test] +fn mirror_FooStruct() { + crate::assert_ok!( + //@check-pass + [ + crate core { + trait CoreTrait {} + + trait Mirror { + type Assoc : []; + } + + impl Mirror for T { + type Assoc = T; + } + }, + crate foo { + struct FooStruct {} + impl CoreTrait for ::Assoc {} + } + ] + + expect_test::expect!["()"] + ) +} + +#[test] +fn covered_VecT() { + crate::assert_ok!( + //@check-pass + [ + crate core { + trait CoreTrait {} + struct Vec {} + }, + crate foo { + struct FooStruct {} + impl CoreTrait for Vec {} + } + ] + + expect_test::expect!["()"] + ) +} + +#[test] +fn uncovered_T() { + crate::assert_err!( + [ + crate core { + trait CoreTrait {} + }, + crate foo { + struct FooStruct {} + impl CoreTrait for T {} + } + ] + + [ /* TODO */ ] + + expect_test::expect![[r#" + orphan_check(impl CoreTrait for ^ty0_0 { }) + + Caused by: + judgment `prove_wc_list { goal: {@ IsLocal(CoreTrait(!ty_0, FooStruct))}, assumptions: {}, env: Env { variables: [!ty_0], coherence_mode: true }, decls: decls(222, [trait CoreTrait ], [impl CoreTrait(^ty0_0, FooStruct)], [], [], [], [adt FooStruct ], {}, {FooStruct}) }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: @ IsLocal(CoreTrait(!ty_0, FooStruct)), assumptions: {}, env: Env { variables: [!ty_0], coherence_mode: true }, decls: decls(222, [trait CoreTrait ], [impl CoreTrait(^ty0_0, FooStruct)], [], [], [], [adt FooStruct ], {}, {FooStruct}) }` failed at the following rule(s): + the rule "trait ref is local" failed at step #0 (src/file.rs:LL:CC) because + judgment `is_local_trait_ref { goal: CoreTrait(!ty_0, FooStruct), assumptions: {}, env: Env { variables: [!ty_0], coherence_mode: true }, decls: decls(222, [trait CoreTrait ], [impl CoreTrait(^ty0_0, FooStruct)], [], [], [], [adt FooStruct ], {}, {FooStruct}) }` failed at the following rule(s): + the rule "local trait" failed at step #0 (src/file.rs:LL:CC) because + condition evaluted to false: `decls.is_local_trait_id(&goal.trait_id)` + decls = decls(222, [trait CoreTrait ], [impl CoreTrait(^ty0_0, FooStruct)], [], [], [], [adt FooStruct ], {}, {FooStruct}) + &goal.trait_id = CoreTrait"#]] + ) +} + +#[test] +fn alias_to_unit() { + crate::assert_err!( + [ + crate core { + trait CoreTrait {} + + trait Unit { + type Assoc : []; + } + + impl Unit for T { + type Assoc = (); + } + }, + crate foo { + struct FooStruct {} + impl CoreTrait for ::Assoc {} + } + ] + + [ /* TODO */ ] + + expect_test::expect![[r#" + orphan_check(impl CoreTrait for ::Assoc { }) + + Caused by: + judgment `prove_wc_list { goal: {@ IsLocal(CoreTrait(::Assoc))}, assumptions: {}, env: Env { variables: [], coherence_mode: true }, decls: decls(222, [trait CoreTrait , trait Unit ], [impl Unit(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Unit>::Assoc = ()], [], [adt FooStruct ], {}, {FooStruct}) }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: @ IsLocal(CoreTrait(::Assoc)), assumptions: {}, env: Env { variables: [], coherence_mode: true }, decls: decls(222, [trait CoreTrait , trait Unit ], [impl Unit(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Unit>::Assoc = ()], [], [adt FooStruct ], {}, {FooStruct}) }` failed at the following rule(s): + the rule "trait ref is local" failed at step #0 (src/file.rs:LL:CC) because + judgment `is_local_trait_ref { goal: CoreTrait(::Assoc), assumptions: {}, env: Env { variables: [], coherence_mode: true }, decls: decls(222, [trait CoreTrait , trait Unit ], [impl Unit(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Unit>::Assoc = ()], [], [adt FooStruct ], {}, {FooStruct}) }` failed at the following rule(s): + the rule "local parameter" failed at step #1 (src/file.rs:LL:CC) because + judgment `is_local_parameter { goal: ::Assoc, assumptions: {}, env: Env { variables: [], coherence_mode: true }, decls: decls(222, [trait CoreTrait , trait Unit ], [impl Unit(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Unit>::Assoc = ()], [], [adt FooStruct ], {}, {FooStruct}) }` failed at the following rule(s): + the rule "local parameter" failed at step #3 (src/file.rs:LL:CC) because + judgment `is_local_parameter { goal: (), assumptions: {}, env: Env { variables: [], coherence_mode: true }, decls: decls(222, [trait CoreTrait , trait Unit ], [impl Unit(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Unit>::Assoc = ()], [], [adt FooStruct ], {}, {FooStruct}) }` failed at the following rule(s): + the rule "fundamental rigid type" failed at step #0 (src/file.rs:LL:CC) because + condition evaluted to false: `is_fundamental(&decls, &name)` + &decls = decls(222, [trait CoreTrait , trait Unit ], [impl Unit(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Unit>::Assoc = ()], [], [adt FooStruct ], {}, {FooStruct}) + &name = tuple(0) + the rule "local trait" failed at step #0 (src/file.rs:LL:CC) because + condition evaluted to false: `decls.is_local_trait_id(&goal.trait_id)` + decls = decls(222, [trait CoreTrait , trait Unit ], [impl Unit(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Unit>::Assoc = ()], [], [adt FooStruct ], {}, {FooStruct}) + &goal.trait_id = CoreTrait"#]] + ) +} + +#[test] +fn CoreTrait_for_CoreStruct_in_Foo() { + crate::assert_err!( + [ + crate core { + trait CoreTrait {} + struct CoreStruct {} + }, + crate foo { + impl CoreTrait for CoreStruct {} + } + ] + + [ /* TODO */ ] + + expect_test::expect![[r#" + orphan_check(impl CoreTrait for CoreStruct { }) + + Caused by: + judgment `prove_wc_list { goal: {@ IsLocal(CoreTrait(CoreStruct))}, assumptions: {}, env: Env { variables: [], coherence_mode: true }, decls: decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: @ IsLocal(CoreTrait(CoreStruct)), assumptions: {}, env: Env { variables: [], coherence_mode: true }, decls: decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): + the rule "trait ref is local" failed at step #0 (src/file.rs:LL:CC) because + judgment `is_local_trait_ref { goal: CoreTrait(CoreStruct), assumptions: {}, env: Env { variables: [], coherence_mode: true }, decls: decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): + the rule "local parameter" failed at step #1 (src/file.rs:LL:CC) because + judgment `is_local_parameter { goal: CoreStruct, assumptions: {}, env: Env { variables: [], coherence_mode: true }, decls: decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): + the rule "fundamental rigid type" failed at step #0 (src/file.rs:LL:CC) because + condition evaluted to false: `is_fundamental(&decls, &name)` + &decls = decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], {}, {}) + &name = (adt CoreStruct) + the rule "local rigid type" failed at step #0 (src/file.rs:LL:CC) because + condition evaluted to false: `decls.is_local_adt_id(&a)` + decls = decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], {}, {}) + &a = CoreStruct + the rule "local trait" failed at step #0 (src/file.rs:LL:CC) because + condition evaluted to false: `decls.is_local_trait_id(&goal.trait_id)` + decls = decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], {}, {}) + &goal.trait_id = CoreTrait"#]] + ) +} \ No newline at end of file diff --git a/src/test/coherence_overlap.rs b/src/test/coherence_overlap.rs new file mode 100644 index 00000000..2aab654b --- /dev/null +++ b/src/test/coherence_overlap.rs @@ -0,0 +1,277 @@ +#![allow(non_snake_case)] + +use formality_core::test; + +#[test] +fn u32_not_u32_impls() { + crate::assert_err!( + // Test that a positive and negative impl for the same type (`u32`, here) is rejected. + [ + crate core { + trait Foo {} + impl Foo for u32 {} + impl !Foo for u32 {} + } + ] + + [ + "check_trait_impl", + "impl Foo for u32", + ] + + expect_test::expect![[r#" + check_trait_impl(impl Foo for u32 { }) + + Caused by: + failed to disprove + {! Foo(u32)} + given + {} + got + {Constraints { env: Env { variables: [], coherence_mode: false }, known_true: true, substitution: {} }}"#]] + ) +} + +#[test] +fn neg_CoreTrait_for_CoreStruct_implies_no_overlap() { + crate::assert_ok!( + //@check-pass + // Variant of foo_crate_cannot_assume_CoreStruct_does_not_impl_CoreTrait + // where there is a negative impl, so it is accepted. + [ + crate core { + trait CoreTrait {} + struct CoreStruct {} + impl !CoreTrait for CoreStruct {} + }, + crate foo { + trait FooTrait {} + impl FooTrait for T where T: CoreTrait {} + impl FooTrait for CoreStruct {} + } + ] + + expect_test::expect!["()"] + ) +} + +#[test] +fn foo_crate_cannot_assume_CoreStruct_does_not_impl_CoreTrait() { + crate::assert_err!( + [ + crate core { + trait CoreTrait {} + struct CoreStruct {} + }, + crate foo { + trait FooTrait {} + impl FooTrait for T where T: CoreTrait {} + impl FooTrait for CoreStruct {} + } + ] + + [ + "impls may overlap", + ] + + expect_test::expect![[r#" + impls may overlap: + impl FooTrait for ^ty0_0 where ^ty0_0 : CoreTrait { } + impl FooTrait for CoreStruct { }"#]] + ) +} + +#[test] +fn T_where_Foo_not_u32_impls() { + crate::assert_err!( + // Test positive impl that has a where-clause which checks for itself, + // i.e., `T: Foo where T: Foo`. This `T: Foo` where-clause isn't harmful + // in the coinductive interpretation of trait matching, it actually + // doesn't change the meaning of the impl at all. However, this formulation + // was erroneously accepted by an earlier variant of negative impls. + [ + crate core { + trait Foo {} + impl Foo for T where T: Foo {} + impl !Foo for u32 {} + } + ] + + [ + "check_trait_impl", + "Foo for ^ty0_0", + ] + + expect_test::expect![[r#" + check_trait_impl(impl Foo for ^ty0_0 where ^ty0_0 : Foo { }) + + Caused by: + failed to disprove + {! Foo(!ty_1)} + given + {Foo(!ty_1)} + got + {Constraints { env: Env { variables: [?ty_1], coherence_mode: false }, known_true: true, substitution: {?ty_1 => u32} }}"#]] + ) +} + +#[test] +fn u32_T_where_T_Is_impls() { + crate::assert_err!( + // Test that we detect "indirect" overlap -- here `Foo` is implemented for `u32` + // and also all `T: Is`, and `u32: Is`. + [ + crate core { + trait Foo {} + impl Foo for u32 {} + impl Foo for T where T: Is {} + + trait Is {} + impl Is for u32 {} + } + ] + + [ + "impls may overlap", + ] + + expect_test::expect![[r#" + impls may overlap: + impl Foo for u32 { } + impl Foo for ^ty0_0 where ^ty0_0 : Is { }"#]] + ) +} + +#[test] +fn u32_T_where_T_Not_impls() { + crate::assert_ok!( + //@check-pass + + // Test that, within a crate, we are able to rely on the fact + // that `u32: Not` is not implemented. + // + // See also test_foo_crate_cannot_assume_CoreStruct_does_not_impl_CoreTrait + [ + crate core { + trait Foo {} + impl Foo for u32 {} + impl Foo for T where T: Not {} + + trait Not {} + } + ] + + expect_test::expect!["()"] + ) +} + +#[test] +fn u32_u32_impls() { + crate::assert_err!( + [ + crate core { + trait Foo {} + impl Foo for u32 {} + impl Foo for u32 {} + } + ] + + [ + "duplicate impl", + ] + + expect_test::expect!["duplicate impl in current crate: impl Foo for u32 { }"] + ) +} + +#[test] +fn u32_i32_impls() { + crate::assert_ok!( + //@check-pass + [ + crate core { + trait Foo {} + impl Foo for u32 {} + impl Foo for i32 {} + } + ] + + expect_test::expect!["()"] + ) +} + +#[test] +fn u32_T_impls() { + crate::assert_err!( + [ + crate core { + trait Foo {} + impl Foo for u32 {} + impl Foo for T {} + } + ] + + [ + "impls may overlap", + ] + + expect_test::expect![[r#" + impls may overlap: + impl Foo for u32 { } + impl Foo for ^ty0_0 { }"#]] + ) +} + +#[test] +fn T_and_T_bar() { + crate::assert_err! { + [ + crate core { + trait Foo { } + + trait Bar { } + + impl Foo for T { } + + impl Foo for T where T: Bar { } + } + ] + + [ + "impls may overlap", + ] + + expect_test::expect![[r#" + impls may overlap: + impl Foo for ^ty0_0 { } + impl Foo for ^ty0_0 where ^ty0_0 : Bar { }"#]] + } +} + +#[test] +fn T_and_Local_Bar_T() { + crate::assert_err! { + [ + crate core { + trait Foo { } + + trait Bar { } + + impl Foo for T { } + + impl Foo for T where LocalType: Bar { } + + struct LocalType { } + } + ] + + [ + "impls may overlap", + ] + + expect_test::expect![[r#" + impls may overlap: + impl Foo for ^ty0_0 { } + impl Foo for ^ty0_0 where LocalType : Bar <^ty0_0> { }"#]] + } +} diff --git a/src/test/consts.rs b/src/test/consts.rs new file mode 100644 index 00000000..36a8488f --- /dev/null +++ b/src/test/consts.rs @@ -0,0 +1,166 @@ +#![allow(non_snake_case)] + +#[test] +fn nonsense_rigid_const_bound() { + crate::assert_err!( + // This test is the short version of `generic_mismatch`, skipping + // substituting and directly going to a wrong constant. + [ + crate Foo { + trait Foo where type_of_const true is u32 {} + } + ] + + [ /* TODO */ ] + + expect_test::expect![[r#" + check_trait(Foo) + + Caused by: + 0: prove_where_clause_well_formed(type_of_const value(0, bool) is u32) + 1: judgment `prove_wc_list { goal: {u32 = bool}, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: u32 = bool, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): + the rule "assumption" failed at step #1 (src/file.rs:LL:CC) because + judgment had no applicable rules: `prove_via { goal: u32 = bool, via: @ ConstHasType(value(0, bool) , u32), assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` + the rule "eq" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_eq { a: u32, b: bool, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): + the rule "normalize-l" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_normalize { p: u32, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): + the rule "normalize-via-assumption" failed at step #1 (src/file.rs:LL:CC) because + judgment had no applicable rules: `prove_normalize_via { goal: u32, via: @ ConstHasType(value(0, bool) , u32), assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` + the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_eq { a: bool, b: u32, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): + the rule "normalize-l" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_normalize { p: bool, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): + the rule "normalize-via-assumption" failed at step #1 (src/file.rs:LL:CC) because + judgment had no applicable rules: `prove_normalize_via { goal: bool, via: @ ConstHasType(value(0, bool) , u32), assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` + the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because + cyclic proof attempt: `prove_eq { a: u32, b: bool, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }`"#]] + ) +} + +#[test] +fn ok() { + crate::assert_ok!( + //@check-pass + [ + crate Foo { + trait Foo where type_of_const C is bool {} + trait Bar where type_of_const C is u32 {} + + impl Foo for u32 where type_of_const C is bool {} + } + ] + + expect_test::expect!["()"] + ) +} + +#[test] +fn mismatch() { + crate::assert_err!( + [ + crate Foo { + trait Foo where type_of_const C is bool {} + + impl Foo for u32 {} + } + ] + + [ /* TODO */ ] + + expect_test::expect![[r#" + check_trait_impl(impl Foo for u32 { }) + + Caused by: + judgment `prove_wc_list { goal: {Foo(u32, const value(42, u32))}, assumptions: {}, env: Env { variables: [], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}], [impl Foo(u32, const value(42, u32))], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: Foo(u32, const value(42, u32)), assumptions: {}, env: Env { variables: [], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}], [impl Foo(u32, const value(42, u32))], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): + the rule "trait implied bound" failed at step #0 (src/file.rs:LL:CC) because + expression evaluated to an empty collection: `decls.trait_invariants()`"#]] + ) +} + +#[test] +fn holds() { + crate::assert_ok!( + //@check-pass + [ + crate Foo { + trait Foo where type_of_const C is bool {} + + impl Foo for u32 {} + } + ] + + expect_test::expect!["()"] + ) +} + +#[test] +fn rigid_const_bound() { + crate::assert_ok!( + // This test is the short version of `holds`, skipping + // substituting and directly going to a rigid constant. + //@check-pass + [ + crate Foo { + trait Foo where type_of_const true is bool {} + } + ] + + expect_test::expect!["()"] + ) +} + +#[test] +fn generic_mismatch() { + crate::assert_err!( + [ + crate Foo { + trait Foo where type_of_const C is bool {} + + impl Foo for u32 where type_of_const C is u32 {} + } + ] + + [ /* TODO */ ] + + expect_test::expect![[r#" + check_trait_impl(impl Foo for u32 where type_of_const ^const0_0 is u32 { }) + + Caused by: + judgment `prove_wc_list { goal: {Foo(u32, const !const_0)}, assumptions: {@ ConstHasType(!const_0 , u32)}, env: Env { variables: [!const_0], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}], [impl Foo(u32, const ^const0_0) where {@ ConstHasType(^const0_0 , u32)}], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: Foo(u32, const !const_0), assumptions: {@ ConstHasType(!const_0 , u32)}, env: Env { variables: [!const_0], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}], [impl Foo(u32, const ^const0_0) where {@ ConstHasType(^const0_0 , u32)}], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): + the rule "positive impl" failed at step #7 (src/file.rs:LL:CC) because + judgment `prove_after { constraints: Constraints { env: Env { variables: [!const_0, ?const_1], coherence_mode: false }, known_true: true, substitution: {?const_1 => const !const_0} }, goal: {@ ConstHasType(?const_1 , bool)}, assumptions: {@ ConstHasType(!const_0 , u32)}, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}], [impl Foo(u32, const ^const0_0) where {@ ConstHasType(^const0_0 , u32)}], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): + the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {@ ConstHasType(!const_0 , bool)}, assumptions: {@ ConstHasType(!const_0 , u32)}, env: Env { variables: [!const_0], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}], [impl Foo(u32, const ^const0_0) where {@ ConstHasType(^const0_0 , u32)}], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: @ ConstHasType(!const_0 , bool), assumptions: {@ ConstHasType(!const_0 , u32)}, env: Env { variables: [!const_0], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}], [impl Foo(u32, const ^const0_0) where {@ ConstHasType(^const0_0 , u32)}], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): + the rule "const has ty" failed at step #0 (src/file.rs:LL:CC) because + pattern `Some((_, const_ty))` did not match value `None` + the rule "trait implied bound" failed at step #0 (src/file.rs:LL:CC) because + expression evaluated to an empty collection: `decls.trait_invariants()`"#]] + ) +} + +#[test] +fn multiple_type_of_const() { + crate::assert_ok!( + // This test is weird, but it's also not something rustc ever generates. + // Types on const generics only get exactly one `type_of_const` bound. + // Either way, it is still sound, because there is no constant that possibly + // satisfies those bounds (similar to how there is no type that satisfies `Drop` + `Copy`). + //@check-pass + [ + crate Foo { + trait Foo where type_of_const C is bool, type_of_const C is u32 {} + } + ] + + expect_test::expect!["()"] + ) +} \ No newline at end of file diff --git a/src/test/decl_safety.rs b/src/test/decl_safety.rs new file mode 100644 index 00000000..5c8a2175 --- /dev/null +++ b/src/test/decl_safety.rs @@ -0,0 +1,126 @@ +#![allow(non_snake_case)] + +#[test] +fn unsafe_trait() { + crate::assert_ok!( + //@check-pass + [ + crate baguette { + unsafe trait Foo {} + unsafe impl Foo for u32 {} + } + ] + + expect_test::expect!["()"] + ) +} + +#[test] +fn safe_trait() { + crate::assert_ok!( + //@check-pass + [ + crate baguette { + safe trait Foo {} + safe impl Foo for u32 {} + } + ] + + expect_test::expect!["()"] + ) +} + +#[test] +fn unsafe_trait_negative_impl() { + crate::assert_ok!( + //@check-pass + [ + crate baguette { + unsafe trait Foo {} + impl !Foo for u32 {} + } + ] + + expect_test::expect!["()"] + ) +} + +#[test] +fn unsafe_trait_negative_impl_mismatch() { + crate::assert_err!( + [ + crate baguette { + unsafe trait Foo {} + unsafe impl !Foo for u32 {} + } + ] + + [ /* TODO */ ] + + expect_test::expect![[r#" + check_neg_trait_impl(unsafe impl ! Foo for u32 {}) + + Caused by: + negative impls cannot be unsafe"#]] + ) +} + +#[test] +fn safe_trait_negative_impl_mismatch() { + crate::assert_err!( + [ + crate baguette { + trait Foo {} + unsafe impl !Foo for u32 {} + } + ] + + [ /* TODO */ ] + + expect_test::expect![[r#" + check_neg_trait_impl(unsafe impl ! Foo for u32 {}) + + Caused by: + negative impls cannot be unsafe"#]] + ) +} + +#[test] +fn unsafe_trait_mismatch() { + crate::assert_err!( + [ + crate baguette { + unsafe trait Foo {} + impl Foo for u32 {} + } + ] + + [ /* TODO */ ] + + expect_test::expect![[r#" + check_trait_impl(impl Foo for u32 { }) + + Caused by: + the trait `Foo` requires an `unsafe impl` declaration"#]] + ) +} + +#[test] +fn safe_trait_mismatch() { + crate::assert_err!( + [ + crate baguette { + trait Foo {} + unsafe impl Foo for u32 {} + } + ] + + [ /* TODO */ ] + + expect_test::expect![[r#" + check_trait_impl(unsafe impl Foo for u32 { }) + + Caused by: + implementing the trait `Foo` is not unsafe"#]] + ) +} \ No newline at end of file diff --git a/src/test/functions.rs b/src/test/functions.rs new file mode 100644 index 00000000..321ad434 --- /dev/null +++ b/src/test/functions.rs @@ -0,0 +1,51 @@ +#![allow(non_snake_case)] + +#[test] +fn ok() { + crate::assert_ok!( + // Test functions, function's arguments, and function's returns + //@check-pass + [ + crate Foo { + // fn simple_fn() {} + fn simple_fn() -> () { trusted } + + // fn one_arg(_: T) {} + fn one_arg(T) -> () { trusted } + + // fn one_ret(_: T) {} + fn one_ret() -> T { trusted } + + // fn arg_ret(_: T) -> U {} + fn arg_ret(T) -> U { trusted } + + // fn multi_arg_ret(_: T, _: Y) -> (U, I) {} + fn multi_arg_ret(T, Y) -> (U, I) { trusted } + } + ] + + expect_test::expect!["()"] + ) +} + +#[test] +fn lifetime() { + crate::assert_err!( + // Test lifetimes on function + [ + crate Foo { + // fn one_lt_arg<'a, T>(_: &'a T) -> () {} + fn one_lt_arg(&a T) -> () { trusted } + } + ] + + [ /* TODO */ ] + + expect_test::expect![[r#" + judgment `prove_wc_list { goal: {@ wf(&!lt_0 !ty_1)}, assumptions: {}, env: Env { variables: [!lt_0, !ty_1], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: @ wf(&!lt_0 !ty_1), assumptions: {}, env: Env { variables: [!lt_0, !ty_1], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + the rule "parameter well formed" failed at step #0 (src/file.rs:LL:CC) because + judgment had no applicable rules: `prove_wf { goal: &!lt_0 !ty_1, assumptions: {}, env: Env { variables: [!lt_0, !ty_1], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }`"#]] + ) +} \ No newline at end of file diff --git a/src/test/mod.rs b/src/test/mod.rs new file mode 100644 index 00000000..826675ed --- /dev/null +++ b/src/test/mod.rs @@ -0,0 +1,135 @@ +#![allow(non_snake_case)] + +mod coherence_orphan; +mod coherence_overlap; +mod functions; +mod decl_safety; +mod consts; + +#[test] +fn parser() { + crate::assert_err!( + [ + crate Foo { + trait Baz where cake {} + } + ] + + [ /* TODO */ ] + + expect_test::expect![[r#" + expected `:` + + Caused by: + 0: {} }] + 1: failed to parse [crate Foo { trait Baz where cake {} }]"#]] + ) +} + +#[test] +fn hello_world_fail() { + crate::assert_err!( + [ + crate Foo { + trait Foo where T: Bar {} + + trait Bar where T: Baz {} + + trait Baz {} + } + ] + + [ /* TODO */ ] + + expect_test::expect![[r#" + check_trait(Foo) + + Caused by: + 0: prove_where_clause_well_formed(!ty_2 : Bar ) + 1: judgment `prove_wc_list { goal: {@ WellFormedTraitRef(Bar(!ty_0, !ty_1))}, assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [trait Foo where {Bar(^ty0_1, ^ty0_0)}, trait Bar where {Baz(^ty0_1)}, trait Baz ], [], [], [], [], [], {Bar, Baz, Foo}, {}) }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: @ WellFormedTraitRef(Bar(!ty_0, !ty_1)), assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [trait Foo where {Bar(^ty0_1, ^ty0_0)}, trait Bar where {Baz(^ty0_1)}, trait Baz ], [], [], [], [], [], {Bar, Baz, Foo}, {}) }` failed at the following rule(s): + the rule "trait well formed" failed at step #2 (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {Baz(!ty_1)}, assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [trait Foo where {Bar(^ty0_1, ^ty0_0)}, trait Bar where {Baz(^ty0_1)}, trait Baz ], [], [], [], [], [], {Bar, Baz, Foo}, {}) }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: Baz(!ty_1), assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [trait Foo where {Bar(^ty0_1, ^ty0_0)}, trait Bar where {Baz(^ty0_1)}, trait Baz ], [], [], [], [], [], {Bar, Baz, Foo}, {}) }` failed at the following rule(s): + the rule "trait implied bound" failed at step #0 (src/file.rs:LL:CC) because + expression evaluated to an empty collection: `decls.trait_invariants()`"#]] + ) +} + +#[test] +fn hello_world() { + crate::assert_ok!( + //@check-pass + [ + crate Foo { + trait Foo where T: Bar, Self: Baz {} + + trait Bar where T: Baz {} + + trait Baz {} + + impl Baz for u32 {} + + impl Bar for u32 {} + impl Bar for () where T: Baz {} + } + ] + + expect_test::expect!["()"] + ) +} + +#[test] +fn basic_where_clauses_pass() { + crate::assert_ok!( + //@check-pass + [ + crate core { + trait A where T: B { } + + trait B { } + + trait WellFormed where for u32: A { } + + impl B for T {} + } + ] + + expect_test::expect!["()"] + ) +} + +#[test] +fn basic_where_clauses_fail() { + crate::assert_err!( + [ + crate core { + trait A where T: B { } + + trait B { } + + trait WellFormed where for u32: A { } + } + ] + + [ /* TODO */ ] + + expect_test::expect![[r#" + check_trait(WellFormed) + + Caused by: + 0: prove_where_clause_well_formed(for u32 : A <^ty0_0>) + 1: prove_where_clause_well_formed(u32 : A ) + 2: judgment `prove_wc_list { goal: {@ WellFormedTraitRef(A(u32, !ty_0))}, assumptions: {for A(u32, ^ty0_0)}, env: Env { variables: [!ty_0], coherence_mode: false }, decls: decls(222, [trait A where {B(^ty0_1)}, trait B , trait WellFormed where {for A(u32, ^ty0_0)}], [], [], [], [], [], {A, B, WellFormed}, {}) }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: @ WellFormedTraitRef(A(u32, !ty_0)), assumptions: {for A(u32, ^ty0_0)}, env: Env { variables: [!ty_0], coherence_mode: false }, decls: decls(222, [trait A where {B(^ty0_1)}, trait B , trait WellFormed where {for A(u32, ^ty0_0)}], [], [], [], [], [], {A, B, WellFormed}, {}) }` failed at the following rule(s): + the rule "trait well formed" failed at step #2 (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {B(!ty_0)}, assumptions: {for A(u32, ^ty0_0)}, env: Env { variables: [!ty_0], coherence_mode: false }, decls: decls(222, [trait A where {B(^ty0_1)}, trait B , trait WellFormed where {for A(u32, ^ty0_0)}], [], [], [], [], [], {A, B, WellFormed}, {}) }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: B(!ty_0), assumptions: {for A(u32, ^ty0_0)}, env: Env { variables: [!ty_0], coherence_mode: false }, decls: decls(222, [trait A where {B(^ty0_1)}, trait B , trait WellFormed where {for A(u32, ^ty0_0)}], [], [], [], [], [], {A, B, WellFormed}, {}) }` failed at the following rule(s): + the rule "trait implied bound" failed at step #0 (src/file.rs:LL:CC) because + expression evaluated to an empty collection: `decls.trait_invariants()`"#]] + ) +} \ No newline at end of file diff --git a/tests/coherence_overlap.rs b/tests/coherence_overlap.rs index 0bc3a15b..2be9a922 100644 --- a/tests/coherence_overlap.rs +++ b/tests/coherence_overlap.rs @@ -47,13 +47,11 @@ fn test_overlap_normalize_alias_to_LocalType() { // ...but it's an error if LocalType implements Iterator (figuring *this* out also // requires normalizing). - test_program_ok(&gen_program( - "impl Iterator for LocalType {}", - )).assert_err( + test_program_ok(&gen_program("impl Iterator for LocalType {}")).assert_err( expect_test::expect![[r#" impls may overlap: impl LocalTrait for ^ty0_0 where ^ty0_0 : Iterator { } - impl LocalTrait for ::T { }"#]] + impl LocalTrait for ::T { }"#]], ); } @@ -91,24 +89,20 @@ fn test_overlap_alias_not_normalizable() { BASE_PROGRAM.replace("ADDITIONAL", addl) }; - // ...you might expect an error here, because we have an impl for all `T` and another - // impl for all `T: Iterator`, but we don't flag it as one because - // Iterator is a local trait and we can see that nobody has implemented it... - // - // FIXME: rustc DOES flag an error here. I think this is because the trait solver - // refuses to solve `?X: Iterator`; we haven't implemented that rule and I haven't - // decided how to think about it. + // ...you get an error here, because a downstream crate could implement + // trait for some local type, in which case it would overlap. - test_program_ok(&gen_program("")).assert_ok(expect_test::expect!["()"]); + test_program_ok(&gen_program("")).assert_err(expect_test::expect![[r#" + impls may overlap: + impl LocalTrait for ^ty0_0 where ^ty0_0 : Iterator { } + impl LocalTrait for <^ty0_0 as Mirror>::T where ^ty0_0 : Mirror { }"#]]); - // ...as long as there is at least one Iterator impl, however, we do flag an error. + // ...and if there is at least one Iterator impl, we also flag an error. - test_program_ok(&gen_program( - "impl Iterator for u32 {}", - )).assert_err( - expect_test::expect![[r#" - impls may overlap: - impl LocalTrait for ^ty0_0 where ^ty0_0 : Iterator { } - impl LocalTrait for <^ty0_0 as Mirror>::T where ^ty0_0 : Mirror { }"#]] - ); // FIXME + test_program_ok(&gen_program("impl Iterator for u32 {}")).assert_err(expect_test::expect![[ + r#" + impls may overlap: + impl LocalTrait for ^ty0_0 where ^ty0_0 : Iterator { } + impl LocalTrait for <^ty0_0 as Mirror>::T where ^ty0_0 : Mirror { }"# + ]]); } diff --git a/tests/ui.rs b/tests/ui.rs deleted file mode 100644 index 171a3276..00000000 --- a/tests/ui.rs +++ /dev/null @@ -1,33 +0,0 @@ -use ui_test::clap::Parser; -use ui_test::color_eyre::Result; -use ui_test::*; - -fn main() -> Result<()> { - let mut config = Config::rustc("tests/ui"); - // Prevent ui_test from trying to query `formality` for the host platform name - config.host = Some("non of ya bizniz".into()); - config.program.program = "target/debug/a-mir-formality".into(); - config.mode = Mode::Fail { - require_patterns: false, - }; - - let args = Args::parse(); - let text = if args.quiet { - status_emitter::Text::quiet() - } else { - status_emitter::Text::verbose() - }; - if !args.check && std::env::var_os("GITHUB_ACTIONS").is_none() { - config.output_conflict_handling = OutputConflictHandling::Bless; - } - - run_tests_generic( - config, - args, - |path, args| { - path.extension().is_some_and(|ext| ext == "frs") && default_filter_by_arg(path, args) - }, - default_per_file_config, - (text, status_emitter::Gha:: { name: "ui".into() }), - ) -} diff --git a/tests/ui/basic_where_clauses_fail.frs b/tests/ui/basic_where_clauses_fail.frs deleted file mode 100644 index 93c779fb..00000000 --- a/tests/ui/basic_where_clauses_fail.frs +++ /dev/null @@ -1,9 +0,0 @@ -[ - crate core { - trait A where T: B { } - - trait B { } - - trait WellFormed where for u32: A { } - } -] diff --git a/tests/ui/basic_where_clauses_fail.stderr b/tests/ui/basic_where_clauses_fail.stderr deleted file mode 100644 index c6b2630e..00000000 --- a/tests/ui/basic_where_clauses_fail.stderr +++ /dev/null @@ -1,14 +0,0 @@ -Error: check_trait(WellFormed) - -Caused by: - 0: prove_where_clause_well_formed(for u32 : A <^ty0_0>) - 1: prove_where_clause_well_formed(u32 : A ) - 2: judgment `prove_wc_list { goal: {@ WellFormedTraitRef(A(u32, !ty_0))}, assumptions: {for A(u32, ^ty0_0)}, env: Env { variables: [!ty_0], coherence_mode: false }, decls: decls(222, [trait A where {B(^ty0_1)}, trait B , trait WellFormed where {for A(u32, ^ty0_0)}], [], [], [], [], [], {A, B, WellFormed}, {}) }` failed at the following rule(s): - the rule "some" failed at step #0 (crates/formality-prove/src/prove/prove_wc_list.rs:28:14) because - judgment `prove_wc { goal: @ WellFormedTraitRef(A(u32, !ty_0)), assumptions: {for A(u32, ^ty0_0)}, env: Env { variables: [!ty_0], coherence_mode: false }, decls: decls(222, [trait A where {B(^ty0_1)}, trait B , trait WellFormed where {for A(u32, ^ty0_0)}], [], [], [], [], [], {A, B, WellFormed}, {}) }` failed at the following rule(s): - the rule "trait well formed" failed at step #2 (crates/formality-prove/src/prove/prove_wc.rs:104:14) because - judgment `prove_wc_list { goal: {B(!ty_0)}, assumptions: {for A(u32, ^ty0_0)}, env: Env { variables: [!ty_0], coherence_mode: false }, decls: decls(222, [trait A where {B(^ty0_1)}, trait B , trait WellFormed where {for A(u32, ^ty0_0)}], [], [], [], [], [], {A, B, WellFormed}, {}) }` failed at the following rule(s): - the rule "some" failed at step #0 (crates/formality-prove/src/prove/prove_wc_list.rs:28:14) because - judgment `prove_wc { goal: B(!ty_0), assumptions: {for A(u32, ^ty0_0)}, env: Env { variables: [!ty_0], coherence_mode: false }, decls: decls(222, [trait A where {B(^ty0_1)}, trait B , trait WellFormed where {for A(u32, ^ty0_0)}], [], [], [], [], [], {A, B, WellFormed}, {}) }` failed at the following rule(s): - the rule "trait implied bound" failed at step #0 (crates/formality-prove/src/prove/prove_wc.rs:86:14) because - expression evaluated to an empty collection: `decls.trait_invariants()` diff --git a/tests/ui/basic_where_clauses_pass.frs b/tests/ui/basic_where_clauses_pass.frs deleted file mode 100644 index b30eadcd..00000000 --- a/tests/ui/basic_where_clauses_pass.frs +++ /dev/null @@ -1,12 +0,0 @@ -//@check-pass -[ - crate core { - trait A where T: B { } - - trait B { } - - trait WellFormed where for u32: A { } - - impl B for T {} - } -] diff --git a/tests/ui/coherence_orphan/CoreTrait_for_CoreStruct_in_Foo.frs b/tests/ui/coherence_orphan/CoreTrait_for_CoreStruct_in_Foo.frs deleted file mode 100644 index 7700102d..00000000 --- a/tests/ui/coherence_orphan/CoreTrait_for_CoreStruct_in_Foo.frs +++ /dev/null @@ -1,9 +0,0 @@ -[ - crate core { - trait CoreTrait {} - struct CoreStruct {} - }, - crate foo { - impl CoreTrait for CoreStruct {} - } -] diff --git a/tests/ui/coherence_orphan/CoreTrait_for_CoreStruct_in_Foo.stderr b/tests/ui/coherence_orphan/CoreTrait_for_CoreStruct_in_Foo.stderr deleted file mode 100644 index 034ac2ad..00000000 --- a/tests/ui/coherence_orphan/CoreTrait_for_CoreStruct_in_Foo.stderr +++ /dev/null @@ -1,22 +0,0 @@ -Error: orphan_check(impl CoreTrait for CoreStruct { }) - -Caused by: - judgment `prove_wc_list { goal: {@ IsLocal(CoreTrait(CoreStruct))}, assumptions: {}, env: Env { variables: [], coherence_mode: true }, decls: decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): - the rule "some" failed at step #0 (crates/formality-prove/src/prove/prove_wc_list.rs:28:14) because - judgment `prove_wc { goal: @ IsLocal(CoreTrait(CoreStruct)), assumptions: {}, env: Env { variables: [], coherence_mode: true }, decls: decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): - the rule "trait ref is local" failed at step #0 (crates/formality-prove/src/prove/prove_wc.rs:110:14) because - judgment `is_local_trait_ref { goal: CoreTrait(CoreStruct), assumptions: {}, env: Env { variables: [], coherence_mode: true }, decls: decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): - the rule "local parameter" failed at step #1 (crates/formality-prove/src/prove/is_local.rs:77:14) because - judgment `is_local_parameter { goal: CoreStruct, assumptions: {}, env: Env { variables: [], coherence_mode: true }, decls: decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): - the rule "fundamental rigid type" failed at step #0 (crates/formality-prove/src/prove/is_local.rs:148:17) because - condition evaluted to false: `is_fundamental(&decls, &name)` - &decls = decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], {}, {}) - &name = (adt CoreStruct) - the rule "local rigid type" failed at step #0 (crates/formality-prove/src/prove/is_local.rs:156:17) because - condition evaluted to false: `decls.is_local_adt_id(&a)` - decls = decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], {}, {}) - &a = CoreStruct - the rule "local trait" failed at step #0 (crates/formality-prove/src/prove/is_local.rs:70:17) because - condition evaluted to false: `decls.is_local_trait_id(&goal.trait_id)` - decls = decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], {}, {}) - &goal.trait_id = CoreTrait diff --git a/tests/ui/coherence_orphan/alias_to_unit.frs b/tests/ui/coherence_orphan/alias_to_unit.frs deleted file mode 100644 index 31bb5744..00000000 --- a/tests/ui/coherence_orphan/alias_to_unit.frs +++ /dev/null @@ -1,17 +0,0 @@ -[ - crate core { - trait CoreTrait {} - - trait Unit { - type Assoc : []; - } - - impl Unit for T { - type Assoc = (); - } - }, - crate foo { - struct FooStruct {} - impl CoreTrait for ::Assoc {} - } -] diff --git a/tests/ui/coherence_orphan/alias_to_unit.stderr b/tests/ui/coherence_orphan/alias_to_unit.stderr deleted file mode 100644 index c7493056..00000000 --- a/tests/ui/coherence_orphan/alias_to_unit.stderr +++ /dev/null @@ -1,20 +0,0 @@ -Error: orphan_check(impl CoreTrait for ::Assoc { }) - -Caused by: - judgment `prove_wc_list { goal: {@ IsLocal(CoreTrait(::Assoc))}, assumptions: {}, env: Env { variables: [], coherence_mode: true }, decls: decls(222, [trait CoreTrait , trait Unit ], [impl Unit(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Unit>::Assoc = ()], [], [adt FooStruct ], {}, {FooStruct}) }` failed at the following rule(s): - the rule "some" failed at step #0 (crates/formality-prove/src/prove/prove_wc_list.rs:28:14) because - judgment `prove_wc { goal: @ IsLocal(CoreTrait(::Assoc)), assumptions: {}, env: Env { variables: [], coherence_mode: true }, decls: decls(222, [trait CoreTrait , trait Unit ], [impl Unit(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Unit>::Assoc = ()], [], [adt FooStruct ], {}, {FooStruct}) }` failed at the following rule(s): - the rule "trait ref is local" failed at step #0 (crates/formality-prove/src/prove/prove_wc.rs:110:14) because - judgment `is_local_trait_ref { goal: CoreTrait(::Assoc), assumptions: {}, env: Env { variables: [], coherence_mode: true }, decls: decls(222, [trait CoreTrait , trait Unit ], [impl Unit(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Unit>::Assoc = ()], [], [adt FooStruct ], {}, {FooStruct}) }` failed at the following rule(s): - the rule "local parameter" failed at step #1 (crates/formality-prove/src/prove/is_local.rs:77:14) because - judgment `is_local_parameter { goal: ::Assoc, assumptions: {}, env: Env { variables: [], coherence_mode: true }, decls: decls(222, [trait CoreTrait , trait Unit ], [impl Unit(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Unit>::Assoc = ()], [], [adt FooStruct ], {}, {FooStruct}) }` failed at the following rule(s): - the rule "local parameter" failed at step #3 (crates/formality-prove/src/prove/is_local.rs:141:14) because - judgment `is_local_parameter { goal: (), assumptions: {}, env: Env { variables: [], coherence_mode: true }, decls: decls(222, [trait CoreTrait , trait Unit ], [impl Unit(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Unit>::Assoc = ()], [], [adt FooStruct ], {}, {FooStruct}) }` failed at the following rule(s): - the rule "fundamental rigid type" failed at step #0 (crates/formality-prove/src/prove/is_local.rs:148:17) because - condition evaluted to false: `is_fundamental(&decls, &name)` - &decls = decls(222, [trait CoreTrait , trait Unit ], [impl Unit(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Unit>::Assoc = ()], [], [adt FooStruct ], {}, {FooStruct}) - &name = tuple(0) - the rule "local trait" failed at step #0 (crates/formality-prove/src/prove/is_local.rs:70:17) because - condition evaluted to false: `decls.is_local_trait_id(&goal.trait_id)` - decls = decls(222, [trait CoreTrait , trait Unit ], [impl Unit(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Unit>::Assoc = ()], [], [adt FooStruct ], {}, {FooStruct}) - &goal.trait_id = CoreTrait diff --git a/tests/ui/coherence_orphan/covered_VecT.frs b/tests/ui/coherence_orphan/covered_VecT.frs deleted file mode 100644 index b054d6d7..00000000 --- a/tests/ui/coherence_orphan/covered_VecT.frs +++ /dev/null @@ -1,11 +0,0 @@ -//@check-pass -[ - crate core { - trait CoreTrait {} - struct Vec {} - }, - crate foo { - struct FooStruct {} - impl CoreTrait for Vec {} - } -] diff --git a/tests/ui/coherence_orphan/mirror_CoreStruct.frs b/tests/ui/coherence_orphan/mirror_CoreStruct.frs deleted file mode 100644 index b6ebb5e8..00000000 --- a/tests/ui/coherence_orphan/mirror_CoreStruct.frs +++ /dev/null @@ -1,17 +0,0 @@ -[ - crate core { - trait CoreTrait {} - struct CoreStruct {} - - trait Mirror { - type Assoc : []; - } - - impl Mirror for T { - type Assoc = T; - } - }, - crate foo { - impl CoreTrait for ::Assoc {} - } -] diff --git a/tests/ui/coherence_orphan/mirror_CoreStruct.stderr b/tests/ui/coherence_orphan/mirror_CoreStruct.stderr deleted file mode 100644 index 60113b62..00000000 --- a/tests/ui/coherence_orphan/mirror_CoreStruct.stderr +++ /dev/null @@ -1,24 +0,0 @@ -Error: orphan_check(impl CoreTrait for ::Assoc { }) - -Caused by: - judgment `prove_wc_list { goal: {@ IsLocal(CoreTrait(::Assoc))}, assumptions: {}, env: Env { variables: [], coherence_mode: true }, decls: decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): - the rule "some" failed at step #0 (crates/formality-prove/src/prove/prove_wc_list.rs:28:14) because - judgment `prove_wc { goal: @ IsLocal(CoreTrait(::Assoc)), assumptions: {}, env: Env { variables: [], coherence_mode: true }, decls: decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): - the rule "trait ref is local" failed at step #0 (crates/formality-prove/src/prove/prove_wc.rs:110:14) because - judgment `is_local_trait_ref { goal: CoreTrait(::Assoc), assumptions: {}, env: Env { variables: [], coherence_mode: true }, decls: decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): - the rule "local parameter" failed at step #1 (crates/formality-prove/src/prove/is_local.rs:77:14) because - judgment `is_local_parameter { goal: ::Assoc, assumptions: {}, env: Env { variables: [], coherence_mode: true }, decls: decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): - the rule "local parameter" failed at step #3 (crates/formality-prove/src/prove/is_local.rs:141:14) because - judgment `is_local_parameter { goal: CoreStruct, assumptions: {}, env: Env { variables: [], coherence_mode: true }, decls: decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): - the rule "fundamental rigid type" failed at step #0 (crates/formality-prove/src/prove/is_local.rs:148:17) because - condition evaluted to false: `is_fundamental(&decls, &name)` - &decls = decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], {}, {}) - &name = (adt CoreStruct) - the rule "local rigid type" failed at step #0 (crates/formality-prove/src/prove/is_local.rs:156:17) because - condition evaluted to false: `decls.is_local_adt_id(&a)` - decls = decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], {}, {}) - &a = CoreStruct - the rule "local trait" failed at step #0 (crates/formality-prove/src/prove/is_local.rs:70:17) because - condition evaluted to false: `decls.is_local_trait_id(&goal.trait_id)` - decls = decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], {}, {}) - &goal.trait_id = CoreTrait diff --git a/tests/ui/coherence_orphan/mirror_FooStruct.frs b/tests/ui/coherence_orphan/mirror_FooStruct.frs deleted file mode 100644 index d92ab188..00000000 --- a/tests/ui/coherence_orphan/mirror_FooStruct.frs +++ /dev/null @@ -1,18 +0,0 @@ -//@check-pass -[ - crate core { - trait CoreTrait {} - - trait Mirror { - type Assoc : []; - } - - impl Mirror for T { - type Assoc = T; - } - }, - crate foo { - struct FooStruct {} - impl CoreTrait for ::Assoc {} - } -] diff --git a/tests/ui/coherence_orphan/neg_CoreTrait_for_CoreStruct_in_Foo.frs b/tests/ui/coherence_orphan/neg_CoreTrait_for_CoreStruct_in_Foo.frs deleted file mode 100644 index 208512f7..00000000 --- a/tests/ui/coherence_orphan/neg_CoreTrait_for_CoreStruct_in_Foo.frs +++ /dev/null @@ -1,9 +0,0 @@ -[ - crate core { - trait CoreTrait {} - struct CoreStruct {} - }, - crate foo { - impl !CoreTrait for CoreStruct {} - } -] diff --git a/tests/ui/coherence_orphan/neg_CoreTrait_for_CoreStruct_in_Foo.stderr b/tests/ui/coherence_orphan/neg_CoreTrait_for_CoreStruct_in_Foo.stderr deleted file mode 100644 index 8ea95ce3..00000000 --- a/tests/ui/coherence_orphan/neg_CoreTrait_for_CoreStruct_in_Foo.stderr +++ /dev/null @@ -1,22 +0,0 @@ -Error: orphan_check_neg(impl ! CoreTrait for CoreStruct {}) - -Caused by: - judgment `prove_wc_list { goal: {@ IsLocal(CoreTrait(CoreStruct))}, assumptions: {}, env: Env { variables: [], coherence_mode: true }, decls: decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): - the rule "some" failed at step #0 (crates/formality-prove/src/prove/prove_wc_list.rs:28:14) because - judgment `prove_wc { goal: @ IsLocal(CoreTrait(CoreStruct)), assumptions: {}, env: Env { variables: [], coherence_mode: true }, decls: decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): - the rule "trait ref is local" failed at step #0 (crates/formality-prove/src/prove/prove_wc.rs:110:14) because - judgment `is_local_trait_ref { goal: CoreTrait(CoreStruct), assumptions: {}, env: Env { variables: [], coherence_mode: true }, decls: decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): - the rule "local parameter" failed at step #1 (crates/formality-prove/src/prove/is_local.rs:77:14) because - judgment `is_local_parameter { goal: CoreStruct, assumptions: {}, env: Env { variables: [], coherence_mode: true }, decls: decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): - the rule "fundamental rigid type" failed at step #0 (crates/formality-prove/src/prove/is_local.rs:148:17) because - condition evaluted to false: `is_fundamental(&decls, &name)` - &decls = decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], {}, {}) - &name = (adt CoreStruct) - the rule "local rigid type" failed at step #0 (crates/formality-prove/src/prove/is_local.rs:156:17) because - condition evaluted to false: `decls.is_local_adt_id(&a)` - decls = decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], {}, {}) - &a = CoreStruct - the rule "local trait" failed at step #0 (crates/formality-prove/src/prove/is_local.rs:70:17) because - condition evaluted to false: `decls.is_local_trait_id(&goal.trait_id)` - decls = decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], {}, {}) - &goal.trait_id = CoreTrait diff --git a/tests/ui/coherence_orphan/uncovered_T.frs b/tests/ui/coherence_orphan/uncovered_T.frs deleted file mode 100644 index 6082f558..00000000 --- a/tests/ui/coherence_orphan/uncovered_T.frs +++ /dev/null @@ -1,9 +0,0 @@ -[ - crate core { - trait CoreTrait {} - }, - crate foo { - struct FooStruct {} - impl CoreTrait for T {} - } -] diff --git a/tests/ui/coherence_orphan/uncovered_T.stderr b/tests/ui/coherence_orphan/uncovered_T.stderr deleted file mode 100644 index 2432395d..00000000 --- a/tests/ui/coherence_orphan/uncovered_T.stderr +++ /dev/null @@ -1,12 +0,0 @@ -Error: orphan_check(impl CoreTrait for ^ty0_0 { }) - -Caused by: - judgment `prove_wc_list { goal: {@ IsLocal(CoreTrait(!ty_0, FooStruct))}, assumptions: {}, env: Env { variables: [!ty_0], coherence_mode: true }, decls: decls(222, [trait CoreTrait ], [impl CoreTrait(^ty0_0, FooStruct)], [], [], [], [adt FooStruct ], {}, {FooStruct}) }` failed at the following rule(s): - the rule "some" failed at step #0 (crates/formality-prove/src/prove/prove_wc_list.rs:28:14) because - judgment `prove_wc { goal: @ IsLocal(CoreTrait(!ty_0, FooStruct)), assumptions: {}, env: Env { variables: [!ty_0], coherence_mode: true }, decls: decls(222, [trait CoreTrait ], [impl CoreTrait(^ty0_0, FooStruct)], [], [], [], [adt FooStruct ], {}, {FooStruct}) }` failed at the following rule(s): - the rule "trait ref is local" failed at step #0 (crates/formality-prove/src/prove/prove_wc.rs:110:14) because - judgment `is_local_trait_ref { goal: CoreTrait(!ty_0, FooStruct), assumptions: {}, env: Env { variables: [!ty_0], coherence_mode: true }, decls: decls(222, [trait CoreTrait ], [impl CoreTrait(^ty0_0, FooStruct)], [], [], [], [adt FooStruct ], {}, {FooStruct}) }` failed at the following rule(s): - the rule "local trait" failed at step #0 (crates/formality-prove/src/prove/is_local.rs:70:17) because - condition evaluted to false: `decls.is_local_trait_id(&goal.trait_id)` - decls = decls(222, [trait CoreTrait ], [impl CoreTrait(^ty0_0, FooStruct)], [], [], [], [adt FooStruct ], {}, {FooStruct}) - &goal.trait_id = CoreTrait diff --git a/tests/ui/coherence_overlap/T_where_Foo_not_u32_impls.frs b/tests/ui/coherence_overlap/T_where_Foo_not_u32_impls.frs deleted file mode 100644 index 9e3c2db0..00000000 --- a/tests/ui/coherence_overlap/T_where_Foo_not_u32_impls.frs +++ /dev/null @@ -1,12 +0,0 @@ -// Test positive impl that has a where-clause which checks for itself, -// i.e., `T: Foo where T: Foo`. This `T: Foo` where-clause isn't harmful -// in the coinductive interpretation of trait matching, it actually -// doesn't change the meaning of the impl at all. However, this formulation -// was erroneously accepted by an earlier variant of negative impls. -[ - crate core { - trait Foo {} - impl Foo for T where T: Foo {} - impl !Foo for u32 {} - } -] diff --git a/tests/ui/coherence_overlap/T_where_Foo_not_u32_impls.stderr b/tests/ui/coherence_overlap/T_where_Foo_not_u32_impls.stderr deleted file mode 100644 index f025f80d..00000000 --- a/tests/ui/coherence_overlap/T_where_Foo_not_u32_impls.stderr +++ /dev/null @@ -1,9 +0,0 @@ -Error: check_trait_impl(impl Foo for ^ty0_0 where ^ty0_0 : Foo { }) - -Caused by: - failed to disprove - {! Foo(!ty_1)} - given - {Foo(!ty_1)} - got - {Constraints { env: Env { variables: [?ty_1], coherence_mode: false }, known_true: true, substitution: {?ty_1 => u32} }} diff --git a/tests/ui/coherence_overlap/foo_crate_cannot_assume_CoreStruct_does_not_impl_CoreTrait.frs b/tests/ui/coherence_overlap/foo_crate_cannot_assume_CoreStruct_does_not_impl_CoreTrait.frs deleted file mode 100644 index 7331d51f..00000000 --- a/tests/ui/coherence_overlap/foo_crate_cannot_assume_CoreStruct_does_not_impl_CoreTrait.frs +++ /dev/null @@ -1,11 +0,0 @@ -[ - crate core { - trait CoreTrait {} - struct CoreStruct {} - }, - crate foo { - trait FooTrait {} - impl FooTrait for T where T: CoreTrait {} - impl FooTrait for CoreStruct {} - } -] diff --git a/tests/ui/coherence_overlap/foo_crate_cannot_assume_CoreStruct_does_not_impl_CoreTrait.stderr b/tests/ui/coherence_overlap/foo_crate_cannot_assume_CoreStruct_does_not_impl_CoreTrait.stderr deleted file mode 100644 index 34f60b86..00000000 --- a/tests/ui/coherence_overlap/foo_crate_cannot_assume_CoreStruct_does_not_impl_CoreTrait.stderr +++ /dev/null @@ -1,3 +0,0 @@ -Error: impls may overlap: -impl FooTrait for ^ty0_0 where ^ty0_0 : CoreTrait { } -impl FooTrait for CoreStruct { } diff --git a/tests/ui/coherence_overlap/neg_CoreTrait_for_CoreStruct_implies_no_overlap.frs b/tests/ui/coherence_overlap/neg_CoreTrait_for_CoreStruct_implies_no_overlap.frs deleted file mode 100644 index 632420b4..00000000 --- a/tests/ui/coherence_overlap/neg_CoreTrait_for_CoreStruct_implies_no_overlap.frs +++ /dev/null @@ -1,15 +0,0 @@ -//@check-pass -// Variant of foo_crate_cannot_assume_CoreStruct_does_not_impl_CoreTrait -// where there is a negative impl, so it is accepted. -[ - crate core { - trait CoreTrait {} - struct CoreStruct {} - impl !CoreTrait for CoreStruct {} - }, - crate foo { - trait FooTrait {} - impl FooTrait for T where T: CoreTrait {} - impl FooTrait for CoreStruct {} - } -] diff --git a/tests/ui/coherence_overlap/u32_T_impls.frs b/tests/ui/coherence_overlap/u32_T_impls.frs deleted file mode 100644 index ebd0cf4d..00000000 --- a/tests/ui/coherence_overlap/u32_T_impls.frs +++ /dev/null @@ -1,7 +0,0 @@ -[ - crate core { - trait Foo {} - impl Foo for u32 {} - impl Foo for T {} - } -] diff --git a/tests/ui/coherence_overlap/u32_T_impls.stderr b/tests/ui/coherence_overlap/u32_T_impls.stderr deleted file mode 100644 index 2ec470b1..00000000 --- a/tests/ui/coherence_overlap/u32_T_impls.stderr +++ /dev/null @@ -1,3 +0,0 @@ -Error: impls may overlap: -impl Foo for u32 { } -impl Foo for ^ty0_0 { } diff --git a/tests/ui/coherence_overlap/u32_T_where_T_Is_impls.frs b/tests/ui/coherence_overlap/u32_T_where_T_Is_impls.frs deleted file mode 100644 index c0abce62..00000000 --- a/tests/ui/coherence_overlap/u32_T_where_T_Is_impls.frs +++ /dev/null @@ -1,12 +0,0 @@ -// Test that we detect "indirect" overlap -- here `Foo` is implemented for `u32` -// and also all `T: Is`, and `u32: Is`. -[ - crate core { - trait Foo {} - impl Foo for u32 {} - impl Foo for T where T: Is {} - - trait Is {} - impl Is for u32 {} - } -] diff --git a/tests/ui/coherence_overlap/u32_T_where_T_Is_impls.stderr b/tests/ui/coherence_overlap/u32_T_where_T_Is_impls.stderr deleted file mode 100644 index aa6c5ed2..00000000 --- a/tests/ui/coherence_overlap/u32_T_where_T_Is_impls.stderr +++ /dev/null @@ -1,3 +0,0 @@ -Error: impls may overlap: -impl Foo for u32 { } -impl Foo for ^ty0_0 where ^ty0_0 : Is { } diff --git a/tests/ui/coherence_overlap/u32_T_where_T_Not_impls.frs b/tests/ui/coherence_overlap/u32_T_where_T_Not_impls.frs deleted file mode 100644 index ce525162..00000000 --- a/tests/ui/coherence_overlap/u32_T_where_T_Not_impls.frs +++ /dev/null @@ -1,15 +0,0 @@ -//@check-pass - -// Test that, within a crate, we are able to rely on the fact -// that `u32: Not` is not implemented. -// -// See also test_foo_crate_cannot_assume_CoreStruct_does_not_impl_CoreTrait -[ - crate core { - trait Foo {} - impl Foo for u32 {} - impl Foo for T where T: Not {} - - trait Not {} - } -] diff --git a/tests/ui/coherence_overlap/u32_i32_impls.frs b/tests/ui/coherence_overlap/u32_i32_impls.frs deleted file mode 100644 index e2fbc191..00000000 --- a/tests/ui/coherence_overlap/u32_i32_impls.frs +++ /dev/null @@ -1,8 +0,0 @@ -//@check-pass -[ - crate core { - trait Foo {} - impl Foo for u32 {} - impl Foo for i32 {} - } -] diff --git a/tests/ui/coherence_overlap/u32_not_u32_impls.frs b/tests/ui/coherence_overlap/u32_not_u32_impls.frs deleted file mode 100644 index 941b8550..00000000 --- a/tests/ui/coherence_overlap/u32_not_u32_impls.frs +++ /dev/null @@ -1,8 +0,0 @@ -// Test that a positive and negative impl for the same type (`u32`, here) is rejected. -[ - crate core { - trait Foo {} - impl Foo for u32 {} - impl !Foo for u32 {} - } -] diff --git a/tests/ui/coherence_overlap/u32_not_u32_impls.stderr b/tests/ui/coherence_overlap/u32_not_u32_impls.stderr deleted file mode 100644 index 364d8d5c..00000000 --- a/tests/ui/coherence_overlap/u32_not_u32_impls.stderr +++ /dev/null @@ -1,9 +0,0 @@ -Error: check_trait_impl(impl Foo for u32 { }) - -Caused by: - failed to disprove - {! Foo(u32)} - given - {} - got - {Constraints { env: Env { variables: [], coherence_mode: false }, known_true: true, substitution: {} }} diff --git a/tests/ui/coherence_overlap/u32_u32_impls.frs b/tests/ui/coherence_overlap/u32_u32_impls.frs deleted file mode 100644 index 59069e29..00000000 --- a/tests/ui/coherence_overlap/u32_u32_impls.frs +++ /dev/null @@ -1,7 +0,0 @@ -[ - crate core { - trait Foo {} - impl Foo for u32 {} - impl Foo for u32 {} - } -] diff --git a/tests/ui/coherence_overlap/u32_u32_impls.stderr b/tests/ui/coherence_overlap/u32_u32_impls.stderr deleted file mode 100644 index 1e241644..00000000 --- a/tests/ui/coherence_overlap/u32_u32_impls.stderr +++ /dev/null @@ -1 +0,0 @@ -Error: duplicate impl in current crate: impl Foo for u32 { } diff --git a/tests/ui/consts/generic_mismatch.frs b/tests/ui/consts/generic_mismatch.frs deleted file mode 100644 index 217d22b9..00000000 --- a/tests/ui/consts/generic_mismatch.frs +++ /dev/null @@ -1,7 +0,0 @@ -[ - crate Foo { - trait Foo where type_of_const C is bool {} - - impl Foo for u32 where type_of_const C is u32 {} - } -] diff --git a/tests/ui/consts/generic_mismatch.stderr b/tests/ui/consts/generic_mismatch.stderr deleted file mode 100644 index 882a9b77..00000000 --- a/tests/ui/consts/generic_mismatch.stderr +++ /dev/null @@ -1,16 +0,0 @@ -Error: check_trait_impl(impl Foo for u32 where type_of_const ^const0_0 is u32 { }) - -Caused by: - judgment `prove_wc_list { goal: {Foo(u32, const !const_0)}, assumptions: {@ ConstHasType(!const_0 , u32)}, env: Env { variables: [!const_0], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}], [impl Foo(u32, const ^const0_0) where {@ ConstHasType(^const0_0 , u32)}], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): - the rule "some" failed at step #0 (crates/formality-prove/src/prove/prove_wc_list.rs:28:14) because - judgment `prove_wc { goal: Foo(u32, const !const_0), assumptions: {@ ConstHasType(!const_0 , u32)}, env: Env { variables: [!const_0], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}], [impl Foo(u32, const ^const0_0) where {@ ConstHasType(^const0_0 , u32)}], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): - the rule "positive impl" failed at step #7 (crates/formality-prove/src/prove/prove_wc.rs:57:14) because - judgment `prove_after { constraints: Constraints { env: Env { variables: [!const_0, ?const_1], coherence_mode: false }, known_true: true, substitution: {?const_1 => const !const_0} }, goal: {@ ConstHasType(?const_1 , bool)}, assumptions: {@ ConstHasType(!const_0 , u32)}, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}], [impl Foo(u32, const ^const0_0) where {@ ConstHasType(^const0_0 , u32)}], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): - the rule "prove_after" failed at step #1 (crates/formality-prove/src/prove/prove_after.rs:19:14) because - judgment `prove_wc_list { goal: {@ ConstHasType(!const_0 , bool)}, assumptions: {@ ConstHasType(!const_0 , u32)}, env: Env { variables: [!const_0], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}], [impl Foo(u32, const ^const0_0) where {@ ConstHasType(^const0_0 , u32)}], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): - the rule "some" failed at step #0 (crates/formality-prove/src/prove/prove_wc_list.rs:28:14) because - judgment `prove_wc { goal: @ ConstHasType(!const_0 , bool), assumptions: {@ ConstHasType(!const_0 , u32)}, env: Env { variables: [!const_0], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}], [impl Foo(u32, const ^const0_0) where {@ ConstHasType(^const0_0 , u32)}], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): - the rule "const has ty" failed at step #0 (crates/formality-prove/src/prove/prove_wc.rs:123:43) because - pattern `Some((_, const_ty))` did not match value `None` - the rule "trait implied bound" failed at step #0 (crates/formality-prove/src/prove/prove_wc.rs:86:14) because - expression evaluated to an empty collection: `decls.trait_invariants()` diff --git a/tests/ui/consts/holds.frs b/tests/ui/consts/holds.frs deleted file mode 100644 index c1ac5ca2..00000000 --- a/tests/ui/consts/holds.frs +++ /dev/null @@ -1,8 +0,0 @@ -//@check-pass -[ - crate Foo { - trait Foo where type_of_const C is bool {} - - impl Foo for u32 {} - } -] diff --git a/tests/ui/consts/mismatch.frs b/tests/ui/consts/mismatch.frs deleted file mode 100644 index d3aad171..00000000 --- a/tests/ui/consts/mismatch.frs +++ /dev/null @@ -1,7 +0,0 @@ -[ - crate Foo { - trait Foo where type_of_const C is bool {} - - impl Foo for u32 {} - } -] diff --git a/tests/ui/consts/mismatch.stderr b/tests/ui/consts/mismatch.stderr deleted file mode 100644 index 5462ed60..00000000 --- a/tests/ui/consts/mismatch.stderr +++ /dev/null @@ -1,8 +0,0 @@ -Error: check_trait_impl(impl Foo for u32 { }) - -Caused by: - judgment `prove_wc_list { goal: {Foo(u32, const value(42, u32))}, assumptions: {}, env: Env { variables: [], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}], [impl Foo(u32, const value(42, u32))], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): - the rule "some" failed at step #0 (crates/formality-prove/src/prove/prove_wc_list.rs:28:14) because - judgment `prove_wc { goal: Foo(u32, const value(42, u32)), assumptions: {}, env: Env { variables: [], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}], [impl Foo(u32, const value(42, u32))], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): - the rule "trait implied bound" failed at step #0 (crates/formality-prove/src/prove/prove_wc.rs:86:14) because - expression evaluated to an empty collection: `decls.trait_invariants()` diff --git a/tests/ui/consts/multiple_type_of_const.frs b/tests/ui/consts/multiple_type_of_const.frs deleted file mode 100644 index b643b71c..00000000 --- a/tests/ui/consts/multiple_type_of_const.frs +++ /dev/null @@ -1,10 +0,0 @@ -/// This test is weird, but it's also not something rustc ever generates. -/// Types on const generics only get exactly one `type_of_const` bound. -/// Either way, it is still sound, because there is no constant that possibly -/// satisfies those bounds (similar to how there is no type that satisfies `Drop` + `Copy`). -//@check-pass -[ - crate Foo { - trait Foo where type_of_const C is bool, type_of_const C is u32 {} - } -] diff --git a/tests/ui/consts/nonsense_rigid_const_bound.frs b/tests/ui/consts/nonsense_rigid_const_bound.frs deleted file mode 100644 index d3d0f2bb..00000000 --- a/tests/ui/consts/nonsense_rigid_const_bound.frs +++ /dev/null @@ -1,7 +0,0 @@ -/// This test is the short version of `generic_mismatch`, skipping -/// substituting and directly going to a wrong constant. -[ - crate Foo { - trait Foo where type_of_const true is u32 {} - } -] diff --git a/tests/ui/consts/nonsense_rigid_const_bound.stderr b/tests/ui/consts/nonsense_rigid_const_bound.stderr deleted file mode 100644 index a022eaef..00000000 --- a/tests/ui/consts/nonsense_rigid_const_bound.stderr +++ /dev/null @@ -1,23 +0,0 @@ -Error: check_trait(Foo) - -Caused by: - 0: prove_where_clause_well_formed(type_of_const value(0, bool) is u32) - 1: judgment `prove_wc_list { goal: {u32 = bool}, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): - the rule "some" failed at step #0 (crates/formality-prove/src/prove/prove_wc_list.rs:28:14) because - judgment `prove_wc { goal: u32 = bool, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): - the rule "assumption" failed at step #1 (crates/formality-prove/src/prove/prove_wc.rs:44:14) because - judgment had no applicable rules: `prove_via { goal: u32 = bool, via: @ ConstHasType(value(0, bool) , u32), assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` - the rule "eq" failed at step #0 (crates/formality-prove/src/prove/prove_wc.rs:96:14) because - judgment `prove_eq { a: u32, b: bool, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): - the rule "normalize-l" failed at step #0 (crates/formality-prove/src/prove/prove_eq.rs:68:14) because - judgment `prove_normalize { p: u32, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): - the rule "normalize-via-assumption" failed at step #1 (crates/formality-prove/src/prove/prove_normalize.rs:27:14) because - judgment had no applicable rules: `prove_normalize_via { goal: u32, via: @ ConstHasType(value(0, bool) , u32), assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` - the rule "symmetric" failed at step #0 (crates/formality-prove/src/prove/prove_eq.rs:38:14) because - judgment `prove_eq { a: bool, b: u32, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): - the rule "normalize-l" failed at step #0 (crates/formality-prove/src/prove/prove_eq.rs:68:14) because - judgment `prove_normalize { p: bool, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): - the rule "normalize-via-assumption" failed at step #1 (crates/formality-prove/src/prove/prove_normalize.rs:27:14) because - judgment had no applicable rules: `prove_normalize_via { goal: bool, via: @ ConstHasType(value(0, bool) , u32), assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` - the rule "symmetric" failed at step #0 (crates/formality-prove/src/prove/prove_eq.rs:38:14) because - cyclic proof attempt: `prove_eq { a: u32, b: bool, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], coherence_mode: false }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` diff --git a/tests/ui/consts/ok.frs b/tests/ui/consts/ok.frs deleted file mode 100644 index e5311ebe..00000000 --- a/tests/ui/consts/ok.frs +++ /dev/null @@ -1,9 +0,0 @@ -//@check-pass -[ - crate Foo { - trait Foo where type_of_const C is bool {} - trait Bar where type_of_const C is u32 {} - - impl Foo for u32 where type_of_const C is bool {} - } -] diff --git a/tests/ui/consts/rigid_const_bound.frs b/tests/ui/consts/rigid_const_bound.frs deleted file mode 100644 index 4a0856ff..00000000 --- a/tests/ui/consts/rigid_const_bound.frs +++ /dev/null @@ -1,8 +0,0 @@ -/// This test is the short version of `holds`, skipping -/// substituting and directly going to a rigid constant. -//@check-pass -[ - crate Foo { - trait Foo where type_of_const true is bool {} - } -] diff --git a/tests/ui/decl_safety/safe_trait-negative_impl_mismatch.frs b/tests/ui/decl_safety/safe_trait-negative_impl_mismatch.frs deleted file mode 100644 index cad4149a..00000000 --- a/tests/ui/decl_safety/safe_trait-negative_impl_mismatch.frs +++ /dev/null @@ -1,6 +0,0 @@ -[ - crate baguette { - trait Foo {} - unsafe impl !Foo for u32 {} - } -] diff --git a/tests/ui/decl_safety/safe_trait-negative_impl_mismatch.stderr b/tests/ui/decl_safety/safe_trait-negative_impl_mismatch.stderr deleted file mode 100644 index 00127498..00000000 --- a/tests/ui/decl_safety/safe_trait-negative_impl_mismatch.stderr +++ /dev/null @@ -1,4 +0,0 @@ -Error: check_neg_trait_impl(unsafe impl ! Foo for u32 {}) - -Caused by: - negative impls cannot be unsafe diff --git a/tests/ui/decl_safety/safe_trait.frs b/tests/ui/decl_safety/safe_trait.frs deleted file mode 100644 index dd6610a4..00000000 --- a/tests/ui/decl_safety/safe_trait.frs +++ /dev/null @@ -1,7 +0,0 @@ -//@check-pass -[ - crate baguette { - safe trait Foo {} - safe impl Foo for u32 {} - } -] diff --git a/tests/ui/decl_safety/safe_trait_mismatch.frs b/tests/ui/decl_safety/safe_trait_mismatch.frs deleted file mode 100644 index 7a2f8d41..00000000 --- a/tests/ui/decl_safety/safe_trait_mismatch.frs +++ /dev/null @@ -1,6 +0,0 @@ -[ - crate baguette { - trait Foo {} - unsafe impl Foo for u32 {} - } -] diff --git a/tests/ui/decl_safety/safe_trait_mismatch.stderr b/tests/ui/decl_safety/safe_trait_mismatch.stderr deleted file mode 100644 index 374a2982..00000000 --- a/tests/ui/decl_safety/safe_trait_mismatch.stderr +++ /dev/null @@ -1,4 +0,0 @@ -Error: check_trait_impl(unsafe impl Foo for u32 { }) - -Caused by: - implementing the trait `Foo` is not unsafe diff --git a/tests/ui/decl_safety/unsafe_trait-negative_impl.frs b/tests/ui/decl_safety/unsafe_trait-negative_impl.frs deleted file mode 100644 index a1fdf102..00000000 --- a/tests/ui/decl_safety/unsafe_trait-negative_impl.frs +++ /dev/null @@ -1,7 +0,0 @@ -//@check-pass -[ - crate baguette { - unsafe trait Foo {} - impl !Foo for u32 {} - } -] diff --git a/tests/ui/decl_safety/unsafe_trait-negative_impl_mismatch.frs b/tests/ui/decl_safety/unsafe_trait-negative_impl_mismatch.frs deleted file mode 100644 index 2ba98a14..00000000 --- a/tests/ui/decl_safety/unsafe_trait-negative_impl_mismatch.frs +++ /dev/null @@ -1,6 +0,0 @@ -[ - crate baguette { - unsafe trait Foo {} - unsafe impl !Foo for u32 {} - } -] diff --git a/tests/ui/decl_safety/unsafe_trait-negative_impl_mismatch.stderr b/tests/ui/decl_safety/unsafe_trait-negative_impl_mismatch.stderr deleted file mode 100644 index 00127498..00000000 --- a/tests/ui/decl_safety/unsafe_trait-negative_impl_mismatch.stderr +++ /dev/null @@ -1,4 +0,0 @@ -Error: check_neg_trait_impl(unsafe impl ! Foo for u32 {}) - -Caused by: - negative impls cannot be unsafe diff --git a/tests/ui/decl_safety/unsafe_trait.frs b/tests/ui/decl_safety/unsafe_trait.frs deleted file mode 100644 index f93b0dac..00000000 --- a/tests/ui/decl_safety/unsafe_trait.frs +++ /dev/null @@ -1,7 +0,0 @@ -//@check-pass -[ - crate baguette { - unsafe trait Foo {} - unsafe impl Foo for u32 {} - } -] diff --git a/tests/ui/decl_safety/unsafe_trait_mismatch.frs b/tests/ui/decl_safety/unsafe_trait_mismatch.frs deleted file mode 100644 index 48c1b0cd..00000000 --- a/tests/ui/decl_safety/unsafe_trait_mismatch.frs +++ /dev/null @@ -1,6 +0,0 @@ -[ - crate baguette { - unsafe trait Foo {} - impl Foo for u32 {} - } -] diff --git a/tests/ui/decl_safety/unsafe_trait_mismatch.stderr b/tests/ui/decl_safety/unsafe_trait_mismatch.stderr deleted file mode 100644 index 662e2398..00000000 --- a/tests/ui/decl_safety/unsafe_trait_mismatch.stderr +++ /dev/null @@ -1,4 +0,0 @@ -Error: check_trait_impl(impl Foo for u32 { }) - -Caused by: - the trait `Foo` requires an `unsafe impl` declaration diff --git a/tests/ui/fn/lifetime.frs b/tests/ui/fn/lifetime.frs deleted file mode 100644 index 59716040..00000000 --- a/tests/ui/fn/lifetime.frs +++ /dev/null @@ -1,7 +0,0 @@ -// Test lifetimes on function -[ - crate Foo { - // fn one_lt_arg<'a, T>(_: &'a T) -> () {} - fn one_lt_arg(&a T) -> () { trusted } - } -] diff --git a/tests/ui/fn/lifetime.stderr b/tests/ui/fn/lifetime.stderr deleted file mode 100644 index 937b530f..00000000 --- a/tests/ui/fn/lifetime.stderr +++ /dev/null @@ -1,5 +0,0 @@ -Error: judgment `prove_wc_list { goal: {@ wf(&!lt_0 !ty_1)}, assumptions: {}, env: Env { variables: [!lt_0, !ty_1], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "some" failed at step #0 (crates/formality-prove/src/prove/prove_wc_list.rs:28:14) because - judgment `prove_wc { goal: @ wf(&!lt_0 !ty_1), assumptions: {}, env: Env { variables: [!lt_0, !ty_1], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "parameter well formed" failed at step #0 (crates/formality-prove/src/prove/prove_wc.rs:117:14) because - judgment had no applicable rules: `prove_wf { goal: &!lt_0 !ty_1, assumptions: {}, env: Env { variables: [!lt_0, !ty_1], coherence_mode: false }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` diff --git a/tests/ui/fn/ok.frs b/tests/ui/fn/ok.frs deleted file mode 100644 index 8925cf45..00000000 --- a/tests/ui/fn/ok.frs +++ /dev/null @@ -1,20 +0,0 @@ -// Test functions, function's arguments, and function's returns -//@check-pass -[ - crate Foo { - // fn simple_fn() {} - fn simple_fn() -> () { trusted } - - // fn one_arg(_: T) {} - fn one_arg(T) -> () { trusted } - - // fn one_ret(_: T) {} - fn one_ret() -> T { trusted } - - // fn arg_ret(_: T) -> U {} - fn arg_ret(T) -> U { trusted } - - // fn multi_arg_ret(_: T, _: Y) -> (U, I) {} - fn multi_arg_ret(T, Y) -> (U, I) { trusted } - } -] diff --git a/tests/ui/hello_world.frs b/tests/ui/hello_world.frs deleted file mode 100644 index 6b035c1e..00000000 --- a/tests/ui/hello_world.frs +++ /dev/null @@ -1,15 +0,0 @@ -//@check-pass -[ - crate Foo { - trait Foo where T: Bar, Self: Baz {} - - trait Bar where T: Baz {} - - trait Baz {} - - impl Baz for u32 {} - - impl Bar for u32 {} - impl Bar for () where T: Baz {} - } -] diff --git a/tests/ui/hello_world_fail.frs b/tests/ui/hello_world_fail.frs deleted file mode 100644 index 69ca1485..00000000 --- a/tests/ui/hello_world_fail.frs +++ /dev/null @@ -1,9 +0,0 @@ -[ - crate Foo { - trait Foo where T: Bar {} - - trait Bar where T: Baz {} - - trait Baz {} - } -] diff --git a/tests/ui/hello_world_fail.stderr b/tests/ui/hello_world_fail.stderr deleted file mode 100644 index 17442cc2..00000000 --- a/tests/ui/hello_world_fail.stderr +++ /dev/null @@ -1,13 +0,0 @@ -Error: check_trait(Foo) - -Caused by: - 0: prove_where_clause_well_formed(!ty_2 : Bar ) - 1: judgment `prove_wc_list { goal: {@ WellFormedTraitRef(Bar(!ty_0, !ty_1))}, assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [trait Foo where {Bar(^ty0_1, ^ty0_0)}, trait Bar where {Baz(^ty0_1)}, trait Baz ], [], [], [], [], [], {Bar, Baz, Foo}, {}) }` failed at the following rule(s): - the rule "some" failed at step #0 (crates/formality-prove/src/prove/prove_wc_list.rs:28:14) because - judgment `prove_wc { goal: @ WellFormedTraitRef(Bar(!ty_0, !ty_1)), assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [trait Foo where {Bar(^ty0_1, ^ty0_0)}, trait Bar where {Baz(^ty0_1)}, trait Baz ], [], [], [], [], [], {Bar, Baz, Foo}, {}) }` failed at the following rule(s): - the rule "trait well formed" failed at step #2 (crates/formality-prove/src/prove/prove_wc.rs:104:14) because - judgment `prove_wc_list { goal: {Baz(!ty_1)}, assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [trait Foo where {Bar(^ty0_1, ^ty0_0)}, trait Bar where {Baz(^ty0_1)}, trait Baz ], [], [], [], [], [], {Bar, Baz, Foo}, {}) }` failed at the following rule(s): - the rule "some" failed at step #0 (crates/formality-prove/src/prove/prove_wc_list.rs:28:14) because - judgment `prove_wc { goal: Baz(!ty_1), assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], coherence_mode: false }, decls: decls(222, [trait Foo where {Bar(^ty0_1, ^ty0_0)}, trait Bar where {Baz(^ty0_1)}, trait Baz ], [], [], [], [], [], {Bar, Baz, Foo}, {}) }` failed at the following rule(s): - the rule "trait implied bound" failed at step #0 (crates/formality-prove/src/prove/prove_wc.rs:86:14) because - expression evaluated to an empty collection: `decls.trait_invariants()` diff --git a/tests/ui/parser.frs b/tests/ui/parser.frs deleted file mode 100644 index d2e35fb2..00000000 --- a/tests/ui/parser.frs +++ /dev/null @@ -1,5 +0,0 @@ -[ - crate Foo { - trait Baz where cake {} - } -] diff --git a/tests/ui/parser.stderr b/tests/ui/parser.stderr deleted file mode 100644 index 5b943336..00000000 --- a/tests/ui/parser.stderr +++ /dev/null @@ -1,13 +0,0 @@ -Error: expected `:` - -Caused by: - 0: {} - } - ] - - 1: failed to parse [ - crate Foo { - trait Baz where cake {} - } - ] -