pub fn storable(
ty: &Ty,
types: &BTreeMap<Arc<str>, TyDecl>,
) -> Result<(), NotSendable>Expand description
May a value of this type be written to the log?
Strictly stronger than sendable: a rendered view can cross a boundary — that is what a patch
stream is — but it cannot be stored, because replay must reconstruct it rather than read it
back. docs/19-phase-1-report.md §19.9 predicted this:
the runtime refusal in value_to_repr was “the right thing to have while the proof is missing”,
and this is the proof. The refusal stays, now unreachable from a program that compiles.