This pr already helps a ton, although there are still some dyn trait related crashes when I try to apply it to Tock. So far, I've seen one main crash that I've minimized it down to:

struct Cow {}

trait CowContainer<'a> {
    fn get_cow(&self) -> &'a Cow;
}

pub struct CowCell<'a> {
    inner: &'a dyn CowContainer<'a>,
}

When you run flux on this code, it errors with:
error: internal compiler error: crates/flux-fhir-analysis/src/conv/mod.rs:444:13: unexpected! conv_poly_dyn_trait_ref

Which points to this code:

Comparing this code to other code that passes, it appears that that the problem is that the the trait being parameterized by the dyn trait has a lifetime parameter. Let me know if you need any other info

I'll probably have some time to look at this tomorrow

Found one more issue: dyn traits are not implemented as possible return values.
If you attempt to verify the code

trait Animal {
    fn noise(&self);
}

#[flux::trusted]
fn get_animal() -> &dyn Animal {
    unimplemented!()
}

It will error with:
thread 'rustc' panicked at crates/flux-middle/src/rty/mod.rs:1160:45: not yet implemented
which points to the code:

@enjhnsn2 are you sure about the second one, it seems to work fine for me:

rjhala@pozole ~/r/flux (dyn)> more tests/tests/todo/dyn02.rs 
pub trait Animal {
    fn noise(&self);
}

#[flux::trusted]
pub fn get_animal() -> &'static dyn Animal {
    unimplemented!()
}
rjhala@pozole ~/r/flux (dyn)> cargo xtask run tests/tests/todo/dyn02.rs
    Finished `dev` profile [unoptimized   debuginfo] target(s) in 0.02s
     Running `target/debug/xtask run tests/tests/todo/dyn02.rs`
$ export FLUX_BUILD_SYSROOT=1
$ cargo build -p flux-rs
    Finished `dev` profile [unoptimized   debuginfo] target(s) in 0.02s
$ cargo build
    Finished `dev` profile [unoptimized   debuginfo] target(s) in 0.06s

@enjhnsn2 - the above two things work now, see

• https://github.com/flux-rs/flux/blob/dyn/tests/tests/pos/surface/dyn02.rs
• https://github.com/flux-rs/flux/blob/dyn/tests/tests/pos/surface/dyn03.rs

pub trait Animal {
fn noise(&self);
}

#[flux::trusted]
pub fn get_animal() -> &'static dyn Animal {
unimplemented!()
}

Whoops, I think I may have messed up the minimization for that one. When I was minimizing I started with tock code that pulled in the tock kernel and I think the error was in the dependency, not the minimized code. Let me try to get a better example

Alright, I found a minimized example that triggers the error. Unfortunately its a little more complicated:

pub trait Animal {
    fn noise(&self);
}

fn apply_closure_to_animal<F>(closure: F, animal: &'static dyn Animal)
where
    F: FnOnce(&dyn Animal),
{
    closure(animal);
}

This bug isn't too frequent and is possible to work around, so I don't think you should block this pr on it.

Alright, I found a minimized example that triggers the error. Unfortunately its a little more complicated:

pub trait Animal {
    fn noise(&self);
}

fn apply_closure_to_animal<F>(closure: F, animal: &'static dyn Animal)
where
    F: FnOnce(&dyn Animal),
{
    closure(animal);
}

This bug isn't too frequent and is possible to work around, so I don't think you should block this pr on it.

This feels it'll fail for various reasons not just dynamic objects. I'd prefer if we don't fix it in this PR.

Ok I think I've fixed the TraitObject/Dynamic mismatch ...

This bug isn't too frequent and is possible to work around, so I don't think you should block this pr on it.

This feels it'll fail for various reasons not just dynamic objects. I'd prefer if we don't fix it in this PR.

@nilehmann -- it turns out that for @enjhnsn2 example with closure and dyn above (see issue #666) -- just filling out the todo! case for Dynamic in the to_rustc(...) fixes #666 i.e. gets this to not crash, so I just tacked it onto this PR since its very much related to the whole conversion to/from ExistentialPredicate/ExistentialTraitRef that is the bulk of this PR...

Ok I think I addressed all the issues above -- except the

We are putting Dynamic in BaseTy which means they can be indexed (by unit as returned by this function),

But I'm pretty certain that's (for now at least) the sensible choice - as in dyn you have to forget all about the underlying concrete type; I suggest we revisit this later if we have reason to (or if we think there's some use-case for indexing Dynamic values...)