Merge pull request #559 from Nadrieril/fix-assertion

charon/src/transform/expand_associated_types.rs

@@ -819,10 +819,14 @@ impl<'a> ComputeItemModifications<'a> {
                 let generics = ItemBinder::new(CurrentItem, generics);
                 if let Some(set_for_clause) = self.compute_assoc_tys_for_impl(*clause_impl_id) {
                     for (path, ty) in set_for_clause.iter() {
-                        let ty = ItemBinder::new(*clause_impl_id, ty)
-                            .substitute(generics)
-                            .under_current_binder();
-                        out.push((path, ty));
+                        // Keep only the paths that apply to the current trait ref, i.e. ignore
+                        // paths on the local clauses of the impl.
+                        if matches!(path.tref.base, BaseClause::SelfClause) {
+                            let ty = ItemBinder::new(*clause_impl_id, ty)
+                                .substitute(generics)
+                                .under_current_binder();
+                            out.push((path, ty));
+                        }
                     }
                 }
             }

charon/tests/ui.rs

@@ -184,6 +184,7 @@ fn perform_test(test_case: &Case, action: Action) -> anyhow::Result<()> {
     cmd.arg("--print-llbc");
     cmd.arg("--crate=test_crate");
     cmd.arg("--rustc-flag=--crate-type=rlib");
+    cmd.arg("--rustc-flag=--allow=unused"); // Removes noise
     cmd.arg("--input");
     cmd.arg(&test_case.input_path);
 

charon/tests/ui/generic-associated-types.out

@@ -40,14 +40,6 @@ error: Error during trait resolution: Found unsupported GAT `Item` when resolvin
    |                            ^^^^^^^^^^^
    |
 
-warning: unused variable: `x`
-  --> tests/ui/generic-associated-types.rs:35:9
-   |
-35 |     let x = 42;
-   |         ^ help: if this is intentional, prefix it with an underscore: `_x`
-   |
-   = note: `#[warn(unused_variables)]` on by default
-
 error: Generic associated types are not supported
   --> tests/ui/generic-associated-types.rs:48:9
    |
@@ -76,6 +68,4 @@ error: Error during trait resolution: Found unsupported GAT `Type` when resolvin
    |         ^^^^^^^
    |
 
-warning: 1 warning emitted
-
 ERROR Charon failed to translate this code (10 errors)

charon/tests/ui/simple/supertrait-impl-with-assoc-type-constraint.out

@@ -0,0 +1,45 @@
+# Final LLBC before serialization:
+
+trait core::marker::Sized<Self>
+
+trait test_crate::HasAssoc<Self>
+{
+    parent_clause0 : [@TraitClause0]: core::marker::Sized<Self::Assoc>
+    type Assoc
+}
+
+trait test_crate::SuperTrait<Self>
+
+trait test_crate::Trait<Self>
+{
+    parent_clause0 : [@TraitClause0]: test_crate::SuperTrait<Self>
+}
+
+impl<T> test_crate::{impl test_crate::SuperTrait for T}<T> : test_crate::SuperTrait<T>
+where
+    [@TraitClause0]: test_crate::HasAssoc<T>,
+    [@TraitClause1]: core::marker::Sized<T>,
+    @TraitClause0::Assoc = (),
+
+impl<T> test_crate::{impl test_crate::Trait for T}#1<T> : test_crate::Trait<T>
+where
+    [@TraitClause0]: test_crate::HasAssoc<T>,
+    [@TraitClause1]: core::marker::Sized<T>,
+    @TraitClause0::Assoc = (),
+{
+    parent_clause0 = test_crate::{impl test_crate::SuperTrait for T}<T>[@TraitClause0, @TraitClause1]
+}
+
+fn test_crate::main()
+{
+    let @0: (); // return
+    let @1: (); // anonymous local
+
+    @1 := ()
+    @0 := move (@1)
+    @0 := ()
+    return
+}
+
+
+

charon/tests/ui/simple/supertrait-impl-with-assoc-type-constraint.rs

@@ -0,0 +1,11 @@
+trait HasAssoc {
+    type Assoc;
+}
+
+trait SuperTrait {}
+trait Trait: SuperTrait {}
+
+impl<T> SuperTrait for T where T: HasAssoc<Assoc = ()> {}
+impl<T> Trait for T where T: HasAssoc<Assoc = ()> {}
+
+fn main() {}