Bug: poly items show up in names with `--monomorphize`

[ssyram]

The following codes produce Not_found error in the main function when calls Charon with --monomorphize. This seems to be something to do with the NameMatcher mechanism.

trait SomeTrait {
    fn some_method(&self);
}

struct Point<T> { x : i32, y : u64, z : T }

impl SomeTrait for Point<i32> {
    fn some_method(&self) {
        assert!(self.x > 0 && self.y < 100 && self.z != 0);
    }
}

fn main() {
    let p = Point { x: 10, y: 50, z: 1 };
    p.some_method();
}

[Nadrieril]

Thanks for the minimized bug! I can reproduce it, and I understand it: we're keeping the impl around after monomorphization, and it referes to the polymorphic version of Point, which doesn't exist after monomorphization. That's definitely a bug.

[ssyram]

Thanks for the quick pinpointing! I spent an hour or two tracking this issue but was still not very clear about how this comes.