Merge pull request #590 from Nadrieril/assoc-ty-defaults

Misc fixes

Author: Nadrieril

charon/src/bin/charon-driver/translate/translate_ctx.rs

@@ -852,8 +852,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
     ) -> TraitImplId {
         let id = id.into();
         // Register the corresponding trait early so we can filter on its name.
-        {
-            let def = self.hax_def(id).expect("hax failed when translating item");
+        if let Ok(def) = self.hax_def(id) {
             let hax::FullDefKind::TraitImpl { trait_pred, .. } = def.kind() else {
                 unreachable!()
             };

charon/src/bin/charon/main.rs

@@ -67,7 +67,7 @@ struct Toolchain {
 impl Toolchain {
     fn is_installed(&self) -> anyhow::Result<bool> {
         // FIXME: check if the right components are installed.
-        let output = self.run("echo").output()?;
+        let output = self.run("rustc").arg("--version").output()?;
         Ok(output.status.success())
     }
 

charon/src/transform/expand_associated_types.rs

@@ -935,7 +935,13 @@ impl UpdateItemBody<'_> {
                 self.lookup_path_on_trait_ref(&path, parent)
             }
             TraitRefKind::ItemClause(..) => {
-                unreachable!("item clause should have been removed in a previous pass")
+                register_error!(
+                    self.ctx,
+                    self.span,
+                    "Found unhandled item clause; \
+                    this is a bug unless the clause is coming from a GAT."
+                );
+                None
             }
             TraitRefKind::BuiltinOrAuto {
                 parent_trait_refs,

charon/tests/ui/gat-causes-unhandled-ty-clause.out

@@ -0,0 +1,37 @@
+error: Generic associated types are not supported
+ --> tests/ui/gat-causes-unhandled-ty-clause.rs:4:5
+  |
+4 |     type GAT<T>;
+  |     ^^^^^^^^^^^
+  |
+
+error: Item `test_crate::HasGAT` caused errors; ignoring.
+ --> tests/ui/gat-causes-unhandled-ty-clause.rs:3:1
+  |
+3 | trait HasGAT {
+  | ^^^^^^^^^^^^
+  |
+
+error: Found unhandled item clause; this is a bug unless the clause is coming from a GAT.
+  --> tests/ui/gat-causes-unhandled-ty-clause.rs:12:1
+   |
+12 | / fn floatify<C>() -> <C::Friend as HasAssoc>::Assoc
+13 | | where
+...  |
+16 | |     todo!()
+17 | | }
+   | |_^
+   |
+
+error: Found unhandled item clause; this is a bug unless the clause is coming from a GAT.
+  --> tests/ui/gat-causes-unhandled-ty-clause.rs:12:1
+   |
+12 | / fn floatify<C>() -> <C::Friend as HasAssoc>::Assoc
+13 | | where
+...  |
+16 | |     todo!()
+17 | | }
+   | |_^
+   |
+
+ERROR Charon failed to translate this code (4 errors)

charon/tests/ui/gat-causes-unhandled-ty-clause.rs

@@ -0,0 +1,17 @@
+//@ known-failure
+//! Regression test minimized from the rustc test suite. This used to cause a panic.
+trait HasGAT {
+    type GAT<T>;
+    type Friend: HasAssoc;
+}
+
+trait HasAssoc {
+    type Assoc;
+}
+
+fn floatify<C>() -> <C::Friend as HasAssoc>::Assoc
+where
+    C: HasGAT,
+{
+    todo!()
+}

charon/tests/ui/simple/gat-default.out

@@ -0,0 +1,25 @@
+thread 'rustc' panicked at /rustc/86d69c705a552236a622eee3fdea94bf13c5f102/compiler/rustc_type_ir/src/binder.rs:697:9:
+type parameter `U/#1` (U/#1/1) out of range when instantiating, args=[()]
+note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
+error: Hax panicked when translating `test_crate::{impl#0}`.
+ --> tests/ui/simple/gat-default.rs:9:1
+  |
+9 | impl Collection for () {}
+  | ^^^^^^^^^^^^^^^^^^^^^^
+  |
+
+error: Generic associated types are not supported
+ --> tests/ui/simple/gat-default.rs:6:5
+  |
+6 |     type Sibling<U> = Vec<U>;
+  |     ^^^^^^^^^^^^^^^
+  |
+
+error: Item `test_crate::Collection` caused errors; ignoring.
+ --> tests/ui/simple/gat-default.rs:5:1
+  |
+5 | trait Collection {
+  | ^^^^^^^^^^^^^^^^
+  |
+
+ERROR Charon failed to translate this code (3 errors)

charon/tests/ui/simple/gat-default.rs

@@ -0,0 +1,11 @@
+//@ known-failure
+//! Test associated type defaults with parameters
+#![feature(associated_type_defaults)]
+
+trait Collection {
+    type Sibling<U> = Vec<U>;
+}
+
+impl Collection for () {}
+
+fn main() {}