Concrete trait impl checks

[Trzyq0712]

Instead of using axiomatized version of the trait check encoding, we will instead use a function with a concrete body.

This makes it clearer which types implement a specific trait without having to resort to making "negative implementations" for types that do not.

• Change encoding from axioms to concrete functions
• Unknown types
• Implementation blocks with trait bounds
• Support for projections with type generics

  impl<T: Foo<i32, Item = bool>> Bar for T {}

  let T_impl == (Self_trait) in
  Self_trait == T_impl &&
  Foo_impl(T_impl) && 
  Foo_assoc_Item(T_impl, i32_type()) == bool_type()
  

• Support for projections with const generics

  impl<T, const N: usize> Bar for T
  where
      T: Foo<CONST = { N }>,
      T: Baz<C = { N }>,
  {}

  let T_impl == (Self_trait) in
  let N_impl == (Foo_assoc_const_CONST(T_impl)) in
  Self_trait == T_impl &&
  Foo_assoc_const_CONST(T_impl) == N_impl && 
  Baz_assoc_const_C(T_impl) == N_impl && 
  Baz_impl(T_impl) && Foo_impl(T_impl)
  

[Aurel300]

@JonasAlaif Do we really want to go with existentials for the generics? It makes sense semantically but (apart from vaguely worrying about performance) I wonder if we need this at all? From our previous discussion about this I assumed it suffices to do, e.g., with struct Foo<T> { ... } and struct Bar<T> { ... }:

• type.is_Foo to encode that Foo<T> implements the trait;
• type.is_Foo && type.Foo_T1.is_i32 (or whatever the names are) to encode that Foo<i32> implements it;
• type.is_Foo && type.Foo_T1.is_Bar to encode that Foo<Bar<T>> implements it; and etc.

[Trzyq0712]

@JonasAlaif Do we really want to go with existentials for the generics? It makes sense semantically but (apart from vaguely worrying about performance) I wonder if we need this at all? From our previous discussion about this I assumed it suffices to do, e.g., with struct Foo<T> { ... } and struct Bar<T> { ... }:

* `type.is_Foo` to encode that `Foo<T>` implements the trait;

* `type.is_Foo && type.Foo_T1.is_i32` (or whatever the names are) to encode that `Foo<i32>` implements it;

* `type.is_Foo && type.Foo_T1.is_Bar` to encode that `Foo<Bar<T>>` implements it; and etc.

I started implementing it that way, but then ran into some issues in more complicated cases. For example this "legal" impl block:

impl<U, V: Foo<U>> Foo<U> for V {}

I would try to encode it as:

function Foo_impl(Self: Type, T: Type): Bool {
    (...)
    Foo_impl(Self, U) // What do we actually put for U
    (...)
}

Even to get to this one has to do some "thinking" and simplifying.

Additionally, the discriminator + destructor style encoding makes it much more verbose for more complex types, for example impl ... for ((i32, bool), (u32, i32, i64)). Though, this is a rather minor concern.

Lastly, I have simply found this easier to implement 😞.

[Trzyq0712]

One other issue that popped up is the Sized trait. Whenever there is a generic, the Sized constraint is automatically added. As the Sized trait is auto-implemented for all types by default, there are no actual impls for Sized making all our types !Sized by default. We can either always skip the Sized bounds, or make special-case it to be implemented by all types. What do you think?

[Trzyq0712]

I believe this is now a mostly final version for the encoding. Ready for review.

[Aurel300]

As the Sized trait is auto-implemented for all types by default, there are no actual impls for Sized making all our types !Sized by default.

Is this the case only for Sized? What about other (user-defined) auto traits? What about the other built-in ones, like Send or Sync?

Besides the minor comments, I worry a bit about:

• The fact that we have so much machinery for dealing with Sized trait specifically; the CanonicalTy seems to only exist for that, right?
• All the type disassembling and reassembling going on in trait_impls is quite a lot of logic.
• How much of this is rebase-able on #127 (if you know)? Some of the changes in traits.rs and trait_impls.rs seem quite similar to that PR's.

[Trzyq0712]

Is this the case only for Sized? What about other (user-defined) auto traits? What about the other built-in ones, like Send or Sync?

It's most certainly the case for other auto-traits too. I am implementing the Sized trait in this PR as Sized constraint is auto-added to all generics by default. The other auto-traits should be implemented later on.

* The fact that we have so much machinery for dealing with `Sized` trait specifically; the `CanonicalTy` seems to only exist for that, right?

Have mostly merged the logic of CanonicalTy into identity_for_ty. The Sized check is based on the check performed by the compiler in a private function.

* All the type disassembling and reassembling going on in `trait_impls` is quite a lot of logic.

It's quite complicated indeed. Without existentials, we need to "discover" an expression to which we can bind each generic instead and then assert equivalences between subsequent occurrences of the generic.

