#[extern_spec]
mod alloc {
    #[flux::refined_by]
    struct Vec<T>;
    
    impl<T> Vec<T> {
        ...
    }
}


#[flux::refined_by()]
struct alloc::Vec<T>;

#[extern_spec(alloc::vec)]
impl<T> Vec<T> {
    ...
}

=>
#[flux::extern_spec]
mod flux_extern_spec_impl_alloc_vec {
    use alloc::vec::Vec;
    
    &self -> &Vec<T>
    self: &Vec<T>
    
    #[flux::sig(fn(&self[@n], aaaa))]
    fn len(self: &Vec<T>, aaaa ) -> usize
    
}


impl<T> Vec<T> {
    #[flux::sig(self: &Vec<T>[@n]) -> usize[n]]
    fn len(&self, x: Option<T>) -> usize;
}

usize -> Res::PrimTy
Option -> Res::Struct(DefId)
Vec -> Res::Struct(DefId)

=> 
mod dummy_mod {
    use alloc::vec;
}

#[extern_spec(alloc)]
mod vec {

}

// use alloc::vec::Vec;
#[extern_spec(alloc::vec::Vec)]
#[flux::sig(fn(v: &alloc::vec::Vec<T>) -> usize)]
fn len(v: &alloc::vec::Vec<T>) -> usize;

#[extern_spec(alloc::vec)]
impl<T> Vec<T> {
    #[flux::sig(fn(&Vec<T>[@n]) -> usize[n])]
    fn len(self: &Vec<T>) -> usize
    // we can allow the below by desugaring it to the above
    fn len(&self) -> usize
}

=>

// mangle the impl name and convert it to a mod
mod flux_extern_spec_impl_alloc_vec {
    // insert the full mod path and drop the generics
    use alloc::vec::Vec;
    
    #[flux::extern_spec]
    #[flux::sig(fn(&Vec<T>[@n]) -> usize[n])]
    // need to mangle the name of self
    fn len(flux_spec_self: &Vec<T>) -> usize {
        // Vec<T> inserted below as part of the mod_path
        alloc::vec::Vec<T>::len(flux_spec_self)
        
    }
}