TraitTypes support

[franziskuskiefer]

Using trait types doesn't work when the trait is used in a type bound or in any other way.

trait T {
    type C;
    fn new() -> Self::C;
}
struct S {}
impl T for S {
    type C = [u8; 4];

    fn new() -> Self::C {
        Self::C::default()
    }
}

fn fun<Type: T>() {}

fn caller() {
    fun::<S>();
}

fn associated_type() -> [u8; 4] {
     S::new()
}

generates

void eurydice_tests_caller(void)
{
  KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n",
    __FILE__,
    __LINE__,
    "Eurydice error: Failure(\"TODO: TraitTypes Self::C\")\n");
  KRML_HOST_EXIT(255U);
}

void eurydice_tests_associated_type(uint8_t ret[4U])
{
  KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n",
    __FILE__,
    __LINE__,
    "Eurydice error: Failure(\"TODO: TraitTypes eurydice_tests::{eurydice_tests::T for eurydice_tests::S}::C\")\n");
  KRML_HOST_EXIT(255U);
}

[Nadrieril]

Will get fixed by AeneasVerif/charon#127.

[franziskuskiefer]

Great! Do you have an ETA for those changes?

[Nadrieril]

This month if all goes well, the next if not.

[msprotz]

@franziskuskiefer and I had a chat this morning, and considering that Franziskus has a workaround already (and contrary to what I said earlier), I am now dropping this and will let you fix it upstream -- it's only a matter of weeks, not worth the extra complexity