Feature request: support TypeId

[N1ark]

Charon currently doesn't support TypeId, a special Rust type that allows identifying types via a hash; while at runtime they're just a u128, they are more complicated than that at compile-time, having their own dedicated global type.

We should handle them in Charon, adding a new GlobalKind::TypeId(Ty)

example of code:

use std::any::{Any, TypeId};

fn is_string<T: ?Sized + Any>(_s: &T) -> bool {
    TypeId::of::<String>() == TypeId::of::<T>()
}
fn main() {
    assert_eq!(is_string(&0), false);
    assert_eq!(is_string(&"cookie monster".to_string()), true);
}

In particular, the function TypeId::of currently translates to:

pub fn of::<String>() -> TypeId
{
    let @0: TypeId; // return
    let @1: TypeId; // anonymous local

    bb0: {
        storage_live(@1);
        @1 := core::intrinsics::type_id::<String>() -> bb1 (unwind: bb2);
    }

    bb1: {
        @0 := move (@1);
        return;
    }

    bb2: {
        unwind_continue;
    }
}

I wonder if there is a nice way we can resolve calls to core::intrinsics::type_id::<T> into instead a global TYPE_ID::<T>. This would allow clients to reuse the globals system to deduplicate typeids, rather than having to track locally which types had their type id generated. The global for the typeid would then have GlobalKind::TypeId(Ty), and their body would be the above function.

[Nadrieril]

Sounds good, would you mind writing a few code samples that you'd like to support?

[N1ark]

edited :)

[Nadrieril]

Hmmm, I'm not certain that the equality I use to deduplicate globals is guaranteed to match the one used for TypeId. E.g. there might be shenanigans with higher-kinded function pointers, or I may equate two types just because they use a type I don't translate faithfully yet. And this would be soundness-bearing.

If we can manage that then piggy-backing on mono deduplication is very cute, I'd like that.