A way to do this differently would be to introduce the generics using let-expressions. This would reduce the visual clutter of repeating long accessor paths at the cost of more equality assertions. Additionally, with let-bindings for the impl block generics, we could now process the predicates in any order, and would avoid the dependencies between the projections.

* How much of this is rebase-able on #127 (if you know)? Some of the changes in `traits.rs` and `trait_impls.rs` seem quite similar to that PR's.

I tried to mimic or copy #127 where I have found it to do similar things. This could be probably improved.

[Aurel300]

This is not very nice. You say "temporary", what does the proper solution look like?

[Trzyq0712]

We have discussed with @JonasAlaif about the proper solution which would be to have an internal representation of GenericArgs and clauses. For now, we are wrapping it in an accessor, so it should not be used for other purposes.

The main reason why we have the ty::Ty here in the first place is to allow greater reuse between the special trait encoders and TraitImplsEnc::impl_block_check by passing it "fake" implementations to generate checks for the special traits.

[Aurel300]

(See comment: #154 (comment))

[JonasAlaif]

It would be nice if we could do that, but in the current architecture we don't have a nice way to do that no?

[Aurel300]

Not without small changes, so I guess you are suggesting to go ahead with this version for this PR?

[JonasAlaif]

What small changes do you mean? I think it would require a fundamental addition to the TaskEncoder stuff where something is encoded iff it's required from two different encoders. Concretely, here we only want to generate an impl_Sized function if we need to call it somewhere (e.g. due to refine_spec), but as soon as that happens we want to generate it for all inputs to TyConstructorEnc (past and future). That is, one might have the following sequence:

deps.require_ref::<TyConstructorEnc>("TypeA");
deps.require_ref::<TyConstructorEnc>("TypeB");
deps.require_dep::<SizedTraitEnc>(); // Needs to look at past inputs to TyConstructorEnc, but also subscribe to future ones
deps.require_ref::<TyConstructorEnc>("TypeC");
deps.require_ref::<TyConstructorEnc>("TypeD");

[Aurel300]

I think the linked comment explained this, no? In this case, the SizedTraitEnc would only create an identifier for the impl function as its "full" output. The work of encoding the actual impl function would happen in emit_outputs. I think the "small change" I mean would just be a new function in the task encoder API that returns all the task keys that have been requested by a(nother) task encoder.

[Trzyq0712]

I have tried to do it this way. The main issue is that we are not allowed to use the any dependencies, so we cannot use TraitImplEnc::impl_block_check. We could then try to write an ad-hoc sizedness check.

An alternative, partial solution would be to still collect all types by enqueuing them from TyConstructorEnc, but only emitting the outputs if TraitEnc was called with the Sized trait.
This could be done by adding another request type to SizedTraitEnc:

enum SizedTraitEncTask<'vir> {
  Activate,
  EncodyType(RustTy<'vir>),
}
// inside the encoder
type TaskDescription<'vir> = SizedTraitEncTask<'vir>;

[Trzyq0712]

I think I will pull out the builtin trait logic out of this PR, so we can actually focus on the trait impls instead. In retrospect, it does not fit the PR in the first place.

[Aurel300]

I would prefer that you don't expose new functions that just give you the identifier when they are not "definitely" coming from an encoding request. Request the encoding of Sized from TraitEnc in do_encode_full and include the result (or the identifiers you need) in the full output? The task encoder output is cached anyway, the allocation you make by calling trait_impl_idn isn't.

[Trzyq0712]

Is this what you had in mind?

[Trzyq0712]

Not sure if this is the more correct thing to do for Dynamic.

[JonasAlaif]

I would probably keep it with ty::TyKind::Never and those. Though we'd need to differentiate the name for different traits (rather than "Dyn")

[Trzyq0712]

I just worry about the fact that with Never and others we don't do any erasure -- we just pass the original ty as the erased one. This might introduce key collisions between different Dyn types.

[JonasAlaif]

But that's the thing, I think that they should be different types. We already have this with other Opaque types having different names, resulting in different keys.

[Trzyq0712]

Yes, but the ty_name function gives them the exact same names. This will, as a result, produce naming conflicts in the TyConstructorEnc. Before, there would only ever be one outputed, as all RustTy of dyns would be indistinguishable.

[JonasAlaif]

That's what I meant by

Though we'd need to differentiate the name for different traits (rather than "Dyn")

in my first comment

[Aurel300]

This bit I find rather messy. Is the invariant here that only type declarations will be in the impl_params map? Can there not be conflicts? Can you add a comment to explain this? Either way matching on a Result (and why Result::Ok instead of just Ok?) here seems strange, I would expect Option maybe? There is no actual error occurring here...

[Trzyq0712]

The matching on Result stems from how GenericParams map each generic to a generic type or const (probably it should have been a custom enum there in the first place to avoid confusion).