Unexpected name clash

[sonmarcho]

Reported by Anders Larsson in the zulip:

pub fn byteToWord (n: u8) -> u16 {
    n.into()
}

triggers:

[Info ] Generated the partial file (because of errors): ./Mylib.lean
[Error] Name clash detected: the following identifiers are bound to the same name "core.convert.Into":
- trait_decl_id: 0
  Source: '/rustc/65ea825f4021eaf77f1b25139969712d65b435a4/library/core/src/convert/mod.rs', lines 444:0-444:24
- trait_impl_id: 0
  Source: '/rustc/65ea825f4021eaf77f1b25139969712d65b435a4/library/core/src/convert/mod.rs', lines 444:0-444:24
You may want to rename some of your definitions, or report an issue.
[Error] Error when registering the name for id: trait_impl_id: 0:
The chosen name is already in the names set: core.convert.Into
Source: '/rustc/65ea825f4021eaf77f1b25139969712d65b435a4/library/core/src/convert/mod.rs', lines 444:0-444:24

[Nadrieril]

For context, the llbc for that is:

trait core::convert::From<Self, T>
{
    fn from : core::convert::From::from
}

trait core::convert::Into<Self, T>
{
    fn into : core::convert::Into::into
}

fn core::convert::{impl core::convert::Into<U> for T#3}::into<T, U>(@1: T) -> U
where
    // Inherited clauses:
    [@TraitClause0]: core::convert::From<U, T>,

impl<T, U> core::convert::{impl core::convert::Into<U> for T#3}<T, U> : core::convert::Into<T, U>
where
    [@TraitClause0]: core::convert::From<U, T>,
{
    fn into = core::convert::{impl core::convert::Into<U> for T#3}::into
}

fn core::convert::num::{impl core::convert::From<u8> for u16#40}::from(@1: u8) -> u16

impl core::convert::num::{impl core::convert::From<u8> for u16#40} : core::convert::From<u16, u8>
{
    fn from = core::convert::num::{impl core::convert::From<u8> for u16#40}::from
}

fn core::convert::Into::into<Self, T>(@1: Self) -> T

fn test_crate::byteToWord(@1: u8) -> u16
{
    let @0: u16; // return
    let n@1: u8; // arg #1
    let @2: u8; // anonymous local

    @2 := copy (n@1)
    @0 := core::convert::{impl core::convert::Into<U> for T#3}<u8, u16>[core::convert::num::{impl core::convert::From<u8> for u16#40}]::into(move (@2))
    drop @2
    return
}

fn core::convert::From::from<Self, T>(@1: T) -> Self

[Nadrieril]

This imports the very generic impl:

impl<T, U> Into<U> for T
where
    U: From<T>,
{ ... }

My guess is that the name you generate for that is core.convert.Into which is the same as the trait name.

[sonmarcho]

Generally speaking, that's slightly annoying.
But here the fix is simple: we need to add hand-written for those (because they should be part of the standard library), and by doing so get get to choose the name. I'll do that later.

[sonmarcho]

Thanks for investigating btw!

[sonmarcho]

I'm closing this because I solved it for the specific issue above, and I opened a more general issue: #380