@nikomatsakis

I don't quite follow this last example

You mean this? Which part is confusing? All I am saying is: there are cases where PhantomEmbedded is needed for soundness (PantomIndirect would be unsound), and at least one such case has been found in the wild by that paper.

I was thinking that there are kind of 3 levels here

I can't follow what you mean by these levels. Are these different user-defined types, using different fields to encode different things they need from the language? Or are these different proposals for how the language works? The three items are too terse for me to understand what each case actually refers to.

I understand you to be opposed to 'logical', I believe because of its interaction with opsem. I guess that you don't want to have to think about what traits are implemented to understand whether some memory is part of a cell and hence determine whether something is UB. Is that correct?

Roughly, yes. What we currently do in the aliasing model to find out which parts of the data behind a shared reference allow mutation is the following:

• Recursively traverse product types (tuples, structs, closure environments, ...)
  • When we hit UnsafeCell, the inside of it is mutable
  • When we hit a union or enum, stop the recursion. This is immutable if and only of if it is NoCell
  • Everything else is immutable

If we allow unsafe impl NoCell, we'll want to change this, though I am not entirely sure how. Does such an impl always "win" over all the inner types? I.e., we could have

• Recursively traverse product types (tuples, structs, closure environments, ...)
  • If this type is NoCell, stop the recursion, everything here is immutable
  • When we hit UnsafeCell, the inside of it is mutable
  • When we hit a union or enum, the inside is mutable (since we already ensured !NoCell)
  • Everything else is immutable

I find this a bit harder to think about, but maybe that's just a matter of habit. It also means this unsafe impl NoCell is really quite unsafe -- if any of the types you use for your fields uses interior mutability now or in a future semver-compatible version, it will be UB to call those operations based on an &YourType reference. It makes me quite uneasy, and while I'm certainly willing to consider it in the future, I don't think we have strong enough motivation for it right now. All we need is PhantomEmbedded and PhantomIndirect (one of which should be called PhantomData, and IMO that should be PhantomEmbedded, but the main point is having both of those types).

(I guess in this case it would be library UB, though?)

Everything the aliasing model does must be language UB. Are we talking about the same thing?

I don't know your take on what I called "phantom".

I don't understand what you are proposing here so I can't answer this question.^^ PhantomData<T>: NoCell sounds like you mean this to be true for all T but that was the main point of "materialized", no? I think you'll need to use more than those 22 characters to describe this option. :)

@riking

The safety proof of the unsafe impl would be that no values are ever constructed with the Cell-containing enum variants, which is a whole-program property.

No, the safety requirement would be that no mutation happens. Just constructing the Cell should be entirely fine.

Stacked Borrows is not happy with this, but that's a (hard to fix) Stacked Borrows bug which should not affect our decision here. Tree Borrows fixes this bug, so there are plausible models that do not have this problem.

@Jules-Bertholet

No, it merely needs to be an underapproximation of what codegen cares about. This leaves crate authors freedom to evolve their crate by delaying a commitment to NoCell.

Agreed. However. if unsafe impl NoCell is something users can write and is intended to have opsem consequences (bring back noalias to shared references), then opsem must treat NoCell as the exact truth, not some underapproximation.

If it does not have opsem consequences, we have the very strange situation where we'll put const promoted data into immutable memory for types where opsem may actually permit mutation through shared references. I think we should not do that -- it would basically be more of rust-lang/unsafe-code-guidelines#493.